case intro.intro
α β : Type u
a : Cardinal
h✝ : lift (succ a) > succ (lift a)
b : Cardinal
e : lift b = succ (lift a)
h : b < succ a
⊢ False
α β : Type u
a : Cardinal
h : lift (succ a) > succ (lift a)
⊢ False
rcases lt_lift_iff.1 h with ⟨b, e, h⟩
case intro.intro
α β : Type u
a : Cardinal
h✝ : lift (succ a) > succ (lift a)
b : Cardinal
e : lift b = succ (lift a)
h : succ (lift a) ≤ lift a
⊢ False
case intro.intro
α β : Type u
a : Cardinal
h✝ : lift (succ a) > succ (lift a)
b : Cardinal
e : lift b = succ (lift a)
h : b < succ a
⊢ False
rw [lt_succ_iff, ← lift_le, e] at h
no goals
case intro.intro
α β : Type u
a : Cardinal
h✝ : lift (succ a) > succ (lift a)
b : Cardinal
e : lift b = succ (lift a)
h : succ (lift a) ≤ lift a
⊢ False
exact h.not_lt (lt_succ _)