awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
⊢ coeff b (eval b (single e x + f)) = single e x + f
have single_add : x < b
Tactic: rw [eval_single_add' _ hf', coeff_opow_mul_add hb hx, IH IH']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
single_add : x < b
⊢ coeff b (eval b (single e x + f)) = single e x + f
have single_add₁ : eval b f < b ^ e
Tactic: rw [eval_single_add' _ hf', coeff_opow_mul_add hb hx, IH IH']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
⊢ x < b
have single_add : (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e = x
Tactic: apply (hf e).trans_eq'
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf' : ∀ c ∈ f.support, c < e
hx : x ≠ 0
IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f
hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b
IH' : ∀ (e' : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e' < b
⊢ (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e = x
have single_add : e ∉ f.support
Tactic: rw [add_apply, single_eq_same, notMem_support_iff.1, add_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b
⊢ coeff b (eval b f) = f
have zero : ∀ (hf : ∀ (e : Ordinal.{u_1}), (0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b 0) = 0
Tactic: induction f using Finsupp.induction_on_max with
  | zero => simp
  | single_add e x f hf' hx IH =>
    have IH' (e') : f e' < b := by
      by_cases he' : e' ∈ f.support
      · apply (hf e').trans_eq'
        rw [add_apply, single_eq_of_ne, zero_add]
        exact (hf' _ he').ne
      · rw [notMem_support_iff.1 he']
        exact hb.pos
    rw [eval_single_add' _ hf', coeff_opow_mul_add hb hx, IH IH']
    · apply (hf e).trans_eq'
      rw [add_apply, single_eq_same, notMem_support_iff.1, add_zero]
      exact fun h ↦ (hf' _ h).false
    · exact eval_lt IH' hf'
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.CantorNormalForm (goal)
Goal:
b : Ordinal.{u_1}
hb : 1 < b
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b
zero : ∀ (hf : ∀ (e : Ordinal.{u_1}), (0 : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b 0) = 0
⊢ coeff b (eval b f) = f
have single_add : ∀ (e x : Ordinal.{u_1}) (f : Ordinal.{u_1} →₀ Ordinal.{u_1}) (hf' : ∀ c ∈ f.support, c < e) (hx : x ≠ 0)
  (IH : ∀ (hf : ∀ (e : Ordinal.{u_1}), (f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e < b), coeff b (eval b f) = f)
  (hf : ∀ (e_1 : Ordinal.{u_1}), (single e x + f : (a : Ordinal.{u_1}) → Ordinal.{u_1}) e_1 < b),
  coeff b (eval b (single e x + f)) = single e x + f
Tactic: induction f using Finsupp.induction_on_max with
  | zero => simp
  | single_add e x f hf' hx IH =>
    have IH' (e') : f e' < b := by
      by_cases he' : e' ∈ f.support
      · apply (hf e').trans_eq'
        rw [add_apply, single_eq_of_ne, zero_add]
        exact (hf' _ he').ne
      · rw [notMem_support_iff.1 he']
        exact hb.pos
    rw [eval_single_add' _ hf', coeff_opow_mul_add hb hx, IH IH']
    · apply (hf e).trans_eq'
      rw [add_apply, single_eq_same, notMem_support_iff.1, add_zero]
      exact fun h ↦ (hf' _ h).false
    · exact eval_lt IH' hf'
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
⊢ AddCommute o₁ o₂ ↔
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
have refine_1 : ∀ (hcomm : AddCommute o₁ o₂),
  ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
Tactic: refine ⟨fun hcomm ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
refine_1 :
  ∀ (hcomm : AddCommute o₁ o₂),
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
⊢ AddCommute o₁ o₂ ↔
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
have refine_2 : (∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂) →
  AddCommute o₁ o₂
Tactic: refine ⟨fun hcomm ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
have refine_1 : ∀ (o : Ordinal.{u_1})
  (ih :
    ∀ y < o,
      ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
        ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
  {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = o),
  ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
Tactic: induction h : o₁ + o₂ using WellFoundedLT.induction generalizing o₁ o₂ with | ind o ih
Cleared hypotheses: o₁, o₂, hcomm
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (hypothesis)
Goal:
o : Ordinal.{u_1}
ih :
  ∀ y < o,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
h : o₁ + o₂ = o
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
have ih₁ : ∀ y < o₁ + o₂,
  ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
Tactic: subst h
Cleared hypotheses: o, ih, h
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
have refine_1 : ∀
  (this :
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂)
      (ih :
        ∀ y < o₁ + o₂,
          ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
            ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
      (hle : o₁ ≤ o₂),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
  (hle : ¬o₁ ≤ o₂),
  ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
Tactic: wlog hle : o₁ ≤ o₂
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
refine_1 :
  ∀
    (this :
      ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂)
        (ih :
          ∀ y < o₁ + o₂,
            ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
              ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
        (hle : o₁ ≤ o₂),
        ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
    (hle : ¬o₁ ≤ o₂),
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
have wlog : ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂)
  (ih :
    ∀ y < o₁ + o₂,
      ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
        ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
  (hle : o₁ ≤ o₂),
  ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
Tactic: wlog hle : o₁ ≤ o₂
Cleared hypotheses: o₁, o₂, hcomm, ih
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
have inl : ∀ (hcomm : AddCommute 0 o₂)
  (ih :
    ∀ y < 0 + o₂,
      ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
        ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
  (hle : 0 ≤ o₂),
  ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = 0 ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
Tactic: rcases eq_or_ne o₁ 0 with (rfl | h₁)
Cleared hypotheses: o₁, hcomm, ih, hle
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
inl :
  ∀ (hcomm : AddCommute 0 o₂)
    (ih :
      ∀ y < 0 + o₂,
        ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
          ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂)
    (hle : 0 ≤ o₂),
    ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = 0 ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
have inr : ∀ (h₁ : o₁ ≠ 0),
  ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
Tactic: rcases eq_or_ne o₁ 0 with (rfl | h₁)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (hypothesis)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
have hsub : o₁ + o₃ = o₂
Tactic: have hsub : o₁ + o₃ = o₂ := Ordinal.add_sub_cancel_of_le hle
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (hypothesis)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
have hcomm' : AddCommute o₁ o₃
Tactic: have hcomm' : AddCommute o₁ o₃ := add_left_cancel (a := o₁) <| by grind
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (hypothesis)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
have hlt : o₁ + o₃ < o₁ + o₂
Tactic: have hlt : o₁ + o₃ < o₁ + o₂ := by simpa [hsub, hcomm.eq] using h₁.pos
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
have inr : ∀ (o : Ordinal.{u_1}) (n₁ n₃ : ℕ) (hn₁ : o * (↑n₁ : Ordinal.{u_1}) = o₁) (hn₃ : o * (↑n₃ : Ordinal.{u_1}) = o₃),
  ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
Tactic: rcases ih _ hlt hcomm' rfl with ⟨o, n₁, n₃, hn₁, hn₃⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * (↑n₁ : Ordinal.{u_1}) = o₁
hn₃ : o * (↑n₃ : Ordinal.{u_1}) = o₃
⊢ ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
have right : o * (↑(n₁ + n₃) : Ordinal.{u_1}) = o₂
Tactic: use o, n₁, n₁ + n₃, hn₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * (↑n₁ : Ordinal.{u_1}) = o₁
hn₃ : o * (↑n₃ : Ordinal.{u_1}) = o₃
⊢ o * (↑(n₁ + n₃) : Ordinal.{u_1}) = o₂
have right : o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₃ : Ordinal.{u_1}) = o₂
Tactic: rw [Nat.cast_add, mul_add, hn₁, hn₃, hsub]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * (↑n₁ : Ordinal.{u_1}) = o₁
hn₃ : o * (↑n₃ : Ordinal.{u_1}) = o₃
right : o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₃ : Ordinal.{u_1}) = o₂
⊢ o * (↑(n₁ + n₃) : Ordinal.{u_1}) = o₂
have right₁ : o * (↑n₁ : Ordinal.{u_1}) + o * (↑n₃ : Ordinal.{u_1}) = o₂
Tactic: rw [Nat.cast_add, mul_add, hn₁, hn₃, hsub]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * (↑n₁ : Ordinal.{u_1}) = o₁
hn₃ : o * (↑n₃ : Ordinal.{u_1}) = o₃
right : o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₃ : Ordinal.{u_1}) = o₂
right₁ : o * (↑n₁ : Ordinal.{u_1}) + o * (↑n₃ : Ordinal.{u_1}) = o₂
⊢ o * (↑(n₁ + n₃) : Ordinal.{u_1}) = o₂
have right₂ : o₁ + o * (↑n₃ : Ordinal.{u_1}) = o₂
Tactic: rw [Nat.cast_add, mul_add, hn₁, hn₃, hsub]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih :
  ∀ y < o₁ + o₂,
    ∀ {o₁ o₂ : Ordinal.{u_1}} (hcomm : AddCommute o₁ o₂) (h : o₁ + o₂ = y),
      ∃ (o : Ordinal.{u_1}) (n₁ : ℕ) (n₂ : ℕ), o * (↑n₁ : Ordinal.{u_1}) = o₁ ∧ o * (↑n₂ : Ordinal.{u_1}) = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * (↑n₁ : Ordinal.{u_1}) = o₁
hn₃ : o * (↑n₃ : Ordinal.{u_1}) = o₃
right : o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₃ : Ordinal.{u_1}) = o₂
right₁ : o * (↑n₁ : Ordinal.{u_1}) + o * (↑n₃ : Ordinal.{u_1}) = o₂
right₂ : o₁ + o * (↑n₃ : Ordinal.{u_1}) = o₂
right₃ : o₁ + o₃ = o₂
⊢ o * (↑(n₁ + n₃) : Ordinal.{u_1}) = o₂
have right₄ : o₂ = o₂
Tactic: rw [Nat.cast_add, mul_add, hn₁, hn₃, hsub]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o : Ordinal.{u_1}
n₁ n₂ : ℕ
⊢ AddCommute (o * (↑n₁ : Ordinal.{u_1})) (o * (↑n₂ : Ordinal.{u_1}))
have refine_2 : o * (↑n₁ : Ordinal.{u_1}) + o * (↑n₂ : Ordinal.{u_1}) = o * (↑n₂ : Ordinal.{u_1}) + o * (↑n₁ : Ordinal.{u_1})
Tactic: rw [addCommute_iff_eq, ← mul_add, ← mul_add, ← Nat.cast_add, add_comm, Nat.cast_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o : Ordinal.{u_1}
n₁ n₂ : ℕ
refine_2 : o * (↑n₁ : Ordinal.{u_1}) + o * (↑n₂ : Ordinal.{u_1}) = o * (↑n₂ : Ordinal.{u_1}) + o * (↑n₁ : Ordinal.{u_1})
⊢ AddCommute (o * (↑n₁ : Ordinal.{u_1})) (o * (↑n₂ : Ordinal.{u_1}))
have refine_2₁ : o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) =
  o * (↑n₂ : Ordinal.{u_1}) + o * (↑n₁ : Ordinal.{u_1})
Tactic: rw [addCommute_iff_eq, ← mul_add, ← mul_add, ← Nat.cast_add, add_comm, Nat.cast_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o : Ordinal.{u_1}
n₁ n₂ : ℕ
refine_2 : o * (↑n₁ : Ordinal.{u_1}) + o * (↑n₂ : Ordinal.{u_1}) = o * (↑n₂ : Ordinal.{u_1}) + o * (↑n₁ : Ordinal.{u_1})
refine_2₁ :
  o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) =
    o * (↑n₂ : Ordinal.{u_1}) + o * (↑n₁ : Ordinal.{u_1})
⊢ AddCommute (o * (↑n₁ : Ordinal.{u_1})) (o * (↑n₂ : Ordinal.{u_1}))
have refine_2₂ : o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) =
  o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
Tactic: rw [addCommute_iff_eq, ← mul_add, ← mul_add, ← Nat.cast_add, add_comm, Nat.cast_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o : Ordinal.{u_1}
n₁ n₂ : ℕ
refine_2 : o * (↑n₁ : Ordinal.{u_1}) + o * (↑n₂ : Ordinal.{u_1}) = o * (↑n₂ : Ordinal.{u_1}) + o * (↑n₁ : Ordinal.{u_1})
refine_2₁ :
  o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) =
    o * (↑n₂ : Ordinal.{u_1}) + o * (↑n₁ : Ordinal.{u_1})
refine_2₂ :
  o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) =
    o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
⊢ AddCommute (o * (↑n₁ : Ordinal.{u_1})) (o * (↑n₂ : Ordinal.{u_1}))
have refine_2₃ : o * (↑(n₁ + n₂) : Ordinal.{u_1}) = o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
Tactic: rw [addCommute_iff_eq, ← mul_add, ← mul_add, ← Nat.cast_add, add_comm, Nat.cast_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o : Ordinal.{u_1}
n₁ n₂ : ℕ
refine_2 : o * (↑n₁ : Ordinal.{u_1}) + o * (↑n₂ : Ordinal.{u_1}) = o * (↑n₂ : Ordinal.{u_1}) + o * (↑n₁ : Ordinal.{u_1})
refine_2₁ :
  o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) =
    o * (↑n₂ : Ordinal.{u_1}) + o * (↑n₁ : Ordinal.{u_1})
refine_2₂ :
  o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) =
    o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
refine_2₃ :
  o * (↑(n₁ + n₂) : Ordinal.{u_1}) = o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
⊢ AddCommute (o * (↑n₁ : Ordinal.{u_1})) (o * (↑n₂ : Ordinal.{u_1}))
have refine_2₄ : o * (↑(n₂ + n₁) : Ordinal.{u_1}) = o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
Tactic: rw [addCommute_iff_eq, ← mul_add, ← mul_add, ← Nat.cast_add, add_comm, Nat.cast_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Commute (goal)
Goal:
o : Ordinal.{u_1}
n₁ n₂ : ℕ
refine_2 : o * (↑n₁ : Ordinal.{u_1}) + o * (↑n₂ : Ordinal.{u_1}) = o * (↑n₂ : Ordinal.{u_1}) + o * (↑n₁ : Ordinal.{u_1})
refine_2₁ :
  o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) =
    o * (↑n₂ : Ordinal.{u_1}) + o * (↑n₁ : Ordinal.{u_1})
refine_2₂ :
  o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) =
    o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
refine_2₃ :
  o * (↑(n₁ + n₂) : Ordinal.{u_1}) = o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
refine_2₄ :
  o * (↑(n₂ + n₁) : Ordinal.{u_1}) = o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
⊢ AddCommute (o * (↑n₁ : Ordinal.{u_1})) (o * (↑n₂ : Ordinal.{u_1}))
have refine_2₅ : o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1}) =
  o * HAdd.hAdd (α := Ordinal.{u_1}) (↑n₂ : Ordinal.{u_1}) (↑n₁ : Ordinal.{u_1})
Tactic: rw [addCommute_iff_eq, ← mul_add, ← mul_add, ← Nat.cast_add, add_comm, Nat.cast_add]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
o a : Ordinal.{u}
s : Set Ordinal.{u}
ha : a ∈ s
H : ∀ b < o, enumOrd s b < a
⊢ enumOrd s o ≤ a
have rw : sInf (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}) ≤ a
Tactic: rw [enumOrd]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
hs : ¬BddAbove s
o : Ordinal.{u}
⊢ (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty
have rw : ∀ (hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y) (o : Ordinal.{u}),
  (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty
Tactic: rw [not_bddAbove_iff] at hs
Cleared hypotheses: hs, o
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Enum (goal)
Goal:
s : Set Ordinal.{u}
hs : ∀ (x : Ordinal.{u}), ∃ y ∈ s, x < y
o : Ordinal.{u}
⊢ (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty
have obtain : ∀ (a : Ordinal.{u}) (ha : a ∈ upperBounds (enumOrd s '' Iio o)),
  (s ∩ {b : Ordinal.{u} | ∀ c < o, enumOrd s c < b}).Nonempty
Tactic: obtain ⟨a, ha⟩ := bddAbove_of_small (s := enumOrd s '' Iio o)