α : Type u_1
β : Type ?u.7670
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ∃ t, IsChain r s ∧ SuperChain r s t
this : IsChain r s ∧ SuperChain r s (choose h)
⊢ SuperChain r s (SuccChain r s)
α : Type u_1
β : Type ?u.7670
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ∃ t, IsChain r s ∧ SuperChain r s t
⊢ SuperChain r s (SuccChain r s)
have : IsChain r s ∧ SuperChain r s (choose h) :=
  @choose_spec _ (fun t => IsChain r s ∧ SuperChain r s t) _
no goals
α : Type u_1
β : Type ?u.7670
r : α → α → Prop
c c₁ c₂ c₃ s t : Set α
a b x y : α
h : ∃ t, IsChain r s ∧ SuperChain r s t
this : IsChain r s ∧ SuperChain r s (choose h)
⊢ SuperChain r s (SuccChain r s)
simpa [SuccChain, dif_pos, exists_and_left.mp h] using this.2