awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
inl : ∀ (b0 : LT.lt.{u_4 + 1} (α := Ordinal.{u_4}) 0 0), IsSuccLimit (a * 0)
inr : ∀ (b : Ordinal.{u_4}) (b0 : 0 < succ b), IsSuccLimit (a * succ b)
inr₁ : ∀ (lb : IsSuccLimit b), IsSuccLimit (a * b)
⊢ IsSuccLimit (a * b)

Tactic:
rcases zero_or_succ_or_isSuccLimit b with (rfl | ⟨b, rfl⟩ | lb)

Premises used: Ordinal.zero_or_succ_or_isSuccLimit, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
l : IsSuccLimit a
b0 : LT.lt.{u_4 + 1} (α := Ordinal.{u_4}) 0 0
⊢ IsSuccLimit (a * 0)

Tactic:
b0.false.elim

Premises used: False.elim, LT.lt.false
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
l : IsSuccLimit a
b0 : LT.lt.{u_4 + 1} (α := Ordinal.{u_4}) 0 0
⊢ IsSuccLimit (a * 0)

Tactic:
exact b0.false.elim

Premises used: False.elim, LT.lt.false
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
inr : IsSuccLimit (a * b + a)
⊢ IsSuccLimit (a * succ b)

Tactic:
rw [mul_succ]

Premises used: Ordinal.mul_succ
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ IsSuccLimit (a * b + a)

Tactic:
isSuccLimit_add _ l

Premises used: Ordinal.isSuccLimit_add
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ IsSuccLimit (a * b + a)

Tactic:
exact isSuccLimit_add _ l

Premises used: Ordinal.isSuccLimit_add
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
lb : IsSuccLimit b
⊢ IsSuccLimit (a * b)

Tactic:
isSuccLimit_mul_right l.bot_lt lb

Premises used: Ordinal.isSuccLimit_mul_right, Order.IsSuccLimit.bot_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
l : IsSuccLimit a
b0 : 0 < b
lb : IsSuccLimit b
⊢ IsSuccLimit (a * b)

Tactic:
exact isSuccLimit_mul_right l.bot_lt lb

Premises used: Ordinal.isSuccLimit_mul_right, Order.IsSuccLimit.bot_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ha : IsSuccLimit a
inl : IsSuccPrelimit (a * 0)
inr : ∀ (hb : 0 < b), IsSuccPrelimit (a * b)
⊢ IsSuccPrelimit (a * b)

Tactic:
obtain rfl | hb := eq_zero_or_pos b

Premises used: eq_zero_or_pos, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
ha : IsSuccLimit a
inl : IsSuccPrelimit.{u_4 + 1} (α := Ordinal.{u_4}) 0
⊢ IsSuccPrelimit (a * 0)

Tactic:
rw [mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit.{u_4 + 1} (α := Ordinal.{u_4}) 0

Tactic:
isSuccPrelimit_zero

Premises used: Ordinal.isSuccPrelimit_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
ha : IsSuccLimit a
⊢ IsSuccPrelimit.{u_4 + 1} (α := Ordinal.{u_4}) 0

Tactic:
exact isSuccPrelimit_zero

Premises used: Ordinal.isSuccPrelimit_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ha : IsSuccLimit a
hb : 0 < b
⊢ IsSuccPrelimit (a * b)

Tactic:
(isSuccLimit_mul_left ha hb).isSuccPrelimit

Premises used: Order.IsSuccLimit.isSuccPrelimit, Ordinal.isSuccLimit_mul_left
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ha : IsSuccLimit a
hb : 0 < b
⊢ IsSuccPrelimit (a * b)

Tactic:
exact (isSuccLimit_mul_left ha hb).isSuccPrelimit

Premises used: Order.IsSuccLimit.isSuccPrelimit, Ordinal.isSuccLimit_mul_left
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
rw : 0 = a * (↑0 : Ordinal.{u_4})
rw₁ : 0 = a * 0
rw₂ rw₃ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) 0 0
⊢ HSMul.hSMul (α := ℕ) 0 a = a * (↑0 : Ordinal.{u_4})

Tactic:
rw [zero_nsmul, Nat.cast_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, zero_nsmul, Nat.cast_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
n : ℕ
a : Ordinal.{u_4}
rw : n • a + a = a * (↑(n + 1) : Ordinal.{u_4})
rw₁ : a * (↑n : Ordinal.{u_4}) + a = a * (↑(n + 1) : Ordinal.{u_4})
rw₂ : a * (↑n : Ordinal.{u_4}) + a = a * HAdd.hAdd (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 1
rw₃ rw₄ : a * (↑n : Ordinal.{u_4}) + a = a * (↑n : Ordinal.{u_4}) + a
⊢ (n + 1) • a = a * (↑(n + 1) : Ordinal.{u_4})

Tactic:
rw [succ_nsmul, nsmul_eq_mul, Nat.cast_add_one, mul_add_one]

Premises used: mul_add_one, Nat.cast_add_one, succ_nsmul
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
c' : Ordinal.{u_4}
h : c' < c
grw : (a + b) * succ c' ≤ a * c
grw₁ : a * succ c' + b ≤ a * c
grw₂ : a * succ c' + (b + a) ≤ a * c
grw₃ : Ordinal.{u_4}
grw₄ : a * succ c' + a ≤ a * c
grw₅ : a * succ (succ c') ≤ a * c
grw₆ grw₇ : a * c ≤ a * c
⊢ (a + b) * c' ≤ a * c

Tactic:
grw [le_succ c', IH _ h, le_self_add (a := b), ba, ← mul_succ, succ_le_of_lt <| l.succ_lt h]

Premises used: Order.succ_le_of_lt, Ordinal.mul_succ, Order.IsSuccLimit.succ_lt, Order.le_succ, le_self_add
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b
grw grw₁ : a * c ≤ a * c
⊢ a * c ≤ (a + b) * c

Tactic:
grw [← le_self_add]

Premises used: le_self_add
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ba : b + a = a
⊢ (a + b) * HAdd.hAdd (α := Ordinal.{u_4}) 0 1 = a * HAdd.hAdd (α := Ordinal.{u_4}) 0 1 + b

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
IH : (a + b) * (c + 1) = a * (c + 1) + b
add_one : (a + b) * (c + 1) + (a + b) = a * (c + 1 + 1) + b
add_one₁ : a * (c + 1) + b + (a + b) = a * (c + 1 + 1) + b
add_one₂ : a * (c + 1) + b + a + b = a * (c + 1 + 1) + b
add_one₃ : a * (c + 1) + (b + a) + b = a * (c + 1 + 1) + b
add_one₄ : a * (c + 1) + a + b = a * (c + 1 + 1) + b
add_one₅ add_one₆ : a * (c + 1 + 1) + b = a * (c + 1 + 1) + b
⊢ (a + b) * (c + 1 + 1) = a * (c + 1 + 1) + b

Tactic:
rw [mul_add_one, IH, ← add_assoc, add_assoc _ b, ba, ← mul_add_one]

Premises used: add_assoc, mul_add_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
l : IsSuccLimit c
IH : ∀ o' < c, (a + b) * (o' + 1) = a * (o' + 1) + b
limit : (a + b) * c + (a + b) = a * (c + 1) + b
limit₁ : a * c + (a + b) = a * (c + 1) + b
limit₂ : a * c + (a + b) = a * c + a + b
limit₃ limit₄ : a * c + (a + b) = a * c + (a + b)
⊢ (a + b) * (c + 1) = a * (c + 1) + b

Tactic:
rw [mul_add_one, add_mul_limit_aux ba l IH, mul_add_one, add_assoc]

Premises used: _private.0.Ordinal.add_mul_limit_aux, add_assoc, mul_add_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
ba : b + a = a
zero : (a + b) * HAdd.hAdd (α := Ordinal.{u_4}) 0 1 = a * HAdd.hAdd (α := Ordinal.{u_4}) 0 1 + b
add_one : ∀ (c : Ordinal.{u_4}) (IH : (a + b) * (c + 1) = a * (c + 1) + b), (a + b) * (c + 1 + 1) = a * (c + 1 + 1) + b
limit :
  ∀ (c : Ordinal.{u_4}) (l : IsSuccLimit c) (IH : ∀ o' < c, (a + b) * (o' + 1) = a * (o' + 1) + b),
    (a + b) * (c + 1) = a * (c + 1) + b
⊢ (a + b) * (c + 1) = a * (c + 1) + b

Tactic:
induction c using limitRecOn with
  | zero => simp
  | add_one c IH => rw [mul_add_one, IH, ← add_assoc, add_assoc _ b, ba, ← mul_add_one]
  | limit c l IH => rw [mul_add_one, add_mul_limit_aux ba l IH, mul_add_one, add_assoc]

Premises used: add_assoc, Ordinal.zero, mul_add_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
ba : b + a = a
⊢ (a + b) * succ c = a * succ c + b

Tactic:
add_mul_add_one c ba

Premises used: Order.succ, Ordinal.add_mul_add_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
ba : b + a = a
l : IsSuccLimit c
⊢ (a + b) * c = a * c

Tactic:
add_mul_limit_aux ba l fun c' _ => add_mul_succ c' ba

Premises used: _private.0.Ordinal.add_mul_limit_aux, Ordinal.add_mul_succ
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
o : Ordinal.{u_4}
rw : o * HAdd.hAdd (α := Ordinal.{u_4}) 1 1 = o + o
rw₁ : o * 1 + o * 1 = o + o
rw₂ rw₃ : o + o = o + o
⊢ o * 2 = o + o

Tactic:
rw [← one_add_one_eq_two, mul_add, mul_one]

Premises used: one_add_one_eq_two, mul_add, mul_one
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
⊢ Eq (α := Ordinal.{u_4}) (sSup ((fun (x : Ordinal.{u_4}) ↦ 0 * x) ⁻¹' Iic a)) 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ Membership.mem (γ := Set Ordinal.{u_4}) ((fun (x : Ordinal.{u_4}) ↦ a * x) ⁻¹' Iic c) 0

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
ha : a ≠ 0
⊢ a * b ≤ c ↔ b ≤ c / a

Tactic:
(mul_div_gc ha).le_iff_le

Premises used: Ordinal.mul_div_gc, GaloisConnection.le_iff_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
ha : a ≠ 0
⊢ c < a * b ↔ c / a < b

Tactic:
(mul_div_gc ha).lt_iff_lt

Premises used: Ordinal.mul_div_gc, GaloisConnection.lt_iff_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : b ≠ 0
rw : a / b < succ (a / b)
rw₁ rw₂ : a / b ≤ a / b
⊢ a < b * succ (a / b)

Tactic:
rw [lt_mul_iff_div_lt h, lt_succ_iff]

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

Tactic:
simpa only [mul_succ] using lt_mul_succ_div a h

Premises used: Ordinal.lt_mul_succ_div, Ordinal.mul_succ
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
b0 : b ≠ 0
rw : a / b < succ c ↔ a < b * succ c
rw₁ rw₂ : a < b * succ c ↔ a < b * succ c
⊢ a / b ≤ c ↔ a < b * succ c

Tactic:
rw [← lt_succ_iff, ← lt_mul_iff_div_lt b0]

Premises used: Ordinal.lt_mul_iff_div_lt, Order.lt_succ_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : c ≠ 0
rw : ¬b / c ≤ a ↔ c * succ a ≤ b
rw₁ : ¬b < c * succ a ↔ c * succ a ≤ b
rw₂ rw₃ : c * succ a ≤ b ↔ c * succ a ≤ b
⊢ a < b / c ↔ c * succ a ≤ b

Tactic:
rw [← not_le, div_le h, not_lt]

Premises used: not_le, Ordinal.div_le, not_lt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
b c : Ordinal.{u_4}
h : c ≠ 0
⊢ 0 < b / c ↔ c ≤ b

Tactic:
simp [lt_div h]

Premises used: Ordinal.lt_div
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
c0 : c ≠ 0
⊢ a ≤ b / c ↔ c * a ≤ b

Tactic:
(mul_le_iff_le_div c0).symm

Premises used: Ordinal.mul_le_iff_le_div, Iff.symm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
b0 : b ≠ 0
⊢ a / b < c ↔ a < b * c

Tactic:
(lt_mul_iff_div_lt b0).symm

Premises used: Ordinal.lt_mul_iff_div_lt, Iff.symm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : a ≤ b * c
inl : ∀ (h : a ≤ 0 * c), a / 0 ≤ c
inr : ∀ (b0 : b ≠ 0), a / b ≤ c
⊢ a / b ≤ c

Tactic:
obtain rfl | b0 := eq_or_ne b 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
h : a ≤ 0 * c
⊢ a / 0 ≤ c

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

Tactic:
(div_le b0).2 <| h.trans_lt <| mul_lt_mul_of_pos_left (lt_succ c) (pos_iff_ne_zero.2 b0)

Premises used: Iff.mpr, Ordinal.div_le, mul_lt_mul_of_pos_left, Order.lt_succ, LE.le.trans_lt, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
h : a ≤ b * c
b0 : b ≠ 0
⊢ a / b ≤ c

Tactic:
exact (div_le b0).2 <| h.trans_lt <| mul_lt_mul_of_pos_left (lt_succ c) (pos_iff_ne_zero.2 b0)

Premises used: Iff.mpr, Ordinal.div_le, mul_lt_mul_of_pos_left, Order.lt_succ, LE.le.trans_lt, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
⊢ a < b / c → c * a < b

Tactic:
lt_imp_lt_of_le_imp_le div_le_of_le_mul

Premises used: Ordinal.div_le_of_le_mul, lt_imp_lt_of_le_imp_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
⊢ 0 / a = 0

Tactic:
nonpos_iff_eq_zero.1 <| div_le_of_le_mul zero_le

Premises used: zero_le, Ordinal.div_le_of_le_mul, Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
b0 : b = 0
⊢ b * (a / b) ≤ a

Tactic:
simp [b0]
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
inl : a / 0 ≤ b / 0
inr : ∀ (hc : c ≠ 0), a / c ≤ b / c
⊢ a / c ≤ b / c

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : a ≤ b
inl : 0 ≤ b / 0
inl₁ inl₂ : LE.le.{u_4 + 1} (α := Ordinal.{u_4}) 0 0
⊢ a / 0 ≤ b / 0

Tactic:
rw [div_zero, div_zero]

Premises used: Ordinal.div_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
inr : c * (a / c) ≤ b
⊢ a / c ≤ b / c

Tactic:
rw [← mul_le_iff_le_div hc]

Premises used: Ordinal.mul_le_iff_le_div
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ c * (a / c) ≤ b

Tactic:
(mul_div_le a c).trans h

Premises used: LE.le.trans, Ordinal.mul_div_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ c * (a / c) ≤ b

Tactic:
exact (mul_div_le a c).trans h

Premises used: LE.le.trans, Ordinal.mul_div_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
a₁ : (b * a + c) / b ≤ a + c / b
a₂ : a + c / b ≤ (b * a + c) / b
⊢ (b * a + c) / b = a + c / b

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
a₁ : b * a + c < b * succ (a + c / b)
⊢ (b * a + c) / b ≤ a + c / b

Tactic:
apply (div_le b0).2

Premises used: Iff.mpr, Ordinal.div_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
a₁ : c < b * (c / b) + b
⊢ b * a + c < b * succ (a + c / b)

Tactic:
rw [mul_succ, mul_add, add_assoc, add_lt_add_iff_left]

Premises used: add_assoc, Ordinal.mul_succ, mul_add, add_lt_add_iff_left
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ c < b * (c / b) + b

Tactic:
apply lt_mul_div_add _ b0

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

Tactic:
rw [← mul_le_iff_le_div b0, mul_add, add_le_add_iff_left]

Premises used: add_le_add_iff_left, mul_add, Ordinal.mul_le_iff_le_div
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * (c / b) ≤ c

Tactic:
apply mul_div_le

Premises used: Ordinal.mul_div_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : a < b
rw : a < b * succ 0
⊢ a / b = 0

Tactic:
rw [← nonpos_iff_eq_zero, div_le h.ne_bot]

Premises used: Ordinal.div_le, LT.lt.ne_bot, nonpos_iff_eq_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
h : a < b
⊢ a < b * succ 0

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
b0 : b ≠ 0
⊢ b * a / b = a

Tactic:
simpa using mul_add_div a b0 0

Premises used: Ordinal.mul_add_div, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
inl : (a * b + c) / (a * 0) = b / 0
inr : ∀ (hd : d ≠ 0), (a * b + c) / (a * d) = b / d
⊢ (a * b + c) / (a * d) = b / d

Tactic:
obtain rfl | hd := eq_or_ne d 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hc : c < a
b : Ordinal.{u_4}
inl : (a * b + c) / 0 = b / 0
inl₁ : 0 = b / 0
inl₂ inl₃ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) 0 0
⊢ (a * b + c) / (a * 0) = b / 0

Tactic:
rw [mul_zero, div_zero, div_zero]

Premises used: MulZeroClass.mul_zero, Ordinal.div_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
⊢ a * d ≠ 0

Tactic:
have H := mul_ne_zero hc.ne_zero hd
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
inr : (a * b + c) / (a * d) ≤ b / d
inr₁ : b / d ≤ (a * b + c) / (a * d)
⊢ (a * b + c) / (a * d) = b / d

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
inr : a * b + c < a * (d * succ (b / d))
⊢ (a * b + c) / (a * d) ≤ b / d

Tactic:
rw [← lt_succ_iff, ← lt_mul_iff_div_lt H, mul_assoc]

Premises used: Ordinal.lt_mul_iff_div_lt, mul_assoc, Order.lt_succ_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
inr : a * b + a ≤ a * (d * succ (b / d))
⊢ a * b + c < a * (d * succ (b / d))

Tactic:
apply (add_lt_add_right hc _).trans_le

Premises used: add_lt_add_right, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
inr : a * succ b ≤ a * (d * succ (b / d))
⊢ a * b + a ≤ a * (d * succ (b / d))

Tactic:
rw [← mul_succ]

Premises used: Ordinal.mul_succ
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
inr : succ b ≤ d * succ (b / d)
⊢ a * succ b ≤ a * (d * succ (b / d))

Tactic:
gcongr
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
inr : b < d * succ (b / d)
⊢ succ b ≤ d * succ (b / d)

Tactic:
rw [succ_le_iff]

Premises used: Order.succ_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ b < d * succ (b / d)

Tactic:
lt_mul_succ_div b hd

Premises used: Ordinal.lt_mul_succ_div
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ b < d * succ (b / d)

Tactic:
exact lt_mul_succ_div b hd

Premises used: Ordinal.lt_mul_succ_div
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
inr : a * d * (b / d) ≤ a * b + c
inr₁ : a * (d * (b / d)) ≤ a * b + c
inr₂ : a * b ≤ a * b + c
inr₃ inr₄ : a * b ≤ a * b
⊢ b / d ≤ (a * b + c) / (a * d)

Tactic:
grw [← mul_le_iff_le_div H, mul_assoc, mul_div_le b d, ← le_self_add]

Premises used: mul_assoc, Ordinal.mul_le_iff_le_div, le_self_add, Ordinal.mul_div_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ (a * b + 0) / (a * c) = b / c

Tactic:
mul_add_div_mul (pos_iff_ne_zero.2 ha) b c

Premises used: Iff.mpr, Ordinal.mul_add_div_mul, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
h : a * b / (a * c) = (a * b + 0) / (a * c)
⊢ a * b / (a * c) = b / c

Tactic:
convert! mul_add_div_mul (pos_iff_ne_zero.2 ha) b c using 1

Premises used: Iff.mpr, Ordinal.mul_add_div_mul, pos_iff_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
h h₁ : a * b / (a * c) = a * b / (a * c)
⊢ a * b / (a * c) = (a * b + 0) / (a * c)

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hle : b * c ≤ a
hlt : a < b * (c + 1)
inl : ∀ (hle : 0 * c ≤ a) (hlt : a < 0 * (c + 1)), a / 0 = c
inr : ∀ (hb : b ≠ 0), a / b = c
⊢ a / b = c

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hle : 0 * c ≤ a
hlt : a < 0 * (c + 1)
⊢ a / 0 = c

Tactic:
simp at hlt
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hle : b * c ≤ a
hlt : a < b * (c + 1)
hb : b ≠ 0
⊢ a / b = c

Tactic:
le_antisymm (div_le hb |>.mpr hlt) (mul_le_iff_le_div hb |>.mp hle)

Premises used: Iff.mpr, Ordinal.div_le, le_antisymm, Iff.mp, Ordinal.mul_le_iff_le_div
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hle : b * c ≤ a
hlt : a < b * (c + 1)
hb : b ≠ 0
⊢ a / b = c

Tactic:
exact le_antisymm (div_le hb |>.mpr hlt) (mul_le_iff_le_div hb |>.mp hle)

Premises used: Iff.mpr, Ordinal.div_le, le_antisymm, Iff.mp, Ordinal.mul_le_iff_le_div
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hb : b ≠ 0
⊢ a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1)

Tactic:
⟨fun h ↦ h ▸ ⟨mul_div_le a b, lt_mul_succ_div a hb⟩, fun ⟨hle, hlt⟩ ↦ div_eq hle hlt⟩

Premises used: Ordinal.lt_mul_succ_div, Ordinal.div_eq, _private.0.Ordinal.div_eq_iff.match_1, Eq.rec, HDiv.hDiv, And.intro, Iff.intro, Eq, Ordinal.mul_div_le
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hc : c ≠ 0
inl : a / 0 = c ↔ 0 * c ≤ a ∧ a < 0 * (c + 1)
inr : ∀ (hb : b ≠ 0), a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1)
⊢ a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1)

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

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / 0 = c ↔ 0 * c ≤ a ∧ a < 0 * (c + 1)

Tactic:
simp [hc.symm]

Premises used: Ne.symm
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hc : c ≠ 0
hb : b ≠ 0
⊢ a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1)

Tactic:
div_eq_iff hb

Premises used: Ordinal.div_eq_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
hc : c ≠ 0
hb : b ≠ 0
⊢ a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1)

Tactic:
exact div_eq_iff hb

Premises used: Ordinal.div_eq_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b : Ordinal.{u_4}
rw : b * 1 ≤ a ∧ a < b * HAdd.hAdd (α := Ordinal.{u_4}) 1 1 ↔ b ≤ a ∧ a < b * 2
rw₁ : b ≤ a ∧ a < b * HAdd.hAdd (α := Ordinal.{u_4}) 1 1 ↔ b ≤ a ∧ a < b * 2
rw₂ rw₃ : b ≤ a ∧ a < b * 2 ↔ b ≤ a ∧ a < b * 2
⊢ a / b = 1 ↔ b ≤ a ∧ a < b * 2

Tactic:
rw [div_eq_iff' one_ne_zero, mul_one, one_add_one_eq_two]

Premises used: one_add_one_eq_two, Ordinal.div_eq_iff', mul_one, one_ne_zero
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
⊢ a / 1 = a

Tactic:
simpa only [one_mul] using mul_div_cancel a one_ne_zero

Premises used: Ordinal.mul_div_cancel, one_ne_zero, one_mul
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a : Ordinal.{u_4}
h : a ≠ 0
⊢ a / a = 1

Tactic:
simpa only [mul_one] using mul_div_cancel 1 h

Premises used: Ordinal.mul_div_cancel, mul_one, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
inl : 0 * (b - c) = 0 * b - 0 * c
inr : ∀ (ha : a ≠ 0), a * (b - c) = a * b - a * c
⊢ a * (b - c) = a * b - a * c

Tactic:
obtain rfl | ha := eq_or_ne a 0

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

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
ha : a ≠ 0
⊢ a * (b - c) = a * b - a * c

Tactic:
eq_of_forall_ge_iff fun d ↦ ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
Goal:
a b c : Ordinal.{u_4}
ha : a ≠ 0
inr : ∀ (d : Ordinal.{u_4}), a * (b - c) ≤ d ↔ a * b - a * c ≤ d
⊢ a * (b - c) = a * b - a * c

Tactic:
refine eq_of_forall_ge_iff fun d ↦ ?_

Premises used: eq_of_forall_ge_iff
-- Module: Mathlib.SetTheory.Ordinal.Arithmetic
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
inr₄ inr₅ : b ≤ c + d / a ↔ b ≤ c + d / a
⊢ 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]

Premises used: Ordinal.mul_add_div, Ordinal.sub_le, Ordinal.mul_le_iff_le_div