Theorem: LO.Modal.Standard.Theory.either_consistent (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
p : Formula α
⊢ (L)-Consistent insert p T ∨ (L)-Consistent insert (~p) T
Tactic:
by_contra hC
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬((L)-Consistent insert p T ∨ (L)-Consistent insert (~p) T)
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬((L)-Consistent insert p T ∨ (L)-Consistent insert (~p) T)
⊢ False
Tactic:
push_neg at hC
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
⊢ False

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
⊢ False
Tactic:
obtain ⟨Γ, hΓ₁, hΓ₂⟩ := iff_insert_notParametricConsistent.mp hC.1
State after:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False

State before:
case intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Tactic:
obtain ⟨Δ, hΔ₁, hΔ₂⟩ := iff_insert_notParametricConsistent.mp hC.2
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
⊢ False
Tactic:
replace hΓ₂ := NegationEquiv.neg_equiv'!.mp hΓ₂
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
⊢ False
Tactic:
replace hΔ₂ := NegationEquiv.neg_equiv'!.mp hΔ₂
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
⊢ False
Tactic:
have : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥ := demorgan₁'! $ disj₃'! (imp_trans! (implyOfNotOr'! $ demorgan₄'! hΓ₂) disj₁!) (imp_trans! (implyOfNotOr'! $ demorgan₄'! hΔ₂) disj₂!) lem!
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ False
Tactic:
have := @consisT (Γ ++ Δ) (by
  intro q hq;
  simp at hq;
  rcases hq with hΓ | hΔ
  . exact hΓ₁ _ hΓ;
  . exact hΔ₁ _ hΔ;
)
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
⊢ False
Tactic:
have : L ⊬! Γ.conj' ⋏ Δ.conj' ⟶ ⊥ := unprovable_imp_trans! imply_left_concat_conj'! (consisT (by
  simp;
  intro q hq;
  rcases hq with hΓ | hΔ
  . exact hΓ₁ _ hΓ;
  . exact hΔ₁ _ hΔ;
))
State after:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝¹ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
this : L ⊬! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ False

State before:
case intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝¹ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
this : L ⊬! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ 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
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ ∀ p ∈ Γ ++ Δ, p ∈ T
Tactic:
intro q hq
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Γ ++ Δ
⊢ q ∈ T

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Γ ++ Δ
⊢ q ∈ T
Tactic:
simp at hq
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Γ ∨ q ∈ Δ
⊢ q ∈ T

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hq : q ∈ Γ ∨ q ∈ Δ
⊢ q ∈ T
Tactic:
rcases hq with hΓ | hΔ
State after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΓ : q ∈ Γ
⊢ q ∈ T

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T

State before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΓ : q ∈ Γ
⊢ q ∈ T

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Tactic:
. exact hΓ₁ _ hΓ;
State after:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T

State before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Tactic:
. exact hΔ₁ _ hΔ;
State after:
no goals

State before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΓ : q ∈ Γ
⊢ q ∈ T
Tactic:
exact hΓ₁ _ hΓ
State after:
no goals

State before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Tactic:
exact hΔ₁ _ hΔ
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
⊢ ∀ p ∈ Γ ++ Δ, p ∈ T
Tactic:
simp
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
⊢ ∀ (p : Formula α), p ∈ Γ ∨ p ∈ Δ → p ∈ T

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
⊢ ∀ (p : Formula α), p ∈ Γ ∨ p ∈ Δ → p ∈ T
Tactic:
intro q hq
State after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hq : q ∈ Γ ∨ q ∈ Δ
⊢ q ∈ T

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hq : q ∈ Γ ∨ q ∈ Δ
⊢ q ∈ T
Tactic:
rcases hq with hΓ | hΔ
State after:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΓ : q ∈ Γ
⊢ q ∈ T

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T

State before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΓ : q ∈ Γ
⊢ q ∈ T

case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Tactic:
. exact hΓ₁ _ hΓ;
State after:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T

State before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Tactic:
. exact hΔ₁ _ hΔ;
State after:
no goals

State before:
case inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΓ : q ∈ Γ
⊢ q ∈ T
Tactic:
exact hΓ₁ _ hΓ
State after:
no goals

State before:
case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
q : Formula α
hΔ : q ∈ Δ
⊢ q ∈ T
Tactic:
exact hΔ₁ _ hΔ
State after:
no goals