awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a : ONote
ha : a.NF
b : ONote
hb : b.NF
h : a.cmp b = Ordering.eq
this : Ordering.eq.Compares a b
⊢ Ordering.eq.Compares (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a ha) (Subtype.mk (p := fun (o : ONote) ↦ o.NF) b hb)

Tactic:
exact Subtype.mk_eq_mk.2 this

Premises used: Iff.mpr, Subtype.mk_eq_mk
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
C : NONote → Sort u_1
o : NONote
H0 : C 0
H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)
obtain : (o : ONote) → (h : o.NF) → C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) o h)
⊢ C o

Tactic:
obtain ⟨o, h⟩ := o
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
C : NONote → Sort u_1
H0 : C 0
H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)
h : ONote.zero.NF
⊢ C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) ONote.zero h)

Tactic:
exact H0
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
C : NONote → Sort u_1
H0 : C 0
H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)
e : ONote
n : ℕ+
a : ONote
IHe : (h : e.NF) → C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) e h)
IHa : (h : a.NF) → C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a h)
h : (e.oadd n a).NF
⊢ C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) (e.oadd n a) h)

Tactic:
exact H1 ⟨e, h.fst⟩ n ⟨a, h.snd⟩ h.snd' (IHe _) (IHa _)

Premises used: ONote.NF.snd, Subtype.mk, ONote.NF.fst, ONote.NF.snd'
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
C : NONote → Sort u_1
H0 : C 0
H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)
o : ONote
h : o.NF
zero : (h : ONote.zero.NF) → C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) ONote.zero h)
oadd :
  (e : ONote) →
    (n : ℕ+) →
      (a : ONote) →
        (IHe : (h : e.NF) → C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) e h)) →
          (IHa : (h : a.NF) → C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) a h)) →
            (h : (e.oadd n a).NF) → C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) (e.oadd n a) h)
⊢ C (Subtype.mk (p := fun (o : ONote) ↦ o.NF) o h)

Tactic:
induction o with
  | zero => exact H0
  | oadd e n a IHe IHa => exact H1 ⟨e, h.fst⟩ n ⟨a, h.snd⟩ h.snd' (IHe _) (IHa _)

Premises used: NONote.oadd
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a b : NONote
⊢ (a + b).repr = a.repr + b.repr

Tactic:
ONote.repr_add a.1 b.1

Premises used: ONote.repr_add, NONote.repr, Subtype.val
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a b : NONote
⊢ (a - b).repr = a.repr - b.repr

Tactic:
ONote.repr_sub a.1 b.1

Premises used: NONote.repr, Subtype.val, ONote.repr_sub
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a b : NONote
⊢ (a * b).repr = a.repr * b.repr

Tactic:
ONote.repr_mul a.1 b.1

Premises used: ONote.repr_mul, NONote.repr, Subtype.val
-- Module: Mathlib.SetTheory.Ordinal.Notation
Goal:
a b : NONote
⊢ (a.opow b).repr = a.repr ^ b.repr

Tactic:
ONote.repr_opow a.1 b.1

Premises used: NONote.repr, ONote.repr_opow, Subtype.val
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
mp : IsPrincipal (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) op) o → IsPrincipal op o
mpr : IsPrincipal op o → IsPrincipal (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) op) o
⊢ IsPrincipal (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) op) o ↔ IsPrincipal op o

Tactic:
constructor
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ IsPrincipal (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) op) o → IsPrincipal op o

Tactic:
fun h a b ha hb => h hb ha

Premises used: Ordinal.IsPrincipal
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ IsPrincipal (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) op) o → IsPrincipal op o

Tactic:
exact fun h a b ha hb => h hb ha
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ IsPrincipal op o → IsPrincipal (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) op) o

Tactic:
fun h a b ha hb => h hb ha

Premises used: Ordinal.IsPrincipal
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ IsPrincipal op o → IsPrincipal (Function.swap (φ := fun (a a_1 : Ordinal.{u}) ↦ Ordinal.{u}) op) o

Tactic:
exact fun h a b ha hb => h hb ha
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ ¬IsPrincipal op o ↔ ∃ a < o, ∃ b < o, o ≤ op a b

Tactic:
simp [IsPrincipal]

Premises used: Ordinal.IsPrincipal
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap (φ := fun (x y : Ordinal.{u}) ↦ Ordinal.{u}) op a)
mpr : (∀ a < o, op a a < o) → IsPrincipal op o
⊢ IsPrincipal op o ↔ ∀ a < o, op a a < o

Tactic:
use fun h a ha => h ha ha
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap (φ := fun (x y : Ordinal.{u}) ↦ Ordinal.{u}) op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
mpr : ∀ (hab : a ≤ b), op a b < o
mpr₁ : ∀ (hba : b < a), op a b < o
⊢ op a b < o

Tactic:
obtain hab | hba := le_or_gt a b

Premises used: le_or_gt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap (φ := fun (x y : Ordinal.{u}) ↦ Ordinal.{u}) op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hab : a ≤ b
⊢ op a b < o

Tactic:
(h₂ b hab).trans_lt <| H b hb

Premises used: LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap (φ := fun (x y : Ordinal.{u}) ↦ Ordinal.{u}) op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hab : a ≤ b
⊢ op a b < o

Tactic:
exact (h₂ b hab).trans_lt <| H b hb

Premises used: LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap (φ := fun (x y : Ordinal.{u}) ↦ Ordinal.{u}) op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hba : b < a
⊢ op a b < o

Tactic:
(h₁ a hba.le).trans_lt <| H a ha

Premises used: LT.lt.le, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap (φ := fun (x y : Ordinal.{u}) ↦ Ordinal.{u}) op a)
H : ∀ a < o, op a a < o
a b : Ordinal.{u}
ha : a < o
hb : b < o
hba : b < a
⊢ op a b < o

Tactic:
exact (h₁ a hba.le).trans_lt <| H a ha

Premises used: LT.lt.le, LE.le.trans_lt
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
h₁ : ∀ (a : Ordinal.{u}), Monotone (op a)
h₂ : ∀ (a : Ordinal.{u}), Monotone (Function.swap (φ := fun (x y : Ordinal.{u}) ↦ Ordinal.{u}) op a)
⊢ ¬IsPrincipal op o ↔ ∃ a < o, o ≤ op a a

Tactic:
simp [isPrincipal_iff_of_monotone h₁ h₂]

Premises used: Ordinal.isPrincipal_iff_of_monotone
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
⊢ IsPrincipal op 0

Tactic:
simp [IsPrincipal]

Premises used: Ordinal.IsPrincipal
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
⊢ IsPrincipal op 1 ↔ op 0 0 = 0

Tactic:
simp [IsPrincipal]

Premises used: Ordinal.IsPrincipal
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
zero zero₁ zero₂ zero₃ : id a < o
⊢ (op a)^[0] a < o

Tactic:
rwa [Function.iterate_zero]

Premises used: Function.iterate_zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
n : ℕ
hn : (op a)^[n] a < o
succ : (op a ∘ (op a)^[n]) a < o
⊢ (op a)^[n + 1] a < o

Tactic:
rw [Function.iterate_succ']

Premises used: Function.iterate_succ'
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
n : ℕ
hn : (op a)^[n] a < o
⊢ (op a ∘ (op a)^[n]) a < o

Tactic:
ho hao hn
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
n : ℕ
hn : (op a)^[n] a < o
⊢ (op a ∘ (op a)^[n]) a < o

Tactic:
exact ho hao hn
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
n : ℕ
zero : (op a)^[0] a < o
succ : ∀ (n : ℕ) (hn : (op a)^[n] a < o), (op a)^[n + 1] a < o
⊢ (op a)^[n] a < o

Tactic:
induction n with
  | zero => rwa [Function.iterate_zero]
  | succ n hn =>
    rw [Function.iterate_succ']
    exact ho hao hn

Premises used: Order.succ, Function.iterate_zero, Function.iterate_succ', Ordinal.zero
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : IsPrincipal op o
ho' : IsSuccLimit o
apply : op a o ≤ o
⊢ op a o = o

Tactic:
apply H.strictMono.le_apply.antisymm'

Premises used: StrictMono.le_apply, LE.le.antisymm', Order.IsNormal.strictMono
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : IsPrincipal op o
ho' : IsSuccLimit o
rw : ∀ (i : (↑(Set.Iio o) : Type (u + 1))), op a (↑i : Ordinal.{u}) ≤ o
⊢ op a o ≤ o

Tactic:
rw [H.apply_of_isSuccLimit ho', Ordinal.iSup_le_iff]

Premises used: Order.IsNormal.apply_of_isSuccLimit, Ordinal.iSup_le_iff
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : IsPrincipal op o
ho' : IsSuccLimit o
⊢ ∀ (i : (↑(Set.Iio o) : Type (u + 1))), op a (↑i : Ordinal.{u}) ≤ o

Tactic:
fun ⟨b, hbo⟩ ↦ (ho hao hbo).le

Premises used: LT.lt.le, LE.le, _private.0.Ordinal.op_eq_self_of_isPrincipal.match_1, Subtype.val
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
H : IsNormal (op a)
ho : IsPrincipal op o
ho' : IsSuccLimit o
⊢ ∀ (i : (↑(Set.Iio o) : Type (u + 1))), op a (↑i : Ordinal.{u}) ≤ o

Tactic:
exact fun ⟨b, hbo⟩ ↦ (ho hao hbo).le
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
a o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
hao : a < o
ho : IsPrincipal op o
⊢ nfp (op a) a ≤ o

Tactic:
nfp_le fun n => (ho.iterate_lt hao n).le

Premises used: LT.lt.le, Ordinal.IsPrincipal.iterate_lt, Ordinal.nfp_le
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
⊢ IsPrincipal op (sSup ∅)

Tactic:
simp
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
⊢ IsPrincipal op (sSup ∅)

Tactic:
have : IsPrincipal op (sSup ∅) := by simp
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
pos : ∀ (hs : BddAbove s), IsPrincipal op (sSup s)
neg : ∀ (hs : ¬BddAbove s), IsPrincipal op (sSup s)
⊢ IsPrincipal op (sSup s)

Tactic:
by_cases hs : BddAbove s

Premises used: BddAbove
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
pos :
  ∀ (H : ∀ (x : Ordinal.{u_1}), Membership.mem (γ := Set Ordinal.{u_1}) ∅ x → IsPrincipal op x)
    (hs : BddAbove.{u_1 + 1} (α := Ordinal.{u_1}) ∅), IsPrincipal op (sSup ∅)
pos₁ : ∀ (hs' : s.Nonempty), IsPrincipal op (sSup s)
⊢ IsPrincipal op (sSup s)

Tactic:
obtain rfl | hs' := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
this : IsPrincipal op (sSup ∅)
H : ∀ (x : Ordinal.{u_1}), Membership.mem (γ := Set Ordinal.{u_1}) ∅ x → IsPrincipal op x
hs : BddAbove.{u_1 + 1} (α := Ordinal.{u_1}) ∅
⊢ IsPrincipal op (sSup ∅)

Tactic:
assumption
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
pos : ∀ ⦃a b : Ordinal.{u_1}⦄, ∀ x ∈ s, a < x → ∀ x ∈ s, b < x → ∃ b_1 ∈ s, op a b < b_1
⊢ IsPrincipal op (sSup s)

Tactic:
simp only [IsPrincipal, lt_csSup_iff hs hs', forall_exists_index, and_imp]

Premises used: Ordinal.IsPrincipal, lt_csSup_iff, and_imp, forall_exists_index
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
x y a : Ordinal.{u_1}
has : a ∈ s
ha : x < a
b : Ordinal.{u_1}
hbs : b ∈ s
hb : y < b
⊢ max a b ∈ s

Tactic:
have h : max a b ∈ s := max_rec' _ has hbs
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
x y a : Ordinal.{u_1}
has : a ∈ s
ha : x < a
b : Ordinal.{u_1}
hbs : b ∈ s
hb : y < b
h : max a b ∈ s
⊢ ∃ b ∈ s, op x y < b

Tactic:
⟨_, h, H (max a b) h (lt_max_of_lt_left ha) (lt_max_of_lt_right hb)⟩

Premises used: lt_max_of_lt_left, lt_max_of_lt_right, Max.max, And.intro, Exists.intro
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : BddAbove s
hs' : s.Nonempty
x y a : Ordinal.{u_1}
has : a ∈ s
ha : x < a
b : Ordinal.{u_1}
hbs : b ∈ s
hb : y < b
h : max a b ∈ s
⊢ ∃ b ∈ s, op x y < b

Tactic:
exact ⟨_, h, H (max a b) h (lt_max_of_lt_left ha) (lt_max_of_lt_right hb)⟩
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
s : Set Ordinal.{u_1}
H : ∀ x ∈ s, IsPrincipal op x
this : IsPrincipal op (sSup ∅)
hs : ¬BddAbove s
neg neg₁ neg₂ neg₃ : IsPrincipal op (sSup ∅)
⊢ IsPrincipal op (sSup s)

Tactic:
rwa [csSup_of_not_bddAbove hs]

Premises used: csSup_of_not_bddAbove
-- Module: Mathlib.SetTheory.Ordinal.Principal
Goal:
op : Ordinal.{u_2} → Ordinal.{u_2} → Ordinal.{u_2}
ι : Sort u_1
f : ι → Ordinal.{u_2}
H : ∀ (i : ι), IsPrincipal op (f i)
⊢ ∀ (x : Ordinal.{u_2}), Membership.mem (γ := Set Ordinal.{u_2}) (Set.range fun (i : ι) ↦ f i) x → IsPrincipal op x

Tactic:
simpa
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
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
⊢ 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

Tactic:
rw [lt_nfp_iff] at *

Premises used: Ordinal.lt_nfp_iff
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
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
⊢ ∃ (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
-- Module: Mathlib.SetTheory.Ordinal.Principal
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
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
⊢ ∃ (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
-- 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
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
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
⊢ ∃ (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)

Premises used: Order.succ, iSup, le_total, Nat.iterate, Prod.fst, Subtype.val, 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
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
⊢ ∃ (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 n + 1