-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_eq_wfRank : lift.{u + 1, u} (rank x) = IsWellFounded.rank (α := ZFSet) (· ∈ ·) x

Proof state:
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
h : Ordinal.{u + 1}
⊢ h < lift.{u + 1, u} x.rank → h < ⨆ b, succ (lift.{u + 1, u} (↑b).rank)

Tactic:
rw [lt_lift_iff]

Result:
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
h : Ordinal.{u + 1}
⊢ (∃ a' < x.rank, lift.{u + 1, u} a' = h) → h < ⨆ b, succ (lift.{u + 1, u} (↑b).rank)

Proof state:
case intro.intro
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
o : Ordinal.{u}
h : o < x.rank
⊢ lift.{u + 1, u} o < ⨆ b, succ (lift.{u + 1, u} (↑b).rank)

Tactic:
simpa [Ordinal.lt_iSup_iff] using lt_rank_iff.1 h

Result:
no goals

Proof state:
case h
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = ⨆ b, succ (IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) ↑b)

Tactic:
simp_rw [← fun y : { y // y ∈ x } => ih y y.2]

Result:
case h
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = ⨆ b, succ (lift.{u + 1, u} (↑b).rank)

Proof state:
case h
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) x

Tactic:
rw [IsWellFounded.rank_eq]

Result:
case h
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = ⨆ b, succ (IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) ↑b)

Proof state:
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
h : { b // b ∈ x }
⊢ succ (lift.{u + 1, u} (↑h).rank) ≤ lift.{u + 1, u} x.rank

Tactic:
simpa using rank_lt_of_mem h.2

Result:
no goals

Proof state:
case h
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = ⨆ b, succ (lift.{u + 1, u} (↑b).rank)

Tactic:
apply (le_of_forall_lt _).antisymm (Ordinal.iSup_le _) <;> intro h

Result:
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
h : Ordinal.{u + 1}
⊢ h < lift.{u + 1, u} x.rank → h < ⨆ b, succ (lift.{u + 1, u} (↑b).rank)

x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
h : { b // b ∈ x }
⊢ succ (lift.{u + 1, u} (↑h).rank) ≤ lift.{u + 1, u} x.rank

Proof state:
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
h : Ordinal.{u + 1}
⊢ (∃ a' < x.rank, lift.{u + 1, u} a' = h) → h < ⨆ b, succ (lift.{u + 1, u} (↑b).rank)

Tactic:
rintro ⟨o, h, rfl⟩

Result:
case intro.intro
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
o : Ordinal.{u}
h : o < x.rank
⊢ lift.{u + 1, u} o < ⨆ b, succ (lift.{u + 1, u} (↑b).rank)

Proof state:
x : ZFSet.{u}
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) x

Tactic:
induction' x using inductionOn with x ih

Result:
case h
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 => x1 ∈ x2) x