Theorem: LO.Propositional.Superintuitionistic.Tableau.iff_not_ParametricConsistent_insert₂ (Logic/Propositional/Superintuitionistic/Kripke/Completeness.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ ¬(𝓓)-Consistent (T, insert p U) ↔ ∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
Tactic:
constructor
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ ¬(𝓓)-Consistent (T, insert p U) → ∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬(𝓓)-Consistent (T, insert p U)

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ ¬(𝓓)-Consistent (T, insert p U) → ∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬(𝓓)-Consistent (T, insert p U)
Tactic:
. contrapose; push_neg; apply iff_ParametricConsistent_insert₂.mpr;
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬(𝓓)-Consistent (T, insert p U)

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬(𝓓)-Consistent (T, insert p U)
Tactic:
. contrapose; push_neg; apply iff_ParametricConsistent_insert₂.mp;
State after:
no goals

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ ¬(𝓓)-Consistent (T, insert p U) → ∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
Tactic:
contrapose
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (¬∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬¬(𝓓)-Consistent (T, insert p U)

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (¬∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬¬(𝓓)-Consistent (T, insert p U)
Tactic:
push_neg
State after:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∀ (Γ Δ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → ¬𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') →
    (𝓓)-Consistent (T, insert p U)

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∀ (Γ Δ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → ¬𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') →
    (𝓓)-Consistent (T, insert p U)
Tactic:
apply iff_ParametricConsistent_insert₂.mpr
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj') → ¬(𝓓)-Consistent (T, insert p U)
Tactic:
contrapose
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ ¬¬(𝓓)-Consistent (T, insert p U) → ¬∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ ¬¬(𝓓)-Consistent (T, insert p U) → ¬∃ Γ Δ, (∀ p ∈ Γ, p ∈ T) ∧ (∀ p ∈ Δ, p ∈ U) ∧ 𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
Tactic:
push_neg
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (𝓓)-Consistent (T, insert p U) →
    ∀ (Γ Δ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → ¬𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
T : Theory α
p : Formula α
U : Theory α
⊢ (𝓓)-Consistent (T, insert p U) →
    ∀ (Γ Δ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → (∀ p ∈ Δ, p ∈ U) → ¬𝓓 ⊢! Γ.conj' ⟶ p ⋎ Δ.disj'
Tactic:
apply iff_ParametricConsistent_insert₂.mp
State after:
no goals