awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha :
  a <
    nfp
      (fun (x : Ordinal.{u_1}) ↦
        ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
          succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))
      o
hb :
  b <
    nfp
      (fun (x : Ordinal.{u_1}) ↦
        ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
          succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))
      o
⊢ op a b <
    nfp
      (fun (x : Ordinal.{u_1}) ↦
        ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
          succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))
      o
have rw : ∀
  (ha :
    ∃ (n : ℕ),
      a <
        (fun (x : Ordinal.{u_1}) ↦
              ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
                succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
          o)
  (hb :
    ∃ (n : ℕ),
      b <
        (fun (x : Ordinal.{u_1}) ↦
              ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
                succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
          o),
  ∃ (n : ℕ),
    op a b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
Tactic: rw [lt_nfp_iff] at *
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha :
  ∃ (n : ℕ),
    a <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
hb :
  ∃ (n : ℕ),
    b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
⊢ ∃ (n : ℕ),
    op a b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
have obtain : ∀ (m : ℕ)
  (ha :
    a <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
        o),
  ∃ (n : ℕ),
    op a b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
Tactic: obtain ⟨m, ha⟩ := ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
hb :
  ∃ (n : ℕ),
    b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
m : ℕ
ha :
  a <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o
⊢ ∃ (n : ℕ),
    op a b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
have obtain : ∀ (n : ℕ)
  (hb :
    b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o),
  ∃ (n : ℕ),
    op a b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
Tactic: obtain ⟨n, hb⟩ := hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha :
  a <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o
n : ℕ
hb :
  b <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o
⊢ ∃ (n : ℕ),
    op a b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
have inl : ∀
  (h :
    (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
        o ≤
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o),
  ∃ (n : ℕ),
    op a b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
Tactic: obtain h | h := le_total
    ((fun x ↦ ⨆ y : Set.Iio x ×ˢ Set.Iio x, succ (op y.1.1 y.1.2))^[m] o)
    ((fun x ↦ ⨆ y : Set.Iio x ×ˢ Set.Iio x, succ (op y.1.1 y.1.2))^[n] o)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha :
  a <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o
n : ℕ
hb :
  b <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o
inl :
  ∀
    (h :
      (fun (x : Ordinal.{u_1}) ↦
              ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
                succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
          o ≤
        (fun (x : Ordinal.{u_1}) ↦
              ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
                succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
          o),
    ∃ (n : ℕ),
      op a b <
        (fun (x : Ordinal.{u_1}) ↦
              ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
                succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
          o
⊢ ∃ (n : ℕ),
    op a b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
have inr : ∀
  (h :
    (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o ≤
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
        o),
  ∃ (n : ℕ),
    op a b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
Tactic: obtain h | h := le_total
    ((fun x ↦ ⨆ y : Set.Iio x ×ˢ Set.Iio x, succ (op y.1.1 y.1.2))^[m] o)
    ((fun x ↦ ⨆ y : Set.Iio x ×ˢ Set.Iio x, succ (op y.1.1 y.1.2))^[n] o)
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha :
  a <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o
n : ℕ
hb :
  b <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o
h :
  (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o ≤
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o
⊢ ∃ (n : ℕ),
    op a b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
have h₁ : op a b <
  (fun (x : Ordinal.{u_1}) ↦
        ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
          succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n + 1]
    o
Tactic: use n + 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha :
  a <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o
n : ℕ
hb :
  b <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o
h :
  (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o ≤
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o
⊢ op a b <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n + 1]
      o
have h₁ : op a b <
  ((fun (x : Ordinal.{u_1}) ↦
        ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
          succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2)) ∘
      (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n])
    o
Tactic: rw [Function.iterate_succ']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha :
  a <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o
n : ℕ
hb :
  b <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o
h :
  (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o ≤
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o
⊢ op a b <
    ((fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2)) ∘
        (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n])
      o
have h₁ : succ (op a b) ≤
  ((fun (x : Ordinal.{u_1}) ↦
        ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
          succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2)) ∘
      (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n])
    o
Tactic: apply (lt_succ _).trans_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha :
  a <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o
n : ℕ
hb :
  b <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o
h :
  (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o ≤
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o
⊢ ∃ (n : ℕ),
    op a b <
      (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
        o
have h₁ : op a b <
  (fun (x : Ordinal.{u_1}) ↦
        ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
          succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m + 1]
    o
Tactic: use m + 1
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha :
  a <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o
n : ℕ
hb :
  b <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o
h :
  (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o ≤
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o
⊢ op a b <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m + 1]
      o
have h₁ : op a b <
  ((fun (x : Ordinal.{u_1}) ↦
        ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
          succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2)) ∘
      (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m])
    o
Tactic: rw [Function.iterate_succ']
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha :
  a <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o
n : ℕ
hb :
  b <
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o
h :
  (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[n]
      o ≤
    (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m]
      o
⊢ op a b <
    ((fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2)) ∘
        (fun (x : Ordinal.{u_1}) ↦
            ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
              succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m])
      o
have h₁ : succ (op a b) ≤
  ((fun (x : Ordinal.{u_1}) ↦
        ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
          succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2)) ∘
      (fun (x : Ordinal.{u_1}) ↦
          ⨆ (y : (↑(Set.Iio x ×ˢ Set.Iio x) : Type (u_1 + 1))),
            succ (op (↑y : Ordinal.{u_1} × Ordinal.{u_1}).1 (↑y : Ordinal.{u_1} × Ordinal.{u_1}).2))^[m])
    o
Tactic: apply (lt_succ _).trans_le
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
ha : a < o
n : ℕ
h : a * (↑n : Ordinal.{u}) < o
⊢ a * (↑(n + 1) : Ordinal.{u}) < o
have succ : a * (↑n : Ordinal.{u}) + a < o
Tactic: rw [Nat.cast_add_one, mul_add_one]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
ha : a < o
n : ℕ
⊢ a * (↑n : Ordinal.{u}) < o
have zero : a * (↑0 : Ordinal.{u}) < o
Tactic: induction n with
  | zero => simpa using ha.pos
  | succ n h =>
    rw [Nat.cast_add_one, mul_add_one]
    exact ho h ha
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
ha : a < o
n : ℕ
zero : a * (↑0 : Ordinal.{u}) < o
⊢ a * (↑n : Ordinal.{u}) < o
have succ : ∀ (n : ℕ) (h : a * (↑n : Ordinal.{u}) < o), a * (↑(n + 1) : Ordinal.{u}) < o
Tactic: induction n with
  | zero => simpa using ha.pos
  | succ n h =>
    rw [Nat.cast_add_one, mul_add_one]
    exact ho h ha
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho : o ≤ 1
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
have inl : ∀ (ho : LE.le.{u + 1} (α := Ordinal.{u}) 0 1), IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0
Tactic: rcases le_one_iff.1 ho with (rfl | rfl)
Cleared hypotheses: o, ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho : o ≤ 1
inl : ∀ (ho : LE.le.{u + 1} (α := Ordinal.{u}) 0 1), IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
have inr : ∀ (ho : LE.le.{u + 1} (α := Ordinal.{u}) 1 1), IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 1
Tactic: rcases le_one_iff.1 ho with (rfl | rfl)
Cleared hypotheses: o, ho
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho₁ : 1 < o
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
⊢ IsSuccLimit o
have rw : o ≠ 0 ∧ ∀ a < o, succ a < o
Tactic: rw [isSuccLimit_iff, isSuccPrelimit_iff_succ_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o ↔ ∀ a < o, a + o = o
have refine_1 : ∀ (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o) (a : Ordinal.{u}) (hao : a < o), a + o = o
Tactic: refine ⟨fun ho a hao => ?_, fun h a b hao hbo => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
refine_1 : ∀ (ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o) (a : Ordinal.{u}) (hao : a < o), a + o = o
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o ↔ ∀ a < o, a + o = o
have refine_2 : ∀ (h : ∀ a < o, a + o = o) (a b : Ordinal.{u}) (hao : a < o) (hbo : b < o),
  (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a b < o
Tactic: refine ⟨fun ho a hao => ?_, fun h a b hao hbo => ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
⊢ a + o = o
have refine_1 : ∀ (ho₁ : 1 < o), a + o = o
Tactic: rcases lt_or_ge 1 o with ho₁ | ho₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
refine_1 : ∀ (ho₁ : 1 < o), a + o = o
⊢ a + o = o
have refine_1₁ : ∀ (ho₁ : o ≤ 1), a + o = o
Tactic: rcases lt_or_ge 1 o with ho₁ | ho₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
⊢ a + o = o
have refine_1 : o = 0 → a + o = o
Tactic: cases le_one_iff.1 ho₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
refine_1 : o = 0 → a + o = o
⊢ a + o = o
have refine_1₁ : o = 1 → a + o = o
Tactic: cases le_one_iff.1 ho₁
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a b < o
have refine_2 : (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a b < a + o
Tactic: rw [← h a hao]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b c : Ordinal.{u}
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
⊢ a + c = c
have rw : a + (b + (c - b)) = b + (c - b)
Tactic: rw [← Ordinal.add_sub_cancel_of_le hbc, ← add_assoc, hb.add_eq_right hab,
    Ordinal.add_sub_cancel_of_le hbc]
-- Lean 4 proof step from Mathlib.SetTheory.Ordinal.Principal (goal)
Goal:
a b c : Ordinal.{u}
hb : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) b
hab : a < b
hbc : b ≤ c
rw : a + (b + (c - b)) = b + (c - b)
⊢ a + c = c
have rw₁ : a + b + (c - b) = b + (c - b)
Tactic: rw [← Ordinal.add_sub_cancel_of_le hbc, ← add_assoc, hb.add_eq_right hab,
    Ordinal.add_sub_cancel_of_le hbc]