chore: fix or silence all multi-goal warnings; small in-passing golfs

SphereEversion/Global/Immersion.lean

@@ -46,7 +46,7 @@ theorem mem_immersionRel_iff' {σ σ' : OneJetBundle I M I' M'} (hσ' : σ' ∈
     σ' ∈ immersionRel I M I' M' ↔ Injective (ψJ σ σ').2 := by
   simp_rw [mem_immersionRel_iff]
   rw [oneJetBundle_chartAt_apply, inCoordinates_eq]
-  simp_rw [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, EquivLike.comp_injective,
+  · simp_rw [ContinuousLinearMap.coe_comp', ContinuousLinearEquiv.coe_coe, EquivLike.comp_injective,
     EquivLike.injective_comp]
   exacts [hσ'.1.1, hσ'.1.2]
 
@@ -224,7 +224,7 @@ theorem formalEversionHolAtOne {t : ℝ} (ht : 3 / 4 < t) :
   ext v
   erw [mfderiv_neg, ContinuousLinearMap.coe_comp', Function.comp_apply,
        ContinuousLinearMap.neg_apply, smoothStep.of_gt ht]
-  rw [ω.rot_one]; rfl
+  rw [ω.rot_one]; · rfl
   rw [← range_mfderiv_coe_sphere (n := 2) x]
   exact LinearMap.mem_range_self _ _
 

SphereEversion/Global/Localisation.lean

@@ -149,22 +149,22 @@ omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
 theorem RelLoc.HtpyFormalSol.unloc_congr {𝓕 𝓕' : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol} {t t' x}
     (h : 𝓕 t x = 𝓕' t' x) : 𝓕.unloc p t x = 𝓕'.unloc p t' x := by
   ext1
-  rfl
-  change (𝓕 t x).1 = (𝓕' t' x).1
-  rw [h]
-  change (𝓕 t x).2 = (𝓕' t' x).2
-  rw [h]
+  · rfl
+  · change (𝓕 t x).1 = (𝓕' t' x).1
+    rw [h]
+  · change (𝓕 t x).2 = (𝓕' t' x).2
+    rw [h]
 
 omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
 theorem RelLoc.HtpyFormalSol.unloc_congr_const {𝓕 : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol}
     {𝓕' : (R.localize p.φ p.ψ).relLoc.FormalSol} {t x} (h : 𝓕 t x = 𝓕' x) :
     𝓕.unloc p t x = 𝓕'.unloc x := by
   ext1
-  rfl
-  change (𝓕 t x).1 = (𝓕' x).1
-  rw [h]
-  change (𝓕 t x).2 = (𝓕' x).2
-  rw [h]
+  · rfl
+  · change (𝓕 t x).1 = (𝓕' x).1
+    rw [h]
+  · change (𝓕 t x).2 = (𝓕' x).2
+    rw [h]
 
 omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M'] in
 theorem RelLoc.HtpyFormalSol.unloc_congr' {𝓕 𝓕' : (R.localize p.φ p.ψ).relLoc.HtpyFormalSol} {t t'}

SphereEversion/Global/OneJetBundle.lean

@@ -405,7 +405,7 @@ theorem ContinuousAt.inTangentCoordinates_comp {f : N → M} {g : N → M'} {h :
   simp_rw [inTangentCoordinates, inCoordinates,
     ContinuousLinearMap.comp_apply]
   rw [Trivialization.symmL_continuousLinearMapAt]
-  rfl
+  · rfl
   exact hx
 
 theorem SmoothAt.clm_comp_inTangentCoordinates {f : N → M} {g : N → M'} {h : N → N'}
@@ -525,6 +525,7 @@ theorem SmoothAt.oneJetBundle_map {f : M'' → M → N} {g : M'' → M' → N'}
 def mapLeft (f : M → N) (Dfinv : ∀ x : M, TangentSpace J (f x) →L[𝕜] TangentSpace I x) :
     J¹MM' → OneJetBundle J N I' M' := fun p ↦ OneJetBundle.mk (f p.1.1) p.1.2 (p.2 ∘L Dfinv p.1.1)
 
+set_option linter.style.multiGoal false in
 omit [SmoothManifoldWithCorners I M] [SmoothManifoldWithCorners I' M']
   [SmoothManifoldWithCorners I₂ M₂] [SmoothManifoldWithCorners I₃ M₃]
   [SmoothManifoldWithCorners J' N'] [SmoothManifoldWithCorners J N] in
@@ -570,7 +571,7 @@ theorem smooth_bundleSnd :
       (inTangentCoordinates I (J.prod I) _ _ _ x₀) x₀ :=
     ContMDiffAt.mfderiv (fun (x : OneJetBundle (J.prod I) (N × M) I' M') (y : M) ↦ (x.1.1.1, y))
       (fun x : OneJetBundle (J.prod I) (N × M) I' M' ↦ x.1.1.2) ?_ ?_ le_top
-  exact this
+  · exact this
   · exact (smooth_oneJetBundle_proj.fst.fst.prod_map smooth_id).smoothAt
   -- slow
   · exact smooth_oneJetBundle_proj.fst.snd.smoothAt

SphereEversion/Global/OneJetSec.lean

@@ -55,7 +55,7 @@ instance : FunLike (OneJetSec I M I' M') M (OneJetBundle I M I' M') where
     intro S T h
     dsimp at h
     ext x
-    simpa using (Bundle.TotalSpace.mk.inj (congrFun h x)).1
+    · simpa using (Bundle.TotalSpace.mk.inj (congrFun h x)).1
     have := heq_eq_eq _ _ ▸ (Bundle.TotalSpace.mk.inj (congrFun h x)).2
     exact congrFun (congrArg DFunLike.coe this) _
 
@@ -65,7 +65,7 @@ namespace OneJetSec
 
 protected def mk' (F : M → OneJetBundle I M I' M') (hF : ∀ m, (F m).1.1 = m)
     (h2F : Smooth I ((I.prod I').prod 𝓘(𝕜, E →L[𝕜] E')) F) : OneJetSec I M I' M' :=
-  ⟨fun x ↦ (F x).1.2, fun x ↦ (F x).2, by convert h2F using 1; ext m; exact (hF m).symm; rfl; rfl⟩
+  ⟨fun x ↦ (F x).1.2, fun x ↦ (F x).2, by convert h2F using 1; ext m; exacts [(hF m).symm, rfl, rfl]⟩
 
 theorem coe_apply (F : OneJetSec I M I' M') (x : M) : F x = ⟨(x, F.bs x), F.ϕ x⟩ :=
   rfl
@@ -185,8 +185,8 @@ instance : FunLike (FamilyOneJetSec I M I' M' J N) N (OneJetSec I M I' M') where
   coe_injective' := by
     intro S T h
     ext n : 2
-    exact (OneJetSec.mk.inj (congrFun h n)).1
-    exact (OneJetSec.mk.inj (congrFun h n)).2
+    · exact (OneJetSec.mk.inj (congrFun h n)).1
+    · exact (OneJetSec.mk.inj (congrFun h n)).2
 
 namespace FamilyOneJetSec
 
@@ -196,7 +196,7 @@ protected def mk' (FF : N → M → OneJetBundle I M I' M') (hF : ∀ n m, (FF n
     (h2F : Smooth (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) (uncurry FF)) :
     FamilyOneJetSec I M I' M' J N :=
   ⟨fun s x ↦ (FF s x).1.2, fun s x ↦ (FF s x).2,
-  by convert h2F using 1; ext ⟨s, m⟩; exact (hF s m).symm; rfl; rfl⟩
+   by convert h2F using 1; ext ⟨s, m⟩; exacts [(hF s m).symm, rfl, rfl]⟩
 
 theorem coe_mk' (FF : N → M → OneJetBundle I M I' M') (hF : ∀ n m, (FF n m).1.1 = m)
     (h2F : Smooth (J.prod I) ((I.prod I').prod 𝓘(ℝ, E →L[ℝ] E')) (uncurry FF)) (x : N) :

SphereEversion/Global/Relation.lean

@@ -85,12 +85,12 @@ def mkFormalSol (F : M → OneJetBundle I M I' M') (hsec : ∀ x, (F x).1.1 = x)
   smooth' := by
     convert hsmooth
     ext
-    rw [hsec]
+    on_goal 1 => rw [hsec]
     all_goals rfl
   is_sol' m := by
     convert hsol m
     ext
-    rw [hsec]
+    on_goal 1 => rw [hsec]
     all_goals rfl
 
 @[simp]
@@ -116,7 +116,7 @@ theorem coe_mk {S : OneJetSec I M I' M'} {h : ∀ x, S x ∈ R} {x : M} : Formal
 theorem coe_inj_iff {S T : FormalSol R} : S = T ↔ ∀ x, S x = T x := by
   constructor
   · rintro rfl x; rfl
-  · intro h; ext x v : 3; show (S x).1.2 = (T x).1.2; rw [h]
+  · intro h; ext x v : 3; · show (S x).1.2 = (T x).1.2; rw [h]
     show (S x).2 v = (T x).2 v; rw [h]
 
 theorem coe_inj {S T : FormalSol R} (h : ∀ x, S x = T x) : S = T :=
@@ -230,8 +230,7 @@ instance : FunLike (FamilyFormalSol J N R) N (FormalSol R) where
       exact congrArg FormalSol.toOneJetSec (congrFun h n)
     congr! 1
     ext n : 2
-    exact (OneJetSec.mk.inj <| fact n).1
-    exact (OneJetSec.mk.inj <| fact n).2
+    exacts [(OneJetSec.mk.inj <| fact n).1, (OneJetSec.mk.inj <| fact n).2]
 
 namespace FamilyFormalSol
 
@@ -280,12 +279,12 @@ def mkHtpyFormalSol (F : ℝ → M → OneJetBundle I M I' M') (hsec : ∀ t x,
   smooth' := by
     convert hsmooth using 1
     ext ⟨t, x⟩
-    exact (hsec t x).symm
+    · exact (hsec t x).symm
     all_goals rfl
   is_sol' t m := by
     convert hsol t m
     ext
-    rw [hsec]
+    on_goal 1 => rw [hsec]
     all_goals rfl
 
 @[simp]
@@ -683,7 +682,7 @@ def Jupdate (F : OneJetSec IM M IN N) (G : HtpyOneJetSec IX X IY Y) (hK : IsComp
 theorem Jupdate_apply {F : OneJetSec IM M IN N} {G : HtpyOneJetSec IX X IY Y} (hK : IsCompact K)
     (hFG : ∀ t, ∀ x ∉ K, F (φ x) = (OneJetBundle.embedding φ ψ) (G t x)) (t : ℝ) (m : M) :
     φ.Jupdate ψ F G hK hFG t m = JΘ F (G t) m := by
-  ext; exact (φ.Jupdate_aux ψ F (G t) m).symm; rfl; rfl
+  ext; exacts [(φ.Jupdate_aux ψ F (G t) m).symm, rfl, rfl]
 
 theorem Jupdate_bs (F : OneJetSec IM M IN N) (G : HtpyOneJetSec IX X IY Y) (t : ℝ)
     (hK : IsCompact K)
@@ -750,8 +749,7 @@ theorem updateFormalSol_bs {F : FormalSol R} {G : HtpyFormalSol (R.localize φ 
   · simp only [hx, update_of_mem_range, OneJetBundle.embedding_toFun, transfer_proj_snd]
     rfl
   · rw [update_of_nmem_range, update_of_nmem_range]
-    rfl
-    exacts [hx, hx]
+    exacts [rfl, hx, hx]
 
 @[simp]
 theorem updateFormalSol_apply_of_mem {F : FormalSol R} {G : HtpyFormalSol (R.localize φ ψ)}

SphereEversion/Global/SmoothEmbedding.lean

@@ -261,7 +261,7 @@ def openSmoothEmbOfDiffeoSubsetChartTarget (x : M) {f : PartialHomeomorph F F} (
     IsOpenMap.isOpen_range fun u hu ↦ by
       have aux : IsOpen (f '' u) := f.isOpen_image_of_subset_source hu (hf₁.symm ▸ subset_univ u)
       convert isOpen_extChartAt_preimage' x aux
-      rw [image_comp]
+      on_goal 1 => rw [image_comp]
       refine
         (extChartAt IF x).symm_image_eq_source_inter_preimage ((image_subset_range f u).trans ?_)
       rw [extChartAt, PartialHomeomorph.extend_target']

SphereEversion/InductiveConstructions.lean

@@ -172,14 +172,13 @@ theorem set_juggling {X : Type*} [TopologicalSpace X] [NormalSpace X] [T2Space X
   obtain ⟨U', U'_op, hKU', hU'U⟩ : ∃ U' : Set X, IsOpen U' ∧ K ⊆ U' ∧ closure U' ⊆ U :=
     normal_exists_closure_subset hK U_op hKU
   refine ⟨K₁ ∪ closure (K₂ ∩ U'), K₂ \ U', U₁ ∪ U, U₂ \ K, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
-  · exact IsOpen.union U₁_op U_op
-  · exact IsOpen.sdiff U₂_op hK
-  · refine IsCompact.union K₁_cpct ?_
+  · exact U₁_op.union U_op
+  · exact U₂_op.sdiff hK
+  · refine K₁_cpct.union ?_
     exact K₂_cpct.closure_of_subset inter_subset_left
-  · exact IsCompact.diff K₂_cpct U'_op
+  · exact K₂_cpct.diff U'_op
   · exact subset_union_left
-  · apply union_subset_union
-    exact hK₁U₁
+  · apply union_subset_union hK₁U₁
     apply subset_trans _ hU'U
     gcongr
     exact inter_subset_right
@@ -470,8 +469,8 @@ theorem inductive_htpy_construction' {X Y : Type*}
     ((finite_lt_nat i).isClosed_biUnion fun j _ ↦ (K_cpct j).isClosed) hf₀ hf₁
     with ⟨F, hF₀, hF₁, hF₂, hFK₁, ht⟩
   refine ⟨F, hF₀, ?_, hF₂, ?_, ht⟩
-  apply hF₁.filter_mono
-  gcongr
-  rw [bUnion_le]
-  exact fun t x hx ↦ hFK₁ t x (not_mem_subset K₁W hx)
+  · apply hF₁.filter_mono
+    gcongr
+    rw [bUnion_le]
+  · exact fun t x hx ↦ hFK₁ t x (not_mem_subset K₁W hx)
 end Htpy

SphereEversion/Local/AmpleRelation.lean

@@ -57,7 +57,7 @@ def IsAmple (R : RelLoc E F) : Prop :=
 theorem IsAmple.mem_hull (h : IsAmple R) {θ : E × F × (E →L[ℝ] F)} (hθ : θ ∈ R) (v : F) (p) :
     v ∈ hull (connectedComponentIn (R.slice p θ) (θ.2.2 p.v)) := by
   rw [h p θ (θ.2.2 p.v)]
-  exact mem_univ _
+  · exact mem_univ _
   rw [mem_slice, p.update_self]
   exact hθ
 

SphereEversion/Local/Corrugation.lean

@@ -197,11 +197,12 @@ theorem Remainder.smooth {γ : G → E → Loop F} (hγ_diff : 𝒞 ∞ ↿γ) {
     refine (ContDiff.contDiff_top_partial_fst ?_).comp₂ hx.fst' (contDiff_fst.prod contDiff_snd)
     dsimp [Loop.normalize]
     apply ContDiff.sub
-    apply hγ_diff.comp₃ hg.fst'.snd' contDiff_fst contDiff_snd.snd
-    apply contDiff_average
-    exact hγ_diff.comp₃ hg.fst'.snd'.fst' contDiff_fst.fst' contDiff_snd
+    · apply hγ_diff.comp₃ hg.fst'.snd' contDiff_fst contDiff_snd.snd
+    · apply contDiff_average
+      exact hγ_diff.comp₃ hg.fst'.snd'.fst' contDiff_fst.fst' contDiff_snd
   · exact contDiff_const.mul (π.contDiff.comp hx)
 
+set_option linter.style.multiGoal false in
 theorem remainder_c0_small_on {K : Set E} (hK : IsCompact K) (hγ_diff : 𝒞 1 ↿γ) {ε : ℝ}
     (ε_pos : 0 < ε) : ∀ᶠ N in atTop, ∀ x ∈ K, ‖R N γ x‖ < ε := by
   simp_rw [fun N ↦ remainder_eq π N hγ_diff]

SphereEversion/Local/SphereEversion.lean

@@ -246,7 +246,7 @@ theorem loc_immersion_rel_ample (n : ℕ) [Fact (dim E = n + 1)] (h : finrank 
     erw [← this, map_comp]
     rfl
   rw [eq, p''.injective_update_iff, mem_compl_iff, eq']
-  exact Iff.rfl
+  · exact Iff.rfl
   rw [← show ((ℝ ∙ x)ᗮ : Set E).restrict φ = φ.comp j by ext; rfl]
   exact hφ.injective
 

SphereEversion/Loops/DeltaMollifier.lean

@@ -51,8 +51,8 @@ def bump (n : ℕ) : ContDiffBump (0 : ℝ) where
   rIn_pos := by positivity
   rIn_lt_rOut := by
     apply one_div_lt_one_div_of_lt
-    exact_mod_cast Nat.succ_pos _
-    exact_mod_cast lt_add_one (n + 2)
+    · exact_mod_cast Nat.succ_pos _
+    · exact_mod_cast lt_add_one (n + 2)
 
 theorem support_bump (n : ℕ) : support (bump n) = Ioo (-((1 : ℝ) / (n + 2))) (1 / (n + 2)) := by
   rw [(bump n).support_eq, Real.ball_eq_Ioo, zero_sub, zero_add, bump]
@@ -280,9 +280,9 @@ theorem Loop.mollify_eq_convolution (γ : Loop F) (hγ : Continuous γ) (t : ℝ
         ((1 : ℝ) / (n + 1)) • ∫ t in (0)..1, γ t := by
   simp_rw [Loop.mollify, deltaMollifier, add_smul, mul_smul]
   rw [integral_add]
-  simp_rw [integral_smul, approxDirac, ← periodize_comp_sub]
-  rw [intervalIntegral_periodize_smul _ γ _ _ (support_shifted_normed_bump_subset n t)]
-  simp_rw [MeasureTheory.convolution_eq_swap, ← neg_sub t, (bump n).normed_neg, lsmul_apply]
+  on_goal 1 => simp_rw [integral_smul, approxDirac, ← periodize_comp_sub]
+  on_goal 1 => rw [intervalIntegral_periodize_smul _ γ _ _ (support_shifted_normed_bump_subset n t)]
+  on_goal 1 => simp_rw [MeasureTheory.convolution_eq_swap, ← neg_sub t, (bump n).normed_neg, lsmul_apply]
   · linarith
   · rw [zero_add]
   · exact (continuous_const.smul (((approxDirac_smooth n).continuous.comp

SphereEversion/Loops/Exists.lean

@@ -202,11 +202,11 @@ theorem exist_loops_aux2 [FiniteDimensional ℝ E] (hK : IsCompact K) (hΩ_op :
         ((EventuallyEq.rfl.prod_mk <| EventuallyEq.rfl.prod_mk <|
               (fract_eventuallyEq hs).comp_tendsto continuousAt_id.snd'.snd').fun_comp ↿γ₅)
   refine ⟨γ, ⟨⟨?_, ?_, ?_, ?_, hγ.continuous⟩, ?_⟩, hγ, ?_⟩
-  · intro x t; simp_rw [fract_zero]; rw [hγ₅C]; exact hγ₃.base x _
+  · intro x t; simp_rw [fract_zero]; rw [hγ₅C]; · exact hγ₃.base x _
     exact Or.inr (by rw [mem_preimage, fract_zero]; exact h0C₁)
   · intro x s; simp_rw [smoothTransition.zero_of_nonpos le_rfl]; rw [hγ₅C]
-    exact hγ₃.t₀ x (fract s)
-    exact Or.inl (show (0 : ℝ) ≤ 5⁻¹ by norm_num)
+    · exact hγ₃.t₀ x (fract s)
+    · exact Or.inl (show (0 : ℝ) ≤ 5⁻¹ by norm_num)
   · intro x t s; simp_rw [smoothTransition_projI]
   · rintro x -; apply hγε₁; intro s
     simp_rw [← (γ₃ x 1).fract_eq s, smoothTransition.one_of_one_le le_rfl]

SphereEversion/Loops/Reparametrization.lean

@@ -76,9 +76,9 @@ theorem Loop.tendsto_mollify_apply (γ : E → Loop F) (h : Continuous ↿γ) (x
     · have := h.tendsto (x, t)
       rw [nhds_prod_eq] at this
       exact this.comp ((tendsto_fst.comp tendsto_fst).prod_mk tendsto_snd)
-  · rw [← zero_smul ℝ (_ : F)]
-    have : Continuous fun z ↦ intervalIntegral (γ z) 0 1 volume :=
+  · have : Continuous fun z ↦ intervalIntegral (γ z) 0 1 volume :=
       intervalIntegral.continuous_parametric_intervalIntegral_of_continuous (by apply h) continuous_const
+    rw [← zero_smul ℝ (_ : F)]
     exact (tendsto_one_div_add_atTop_nhds_zero_nat.comp tendsto_snd).smul
       ((this.tendsto x).comp tendsto_fst)
 

SphereEversion/ToMathlib/Algebra/Periodic.lean

@@ -55,7 +55,7 @@ def 𝕊₁ :=
   Quotient transOne
 deriving TopologicalSpace, Inhabited
 
-theorem transOne_rel_iff {a b : ℝ} : transOne.Rel a b ↔ ∃ k : ℤ, b = a + k := by
+theorem transOne_rel_iff {a b : ℝ} : transOne.r a b ↔ ∃ k : ℤ, b = a + k := by
   refine QuotientAddGroup.leftRel_apply.trans ?_
   refine exists_congr fun k ↦ ?_
   rw [coe_castAddHom, eq_neg_add_iff_add_eq, eq_comm]

SphereEversion/ToMathlib/Analysis/InnerProductSpace/Projection.lean

@@ -151,17 +151,16 @@ theorem foo {x₀ x : E} (h : ⟪x₀, x⟫ ≠ 0) (y : E) (hy : y ∈ {.x₀}
   dsimp only
   rwa [add_mul, MulZeroClass.zero_mul, div_mul_cancel₀ _ h]
 
+attribute [fun_prop] Continuous.inner
+
 /-- Given two non-orthogonal vectors in an inner product space,
 `orthogonal_projection_orthogonal_line_iso` is the continuous linear equivalence between their
 orthogonal complements obtained from orthogonal projection. -/
 def orthogonalProjectionOrthogonalLineIso {x₀ x : E} (h : ⟪x₀, x⟫ ≠ 0) : {.x₀}ᗮ ≃L[ℝ] {.x}ᗮ :=
   {
-    pr[x]ᗮ.comp
-      (subtypeL
-        {.x₀}ᗮ) with
+    pr[x]ᗮ.comp (subtypeL {.x₀}ᗮ) with
     invFun := fun y ↦
-      ⟨y - (⟪x₀, y⟫ / ⟪x₀, x⟫) • x,
-    by
+      ⟨y - (⟪x₀, y⟫ / ⟪x₀, x⟫) • x, by
         rw [mem_orthogonal_span_singleton_iff, inner_sub_right, inner_smul_right]
         field_simp [h]⟩
     left_inv := by
@@ -260,24 +259,22 @@ theorem continuousAt_orthogonalProjection_orthogonal {x₀ : E} (hx₀ : x₀ 
   simp only [key]
   simp_rw [Metric.tendsto_nhds_nhds, Real.dist_0_eq_abs, dist_eq_norm] at lim
   rcases lim (ε / 2) (half_pos ε_pos) with ⟨η, η_pos, hη⟩
-  refine ⟨min (ε / 2 / ‖N x₀‖) (η / 2), ?_, ?_⟩
-  · apply lt_min; positivity; exact half_pos η_pos
-  · intro y hy x
-    have hy₁ := hy.trans (min_le_left _ _); have hy₂ := hy.trans (min_le_right _ _); clear hy
-    specialize hη (by linarith : ‖y - x₀‖ < η)
-    rw [abs_of_nonneg] at hη
-    calc
+  refine ⟨min (ε / 2 / ‖N x₀‖) (η / 2), by positivity, ?_⟩
+  intro y hy x
+  have hy₁ := hy.trans (min_le_left _ _); have hy₂ := hy.trans (min_le_right _ _); clear hy
+  specialize hη (by linarith : ‖y - x₀‖ < η)
+  rw [abs_of_nonneg (by positivity)] at hη
+  calc
       ‖⟪N x₀, x⟫ • (x₀ - y) + ⟪N x₀ - N y, x⟫ • y‖ ≤ ‖⟪N x₀, x⟫ • (x₀ - y)‖ + ‖⟪N x₀ - N y, x⟫ • y‖ :=
         norm_add_le _ _
       _ ≤ ‖N x₀‖ * ‖x‖ * ‖x₀ - y‖ + ‖N x₀ - N y‖ * ‖x‖ * ‖y‖ := (add_le_add ?_ ?_)
       _ ≤ ε / 2 * ‖x‖ + ε / 2 * ‖x‖ := (add_le_add ?_ ?_)
       _ = ε * ‖x‖ := by linarith
-    · rw [norm_smul]
-      exact mul_le_mul_of_nonneg_right (norm_inner_le_norm _ _) (norm_nonneg _)
-    · rw [norm_smul]
-      exact mul_le_mul_of_nonneg_right (norm_inner_le_norm _ _) (norm_nonneg _)
-    · rw [mul_comm, ← mul_assoc, norm_sub_rev]
-      exact mul_le_mul_of_nonneg_right ((le_div_iff₀ hNx₀).mp hy₁) (norm_nonneg x)
-    · rw [mul_comm, ← mul_assoc, mul_comm ‖y‖]
-      exact mul_le_mul_of_nonneg_right hη.le (norm_nonneg x)
-    · positivity
+  · rw [norm_smul]
+    exact mul_le_mul_of_nonneg_right (norm_inner_le_norm _ _) (norm_nonneg _)
+  · rw [norm_smul]
+    exact mul_le_mul_of_nonneg_right (norm_inner_le_norm _ _) (norm_nonneg _)
+  · rw [mul_comm, ← mul_assoc, norm_sub_rev]
+    exact mul_le_mul_of_nonneg_right ((le_div_iff₀ hNx₀).mp hy₁) (norm_nonneg x)
+  · rw [mul_comm, ← mul_assoc, mul_comm ‖y‖]
+    exact mul_le_mul_of_nonneg_right hη.le (norm_nonneg x)

SphereEversion/ToMathlib/Analysis/InnerProductSpace/Rotation.lean

@@ -130,6 +130,7 @@ open Real Submodule
 
 open scoped Real
 
+set_option linter.style.multiGoal false in
 theorem injOn_rot_of_ne (t : ℝ) {x : E} (hx : x ≠ 0) : Set.InjOn (ω.rot (t, x)) (ℝ ∙ x)ᗮ := by
   change Set.InjOn (ω.rot (t, x)).toLinearMap (ℝ ∙ x)ᗮ
   simp_rw [← LinearMap.ker_inf_eq_bot, Submodule.eq_bot_iff, Submodule.mem_inf]

SphereEversion/ToMathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean

@@ -72,9 +72,8 @@ theorem isBoundedLinearMap_coprod (𝕜 : Type*) [NontriviallyNormedField 𝕜]
       simp only [Prod.smul_fst, Prod.smul_snd, ContinuousLinearMap.coprod_apply,
         ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_add]
     bound := by
-      refine ⟨2, zero_lt_two, ?_⟩
-      rintro ⟨φ, ψ⟩
-      apply ContinuousLinearMap.opNorm_le_bound; positivity
+      refine ⟨2, zero_lt_two, fun ⟨φ, ψ⟩ ↦ ?_⟩
+      apply ContinuousLinearMap.opNorm_le_bound _ (by positivity)
       rintro ⟨e, f⟩
       calc
         ‖φ e + ψ f‖ ≤ ‖φ e‖ + ‖ψ f‖ := norm_add_le _ _