Theorem: LO.Propositional.Classical.exists_maximal_consistent_theory (Logic/Propositional/Classical/Basic/Completeness.lean)

State before:
α : 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
⊢ ⋃₀ c ∈ {U | Consistent U}
Tactic:
simp
State after:
α : 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
⊢ Consistent (⋃₀ c)

State before:
α : 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
⊢ Consistent (⋃₀ c)
Tactic:
by_contra A
State after:
α : 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)
⊢ False

State before:
α : 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)
⊢ False
Tactic:
rcases System.inconsistent_compact.mp (System.not_consistent_iff_inconsistent.mp A) with ⟨𝓕, h𝓕, fin, 𝓕_consis⟩
State after:
case 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 𝓕
⊢ False

State before:
case 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 𝓕
⊢ False
Tactic:
rcases Set.subset_mem_chain_of_finite c hnc chain (s := 𝓕) fin h𝓕 with ⟨U, hUc, hsU⟩
State after:
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

State before:
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
Tactic:
have : Consistent U := hc hUc
State after:
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

State before:
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
Tactic:
have : ¬Consistent U := (𝓕_consis.of_supset hsU).not_con
State after:
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
this : ¬Consistent U
⊢ False

State before:
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
this : ¬Consistent U
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
this : ∃ Z, Consistent Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
⊢ ∃ Z, Consistent Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
Tactic:
rcases this with ⟨Z, con, ss, hZ⟩
State after:
case intro.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
Z : Theory α
con : Consistent Z
ss : T ⊆ Z
hZ : ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
⊢ ∃ Z, Consistent Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z

State before:
case intro.intro.intro
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
Z : Theory α
con : Consistent Z
ss : T ⊆ Z
hZ : ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
⊢ ∃ Z, Consistent Z ∧ T ⊆ Z ∧ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
Tactic:
exact ⟨Z, con, ss, by intro U conU ssU; simpa using hZ U conU ssU⟩
State after:
no goals

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
Z : Theory α
con : Consistent Z
ss : T ⊆ Z
hZ : ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
⊢ ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
Tactic:
intro U conU ssU
State after:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
Z : Theory α
con : Consistent Z
ss : T ⊆ Z
hZ : ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
U : Theory α
conU : Consistent U
ssU : Z ⊆ U
⊢ U = Z

State before:
α : Type u_1
Δ : Sequent α
T : Theory α
consisT : Consistent T
Z : Theory α
con : Consistent Z
ss : T ⊆ Z
hZ : ∀ (U : Theory α), Consistent U → Z ⊆ U → U = Z
U : Theory α
conU : Consistent U
ssU : Z ⊆ U
⊢ U = Z
Tactic:
simpa using hZ U conU ssU
State after:
no goals