[Merged by Bors] - chore(*): remove some deprecated theorems

Mathlib/Analysis/InnerProductSpace/Calculus.lean

@@ -395,12 +395,7 @@ theorem Homeomorph.contDiff_unitBall : ContDiff ℝ n fun x : E => (unitBall x :
   PartialHomeomorph.contDiff_univUnitBall
 #align cont_diff_homeomorph_unit_ball Homeomorph.contDiff_unitBall
 
-@[deprecated PartialHomeomorph.contDiffOn_univUnitBall_symm (since := "2023-07-26")]
-theorem Homeomorph.contDiffOn_unitBall_symm {f : E → E}
-    (h : ∀ (y) (hy : y ∈ ball (0 : E) 1), f y = Homeomorph.unitBall.symm ⟨y, hy⟩) :
-    ContDiffOn ℝ n f <| ball 0 1 :=
-  PartialHomeomorph.contDiffOn_univUnitBall_symm.congr h
-#align cont_diff_on_homeomorph_unit_ball_symm Homeomorph.contDiffOn_unitBall_symm
+#align cont_diff_on_homeomorph_unit_ball_symm PartialHomeomorph.contDiffOn_univUnitBall_symm
 
 namespace PartialHomeomorph
 

Mathlib/Logic/Basic.lean

@@ -1167,19 +1167,9 @@ theorem exists_mem_or_left :
   exact Iff.trans (exists_congr fun x ↦ or_and_right) exists_or
 #align bex_or_left_distrib exists_mem_or_left
 
-@[deprecated (since := "2023-03-23")] alias not_ball_of_bex_not := not_forall₂_of_exists₂_not
-@[deprecated (since := "2023-03-23")] alias Decidable.not_ball := Decidable.not_forall₂
-@[deprecated (since := "2023-03-23")] alias not_ball := not_forall₂
-@[deprecated (since := "2023-03-23")] alias ball_true_iff := forall₂_true_iff
-@[deprecated (since := "2023-03-23")] alias ball_and := forall₂_and
-@[deprecated (since := "2023-03-23")] alias not_bex := not_exists_mem
-@[deprecated (since := "2023-03-23")] alias bex_or := exists_mem_or
-@[deprecated (since := "2023-03-23")] alias ball_or_left := forall₂_or_left
-@[deprecated (since := "2023-03-23")] alias bex_or_left := exists_mem_or_left
-
 end BoundedQuantifiers
 
-#align classical.not_ball not_ball
+#align classical.not_ball not_forall₂
 
 section ite
 

Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

@@ -890,15 +890,7 @@ theorem exists_measurable_piecewise {ι} [Countable ι] [Nonempty ι] (t : ι 
     simp only [dif_pos (mem_iUnion.2 ⟨i, hx⟩)]
     exact iUnionLift_of_mem ⟨x, mem_iUnion.2 ⟨i, hx⟩⟩ hx
 
-/-- Given countably many disjoint measurable sets `t n` and countably many measurable
-functions `g n`, one can construct a measurable function that coincides with `g n` on `t n`. -/
-@[deprecated exists_measurable_piecewise (since := "2023-02-11")]
-theorem exists_measurable_piecewise_nat {m : MeasurableSpace α} (t : ℕ → Set β)
-    (t_meas : ∀ n, MeasurableSet (t n)) (t_disj : Pairwise (Disjoint on t)) (g : ℕ → β → α)
-    (hg : ∀ n, Measurable (g n)) : ∃ f : β → α, Measurable f ∧ ∀ n x, x ∈ t n → f x = g n x :=
-  exists_measurable_piecewise t t_meas g hg <| t_disj.mono fun i j h => by
-    simp only [h.inter_eq, eqOn_empty]
-#align exists_measurable_piecewise_nat exists_measurable_piecewise_nat
+#align exists_measurable_piecewise_nat exists_measurable_piecewise
 
 end Prod
 

Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

@@ -123,11 +123,7 @@ protected theorem MeasurableSet.iUnion [Countable ι] ⦃f : ι → Set α⦄
     exact m.measurableSet_iUnion _ fun _ => h _
 #align measurable_set.Union MeasurableSet.iUnion
 
-@[deprecated MeasurableSet.iUnion (since := "2023-02-06")]
-theorem MeasurableSet.biUnion_decode₂ [Encodable β] ⦃f : β → Set α⦄ (h : ∀ b, MeasurableSet (f b))
-    (n : ℕ) : MeasurableSet (⋃ b ∈ decode₂ β n, f b) :=
-  .iUnion fun _ => .iUnion fun _ => h _
-#align measurable_set.bUnion_decode₂ MeasurableSet.biUnion_decode₂
+#align measurable_set.bUnion_decode₂ MeasurableSet.iUnion
 
 protected theorem MeasurableSet.biUnion {f : β → Set α} {s : Set β} (hs : s.Countable)
     (h : ∀ b ∈ s, MeasurableSet (f b)) : MeasurableSet (⋃ b ∈ s, f b) := by

Mathlib/MeasureTheory/Measure/NullMeasurable.lean

@@ -142,11 +142,7 @@ protected theorem iUnion {ι : Sort*} [Countable ι] {s : ι → Set α}
   MeasurableSet.iUnion h
 #align measure_theory.null_measurable_set.Union MeasureTheory.NullMeasurableSet.iUnion
 
-@[deprecated iUnion (since := "2023-05-06")]
-protected theorem biUnion_decode₂ [Encodable ι] ⦃f : ι → Set α⦄ (h : ∀ i, NullMeasurableSet (f i) μ)
-    (n : ℕ) : NullMeasurableSet (⋃ b ∈ Encodable.decode₂ ι n, f b) μ :=
-  .iUnion fun _ => .iUnion fun _ => h _
-#align measure_theory.null_measurable_set.bUnion_decode₂ MeasureTheory.NullMeasurableSet.biUnion_decode₂
+#align measure_theory.null_measurable_set.bUnion_decode₂ MeasureTheory.NullMeasurableSet.iUnion
 
 protected theorem biUnion {f : ι → Set α} {s : Set ι} (hs : s.Countable)
     (h : ∀ b ∈ s, NullMeasurableSet (f b) μ) : NullMeasurableSet (⋃ b ∈ s, f b) μ :=

Mathlib/NumberTheory/SumFourSquares.lean

@@ -92,13 +92,7 @@ theorem exists_sq_add_sq_add_one_eq_mul (p : ℕ) [hp : Fact p.Prime] :
   · exact (mul_le_mul' le_rfl hb).trans_lt (Nat.mul_div_lt_iff_not_dvd.2 hodd.not_two_dvd_nat)
   · exact lt_of_le_of_ne hp.1.two_le (hodd.ne_two_of_dvd_nat (dvd_refl _)).symm
   · exact hp.1.pos
-
-@[deprecated exists_sq_add_sq_add_one_eq_mul (since := "2023-06-04")]
-theorem exists_sq_add_sq_add_one_eq_k (p : ℕ) [Fact p.Prime] :
-    ∃ (a b : ℤ) (k : ℕ), a ^ 2 + b ^ 2 + 1 = k * p ∧ k < p :=
-  let ⟨a, b, k, _, hkp, hk⟩ := exists_sq_add_sq_add_one_eq_mul p
-  ⟨a, b, k, mod_cast hk, hkp⟩
-#align int.exists_sq_add_sq_add_one_eq_k Int.exists_sq_add_sq_add_one_eq_k
+#align int.exists_sq_add_sq_add_one_eq_k Int.exists_sq_add_sq_add_one_eq_mul
 
 end Int
 

Mathlib/Topology/Algebra/WithZeroTopology.lean

@@ -172,9 +172,7 @@ scoped instance (priority := 100) t5Space : T5Space Γ₀ where
       rwa [(isOpen_iff.2 (.inl ht)).nhdsSet_eq, disjoint_nhdsSet_principal]
     · rwa [(isOpen_iff.2 (.inl hs)).nhdsSet_eq, disjoint_principal_nhdsSet]
 
-/-- The topology on a linearly ordered group with zero element adjoined is T₃. -/
-@[deprecated t5Space (since := "2023-03-17")] lemma t3Space : T3Space Γ₀ := inferInstance
-#align with_zero_topology.t3_space WithZeroTopology.t3Space
+#align with_zero_topology.t3_space WithZeroTopology.t5Space
 
 /-- The topology on a linearly ordered group with zero element adjoined makes it a topological
 monoid. -/

Mathlib/Topology/FiberBundle/Trivialization.lean

@@ -592,9 +592,7 @@ theorem coe_mem_source : ↑y ∈ e'.source ↔ b ∈ e'.baseSet :=
   e'.mem_source
 #align trivialization.coe_mem_source Trivialization.coe_mem_source
 
-@[deprecated PartialHomeomorph.open_target (since := "2023-03-10")]
-theorem open_target' : IsOpen e'.target := e'.open_target
-#align trivialization.open_target Trivialization.open_target'
+#align trivialization.open_target PartialHomeomorph.open_target
 
 @[simp, mfld_simps]
 theorem coe_coe_fst (hb : b ∈ e'.baseSet) : (e' y).1 = b :=

Mathlib/Topology/Instances/EReal.lean

@@ -242,15 +242,7 @@ theorem continuousAt_add {p : EReal × EReal} (h : p.1 ≠ ⊤ ∨ p.2 ≠ ⊥)
 
 instance : ContinuousNeg EReal := ⟨negOrderIso.continuous⟩
 
-/-- Negation on `EReal` as a homeomorphism -/
-@[deprecated Homeomorph.neg (since := "2023-03-14")]
-def negHomeo : EReal ≃ₜ EReal :=
-  negOrderIso.toHomeomorph
-#align ereal.neg_homeo EReal.negHomeo
-
-@[deprecated continuous_neg (since := "2023-03-14")]
-protected theorem continuous_neg : Continuous fun x : EReal => -x :=
-  continuous_neg
-#align ereal.continuous_neg EReal.continuous_neg
+#align ereal.neg_homeo Homeomorph.neg
+#align ereal.continuous_neg ContinuousNeg.continuous_neg
 
 end EReal

Mathlib/Topology/Instances/Real.lean

@@ -106,20 +106,13 @@ theorem Real.uniformContinuous_abs : UniformContinuous (abs : ℝ → ℝ) :=
     ⟨ε, ε0, lt_of_le_of_lt (abs_abs_sub_abs_le_abs_sub _ _)⟩
 #align real.uniform_continuous_abs Real.uniformContinuous_abs
 
-@[deprecated continuousAt_inv₀ (since := "2023-03-06")]
-theorem Real.tendsto_inv {r : ℝ} (r0 : r ≠ 0) : Tendsto (fun q => q⁻¹) (𝓝 r) (𝓝 r⁻¹) :=
-  continuousAt_inv₀ r0
-#align real.tendsto_inv Real.tendsto_inv
+#align real.tendsto_inv HasContinuousInv₀.continuousAt_inv₀
 
 theorem Real.continuous_inv : Continuous fun a : { r : ℝ // r ≠ 0 } => a.val⁻¹ :=
   continuousOn_inv₀.restrict
 #align real.continuous_inv Real.continuous_inv
 
-@[deprecated Continuous.inv₀ (since := "2023-03-06")]
-theorem Real.Continuous.inv [TopologicalSpace α] {f : α → ℝ} (h : ∀ a, f a ≠ 0)
-    (hf : Continuous f) : Continuous fun a => (f a)⁻¹ :=
-  hf.inv₀ h
-#align real.continuous.inv Real.Continuous.inv
+#align real.continuous.inv Continuous.inv₀
 
 theorem Real.uniformContinuous_const_mul {x : ℝ} : UniformContinuous (x * ·) :=
   uniformContinuous_const_smul x
@@ -135,9 +128,7 @@ theorem Real.uniformContinuous_mul (s : Set (ℝ × ℝ)) {r₁ r₂ : ℝ}
       Hδ (H _ a.2).1 (H _ b.2).2 h₁ h₂⟩
 #align real.uniform_continuous_mul Real.uniformContinuous_mul
 
-@[deprecated continuous_mul (since := "2023-03-06")]
-protected theorem Real.continuous_mul : Continuous fun p : ℝ × ℝ => p.1 * p.2 := continuous_mul
-#align real.continuous_mul Real.continuous_mul
+#align real.continuous_mul continuous_mul
 
 -- Porting note: moved `TopologicalRing` instance up
 
@@ -197,12 +188,7 @@ theorem Periodic.compact_of_continuous [TopologicalSpace α] {f : ℝ → α} {c
   rw [← hp.image_uIcc hc 0]
   exact isCompact_uIcc.image hf
 #align function.periodic.compact_of_continuous Function.Periodic.compact_of_continuous
-
-@[deprecated Function.Periodic.compact_of_continuous (since := "2023-03-06")]
-theorem Periodic.compact_of_continuous' [TopologicalSpace α] {f : ℝ → α} {c : ℝ} (hp : Periodic f c)
-    (hc : 0 < c) (hf : Continuous f) : IsCompact (range f) :=
-  hp.compact_of_continuous hc.ne' hf
-#align function.periodic.compact_of_continuous' Function.Periodic.compact_of_continuous'
+#align function.periodic.compact_of_continuous' Function.Periodic.compact_of_continuous
 
 /-- A continuous, periodic function is bounded. -/
 theorem Periodic.isBounded_of_continuous [PseudoMetricSpace α] {f : ℝ → α} {c : ℝ}