α : Type u_1
β : Type ?u.8828
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
⊢ SuperChain r s (SuccChain r s)
α : Type u_1
β : Type ?u.8828
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs₁ : IsChain r s
hs₂ : ¬IsMaxChain r s
⊢ SuperChain r s (SuccChain r s)
simp only [IsMaxChain, not_and, not_forall, exists_prop, exists_and_left] at hs₂
case intro.intro
α : Type u_1
β : Type ?u.8828
r : α → α → Prop
c c₁ c₂ c₃ s t✝ : Set α
a b x y : α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
t : Set α
ht : IsChain r t
hst : s ⊆ t ∧ ¬s = t
⊢ SuperChain r s (SuccChain r s)
α : Type u_1
β : Type ?u.8828
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
⊢ SuperChain r s (SuccChain r s)
obtain ⟨t, ht, hst⟩ := hs₂ hs₁
no goals
case intro.intro
α : Type u_1
β : Type ?u.8828
r : α → α → Prop
c c₁ c₂ c₃ s t✝ : Set α
a b x y : α
hs₁ : IsChain r s
hs₂ : IsChain r s → ∃ x, IsChain r x ∧ s ⊆ x ∧ ¬s = x
t : Set α
ht : IsChain r t
hst : s ⊆ t ∧ ¬s = t
⊢ SuperChain r s (SuccChain r s)
exact succChain_spec ⟨t, hs₁, ht, ssubset_iff_subset_ne.2 hst⟩