-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_nfp_blsub₂ (op : Ordinal → Ordinal → Ordinal) (o : Ordinal) :
    Principal op (nfp (fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b)) o)

Proof state:
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
ha : a < nfp (fun o' => o'.blsub₂ o' fun a x b x => op a b) o
hb : b < nfp (fun o' => o'.blsub₂ o' fun a x b x => op a b) o
⊢ op a b < nfp (fun o' => o'.blsub₂ o' fun a x b x => op a b) o

Tactic:
rw [lt_nfp_iff] at *

Result:
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
ha : ∃ n, a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
hb : ∃ n, b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
⊢ ∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o

Proof state:
case h
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
⊢ op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m + 1] o

Tactic:
rw [Function.iterate_succ']

Result:
case h
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
⊢ op a b < ((fun o' => o'.blsub₂ o' fun a x b x => op a b) ∘ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m]) o

Proof state:
case intro.intro.inl
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
⊢ ∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o

Tactic:
use n + 1

Result:
case h
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
⊢ op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n + 1] o

Proof state:
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o : Ordinal.{u}
⊢ Principal op (nfp (fun o' => o'.blsub₂ o' fun a x b x => op a b) o)

Tactic:
intro a b ha hb

Result:
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
ha : a < nfp (fun o' => o'.blsub₂ o' fun a x b x => op a b) o
hb : b < nfp (fun o' => o'.blsub₂ o' fun a x b x => op a b) o
⊢ op a b < nfp (fun o' => o'.blsub₂ o' fun a x b x => op a b) o

Proof state:
case h
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
⊢ op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n + 1] o

Tactic:
rw [Function.iterate_succ']

Result:
case h
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
⊢ op a b < ((fun o' => o'.blsub₂ o' fun a x b x => op a b) ∘ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n]) o

Proof state:
case intro
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
hb : ∃ n, b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
⊢ ∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o

Tactic:
obtain ⟨n, hn⟩ := hb

Result:
case intro.intro
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
⊢ ∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o

Proof state:
case h
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
⊢ op a b < ((fun o' => o'.blsub₂ o' fun a x b x => op a b) ∘ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m]) o

Tactic:
exact lt_blsub₂ (@fun a _ b _ => op a b) hm (hn.trans_le h)

Result:
no goals

Proof state:
case intro.intro
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
⊢ ∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o

Tactic:
rcases le_total
  ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[m] o)
  ((fun o' => blsub₂.{u, u, u} o' o' (@fun a _ b _ => op a b))^[n] o) with h | h

Result:
case intro.intro.inl
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
⊢ ∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o

case intro.intro.inr
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
⊢ ∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o

Proof state:
case intro.intro.inr
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
⊢ ∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o

Tactic:
use m + 1

Result:
case h
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
n : ℕ
hn : b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
h : (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o ≤ (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
⊢ op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m + 1] o

Proof state:
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
ha : ∃ n, a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
hb : ∃ n, b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
⊢ ∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o

Tactic:
obtain ⟨m, hm⟩ := ha

Result:
case intro
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
o a b : Ordinal.{u}
hb : ∃ n, b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o
m : ℕ
hm : a < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[m] o
⊢ ∃ n, op a b < (fun o' => o'.blsub₂ o' fun a x b x => op a b)^[n] o