-- Mathlib/SetTheory/Ordinal/Rank.lean
theorem mem_range_rank_of_le {o : Ordinal} (ha : Acc r a) (ho : o ≤ ha.rank) :
    ∃ (b : α) (hb : Acc r b), hb.rank = o

Proof state:
case inr
α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho✝ : o ≤ ha.rank
ho : o < ha.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Tactic:
revert ho

Result:
case inr
α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho : o ≤ ha.rank
⊢ o < ha.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o

Proof state:
case inr.intro.mk.inl
α : Type u
a✝ : α
r : α → α → Prop
ha✝ : Acc r a✝
a : α
ha : ∀ (y : α), r y a → Acc r y
b : α
hb : r b a
ho✝ : ⋯.rank ≤ ha✝.rank
IH : ∀ (y : α) (a_1 : r y a), ⋯.rank < ⋯.rank → ∃ b_1, ∃ (hb_1 : Acc r b_1), hb_1.rank = ⋯.rank
ho : ⋯.rank ≤ ⋯.rank
⊢ ∃ b_1, ∃ (hb_1 : Acc r b_1), hb_1.rank = ⋯.rank

case inr.intro.mk.inr
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝¹ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
b : α
hb : r b a
ho✝ : o ≤ ⋯.rank
ho : o < ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Tactic:
exacts [⟨b, ha b hb, rfl⟩, IH _ hb ho]

Result:
no goals

Proof state:
case inr.intro.mk
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
b : α
hb : r b a
ho : o ≤ ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Tactic:
obtain rfl | ho := ho.eq_or_lt

Result:
case inr.intro.mk.inl
α : Type u
a✝ : α
r : α → α → Prop
ha✝ : Acc r a✝
a : α
ha : ∀ (y : α), r y a → Acc r y
b : α
hb : r b a
ho✝ : ⋯.rank ≤ ha✝.rank
IH : ∀ (y : α) (a_1 : r y a), ⋯.rank < ⋯.rank → ∃ b_1, ∃ (hb_1 : Acc r b_1), hb_1.rank = ⋯.rank
ho : ⋯.rank ≤ ⋯.rank
⊢ ∃ b_1, ∃ (hb_1 : Acc r b_1), hb_1.rank = ⋯.rank

case inr.intro.mk.inr
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝¹ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
b : α
hb : r b a
ho✝ : o ≤ ⋯.rank
ho : o < ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Proof state:
case inr
α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho : o ≤ ha.rank
⊢ o < ha.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o

Tactic:
refine ha.recOn fun a ha IH ho ↦ ?_

Result:
case inr
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
ho : o < ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Proof state:
case inr
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
ho : ∃ i, o < Order.succ ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Tactic:
obtain ⟨⟨b, hb⟩, ho⟩ := ho

Result:
case inr.intro.mk
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
b : α
hb : r b a
ho : o < Order.succ ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Proof state:
case inr.intro.mk
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
b : α
hb : r b a
ho : o < Order.succ ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Tactic:
rw [Order.lt_succ_iff] at ho

Result:
case inr.intro.mk
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
b : α
hb : r b a
ho : o ≤ ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Proof state:
case inl
α : Type u
a : α
r : α → α → Prop
ha : Acc r a
ho : ha.rank ≤ ha.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = ha.rank

Tactic:
exact ⟨a, ha, rfl⟩

Result:
no goals

Proof state:
case inr
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
ho : o < ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Tactic:
rw [rank_eq, Ordinal.lt_iSup_iff] at ho

Result:
case inr
α : Type u
a✝ : α
r : α → α → Prop
o : Ordinal.{u}
ha✝ : Acc r a✝
ho✝ : o ≤ ha✝.rank
a : α
ha : ∀ (y : α), r y a → Acc r y
IH : ∀ (y : α) (a : r y a), o < ⋯.rank → ∃ b, ∃ (hb : Acc r b), hb.rank = o
ho : ∃ i, o < Order.succ ⋯.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Proof state:
α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho : o ≤ ha.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o

Tactic:
obtain rfl | ho := ho.eq_or_lt

Result:
case inl
α : Type u
a : α
r : α → α → Prop
ha : Acc r a
ho : ha.rank ≤ ha.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = ha.rank

case inr
α : Type u
a : α
r : α → α → Prop
o : Ordinal.{u}
ha : Acc r a
ho✝ : o ≤ ha.rank
ho : o < ha.rank
⊢ ∃ b, ∃ (hb : Acc r b), hb.rank = o