chore: more fixes for multigoal linter (#17966)

Preparation for #12339.

Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean

@@ -198,7 +198,7 @@ theorem aeval_sumIDeriv_of_pos [Nontrivial A] [NoZeroDivisors A] (p : R[X]) {q :
     rw [map_zero, map_zero, smul_zero, add_zero]
     rw [Polynomial.map_zero] at hp
     replace hp := (mul_eq_zero.mp hp.symm).resolve_left ?_
-    rw [hp, eval_zero, smul_zero]
+    · rw [hp, eval_zero, smul_zero]
     exact fun h => X_sub_C_ne_zero r (pow_eq_zero h)
   let c k := if hk : q ≤ k then (aeval_iterate_derivative_of_ge A p q hk).choose else 0
   have c_le (k) : (c k).natDegree ≤ p.natDegree - k := by
@@ -228,13 +228,13 @@ theorem aeval_sumIDeriv_of_pos [Nontrivial A] [NoZeroDivisors A] (p : R[X]) {q :
   rw [sumIDeriv_apply, map_sum, map_sum, this]
   have : range q = range (q - 1 + 1) := by rw [tsub_add_cancel_of_le (Nat.one_le_of_lt hq)]
   rw [sum_union, this, sum_range_succ]
-  congr 2
-  · apply sum_eq_zero
-    exact fun x hx => aeval_iterate_derivative_of_lt p _ r hp (mem_range.mp hx)
-  · rw [← aeval_iterate_derivative_self _ _ _ hp]
-  · rw [smul_sum, sum_congr rfl]
-    intro k hk
-    exact hc k (mem_Ico.mp hk).1 r
+  · congr 2
+    · apply sum_eq_zero
+      exact fun x hx => aeval_iterate_derivative_of_lt p _ r hp (mem_range.mp hx)
+    · rw [← aeval_iterate_derivative_self _ _ _ hp]
+    · rw [smul_sum, sum_congr rfl]
+      intro k hk
+      exact hc k (mem_Ico.mp hk).1 r
   · rw [range_eq_Ico, disjoint_iff_inter_eq_empty, eq_empty_iff_forall_not_mem]
     intro x hx
     rw [mem_inter, mem_Ico, mem_Ico] at hx

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -444,18 +444,18 @@ private lemma respects_isOpenImmersion_aux {X Y : Scheme.{u}} [IsAffine Y] {U :
   · obtain ⟨(Us : Set Y.Opens), hUs, heq⟩ := Opens.isBasis_iff_cover.mp (isBasis_basicOpen Y) U
     let V (s : Us) : X.Opens := f ⁻¹ᵁ U.ι ⁻¹ᵁ s
     rw [IsLocalAtSource.iff_of_iSup_eq_top (P := P) V]
-    intro s
-    let f' : (V s).toScheme ⟶ U.ι ⁻¹ᵁ s := f ∣_ U.ι ⁻¹ᵁ s
-    have hf' : P f' := IsLocalAtTarget.restrict hf _
-    let e : (U.ι ⁻¹ᵁ s).toScheme ≅ s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ s).ι ≫ U.ι) s.1.ι
-      (by simpa [Set.range_comp, Set.image_preimage_eq_iff, heq] using le_sSup s.2)
-    have heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ s.1.ι := by
-      simp only [IsOpenImmersion.isoOfRangeEq_hom_fac, f', e, morphismRestrict_ι_assoc]
-    rw [heq, ← Category.assoc]
-    refine this _ ?_ ?_
-    · rwa [P.cancel_right_of_respectsIso]
-    · obtain ⟨a, ha⟩ := hUs s.2
-      use a, ha.symm
+    · intro s
+      let f' : (V s).toScheme ⟶ U.ι ⁻¹ᵁ s := f ∣_ U.ι ⁻¹ᵁ s
+      have hf' : P f' := IsLocalAtTarget.restrict hf _
+      let e : (U.ι ⁻¹ᵁ s).toScheme ≅ s := IsOpenImmersion.isoOfRangeEq ((U.ι ⁻¹ᵁ s).ι ≫ U.ι) s.1.ι
+        (by simpa [Set.range_comp, Set.image_preimage_eq_iff, heq] using le_sSup s.2)
+      have heq : (V s).ι ≫ f ≫ U.ι = f' ≫ e.hom ≫ s.1.ι := by
+        simp only [IsOpenImmersion.isoOfRangeEq_hom_fac, f', e, morphismRestrict_ι_assoc]
+      rw [heq, ← Category.assoc]
+      refine this _ ?_ ?_
+      · rwa [P.cancel_right_of_respectsIso]
+      · obtain ⟨a, ha⟩ := hUs s.2
+        use a, ha.symm
     · apply f.preimage_iSup_eq_top
       apply U.ι.image_injective
       simp only [U.ι.image_iSup, U.ι.image_preimage_eq_opensRange_inter, Scheme.Opens.opensRange_ι]

Mathlib/Analysis/SpecificLimits/RCLike.lean

@@ -29,8 +29,8 @@ theorem RCLike.tendsto_add_mul_div_add_mul_atTop_nhds (a b c : 𝕜) {d : 𝕜}
     Tendsto (fun k : ℕ ↦ (a + c * k) / (b + d * k)) atTop (𝓝 (c / d)) := by
   apply Filter.Tendsto.congr'
   case f₁ => exact fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)
-  refine (eventually_ne_atTop 0).mp (Eventually.of_forall ?_)
-  · intro h hx
+  · refine (eventually_ne_atTop 0).mp (Eventually.of_forall ?_)
+    intro h hx
     field_simp [hx]
   · apply Filter.Tendsto.div _ _ hd
     all_goals

Mathlib/Data/Nat/Choose/Factorization.lean

@@ -40,8 +40,8 @@ theorem factorization_choose_le_log : (choose n k).factorization p ≤ log p n :
     simp [choose_eq_zero_of_lt hnk]
   rw [factorization_def _ hp, @padicValNat_def _ ⟨hp⟩ _ (choose_pos hkn)]
   rw [← Nat.cast_le (α := ℕ∞), ← multiplicity.Finite.emultiplicity_eq_multiplicity]
-  simp only [hp.emultiplicity_choose hkn (lt_add_one _), Nat.cast_le]
-  exact (Finset.card_filter_le _ _).trans (le_of_eq (Nat.card_Ico _ _))
+  · simp only [hp.emultiplicity_choose hkn (lt_add_one _), Nat.cast_le]
+    exact (Finset.card_filter_le _ _).trans (le_of_eq (Nat.card_Ico _ _))
   apply Nat.multiplicity_finite_iff.2 ⟨hp.ne_one, choose_pos hkn⟩
 
 /-- A `pow` form of `Nat.factorization_choose_le` -/

Mathlib/NumberTheory/Ostrowski.lean

@@ -335,7 +335,8 @@ lemma one_lt_of_not_bounded (notbdd : ¬ ∀ n : ℕ, f n ≤ 1) {n₀ : ℕ} (h
       rw [← mul_rpow (by positivity) (by positivity), mul_assoc, add_mul, one_mul,
       mul_comm _ (k : ℝ)]
 -- For 0 < logb n₀ n below we also need to exclude n = 1.
-  rcases eq_or_ne n 1 with rfl | h₁; simp only [Nat.cast_one, map_one, le_refl]
+  rcases eq_or_ne n 1 with rfl | h₁
+  · simp only [Nat.cast_one, map_one, le_refl]
   refine le_of_tendsto_of_tendsto tendsto_const_nhds ?_ (eventually_atTop.2 ⟨1, h_ineq2⟩)
   nth_rw 2 [← mul_one 1]
   have : 0 < logb n₀ n := logb_pos (mod_cast hn₀) (by norm_cast; omega)

Mathlib/RingTheory/LocalRing/Quotient.lean

@@ -67,7 +67,7 @@ theorem finrank_quotient_map :
   · let b := Module.Free.chooseBasis (R ⧸ p) (S ⧸ pS)
     choose b' hb' using fun i ↦ Ideal.Quotient.mk_surjective (b i)
     conv_rhs => rw [finrank_eq_card_chooseBasisIndex]
-    apply finrank_le_of_span_eq_top
+    refine finrank_le_of_span_eq_top (v := b') ?_
     apply (quotient_span_eq_top_iff_span_eq_top _).mp
     rw [← Set.range_comp, show Ideal.Quotient.mk pS ∘ b' = ⇑b from funext hb']
     exact b.span_eq

Mathlib/RingTheory/Smooth/Pi.lean

@@ -28,18 +28,18 @@ theorem of_pi [FormallySmooth R (Π i, A i)] (i) :
     FormallySmooth R (A i) := by
   classical
   fapply FormallySmooth.of_split (Pi.evalAlgHom R A i)
-  apply AlgHom.ofLinearMap
-    ((Ideal.Quotient.mkₐ R _).toLinearMap.comp (LinearMap.single _ _ i))
-  · show Ideal.Quotient.mk _ (Pi.single i 1) = 1
-    rw [← (Ideal.Quotient.mk _).map_one, ← sub_eq_zero, ← map_sub,
-      Ideal.Quotient.eq_zero_iff_mem]
-    have : Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom := by
-      simp [RingHom.mem_ker]
-    convert neg_mem (Ideal.pow_mem_pow this 2) using 1
-    simp [pow_two, sub_mul, mul_sub, ← Pi.single_mul]
-  · intro x y
-    show Ideal.Quotient.mk _ _ = Ideal.Quotient.mk _ _ * Ideal.Quotient.mk _ _
-    simp only [AlgHom.toRingHom_eq_coe, LinearMap.coe_single, Pi.single_mul, map_mul]
+  · apply AlgHom.ofLinearMap
+      ((Ideal.Quotient.mkₐ R _).toLinearMap.comp (LinearMap.single _ _ i))
+    · show Ideal.Quotient.mk _ (Pi.single i 1) = 1
+      rw [← (Ideal.Quotient.mk _).map_one, ← sub_eq_zero, ← map_sub,
+        Ideal.Quotient.eq_zero_iff_mem]
+      have : Pi.single i 1 - 1 ∈ RingHom.ker (Pi.evalAlgHom R A i).toRingHom := by
+        simp [RingHom.mem_ker]
+      convert neg_mem (Ideal.pow_mem_pow this 2) using 1
+      simp [pow_two, sub_mul, mul_sub, ← Pi.single_mul]
+    · intro x y
+      show Ideal.Quotient.mk _ _ = Ideal.Quotient.mk _ _ * Ideal.Quotient.mk _ _
+      simp only [AlgHom.toRingHom_eq_coe, LinearMap.coe_single, Pi.single_mul, map_mul]
   · ext x
     show (Pi.single i x) i = x
     simp

Mathlib/Topology/MetricSpace/HolderNorm.lean

@@ -158,7 +158,7 @@ lemma MemHolder.holderWith {r : ℝ≥0} {f : X → Y} (hf : MemHolder r f) :
   by_cases hx : x₁ = x₂
   · simp only [hx, edist_self, zero_le]
   rw [nnHolderNorm, eHolderNorm, coe_toNNReal]
-  swap; exact hf.eHolderNorm_lt_top.ne
+  on_goal 2 => exact hf.eHolderNorm_lt_top.ne
   have h₁ : edist x₁ x₂ ^ (r : ℝ) ≠ 0 :=
     (Ne.symm <| ne_of_lt <| ENNReal.rpow_pos (edist_pos.2 hx) (edist_lt_top x₁ x₂).ne)
   have h₂ : edist x₁ x₂ ^ (r : ℝ) ≠ ∞ := by