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

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
⊢ p ∈ Ω.theory ∨ ~p ∈ Ω.theory
Tactic:
by_contra hC
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : ¬(p ∈ Ω.theory ∨ ~p ∈ Ω.theory)
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : ¬(p ∈ Ω.theory ∨ ~p ∈ Ω.theory)
⊢ False
Tactic:
push_neg at hC
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
⊢ False
Tactic:
cases either_consistent Ω.consistent p with
| inl h => have := Ω.maximal (Set.ssubset_insert hC.1); contradiction;
| inr h => have := Ω.maximal (Set.ssubset_insert hC.2); contradiction;
State after:
no goals

State before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert p Ω.theory
⊢ False
Tactic:
have := Ω.maximal (Set.ssubset_insert hC.1)
State after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert p Ω.theory
this : ¬(L)-Consistent insert p Ω.theory
⊢ False

State before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert p Ω.theory
this : ¬(L)-Consistent insert p Ω.theory
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert (~p) Ω.theory
⊢ False
Tactic:
have := Ω.maximal (Set.ssubset_insert hC.2)
State after:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert (~p) Ω.theory
this : ¬(L)-Consistent insert (~p) Ω.theory
⊢ False

State before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
Ω✝ Ω₁ Ω₂ : MCT L
p✝ : Formula α
Ω : MCT L
p : Formula α
hC : p ∉ Ω.theory ∧ ~p ∉ Ω.theory
h : (L)-Consistent insert (~p) Ω.theory
this : ¬(L)-Consistent insert (~p) Ω.theory
⊢ False
Tactic:
contradiction
State after:
no goals