Theorem: LO.Modal.Standard.unprovable_AxiomT_GL (Logic/Modal/Standard/Maximal.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊬! Axioms.T (atom default)
Tactic:
apply not_imp_not.mpr verTranslated_of_GL
State after:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ⊢! (Axioms.T (atom default)ⱽᴾ) ⋯

State before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ⊢! (Axioms.T (atom default)ⱽᴾ) ⋯
Tactic:
apply unprovable_classical_of_exists_ClassicalValuation
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ V, ¬V ⊧ (Axioms.T (atom default)ⱽᴾ) ⋯

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ V, ¬V ⊧ (Axioms.T (atom default)ⱽᴾ) ⋯
Tactic:
simp [Axioms.T, VerTranslation, toPropFormula]
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ V, ¬V default

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ V, ¬V default
Tactic:
use (λ _ => False)
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬False

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬False
Tactic:
trivial
State after:
no goals