α : Type u_1
β : Type ?u.8171
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs : IsChain r s
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ IsChain r (SuccChain r s)
α : Type u_1
β : Type ?u.8171
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs : IsChain r s
h : ¬∃ t, IsChain r s ∧ SuperChain r s t
⊢ IsChain r (SuccChain r s)
rw [exists_and_left] at h
no goals
α : Type u_1
β : Type ?u.8171
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs : IsChain r s
h : ¬(IsChain r s ∧ ∃ x, SuperChain r s x)
⊢ IsChain r (SuccChain r s)
simpa [SuccChain, dif_neg, h] using hs