awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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})
⊢ (n + 1) • a = a * (↑(n + 1) : Ordinal.{u_4})
have rw₂ : a * (↑n : Ordinal.{u_4}) + a = a * HAdd.hAdd (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 1
Tactic: rw [succ_nsmul, nsmul_eq_mul, Nat.cast_add_one, mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (n + 1) • a = a * (↑(n + 1) : Ordinal.{u_4})
have rw₃ : a * (↑n : Ordinal.{u_4}) + a = a * (↑n : Ordinal.{u_4}) + a
Tactic: rw [succ_nsmul, nsmul_eq_mul, Nat.cast_add_one, mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * c' ≤ a * c
have grw : (a + b) * succ 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]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * c' ≤ a * c
have grw₁ : a * succ c' + b ≤ 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]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * c' ≤ a * c
have grw₂ : a * succ c' + (b + a) ≤ 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]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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}
⊢ (a + b) * c' ≤ a * c
have grw₄ : a * succ c' + a ≤ 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]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * c' ≤ a * c
have grw₅ : a * succ (succ 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]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * c' ≤ a * c
have grw₆ : a * 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]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ a * c ≤ (a + b) * c
have grw : a * c ≤ a * c
Tactic: grw [← le_self_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
ba : b + a = a
c : Ordinal.{u_4}
IH : (a + b) * (c + 1) = a * (c + 1) + b
⊢ (a + b) * (c + 1 + 1) = a * (c + 1 + 1) + b
have add_one : (a + b) * (c + 1) + (a + b) = a * (c + 1 + 1) + b
Tactic: rw [mul_add_one, IH, ← add_assoc, add_assoc _ b, ba, ← mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * (c + 1 + 1) = a * (c + 1 + 1) + b
have add_one₁ : a * (c + 1) + b + (a + b) = a * (c + 1 + 1) + b
Tactic: rw [mul_add_one, IH, ← add_assoc, add_assoc _ b, ba, ← mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * (c + 1 + 1) = a * (c + 1 + 1) + b
have add_one₂ : a * (c + 1) + b + a + b = a * (c + 1 + 1) + b
Tactic: rw [mul_add_one, IH, ← add_assoc, add_assoc _ b, ba, ← mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * (c + 1 + 1) = a * (c + 1 + 1) + b
have add_one₃ : a * (c + 1) + (b + a) + b = a * (c + 1 + 1) + b
Tactic: rw [mul_add_one, IH, ← add_assoc, add_assoc _ b, ba, ← mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * (c + 1 + 1) = a * (c + 1 + 1) + b
have add_one₄ : a * (c + 1) + a + b = a * (c + 1 + 1) + b
Tactic: rw [mul_add_one, IH, ← add_assoc, add_assoc _ b, ba, ← mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * (c + 1 + 1) = a * (c + 1 + 1) + b
have add_one₅ : a * (c + 1 + 1) + b = a * (c + 1 + 1) + b
Tactic: rw [mul_add_one, IH, ← add_assoc, add_assoc _ b, ba, ← mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * (c + 1) = a * (c + 1) + b
have limit : (a + b) * c + (a + b) = a * (c + 1) + b
Tactic: rw [mul_add_one, add_mul_limit_aux ba l IH, mul_add_one, add_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * (c + 1) = a * (c + 1) + b
have limit₁ : a * c + (a + b) = a * (c + 1) + b
Tactic: rw [mul_add_one, add_mul_limit_aux ba l IH, mul_add_one, add_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * (c + 1) = a * (c + 1) + b
have limit₂ : a * c + (a + b) = a * c + a + b
Tactic: rw [mul_add_one, add_mul_limit_aux ba l IH, mul_add_one, add_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * (c + 1) = a * (c + 1) + b
have limit₃ : a * c + (a + b) = a * c + (a + b)
Tactic: rw [mul_add_one, add_mul_limit_aux ba l IH, mul_add_one, add_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
ba : b + a = a
⊢ (a + b) * (c + 1) = a * (c + 1) + b
have zero : (a + b) * HAdd.hAdd (α := Ordinal.{u_4}) 0 1 = a * HAdd.hAdd (α := Ordinal.{u_4}) 0 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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * (c + 1) = a * (c + 1) + b
have 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
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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a + b) * (c + 1) = a * (c + 1) + b
have 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
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]
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
⊢ o * 2 = o + o
have rw : o * HAdd.hAdd (α := Ordinal.{u_4}) 1 1 = o + o
Tactic: rw [← one_add_one_eq_two, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
rw : o * HAdd.hAdd (α := Ordinal.{u_4}) 1 1 = o + o
⊢ o * 2 = o + o
have rw₁ : o * 1 + o * 1 = o + o
Tactic: rw [← one_add_one_eq_two, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
rw : o * HAdd.hAdd (α := Ordinal.{u_4}) 1 1 = o + o
rw₁ : o * 1 + o * 1 = o + o
⊢ o * 2 = o + o
have rw₂ : o + o = o + o
Tactic: rw [← one_add_one_eq_two, mul_add, mul_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : b ≠ 0
⊢ a < b * succ (a / b)
have rw : a / b < succ (a / b)
Tactic: rw [lt_mul_iff_div_lt h, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : b ≠ 0
rw : a / b < succ (a / b)
⊢ a < b * succ (a / b)
have rw₁ : a / b ≤ a / b
Tactic: rw [lt_mul_iff_div_lt h, lt_succ_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
b0 : b ≠ 0
⊢ a / b ≤ c ↔ a < b * succ c
have rw : a / b < succ c ↔ a < b * succ c
Tactic: rw [← lt_succ_iff, ← lt_mul_iff_div_lt b0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
b0 : b ≠ 0
rw : a / b < succ c ↔ a < b * succ c
⊢ a / b ≤ c ↔ a < b * succ c
have rw₁ : a < b * succ c ↔ a < b * succ c
Tactic: rw [← lt_succ_iff, ← lt_mul_iff_div_lt b0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : c ≠ 0
⊢ a < b / c ↔ c * succ a ≤ b
have rw : ¬b / c ≤ a ↔ c * succ a ≤ b
Tactic: rw [← not_le, div_le h, not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : c ≠ 0
rw : ¬b / c ≤ a ↔ c * succ a ≤ b
⊢ a < b / c ↔ c * succ a ≤ b
have rw₁ : ¬b < c * succ a ↔ c * succ a ≤ b
Tactic: rw [← not_le, div_le h, not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ a < b / c ↔ c * succ a ≤ b
have rw₂ : c * succ a ≤ b ↔ c * succ a ≤ b
Tactic: rw [← not_le, div_le h, not_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : a ≤ b * c
⊢ a / b ≤ c
have inl : ∀ (h : a ≤ 0 * c), a / 0 ≤ c
Tactic: obtain rfl | b0 := eq_or_ne b 0
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
h : a ≤ b * c
inl : ∀ (h : a ≤ 0 * c), a / 0 ≤ c
⊢ a / b ≤ c
have inr : ∀ (b0 : b ≠ 0), a / b ≤ c
Tactic: obtain rfl | b0 := eq_or_ne b 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
⊢ a / c ≤ b / c
have inl : a / 0 ≤ b / 0
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
inl : a / 0 ≤ b / 0
⊢ a / c ≤ b / c
have inr : ∀ (hc : c ≠ 0), a / c ≤ b / c
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : a ≤ b
⊢ a / 0 ≤ b / 0
have inl : 0 ≤ b / 0
Tactic: rw [div_zero, div_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : a ≤ b
inl : 0 ≤ b / 0
⊢ a / 0 ≤ b / 0
have inl₁ : LE.le.{u_4 + 1} (α := Ordinal.{u_4}) 0 0
Tactic: rw [div_zero, div_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : a ≤ b
c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / c ≤ b / c
have inr : c * (a / c) ≤ b
Tactic: rw [← mul_le_iff_le_div hc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ (b * a + c) / b = a + c / b
have a₁ : (b * a + c) / b ≤ a + c / b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
a₁ : (b * a + c) / b ≤ a + c / b
⊢ (b * a + c) / b = a + c / b
have a₂ : a + c / b ≤ (b * a + c) / b
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ (b * a + c) / b ≤ a + c / b
have a₁ : b * a + c < b * succ (a + c / b)
Tactic: apply (div_le b0).2
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ b * a + c < b * succ (a + c / b)
have a₁ : c < b * (c / b) + b
Tactic: rw [mul_succ, mul_add, add_assoc, add_lt_add_iff_left]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
b0 : b ≠ 0
c : Ordinal.{u_4}
⊢ a + c / b ≤ (b * a + c) / b
have a₁ : b * (c / b) ≤ c
Tactic: rw [← mul_le_iff_le_div b0, mul_add, add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
h : a < b
⊢ a / b = 0
have rw : a < b * succ 0
Tactic: rw [← nonpos_iff_eq_zero, div_le h.ne_bot]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
⊢ (a * b + c) / (a * d) = b / d
have inl : (a * b + c) / (a * 0) = b / 0
Tactic: obtain rfl | hd := eq_or_ne d 0
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
inl : (a * b + c) / (a * 0) = b / 0
⊢ (a * b + c) / (a * d) = b / d
have inr : ∀ (hd : d ≠ 0), (a * b + c) / (a * d) = b / d
Tactic: obtain rfl | hd := eq_or_ne d 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c : Ordinal.{u_4}
hc : c < a
b : Ordinal.{u_4}
⊢ (a * b + c) / (a * 0) = b / 0
have inl : (a * b + c) / 0 = b / 0
Tactic: rw [mul_zero, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c : Ordinal.{u_4}
hc : c < a
b : Ordinal.{u_4}
inl : (a * b + c) / 0 = b / 0
⊢ (a * b + c) / (a * 0) = b / 0
have inl₁ : 0 = b / 0
Tactic: rw [mul_zero, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c : Ordinal.{u_4}
hc : c < a
b : Ordinal.{u_4}
inl : (a * b + c) / 0 = b / 0
inl₁ : 0 = b / 0
⊢ (a * b + c) / (a * 0) = b / 0
have inl₂ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) 0 0
Tactic: rw [mul_zero, div_zero, div_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (hypothesis)
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
⊢ (a * b + c) / (a * d) = b / d
have H : a * d ≠ 0
Tactic: have H := mul_ne_zero hc.ne_zero hd
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ (a * b + c) / (a * d) = b / d
have inr : (a * b + c) / (a * d) ≤ b / d
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (a * b + c) / (a * d) = b / d
have inr₁ : b / d ≤ (a * b + c) / (a * d)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ (a * b + c) / (a * d) ≤ b / d
have inr : a * b + c < a * (d * succ (b / d))
Tactic: rw [← lt_succ_iff, ← lt_mul_iff_div_lt H, mul_assoc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + c < a * (d * succ (b / d))
have inr : a * b + a ≤ a * (d * succ (b / d))
Tactic: apply (add_lt_add_right hc _).trans_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * b + a ≤ a * (d * succ (b / d))
have inr : a * succ b ≤ a * (d * succ (b / d))
Tactic: rw [← mul_succ]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ a * succ b ≤ a * (d * succ (b / d))
have inr : succ b ≤ d * succ (b / d)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ succ b ≤ d * succ (b / d)
have inr : b < d * succ (b / d)
Tactic: rw [succ_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a c : Ordinal.{u_4}
hc : c < a
b d : Ordinal.{u_4}
hd : d ≠ 0
H : a * d ≠ 0
⊢ b / d ≤ (a * b + c) / (a * d)
have inr : a * d * (b / d) ≤ a * b + c
Tactic: grw [← mul_le_iff_le_div H, mul_assoc, mul_div_le b d, ← le_self_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ b / d ≤ (a * b + c) / (a * d)
have inr₁ : a * (d * (b / d)) ≤ a * b + c
Tactic: grw [← mul_le_iff_le_div H, mul_assoc, mul_div_le b d, ← le_self_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ b / d ≤ (a * b + c) / (a * d)
have inr₂ : a * b ≤ a * b + c
Tactic: grw [← mul_le_iff_le_div H, mul_assoc, mul_div_le b d, ← le_self_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ b / d ≤ (a * b + c) / (a * d)
have inr₃ : a * b ≤ a * b
Tactic: grw [← mul_le_iff_le_div H, mul_assoc, mul_div_le b d, ← le_self_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ a * b / (a * c) = b / c
have h : a * b / (a * c) = (a * b + 0) / (a * c)
Tactic: convert! mul_add_div_mul (pos_iff_ne_zero.2 ha) b c using 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ a * b / (a * c) = (a * b + 0) / (a * c)
have h : a * b / (a * c) = a * b / (a * c)
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
hle : b * c ≤ a
hlt : a < b * (c + 1)
⊢ a / b = c
have inl : ∀ (hle : 0 * c ≤ a) (hlt : a < 0 * (c + 1)), a / 0 = c
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
Cleared hypotheses: b, hle, hlt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ a / b = c
have inr : ∀ (hb : b ≠ 0), a / b = c
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
hc : c ≠ 0
⊢ a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1)
have inl : a / 0 = c ↔ 0 * c ≤ a ∧ a < 0 * (c + 1)
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
hc : c ≠ 0
inl : a / 0 = c ↔ 0 * c ≤ a ∧ a < 0 * (c + 1)
⊢ a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1)
have inr : ∀ (hb : b ≠ 0), a / b = c ↔ b * c ≤ a ∧ a < b * (c + 1)
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
⊢ a / b = 1 ↔ b ≤ a ∧ a < b * 2
have rw : b * 1 ≤ a ∧ a < b * HAdd.hAdd (α := Ordinal.{u_4}) 1 1 ↔ b ≤ a ∧ a < b * 2
Tactic: rw [div_eq_iff' one_ne_zero, mul_one, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b : Ordinal.{u_4}
rw : b * 1 ≤ a ∧ a < b * HAdd.hAdd (α := Ordinal.{u_4}) 1 1 ↔ b ≤ a ∧ a < b * 2
⊢ a / b = 1 ↔ b ≤ a ∧ a < b * 2
have rw₁ : b ≤ a ∧ a < b * HAdd.hAdd (α := Ordinal.{u_4}) 1 1 ↔ b ≤ a ∧ a < b * 2
Tactic: rw [div_eq_iff' one_ne_zero, mul_one, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ a / b = 1 ↔ b ≤ a ∧ a < b * 2
have rw₂ : b ≤ a ∧ a < b * 2 ↔ b ≤ a ∧ a < b * 2
Tactic: rw [div_eq_iff' one_ne_zero, mul_one, one_add_one_eq_two]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
⊢ a * (b - c) = a * b - a * c
have inl : 0 * (b - c) = 0 * b - 0 * c
Tactic: obtain rfl | ha := eq_or_ne a 0
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
inl : 0 * (b - c) = 0 * b - 0 * c
⊢ a * (b - c) = a * b - a * c
have inr : ∀ (ha : a ≠ 0), a * (b - c) = a * b - a * c
Tactic: obtain rfl | ha := eq_or_ne a 0
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a b c : Ordinal.{u_4}
ha : a ≠ 0
⊢ a * (b - c) = a * b - a * c
have inr : ∀ (d : Ordinal.{u_4}), a * (b - c) ≤ d ↔ a * b - a * c ≤ d
Tactic: refine eq_of_forall_ge_iff fun d ↦ ?_