awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
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
⊢ 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:
rw [Function.iterate_succ']

Premises used: Function.iterate_succ'
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
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
⊢ 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

Premises used: Order.lt_succ, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
⊢ 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:
Ordinal.le_iSup (fun y : Set.Iio _ ×ˢ Set.Iio _ ↦ succ (op y.1.1 y.1.2))
      ⟨_, Set.mk_mem_prod (ha.trans_le h) hb⟩

Premises used: Order.succ, iSup, Prod.fst, Subtype.mk, Ordinal.le_iSup, LT.lt.trans_le, Subtype.val, Set.mk_mem_prod, Prod.snd
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
⊢ 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:
exact Ordinal.le_iSup (fun y : Set.Iio _ ×ˢ Set.Iio _ ↦ succ (op y.1.1 y.1.2))
      ⟨_, Set.mk_mem_prod (ha.trans_le h) hb⟩

Premises used: Order.succ, Prod.fst, Subtype.mk, Ordinal.le_iSup, LT.lt.trans_le, Subtype.val, Set.mk_mem_prod, Prod.snd
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
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
⊢ ∃ (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:
use m + 1
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
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
⊢ 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:
rw [Function.iterate_succ']

Premises used: Function.iterate_succ'
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
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
⊢ 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

Premises used: Order.lt_succ, LT.lt.trans_le
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
⊢ 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:
Ordinal.le_iSup (fun y : Set.Iio _ ×ˢ Set.Iio _ ↦ succ (op y.1.1 y.1.2))
      ⟨_, Set.mk_mem_prod ha (hb.trans_le h)⟩

Premises used: Order.succ, iSup, Prod.fst, Subtype.mk, Ordinal.le_iSup, LT.lt.trans_le, Subtype.val, Set.mk_mem_prod, Prod.snd
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
⊢ 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:
exact Ordinal.le_iSup (fun y : Set.Iio _ ×ˢ Set.Iio _ ↦ succ (op y.1.1 y.1.2))
      ⟨_, Set.mk_mem_prod ha (hb.trans_le h)⟩

Premises used: Order.succ, Prod.fst, Subtype.mk, Ordinal.le_iSup, LT.lt.trans_le, Subtype.val, Set.mk_mem_prod, Prod.snd
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
ha : Membership.mem (γ := Set Ordinal.{u_1}) (upperBounds {o : Ordinal.{u_1} | IsPrincipal op o}) a
⊢ False

Tactic:
((le_nfp _ _).trans (ha (isPrincipal_nfp_iSup op (succ a)))).not_gt (lt_succ a)

Premises used: Order.succ, _private.0.Ordinal.isPrincipal_nfp_iSup, Ordinal.le_nfp, Order.lt_succ, LE.le.not_gt, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
a : Ordinal.{u_1}
ha : Membership.mem (γ := Set Ordinal.{u_1}) (upperBounds {o : Ordinal.{u_1} | IsPrincipal op o}) a
⊢ False

Tactic:
exact ((le_nfp _ _).trans (ha (isPrincipal_nfp_iSup op (succ a)))).not_gt (lt_succ a)

Premises used: Order.succ, _private.0.Ordinal.isPrincipal_nfp_iSup, Ordinal.le_nfp, Order.lt_succ, LE.le.not_gt, LE.le.trans
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a : Ordinal.{u}
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a ↔ ∀ b < a, b + b < a

Tactic:
isPrincipal_iff_of_monotone
    (fun x _ _ h ↦ add_le_add_right h x) (fun x _ _ h ↦ add_le_add_left h x)

Premises used: Ordinal.isPrincipal_iff_of_monotone, add_le_add_left, add_le_add_right
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
ha : a < o
⊢ a * (↑0 : Ordinal.{u}) < o

Tactic:
simpa using ha.pos

Premises used: LT.lt.pos
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
succ : a * (↑n : Ordinal.{u}) + a < o
⊢ a * (↑(n + 1) : Ordinal.{u}) < o

Tactic:
rw [Nat.cast_add_one, mul_add_one]

Premises used: mul_add_one, Nat.cast_add_one
-- Module: Mathlib.SetTheory.Ordinal.Principal
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 : Ordinal.{u}) + a < o

Tactic:
ho h ha
-- Module: Mathlib.SetTheory.Ordinal.Principal
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 : Ordinal.{u}) + a < o

Tactic:
exact ho h ha
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
succ : ∀ (n : ℕ) (h : a * (↑n : Ordinal.{u}) < o), a * (↑(n + 1) : Ordinal.{u}) < o
⊢ a * (↑n : 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

Premises used: LT.lt.pos, Order.succ, Ordinal.zero, mul_add_one, Nat.cast_add_one
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
⊢ IsPrincipal.{u_1} (fun (x1 x2 : Ordinal.{u_1}) ↦ x1 + x2) 1

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
inr : ∀ (ho : LE.le.{u + 1} (α := Ordinal.{u}) 1 1), IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 1
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o

Tactic:
rcases le_one_iff.1 ho with (rfl | rfl)

Premises used: Iff.mp, Order.le_one_iff, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ho : LE.le.{u + 1} (α := Ordinal.{u}) 0 1
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0

Tactic:
isPrincipal_zero

Premises used: Ordinal.isPrincipal_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ho : LE.le.{u + 1} (α := Ordinal.{u}) 0 1
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 0

Tactic:
exact isPrincipal_zero

Premises used: Ordinal.isPrincipal_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ho : LE.le.{u + 1} (α := Ordinal.{u}) 1 1
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 1

Tactic:
isPrincipal_add_one

Premises used: Ordinal.isPrincipal_add_one
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
ho : LE.le.{u + 1} (α := Ordinal.{u}) 1 1
⊢ IsPrincipal.{u} (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) 1

Tactic:
exact isPrincipal_add_one

Premises used: Ordinal.isPrincipal_add_one
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho₁ : 1 < o
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
rw : o ≠ 0 ∧ ∀ a < o, succ a < o
⊢ IsSuccLimit o

Tactic:
rw [isSuccLimit_iff, isSuccPrelimit_iff_succ_lt]

Premises used: Order.isSuccPrelimit_iff_succ_lt, Ordinal.isSuccLimit_iff
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho₁ : 1 < o
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
⊢ o ≠ 0 ∧ ∀ a < o, succ a < o

Tactic:
⟨ho₁.ne_bot, fun _ ha ↦ ho ha ho₁⟩

Premises used: And.intro, LT.lt.ne_bot
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho₁ : 1 < o
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
⊢ o ≠ 0 ∧ ∀ a < o, succ a < o

Tactic:
exact ⟨ho₁.ne_bot, fun _ ha ↦ ho ha ho₁⟩
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o ↔ ∀ a < o, a + o = o

Tactic:
⟨fun ho a hao => ?_, fun h a b hao hbo => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
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
⊢ IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o ↔ ∀ a < o, a + o = o

Tactic:
refine ⟨fun ho a hao => ?_, fun h a b hao hbo => ?_⟩
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
refine_1₁ : ∀ (ho₁ : o ≤ 1), a + o = o
⊢ a + o = o

Tactic:
rcases lt_or_ge 1 o with ho₁ | ho₁

Premises used: lt_or_ge, OfNat.ofNat
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : 1 < o
⊢ a + o = o

Tactic:
op_eq_self_of_isPrincipal hao (isNormal_add_right a) ho
        (isSuccLimit_of_isPrincipal_add ho₁ ho)

Premises used: Ordinal.isSuccLimit_of_isPrincipal_add, Ordinal.op_eq_self_of_isPrincipal, Ordinal.isNormal_add_right
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : 1 < o
⊢ a + o = o

Tactic:
exact op_eq_self_of_isPrincipal hao (isNormal_add_right a) ho
        (isSuccLimit_of_isPrincipal_add ho₁ ho)

Premises used: Ordinal.isSuccLimit_of_isPrincipal_add, Ordinal.op_eq_self_of_isPrincipal
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
refine_1₁ : o = 1 → a + o = o
⊢ a + o = o

Tactic:
cases le_one_iff.1 ho₁

Premises used: Iff.mp, Order.le_one_iff
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
h : o = 0
⊢ a + o = o

Tactic:
simp_all
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
a : Ordinal.{u}
hao : a < o
ho₁ : o ≤ 1
h : o = 1
⊢ a + o = o

Tactic:
simp_all
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
h : ∀ a < o, a + o = o
a b : Ordinal.{u}
hao : a < o
hbo : b < o
refine_2 : (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a b < a + o
⊢ (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) a b < o

Tactic:
rw [← h a hao]
-- Module: Mathlib.SetTheory.Ordinal.Principal
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 < a + o

Tactic:
(isNormal_add_right a).strictMono hbo

Premises used: Ordinal.isNormal_add_right, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Principal
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 < a + o

Tactic:
exact (isNormal_add_right a).strictMono hbo

Premises used: Ordinal.isNormal_add_right, Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a o : Ordinal.{u}
ho : IsPrincipal (fun (x1 x2 : Ordinal.{u}) ↦ x1 + x2) o
ha : a < o
⊢ a + o = o

Tactic:
isPrincipal_add_iff_add_left_eq_self.1 ho a ha

Premises used: Ordinal.isPrincipal_add_iff_add_left_eq_self, Iff.mp