case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort ?u.4712
h : ¬IsSuccLimit a
b : α
hb : ¬IsMax b ∧ succ b = a
⊢ a ∈ range succ
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort ?u.4712
h : ¬IsSuccLimit a
⊢ a ∈ range succ
cases' not_isSuccLimit_iff.1 h with b hb
no goals
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort ?u.4712
h : ¬IsSuccLimit a
b : α
hb : ¬IsMax b ∧ succ b = a
⊢ a ∈ range succ
exact ⟨b, hb.2⟩