unreviewed

Author: YaelDillies

Mathlib/Analysis/Complex/PhragmenLindelof.lean

@@ -765,7 +765,8 @@ theorem eq_zero_on_right_half_plane_of_superexponential_decay (hd : DiffContOnCl
   -- Due to continuity, it suffices to prove the equality on the open right half-plane.
   suffices ∀ z : ℂ, 0 < z.re → f z = 0 by
     simpa only [closure_setOfPred_lt_re] using!
-      EqOn.of_subset_closure this hd.continuousOn continuousOn_const subset_closure Subset.rfl
+      EqOn.of_subset_closure (s := {z | 0 < z.re}) (fun z hz ↦ this z hz)
+        hd.continuousOn continuousOn_const subset_closure Subset.rfl
   -- Consider $g_n(z)=e^{nz}f(z)$.
   set g : ℕ → ℂ → E := fun (n : ℕ) (z : ℂ) => exp z ^ n • f z
   have hg : ∀ n z, ‖g n z‖ = expR z.re ^ n * ‖f z‖ := fun n z ↦ by

Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean

@@ -244,7 +244,7 @@ protected theorem IsOpen.balancedHull [ContinuousConstSMul 𝕜 E] {s : Set E} (
     · exact ⟨1, by simp, by simpa [Set.zero_smul_set ⟨0, hzero⟩]⟩
     · use r
   rw [balancedHull, this]
-  exact isOpen_biUnion (fun r hr ↦ hs.smul₀ hr.2)
+  exact isOpen_biUnion (s := {r : 𝕜 | ‖r‖ ≤ 1 ∧ r ≠ 0}) (fun r hr ↦ hs.smul₀ hr.2)
 
 -- We don't have a `NontriviallyNormedDivisionRing`, so we use a `NeBot` assumption instead
 variable [NeBot (𝓝[≠] (0 : 𝕜))]

Mathlib/Analysis/LocallyConvex/Polar.lean

@@ -220,7 +220,7 @@ alias polarSubmodule_eq_setOf := polarSubmodule_eq_setOfPred
 
 lemma mem_polarSubmodule {S : Type*} [SetLike S E] [SMulMemClass S 𝕜 E] (m : S)
     (y : StrongDual 𝕜 E) : y ∈ polarSubmodule 𝕜 m ↔ ∀ x ∈ m, y x = 0 :=
-  propext_iff.mp congr($(polarSubmodule_eq_setOfPred 𝕜 m) y)
+  Set.ext_iff.mp (polarSubmodule_eq_setOfPred 𝕜 m) y
 
 @[simp]
 theorem zero_mem_polar (s : Set E) : (0 : StrongDual 𝕜 E) ∈ polar 𝕜 s :=

Mathlib/Analysis/LocallyConvex/Separation.lean

@@ -66,8 +66,8 @@ theorem separate_convex_open_set [TopologicalSpace E] [AddCommGroup E] [IsTopolo
       (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_isOpen hs₂ hx)
     refine ⟨⟨φ, ?_⟩, hφ₃, hφ₄⟩
     refine
-      φ.continuous_of_nonzero_on_open _ (hs₂.vadd (-x₀)) (Nonempty.vadd_set ⟨0, hs₀⟩)
-        (vadd_set_subset_iff.mpr fun x hx => ?_)
+      φ.continuous_of_nonzero_on_open _ (hs₂.vadd (-x₀)) (Nonempty.vadd_set ⟨0, hs₀⟩) ?_
+    rintro _ ⟨x, hx, rfl⟩
     change φ (-x₀ + x) ≠ 0
     rw [map_add, map_neg]
     specialize hφ₄ x hx

Mathlib/Analysis/Meromorphic/Order.lean

@@ -726,9 +726,6 @@ theorem isClopen_setOfPred_meromorphicOrderAt_eq_top (hf : MeromorphicOn f U) :
     · exact h₂t'.sdiff isClosed_singleton
     · exact ⟨hw, mem_singleton_iff.not.1 (Subtype.coe_ne_coe.2 h₁w)⟩
 
-@[deprecated (since := "2026-07-03")] alias isClopen_setOf_meromorphicOrderAt_eq_top :=
-  isClopen_ofPred_meromorphicOrderAt_eq_top
-
 @[deprecated (since := "2026-07-09")]
 alias isClopen_setOf_meromorphicOrderAt_eq_top := isClopen_setOfPred_meromorphicOrderAt_eq_top
 

Mathlib/Analysis/Normed/Group/Quotient.lean

@@ -152,7 +152,8 @@ lemma norm_lt_iff : ‖x‖ < r ↔ ∃ m : M, ↑m = x ∧ ‖m‖ < r := by
 lemma nhds_one_hasBasis : (𝓝 (1 : M ⧸ S)).HasBasis (fun ε ↦ 0 < ε) fun ε ↦ {x | ‖x‖ < ε} := by
   have : ∀ ε : ℝ, mk '' ball (1 : M) ε = {x : M ⧸ S | ‖x‖ < ε} := by
     refine fun ε ↦ Set.ext <| forall_mk.2 fun x ↦ ?_
-    rw [ball_one_eq, mem_ofPred_eq, norm_lt_iff, mem_image]
+    rw [ball_one_eq]
+    simp only [mem_image, mem_ofPred_eq, norm_lt_iff]
     exact exists_congr fun _ ↦ and_comm
   rw [← mk_one, nhds_eq, ← funext this]
   exact .map _ Metric.nhds_basis_ball

Mathlib/Analysis/Normed/Lp/lpSpace.lean

@@ -508,7 +508,7 @@ theorem norm_eq_zero_iff {f : lp E p} : ‖f‖ = 0 ↔ f = 0 := by
   rcases p.trichotomy with (rfl | rfl | hp)
   · ext i
     have : { i : α | ¬f i = 0 } = ∅ := by simpa [lp.norm_eq_card_dsupport f] using! h
-    have : (¬f i = 0) = False := congr_fun this i
+    have : ¬¬f i = 0 := Set.eq_empty_iff_forall_notMem.mp this i
     tauto
   · rcases isEmpty_or_nonempty α with _i | _i
     · simp [eq_iff_true_of_subsingleton]

Mathlib/Analysis/Normed/Module/FiniteDimension.lean

@@ -337,7 +337,7 @@ alias isOpen_setOf_linearIndependent := isOpen_setOfPred_linearIndependent
 theorem isOpen_setOfPred_nat_le_rank (n : ℕ) :
     IsOpen { f : E →L[𝕜] F | ↑n ≤ (f : E →ₗ[𝕜] F).rank } := by
   simp only [LinearMap.le_rank_iff_exists_linearIndependent_finset, ofPred_exists, ← exists_prop]
-  refine isOpen_biUnion fun t _ => ?_
+  refine isOpen_iUnion fun t => isOpen_iUnion fun _ => ?_
   have : Continuous fun f : E →L[𝕜] F => fun x : (t : Set E) => f x :=
     continuous_pi fun x => (ContinuousLinearMap.apply 𝕜 F (x : E)).continuous
   exact isOpen_setOfPred_linearIndependent.preimage this

Mathlib/Analysis/ODE/Transform.lean

@@ -117,24 +117,29 @@ lemma isIntegralCurveOn_comp_mul_ne_zero {a : ℝ} (ha : a ≠ 0) :
     rw [mem_inv_smul_set_iff₀ ha, smul_eq_mul, mul_comm]
     rfl
   refine ⟨fun hγ ↦ ?_, heq ▸ fun hγ ↦ hγ.comp_mul a⟩
-  convert! hγ.comp_mul a⁻¹
+  have hs : {t | t * a⁻¹ ∈ a⁻¹ • s} = s := by
+    ext t
+    rw [mem_ofPred_eq, mul_comm _ a⁻¹, ← smul_eq_mul, mem_inv_smul_set_iff₀ ha,
+      smul_inv_smul₀ ha]
+  have h2 := hγ.comp_mul a⁻¹
+  rw [hs] at h2
+  convert! h2
   · ext t
     simp only [comp_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one]
   · ext t
     simp only [comp_apply, Pi.smul_apply, mul_assoc, inv_mul_eq_div, div_self ha, mul_one,
       smul_smul, one_smul]
-  · simp only [mul_comm _ a⁻¹, ← smul_eq_mul, mem_inv_smul_set_iff₀ ha, smul_inv_smul₀ ha,
-      ofPred_mem_eq]
 
 lemma IsIntegralCurveAt.comp_mul_ne_zero (hγ : IsIntegralCurveAt γ v t₀) {a : ℝ} (ha : a ≠ 0) :
     IsIntegralCurveAt (γ ∘ (· * a)) (a • v ∘ (· * a)) (t₀ / a) := by
   rw [isIntegralCurveAt_iff_exists_pos] at *
   obtain ⟨ε, hε, h⟩ := hγ
   refine ⟨ε / |a|, by positivity, ?_⟩
-  convert! h.comp_mul a
-  ext t
-  rw [mem_ofPred_eq, Metric.mem_ball, Metric.mem_ball, Real.dist_eq, Real.dist_eq,
-    lt_div_iff₀ (abs_pos.mpr ha), ← abs_mul, sub_mul, div_mul_cancel₀ _ ha]
+  have hs : {t | t * a ∈ Metric.ball t₀ ε} = Metric.ball (t₀ / a) (ε / |a|) := by
+    ext t
+    rw [mem_ofPred_eq, Metric.mem_ball, Metric.mem_ball, Real.dist_eq, Real.dist_eq,
+      lt_div_iff₀ (abs_pos.mpr ha), ← abs_mul, sub_mul, div_mul_cancel₀ _ ha]
+  exact hs ▸ h.comp_mul a
 
 lemma isIntegralCurveAt_comp_mul_ne_zero {a : ℝ} (ha : a ≠ 0) :
     IsIntegralCurveAt (γ ∘ (· * a)) (a • v ∘ (· * a)) (t₀ / a) ↔ IsIntegralCurveAt γ v t₀ := by

Mathlib/Analysis/Polynomial/MahlerMeasure.lean

@@ -137,12 +137,13 @@ theorem mahlerMeasure_mul (p q : ℂ[X]) :
   rw [MeasureTheory.ae_iff]
   apply Set.Finite.measure_zero _ MeasureTheory.volume
   simp only [Classical.not_imp]
-  apply Set.Finite.of_finite_image (f := circleMap 0 1) _ <|
-    (injOn_circleMap_of_abs_sub_le one_ne_zero (by simp [le_of_eq, pi_nonneg])).mono (fun _ h ↦ h.1)
-  apply (p * q).roots.finite_toSet.subset
-  rintro _ ⟨_, ⟨_, h⟩, _⟩
-  contrapose h
-  simp_all [log_mul]
+  apply Set.Finite.of_finite_image (f := circleMap 0 1)
+  · apply (p * q).roots.finite_toSet.subset
+    rintro _ ⟨_, ⟨_, h⟩, _⟩
+    contrapose h
+    simp_all [log_mul]
+  · exact (injOn_circleMap_of_abs_sub_le one_ne_zero (by simp [le_of_eq, pi_nonneg])).mono
+      fun _ h ↦ h.1
 
 @[simp]
 theorem prod_mahlerMeasure_eq_mahlerMeasure_prod (s : Multiset ℂ[X]) :
@@ -284,9 +285,11 @@ theorem mahlerMeasure_le_sum_norm_coeff (p : ℂ[X]) : p.mahlerMeasure ≤ p.sum
     apply (Finite.of_sdiff _ <| finite_singleton (2 * π)).measure_zero
     simp only [ne_eq, mem_ofPred_eq, Decidable.not_not, inter_sdiff_assoc, Icc_sdiff_right]
     rw [ofPred_inter_eq_sep]
-    apply Finite.of_finite_image (f := circleMap 0 1) ((Multiset.finite_toSet p.roots).subset _)
-      <| fun _ h _ k l ↦ injOn_circleMap_of_abs_sub_le' one_ne_zero (by linarith) h.1 k.1 l
-    simp [hp]
+    apply Finite.of_finite_image (f := circleMap 0 1)
+    · apply (Multiset.finite_toSet p.roots).subset
+      simp [hp]
+    · exact fun _ h _ k l ↦
+        injOn_circleMap_of_abs_sub_le' one_ne_zero (by linarith) h.1 k.1 l
   · intro _ _
     gcongr
     rw [eval_eq_sum]