α : Type u
r : α → α → Prop
a b : α
hb : Acc r b
h : r a b
⊢ succ (rank (_ : Acc r a)) ≤ sup fun b_1 => succ (rank (_ : Acc r ↑b_1))
α : Type u
r : α → α → Prop
a b : α
hb : Acc r b
h : r a b
⊢ succ (rank (_ : Acc r a)) ≤ rank hb
rw [hb.rank_eq]
α : Type u
r : α → α → Prop
a b : α
hb : Acc r b
h : r a b
⊢ succ (rank (_ : Acc r a)) ≤ succ (rank (_ : Acc r ↑{ val := a, property := h }))
α : Type u
r : α → α → Prop
a b : α
hb : Acc r b
h : r a b
⊢ succ (rank (_ : Acc r a)) ≤ sup fun b_1 => succ (rank (_ : Acc r ↑b_1))
refine' le_trans _ (Ordinal.le_sup _ ⟨a, h⟩)
no goals
α : Type u
r : α → α → Prop
a b : α
hb : Acc r b
h : r a b
⊢ succ (rank (_ : Acc r a)) ≤ succ (rank (_ : Acc r ↑{ val := a, property := h }))
rfl