α : Type u
r : α → α → Prop
a b : α
hwf : WellFounded r
⊢ (sup fun b => succ (Acc.rank (_ : Acc r ↑b))) = sup fun b => succ (rank hwf ↑b)
α : Type u
r : α → α → Prop
a b : α
hwf : WellFounded r
⊢ rank hwf a = sup fun b => succ (rank hwf ↑b)
rw [rank, Acc.rank_eq]
no goals
α : Type u
r : α → α → Prop
a b : α
hwf : WellFounded r
⊢ (sup fun b => succ (Acc.rank (_ : Acc r ↑b))) = sup fun b => succ (rank hwf ↑b)
rfl