Theorem: LO.Modal.Standard.Theory.exists_maximal_Lconsistent_theory (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
⊢ ∀ c ⊆ {T | (L)-Consistent T},
    IsChain (fun x x_1 => x ⊆ x_1) c → c.Nonempty → ∃ ub ∈ {T | (L)-Consistent T}, ∀ s ∈ c, s ⊆ ub
Tactic:
intro c hc chain hnc
State after:
α : 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
⊢ ∃ ub ∈ {T | (L)-Consistent T}, ∀ s ∈ c, s ⊆ ub

State before:
α : 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
⊢ ∃ ub ∈ {T | (L)-Consistent T}, ∀ s ∈ c, s ⊆ ub
Tactic:
existsi (⋃₀ c)
State after:
α : 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
⊢ ⋃₀ c ∈ {T | (L)-Consistent T} ∧ ∀ s ∈ c, s ⊆ ⋃₀ c

State before:
α : 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
⊢ ⋃₀ c ∈ {T | (L)-Consistent T} ∧ ∀ s ∈ c, s ⊆ ⋃₀ c
Tactic:
simp only [ParametricConsistent, Set.mem_setOf_eq, Set.mem_sUnion]
State after:
α : 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 α)}, (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥) ∧ ∀ s ∈ c, s ⊆ ⋃₀ c

State before:
α : 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 α)}, (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥) ∧ ∀ s ∈ c, s ⊆ ⋃₀ c
Tactic:
constructor
State after:
case left
α : 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 α)}, (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥

case right
α : 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
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c

State before:
case left
α : 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 α)}, (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥

case right
α : 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
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c
Tactic:
. intro Γ;
  by_contra hC;
  obtain ⟨hΓs, hΓd⟩ := by simpa using hC;
  obtain ⟨U, hUc, hUs⟩ :=
    Set.subset_mem_chain_of_finite c hnc chain
      (s := ↑Γ.toFinset) (by simp)
      (by intro p hp; simp_all);
  simp [List.coe_toFinset] at hUs;
  have : (L)-Consistent U := hc hUc;
  have : ¬(L)-Consistent U := by
    simp only [ParametricConsistent, not_forall, not_not, exists_prop];
    existsi Γ;
    constructor;
    . intro p hp; exact hUs hp;
    . assumption;
  contradiction;
State after:
case right
α : 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
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c

State before:
case right
α : 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
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c
Tactic:
. intro s a;
  exact Set.subset_sUnion_of_mem a;
State after:
no goals

State before:
case left
α : 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 α)}, (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
intro Γ
State after:
case left
α : 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 α)
⊢ (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥

State before:
case left
α : 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 α)
⊢ (∀ p ∈ Γ, ∃ t ∈ c, p ∈ t) → L ⊬! Γ.conj' ⟶ ⊥
Tactic:
by_contra hC
State after:
case left
α : 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' ⟶ ⊥)
⊢ False

State before:
case left
α : 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' ⟶ ⊥)
⊢ False
Tactic:
obtain ⟨hΓs, hΓd⟩ := by simpa using hC;
State after:
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

State before:
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
Tactic:
obtain ⟨U, hUc, hUs⟩ :=
  Set.subset_mem_chain_of_finite c hnc chain
    (s := ↑Γ.toFinset) (by simp)
    (by intro p hp; simp_all)
State after:
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

State before:
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
Tactic:
simp [List.coe_toFinset] at hUs
State after:
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 : {a | a ∈ Γ} ⊆ U
⊢ False

State before:
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 : {a | a ∈ Γ} ⊆ U
⊢ False
Tactic:
have : (L)-Consistent U := hc hUc
State after:
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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ False

State before:
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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ False
Tactic:
have : ¬(L)-Consistent U := by
  simp only [ParametricConsistent, not_forall, not_not, exists_prop];
  existsi Γ;
  constructor;
  . intro p hp; exact hUs hp;
  . assumption;
State after:
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 : {a | a ∈ Γ} ⊆ U
this✝ : (L)-Consistent U
this : ¬(L)-Consistent U
⊢ False

State before:
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 : {a | a ∈ Γ} ⊆ U
this✝ : (L)-Consistent U
this : ¬(L)-Consistent U
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
α : 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' ⟶ ⊥)
⊢ ?m.149979
Tactic:
simpa using hC
State after:
no goals

State before:
α : 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' ⟶ ⊥
⊢ (↑Γ.toFinset).Finite
Tactic:
simp
State after:
no goals

State before:
α : 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' ⟶ ⊥
⊢ ↑Γ.toFinset ⊆ ⋃₀ c
Tactic:
intro p hp
State after:
α : 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' ⟶ ⊥
p : Formula α
hp : p ∈ ↑Γ.toFinset
⊢ p ∈ ⋃₀ c

State before:
α : 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' ⟶ ⊥
p : Formula α
hp : p ∈ ↑Γ.toFinset
⊢ p ∈ ⋃₀ c
Tactic:
simp_all
State after:
no goals

State before:
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ ¬(L)-Consistent U
Tactic:
simp only [ParametricConsistent, not_forall, not_not, exists_prop]
State after:
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ ∃ x, (∀ p ∈ x, p ∈ U) ∧ L ⊢! x.conj' ⟶ ⊥

State before:
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ ∃ x, (∀ p ∈ x, p ∈ U) ∧ L ⊢! x.conj' ⟶ ⊥
Tactic:
existsi Γ
State after:
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ (∀ p ∈ Γ, p ∈ U) ∧ L ⊢! Γ.conj' ⟶ ⊥

State before:
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ (∀ p ∈ Γ, p ∈ U) ∧ L ⊢! Γ.conj' ⟶ ⊥
Tactic:
constructor
State after:
case left
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ ∀ p ∈ Γ, p ∈ U

case right
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ L ⊢! Γ.conj' ⟶ ⊥

State before:
case left
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ ∀ p ∈ Γ, p ∈ U

case right
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ L ⊢! Γ.conj' ⟶ ⊥
Tactic:
. intro p hp; exact hUs hp;
State after:
case right
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ L ⊢! Γ.conj' ⟶ ⊥

State before:
case right
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ L ⊢! Γ.conj' ⟶ ⊥
Tactic:
. assumption;
State after:
no goals

State before:
case left
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ ∀ p ∈ Γ, p ∈ U
Tactic:
intro p hp
State after:
case left
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
p : Formula α
hp : p ∈ Γ
⊢ p ∈ U

State before:
case left
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
p : Formula α
hp : p ∈ Γ
⊢ p ∈ U
Tactic:
exact hUs hp
State after:
no goals

State before:
case right
α : 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 : {a | a ∈ Γ} ⊆ U
this : (L)-Consistent U
⊢ L ⊢! Γ.conj' ⟶ ⊥
Tactic:
assumption
State after:
no goals

State before:
case right
α : 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
⊢ ∀ s ∈ c, s ⊆ ⋃₀ c
Tactic:
intro s a
State after:
case right
α : 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
s : Set (Formula α)
a : s ∈ c
⊢ s ⊆ ⋃₀ c

State before:
case right
α : 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
s : Set (Formula α)
a : s ∈ c
⊢ s ⊆ ⋃₀ c
Tactic:
exact Set.subset_sUnion_of_mem a
State after:
no goals