obtain ⟨U, hUc, hUs⟩ :=
  Set.subset_mem_chain_of_finite c hnc chain
    (s := ↑Γ.toFinset) (by simp)
    (by intro p hp; simp_all)
case left.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
⊢ False
case left.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {T | (L)-Consistent T}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
Γ : List (Formula α)
hC : ¬((∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥)
hΓs : ∀ p ∈ Γ, ∃ t ∈ c, p ∈ t
hΓd : L ⊢! Γ.conj' ⟶ ⊥
U : Set (Formula α)
hUc : U ∈ c
hUs : ↑Γ.toFinset ⊆ U
⊢ False