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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐒𝟒 ≤ₛ 𝐆𝐋
Tactic:
apply System.not_reducible_iff.mpr
State after:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ f, 𝐒𝟒 ⊢! f ∧ 𝐆𝐋 ⊬! f

State before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ f, 𝐒𝟒 ⊢! f ∧ 𝐆𝐋 ⊬! f
Tactic:
existsi (Axioms.T (atom default))
State after:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐒𝟒 ⊢! Axioms.T (atom default) ∧ 𝐆𝐋 ⊬! Axioms.T (atom default)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐒𝟒 ⊢! Axioms.T (atom default) ∧ 𝐆𝐋 ⊬! Axioms.T (atom default)
Tactic:
constructor
State after:
case left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐒𝟒 ⊢! Axioms.T (atom default)

case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊬! Axioms.T (atom default)

State before:
case left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐒𝟒 ⊢! Axioms.T (atom default)

case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊬! Axioms.T (atom default)
Tactic:
. exact axiomT!;
State after:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊬! Axioms.T (atom default)

State before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊬! Axioms.T (atom default)
Tactic:
. exact unprovable_AxiomT_GL;
State after:
no goals

State before:
case left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐒𝟒 ⊢! Axioms.T (atom default)
Tactic:
exact axiomT!
State after:
no goals

State before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊬! Axioms.T (atom default)
Tactic:
exact unprovable_AxiomT_GL
State after:
no goals