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

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

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → ¬(L)-Consistent insert p T

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ ¬(L)-Consistent insert p T → ∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥

case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → ¬(L)-Consistent insert p T
Tactic:
. contrapose; push_neg; apply iff_insert_ParametricConsistent.mpr;
State after:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → ¬(L)-Consistent insert p T

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∃ Γ, (∀ p ∈ Γ, p ∈ T) ∧ L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → ¬(L)-Consistent insert p T
Tactic:
. contrapose; push_neg; apply iff_insert_ParametricConsistent.mp;
State after:
no goals

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

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

State before:
case mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (∀ (Γ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → ¬L ⊢! p ⋏ Γ.conj' ⟶ ⊥) → (L)-Consistent insert p T
Tactic:
apply iff_insert_ParametricConsistent.mpr
State after:
no goals

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

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

State before:
case mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
p : Formula α
⊢ (L)-Consistent insert p T → ∀ (Γ : List (Formula α)), (∀ p ∈ Γ, p ∈ T) → ¬L ⊢! p ⋏ Γ.conj' ⟶ ⊥
Tactic:
apply iff_insert_ParametricConsistent.mp
State after:
no goals