-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_nfp_iSup (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) :
    Principal op (nfp (fun x ↦ ⨆ y : Set.Iio x ×ˢ Set.Iio x, succ (op y.1.1 y.1.2)) o)

Proof state:
case intro.intro.inr
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ ∃ n, op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Tactic:
use m + 1

Result:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m + 1] o

Proof state:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m + 1] o

Tactic:
rw [Function.iterate_succ']

Result:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ op a b < ((fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m]) o

Proof state:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha : a < nfp (fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) o
hb : b < nfp (fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) o
⊢ op a b < nfp (fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) o

Tactic:
rw [lt_nfp_iff] at *

Result:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha : ∃ n, a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
hb : ∃ n, b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ ∃ n, op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Proof state:
case intro.intro.inl
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ ∃ n, op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Tactic:
use n + 1

Result:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n + 1] o

Proof state:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ succ (op a b) ≤ ((fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x => ⨆ y, succ (op (↑y).1 (↑y).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⟩

Result:
no goals

Proof state:
case intro
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
hb : ∃ n, b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ ∃ n, op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Tactic:
obtain ⟨n, hb⟩ := hb

Result:
case intro.intro
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ ∃ n, op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Proof state:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ op a b < ((fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n]) o

Tactic:
apply (lt_succ _).trans_le

Result:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ succ (op a b) ≤ ((fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n]) o

Proof state:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ Principal op (nfp (fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) o)

Tactic:
intro a b ha hb

Result:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha : a < nfp (fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) o
hb : b < nfp (fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) o
⊢ op a b < nfp (fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) o

Proof state:
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
ha : ∃ n, a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
hb : ∃ n, b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
⊢ ∃ n, op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Tactic:
obtain ⟨m, ha⟩ := ha

Result:
case intro
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
hb : ∃ n, b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ ∃ n, op a b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o

Proof state:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ succ (op a b) ≤ ((fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x => ⨆ y, succ (op (↑y).1 (↑y).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)⟩

Result:
no goals

Proof state:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ op a b < ((fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m]) o

Tactic:
apply (lt_succ _).trans_le

Result:
case h
op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}
o a b : Ordinal.{u_1}
m : ℕ
ha : a < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
n : ℕ
hb : b < (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o
h : (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[n] o ≤ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m] o
⊢ succ (op a b) ≤ ((fun x => ⨆ y, succ (op (↑y).1 (↑y).2)) ∘ (fun x => ⨆ y, succ (op (↑y).1 (↑y).2))^[m]) o