[Merged by Bors] - chore: adapt to multiple goal linter 2

Archive/Wiedijk100Theorems/BirthdayProblem.lean

@@ -80,7 +80,10 @@ theorem birthday_measure :
     · rw [Fintype.card_embedding_eq, Fintype.card_fin, Fintype.card_fin]
       rfl
   rw [this, ENNReal.lt_div_iff_mul_lt, mul_comm, mul_div, ENNReal.div_lt_iff]
-  rotate_left; (iterate 2 right; norm_num); decide; (iterate 2 left; norm_num)
+  rotate_left
+  iterate 2 right; norm_num
+  · decide
+  iterate 2 left; norm_num
   simp only [Fintype.card_pi]
   norm_num
 #align theorems_100.birthday_measure Theorems100.birthday_measure

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -284,9 +284,9 @@ lemma integral_min_eq_two_mul :
     ∫ θ in (0)..π, min d (θ.sin * l) = 2 * ∫ θ in (0)..π / 2, min d (θ.sin * l) := by
   rw [← intervalIntegral.integral_add_adjacent_intervals (b := π / 2) (c := π)]
   conv => lhs; arg 2; arg 1; intro θ; rw [← neg_neg θ, Real.sin_neg]
-  simp_rw [intervalIntegral.integral_comp_neg fun θ => min d (-θ.sin * l), ← Real.sin_add_pi,
-    intervalIntegral.integral_comp_add_right (fun θ => min d (θ.sin * l)), add_left_neg,
-    (by ring : -(π / 2) + π = π / 2), two_mul]
+  · simp_rw [intervalIntegral.integral_comp_neg fun θ => min d (-θ.sin * l), ← Real.sin_add_pi,
+      intervalIntegral.integral_comp_add_right (fun θ => min d (θ.sin * l)), add_left_neg,
+      (by ring : -(π / 2) + π = π / 2), two_mul]
   all_goals exact intervalIntegrable_min_const_sin_mul d l _ _
 
 /--

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -198,10 +198,13 @@ theorem w_ne_one [Nontrivial ι] (i : ι) : (cs i).w ≠ 1 := by
   have hp : p ∈ (cs i').toSet := (cs i').b_mem_toSet
   have h2p : p ∈ (cs i).toSet := by
     intro j; constructor
-    trans (0 : ℝ)
-    · rw [← add_le_add_iff_right (1 : ℝ)]; convert b_add_w_le_one h; rw [hi]; rw [zero_add]
-    apply zero_le_b h; apply lt_of_lt_of_le (side_subset h <| (cs i').b_mem_side j).2
-    simp [hi, zero_le_b h]
+    · trans (0 : ℝ)
+      · rw [← add_le_add_iff_right (1 : ℝ)]; convert b_add_w_le_one h
+        · rw [hi]
+        · rw [zero_add]
+      · apply zero_le_b h
+    · apply lt_of_lt_of_le (side_subset h <| (cs i').b_mem_side j).2
+      simp [hi, zero_le_b h]
   exact (h.PairwiseDisjoint hi').le_bot ⟨hp, h2p⟩
 #align theorems_100.«82».correct.w_ne_one Theorems100.«82».Correct.w_ne_one
 

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -363,7 +363,8 @@ lemma mem_posFittingCompOf (x : L) (m : M) :
     obtain ⟨n, rfl⟩ := (mem_posFittingCompOf R x m).mp hm k
     exact this n k
   intro m l
-  induction' l with l ih; simp
+  induction' l with l ih
+  · simp
   simp only [lowerCentralSeries_succ, pow_succ', LinearMap.mul_apply]
   exact LieSubmodule.lie_mem_lie _ ⊤ (LieSubmodule.mem_top x) ih
 
@@ -602,7 +603,8 @@ lemma independent_weightSpace [NoZeroSMulDivisors R M] :
     simpa only [CompleteLattice.independent_iff_supIndep_of_injOn (injOn_weightSpace R L M),
       Finset.supIndep_iff_disjoint_erase] using fun s χ _ ↦ this _ _ (s.not_mem_erase χ)
   intro χ₁ s
-  induction' s using Finset.induction_on with χ₂ s _ ih; simp
+  induction' s using Finset.induction_on with χ₂ s _ ih
+  · simp
   intro hχ₁₂
   obtain ⟨hχ₁₂ : χ₁ ≠ χ₂, hχ₁ : χ₁ ∉ s⟩ := by rwa [Finset.mem_insert, not_or] at hχ₁₂
   specialize ih hχ₁

Mathlib/Algebra/Module/Zlattice/Basic.lean

@@ -518,8 +518,8 @@ theorem Zlattice.rank [hs : IsZlattice K L] : finrank ℤ L = finrank K E := by
   have h_card : Fintype.card (Module.Free.ChooseBasisIndex ℤ L) =
       (Set.range b).toFinset.card := by
     rw [Set.toFinset_range, Finset.univ.card_image_of_injective]
-    rfl
-    exact Subtype.coe_injective.comp (Basis.injective _)
+    · rfl
+    · exact Subtype.coe_injective.comp (Basis.injective _)
   rw [finrank_eq_card_chooseBasisIndex]
     -- We prove that `finrank ℤ L ≤ finrank K E` and `finrank K E ≤ finrank ℤ L`
   refine le_antisymm ?_ ?_

Mathlib/Algebra/Polynomial/UnitTrinomial.lean

@@ -273,10 +273,10 @@ theorem irreducible_aux2 {k m m' n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k
       rw [this] at hp
       exact Or.inl (hq.trans hp.symm)
     rw [tsub_add_eq_add_tsub hmn.le, eq_tsub_iff_add_eq_of_le, ← two_mul] at hm
-    rw [tsub_add_eq_add_tsub hmn'.le, eq_tsub_iff_add_eq_of_le, ← two_mul] at hm'
-    exact mul_left_cancel₀ two_ne_zero (hm.trans hm'.symm)
-    exact hmn'.le.trans (Nat.le_add_right n k)
-    exact hmn.le.trans (Nat.le_add_right n k)
+    · rw [tsub_add_eq_add_tsub hmn'.le, eq_tsub_iff_add_eq_of_le, ← two_mul] at hm'
+      · exact mul_left_cancel₀ two_ne_zero (hm.trans hm'.symm)
+      · exact hmn'.le.trans (Nat.le_add_right n k)
+    · exact hmn.le.trans (Nat.le_add_right n k)
 #align polynomial.is_unit_trinomial.irreducible_aux2 Polynomial.IsUnitTrinomial.irreducible_aux2
 
 theorem irreducible_aux3 {k m m' n : ℕ} (hkm : k < m) (hmn : m < n) (hkm' : k < m') (hmn' : m' < n)

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -267,7 +267,7 @@ theorem fromSpec_range :
     Set.range hU.fromSpec.1.base = (U : Set X) := by
   delta IsAffineOpen.fromSpec; dsimp
   rw [← Category.assoc, coe_comp, Set.range_comp, Set.range_iff_surjective.mpr, Set.image_univ]
-  exact Subtype.range_coe
+  · exact Subtype.range_coe
   rw [← TopCat.epi_iff_surjective]
   infer_instance
 #align algebraic_geometry.is_affine_open.from_Spec_range AlgebraicGeometry.IsAffineOpen.fromSpec_range
@@ -555,26 +555,26 @@ def _root_.AlgebraicGeometry.Scheme.affineBasicOpen
 theorem basicOpen_union_eq_self_iff (s : Set (X.presheaf.obj <| op U)) :
     ⨆ f : s, X.basicOpen (f : X.presheaf.obj <| op U) = U ↔ Ideal.span s = ⊤ := by
   trans ⋃ i : s, (PrimeSpectrum.basicOpen i.1).1 = Set.univ
-  trans
-    hU.fromSpec.1.base ⁻¹' (⨆ f : s, X.basicOpen (f : X.presheaf.obj <| op U)).1 =
-      hU.fromSpec.1.base ⁻¹' U.1
-  · refine' ⟨fun h => by rw [h], _⟩
-    intro h
-    apply_fun Set.image hU.fromSpec.1.base at h
-    rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.fromSpec_range]
-      at h
-    simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h
-    ext1
-    refine' Set.Subset.antisymm _ h
-    simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup]
-    intro x _
-    exact X.basicOpen_le x
-  · simp only [Opens.iSup_def, Subtype.coe_mk, Set.preimage_iUnion]
-    congr! 1
-    · refine congr_arg (Set.iUnion ·) ?_
-      ext1 x
-      exact congr_arg Opens.carrier (hU.fromSpec_map_basicOpen _)
-    · exact congr_arg Opens.carrier hU.fromSpec_base_preimage
+  · trans
+      hU.fromSpec.1.base ⁻¹' (⨆ f : s, X.basicOpen (f : X.presheaf.obj <| op U)).1 =
+        hU.fromSpec.1.base ⁻¹' U.1
+    · refine' ⟨fun h => by rw [h], _⟩
+      intro h
+      apply_fun Set.image hU.fromSpec.1.base at h
+      rw [Set.image_preimage_eq_inter_range, Set.image_preimage_eq_inter_range, hU.fromSpec_range]
+        at h
+      simp only [Set.inter_self, Opens.carrier_eq_coe, Set.inter_eq_right] at h
+      ext1
+      refine' Set.Subset.antisymm _ h
+      simp only [Set.iUnion_subset_iff, SetCoe.forall, Opens.coe_iSup]
+      intro x _
+      exact X.basicOpen_le x
+    · simp only [Opens.iSup_def, Subtype.coe_mk, Set.preimage_iUnion]
+      congr! 1
+      · refine congr_arg (Set.iUnion ·) ?_
+        ext1 x
+        exact congr_arg Opens.carrier (hU.fromSpec_map_basicOpen _)
+      · exact congr_arg Opens.carrier hU.fromSpec_base_preimage
   · simp only [Opens.carrier_eq_coe, PrimeSpectrum.basicOpen_eq_zeroLocus_compl]
     rw [← Set.compl_iInter, Set.compl_univ_iff, ← PrimeSpectrum.zeroLocus_iUnion, ←
       PrimeSpectrum.zeroLocus_empty_iff_eq_top, PrimeSpectrum.zeroLocus_span]

Mathlib/AlgebraicGeometry/FunctionField.lean

@@ -56,8 +56,9 @@ noncomputable instance [IsIntegral X] : Field X.functionField := by
   have hs : genericPoint X.carrier ∈ RingedSpace.basicOpen _ s := by
     rw [← SetLike.mem_coe, (genericPoint_spec X.carrier).mem_open_set_iff, Set.top_eq_univ,
       Set.univ_inter, Set.nonempty_iff_ne_empty, Ne, ← Opens.coe_bot, ← SetLike.ext'_iff]
-    erw [basicOpen_eq_bot_iff]
-    exacts [ha, (RingedSpace.basicOpen _ _).isOpen]
+    · erw [basicOpen_eq_bot_iff]
+      exact ha
+    · exact (RingedSpace.basicOpen _ _).isOpen
   have := (X.presheaf.germ ⟨_, hs⟩).isUnit_map (RingedSpace.isUnit_res_basicOpen _ s)
   rwa [TopCat.Presheaf.germ_res_apply] at this
 
@@ -87,9 +88,9 @@ theorem genericPoint_eq_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsO
   symm
   rw [eq_top_iff, Set.top_eq_univ, Set.top_eq_univ]
   convert subset_closure_inter_of_isPreirreducible_of_isOpen _ H.base_open.isOpen_range _
-  rw [Set.univ_inter, Set.image_univ]
-  apply PreirreducibleSpace.isPreirreducible_univ (X := Y.carrier)
-  exact ⟨_, trivial, Set.mem_range_self hX.2.some⟩
+  · rw [Set.univ_inter, Set.image_univ]
+  · apply PreirreducibleSpace.isPreirreducible_univ (X := Y.carrier)
+  · exact ⟨_, trivial, Set.mem_range_self hX.2.some⟩
 #align algebraic_geometry.generic_point_eq_of_is_open_immersion AlgebraicGeometry.genericPoint_eq_of_isOpenImmersion
 
 noncomputable instance stalkFunctionFieldAlgebra [IrreducibleSpace X.carrier] (x : X.carrier) :

Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

@@ -301,8 +301,8 @@ theorem AffineTargetMorphismProperty.isLocalOfOpenCoverImply (P : AffineTargetMo
   · introv hs hs'
     replace hs := ((topIsAffineOpen Y).basicOpen_union_eq_self_iff _).mpr hs
     have := H f ⟨Y.openCoverOfSuprEqTop _ hs, ?_, ?_⟩ (𝟙 _)
-    rwa [← Category.comp_id pullback.snd, ← pullback.condition, affine_cancel_left_isIso hP]
-      at this
+    · rwa [← Category.comp_id pullback.snd, ← pullback.condition, affine_cancel_left_isIso hP]
+        at this
     · intro i; exact (topIsAffineOpen Y).basicOpenIsAffine _
     · rintro (i : s)
       specialize hs' i

Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean

@@ -59,8 +59,9 @@ instance (priority := 900) quasiCompactOfIsIso {X Y : Scheme} (f : X ⟶ Y) [IsI
   intro U _ hU'
   convert hU'.image (inv f.1.base).continuous_toFun using 1
   rw [Set.image_eq_preimage_of_inverse]
-  delta Function.LeftInverse
-  exacts [IsIso.inv_hom_id_apply f.1.base, IsIso.hom_inv_id_apply f.1.base]
+  · delta Function.LeftInverse
+    exact IsIso.inv_hom_id_apply f.1.base
+  · exact IsIso.hom_inv_id_apply f.1.base
 #align algebraic_geometry.quasi_compact_of_is_iso AlgebraicGeometry.quasiCompactOfIsIso
 
 instance quasiCompactComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [QuasiCompact f]
@@ -171,14 +172,14 @@ theorem QuasiCompact.affineProperty_isLocal : (QuasiCompact.affineProperty : _).
     exact H
   · rintro X Y H f S hS hS'
     rw [← IsAffineOpen.basicOpen_union_eq_self_iff] at hS
-    delta QuasiCompact.affineProperty
-    rw [← isCompact_univ_iff]
-    change IsCompact ((Opens.map f.val.base).obj ⊤).1
-    rw [← hS]
-    dsimp [Opens.map]
-    simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk, Set.preimage_iUnion]
-    exacts [isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i),
-      topIsAffineOpen _]
+    · delta QuasiCompact.affineProperty
+      rw [← isCompact_univ_iff]
+      change IsCompact ((Opens.map f.val.base).obj ⊤).1
+      rw [← hS]
+      dsimp [Opens.map]
+      simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_mk, Set.preimage_iUnion]
+      exact isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i)
+    · exact topIsAffineOpen _
 #align algebraic_geometry.quasi_compact.affine_property_is_local AlgebraicGeometry.QuasiCompact.affineProperty_isLocal
 
 theorem QuasiCompact.affine_openCover_tfae {X Y : Scheme.{u}} (f : X ⟶ Y) :
@@ -322,8 +323,8 @@ theorem exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isCompact (X : Scheme
     convert congr_arg (X.presheaf.map (homOfLE _).op) H
     -- Note: the below was `simp only [← comp_apply]`
     · rw [← comp_apply, ← comp_apply]
-      simp only [← Functor.map_comp]
-      rfl
+      · simp only [← Functor.map_comp]
+        rfl
       · simp only [Scheme.basicOpen_res, ge_iff_le, inf_le_right]
     · rw [map_zero]
   choose n hn using H'

Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean

@@ -393,12 +393,16 @@ theorem exists_eq_pow_mul_of_isCompact_of_isQuasiSeparated (X : Scheme.{u}) (U :
     replace hs : S ⊓ U.1 = iSup fun i : s => (i : Opens X.carrier) := by ext1; simpa using hs
     have hs₁ : ∀ i : s, i.1.1 ≤ S := by
       intro i; change (i : Opens X.carrier) ≤ S
-      refine' le_trans _ inf_le_left; swap; exact U.1; erw [hs]
+      refine' le_trans _ inf_le_left; swap
+      · exact U.1
+      erw [hs]
       -- Porting note: have to add argument explicitly
       exact @le_iSup (Opens X) s _ (fun (i : s) => (i : Opens X)) i
     have hs₂ : ∀ i : s, i.1.1 ≤ U.1 := by
       intro i; change (i : Opens X.carrier) ≤ U
-      refine' le_trans _ inf_le_right; swap; exact S; erw [hs]
+      refine' le_trans _ inf_le_right; swap
+      · exact S
+      erw [hs]
       -- Porting note: have to add argument explicitly
       exact @le_iSup (Opens X) s _ (fun (i : s) => (i : Opens X)) i
     -- On each affine open in the intersection, we have `f ^ (n + n₂) * y₁ = f ^ (n + n₁) * y₂`

Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

@@ -180,25 +180,25 @@ theorem affineLocally_iff_affineOpens_le (hP : RingHom.RespectsIso @P) {X Y : Sc
       erw [Subtype.range_val]
       convert e
     have := H ⟨(Opens.map (X.ofRestrict U'.openEmbedding).1.base).obj V.1, ?h'⟩
-    erw [← X.presheaf.map_comp] at this
-    rw [← hP.cancel_right_isIso _ (X.presheaf.map (eqToHom _)), Category.assoc,
-      ← X.presheaf.map_comp]
-    convert this using 1
-    dsimp only [Functor.op, unop_op]
-    rw [Opens.openEmbedding_obj_top]
-    congr 1
-    exact e'.symm
-    case h' =>
-      apply (X.ofRestrict U'.openEmbedding).isAffineOpen_iff_of_isOpenImmersion.mp
-      -- Porting note: was convert V.2
-      erw [e']
-      apply V.2
+    · erw [← X.presheaf.map_comp] at this
+      · rw [← hP.cancel_right_isIso _ (X.presheaf.map (eqToHom _)), Category.assoc,
+          ← X.presheaf.map_comp]
+        · convert this using 1
+        dsimp only [Functor.op, unop_op]
+        rw [Opens.openEmbedding_obj_top]
+        congr 1
+        exact e'.symm
+      case h' =>
+        apply (X.ofRestrict U'.openEmbedding).isAffineOpen_iff_of_isOpenImmersion.mp
+        -- Porting note: was convert V.2
+        erw [e']
+        apply V.2
   · intro H V
     specialize H ⟨_, V.2.imageIsOpenImmersion (X.ofRestrict _)⟩ (Subtype.coe_image_subset _ _)
     erw [← X.presheaf.map_comp]
     rw [← hP.cancel_right_isIso _ (X.presheaf.map (eqToHom _)), Category.assoc, ←
       X.presheaf.map_comp]
-    convert H
+    · convert H
     · dsimp only [Functor.op, unop_op]; rw [Opens.openEmbedding_obj_top]
 #align algebraic_geometry.affine_locally_iff_affine_opens_le AlgebraicGeometry.affineLocally_iff_affineOpens_le
 
@@ -230,16 +230,16 @@ theorem sourceAffineLocally_isLocal (h₁ : RingHom.RespectsIso @P)
     apply h₃ _ _ hs
     intro r
     have := hs' r ⟨(Opens.map (X.ofRestrict _).1.base).obj U.1, ?_⟩
-    rwa [h₁.ofRestrict_morphismRestrict_iff] at this
-    · exact U.2
-    · rfl
-    · suffices ∀ (V) (_ : V = (Opens.map f.val.base).obj (Y.basicOpen r.val)),
-          IsAffineOpen ((Opens.map (X.ofRestrict V.openEmbedding).1.base).obj U.1) by
-        exact this _ rfl
-      intro V hV
-      rw [Scheme.preimage_basicOpen] at hV
-      subst hV
-      exact U.2.mapRestrictBasicOpen (Scheme.Γ.map f.op r.1)
+    · rwa [h₁.ofRestrict_morphismRestrict_iff] at this
+      · exact U.2
+      · rfl
+      · suffices ∀ (V) (_ : V = (Opens.map f.val.base).obj (Y.basicOpen r.val)),
+            IsAffineOpen ((Opens.map (X.ofRestrict V.openEmbedding).1.base).obj U.1) by
+          exact this _ rfl
+        intro V hV
+        rw [Scheme.preimage_basicOpen] at hV
+        subst hV
+        exact U.2.mapRestrictBasicOpen (Scheme.Γ.map f.op r.1)
 #align algebraic_geometry.source_affine_locally_is_local AlgebraicGeometry.sourceAffineLocally_isLocal
 
 variable (hP : RingHom.PropertyIsLocal @P)
@@ -271,9 +271,9 @@ theorem isOpenImmersionCat_comp_of_sourceAffineLocally (h₁ : RingHom.RespectsI
   rw [← h₁.cancel_right_isIso _
     (Scheme.Γ.map (IsOpenImmersion.isoOfRangeEq (Y.ofRestrict _) f _).hom.op),
     ← Functor.map_comp, ← op_comp]
-  convert h₂ ⟨_, rangeIsAffineOpenOfOpenImmersion f⟩ using 3
-  · rw [IsOpenImmersion.isoOfRangeEq_hom_fac_assoc]
-    exact Subtype.range_coe
+  · convert h₂ ⟨_, rangeIsAffineOpenOfOpenImmersion f⟩ using 3
+    · rw [IsOpenImmersion.isoOfRangeEq_hom_fac_assoc]
+      exact Subtype.range_coe
 #align algebraic_geometry.is_open_immersion_comp_of_source_affine_locally AlgebraicGeometry.isOpenImmersionCat_comp_of_sourceAffineLocally
 
 end AlgebraicGeometry