Trigger CI for leanprover/lean4#7185

Batteries/Classes/Order.lean

@@ -37,7 +37,7 @@ theorem cmp_refl [OrientedCmp cmp] : cmp x x = .eq :=
 end OrientedCmp
 
 /-- `TransCmp cmp` asserts that `cmp` induces a transitive relation. -/
-class TransCmp (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where
+class TransCmp (cmp : α → α → Ordering) : Prop extends OrientedCmp cmp where
   /-- The comparator operation is transitive. -/
   le_trans : cmp x y ≠ .gt → cmp y z ≠ .gt → cmp x z ≠ .gt
 
@@ -99,15 +99,15 @@ theorem BEqCmp.cmp_iff_eq [BEq α] [LawfulBEq α] [BEqCmp (α := α) cmp] : cmp
   simp [BEqCmp.cmp_iff_beq]
 
 /-- `LTCmp cmp` asserts that `cmp x y = .lt` and `x < y` coincide. -/
-class LTCmp [LT α] (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where
+class LTCmp [LT α] (cmp : α → α → Ordering) : Prop extends OrientedCmp cmp where
   /-- `cmp x y = .lt` holds iff `x < y` is true. -/
   cmp_iff_lt : cmp x y = .lt ↔ x < y
 
 theorem LTCmp.cmp_iff_gt [LT α] [LTCmp (α := α) cmp] : cmp x y = .gt ↔ y < x := by
   rw [OrientedCmp.cmp_eq_gt, LTCmp.cmp_iff_lt]
 
 /-- `LECmp cmp` asserts that `cmp x y ≠ .gt` and `x ≤ y` coincide. -/
-class LECmp [LE α] (cmp : α → α → Ordering) extends OrientedCmp cmp : Prop where
+class LECmp [LE α] (cmp : α → α → Ordering) : Prop extends OrientedCmp cmp where
   /-- `cmp x y ≠ .gt` holds iff `x ≤ y` is true. -/
   cmp_iff_le : cmp x y ≠ .gt ↔ x ≤ y
 
@@ -116,8 +116,8 @@ theorem LECmp.cmp_iff_ge [LE α] [LECmp (α := α) cmp] : cmp x y ≠ .lt ↔ y
 
 /-- `LawfulCmp cmp` asserts that the `LE`, `LT`, `BEq` instances are all coherent with each other
 and with `cmp`, describing a strict weak order (a linear order except for antisymmetry). -/
-class LawfulCmp [LE α] [LT α] [BEq α] (cmp : α → α → Ordering) extends
-  TransCmp cmp, BEqCmp cmp, LTCmp cmp, LECmp cmp : Prop
+class LawfulCmp [LE α] [LT α] [BEq α] (cmp : α → α → Ordering) : Prop extends
+  TransCmp cmp, BEqCmp cmp, LTCmp cmp, LECmp cmp
 
 /-- `OrientedOrd α` asserts that the `Ord` instance satisfies `OrientedCmp`. -/
 abbrev OrientedOrd (α) [Ord α] := OrientedCmp (α := α) compare

Batteries/Data/List/Perm.lean

@@ -70,7 +70,7 @@ theorem Subperm.filter (p : α → Bool) ⦃l l' : List α⦄ (h : l <+~ l') :
   exact ⟨_, hp.filter p, h.filter p⟩
 
 @[simp] theorem subperm_nil : l <+~ [] ↔ l = [] :=
-  ⟨fun h => length_eq_zero.1 $ Nat.le_zero.1 h.length_le, by rintro rfl; rfl⟩
+  ⟨fun h => length_eq_zero_iff.1 $ Nat.le_zero.1 h.length_le, by rintro rfl; rfl⟩
 
 @[simp] theorem singleton_subperm_iff {α} {l : List α} {a : α} : [a] <+~ l ↔ a ∈ l := by
   refine ⟨fun ⟨s, hla, h⟩ => ?_, fun h => ⟨[a], .rfl, singleton_sublist.mpr h⟩⟩

Batteries/Data/RBMap/Lemmas.lean

@@ -111,7 +111,7 @@ instance (cmp cut) [@IsCut α cmp cut] : IsCut (flip cmp) (cut · |>.swap) where
 `IsStrictCut` upgrades the `IsCut` property to ensure that at most one element of the tree
 can match the cut, and hence `find?` will return the unique such element if one exists.
 -/
-class IsStrictCut (cmp : α → α → Ordering) (cut : α → Ordering) extends IsCut cmp cut : Prop where
+class IsStrictCut (cmp : α → α → Ordering) (cut : α → Ordering) : Prop extends IsCut cmp cut where
   /-- If `cut = x`, then `cut` and `x` have compare the same with respect to other elements. -/
   exact [TransCmp cmp] : cut x = .eq → cmp x y = cut y
 

Batteries/Data/UInt.lean

@@ -10,8 +10,6 @@ import Batteries.Classes.Order
 @[ext] theorem UInt8.ext : {x y : UInt8} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-theorem UInt8.toNat_lt (x : UInt8) : x.toNat < 2 ^ 8 := x.toFin.isLt
-
 @[simp] theorem UInt8.toUInt16_toNat (x : UInt8) : x.toUInt16.toNat = x.toNat := rfl
 
 @[simp] theorem UInt8.toUInt32_toNat (x : UInt8) : x.toUInt32.toNat = x.toNat := rfl
@@ -26,8 +24,6 @@ instance : Batteries.LawfulOrd UInt8 := .compareOfLessAndEq
 @[ext] theorem UInt16.ext : {x y : UInt16} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-theorem UInt16.toNat_lt (x : UInt16) : x.toNat < 2 ^ 16 := x.toFin.isLt
-
 @[simp] theorem UInt16.toUInt8_toNat (x : UInt16) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
 
 @[simp] theorem UInt16.toUInt32_toNat (x : UInt16) : x.toUInt32.toNat = x.toNat := rfl
@@ -42,8 +38,6 @@ instance : Batteries.LawfulOrd UInt16 := .compareOfLessAndEq
 @[ext] theorem UInt32.ext : {x y : UInt32} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-theorem UInt32.toNat_lt (x : UInt32) : x.toNat < 2 ^ 32 := x.toFin.isLt
-
 @[simp] theorem UInt32.toUInt8_toNat (x : UInt32) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
 
 @[simp] theorem UInt32.toUInt16_toNat (x : UInt32) : x.toUInt16.toNat = x.toNat % 2 ^ 16 := rfl
@@ -58,8 +52,6 @@ instance : Batteries.LawfulOrd UInt32 := .compareOfLessAndEq
 @[ext] theorem UInt64.ext : {x y : UInt64} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-theorem UInt64.toNat_lt (x : UInt64) : x.toNat < 2 ^ 64 := x.toFin.isLt
-
 @[simp] theorem UInt64.toUInt8_toNat (x : UInt64) : x.toUInt8.toNat = x.toNat % 2 ^ 8 := rfl
 
 @[simp] theorem UInt64.toUInt16_toNat (x : UInt64) : x.toUInt16.toNat = x.toNat % 2 ^ 16 := rfl
@@ -74,22 +66,6 @@ instance : Batteries.LawfulOrd UInt64 := .compareOfLessAndEq
 @[ext] theorem USize.ext : {x y : USize} → x.toNat = y.toNat → x = y
   | ⟨⟨_,_⟩⟩, ⟨⟨_,_⟩⟩, rfl => rfl
 
-theorem USize.size_eq : USize.size = 2 ^ System.Platform.numBits := by
-  rw [USize.size]
-
-theorem USize.le_size : 2 ^ 32 ≤ USize.size := by
-  rw [size_eq]
-  apply Nat.pow_le_pow_right (by decide)
-  cases System.Platform.numBits_eq <;> simp +arith [*]
-
-theorem USize.size_le : USize.size ≤ 2 ^ 64 := by
-  rw [size_eq]
-  apply Nat.pow_le_pow_right (by decide)
-  cases System.Platform.numBits_eq <;> simp +arith [*]
-
-theorem USize.toNat_lt (x : USize) : x.toNat < 2 ^ System.Platform.numBits := by
-  rw [←USize.size_eq]; exact x.toFin.isLt
-
 @[simp] theorem USize.toUInt64_toNat (x : USize) : x.toUInt64.toNat = x.toNat := by
   simp only [USize.toUInt64, UInt64.toNat]; rfl