unreviewed

Author: YaelDillies

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/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/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 @@ theorem isOpen_ofPred_linearIndependent {ι : Type*} [Finite ι] :
 theorem isOpen_ofPred_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_ofPred_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]

Mathlib/Analysis/SpecialFunctions/Complex/Analytic.lean

@@ -153,8 +153,9 @@ lemma AnalyticOnNhd.log (fs : AnalyticOnNhd ℝ f s) (m : ∀ x ∈ s, 0 < f x)
   fun z n ↦ (analyticAt_log (m z n)).comp (fs z n)
 
 lemma AnalyticOn.log (fs : AnalyticOn ℝ f s) (m : ∀ x ∈ s, 0 < f x) :
-    AnalyticOn ℝ (fun z ↦ Real.log (f z)) s :=
-  fun z n ↦ (analyticAt_log (m z n)).analyticWithinAt.comp (fs z n) m
+    AnalyticOn ℝ (fun z ↦ Real.log (f z)) s := by
+  have hm : MapsTo f s {y | 0 < y} := m
+  exact fun z n ↦ (analyticAt_log (m z n)).analyticWithinAt.comp (fs z n) hm
 
 theorem iteratedDeriv_succ_log {n : ℕ} {x : ℂ} (hx : x ∈ slitPlane) :
     iteratedDeriv (n + 1) log x = (-1 : ℂ) ^ n * n.factorial * x ^ (-(n : ℤ) - 1) := by

Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean

@@ -558,15 +558,15 @@ theorem arg_eq_nhds_of_re_neg_of_im_pos (hx_re : x.re < 0) (hx_im : 0 < x.im) :
     arg =ᶠ[𝓝 x] fun x => Real.arcsin ((-x).im / ‖x‖) + π := by
   suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ 0 < y.im from
     h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_nonneg hy.1 hy.2.le
-  refine IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ 0 < x.im)
+  refine IsOpen.eventually_mem (s := {z : ℂ | z.re < 0 ∧ 0 < z.im}) ?_ ⟨hx_re, hx_im⟩
   exact
     IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_zero continuous_im)
 
 theorem arg_eq_nhds_of_re_neg_of_im_neg (hx_re : x.re < 0) (hx_im : x.im < 0) :
     arg =ᶠ[𝓝 x] fun x => Real.arcsin ((-x).im / ‖x‖) - π := by
   suffices h_forall_nhds : ∀ᶠ y : ℂ in 𝓝 x, y.re < 0 ∧ y.im < 0 from
     h_forall_nhds.mono fun y hy => arg_of_re_neg_of_im_neg hy.1 hy.2
-  refine IsOpen.eventually_mem ?_ (⟨hx_re, hx_im⟩ : x.re < 0 ∧ x.im < 0)
+  refine IsOpen.eventually_mem (s := {z : ℂ | z.re < 0 ∧ z.im < 0}) ?_ ⟨hx_re, hx_im⟩
   exact
     IsOpen.and (isOpen_lt continuous_re continuous_zero) (isOpen_lt continuous_im continuous_zero)
 

Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

@@ -505,9 +505,12 @@ theorem Circle.isQuotientCoveringMap_zpow (n : ℤ) [NeZero n] :
         IsUnit.isQuotientMap_zsmul (M := ℝ) (QuotientAddGroup.mk' (AddSubgroup.zmultiples (1 : ℝ)))
           isQuotientMap_quotient_mk' n hn
     ext; simp [zpowGroupHom, e, homeomorphCircle_apply, toCircle_zsmul]
-  · convert! finite_torsion_of_isSMulRegular_int (1 : ℝ) n fun _ ↦ by simp [NeZero.ne]
-    ext
-    simp [e, homeomorphCircle_apply, ← toCircle_zsmul, ← (injective_toCircle one_ne_zero).eq_iff]
+  · have key : ⇑e ⁻¹' ((zpowGroupHom (α := Circle) n).ker : Set Circle) =
+        {x : AddCircle 1 | n • x = 0} := by
+      ext
+      simp [e, homeomorphCircle_apply, ← toCircle_zsmul,
+        ← (injective_toCircle one_ne_zero).eq_iff]
+    exact key ▸ finite_torsion_of_isSMulRegular_int (1 : ℝ) n fun _ ↦ by simp [NeZero.ne]
 
 theorem Circle.isQuotientCoveringMap_npow (n : ℕ) [NeZero n] :
     IsQuotientCoveringMap (· ^ n : Circle → _) (powMonoidHom (α := Circle) n).ker :=