α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort ?u.4246
⊢ (∃ b, b ⋖ a) ↔ ∃ b, ¬IsMax b ∧ succ b = a
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort ?u.4246
⊢ ¬IsSuccLimit a ↔ ∃ b, ¬IsMax b ∧ succ b = a
rw [not_isSuccLimit_iff_exists_covby]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort ?u.4246
b : α
⊢ ¬IsMax b ∧ succ b = a → b ⋖ a
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
C : α → Sort ?u.4246
⊢ (∃ b, b ⋖ a) ↔ ∃ b, ¬IsMax b ∧ succ b = a
refine' exists_congr fun b => ⟨fun hba => ⟨hba.lt.not_isMax, (Covby.succ_eq hba)⟩, _⟩
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b✝ : α
C : α → Sort ?u.4246
b : α
h : ¬IsMax b
⊢ b ⋖ succ b
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b✝ : α
C : α → Sort ?u.4246
b : α
⊢ ¬IsMax b ∧ succ b = a → b ⋖ a
rintro ⟨h, rfl⟩
no goals
case intro
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b✝ : α
C : α → Sort ?u.4246
b : α
h : ¬IsMax b
⊢ b ⋖ succ b
exact covby_succ_of_not_isMax h