case pos
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort ?u.5191
hb : IsSuccLimit b
ha : a < b
h : IsMax a
⊢ succ a < b

case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort ?u.5191
hb : IsSuccLimit b
ha : a < b
h : ¬IsMax a
⊢ succ a < b
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort ?u.5191
hb : IsSuccLimit b
ha : a < b
⊢ succ a < b
by_cases h : IsMax a
no goals
case pos
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort ?u.5191
hb : IsSuccLimit b
ha : a < b
h : IsMax a
⊢ succ a < b
rwa [h.succ_eq]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort ?u.5191
hb : IsSuccLimit b
ha : a < b
h : ¬IsMax a
⊢ a < b ∧ succ a ≠ b
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort ?u.5191
hb : IsSuccLimit b
ha : a < b
h : ¬IsMax a
⊢ succ a < b
rw [lt_iff_le_and_ne, succ_le_iff_of_not_isMax h]
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort ?u.5191
hb : IsSuccLimit b
ha : a < b
h : ¬IsMax a
hab : succ a = b
⊢ False
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort ?u.5191
hb : IsSuccLimit b
ha : a < b
h : ¬IsMax a
⊢ a < b ∧ succ a ≠ b
refine' ⟨ha, fun hab => _⟩
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
C : α → Sort ?u.5191
h : ¬IsMax a
hb : IsSuccLimit (succ a)
ha : a < succ a
⊢ False
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort ?u.5191
hb : IsSuccLimit b
ha : a < b
h : ¬IsMax a
hab : succ a = b
⊢ False
subst hab
no goals
case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
C : α → Sort ?u.5191
h : ¬IsMax a
hb : IsSuccLimit (succ a)
ha : a < succ a
⊢ False
exact (h hb.isMax).elim