have : Consistent U := hc hUc
case intro.intro.intro.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {U | Consistent U}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
A : ¬Consistent (⋃₀ c)
𝓕 : Theory α
h𝓕 : 𝓕 ⊆ ⋃₀ c
fin : Collection.Finite 𝓕
𝓕_consis : Inconsistent 𝓕
U : Set (Formula α)
hUc : U ∈ c
hsU : 𝓕 ⊆ U
⊢ False
case intro.intro.intro.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
c : Set (Set (Formula α))
hc : c ⊆ {U | Consistent U}
chain : IsChain (fun x x_1 => x ⊆ x_1) c
hnc : c.Nonempty
A : ¬Consistent (⋃₀ c)
𝓕 : Theory α
h𝓕 : 𝓕 ⊆ ⋃₀ c
fin : Collection.Finite 𝓕
𝓕_consis : Inconsistent 𝓕
U : Set (Formula α)
hUc : U ∈ c
hsU : 𝓕 ⊆ U
this : Consistent U
⊢ False