chore: adaptations for nightly-2025-02-24 (#22266)

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kyle Miller <[email protected]>

Archive/Imo/Imo2024Q5.lean

@@ -263,9 +263,9 @@ lemma Path.one_lt_length_cells (p : Path N): 1 < p.cells.length := by
   by_contra hl
   have h : p.cells.length = 0 ∨ p.cells.length = 1 := by omega
   rcases h with h | h
-  · rw [List.length_eq_zero] at h
+  · rw [List.length_eq_zero_iff] at h
     exact p.nonempty h
-  · rw [List.length_eq_one] at h
+  · rw [List.length_eq_one_iff] at h
     rcases h with ⟨c, hc⟩
     have h1 := p.head_first_row
     simp_rw [hc, List.head_cons] at h1

Archive/Wiedijk100Theorems/BallotProblem.lean

@@ -96,7 +96,7 @@ theorem length_of_mem_countedSequence {p q} {l : List ℤ} (hl : l ∈ countedSe
 
 theorem counted_eq_nil_iff {p q : ℕ} {l : List ℤ} (hl : l ∈ countedSequence p q) :
     l = [] ↔ p = 0 ∧ q = 0 :=
-  List.length_eq_zero.symm.trans <| by simp [length_of_mem_countedSequence hl]
+  List.length_eq_zero_iff.symm.trans <| by simp [length_of_mem_countedSequence hl]
 
 theorem counted_ne_nil_left {p q : ℕ} (hp : p ≠ 0) {l : List ℤ} (hl : l ∈ countedSequence p q) :
     l ≠ [] := by simp [counted_eq_nil_iff hl, hp]

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -18,8 +18,8 @@ More lemmas about `adjoin` can be found in `RingTheory.Adjoin`.
 universe u u' v w w'
 
 /-- A subalgebra is a sub(semi)ring that includes the range of `algebraMap`. -/
-structure Subalgebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] extends
-  Subsemiring A : Type v where
+structure Subalgebra (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] [Algebra R A] : Type v
+    extends Subsemiring A where
   /-- The image of `algebraMap` is contained in the underlying set of the subalgebra -/
   algebraMap_mem' : ∀ r, algebraMap R A r ∈ carrier
   zero_mem' := (algebraMap R A).map_zero ▸ algebraMap_mem' 0

Mathlib/Algebra/Field/Subfield/Defs.lean

@@ -49,8 +49,8 @@ variable {K : Type u} {L : Type v} {M : Type w}
 variable [DivisionRing K] [DivisionRing L] [DivisionRing M]
 
 /-- `SubfieldClass S K` states `S` is a type of subsets `s ⊆ K` closed under field operations. -/
-class SubfieldClass (S K : Type*) [DivisionRing K] [SetLike S K] extends SubringClass S K,
-  InvMemClass S K : Prop
+class SubfieldClass (S K : Type*) [DivisionRing K] [SetLike S K] : Prop
+    extends SubringClass S K, InvMemClass S K
 
 namespace SubfieldClass
 

Mathlib/Algebra/FreeMonoid/Basic.lean

@@ -128,14 +128,14 @@ def length (a : FreeMonoid α) : ℕ := a.toList.length
 theorem length_one : length (1 : FreeMonoid α) = 0 := rfl
 
 @[to_additive (attr := simp)]
-theorem length_eq_zero : length a = 0 ↔ a = 1 := List.length_eq_zero
+theorem length_eq_zero : length a = 0 ↔ a = 1 := List.length_eq_zero_iff
 
 @[to_additive (attr := simp)]
 theorem length_of (m : α) : length (of m) = 1 := rfl
 
 @[to_additive existing]
 theorem length_eq_one : length a = 1 ↔ ∃ m, a = FreeMonoid.of m :=
-  List.length_eq_one
+  List.length_eq_one_iff
 
 @[to_additive]
 theorem length_eq_two {v : FreeMonoid α} :

Mathlib/Algebra/GradedMonoid.lean

@@ -523,8 +523,8 @@ theorem SetLike.coe_gMul {S : Type*} [SetLike S R] [Mul R] [Add ι] (A : ι →
   rfl
 
 /-- A version of `GradedMonoid.GMonoid` for internally graded objects. -/
-class SetLike.GradedMonoid {S : Type*} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S) extends
-  SetLike.GradedOne A, SetLike.GradedMul A : Prop
+class SetLike.GradedMonoid {S : Type*} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S) : Prop
+    extends SetLike.GradedOne A, SetLike.GradedMul A
 
 namespace SetLike
 

Mathlib/Algebra/Group/Submonoid/Defs.lean

@@ -86,8 +86,8 @@ add_decl_doc Submonoid.toSubsemigroup
 
 /-- `SubmonoidClass S M` says `S` is a type of subsets `s ≤ M` that contain `1`
 and are closed under `(*)` -/
-class SubmonoidClass (S : Type*) (M : outParam Type*) [MulOneClass M] [SetLike S M] extends
-  MulMemClass S M, OneMemClass S M : Prop
+class SubmonoidClass (S : Type*) (M : outParam Type*) [MulOneClass M] [SetLike S M] : Prop
+    extends MulMemClass S M, OneMemClass S M
 
 section
 
@@ -105,8 +105,8 @@ add_decl_doc AddSubmonoid.toAddSubsemigroup
 
 /-- `AddSubmonoidClass S M` says `S` is a type of subsets `s ≤ M` that contain `0`
 and are closed under `(+)` -/
-class AddSubmonoidClass (S : Type*) (M : outParam Type*) [AddZeroClass M] [SetLike S M] extends
-  AddMemClass S M, ZeroMemClass S M : Prop
+class AddSubmonoidClass (S : Type*) (M : outParam Type*) [AddZeroClass M] [SetLike S M] : Prop
+  extends AddMemClass S M, ZeroMemClass S M
 
 attribute [to_additive] Submonoid SubmonoidClass
 

Mathlib/Algebra/Module/Submodule/Defs.lean

@@ -34,8 +34,8 @@ variable {G : Type u''} {S : Type u'} {R : Type u} {M : Type v} {ι : Type w}
 /-- A submodule of a module is one which is closed under vector operations.
   This is a sufficient condition for the subset of vectors in the submodule
   to themselves form a module. -/
-structure Submodule (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] extends
-  AddSubmonoid M, SubMulAction R M : Type v
+structure Submodule (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type v
+    extends AddSubmonoid M, SubMulAction R M
 
 /-- Reinterpret a `Submodule` as an `AddSubmonoid`. -/
 add_decl_doc Submodule.toAddSubmonoid

Mathlib/Algebra/Order/AddTorsor.lean

@@ -97,16 +97,16 @@ class IsCancelSMul (G P : Type*) [SMul G P] : Prop where
   protected right_cancel : ∀ (a b : G) (c : P), a • c = b • c → a = b
 
 /-- An ordered cancellative vector addition is an ordered vector addition that is cancellative. -/
-class IsOrderedCancelVAdd (G P : Type*) [LE G] [LE P] [VAdd G P] extends
-    IsOrderedVAdd G P : Prop where
+class IsOrderedCancelVAdd (G P : Type*) [LE G] [LE P] [VAdd G P] : Prop
+    extends IsOrderedVAdd G P where
   protected le_of_vadd_le_vadd_left : ∀ (a : G) (b c : P), a +ᵥ b ≤ a +ᵥ c → b ≤ c
   protected le_of_vadd_le_vadd_right : ∀ (a b : G) (c : P), a +ᵥ c ≤ b +ᵥ c → a ≤ b
 
 /-- An ordered cancellative scalar multiplication is an ordered scalar multiplication that is
   cancellative. -/
 @[to_additive]
-class IsOrderedCancelSMul (G P : Type*) [LE G] [LE P] [SMul G P] extends
-    IsOrderedSMul G P : Prop where
+class IsOrderedCancelSMul (G P : Type*) [LE G] [LE P] [SMul G P] : Prop
+    extends IsOrderedSMul G P where
   protected le_of_smul_le_smul_left : ∀ (a : G) (b c : P), a • b ≤ a • c → b ≤ c
   protected le_of_smul_le_smul_right : ∀ (a b : G) (c : P), a • c ≤ b • c → a ≤ b
 

Mathlib/Algebra/Order/Group/Cone.lean

@@ -24,8 +24,8 @@ class AddGroupConeClass (S : Type*) (G : outParam Type*) [AddCommGroup G] [SetLi
 
 /-- `GroupConeClass S G` says that `S` is a type of cones in `G`. -/
 @[to_additive]
-class GroupConeClass (S : Type*) (G : outParam Type*) [CommGroup G] [SetLike S G] extends
-    SubmonoidClass S G : Prop where
+class GroupConeClass (S : Type*) (G : outParam Type*) [CommGroup G] [SetLike S G] : Prop
+    extends SubmonoidClass S G where
   eq_one_of_mem_of_inv_mem {C : S} {a : G} : a ∈ C → a⁻¹ ∈ C → a = 1
 
 export GroupConeClass (eq_one_of_mem_of_inv_mem)

Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

@@ -105,56 +105,56 @@ namely `b₁ ≤ b₂ → a * b₁ ≤ a * b₂` if `0 ≤ a`.
 
 You should usually not use this very granular typeclass directly, but rather a typeclass like
 `OrderedSemiring`. -/
-@[mk_iff] class PosMulMono extends CovariantClass α≥0 α (fun x y => x * y) (· ≤ ·) : Prop
+@[mk_iff] class PosMulMono : Prop extends CovariantClass α≥0 α (fun x y => x * y) (· ≤ ·)
 
 /-- Typeclass for monotonicity of multiplication by nonnegative elements on the right,
 namely `a₁ ≤ a₂ → a₁ * b ≤ a₂ * b` if `0 ≤ b`.
 
 You should usually not use this very granular typeclass directly, but rather a typeclass like
 `OrderedSemiring`. -/
-@[mk_iff] class MulPosMono extends CovariantClass α≥0 α (fun x y => y * x) (· ≤ ·) : Prop
+@[mk_iff] class MulPosMono : Prop extends CovariantClass α≥0 α (fun x y => y * x) (· ≤ ·)
 
 /-- Typeclass for strict monotonicity of multiplication by positive elements on the left,
 namely `b₁ < b₂ → a * b₁ < a * b₂` if `0 < a`.
 
 You should usually not use this very granular typeclass directly, but rather a typeclass like
 `StrictOrderedSemiring`. -/
-@[mk_iff] class PosMulStrictMono extends CovariantClass α>0 α (fun x y => x * y) (· < ·) : Prop
+@[mk_iff] class PosMulStrictMono : Prop extends CovariantClass α>0 α (fun x y => x * y) (· < ·)
 
 /-- Typeclass for strict monotonicity of multiplication by positive elements on the right,
 namely `a₁ < a₂ → a₁ * b < a₂ * b` if `0 < b`.
 
 You should usually not use this very granular typeclass directly, but rather a typeclass like
 `StrictOrderedSemiring`. -/
-@[mk_iff] class MulPosStrictMono extends CovariantClass α>0 α (fun x y => y * x) (· < ·) : Prop
+@[mk_iff] class MulPosStrictMono : Prop extends CovariantClass α>0 α (fun x y => y * x) (· < ·)
 
 /-- Typeclass for strict reverse monotonicity of multiplication by nonnegative elements on
 the left, namely `a * b₁ < a * b₂ → b₁ < b₂` if `0 ≤ a`.
 
 You should usually not use this very granular typeclass directly, but rather a typeclass like
 `LinearOrderedSemiring`. -/
-@[mk_iff] class PosMulReflectLT extends ContravariantClass α≥0 α (fun x y => x * y) (· < ·) : Prop
+@[mk_iff] class PosMulReflectLT : Prop extends ContravariantClass α≥0 α (fun x y => x * y) (· < ·)
 
 /-- Typeclass for strict reverse monotonicity of multiplication by nonnegative elements on
 the right, namely `a₁ * b < a₂ * b → a₁ < a₂` if `0 ≤ b`.
 
 You should usually not use this very granular typeclass directly, but rather a typeclass like
 `LinearOrderedSemiring`. -/
-@[mk_iff] class MulPosReflectLT extends ContravariantClass α≥0 α (fun x y => y * x) (· < ·) : Prop
+@[mk_iff] class MulPosReflectLT : Prop extends ContravariantClass α≥0 α (fun x y => y * x) (· < ·)
 
 /-- Typeclass for reverse monotonicity of multiplication by positive elements on the left,
 namely `a * b₁ ≤ a * b₂ → b₁ ≤ b₂` if `0 < a`.
 
 You should usually not use this very granular typeclass directly, but rather a typeclass like
 `LinearOrderedSemiring`. -/
-@[mk_iff] class PosMulReflectLE extends ContravariantClass α>0 α (fun x y => x * y) (· ≤ ·) : Prop
+@[mk_iff] class PosMulReflectLE : Prop extends ContravariantClass α>0 α (fun x y => x * y) (· ≤ ·)
 
 /-- Typeclass for reverse monotonicity of multiplication by positive elements on the right,
 namely `a₁ * b ≤ a₂ * b → a₁ ≤ a₂` if `0 < b`.
 
 You should usually not use this very granular typeclass directly, but rather a typeclass like
 `LinearOrderedSemiring`. -/
-@[mk_iff] class MulPosReflectLE extends ContravariantClass α>0 α (fun x y => y * x) (· ≤ ·) : Prop
+@[mk_iff] class MulPosReflectLE : Prop extends ContravariantClass α>0 α (fun x y => y * x) (· ≤ ·)
 
 end Abbreviations
 

Mathlib/Algebra/Order/Monoid/Canonical/Defs.lean

@@ -22,8 +22,8 @@ variable {α : Type u}
   which is to say, `a ≤ b` iff there exists `c` with `b = a + c`.
   This is satisfied by the natural numbers, for example, but not
   the integers or other nontrivial `OrderedAddCommGroup`s. -/
-class CanonicallyOrderedAdd (α : Type*) [Add α] [LE α] extends
-  ExistsAddOfLE α : Prop where
+class CanonicallyOrderedAdd (α : Type*) [Add α] [LE α] : Prop
+    extends ExistsAddOfLE α where
   /-- For any `a` and `b`, `a ≤ a + b` -/
   protected le_self_add : ∀ a b : α, a ≤ a + b
 
@@ -38,8 +38,8 @@ attribute [instance 50] CanonicallyOrderedAdd.toExistsAddOfLE
   Dedekind domain satisfy this; collections of all things ≤ 1 seem to
   be more natural that collections of all things ≥ 1). -/
 @[to_additive]
-class CanonicallyOrderedMul (α : Type*) [Mul α] [LE α] extends
-  ExistsMulOfLE α : Prop where
+class CanonicallyOrderedMul (α : Type*) [Mul α] [LE α] : Prop
+    extends ExistsMulOfLE α where
   /-- For any `a` and `b`, `a ≤ a * b` -/
   protected le_self_mul : ∀ a b : α, a ≤ a * b
 

Mathlib/Algebra/Ring/Subring/Defs.lean

@@ -71,8 +71,8 @@ section SubringClass
 
 /-- `SubringClass S R` states that `S` is a type of subsets `s ⊆ R` that
 are both a multiplicative submonoid and an additive subgroup. -/
-class SubringClass (S : Type*) (R : outParam (Type u)) [Ring R] [SetLike S R] extends
-  SubsemiringClass S R, NegMemClass S R : Prop
+class SubringClass (S : Type*) (R : outParam (Type u)) [Ring R] [SetLike S R] : Prop
+    extends SubsemiringClass S R, NegMemClass S R
 
 -- See note [lower instance priority]
 instance (priority := 100) SubringClass.addSubgroupClass (S : Type*) (R : Type u)

Mathlib/Analysis/Analytic/CPolynomialDef.lean

@@ -56,7 +56,7 @@ section FiniteFPowerSeries
 `f` has `p` as a finite power series on the ball of radius `r > 0` around `x` if
 `f (x + y) = ∑' pₘ yᵐ` for all `‖y‖ < r` and `pₙ = 0` for `n ≤ m`. -/
 structure HasFiniteFPowerSeriesOnBall (f : E → F) (p : FormalMultilinearSeries 𝕜 E F) (x : E)
-    (n : ℕ) (r : ℝ≥0∞) extends HasFPowerSeriesOnBall f p x r : Prop where
+    (n : ℕ) (r : ℝ≥0∞) : Prop extends HasFPowerSeriesOnBall f p x r where
   finite : ∀ (m : ℕ), n ≤ m → p m = 0
 
 theorem HasFiniteFPowerSeriesOnBall.mk' {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E}

Mathlib/Analysis/Normed/Algebra/Norm.lean

@@ -41,8 +41,8 @@ instance (K : Type*) [NormedField K] : Inhabited (AlgebraNorm K K) :=
 /-- `AlgebraNormClass F R S` states that `F` is a type of `R`-algebra norms on the ring `S`.
 You should extend this class when you extend `AlgebraNorm`. -/
 class AlgebraNormClass (F : Type*) (R : outParam <| Type*) [SeminormedCommRing R]
-    (S : outParam <| Type*) [Ring S] [Algebra R S] [FunLike F S ℝ] extends RingNormClass F S ℝ,
-    SeminormClass F R S : Prop
+    (S : outParam <| Type*) [Ring S] [Algebra R S] [FunLike F S ℝ] : Prop
+    extends RingNormClass F S ℝ, SeminormClass F R S
 
 namespace AlgebraNorm
 
@@ -133,8 +133,8 @@ instance (K : Type*) [NormedField K] : Inhabited (MulAlgebraNorm K K) :=
 /-- `MulAlgebraNormClass F R S` states that `F` is a type of multiplicative `R`-algebra norms on
 the ring `S`. You should extend this class when you extend `MulAlgebraNorm`. -/
 class MulAlgebraNormClass (F : Type*) (R : outParam <| Type*) [SeminormedCommRing R]
-    (S : outParam <| Type*) [Ring S] [Algebra R S] [FunLike F S ℝ] extends MulRingNormClass F S ℝ,
-    SeminormClass F R S : Prop
+    (S : outParam <| Type*) [Ring S] [Algebra R S] [FunLike F S ℝ] : Prop
+    extends MulRingNormClass F S ℝ, SeminormClass F R S
 
 namespace MulAlgebraNorm
 

Mathlib/Analysis/Normed/Operator/BoundedLinearMaps.lean

@@ -66,8 +66,8 @@ variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] {E : Type*} [SeminormedAd
 /-- A function `f` satisfies `IsBoundedLinearMap 𝕜 f` if it is linear and satisfies the
 inequality `‖f x‖ ≤ M * ‖x‖` for some positive constant `M`. -/
 structure IsBoundedLinearMap (𝕜 : Type*) [NormedField 𝕜] {E : Type*} [SeminormedAddCommGroup E]
-  [NormedSpace 𝕜 E] {F : Type*} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) extends
-  IsLinearMap 𝕜 f : Prop where
+    [NormedSpace 𝕜 E] {F : Type*} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) : Prop
+    extends IsLinearMap 𝕜 f where
   bound : ∃ M, 0 < M ∧ ∀ x : E, ‖f x‖ ≤ M * ‖x‖
 
 lemma isBoundedLinearMap_iff {f : E → F} :

Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

@@ -66,9 +66,9 @@ A map `f` between an `R`-module and an `S`-module over a ring homomorphism `σ :
 is semilinear if it satisfies the two properties `f (x + y) = f x + f y` and
 `f (c • x) = (σ c) • f x`. -/
 class SemilinearIsometryClass (𝓕 : Type*) {R R₂ : outParam Type*} [Semiring R] [Semiring R₂]
-  (σ₁₂ : outParam <| R →+* R₂) (E E₂ : outParam Type*) [SeminormedAddCommGroup E]
-  [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] extends
-  SemilinearMapClass 𝓕 σ₁₂ E E₂ : Prop where
+    (σ₁₂ : outParam <| R →+* R₂) (E E₂ : outParam Type*) [SeminormedAddCommGroup E]
+    [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] : Prop
+    extends SemilinearMapClass 𝓕 σ₁₂ E E₂ where
   norm_map : ∀ (f : 𝓕) (x : E), ‖f x‖ = ‖x‖
 
 /-- `LinearIsometryClass F R E E₂` asserts `F` is a type of bundled `R`-linear isometries

Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

@@ -126,8 +126,8 @@ end CommSq
 ```
 is a pullback square. (Also known as a fibered product or cartesian square.)
 -/
-structure IsPullback {P X Y Z : C} (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z) (g : Y ⟶ Z) extends
-  CommSq fst snd f g : Prop where
+structure IsPullback {P X Y Z : C} (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z) (g : Y ⟶ Z) : Prop
+    extends CommSq fst snd f g where
   /-- the pullback cone is a limit -/
   isLimit' : Nonempty (IsLimit (PullbackCone.mk _ _ w))
 
@@ -143,8 +143,8 @@ structure IsPullback {P X Y Z : C} (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z)
 ```
 is a pushout square. (Also known as a fiber coproduct or cocartesian square.)
 -/
-structure IsPushout {Z X Y P : C} (f : Z ⟶ X) (g : Z ⟶ Y) (inl : X ⟶ P) (inr : Y ⟶ P) extends
-  CommSq f g inl inr : Prop where
+structure IsPushout {Z X Y P : C} (f : Z ⟶ X) (g : Z ⟶ Y) (inl : X ⟶ P) (inr : Y ⟶ P) : Prop
+    extends CommSq f g inl inr where
   /-- the pushout cocone is a colimit -/
   isColimit' : Nonempty (IsColimit (PushoutCocone.mk _ _ w))
 
@@ -162,8 +162,8 @@ section
 ```
 that is both a pullback square and a pushout square.
 -/
-structure BicartesianSq {W X Y Z : C} (f : W ⟶ X) (g : W ⟶ Y) (h : X ⟶ Z) (i : Y ⟶ Z) extends
-  IsPullback f g h i, IsPushout f g h i : Prop
+structure BicartesianSq {W X Y Z : C} (f : W ⟶ X) (g : W ⟶ Y) (h : X ⟶ Z) (i : Y ⟶ Z) : Prop
+    extends IsPullback f g h i, IsPushout f g h i
 
 -- Lean should make these parent projections as `lemma`, not `def`.
 attribute [nolint defLemma docBlame] BicartesianSq.toIsPushout

Mathlib/CategoryTheory/Monoidal/Bimon_.lean

@@ -69,8 +69,8 @@ theorem one_counit (M : C) [Bimon_Class M] : η[M] ≫ ε[M] = 𝟙 (𝟙_ C) :=
 end Bimon_Class
 
 /-- The property that a morphism between bimonoid objects is a bimonoid morphism. -/
-class IsBimon_Hom {M N : C} [Bimon_Class M] [Bimon_Class N] (f : M ⟶ N) extends
-    IsMon_Hom f, IsComon_Hom f : Prop
+class IsBimon_Hom {M N : C} [Bimon_Class M] [Bimon_Class N] (f : M ⟶ N) : Prop extends
+    IsMon_Hom f, IsComon_Hom f
 
 variable (C)
 

Mathlib/CategoryTheory/MorphismProperty/Composition.lean

@@ -307,9 +307,8 @@ class HasOfPrecompProperty (W W' : MorphismProperty C) : Prop where
 
 /-- A class of morphisms `W` has the two-out-of-three property if whenever two out
 of three maps in `f`, `g`, `f ≫ g` are in `W`, then the third map is also in `W`. -/
-class HasTwoOutOfThreeProperty (W : MorphismProperty C)
-    extends W.IsStableUnderComposition, W.HasOfPostcompProperty W,
-      W.HasOfPrecompProperty W : Prop where
+class HasTwoOutOfThreeProperty (W : MorphismProperty C) : Prop
+    extends W.IsStableUnderComposition, W.HasOfPostcompProperty W, W.HasOfPrecompProperty W where
 
 section
 

Mathlib/Combinatorics/Enumerative/Composition.lean

@@ -655,7 +655,7 @@ theorem getElem_splitWrtComposition (l : List α) (c : Composition n)
 theorem flatten_splitWrtCompositionAux {ns : List ℕ} :
     ∀ {l : List α}, ns.sum = l.length → (l.splitWrtCompositionAux ns).flatten = l := by
   induction ns with
-  | nil => exact fun h ↦ (length_eq_zero.1 h.symm).symm
+  | nil => exact fun h ↦ (length_eq_zero_iff.1 h.symm).symm
   | cons n ns IH =>
     intro l h; rw [sum_cons] at h
     simp only [splitWrtCompositionAux_cons]; dsimp

Mathlib/Combinatorics/Enumerative/DyckWord.lean

@@ -204,7 +204,7 @@ def denest (hn : p.IsNested) : DyckWord where
       · tauto
     rw [← drop_one, take_drop, dropLast_eq_take, take_take]
     have ub : min (1 + i) (p.toList.length - 1) < p.toList.length :=
-      (min_le_right _ p.toList.length.pred).trans_lt (Nat.pred_lt ((length_pos.mpr h).ne'))
+      (min_le_right _ p.toList.length.pred).trans_lt (Nat.pred_lt ((length_pos_iff.mpr h).ne'))
     have lb : 0 < min (1 + i) (p.toList.length - 1) := by omega
     have eq := hn.2 lb ub
     set j := min (1 + i) (p.toList.length - 1)
@@ -263,7 +263,7 @@ lemma firstReturn_pos : 0 < p.firstReturn := by
   What's going on?
   -/
   swap
-  · rw [length_range, length_pos]
+  · rw [length_range, length_pos_iff]
     exact toList_ne_nil.mpr h
   · rw [getElem_range] at f
     simp at f