chore: tidy various files (#8409)

Mathlib/Algebra/CovariantAndContravariant.lean

@@ -43,7 +43,7 @@ A formal remark is that normally `CovariantClass` uses the `(≤)`-relation, whi
 `ContravariantClass` uses the `(<)`-relation. This need not be the case in general, but seems to be
 the most common usage. In the opposite direction, the implication
 ```lean
-[Semigroup α] [PartialOrder α] [ContravariantClass α α (*) (≤)] ↦ LeftCancelSemigroup α
+[Semigroup α] [PartialOrder α] [ContravariantClass α α (*) (≤)] → LeftCancelSemigroup α
 ```
 holds -- note the `Co*ntra*` assumption on the `(≤)`-relation.
 

Mathlib/Algebra/Group/UniqueProds.lean

@@ -203,7 +203,7 @@ theorem to_mulOpposite (h : UniqueMul A B a0 b0) :
 theorem iff_mulOpposite :
     UniqueMul (B.map ⟨_, op_injective⟩) (A.map ⟨_, op_injective⟩) (op b0) (op a0) ↔
       UniqueMul A B a0 b0 :=
-⟨of_mulOpposite, to_mulOpposite⟩
+  ⟨of_mulOpposite, to_mulOpposite⟩
 
 end Opposites
 
@@ -332,7 +332,7 @@ theorem mulHom_image_of_injective (f : H →ₙ* G) (hf : Function.Injective f)
 @[to_additive "`UniqueSums` is preserved under additive equivalences."]
 theorem mulHom_image_iff (f : G ≃* H) :
     UniqueProds G ↔ UniqueProds H :=
-⟨mulHom_image_of_injective f.symm f.symm.injective, mulHom_image_of_injective f f.injective⟩
+  ⟨mulHom_image_of_injective f.symm f.symm.injective, mulHom_image_of_injective f f.injective⟩
 
 open Finset MulOpposite in
 @[to_additive]
@@ -500,7 +500,7 @@ theorem mulHom_image_of_injective (f : H →ₙ* G) (hf : Function.Injective f)
 /-- `TwoUniqueProd` is preserved under multiplicative equivalences. -/
 @[to_additive "`TwoUniqueSums` is preserved under additive equivalences."]
 theorem mulHom_image_iff (f : G ≃* H) : TwoUniqueProds G ↔ TwoUniqueProds H :=
-⟨mulHom_image_of_injective f.symm f.symm.injective, mulHom_image_of_injective f f.injective⟩
+  ⟨mulHom_image_of_injective f.symm f.symm.injective, mulHom_image_of_injective f f.injective⟩
 
 @[to_additive] instance {ι} (G : ι → Type*) [∀ i, Mul (G i)] [∀ i, TwoUniqueProds (G i)] :
     TwoUniqueProds (∀ i, G i) where
@@ -564,7 +564,7 @@ theorem of_mulOpposite (h : TwoUniqueProds Gᵐᵒᵖ) : TwoUniqueProds G where
 @[to_additive
   "This instance asserts that if `G` has a right-cancellative addition, a linear order,
   and addition is strictly monotone w.r.t. the second argument, then `G` has `TwoUniqueSums`." ]
-instance (priority := 100) of_Covariant_right [IsRightCancelMul G]
+instance (priority := 100) of_covariant_right [IsRightCancelMul G]
     [LinearOrder G] [CovariantClass G G (· * ·) (· < ·)] :
     TwoUniqueProds G where
   uniqueMul_of_one_lt_card {A B} hc := by
@@ -598,13 +598,13 @@ open MulOpposite in
 @[to_additive
   "This instance asserts that if `G` has a left-cancellative addition, a linear order, and
   addition is strictly monotone w.r.t. the first argument, then `G` has `TwoUniqueSums`." ]
-instance (priority := 100) of_Covariant_left [IsLeftCancelMul G]
+instance (priority := 100) of_covariant_left [IsLeftCancelMul G]
     [LinearOrder G] [CovariantClass G G (Function.swap (· * ·)) (· < ·)] :
     TwoUniqueProds G :=
   let _ := LinearOrder.lift' (unop : Gᵐᵒᵖ → G) unop_injective
   let _ : CovariantClass Gᵐᵒᵖ Gᵐᵒᵖ (· * ·) (· < ·) :=
-  { elim := fun _ _ _ bc ↦ mul_lt_mul_right' (α := G) bc (unop _) }
-  of_mulOpposite of_Covariant_right
+    { elim := fun _ _ _ bc ↦ mul_lt_mul_right' (α := G) bc (unop _) }
+  of_mulOpposite of_covariant_right
 
 end TwoUniqueProds
 

Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

@@ -97,9 +97,9 @@ as a product of monomials in the supports of `f` and `g` is a product. -/
 theorem mul_apply_add_eq_mul_of_uniqueAdd [Add A] {f g : R[A]} {a0 b0 : A}
     (h : UniqueAdd f.support g.support a0 b0) :
     (f * g) (a0 + b0) = f a0 * g b0 :=
-MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul (A := Multiplicative A) h
+  MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul (A := Multiplicative A) h
 
 instance [NoZeroDivisors R] [Add A] [UniqueSums A] : NoZeroDivisors R[A] :=
-MonoidAlgebra.instNoZeroDivisorsOfUniqueProds (A := Multiplicative A)
+  MonoidAlgebra.instNoZeroDivisorsOfUniqueProds (A := Multiplicative A)
 
 end AddMonoidAlgebra

Mathlib/Analysis/Convex/Cone/Proper.lean

@@ -75,7 +75,7 @@ cone programs and proving duality theorems. -/
 structure ProperCone (𝕜 : Type*) (E : Type*) [OrderedSemiring 𝕜] [AddCommMonoid E]
     [TopologicalSpace E] [SMul 𝕜 E] extends ConvexCone 𝕜 E where
   nonempty' : (carrier : Set E).Nonempty
-  is_closed' : IsClosed (carrier : Set E)
+  isClosed' : IsClosed (carrier : Set E)
 #align proper_cone ProperCone
 
 namespace ProperCone
@@ -86,14 +86,16 @@ variable {𝕜 : Type*} [OrderedSemiring 𝕜]
 
 variable {E : Type*} [AddCommMonoid E] [TopologicalSpace E] [SMul 𝕜 E]
 
+attribute [coe] toConvexCone
+
 instance : Coe (ProperCone 𝕜 E) (ConvexCone 𝕜 E) :=
-  ⟨fun K => K.1⟩
+  ⟨toConvexCone⟩
 
 -- Porting note: now a syntactic tautology
 -- @[simp]
 -- theorem toConvexCone_eq_coe (K : ProperCone 𝕜 E) : K.toConvexCone = K :=
 --   rfl
--- #align proper_cone.to_convex_cone_eq_coe ProperCone.toConvexCone_eq_coe
+#noalign proper_cone.to_convex_cone_eq_coe
 
 theorem ext' : Function.Injective ((↑) : ProperCone 𝕜 E → ConvexCone 𝕜 E) := fun S T h => by
   cases S; cases T; congr
@@ -119,7 +121,7 @@ protected theorem nonempty (K : ProperCone 𝕜 E) : (K : Set E).Nonempty :=
 #align proper_cone.nonempty ProperCone.nonempty
 
 protected theorem isClosed (K : ProperCone 𝕜 E) : IsClosed (K : Set E) :=
-  K.is_closed'
+  K.isClosed'
 #align proper_cone.is_closed ProperCone.isClosed
 
 end SMul
@@ -135,7 +137,7 @@ module. -/
 def positive : ProperCone 𝕜 E where
   toConvexCone := ConvexCone.positive 𝕜 E
   nonempty' := ⟨0, ConvexCone.pointed_positive _ _⟩
-  is_closed' := isClosed_Ici
+  isClosed' := isClosed_Ici
 
 @[simp]
 theorem mem_positive {x : E} : x ∈ positive 𝕜 E ↔ 0 ≤ x :=
@@ -156,7 +158,7 @@ variable {E : Type*} [AddCommMonoid E] [TopologicalSpace E] [T1Space E] [Module
 instance : Zero (ProperCone 𝕜 E) :=
   ⟨{  toConvexCone := 0
       nonempty' := ⟨0, rfl⟩
-      is_closed' := isClosed_singleton }⟩
+      isClosed' := isClosed_singleton }⟩
 
 instance : Inhabited (ProperCone 𝕜 E) :=
   ⟨0⟩
@@ -166,7 +168,7 @@ theorem mem_zero (x : E) : x ∈ (0 : ProperCone 𝕜 E) ↔ x = 0 :=
   Iff.rfl
 #align proper_cone.mem_zero ProperCone.mem_zero
 
-@[simp] -- Porting note: removed `norm_cast` (new-style structures)
+@[simp, norm_cast]
 theorem coe_zero : ↑(0 : ProperCone 𝕜 E) = (0 : ConvexCone 𝕜 E) :=
   rfl
 #align proper_cone.coe_zero ProperCone.coe_zero
@@ -194,10 +196,10 @@ noncomputable def map (f : E →L[ℝ] F) (K : ProperCone ℝ E) : ProperCone 
   toConvexCone := ConvexCone.closure (ConvexCone.map (f : E →ₗ[ℝ] F) ↑K)
   nonempty' :=
     ⟨0, subset_closure <| SetLike.mem_coe.2 <| ConvexCone.mem_map.2 ⟨0, K.pointed, map_zero _⟩⟩
-  is_closed' := isClosed_closure
+  isClosed' := isClosed_closure
 #align proper_cone.map ProperCone.map
 
-@[simp] -- Porting note: removed `norm_cast` (new-style structures)
+@[simp, norm_cast]
 theorem coe_map (f : E →L[ℝ] F) (K : ProperCone ℝ E) :
     ↑(K.map f) = (ConvexCone.map (f : E →ₗ[ℝ] F) ↑K).closure :=
   rfl
@@ -218,10 +220,10 @@ theorem map_id (K : ProperCone ℝ E) : K.map (ContinuousLinearMap.id ℝ E) = K
 def dual (K : ProperCone ℝ E) : ProperCone ℝ E where
   toConvexCone := (K : Set E).innerDualCone
   nonempty' := ⟨0, pointed_innerDualCone _⟩
-  is_closed' := isClosed_innerDualCone _
+  isClosed' := isClosed_innerDualCone _
 #align proper_cone.dual ProperCone.dual
 
-@[simp] -- Porting note: removed `norm_cast` (new-style structures)
+@[simp, norm_cast]
 theorem coe_dual (K : ProperCone ℝ E) : ↑(dual K) = (K : Set E).innerDualCone :=
   rfl
 #align proper_cone.coe_dual ProperCone.coe_dual
@@ -232,14 +234,13 @@ theorem mem_dual {K : ProperCone ℝ E} {y : E} : y ∈ dual K ↔ ∀ ⦃x⦄,
 #align proper_cone.mem_dual ProperCone.mem_dual
 
 /-- The preimage of a proper cone under a continuous `ℝ`-linear map is a proper cone. -/
-noncomputable def comap (f : E →L[ℝ] F) (S : ProperCone ℝ F) : ProperCone ℝ E
-    where
+noncomputable def comap (f : E →L[ℝ] F) (S : ProperCone ℝ F) : ProperCone ℝ E where
   toConvexCone := ConvexCone.comap (f : E →ₗ[ℝ] F) S
   nonempty' :=
     ⟨0, by
       simp only [ConvexCone.comap, mem_preimage, map_zero, SetLike.mem_coe, mem_coe]
       apply ProperCone.pointed⟩
-  is_closed' := by
+  isClosed' := by
     simp only [ConvexCone.comap, ContinuousLinearMap.coe_coe]
     apply IsClosed.preimage f.2 S.isClosed
 #align proper_cone.comap ProperCone.comap
@@ -292,8 +293,7 @@ theorem hyperplane_separation (K : ProperCone ℝ E) {f : E →L[ℝ] F} {b : F}
         ConvexCone.mem_closure, mem_closure_iff_seq_limit]
       -- there is a sequence `seq : ℕ → F` in the image of `f` that converges to `b`
       rintro ⟨seq, hmem, htends⟩ y hinner
-      suffices h : ∀ n, 0 ≤ ⟪y, seq n⟫_ℝ;
-      exact
+      suffices h : ∀ n, 0 ≤ ⟪y, seq n⟫_ℝ from
         ge_of_tendsto'
           (Continuous.seqContinuous (Continuous.inner (@continuous_const _ _ _ _ y) continuous_id)
             htends)

Mathlib/Data/Polynomial/Div.lean

@@ -237,7 +237,7 @@ theorem degree_modByMonic_le (p : R[X]) {q : R[X]} (hq : Monic q) : degree (p %
 
 theorem natDegree_modByMonic_le (p : Polynomial R) {g : Polynomial R} (hg : g.Monic) :
     natDegree (p %ₘ g) ≤ g.natDegree :=
-natDegree_le_natDegree (degree_modByMonic_le p hg)
+  natDegree_le_natDegree (degree_modByMonic_le p hg)
 
 end Ring
 

Mathlib/Data/Polynomial/Inductions.lean

@@ -94,9 +94,9 @@ theorem divX_X_pow : divX (X ^ n : R[X]) = if (n = 0) then 0 else X ^ (n - 1) :=
 /-- `divX` as an additive homomorphism. -/
 noncomputable
 def divX_hom : R[X] →+ R[X] :=
-{ toFun := divX
-  map_zero' := divX_zero
-  map_add' := fun _ _ => divX_add }
+  { toFun := divX
+    map_zero' := divX_zero
+    map_add' := fun _ _ => divX_add }
 
 @[simp] theorem divX_hom_toFun : divX_hom p = divX p := rfl
 
@@ -111,7 +111,7 @@ theorem natDegree_divX_eq_natDegree_tsub_one : p.divX.natDegree = p.natDegree -
     · exact natDegree_C_mul_X_pow (n - 1) c c0
 
 theorem natDegree_divX_le : p.divX.natDegree ≤ p.natDegree :=
-natDegree_divX_eq_natDegree_tsub_one.trans_le (Nat.pred_le _)
+  natDegree_divX_eq_natDegree_tsub_one.trans_le (Nat.pred_le _)
 
 theorem divX_C_mul_X_pow : divX (C a * X ^ n) = if n = 0 then 0 else C a * X ^ (n - 1) := by
   simp only [divX_C_mul, divX_X_pow, mul_ite, mul_zero]

Mathlib/MeasureTheory/Measure/VectorMeasure.lean

@@ -54,7 +54,7 @@ variable {α β : Type*} {m : MeasurableSpace α}
 /-- A vector measure on a measurable space `α` is a σ-additive `M`-valued function (for some `M`
 an add monoid) such that the empty set and non-measurable sets are mapped to zero. -/
 structure VectorMeasure (α : Type*) [MeasurableSpace α] (M : Type*) [AddCommMonoid M]
-  [TopologicalSpace M] where
+    [TopologicalSpace M] where
   measureOf' : Set α → M
   empty' : measureOf' ∅ = 0
   not_measurable' ⦃i : Set α⦄ : ¬MeasurableSet i → measureOf' i = 0
@@ -701,8 +701,7 @@ theorem restrict_univ : v.restrict Set.univ = v :=
 theorem restrict_zero {i : Set α} : (0 : VectorMeasure α M).restrict i = 0 := by
   by_cases hi : MeasurableSet i
   · ext j hj
-    rw [restrict_apply 0 hi hj]
-    rfl
+    rw [restrict_apply 0 hi hj, zero_apply, zero_apply]
   · exact dif_neg hi
 #align measure_theory.vector_measure.restrict_zero MeasureTheory.VectorMeasure.restrict_zero
 
@@ -1151,7 +1150,6 @@ def MutuallySingular (v : VectorMeasure α M) (w : VectorMeasure α N) : Prop :=
   ∃ s : Set α, MeasurableSet s ∧ (∀ (t) (_ : t ⊆ s), v t = 0) ∧ ∀ (t) (_ : t ⊆ sᶜ), w t = 0
 #align measure_theory.vector_measure.mutually_singular MeasureTheory.VectorMeasure.MutuallySingular
 
--- mathport name: vector_measure.mutually_singular
 @[inherit_doc VectorMeasure.MutuallySingular]
 scoped[MeasureTheory] infixl:60 " ⟂ᵥ " => MeasureTheory.VectorMeasure.MutuallySingular
 

Mathlib/ModelTheory/Algebra/Field/Basic.lean

@@ -45,7 +45,7 @@ inductive FieldAxiom : Type
   | oneMul : FieldAxiom
   | existsInv : FieldAxiom
   | leftDistrib : FieldAxiom
-  | existsPairNe : FieldAxiom
+  | existsPairNE : FieldAxiom
 
 /-- The first order sentence corresponding to each field axiom -/
 @[simp]
@@ -58,7 +58,7 @@ def FieldAxiom.toSentence : FieldAxiom → Language.ring.Sentence
   | .oneMul => ∀' (((1 : Language.ring.Term _) * &0) =' &0)
   | .existsInv => ∀' (∼(&0 =' 0) ⟹ ∃' ((&0 * &1) =' 1))
   | .leftDistrib => ∀' ∀' ∀' ((&0 * (&1 + &2)) =' ((&0 * &1) + (&0 * &2)))
-  | .existsPairNe => ∃' ∃' (∼(&0 =' &1))
+  | .existsPairNE => ∃' ∃' (∼(&0 =' &1))
 
 /-- The Proposition corresponding to each field axiom -/
 @[simp]
@@ -72,7 +72,7 @@ def FieldAxiom.toProp (K : Type*) [Add K] [Mul K] [Neg K] [Zero K] [One K] :
   | .oneMul => ∀ x : K, 1 * x = x
   | .existsInv => ∀ x : K, x ≠ 0 → ∃ y, x * y = 1
   | .leftDistrib => ∀ x y z : K, x * (y + z) = x * y + x * z
-  | .existsPairNe => ∃ x y : K, x ≠ y
+  | .existsPairNE => ∃ x y : K, x ≠ y
 
 /-- The first order theory of fields, as a theory over the language of rings -/
 def _root_.FirstOrder.Language.Theory.field : Language.ring.Theory :=
@@ -123,7 +123,7 @@ noncomputable def fieldOfModelField (K : Type*) [Language.ring.Structure K]
         (dif_neg hx0).symm ▸ Classical.choose_spec (existsInv.toProp_of_model x hx0))
     (dif_pos rfl)
     leftDistrib.toProp_of_model
-    existsPairNe.toProp_of_model
+    existsPairNE.toProp_of_model
 
 section
 
@@ -148,7 +148,7 @@ instance [Field K] [CompatibleRing K] : Theory.field.Model K :=
       rintro φ a rfl
       rw [a.realize_toSentence_iff_toProp (K := K)]
       cases a with
-      | existsPairNe => exact exists_pair_ne K
+      | existsPairNE => exact exists_pair_ne K
       | existsInv => exact fun x hx0 => ⟨x⁻¹, mul_inv_cancel hx0⟩
       | addAssoc => exact add_assoc
       | zeroAdd => exact zero_add

Mathlib/Order/Filter/Basic.lean

@@ -380,8 +380,8 @@ theorem mem_generate_iff {s : Set <| Set α} {U : Set α} :
 #align filter.mem_generate_iff Filter.mem_generate_iff
 
 @[simp] lemma generate_singleton (s : Set α) : generate {s} = 𝓟 s :=
-le_antisymm (λ _t ht ↦ mem_of_superset (mem_generate_of_mem $ mem_singleton _) ht) $
-  le_generate_iff.2 $ singleton_subset_iff.2 Subset.rfl
+  le_antisymm (λ _t ht ↦ mem_of_superset (mem_generate_of_mem $ mem_singleton _) ht) <|
+    le_generate_iff.2 $ singleton_subset_iff.2 Subset.rfl
 
 /-- `mk_of_closure s hs` constructs a filter on `α` whose elements set is exactly
 `s : Set (Set α)`, provided one gives the assumption `hs : (generate s).sets = s`. -/

Mathlib/Order/Monotone/Basic.lean

@@ -246,23 +246,23 @@ theorem monotone_dual_iff : Monotone (toDual ∘ f ∘ ofDual : αᵒᵈ → β
 theorem antitone_dual_iff : Antitone (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ Antitone f := by
   rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff]
 
-theorem monotone_on_dual_iff : MonotoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ MonotoneOn f s := by
+theorem monotoneOn_dual_iff : MonotoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ MonotoneOn f s := by
   rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff]
 
-theorem antitone_on_dual_iff : AntitoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ AntitoneOn f s := by
+theorem antitoneOn_dual_iff : AntitoneOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ AntitoneOn f s := by
   rw [antitoneOn_toDual_comp_iff, monotoneOn_comp_ofDual_iff]
 
-theorem strict_mono_dual_iff : StrictMono (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictMono f := by
+theorem strictMono_dual_iff : StrictMono (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictMono f := by
   rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff]
 
-theorem strict_anti_dual_iff : StrictAnti (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictAnti f := by
+theorem strictAnti_dual_iff : StrictAnti (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) ↔ StrictAnti f := by
   rw [strictAnti_toDual_comp_iff, strictMono_comp_ofDual_iff]
 
-theorem strict_mono_on_dual_iff :
+theorem strictMonoOn_dual_iff :
     StrictMonoOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictMonoOn f s := by
   rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff]
 
-theorem strict_anti_on_dual_iff :
+theorem strictAntiOn_dual_iff :
     StrictAntiOn (toDual ∘ f ∘ ofDual : αᵒᵈ → βᵒᵈ) s ↔ StrictAntiOn f s := by
   rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff]
 
@@ -320,22 +320,22 @@ alias ⟨_, Monotone.dual⟩ := monotone_dual_iff
 alias ⟨_, Antitone.dual⟩ := antitone_dual_iff
 #align antitone.dual Antitone.dual
 
-alias ⟨_, MonotoneOn.dual⟩ := monotone_on_dual_iff
+alias ⟨_, MonotoneOn.dual⟩ := monotoneOn_dual_iff
 #align monotone_on.dual MonotoneOn.dual
 
-alias ⟨_, AntitoneOn.dual⟩ := antitone_on_dual_iff
+alias ⟨_, AntitoneOn.dual⟩ := antitoneOn_dual_iff
 #align antitone_on.dual AntitoneOn.dual
 
-alias ⟨_, StrictMono.dual⟩ := strict_mono_dual_iff
+alias ⟨_, StrictMono.dual⟩ := strictMono_dual_iff
 #align strict_mono.dual StrictMono.dual
 
-alias ⟨_, StrictAnti.dual⟩ := strict_anti_dual_iff
+alias ⟨_, StrictAnti.dual⟩ := strictAnti_dual_iff
 #align strict_anti.dual StrictAnti.dual
 
-alias ⟨_, StrictMonoOn.dual⟩ := strict_mono_on_dual_iff
+alias ⟨_, StrictMonoOn.dual⟩ := strictMonoOn_dual_iff
 #align strict_mono_on.dual StrictMonoOn.dual
 
-alias ⟨_, StrictAntiOn.dual⟩ := strict_anti_on_dual_iff
+alias ⟨_, StrictAntiOn.dual⟩ := strictAntiOn_dual_iff
 #align strict_anti_on.dual StrictAntiOn.dual
 
 end OrderDual