Theorem: LO.Modal.Standard.MaximalParametricConsistentTheory.exists_maximal_Lconsistented_theory (Logic/Modal/Standard/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
⊢ ∃ Ω, T ⊆ Ω.theory
Tactic:
have ⟨Ω, hΩ₁, hΩ₂, hΩ₃⟩ := exists_maximal_Lconsistent_theory consisT
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
⊢ ∃ Ω, T ⊆ Ω.theory

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
⊢ ∃ Ω, T ⊆ Ω.theory
Tactic:
existsi ⟨
  Ω,
  hΩ₁,
  by
    rintro U ⟨hU₁, hU₂⟩;
    by_contra hC;
    have : U = Ω := hΩ₃ U hC hU₁;
    subst_vars;
    simp at hU₂,
⟩
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
⊢ T ⊆ { theory := Ω, consistent := ⋯, maximal := ⋯ }.theory

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
⊢ T ⊆ { theory := Ω, consistent := ⋯, maximal := ⋯ }.theory
Tactic:
exact hΩ₂
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
⊢ ∀ {U : Theory α}, Ω ⊂ U → ¬(L)-Consistent U
Tactic:
rintro U ⟨hU₁, hU₂⟩
State after:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
U : Theory α
hU₁ : Ω ⊆ U
hU₂ : ¬U ⊆ Ω
⊢ ¬(L)-Consistent U

State before:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
U : Theory α
hU₁ : Ω ⊆ U
hU₂ : ¬U ⊆ Ω
⊢ ¬(L)-Consistent U
Tactic:
by_contra hC
State after:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
U : Theory α
hU₁ : Ω ⊆ U
hU₂ : ¬U ⊆ Ω
hC : (L)-Consistent U
⊢ False

State before:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
U : Theory α
hU₁ : Ω ⊆ U
hU₂ : ¬U ⊆ Ω
hC : (L)-Consistent U
⊢ False
Tactic:
have : U = Ω := hΩ₃ U hC hU₁
State after:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
U : Theory α
hU₁ : Ω ⊆ U
hU₂ : ¬U ⊆ Ω
hC : (L)-Consistent U
this : U = Ω
⊢ False

State before:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
Ω : Theory α
hΩ₁ : (L)-Consistent Ω
hΩ₂ : T ⊆ Ω
hΩ₃ : ∀ (U : Theory α), (L)-Consistent U → Ω ⊆ U → U = Ω
U : Theory α
hU₁ : Ω ⊆ U
hU₂ : ¬U ⊆ Ω
hC : (L)-Consistent U
this : U = Ω
⊢ False
Tactic:
subst_vars
State after:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
U : Theory α
hC hΩ₁ : (L)-Consistent U
hΩ₂ : T ⊆ U
hΩ₃ : ∀ (U_1 : Theory α), (L)-Consistent U_1 → U ⊆ U_1 → U_1 = U
hU₁ : U ⊆ U
hU₂ : ¬U ⊆ U
⊢ False

State before:
case intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω Ω₁ Ω₂ : MCT L
p : Formula α
T : Theory α
consisT : (L)-Consistent T
U : Theory α
hC hΩ₁ : (L)-Consistent U
hΩ₂ : T ⊆ U
hΩ₃ : ∀ (U_1 : Theory α), (L)-Consistent U_1 → U ⊆ U_1 → U_1 = U
hU₁ : U ⊆ U
hU₂ : ¬U ⊆ U
⊢ False
Tactic:
simp at hU₂
State after:
no goals