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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ⊬! Axioms.L (atom default)
Tactic:
apply not_imp_not.mpr trivTranslated_of_K4
State after:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ⊢! (Axioms.L (atom default)ᵀᴾ) ⋯

State before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐂𝐥 ⊢! (Axioms.L (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.L (atom default)ᵀᴾ) ⋯

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ V, ¬V ⊧ (Axioms.L (atom default)ᵀᴾ) ⋯
Tactic:
simp [Axioms.L, TrivTranslation, 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