chore: adaptations for lean4#5542 (#17564)

kmill · kmill · commit e2b29fbc0b17 · 2024-10-09T08:43:10.000Z
In [lean4#5542](leanprover/lean4#5542) we are deprecating `inductive ... :=`, `structure ... :=`, and `class ... :=` for their `... where` counterparts.
diff --git a/Mathlib/Algebra/Category/BialgebraCat/Basic.lean b/Mathlib/Algebra/Category/BialgebraCat/Basic.lean
@@ -59,7 +59,7 @@ lemma of_counit {X : Type v} [Ring X] [Bialgebra R X] :
 /-- A type alias for `BialgHom` to avoid confusion between the categorical and
 algebraic spellings of composition. -/
 @[ext]
-structure Hom (V W : BialgebraCat.{v} R) :=
+structure Hom (V W : BialgebraCat.{v} R) where
   /-- The underlying `BialgHom` -/
   toBialgHom : V →ₐc[R] W
 
diff --git a/Mathlib/Algebra/Category/CoalgebraCat/Basic.lean b/Mathlib/Algebra/Category/CoalgebraCat/Basic.lean
@@ -62,7 +62,7 @@ lemma of_counit {X : Type v} [AddCommGroup X] [Module R X] [Coalgebra R X] :
 /-- A type alias for `CoalgHom` to avoid confusion between the categorical and
 algebraic spellings of composition. -/
 @[ext]
-structure Hom (V W : CoalgebraCat.{v} R) :=
+structure Hom (V W : CoalgebraCat.{v} R) where
   /-- The underlying `CoalgHom` -/
   toCoalgHom : V →ₗc[R] W
 
diff --git a/Mathlib/Algebra/Category/HopfAlgebraCat/Basic.lean b/Mathlib/Algebra/Category/HopfAlgebraCat/Basic.lean
@@ -58,7 +58,7 @@ lemma of_counit {X : Type v} [Ring X] [HopfAlgebra R X] :
 /-- A type alias for `BialgHom` to avoid confusion between the categorical and
 algebraic spellings of composition. -/
 @[ext]
-structure Hom (V W : HopfAlgebraCat.{v} R) :=
+structure Hom (V W : HopfAlgebraCat.{v} R) where
   /-- The underlying `BialgHom`. -/
   toBialgHom : V →ₐc[R] W
 
diff --git a/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean b/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@@ -381,7 +381,7 @@ variable (S₁ S₂ S₃ : SnakeInput C)
 /-- A morphism of snake inputs involve four morphisms of short complexes
 which make the obvious diagram commute. -/
 @[ext]
-structure Hom :=
+structure Hom where
   /-- a morphism between the zeroth lines -/
   f₀ : S₁.L₀ ⟶ S₂.L₀
   /-- a morphism between the first lines -/
diff --git a/Mathlib/Algebra/Lie/Killing.lean b/Mathlib/Algebra/Lie/Killing.lean
@@ -46,7 +46,7 @@ namespace LieAlgebra
 
 NB: This is not standard terminology (the literature does not seem to name Lie algebras with this
 property). -/
-class IsKilling : Prop :=
+class IsKilling : Prop where
   /-- We say a Lie algebra is Killing if its Killing form is non-singular. -/
   killingCompl_top_eq_bot : LieIdeal.killingCompl R L ⊤ = ⊥
 
diff --git a/Mathlib/Algebra/Lie/Weights/Basic.lean b/Mathlib/Algebra/Lie/Weights/Basic.lean
@@ -724,7 +724,7 @@ noncomputable instance Weight.instFintype [NoZeroSMulDivisors R M] [IsNoetherian
 
 /-- A Lie module `M` of a Lie algebra `L` is triangularizable if the endomorhpism of `M` defined by
 any `x : L` is triangularizable. -/
-class IsTriangularizable : Prop :=
+class IsTriangularizable : Prop where
   iSup_eq_top : ∀ x, ⨆ φ, ⨆ k, (toEnd R L M x).genEigenspace φ k = ⊤
 
 instance (L' : LieSubalgebra R L) [IsTriangularizable R L M] : IsTriangularizable R L' M where
diff --git a/Mathlib/Algebra/Lie/Weights/Linear.lean b/Mathlib/Algebra/Lie/Weights/Linear.lean
@@ -48,7 +48,7 @@ namespace LieModule
 
 /-- A typeclass encoding the fact that a given Lie module has linear weights, vanishing on the
 derived ideal. -/
-class LinearWeights [LieAlgebra.IsNilpotent R L] : Prop :=
+class LinearWeights [LieAlgebra.IsNilpotent R L] : Prop where
   map_add : ∀ χ : L → R, genWeightSpace M χ ≠ ⊥ → ∀ x y, χ (x + y) = χ x + χ y
   map_smul : ∀ χ : L → R, genWeightSpace M χ ≠ ⊥ → ∀ (t : R) x, χ (t • x) = t • χ x
   map_lie : ∀ χ : L → R, genWeightSpace M χ ≠ ⊥ → ∀ x y : L, χ ⁅x, y⁆ = 0
diff --git a/Mathlib/Algebra/Quandle.lean b/Mathlib/Algebra/Quandle.lean
@@ -100,9 +100,9 @@ class Shelf (α : Type u) where
 A *unital shelf* is a shelf equipped with an element `1` such that, for all elements `x`,
 we have both `x ◃ 1` and `1 ◃ x` equal `x`.
 -/
-class UnitalShelf (α : Type u) extends Shelf α, One α :=
-(one_act : ∀ a : α, act 1 a = a)
-(act_one : ∀ a : α, act a 1 = a)
+class UnitalShelf (α : Type u) extends Shelf α, One α where
+  one_act : ∀ a : α, act 1 a = a
+  act_one : ∀ a : α, act a 1 = a
 
 /-- The type of homomorphisms between shelves.
 This is also the notion of rack and quandle homomorphisms.
diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean
@@ -579,7 +579,7 @@ open MeasureTheory Module
 
 /-- A measure `μ` has temperate growth if there is an `n : ℕ` such that `(1 + ‖x‖) ^ (- n)` is
 `μ`-integrable. -/
-class _root_.MeasureTheory.Measure.HasTemperateGrowth (μ : Measure D) : Prop :=
+class _root_.MeasureTheory.Measure.HasTemperateGrowth (μ : Measure D) : Prop where
   exists_integrable : ∃ (n : ℕ), Integrable (fun x ↦ (1 + ‖x‖) ^ (- (n : ℝ))) μ
 
 open Classical in
diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/Mul.lean
@@ -121,7 +121,7 @@ examples. Any algebra with an approximate identity (e.g., $$L^1$$) is also regul
 
 This is a useful class because it gives rise to a nice norm on the unitization; in particular it is
 a C⋆-norm when the norm on `A` is a C⋆-norm. -/
-class _root_.RegularNormedAlgebra : Prop :=
+class _root_.RegularNormedAlgebra : Prop where
   /-- The left regular representation of the algebra on itself is an isometry. -/
   isometry_mul' : Isometry (mul 𝕜 𝕜')
 
diff --git a/Mathlib/Analysis/RCLike/Basic.lean b/Mathlib/Analysis/RCLike/Basic.lean
@@ -1086,7 +1086,7 @@ section
 /-- A mixin over a normed field, saying that the norm field structure is the same as `ℝ` or `ℂ`.
 To endow such a field with a compatible `RCLike` structure in a proof, use
 `letI := IsRCLikeNormedField.rclike 𝕜`.-/
-class IsRCLikeNormedField (𝕜 : Type*) [hk : NormedField 𝕜] : Prop :=
+class IsRCLikeNormedField (𝕜 : Type*) [hk : NormedField 𝕜] : Prop where
   out : ∃ h : RCLike 𝕜, hk = h.toNormedField
 
 instance (priority := 100) (𝕜 : Type*) [h : RCLike 𝕜] : IsRCLikeNormedField 𝕜 := ⟨⟨h, rfl⟩⟩
diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean
@@ -252,7 +252,7 @@ alias tendsto_pow_atTop_nhds_0_of_abs_lt_1 := tendsto_pow_atTop_nhds_zero_of_abs
 /-- A normed ring has summable geometric series if, for all `ξ` of norm `< 1`, the geometric series
 `∑ ξ ^ n` converges. This holds both in complete normed rings and in normed fields, providing a
 convenient abstraction of these two classes to avoid repeating the same proofs. -/
-class HasSummableGeomSeries (K : Type*) [NormedRing K] : Prop :=
+class HasSummableGeomSeries (K : Type*) [NormedRing K] : Prop where
   summable_geometric_of_norm_lt_one : ∀ (ξ : K), ‖ξ‖ < 1 → Summable (fun n ↦ ξ ^ n)
 
 lemma summable_geometric_of_norm_lt_one {K : Type*} [NormedRing K] [HasSummableGeomSeries K]
diff --git a/Mathlib/CategoryTheory/GradedObject/Trifunctor.lean b/Mathlib/CategoryTheory/GradedObject/Trifunctor.lean
@@ -259,7 +259,7 @@ variable (F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂) (G : C₁₂ ⥤ C₃ ⥤ C₄)
 /-- Given a map `r : I₁ × I₂ × I₃ → J`, a `BifunctorComp₁₂IndexData r` consists of the data
 of a type `I₁₂`, maps `p : I₁ × I₂ → I₁₂` and `q : I₁₂ × I₃ → J`, such that `r` is obtained
 by composition of `p` and `q`. -/
-structure BifunctorComp₁₂IndexData :=
+structure BifunctorComp₁₂IndexData where
   /-- an auxiliary type -/
   I₁₂ : Type*
   /-- a map `I₁ × I₂ → I₁₂` -/
@@ -439,7 +439,7 @@ variable (F : C₁ ⥤ C₂₃ ⥤ C₄) (G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃)
 /-- Given a map `r : I₁ × I₂ × I₃ → J`, a `BifunctorComp₂₃IndexData r` consists of the data
 of a type `I₂₃`, maps `p : I₂ × I₃ → I₂₃` and `q : I₁ × I₂₃ → J`, such that `r` is obtained
 by composition of `p` and `q`. -/
-structure BifunctorComp₂₃IndexData :=
+structure BifunctorComp₂₃IndexData where
   /-- an auxiliary type -/
   I₂₃ : Type*
   /-- a map `I₂ × I₃ → I₂₃` -/
diff --git a/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean b/Mathlib/CategoryTheory/Localization/LocalizerMorphism.lean
@@ -128,7 +128,7 @@ lemma isEquivalence_iff : G.IsEquivalence ↔ G'.IsEquivalence :=
 end
 
 /-- Condition that a `LocalizerMorphism` induces an equivalence on the localized categories -/
-class IsLocalizedEquivalence : Prop :=
+class IsLocalizedEquivalence : Prop where
   /-- the induced functor on the constructed localized categories is an equivalence -/
   isEquivalence : (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence
 
diff --git a/Mathlib/CategoryTheory/MorphismProperty/Composition.lean b/Mathlib/CategoryTheory/MorphismProperty/Composition.lean
@@ -24,7 +24,7 @@ namespace MorphismProperty
 variable {C : Type u} [Category.{v} C] {D : Type u'} [Category.{v'} D]
 
 /-- Typeclass expressing that a morphism property contain identities. -/
-class ContainsIdentities (W : MorphismProperty C) : Prop :=
+class ContainsIdentities (W : MorphismProperty C) : Prop where
   /-- for all `X : C`, the identity of `X` satisfies the morphism property -/
   id_mem : ∀ (X : C), W (𝟙 X)
 
@@ -63,7 +63,7 @@ instance Pi.containsIdentities {J : Type w} {C : J → Type u}
 
 /-- A morphism property satisfies `IsStableUnderComposition` if the composition of
 two such morphisms still falls in the class. -/
-class IsStableUnderComposition (P : MorphismProperty C) : Prop :=
+class IsStableUnderComposition (P : MorphismProperty C) : Prop where
   comp_mem {X Y Z} (f : X ⟶ Y) (g : Y ⟶ Z) : P f → P g → P (f ≫ g)
 
 lemma comp_mem (W : MorphismProperty C) [W.IsStableUnderComposition]
@@ -129,7 +129,7 @@ end naturalityProperty
 /-- A morphism property is multiplicative if it contains identities and is stable by
 composition. -/
 class IsMultiplicative (W : MorphismProperty C)
-    extends W.ContainsIdentities, W.IsStableUnderComposition : Prop :=
+    extends W.ContainsIdentities, W.IsStableUnderComposition : Prop
 
 namespace IsMultiplicative
 
diff --git a/Mathlib/CategoryTheory/MorphismProperty/Limits.lean b/Mathlib/CategoryTheory/MorphismProperty/Limits.lean
@@ -203,7 +203,7 @@ lemma IsStableUnderProductsOfShape.mk (J : Type*)
   simp
 
 /-- The condition that a property of morphisms is stable by finite products. -/
-class IsStableUnderFiniteProducts : Prop :=
+class IsStableUnderFiniteProducts : Prop where
   isStableUnderProductsOfShape (J : Type) [Finite J] : W.IsStableUnderProductsOfShape J
 
 lemma isStableUnderProductsOfShape_of_isStableUnderFiniteProducts
diff --git a/Mathlib/CategoryTheory/Shift/CommShift.lean b/Mathlib/CategoryTheory/Shift/CommShift.lean
@@ -246,7 +246,7 @@ variable {C D E J : Type*} [Category C] [Category D] [Category E] [Category J]
 /-- If `τ : F₁ ⟶ F₂` is a natural transformation between two functors
 which commute with a shift by an additive monoid `A`, this typeclass
 asserts a compatibility of `τ` with these shifts. -/
-class CommShift : Prop :=
+class CommShift : Prop where
   comm' (a : A) : (F₁.commShiftIso a).hom ≫ whiskerRight τ _ =
     whiskerLeft _ τ ≫ (F₂.commShiftIso a).hom
 
diff --git a/Mathlib/CategoryTheory/Shift/Localization.lean b/Mathlib/CategoryTheory/Shift/Localization.lean
@@ -32,7 +32,7 @@ namespace MorphismProperty
 /-- A morphism property `W` on a category `C` is compatible with the shift by a
 monoid `A` when for all `a : A`, a morphism `f` belongs to `W`
 if and only if `f⟦a⟧'` does. -/
-class IsCompatibleWithShift : Prop :=
+class IsCompatibleWithShift : Prop where
   /-- the condition that for all `a : A`, the morphism property `W` is not changed when
   we take its inverse image by the shift functor by `a` -/
   condition : ∀ (a : A), W.inverseImage (shiftFunctor C a) = W
diff --git a/Mathlib/CategoryTheory/Shift/Quotient.lean b/Mathlib/CategoryTheory/Shift/Quotient.lean
@@ -32,7 +32,7 @@ namespace HomRel
 
 /-- A relation on morphisms is compatible with the shift by a monoid `A` when the
 relation if preserved by the shift. -/
-class IsCompatibleWithShift : Prop :=
+class IsCompatibleWithShift : Prop where
   /-- the condition that the relation is preserved by the shift -/
   condition : ∀ (a : A) ⦃X Y : C⦄ (f g : X ⟶ Y), r f g → r (f⟦a⟧') (g⟦a⟧')
 
diff --git a/Mathlib/Combinatorics/Colex.lean b/Mathlib/Combinatorics/Colex.lean
@@ -65,7 +65,7 @@ namespace Finset
 /-- Type synonym of `Finset α` equipped with the colexicographic order rather than the inclusion
 order. -/
 @[ext]
-structure Colex (α) :=
+structure Colex (α) where
   /-- `toColex` is the "identity" function between `Finset α` and `Finset.Colex α`. -/
   toColex ::
   /-- `ofColex` is the "identity" function between `Finset.Colex α` and `Finset α`. -/
diff --git a/Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean b/Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
@@ -66,7 +66,7 @@ lemma IsHamiltonian.length_eq (hp : p.IsHamiltonian) : p.length = Fintype.card 
 end
 
 /-- A hamiltonian cycle is a cycle that visits every vertex once. -/
-structure IsHamiltonianCycle (p : G.Walk a a) extends p.IsCycle : Prop :=
+structure IsHamiltonianCycle (p : G.Walk a a) extends p.IsCycle : Prop where
   isHamiltonian_tail : p.tail.IsHamiltonian
 
 variable {p : G.Walk a a}
diff --git a/Mathlib/Data/FunLike/Basic.lean b/Mathlib/Data/FunLike/Basic.lean
@@ -17,7 +17,7 @@ There is the "D"ependent version `DFunLike` and the non-dependent version `FunLi
 
 A typical type of morphisms should be declared as:
 ```
-structure MyHom (A B : Type*) [MyClass A] [MyClass B] :=
+structure MyHom (A B : Type*) [MyClass A] [MyClass B] where
   (toFun : A → B)
   (map_op' : ∀ (x y : A), toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
 
@@ -79,7 +79,7 @@ The second step is to add instances of your new `MyHomClass` for all types exten
 Typically, you can just declare a new class analogous to `MyHomClass`:
 
 ```
-structure CoolerHom (A B : Type*) [CoolClass A] [CoolClass B] extends MyHom A B :=
+structure CoolerHom (A B : Type*) [CoolClass A] [CoolClass B] extends MyHom A B where
   (map_cool' : toFun CoolClass.cool = CoolClass.cool)
 
 class CoolerHomClass (F : Type*) (A B : outParam Type*) [CoolClass A] [CoolClass B]
diff --git a/Mathlib/Data/FunLike/Embedding.lean b/Mathlib/Data/FunLike/Embedding.lean
@@ -14,7 +14,7 @@ This typeclass is primarily for use by embeddings such as `RelEmbedding`.
 
 A typical type of embeddings should be declared as:
 ```
-structure MyEmbedding (A B : Type*) [MyClass A] [MyClass B] :=
+structure MyEmbedding (A B : Type*) [MyClass A] [MyClass B] where
   (toFun : A → B)
   (injective' : Function.Injective toFun)
   (map_op' : ∀ (x y : A), toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
@@ -58,8 +58,8 @@ Continuing the example above:
 You should extend this class when you extend `MyEmbedding`. -/
 class MyEmbeddingClass (F : Type*) (A B : outParam Type*) [MyClass A] [MyClass B]
     [FunLike F A B]
-    extends EmbeddingLike F A B :=
-  (map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y))
+    extends EmbeddingLike F A B where
+  map_op : ∀ (f : F) (x y : A), f (MyClass.op x y) = MyClass.op (f x) (f y)
 
 @[simp]
 lemma map_op {F A B : Type*} [MyClass A] [MyClass B] [FunLike F A B] [MyEmbeddingClass F A B]
@@ -84,12 +84,12 @@ The second step is to add instances of your new `MyEmbeddingClass` for all types
 Typically, you can just declare a new class analogous to `MyEmbeddingClass`:
 
 ```
-structure CoolerEmbedding (A B : Type*) [CoolClass A] [CoolClass B] extends MyEmbedding A B :=
+structure CoolerEmbedding (A B : Type*) [CoolClass A] [CoolClass B] extends MyEmbedding A B where
   (map_cool' : toFun CoolClass.cool = CoolClass.cool)
 
 class CoolerEmbeddingClass (F : Type*) (A B : outParam Type*) [CoolClass A] [CoolClass B]
     [FunLike F A B]
-    extends MyEmbeddingClass F A B :=
+    extends MyEmbeddingClass F A B where
   (map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
 
 @[simp]
diff --git a/Mathlib/Data/FunLike/Equiv.lean b/Mathlib/Data/FunLike/Equiv.lean
@@ -14,7 +14,7 @@ This typeclass is primarily for use by isomorphisms like `MonoidEquiv` and `Line
 
 A typical type of isomorphisms should be declared as:
 ```
-structure MyIso (A B : Type*) [MyClass A] [MyClass B] extends Equiv A B :=
+structure MyIso (A B : Type*) [MyClass A] [MyClass B] extends Equiv A B where
   (map_op' : ∀ (x y : A), toFun (MyClass.op x y) = MyClass.op (toFun x) (toFun y))
 
 namespace MyIso
@@ -77,12 +77,12 @@ The second step is to add instances of your new `MyIsoClass` for all types exten
 Typically, you can just declare a new class analogous to `MyIsoClass`:
 
 ```
-structure CoolerIso (A B : Type*) [CoolClass A] [CoolClass B] extends MyIso A B :=
+structure CoolerIso (A B : Type*) [CoolClass A] [CoolClass B] extends MyIso A B where
   (map_cool' : toFun CoolClass.cool = CoolClass.cool)
 
 class CoolerIsoClass (F : Type*) (A B : outParam Type*) [CoolClass A] [CoolClass B]
     [EquivLike F A B]
-    extends MyIsoClass F A B :=
+    extends MyIsoClass F A B where
   (map_cool : ∀ (f : F), f CoolClass.cool = CoolClass.cool)
 
 @[simp] lemma map_cool {F A B : Type*} [CoolClass A] [CoolClass B]
diff --git a/Mathlib/Data/Opposite.lean b/Mathlib/Data/Opposite.lean
@@ -30,7 +30,7 @@ variable (α : Sort u)
   both `unop (op X) = X` and `op (unop X) = X` are definitional equalities.
 
 -/
-structure Opposite :=
+structure Opposite where
   /-- The canonical map `α → αᵒᵖ`. -/
   op ::
   /-- The canonical map `αᵒᵖ → α`. -/
diff --git a/Mathlib/Data/SetLike/Basic.lean b/Mathlib/Data/SetLike/Basic.lean
@@ -28,7 +28,7 @@ boilerplate for every `SetLike`: a `coe_sort`, a `coe` to set, a
 
 A typical subobject should be declared as:
 ```
-structure MySubobject (X : Type*) [ObjectTypeclass X] :=
+structure MySubobject (X : Type*) [ObjectTypeclass X] where
   (carrier : Set X)
   (op_mem' : ∀ {x : X}, x ∈ carrier → sorry ∈ carrier)
 
@@ -60,7 +60,7 @@ end MySubobject
 
 An alternative to `SetLike` could have been an extensional `Membership` typeclass:
 ```
-class ExtMembership (α : out_param <| Type u) (β : Type v) extends Membership α β :=
+class ExtMembership (α : out_param <| Type u) (β : Type v) extends Membership α β where
   (ext_iff : ∀ {s t : β}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ t)
 ```
 While this is equivalent, `SetLike` conveniently uses a carrier set projection directly.
diff --git a/Mathlib/GroupTheory/HNNExtension.lean b/Mathlib/GroupTheory/HNNExtension.lean
@@ -174,7 +174,7 @@ namespace NormalWord
 variable (G A B)
 /-- To put word in the HNN Extension into a normal form, we must choose an element of each right
 coset of both `A` and `B`, such that the chosen element of the subgroup itself is `1`. -/
-structure TransversalPair : Type _ :=
+structure TransversalPair : Type _ where
   /-- The transversal of each subgroup -/
   set : ℤˣ → Set G
   /-- We have exactly one element of each coset of the subgroup -/
@@ -187,7 +187,7 @@ instance TransversalPair.nonempty : Nonempty (TransversalPair G A B) := by
 /-- A reduced word is a `head`, which is an element of `G`, followed by the product list of pairs.
 There should also be no sequences of the form `t^u * g * t^-u`, where `g` is in
 `toSubgroup A B u` This is a less strict condition than required for `NormalWord`. -/
-structure ReducedWord : Type _ :=
+structure ReducedWord : Type _ where
   /-- Every `ReducedWord` is the product of an element of the group and a word made up
   of letters each of which is in the transversal. `head` is that element of the base group. -/
   head : G
@@ -215,7 +215,7 @@ The normal form is a `head`, which is an element of `G`, followed by the product
 `toSubgroup A B u`. There should also be no sequences of the form `t^u * g * t^-u`
 where `g ∈ toSubgroup A B u` -/
 structure _root_.HNNExtension.NormalWord (d : TransversalPair G A B)
-    extends ReducedWord G A B : Type _ :=
+    extends ReducedWord G A B : Type _ where
   /-- Every element `g : G` in the list is the chosen element of its coset -/
   mem_set : ∀ (u : ℤˣ) (g : G), (u, g) ∈ toList → g ∈ d.set u
 
diff --git a/Mathlib/LinearAlgebra/PerfectPairing.lean b/Mathlib/LinearAlgebra/PerfectPairing.lean
@@ -34,7 +34,7 @@ open Function Module
 variable (R M N : Type*) [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N]
 
 /-- A perfect pairing of two (left) modules over a commutative ring. -/
-structure PerfectPairing :=
+structure PerfectPairing where
   toLin : M →ₗ[R] N →ₗ[R] R
   bijectiveLeft : Bijective toLin
   bijectiveRight : Bijective toLin.flip
diff --git a/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean b/Mathlib/LinearAlgebra/QuadraticForm/QuadraticModuleCat.lean
@@ -43,7 +43,7 @@ def of {X : Type v} [AddCommGroup X] [Module R X] (Q : QuadraticForm R X) :
 /-- A type alias for `QuadraticForm.LinearIsometry` to avoid confusion between the categorical and
 algebraic spellings of composition. -/
 @[ext]
-structure Hom (V W : QuadraticModuleCat.{v} R) :=
+structure Hom (V W : QuadraticModuleCat.{v} R) where
   /-- The underlying isometry -/
   toIsometry : V.form →qᵢ W.form
 
diff --git a/Mathlib/LinearAlgebra/RootSystem/Defs.lean b/Mathlib/LinearAlgebra/RootSystem/Defs.lean
@@ -86,7 +86,7 @@ evaluates to `2`, and the permutation attached to each element of `ι` is compat
 reflections on the corresponding roots and coroots.
 
 It exists to allow for a convenient unification of the theories of root systems and root data. -/
-structure RootPairing extends PerfectPairing R M N :=
+structure RootPairing extends PerfectPairing R M N where
   /-- A parametrized family of vectors, called roots. -/
   root : ι ↪ M
   /-- A parametrized family of dual vectors, called coroots. -/
@@ -110,7 +110,7 @@ abbrev RootDatum (X₁ X₂ : Type*) [AddCommGroup X₁] [AddCommGroup X₂] :=
 
 Note that this is slightly more general than the usual definition in the sense that `N` is not
 required to be the dual of `M`. -/
-structure RootSystem extends RootPairing ι R M N :=
+structure RootSystem extends RootPairing ι R M N where
   span_eq_top : span R (range root) = ⊤
 
 attribute [simp] RootSystem.span_eq_top
diff --git a/Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean b/Mathlib/LinearAlgebra/RootSystem/OfBilinear.lean
@@ -33,7 +33,7 @@ namespace LinearMap
 injective, and for any vector `y`, the norm of `x` divides twice the inner product of `x` and `y`.
 These conditions are what we need when describing reflection as a map taking `y` to
 `y - 2 • (B x y) / (B x x) • x`. -/
-structure IsReflective (B : M →ₗ[R] M →ₗ[R] R) (x : M) : Prop :=
+structure IsReflective (B : M →ₗ[R] M →ₗ[R] R) (x : M) : Prop where
   regular : IsRegular (B x x)
   dvd_two_mul : ∀ y, B x x ∣ 2 * B x y
 
diff --git a/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean b/Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
diff --git a/Mathlib/MeasureTheory/Measure/SeparableMeasure.lean b/Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
diff --git a/Mathlib/Order/Defs.lean b/Mathlib/Order/Defs.lean
diff --git a/Mathlib/Order/SuccPred/Basic.lean b/Mathlib/Order/SuccPred/Basic.lean
diff --git a/Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean b/Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
diff --git a/Mathlib/RingTheory/DedekindDomain/Basic.lean b/Mathlib/RingTheory/DedekindDomain/Basic.lean
diff --git a/Mathlib/Tactic/Ring/Basic.lean b/Mathlib/Tactic/Ring/Basic.lean
diff --git a/Mathlib/Topology/Perfect.lean b/Mathlib/Topology/Perfect.lean
diff --git a/Mathlib/Util/AtomM.lean b/Mathlib/Util/AtomM.lean
diff --git a/test/MfldSetTac.lean b/test/MfldSetTac.lean
diff --git a/test/NthRewrite.lean b/test/NthRewrite.lean
diff --git a/test/Simps.lean b/test/Simps.lean
diff --git a/test/toAdditive.lean b/test/toAdditive.lean
