case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b✝ : α
C : α → Sort ?u.17064
h : ¬IsPredLimit a
b : α
hb : ¬IsMin b ∧ pred b = a
⊢ a ∈ range pred
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b : α
C : α → Sort ?u.17064
h : ¬IsPredLimit a
⊢ a ∈ range pred
cases' not_isPredLimit_iff.1 h with b hb
no goals
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : PredOrder α
a b✝ : α
C : α → Sort ?u.17064
h : ¬IsPredLimit a
b : α
hb : ¬IsMin b ∧ pred b = a
⊢ a ∈ range pred
exact ⟨b, hb.2⟩