awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
⊢ a * (b - c) ≤ d ↔ a * b - a * c ≤ d
have inr : a * (b - c) ≤ d ↔ a * b ≤ a * c + d
Tactic: rw [sub_le, mul_le_iff_le_div ha, sub_le, mul_le_iff_le_div ha, mul_add_div _ ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
inr : a * (b - c) ≤ d ↔ a * b ≤ a * c + d
⊢ a * (b - c) ≤ d ↔ a * b - a * c ≤ d
have inr₁ : b - c ≤ d / a ↔ a * b ≤ a * c + d
Tactic: rw [sub_le, mul_le_iff_le_div ha, sub_le, mul_le_iff_le_div ha, mul_add_div _ ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
inr : a * (b - c) ≤ d ↔ a * b ≤ a * c + d
inr₁ : b - c ≤ d / a ↔ a * b ≤ a * c + d
⊢ a * (b - c) ≤ d ↔ a * b - a * c ≤ d
have inr₂ : b ≤ c + d / a ↔ a * b ≤ a * c + d
Tactic: rw [sub_le, mul_le_iff_le_div ha, sub_le, mul_le_iff_le_div ha, mul_add_div _ ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
inr : a * (b - c) ≤ d ↔ a * b ≤ a * c + d
inr₁ : b - c ≤ d / a ↔ a * b ≤ a * c + d
inr₂ : b ≤ c + d / a ↔ a * b ≤ a * c + d
⊢ a * (b - c) ≤ d ↔ a * b - a * c ≤ d
have inr₃ : b ≤ c + d / a ↔ b ≤ (a * c + d) / a
Tactic: rw [sub_le, mul_le_iff_le_div ha, sub_le, mul_le_iff_le_div ha, mul_add_div _ ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
ha : a ≠ 0
d : Ordinal.{u_4}
inr : a * (b - c) ≤ d ↔ a * b ≤ a * c + d
inr₁ : b - c ≤ d / a ↔ a * b ≤ a * c + d
inr₂ : b ≤ c + d / a ↔ a * b ≤ a * c + d
inr₃ : b ≤ c + d / a ↔ b ≤ (a * c + d) / a
⊢ a * (b - c) ≤ d ↔ a * b - a * c ≤ d
have inr₄ : b ≤ c + d / a ↔ b ≤ c + d / a
Tactic: rw [sub_le, mul_le_iff_le_div ha, sub_le, mul_le_iff_le_div ha, mul_add_div _ ha]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
⊢ IsSuccLimit (a + b) ↔ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a
have refine : ∀ (h : IsSuccLimit (a + b)), IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a
Tactic: refine ⟨fun h ↦ ?_, by grind [isSuccLimit_add]⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a
have inl : ∀ (h : IsSuccLimit (a + 0)),
  IsSuccLimit.{u_4 + 1} (α := Ordinal.{u_4}) 0 ∨ Eq.{u_4 + 2} (α := Ordinal.{u_4}) 0 0 ∧ IsSuccLimit a
Tactic: rcases eq_or_ne b 0 with (rfl | h')
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
inl :
  ∀ (h : IsSuccLimit (a + 0)),
    IsSuccLimit.{u_4 + 1} (α := Ordinal.{u_4}) 0 ∨ Eq.{u_4 + 2} (α := Ordinal.{u_4}) 0 0 ∧ IsSuccLimit a
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a
have inr : ∀ (h' : b ≠ 0), IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a
Tactic: rcases eq_or_ne b 0 with (rfl | h')
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
h' : b ≠ 0
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a
have inr : IsSuccLimit (a + b - a) ∨ a + b - a = 0 ∧ IsSuccLimit a
Tactic: rw [← add_sub_cancel a b]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit (a + b) ↔ IsSuccPrelimit b
have rw : IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b
Tactic: rw [isSuccLimit_add_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : IsSuccLimit a
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b
have inl : IsSuccLimit.{u_4 + 1} (α := Ordinal.{u_4}) 0 ∨ Eq.{u_4 + 2} (α := Ordinal.{u_4}) 0 0 ∧ IsSuccLimit a ↔
  IsSuccPrelimit.{u_4 + 1} (α := Ordinal.{u_4}) 0
Tactic: obtain rfl | hb := eq_or_ne b 0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : IsSuccLimit a
inl :
  IsSuccLimit.{u_4 + 1} (α := Ordinal.{u_4}) 0 ∨ Eq.{u_4 + 2} (α := Ordinal.{u_4}) 0 0 ∧ IsSuccLimit a ↔
    IsSuccPrelimit.{u_4 + 1} (α := Ordinal.{u_4}) 0
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b
have inr : ∀ (hb : b ≠ 0), IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b
Tactic: obtain rfl | hb := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c b : Ordinal.{u_4}
h : a ∣ a * b + c
d : Ordinal.{u_4}
e : a * b + c = a * d
⊢ c = a * (d - b)
have rw : c = a * d - a * b
Tactic: rw [mul_sub, ← e, add_sub_cancel]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c b : Ordinal.{u_4}
h : a ∣ a * b + c
d : Ordinal.{u_4}
e : a * b + c = a * d
rw : c = a * d - a * b
⊢ c = a * (d - b)
have rw₁ : c = a * b + c - a * b
Tactic: rw [mul_sub, ← e, add_sub_cancel]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c b : Ordinal.{u_4}
h : a ∣ a * b + c
d : Ordinal.{u_4}
e : a * b + c = a * d
rw : c = a * d - a * b
rw₁ : c = a * b + c - a * b
⊢ c = a * (d - b)
have rw₂ : c = c
Tactic: rw [mul_sub, ← e, add_sub_cancel]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c b : Ordinal.{u_4}
h : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * b + c
have rw : a ∣ a * (b + d)
Tactic: rw [e, ← mul_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
a0 : a ≠ 0
b : Ordinal.{u_4}
⊢ a * (a * b / a) = a * b
have rw : a * b = a * b
Tactic: rw [mul_div_cancel _ a0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
b0 : b ≠ 0
h : a ∣ b
⊢ a ≤ b
have rcases : ∀ (b : Ordinal.{u_4}) (b0 : a * b ≠ 0), a ≤ a * b
Tactic: rcases h with ⟨b, rfl⟩
Cleared hypotheses: b, b0, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h₁ : a ∣ b
h₂ : b ∣ a
a0 : a = 0
⊢ a = b
have subst : ∀ (h₁ : 0 ∣ b) (h₂ : b ∣ 0), 0 = b
Tactic: subst a
Cleared hypotheses: a, h₁, h₂, a0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h₁ : a ∣ b
h₂ : b ∣ a
a0 : ¬a = 0
b0 : b = 0
⊢ a = b
have subst : ∀ (h₁ : a ∣ 0) (h₂ : 0 ∣ a), a = 0
Tactic: subst b
Cleared hypotheses: b, h₁, h₂, b0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a % b < b
have rw : a < b * (a / b) + b
Tactic: rw [← add_lt_add_iff_left, div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
⊢ a % a = 0
have inl : HMod.hMod (α := Ordinal.{u_4}) 0 0 = 0
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
inl : HMod.hMod (α := Ordinal.{u_4}) 0 0 = 0
⊢ a % a = 0
have inr : ∀ (ha : a ≠ 0), a % a = 0
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
H : b ∣ a
⊢ a % b = 0
have rcases : ∀ (c : Ordinal.{u_4}), b * c % b = 0
Tactic: rcases H with ⟨c, rfl⟩
Cleared hypotheses: a, H
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
b c : Ordinal.{u_4}
⊢ b * c % b = 0
have inl : 0 * c % 0 = 0
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
b c : Ordinal.{u_4}
inl : 0 * c % 0 = 0
⊢ b * c % b = 0
have inr : ∀ (hb : b ≠ 0), b * c % b = 0
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
⊢ (x * y + z) % x = z % x
have inl : (0 * y + z) % 0 = z % 0
Tactic: rcases eq_or_ne x 0 with rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
inl : (0 * y + z) % 0 = z % 0
⊢ (x * y + z) % x = z % x
have inr : ∀ (hx : x ≠ 0), (x * y + z) % x = z % x
Tactic: rcases eq_or_ne x 0 with rfl | hx
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ (x * y + z) % x = z % x
have inr : x * y + z - x * ((x * y + z) / x) = z % x
Tactic: rwa [mod_def, mul_add_div, mul_add, ← sub_sub, add_sub_cancel, mod_def]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
hx : x ≠ 0
inr : x * y + z - x * ((x * y + z) / x) = z % x
⊢ (x * y + z) % x = z % x
have inr₁ : x * y + z - x * (y + z / x) = z % x
Tactic: rwa [mod_def, mul_add_div, mul_add, ← sub_sub, add_sub_cancel, mod_def]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
hx : x ≠ 0
inr : x * y + z - x * ((x * y + z) / x) = z % x
inr₁ : x * y + z - x * (y + z / x) = z % x
inr₂ : x ≠ 0
⊢ (x * y + z) % x = z % x
have inr₃ : x * y + z - (x * y + x * (z / x)) = z % x
Tactic: rwa [mod_def, mul_add_div, mul_add, ← sub_sub, add_sub_cancel, mod_def]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
hx : x ≠ 0
inr : x * y + z - x * ((x * y + z) / x) = z % x
inr₁ : x * y + z - x * (y + z / x) = z % x
inr₂ : x ≠ 0
inr₃ : x * y + z - (x * y + x * (z / x)) = z % x
inr₄ : x ≠ 0
⊢ (x * y + z) % x = z % x
have inr₅ : x * y + z - x * y - x * (z / x) = z % x
Tactic: rwa [mod_def, mul_add_div, mul_add, ← sub_sub, add_sub_cancel, mod_def]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
hx : x ≠ 0
inr : x * y + z - x * ((x * y + z) / x) = z % x
inr₁ : x * y + z - x * (y + z / x) = z % x
inr₂ : x ≠ 0
inr₃ : x * y + z - (x * y + x * (z / x)) = z % x
inr₄ : x ≠ 0
inr₅ : x * y + z - x * y - x * (z / x) = z % x
inr₆ : x ≠ 0
⊢ (x * y + z) % x = z % x
have inr₇ : z - x * (z / x) = z % x
Tactic: rwa [mod_def, mul_add_div, mul_add, ← sub_sub, add_sub_cancel, mod_def]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
hx : x ≠ 0
inr : x * y + z - x * ((x * y + z) / x) = z % x
inr₁ : x * y + z - x * (y + z / x) = z % x
inr₂ : x ≠ 0
inr₃ : x * y + z - (x * y + x * (z / x)) = z % x
inr₄ : x ≠ 0
inr₅ : x * y + z - x * y - x * (z / x) = z % x
inr₆ : x ≠ 0
inr₇ : z - x * (z / x) = z % x
inr₈ : x ≠ 0
⊢ (x * y + z) % x = z % x
have inr₉ : z - x * (z / x) = z - x * (z / x)
Tactic: rwa [mod_def, mul_add_div, mul_add, ← sub_sub, add_sub_cancel, mod_def]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ (x * y + w) % (x * z) = x * (y % z) + w
have rw : x * y + w - x * z * (y / z) = x * (y % z) + w
Tactic: rw [mod_def, mul_add_div_mul hw]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * y + w - x * z * (y / z) = x * (y % z) + w
have h : x * z * (y / z) + (x * (y % z) + w) = x * y + w
Tactic: apply sub_eq_of_add_eq
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
⊢ x * z * (y / z) + (x * (y % z) + w) = x * y + w
have h : x * z * (y / z) + x * (y % z) + w = x * y + w
Tactic: rw [← add_assoc, mul_assoc, ← mul_add, div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
h : x * z * (y / z) + x * (y % z) + w = x * y + w
⊢ x * z * (y / z) + (x * (y % z) + w) = x * y + w
have h₁ : x * (z * (y / z)) + x * (y % z) + w = x * y + w
Tactic: rw [← add_assoc, mul_assoc, ← mul_add, div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
h : x * z * (y / z) + x * (y % z) + w = x * y + w
h₁ : x * (z * (y / z)) + x * (y % z) + w = x * y + w
⊢ x * z * (y / z) + (x * (y % z) + w) = x * y + w
have h₂ : x * (z * (y / z) + y % z) + w = x * y + w
Tactic: rw [← add_assoc, mul_assoc, ← mul_add, div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
h : x * z * (y / z) + x * (y % z) + w = x * y + w
h₁ : x * (z * (y / z)) + x * (y % z) + w = x * y + w
h₂ : x * (z * (y / z) + y % z) + w = x * y + w
⊢ x * z * (y / z) + (x * (y % z) + w) = x * y + w
have h₃ : x * y + w = x * y + w
Tactic: rw [← add_assoc, mul_assoc, ← mul_add, div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
⊢ x * y % (x * z) = x * (y % z)
have inl : 0 * y % (0 * z) = 0 * (y % z)
Tactic: obtain rfl | hx := eq_zero_or_pos x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
inl : 0 * y % (0 * z) = 0 * (y % z)
⊢ x * y % (x * z) = x * (y % z)
have inr : ∀ (hx : 0 < x), x * y % (x * z) = x * (y % z)
Tactic: obtain rfl | hx := eq_zero_or_pos x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = x * (y % z)
have h : x * y % (x * z) = (x * y + 0) % (x * z)
Tactic: convert! mul_add_mod_mul hx y z using 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
hx : 0 < x
h : x * y % (x * z) = (x * y + 0) % (x * z)
⊢ x * y % (x * z) = x * (y % z)
have h₁ : x * (y % z) = x * (y % z) + 0
Tactic: convert! mul_add_mod_mul hx y z using 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * y % (x * z) = (x * y + 0) % (x * z)
have h : x * y % (x * z) = x * y % (x * z)
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ x * (y % z) = x * (y % z) + 0
have h : x * (y % z) = x * (y % z)
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : c ∣ b
⊢ a % b % c = a % c
have nth_rw : a % b % c = (b * (a / b) + a % b) % c
Tactic: nth_rw 2 [← div_add_mod a b]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : c ∣ b
⊢ a % b % c = (b * (a / b) + a % b) % c
have rcases : ∀ (d : Ordinal.{u_4}), a % (c * d) % c = (c * d * (a / (c * d)) + a % (c * d)) % c
Tactic: rcases h with ⟨d, rfl⟩
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c d : Ordinal.{u_4}
⊢ a % (c * d) % c = (c * d * (a / (c * d)) + a % (c * d)) % c
have rw : a % (c * d) % c = (c * (d * (a / (c * d))) + a % (c * d)) % c
Tactic: rw [mul_assoc, mul_add_mod_self]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c d : Ordinal.{u_4}
rw : a % (c * d) % c = (c * (d * (a / (c * d))) + a % (c * d)) % c
⊢ a % (c * d) % c = (c * d * (a / (c * d)) + a % (c * d)) % c
have rw₁ : a % (c * d) % c = a % (c * d) % c
Tactic: rw [mul_assoc, mul_add_mod_self]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
⊢ a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r
have inl : a < 0 * c ↔ ∃ q < c, ∃ r < 0, a = 0 * q + r
Tactic: obtain rfl | hb₀ := eq_or_ne b 0
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
inl : a < 0 * c ↔ ∃ q < c, ∃ r < 0, a = 0 * q + r
⊢ a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r
have inr : ∀ (hb₀ : b ≠ 0), a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r
Tactic: obtain rfl | hb₀ := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
hb₀ : b ≠ 0
⊢ a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r
have inr : (∃ q < c, ∃ r < b, a = b * q + r) → a < b * c
Tactic: refine ⟨fun h ↦ ⟨_, (lt_mul_iff_div_lt hb₀).1 h, _, mod_lt a hb₀, (div_add_mod ..).symm⟩, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
b c : Ordinal.{u_4}
hb₀ : b ≠ 0
q : Ordinal.{u_4}
hq : q < c
r : Ordinal.{u_4}
hr : r < b
⊢ b * q + r < b * c
have inr : b * q + b ≤ b * c
Tactic: apply add_lt_add_right hr _ |>.trans_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
b c : Ordinal.{u_4}
hb₀ : b ≠ 0
q : Ordinal.{u_4}
hq : q < c
r : Ordinal.{u_4}
hr : r < b
⊢ b * q + b ≤ b * c
have inr : b * (q + 1) ≤ b * c
Tactic: grw [← mul_add_one, add_one_le_iff.2 hq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
b c : Ordinal.{u_4}
hb₀ : b ≠ 0
q : Ordinal.{u_4}
hq : q < c
r : Ordinal.{u_4}
hr : r < b
inr : b * (q + 1) ≤ b * c
⊢ b * q + b ≤ b * c
have inr₁ : b * c ≤ b * c
Tactic: grw [← mul_add_one, add_one_le_iff.2 hq]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ CharZero Ordinal.{u_4}
have refine : ∀ (a b : ℕ) (h : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑a : Ordinal.{u_4}) (↑b : Ordinal.{u_4})), a = b
Tactic: refine ⟨fun a b h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : ℕ
h : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑a : Ordinal.{u_4}) (↑b : Ordinal.{u_4})
⊢ a = b
have rwa : ∀ (h : ord (↑a : Cardinal.{u_4}) = (↑b : Ordinal.{u_4})), a = b
Tactic: rwa [← Cardinal.ord_natCast, ← Cardinal.ord_natCast, Cardinal.ord_inj, Nat.cast_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : ℕ
h : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑a : Ordinal.{u_4}) (↑b : Ordinal.{u_4})
rwa : ∀ (h : ord (↑a : Cardinal.{u_4}) = (↑b : Ordinal.{u_4})), a = b
⊢ a = b
have rwa₁ : ∀ (h : ord (↑a : Cardinal.{u_4}) = ord (↑b : Cardinal.{u_4})), a = b
Tactic: rwa [← Cardinal.ord_natCast, ← Cardinal.ord_natCast, Cardinal.ord_inj, Nat.cast_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : ℕ
h : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑a : Ordinal.{u_4}) (↑b : Ordinal.{u_4})
rwa : ∀ (h : ord (↑a : Cardinal.{u_4}) = (↑b : Ordinal.{u_4})), a = b
rwa₁ : ∀ (h : ord (↑a : Cardinal.{u_4}) = ord (↑b : Cardinal.{u_4})), a = b
⊢ a = b
have rwa₂ : ∀ (h : Eq.{u_4 + 2} (α := Cardinal.{u_4}) (↑a : Cardinal.{u_4}) (↑b : Cardinal.{u_4})), a = b
Tactic: rwa [← Cardinal.ord_natCast, ← Cardinal.ord_natCast, Cardinal.ord_inj, Nat.cast_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
a b : ℕ
h : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑a : Ordinal.{u_4}) (↑b : Ordinal.{u_4})
rwa : ∀ (h : ord (↑a : Cardinal.{u_4}) = (↑b : Ordinal.{u_4})), a = b
rwa₁ : ∀ (h : ord (↑a : Cardinal.{u_4}) = ord (↑b : Cardinal.{u_4})), a = b
rwa₂ : ∀ (h : Eq.{u_4 + 2} (α := Cardinal.{u_4}) (↑a : Cardinal.{u_4}) (↑b : Cardinal.{u_4})), a = b
⊢ a = b
have rwa₃ : ∀ (h : a = b), a = b
Tactic: rwa [← Cardinal.ord_natCast, ← Cardinal.ord_natCast, Cardinal.ord_inj, Nat.cast_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m : ℕ
⊢ HAdd.hAdd (α := Ordinal.{u_4}) 1 (↑m : Ordinal.{u_4}) = (↑(succ m) : Ordinal.{u_4})
have rw : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑(m + 1) : Ordinal.{u_4}) (↑(succ m) : Ordinal.{u_4})
Tactic: rw [← Nat.cast_one, ← Nat.cast_add, add_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
⊢ (↑(m * (n + 1)) : Ordinal.{u_4}) = HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
have rw : (↑(m * n + m) : Ordinal.{u_4}) = HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
Tactic: rw [Nat.mul_succ, Nat.cast_add, natCast_mul m n, Nat.cast_succ, mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
rw : (↑(m * n + m) : Ordinal.{u_4}) = HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
⊢ (↑(m * (n + 1)) : Ordinal.{u_4}) = HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
have rw₁ : HAdd.hAdd (α := Ordinal.{u_4}) (↑(m * n) : Ordinal.{u_4}) (↑m : Ordinal.{u_4}) =
  HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
Tactic: rw [Nat.mul_succ, Nat.cast_add, natCast_mul m n, Nat.cast_succ, mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
rw : (↑(m * n + m) : Ordinal.{u_4}) = HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
rw₁ :
  HAdd.hAdd (α := Ordinal.{u_4}) (↑(m * n) : Ordinal.{u_4}) (↑m : Ordinal.{u_4}) =
    HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
⊢ (↑(m * (n + 1)) : Ordinal.{u_4}) = HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
have rw₂ : HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) + (↑m : Ordinal.{u_4}) =
  HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
Tactic: rw [Nat.mul_succ, Nat.cast_add, natCast_mul m n, Nat.cast_succ, mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
rw : (↑(m * n + m) : Ordinal.{u_4}) = HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
rw₁ :
  HAdd.hAdd (α := Ordinal.{u_4}) (↑(m * n) : Ordinal.{u_4}) (↑m : Ordinal.{u_4}) =
    HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
rw₂ :
  HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) + (↑m : Ordinal.{u_4}) =
    HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
⊢ (↑(m * (n + 1)) : Ordinal.{u_4}) = HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
have rw₃ : HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) + (↑m : Ordinal.{u_4}) =
  (↑m : Ordinal.{u_4}) * HAdd.hAdd (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 1
Tactic: rw [Nat.mul_succ, Nat.cast_add, natCast_mul m n, Nat.cast_succ, mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
rw : (↑(m * n + m) : Ordinal.{u_4}) = HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
rw₁ :
  HAdd.hAdd (α := Ordinal.{u_4}) (↑(m * n) : Ordinal.{u_4}) (↑m : Ordinal.{u_4}) =
    HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
rw₂ :
  HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) + (↑m : Ordinal.{u_4}) =
    HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
rw₃ :
  HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) + (↑m : Ordinal.{u_4}) =
    (↑m : Ordinal.{u_4}) * HAdd.hAdd (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 1
⊢ (↑(m * (n + 1)) : Ordinal.{u_4}) = HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑(n + 1) : Ordinal.{u_4})
have rw₄ : HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) + (↑m : Ordinal.{u_4}) =
  HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) + (↑m : Ordinal.{u_4})
Tactic: rw [Nat.mul_succ, Nat.cast_add, natCast_mul m n, Nat.cast_succ, mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
⊢ (↑(m - n) : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have inl : ∀ (h : m ≤ n), (↑(m - n) : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
Tactic: rcases le_total m n with h | h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
inl :
  ∀ (h : m ≤ n), (↑(m - n) : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
⊢ (↑(m - n) : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have inr : ∀ (h : n ≤ m), (↑(m - n) : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
Tactic: rcases le_total m n with h | h