awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a → IsSuccLimit (a + b)

Tactic:
grind [isSuccLimit_add]

Premises used: Ordinal.isSuccLimit_add
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
refine : ∀ (h : IsSuccLimit (a + b)), IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a
⊢ IsSuccLimit (a + b) ↔ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a

Tactic:
refine ⟨fun h ↦ ?_, by grind [isSuccLimit_add]⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
inr : ∀ (h' : b ≠ 0), IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a

Tactic:
rcases eq_or_ne b 0 with (rfl | h')

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
h : IsSuccLimit (a + 0)
⊢ IsSuccLimit.{u_4 + 1} (α := Ordinal.{u_4}) 0 ∨ Eq.{u_4 + 2} (α := Ordinal.{u_4}) 0 0 ∧ IsSuccLimit a

Tactic:
grind
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
h' : b ≠ 0
inr : IsSuccLimit (a + b - a) ∨ a + b - a = 0 ∧ IsSuccLimit a
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a

Tactic:
rw [← add_sub_cancel a b]

Premises used: Ordinal.add_sub_cancel
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
h' : b ≠ 0
⊢ IsSuccLimit (a + b - a) ∨ a + b - a = 0 ∧ IsSuccLimit a

Tactic:
.inl <| isSuccLimit_sub h.isSuccPrelimit <| lt_add_of_pos_right a h'.pos

Premises used: lt_add_of_pos_right, Ne.pos, Order.IsSuccLimit.isSuccPrelimit, Or.inl, Ordinal.isSuccLimit_sub
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : IsSuccLimit (a + b)
h' : b ≠ 0
⊢ IsSuccLimit (a + b - a) ∨ a + b - a = 0 ∧ IsSuccLimit a

Tactic:
exact .inl <| isSuccLimit_sub h.isSuccPrelimit <| lt_add_of_pos_right a h'.pos

Premises used: lt_add_of_pos_right, Ne.pos, Order.IsSuccLimit.isSuccPrelimit, Ordinal.isSuccLimit_sub
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : IsSuccLimit a
rw : IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b
⊢ IsSuccLimit (a + b) ↔ IsSuccPrelimit b

Tactic:
rw [isSuccLimit_add_iff]

Premises used: Ordinal.isSuccLimit_add_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
inr : ∀ (hb : b ≠ 0), IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b

Tactic:
obtain rfl | hb := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
h : IsSuccLimit a
⊢ 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:
simpa
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : IsSuccLimit a
hb : b ≠ 0
⊢ IsSuccLimit b ∨ b = 0 ∧ IsSuccLimit a ↔ IsSuccPrelimit b

Tactic:
simp [hb, isSuccLimit_iff]

Premises used: Ordinal.isSuccLimit_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
rw₂ rw₃ : c = c
⊢ c = a * (d - b)

Tactic:
rw [mul_sub, ← e, add_sub_cancel]

Premises used: Ordinal.add_sub_cancel, Ordinal.mul_sub
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c b : Ordinal.{u_4}
h : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
rw : a ∣ a * (b + d)
⊢ a ∣ a * b + c

Tactic:
rw [e, ← mul_add]

Premises used: mul_add
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c b : Ordinal.{u_4}
h : a ∣ c
d : Ordinal.{u_4}
e : c = a * d
⊢ a ∣ a * (b + d)

Tactic:
apply dvd_mul_right

Premises used: dvd_mul_right
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
a0 : a ≠ 0
b : Ordinal.{u_4}
rw rw₁ : a * b = a * b
⊢ a * (a * b / a) = a * b

Tactic:
rw [mul_div_cancel _ a0]

Premises used: Ordinal.mul_div_cancel
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
b0 : b ≠ 0
h : a ∣ b
rcases : ∀ (b : Ordinal.{u_4}) (b0 : a * b ≠ 0), a ≤ a * b
⊢ a ≤ b

Tactic:
rcases h with ⟨b, rfl⟩

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
b0 : a * b ≠ 0
h : b = 0
⊢ False

Tactic:
simp [h] at b0
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
b0 : a * b ≠ 0
⊢ a ≤ a * b

Tactic:
simpa using mul_le_mul_right (one_le_iff_ne_zero.mpr fun h ↦ by simp [h] at b0) a

Premises used: Iff.mpr, mul_le_mul_right, Order.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h₁ : a ∣ b
h₂ : b ∣ a
a0 : a = 0
subst : ∀ (h₁ : 0 ∣ b) (h₂ : b ∣ 0), 0 = b
⊢ a = b

Tactic:
subst a
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
b : Ordinal.{u_4}
h₁ : 0 ∣ b
h₂ : b ∣ 0
⊢ 0 = b

Tactic:
(eq_zero_of_zero_dvd h₁).symm

Premises used: eq_zero_of_zero_dvd, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
b : Ordinal.{u_4}
h₁ : 0 ∣ b
h₂ : b ∣ 0
⊢ 0 = b

Tactic:
exact (eq_zero_of_zero_dvd h₁).symm

Premises used: eq_zero_of_zero_dvd, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h₁ : a ∣ b
h₂ : b ∣ a
a0 : ¬a = 0
b0 : b = 0
subst : ∀ (h₁ : a ∣ 0) (h₂ : 0 ∣ a), a = 0
⊢ a = b

Tactic:
subst b
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
a0 : ¬a = 0
h₁ : a ∣ 0
h₂ : 0 ∣ a
⊢ a = 0

Tactic:
eq_zero_of_zero_dvd h₂

Premises used: eq_zero_of_zero_dvd
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
a0 : ¬a = 0
h₁ : a ∣ 0
h₂ : 0 ∣ a
⊢ a = 0

Tactic:
exact eq_zero_of_zero_dvd h₂

Premises used: eq_zero_of_zero_dvd
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ a % b = a - b * (a / b)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ a % b ≤ a

Tactic:
sub_le_self a _

Premises used: Ordinal.sub_le_self
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
⊢ a % 0 = a

Tactic:
simp [mod_def]

Premises used: Ordinal.mod_def
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : a < b
⊢ a % b = a

Tactic:
simp [mod_def, div_eq_zero_of_lt h]

Premises used: Ordinal.div_eq_zero_of_lt, Ordinal.mod_def
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
b : Ordinal.{u_4}
⊢ 0 % b = 0

Tactic:
simp [mod_def]

Premises used: Ordinal.mod_def
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ b * (a / b) + a % b = a

Tactic:
Ordinal.add_sub_cancel_of_le <| mul_div_le _ _

Premises used: Ordinal.add_sub_cancel_of_le, Ordinal.mul_div_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : b ≠ 0
rw : a < b * (a / b) + b
⊢ a % b < b

Tactic:
rw [← add_lt_add_iff_left, div_add_mod]

Premises used: Ordinal.div_add_mod, add_lt_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * (a / b) + b

Tactic:
lt_mul_div_add a h

Premises used: Ordinal.lt_mul_div_add
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * (a / b) + b

Tactic:
exact lt_mul_div_add a h

Premises used: Ordinal.lt_mul_div_add
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
inl : HMod.hMod (α := Ordinal.{u_4}) 0 0 = 0
inr : ∀ (ha : a ≠ 0), a % a = 0
⊢ a % a = 0

Tactic:
obtain rfl | ha := eq_or_ne a 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
⊢ HMod.hMod (α := Ordinal.{u_4}) 0 0 = 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
ha : a ≠ 0
⊢ a % a = 0

Tactic:
simp [mod_def, ha]

Premises used: Ordinal.mod_def
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
⊢ a % 1 = 0

Tactic:
simp [mod_def]

Premises used: Ordinal.mod_def
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
H : a % b = 0
⊢ a = b * (a / b)

Tactic:
simpa [H] using (div_add_mod a b).symm

Premises used: Ordinal.div_add_mod, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
H : b ∣ a
rcases : ∀ (c : Ordinal.{u_4}), b * c % b = 0
⊢ a % b = 0

Tactic:
rcases H with ⟨c, rfl⟩

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
b c : Ordinal.{u_4}
inl : 0 * c % 0 = 0
inr : ∀ (hb : b ≠ 0), b * c % b = 0
⊢ b * c % b = 0

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
c : Ordinal.{u_4}
⊢ 0 * c % 0 = 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ b * c % b = 0

Tactic:
simp [mod_def, hb]

Premises used: Ordinal.mod_def
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ b ∣ a ↔ a % b = 0

Tactic:
⟨mod_eq_zero_of_dvd, dvd_of_mod_eq_zero⟩

Premises used: Ordinal.dvd_of_mod_eq_zero, Iff.intro, Ordinal.mod_eq_zero_of_dvd
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
x y z : Ordinal.{u_4}
inl : (0 * y + z) % 0 = z % 0
inr : ∀ (hx : x ≠ 0), (x * y + z) % x = z % x
⊢ (x * y + z) % x = z % x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
y z : Ordinal.{u_4}
⊢ (0 * y + z) % 0 = z % 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
inr₉ : z - x * (z / x) = z - x * (z / x)
inr₁₀ : x ≠ 0
inr₁₁ : z - x * (z / x) = z - x * (z / x)
inr₁₂ inr₁₃ inr₁₄ : x ≠ 0
⊢ (x * y + z) % x = z % x

Tactic:
rwa [mod_def, mul_add_div, mul_add, ← sub_sub, add_sub_cancel, mod_def]

Premises used: Ordinal.mul_add_div, Ordinal.add_sub_cancel, mul_add, Ordinal.sub_sub, Ordinal.mod_def
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
x y : Ordinal.{u_4}
⊢ x * y % x = 0

Tactic:
simpa using mul_add_mod_self x y 0

Premises used: Ordinal.mul_add_mod_self, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
w x : Ordinal.{u_4}
hw : w < x
y z : Ordinal.{u_4}
rw : x * y + w - x * z * (y / z) = x * (y % z) + w
⊢ (x * y + w) % (x * z) = x * (y % z) + w

Tactic:
rw [mod_def, mul_add_div_mul hw]

Premises used: Ordinal.mul_add_div_mul, Ordinal.mod_def
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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 * y + w - x * z * (y / z) = x * (y % z) + w

Tactic:
apply sub_eq_of_add_eq

Premises used: Ordinal.sub_eq_of_add_eq
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
h₃ h₄ : x * y + w = x * y + w
⊢ x * z * (y / z) + (x * (y % z) + w) = x * y + w

Tactic:
rw [← add_assoc, mul_assoc, ← mul_add, div_add_mod]

Premises used: Ordinal.div_add_mod, add_assoc, mul_assoc, mul_add
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
x y z : Ordinal.{u_4}
inl : 0 * y % (0 * z) = 0 * (y % z)
inr : ∀ (hx : 0 < x), x * y % (x * z) = x * (y % z)
⊢ x * y % (x * z) = x * (y % z)

Tactic:
obtain rfl | hx := eq_zero_or_pos x

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
y z : Ordinal.{u_4}
⊢ 0 * y % (0 * z) = 0 * (y % z)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
x y z : Ordinal.{u_4}
hx : 0 < x
⊢ (x * y + 0) % (x * z) = x * (y % z) + 0

Tactic:
mul_add_mod_mul hx y z

Premises used: Ordinal.mul_add_mod_mul
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
x y z : Ordinal.{u_4}
hx : 0 < x
h : x * y % (x * z) = (x * y + 0) % (x * z)
h₁ : x * (y % z) = x * (y % z) + 0
⊢ x * y % (x * z) = x * (y % z)

Tactic:
convert! mul_add_mod_mul hx y z using 1

Premises used: Ordinal.mul_add_mod_mul
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
x y z : Ordinal.{u_4}
hx : 0 < x
h h₁ : x * y % (x * z) = x * y % (x * z)
⊢ x * y % (x * z) = (x * y + 0) % (x * z)

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
x y z : Ordinal.{u_4}
hx : 0 < x
h h₁ : x * (y % z) = x * (y % z)
⊢ x * (y % z) = x * (y % z) + 0

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : c ∣ b
nth_rw : a % b % c = (b * (a / b) + a % b) % c
⊢ a % b % c = a % c

Tactic:
nth_rw 2 [← div_add_mod a b]

Premises used: Ordinal.div_add_mod
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : c ∣ b
rcases : ∀ (d : Ordinal.{u_4}), a % (c * d) % c = (c * d * (a / (c * d)) + a % (c * d)) % c
⊢ a % b % c = (b * (a / b) + a % b) % c

Tactic:
rcases h with ⟨d, rfl⟩

Premises used: rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c d : Ordinal.{u_4}
rw : a % (c * d) % c = (c * (d * (a / (c * d))) + a % (c * d)) % c
rw₁ rw₂ : a % (c * d) % c = a % (c * d) % c
⊢ a % (c * d) % c = (c * d * (a / (c * d)) + a % (c * d)) % c

Tactic:
rw [mul_assoc, mul_add_mod_self]

Premises used: mul_assoc, Ordinal.mul_add_mod_self
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
⊢ a % b % b = a % b

Tactic:
mod_mod_of_dvd a dvd_rfl

Premises used: dvd_rfl, Ordinal.mod_mod_of_dvd
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
inl : a < 0 * c ↔ ∃ q < c, ∃ r < 0, a = 0 * q + r
inr : ∀ (hb₀ : b ≠ 0), a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r
⊢ a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r

Tactic:
obtain rfl | hb₀ := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
⊢ a < 0 * c ↔ ∃ q < c, ∃ r < 0, a = 0 * q + r

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hb₀ : b ≠ 0
⊢ a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r

Tactic:
⟨fun h ↦ ⟨_, (lt_mul_iff_div_lt hb₀).1 h, _, mod_lt a hb₀, (div_add_mod ..).symm⟩, ?_⟩

Premises used: Ordinal.lt_mul_iff_div_lt, Ordinal.div_add_mod, HDiv.hDiv, Ordinal.mod_lt, HMod.hMod, And.intro, Iff.intro, Exists.intro, Iff.mp, Eq.symm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hb₀ : b ≠ 0
inr : (∃ q < c, ∃ r < b, a = b * q + r) → a < b * c
⊢ a < b * c ↔ ∃ q < c, ∃ r < b, a = b * q + r

Tactic:
refine ⟨fun h ↦ ⟨_, (lt_mul_iff_div_lt hb₀).1 h, _, mod_lt a hb₀, (div_add_mod ..).symm⟩, ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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 + b ≤ b * c
⊢ b * q + r < b * c

Tactic:
apply add_lt_add_right hr _ |>.trans_le

Premises used: add_lt_add_right, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
inr₁ inr₂ : b * c ≤ b * c
⊢ b * q + b ≤ b * c

Tactic:
grw [← mul_add_one, add_one_le_iff.2 hq]

Premises used: Iff.mpr, Order.add_one_le_iff, mul_add_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
b c : Ordinal.{u_4}
P : Ordinal.{u_4} → Prop
⊢ (∀ a < b * c, P a) ↔ ∀ q < c, ∀ r < b, P (b * q + r)

Tactic:
grind [lt_mul_iff]

Premises used: Ordinal.lt_mul_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
b c : Ordinal.{u_4}
P : Ordinal.{u_4} → Prop
⊢ (∃ a < b * c, P a) ↔ ∃ q < c, ∃ r < b, P (b * q + r)

Tactic:
grind [lt_mul_iff]

Premises used: Ordinal.lt_mul_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ CharZero Ordinal.{u_4}

Tactic:
⟨fun a b h ↦ ?_⟩

Premises used: CharZero.mk
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
refine : ∀ (a b : ℕ) (h : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑a : Ordinal.{u_4}) (↑b : Ordinal.{u_4})), a = b
⊢ CharZero Ordinal.{u_4}

Tactic:
refine ⟨fun a b h ↦ ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (h : a = b), a = b
⊢ a = b

Tactic:
rwa [← Cardinal.ord_natCast, ← Cardinal.ord_natCast, Cardinal.ord_inj, Nat.cast_inj] at h

Premises used: Cardinal.ord_inj, Nat.cast_inj, Cardinal.ord_natCast
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m : ℕ
rw : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑(m + 1) : Ordinal.{u_4}) (↑(succ m) : Ordinal.{u_4})
⊢ HAdd.hAdd (α := Ordinal.{u_4}) 1 (↑m : Ordinal.{u_4}) = (↑(succ m) : Ordinal.{u_4})

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, add_comm]

Premises used: add_comm, Nat.cast_add, Nat.cast_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m : ℕ
⊢ Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑(m + 1) : Ordinal.{u_4}) (↑(succ m) : Ordinal.{u_4})

Tactic:
rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m : ℕ
inst : m.AtLeastTwo
⊢ HAdd.hAdd (α := Ordinal.{u_4}) 1 (OfNat.ofNat m) = succ (OfNat.ofNat m)

Tactic:
one_add_natCast m

Premises used: Order.succ, Ordinal.one_add_natCast, Nat.unaryCast
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m : ℕ
⊢ (↑(m * 0) : Ordinal.{u_4}) = HMul.hMul (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑0 : Ordinal.{u_4})

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
rw₄ 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})
⊢ (↑(m * (n + 1)) : 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]

Premises used: Nat.cast_succ, Nat.mul_succ, Nat.cast_add, mul_add_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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})
inr :
  ∀ (h : n ≤ m), (↑(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})

Tactic:
rcases le_total m n with h | h

Premises used: le_total
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m n : ℕ
h : m ≤ n
inl : (↑0 : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
inl₁ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑0 : Ordinal.{u_4}) 0
inl₂ inl₃ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) 0 0
⊢ (↑(m - n) : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})

Tactic:
rw [tsub_eq_zero_iff_le.2 h, Ordinal.sub_eq_zero_iff_le.2 (Nat.cast_le.2 h), Nat.cast_zero]

Premises used: Iff.mpr, Ordinal.sub_eq_zero_iff_le, tsub_eq_zero_iff_le, Nat.cast_zero, Nat.cast_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m n : ℕ
h : n ≤ m
inr :
  HAdd.hAdd (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑(m - n) : Ordinal.{u_4}) =
    (↑n : Ordinal.{u_4}) + HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
inr₁ :
  (↑(n + (m - n)) : Ordinal.{u_4}) =
    (↑n : Ordinal.{u_4}) + HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
inr₂ :
  (↑m : Ordinal.{u_4}) = (↑n : Ordinal.{u_4}) + HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
inr₃ inr₄ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑m : Ordinal.{u_4})
⊢ (↑(m - n) : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})

Tactic:
rw [← add_left_cancel_iff (a := ↑n), ← Nat.cast_add, add_tsub_cancel_of_le h,
      Ordinal.add_sub_cancel_of_le (Nat.cast_le.2 h)]

Premises used: Iff.mpr, add_left_cancel_iff, Nat.cast_add, Ordinal.add_sub_cancel_of_le, Nat.cast_le, add_tsub_cancel_of_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m n : ℕ
inl : (↑(m / 0) : Ordinal.{u_4}) = HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑0 : Ordinal.{u_4})
inr :
  ∀ (hn : n ≠ 0), (↑(m / n) : Ordinal.{u_4}) = HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
⊢ (↑(m / n) : Ordinal.{u_4}) = HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m : ℕ
⊢ (↑(m / 0) : Ordinal.{u_4}) = HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑0 : Ordinal.{u_4})

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m n : ℕ
hn : n ≠ 0
⊢ Ne.{u_4 + 2} (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 0

Tactic:
have hn' : (n : Ordinal) ≠ 0 := Nat.cast_ne_zero.2 hn
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m n : ℕ
hn : n ≠ 0
hn' : Ne.{u_4 + 2} (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 0
inr : (↑(m / n) : Ordinal.{u_4}) ≤ HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
inr₁ : HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) ≤ (↑(m / n) : Ordinal.{u_4})
⊢ (↑(m / n) : Ordinal.{u_4}) = HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m n : ℕ
hn : n ≠ 0
hn' : Ne.{u_4 + 2} (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 0
inr : m / n * n ≤ m
⊢ (↑(m / n) : Ordinal.{u_4}) ≤ HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})

Tactic:
rw [← mul_le_iff_le_div hn', ← natCast_mul, Nat.cast_le, mul_comm]

Premises used: Ordinal.natCast_mul, mul_comm, Ordinal.mul_le_iff_le_div, Nat.cast_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m n : ℕ
hn : n ≠ 0
hn' : Ne.{u_4 + 2} (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 0
⊢ m / n * n ≤ m

Tactic:
apply Nat.div_mul_le_self

Premises used: Nat.div_mul_le_self
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m n : ℕ
hn : n ≠ 0
hn' : Ne.{u_4 + 2} (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 0
inr : m / n < (m / n).succ
⊢ HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) ≤ (↑(m / n) : Ordinal.{u_4})

Tactic:
rw [div_le hn', succ_eq_add_one, ← Nat.cast_succ, ← natCast_mul, Nat.cast_lt, mul_comm,
        ← Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero hn)]

Premises used: Nat.cast_succ, Order.succ_eq_add_one, Ordinal.div_le, Nat.div_lt_iff_lt_mul, Ordinal.natCast_mul, Nat.pos_of_ne_zero, mul_comm, Nat.cast_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
m n : ℕ
hn : n ≠ 0
hn' : Ne.{u_4 + 2} (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 0
⊢ m / n < (m / n).succ

Tactic:
apply Nat.lt_succ_self

Premises used: Nat.lt_succ_self