awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
h : m ≤ n
⊢ (↑(m - n) : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have inl : (↑0 : 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]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
h : m ≤ n
inl : (↑0 : 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 inl₁ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑0 : Ordinal.{u_4}) 0
Tactic: rw [tsub_eq_zero_iff_le.2 h, Ordinal.sub_eq_zero_iff_le.2 (Nat.cast_le.2 h), Nat.cast_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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
⊢ (↑(m - n) : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have inl₂ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) 0 0
Tactic: rw [tsub_eq_zero_iff_le.2 h, Ordinal.sub_eq_zero_iff_le.2 (Nat.cast_le.2 h), Nat.cast_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
h : n ≤ m
⊢ (↑(m - n) : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have 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})
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)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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})
⊢ (↑(m - n) : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have inr₁ : (↑(n + (m - n)) : Ordinal.{u_4}) =
  (↑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)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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})
⊢ (↑(m - n) : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have inr₂ : (↑m : Ordinal.{u_4}) = (↑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)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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})
⊢ (↑(m - n) : Ordinal.{u_4}) = HSub.hSub (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have inr₃ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑m : 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)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
⊢ (↑(m / n) : Ordinal.{u_4}) = HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have inl : (↑(m / 0) : Ordinal.{u_4}) = HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑0 : Ordinal.{u_4})
Tactic: rcases eq_or_ne n 0 with (rfl | hn)
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
inl : (↑(m / 0) : Ordinal.{u_4}) = HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑0 : Ordinal.{u_4})
⊢ (↑(m / n) : Ordinal.{u_4}) = HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have inr : ∀ (hn : n ≠ 0), (↑(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)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (hypothesis)
Goal:
m n : ℕ
hn : n ≠ 0
⊢ (↑(m / n) : Ordinal.{u_4}) = HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have hn' : Ne.{u_4 + 2} (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 0
Tactic: have hn' : (n : Ordinal) ≠ 0 := Nat.cast_ne_zero.2 hn
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hn' : Ne.{u_4 + 2} (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 0
⊢ (↑(m / n) : Ordinal.{u_4}) = HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have inr : (↑(m / n) : Ordinal.{u_4}) ≤ HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
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})
⊢ (↑(m / n) : Ordinal.{u_4}) = HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have inr₁ : HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) ≤ (↑(m / n) : Ordinal.{u_4})
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hn' : Ne.{u_4 + 2} (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 0
⊢ (↑(m / n) : Ordinal.{u_4}) ≤ HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have inr : m / n * n ≤ m
Tactic: rw [← mul_le_iff_le_div hn', ← natCast_mul, Nat.cast_le, mul_comm]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
hn : n ≠ 0
hn' : Ne.{u_4 + 2} (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) 0
⊢ HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) ≤ (↑(m / n) : Ordinal.{u_4})
have inr : m / n < (m / n).succ
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)]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
⊢ (↑(m % n) : Ordinal.{u_4}) = HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have rw : (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
    (↑(m % n) : Ordinal.{u_4}) =
  (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
    HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
Tactic: rw [← add_left_cancel_iff, div_add_mod, ← natCast_div, ← natCast_mul, ← Nat.cast_add,
    Nat.div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
rw :
  (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      (↑(m % n) : Ordinal.{u_4}) =
    (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
⊢ (↑(m % n) : Ordinal.{u_4}) = HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have rw₁ : Ordinal.{u_4}
Tactic: rw [← add_left_cancel_iff, div_add_mod, ← natCast_div, ← natCast_mul, ← Nat.cast_add,
    Nat.div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
rw :
  (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      (↑(m % n) : Ordinal.{u_4}) =
    (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
rw₁ : Ordinal.{u_4}
⊢ (↑(m % n) : Ordinal.{u_4}) = HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have rw₂ : (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
    (↑(m % n) : Ordinal.{u_4}) =
  (↑m : Ordinal.{u_4})
Tactic: rw [← add_left_cancel_iff, div_add_mod, ← natCast_div, ← natCast_mul, ← Nat.cast_add,
    Nat.div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
rw :
  (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      (↑(m % n) : Ordinal.{u_4}) =
    (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
rw₁ : Ordinal.{u_4}
rw₂ :
  (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      (↑(m % n) : Ordinal.{u_4}) =
    (↑m : Ordinal.{u_4})
⊢ (↑(m % n) : Ordinal.{u_4}) = HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have rw₃ : HMul.hMul (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑(m / n) : Ordinal.{u_4}) + (↑(m % n) : Ordinal.{u_4}) =
  (↑m : Ordinal.{u_4})
Tactic: rw [← add_left_cancel_iff, div_add_mod, ← natCast_div, ← natCast_mul, ← Nat.cast_add,
    Nat.div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
rw :
  (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      (↑(m % n) : Ordinal.{u_4}) =
    (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
rw₁ : Ordinal.{u_4}
rw₂ :
  (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      (↑(m % n) : Ordinal.{u_4}) =
    (↑m : Ordinal.{u_4})
rw₃ :
  HMul.hMul (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑(m / n) : Ordinal.{u_4}) + (↑(m % n) : Ordinal.{u_4}) =
    (↑m : Ordinal.{u_4})
⊢ (↑(m % n) : Ordinal.{u_4}) = HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have rw₄ : HAdd.hAdd (α := Ordinal.{u_4}) (↑(n * (m / n)) : Ordinal.{u_4}) (↑(m % n) : Ordinal.{u_4}) = (↑m : Ordinal.{u_4})
Tactic: rw [← add_left_cancel_iff, div_add_mod, ← natCast_div, ← natCast_mul, ← Nat.cast_add,
    Nat.div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
rw :
  (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      (↑(m % n) : Ordinal.{u_4}) =
    (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
rw₁ : Ordinal.{u_4}
rw₂ :
  (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      (↑(m % n) : Ordinal.{u_4}) =
    (↑m : Ordinal.{u_4})
rw₃ :
  HMul.hMul (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑(m / n) : Ordinal.{u_4}) + (↑(m % n) : Ordinal.{u_4}) =
    (↑m : Ordinal.{u_4})
rw₄ : HAdd.hAdd (α := Ordinal.{u_4}) (↑(n * (m / n)) : Ordinal.{u_4}) (↑(m % n) : Ordinal.{u_4}) = (↑m : Ordinal.{u_4})
⊢ (↑(m % n) : Ordinal.{u_4}) = HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have rw₅ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑(n * (m / n) + m % n) : Ordinal.{u_4}) (↑m : Ordinal.{u_4})
Tactic: rw [← add_left_cancel_iff, div_add_mod, ← natCast_div, ← natCast_mul, ← Nat.cast_add,
    Nat.div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
m n : ℕ
rw :
  (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      (↑(m % n) : Ordinal.{u_4}) =
    (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
rw₁ : Ordinal.{u_4}
rw₂ :
  (↑n : Ordinal.{u_4}) * HDiv.hDiv (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4}) +
      (↑(m % n) : Ordinal.{u_4}) =
    (↑m : Ordinal.{u_4})
rw₃ :
  HMul.hMul (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑(m / n) : Ordinal.{u_4}) + (↑(m % n) : Ordinal.{u_4}) =
    (↑m : Ordinal.{u_4})
rw₄ : HAdd.hAdd (α := Ordinal.{u_4}) (↑(n * (m / n)) : Ordinal.{u_4}) (↑(m % n) : Ordinal.{u_4}) = (↑m : Ordinal.{u_4})
rw₅ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑(n * (m / n) + m % n) : Ordinal.{u_4}) (↑m : Ordinal.{u_4})
⊢ (↑(m % n) : Ordinal.{u_4}) = HMod.hMod (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑n : Ordinal.{u_4})
have rw₆ : Eq.{u_4 + 2} (α := Ordinal.{u_4}) (↑m : Ordinal.{u_4}) (↑m : Ordinal.{u_4})
Tactic: rw [← add_left_cancel_iff, div_add_mod, ← natCast_div, ← natCast_mul, ← Nat.cast_add,
    Nat.div_add_mod]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x : ℕ
⊢ Eq (α := Ordinal.{0})
    ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{0}) ↦ x1 < x2) (typein LT.lt) :
          (a : ℕ) → Ordinal.{0})
        x :
      Ordinal.{0})
    ((↑x : Ordinal.{0}) : Ordinal.{0})
have have : ∀ (this : Fintype (↑(Iio x) : Type)),
  Eq (α := Ordinal.{0})
    ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{0}) ↦ x1 < x2) (typein LT.lt) :
          (a : ℕ) → Ordinal.{0})
        x :
      Ordinal.{0})
    ((↑x : Ordinal.{0}) : Ordinal.{0})
Tactic: have : Fintype <| Iio x := Nat.fintypeIio x
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x : ℕ
this : Fintype (↑(Iio x) : Type)
⊢ Eq (α := Ordinal.{0})
    ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{0}) ↦ x1 < x2) (typein LT.lt) :
          (a : ℕ) → Ordinal.{0})
        x :
      Ordinal.{0})
    ((↑x : Ordinal.{0}) : Ordinal.{0})
have rw : Fintype.card (↑(Iio x) : Type) = x
Tactic: rw [← type_Iio_lt, type_fintype, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
x : ℕ
this : Fintype (↑(Iio x) : Type)
⊢ Fintype.card (↑(Iio x) : Type) = x
have nth_rw : Fintype.card (↑(Iio x) : Type) = Fintype.card (Fin x)
Tactic: nth_rw 2 [← Fintype.card_fin x]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
n : ℕ
x : Fin n
⊢ Eq (α := Ordinal.{0})
    ((PrincipalSeg.toRelEmbedding (r := LT.lt) (s := fun (x1 x2 : Ordinal.{0}) ↦ x1 < x2) (typein LT.lt) :
          (a : Fin n) → Ordinal.{0})
        x :
      Ordinal.{0})
    ((↑(↑x : ℕ) : Ordinal.{0}) : Ordinal.{0})
have rw : Fintype.card (↑(Iio x) : Type) = (↑x : ℕ)
Tactic: rw [← type_Iio_lt, type_fintype, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
⊢ o < ω ↔ ∃ (n : ℕ), o = (↑n : Ordinal.{u_4})
have simp_rw : o < ℵ₀.ord ↔ ∃ (n : ℕ), o = (↑n : Ordinal.{u_4})
Tactic: simp_rw [← Cardinal.ord_aleph0, Cardinal.lt_ord, lt_aleph0, card_eq_nat]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
simp_rw : o < ℵ₀.ord ↔ ∃ (n : ℕ), o = (↑n : Ordinal.{u_4})
⊢ o < ω ↔ ∃ (n : ℕ), o = (↑n : Ordinal.{u_4})
have simp_rw₁ : o.card < ℵ₀ ↔ ∃ (n : ℕ), o = (↑n : Ordinal.{u_4})
Tactic: simp_rw [← Cardinal.ord_aleph0, Cardinal.lt_ord, lt_aleph0, card_eq_nat]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
simp_rw : o < ℵ₀.ord ↔ ∃ (n : ℕ), o = (↑n : Ordinal.{u_4})
simp_rw₁ : o.card < ℵ₀ ↔ ∃ (n : ℕ), o = (↑n : Ordinal.{u_4})
⊢ o < ω ↔ ∃ (n : ℕ), o = (↑n : Ordinal.{u_4})
have simp_rw₂ : (∃ (n : ℕ), o.card = (↑n : Cardinal.{u_4})) ↔ ∃ (n : ℕ), o = (↑n : Ordinal.{u_4})
Tactic: simp_rw [← Cardinal.ord_aleph0, Cardinal.lt_ord, lt_aleph0, card_eq_nat]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
⊢ (∃ (n : ℕ), o = (↑n : Ordinal.{u_4})) ∨ ω ≤ o
have inl : ∀ (ho : o < ω), (∃ (n : ℕ), o = (↑n : Ordinal.{u_4})) ∨ ω ≤ o
Tactic: obtain ho | ho := lt_or_ge o ω
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
inl : ∀ (ho : o < ω), (∃ (n : ℕ), o = (↑n : Ordinal.{u_4})) ∨ ω ≤ o
⊢ (∃ (n : ℕ), o = (↑n : Ordinal.{u_4})) ∨ ω ≤ o
have inr : ∀ (ho : ω ≤ o), (∃ (n : ℕ), o = (↑n : Ordinal.{u_4})) ∨ ω ≤ o
Tactic: obtain ho | ho := lt_or_ge o ω
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
n : ℕ
⊢ Eq.{u_4 + 2} (α := Set Ordinal.{u_4}) (Nat.cast '' Iio n) (Iio (↑n : Ordinal.{u_4}))
have h : ∀ (o : Ordinal.{u_4}),
  Membership.mem (γ := Set Ordinal.{u_4}) (Nat.cast '' Iio n) o ↔
    Membership.mem (γ := Set Ordinal.{u_4}) (Iio (↑n : Ordinal.{u_4})) o
Tactic: ext o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (hypothesis)
Goal:
n : ℕ
o : Ordinal.{u_4}
⊢ Membership.mem (γ := Set Ordinal.{u_4}) (Nat.cast '' Iio n) o ↔
    Membership.mem (γ := Set Ordinal.{u_4}) (Iio (↑n : Ordinal.{u_4})) o
have this : ∀ {b : ℕ} (h : o ≤ (↑b : Ordinal.{u_4})), ∃ (c : ℕ), o = (↑c : Ordinal.{u_4})
Tactic: have := @eq_natCast_of_le_natCast o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
⊢ IsSuccLimit ω
have rw : ω ≠ 0 ∧ ∀ a < ω, succ a < ω
Tactic: rw [isSuccLimit_iff, isSuccPrelimit_iff_succ_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
⊢ ω ≠ 0 ∧ ∀ a < ω, succ a < ω
have refine : ∀ (o : Ordinal.{u_4}) (h : o < ω), succ o < ω
Tactic: refine ⟨omega0_ne_zero, fun o h => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
h : o < ω
⊢ succ o < ω
have obtain : ∀ (n : ℕ) (h : (↑n : Ordinal.{u_4}) < ω), succ (↑n : Ordinal.{u_4}) < ω
Tactic: obtain ⟨n, rfl⟩ := lt_omega0.1 h
Cleared hypotheses: o, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
H : ∀ (n : ℕ), (↑n : Ordinal.{u_4}) ≤ o
a : Ordinal.{u_4}
h : a < ω
⊢ a < o
have let : ∀ (n : ℕ) (e : a = (↑n : Ordinal.{u_4})), a < o
Tactic: let ⟨n, e⟩ := lt_omega0.1 h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
H : ∀ (n : ℕ), (↑n : Ordinal.{u_4}) ≤ o
a : Ordinal.{u_4}
h : a < ω
n : ℕ
e : a = (↑n : Ordinal.{u_4})
⊢ a < o
have rw : succ (↑n : Ordinal.{u_4}) ≤ o
Tactic: rw [e, ← succ_le_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
n : ℕ
⊢ (↑n : Ordinal.{u_4}) + ω = ω
have refine : ∀ (a : Ordinal.{u_4}) (ha : a < (↑n : Ordinal.{u_4}) + ω), a < ω
Tactic: refine le_antisymm (le_of_forall_lt fun a ha ↦ ?_) le_add_self
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
n : ℕ
a : Ordinal.{u_4}
ha : a < (↑n : Ordinal.{u_4}) + ω
⊢ a < ω
have obtain : ∀ (b : Ordinal.{u_4}) (hb' : b < ω) (hb : a ≤ (↑n : Ordinal.{u_4}) + b), a < ω
Tactic: obtain ⟨b, hb', hb⟩ := (lt_add_iff omega0_ne_zero).1 ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
n : ℕ
a : Ordinal.{u_4}
ha : a < (↑n : Ordinal.{u_4}) + ω
b : Ordinal.{u_4}
hb' : b < ω
hb : a ≤ (↑n : Ordinal.{u_4}) + b
⊢ a < ω
have obtain : ∀ (m : ℕ) (hb' : (↑m : Ordinal.{u_4}) < ω)
  (hb : a ≤ HAdd.hAdd (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑m : Ordinal.{u_4})), a < ω
Tactic: obtain ⟨m, rfl⟩ := lt_omega0.1 hb'
Cleared hypotheses: b, hb', hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
n : ℕ
a : Ordinal.{u_4}
ha : a < (↑n : Ordinal.{u_4}) + ω
m : ℕ
hb' : (↑m : Ordinal.{u_4}) < ω
hb : a ≤ HAdd.hAdd (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑m : Ordinal.{u_4})
⊢ a < ω
have apply : HAdd.hAdd (α := Ordinal.{u_4}) (↑n : Ordinal.{u_4}) (↑m : Ordinal.{u_4}) < ω
Tactic: apply hb.trans_lt
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
h : a < ω
⊢ a + ω = ω
have obtain : ∀ (n : ℕ) (h : (↑n : Ordinal.{u_4}) < ω), (↑n : Ordinal.{u_4}) + ω = ω
Tactic: obtain ⟨n, rfl⟩ := lt_omega0.1 h
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
h : ω ≤ o
n : ℕ
⊢ (↑n : Ordinal.{u_4}) + o = o
have rw : (↑n : Ordinal.{u_4}) + (ω + (o - ω)) = ω + (o - ω)
Tactic: rw [← Ordinal.add_sub_cancel_of_le h, ← add_assoc, natCast_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
h : ω ≤ o
n : ℕ
rw : (↑n : Ordinal.{u_4}) + (ω + (o - ω)) = ω + (o - ω)
⊢ (↑n : Ordinal.{u_4}) + o = o
have rw₁ : (↑n : Ordinal.{u_4}) + ω + (o - ω) = ω + (o - ω)
Tactic: rw [← Ordinal.add_sub_cancel_of_le h, ← add_assoc, natCast_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
o : Ordinal.{u_4}
h : ω ≤ o
n : ℕ
rw : (↑n : Ordinal.{u_4}) + (ω + (o - ω)) = ω + (o - ω)
rw₁ : (↑n : Ordinal.{u_4}) + ω + (o - ω) = ω + (o - ω)
⊢ (↑n : Ordinal.{u_4}) + o = o
have rw₂ : ω + (o - ω) = ω + (o - ω)
Tactic: rw [← Ordinal.add_sub_cancel_of_le h, ← add_assoc, natCast_add_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
⊢ IsSuccPrelimit a ↔ ω ∣ a
have refine_1 : ∀ (l : IsSuccPrelimit a), a ≤ ω * (a / ω)
Tactic: refine ⟨fun l => ⟨a / ω, le_antisymm ?_ (mul_div_le _ _)⟩, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
refine_1 : ∀ (l : IsSuccPrelimit a), a ≤ ω * (a / ω)
⊢ IsSuccPrelimit a ↔ ω ∣ a
have refine_2 : ∀ (h : ω ∣ a), IsSuccPrelimit a
Tactic: refine ⟨fun l => ⟨a / ω, le_antisymm ?_ (mul_div_le _ _)⟩, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
l : IsSuccPrelimit a
⊢ a ≤ ω * (a / ω)
have refine_1 : ∀ (x : Ordinal.{u_4}) (hx : x < a), x < ω * (a / ω)
Tactic: refine l.le_iff_forall_le.2 fun x hx => le_of_lt ?_
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
⊢ x < ω * (a / ω)
have refine_1 : ∀ d < ω, ω * (x / ω) + d ≤ a
Tactic: rw [lt_mul_iff_div_lt omega0_ne_zero, ← succ_le_iff, ← mul_le_iff_le_div omega0_ne_zero,
      mul_succ, add_le_iff_of_isSuccLimit isSuccLimit_omega0]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
b : Ordinal.{u_4}
hb : b < ω
⊢ ω * (x / ω) + b ≤ a
have refine_1 : ∀ (n : ℕ) (hb : (↑n : Ordinal.{u_4}) < ω), ω * (x / ω) + (↑n : Ordinal.{u_4}) ≤ a
Tactic: rcases lt_omega0.1 hb with ⟨n, rfl⟩
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
l : IsSuccPrelimit a
x : Ordinal.{u_4}
hx : x < a
n : ℕ
hb : (↑n : Ordinal.{u_4}) < ω
⊢ ω * (x / ω) + (↑n : Ordinal.{u_4}) ≤ a
have refine_1 : x + (↑n : Ordinal.{u_4}) ≤ a
Tactic: grw [mul_div_le]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
h : ω ∣ a
⊢ IsSuccPrelimit a
have refine_2 : ∀ (a0 : Ordinal.{u_4}), IsSuccPrelimit (ω * a0)
Tactic: rcases h with ⟨a0, b, rfl⟩
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
⊢ IsSuccLimit a ↔ a ≠ 0 ∧ ω ∣ a
have rw : a ≠ 0 ∧ IsSuccPrelimit a ↔ a ≠ 0 ∧ ω ∣ a
Tactic: rw [isSuccLimit_iff, isSuccPrelimit_iff_omega0_dvd]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Arithmetic (goal)
Goal:
a : Ordinal.{u_4}
rw : a ≠ 0 ∧ IsSuccPrelimit a ↔ a ≠ 0 ∧ ω ∣ a
⊢ IsSuccLimit a ↔ a ≠ 0 ∧ ω ∣ a
have rw₁ : a ≠ 0 ∧ ω ∣ a ↔ a ≠ 0 ∧ ω ∣ a
Tactic: rw [isSuccLimit_iff, isSuccPrelimit_iff_omega0_dvd]