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

State before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 <ₛ 𝐆𝐋
Tactic:
dsimp [StrictReducible]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ≤ₛ 𝐆𝐋 ∧ ¬𝐆𝐋 ≤ₛ 𝐊𝟒

State before:
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ≤ₛ 𝐆𝐋 ∧ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
Tactic:
constructor
State after:
case left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ≤ₛ 𝐆𝐋

case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒

State before:
case left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ≤ₛ 𝐆𝐋

case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
Tactic:
. apply reducible_K4_GL;
State after:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒

State before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
Tactic:
. simp [System.not_reducible_iff];
  existsi (Axioms.L (atom default))
  constructor;
  . exact axiomL!;
  . exact unprovable_AxiomL_K4;
State after:
no goals

State before:
case left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ≤ₛ 𝐆𝐋
Tactic:
apply reducible_K4_GL
State after:
no goals

State before:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ¬𝐆𝐋 ≤ₛ 𝐊𝟒
Tactic:
simp [System.not_reducible_iff]
State after:
case right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ ∃ f, 𝐆𝐋 ⊢! f ∧ 𝐊𝟒 ⊬! f

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

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

case right.right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ⊬! Axioms.L (atom default)

State before:
case right.left
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐆𝐋 ⊢! Axioms.L (atom default)

case right.right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ⊬! Axioms.L (atom default)
Tactic:
. exact axiomL!;
State after:
case right.right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ⊬! Axioms.L (atom default)

State before:
case right.right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ⊬! Axioms.L (atom default)
Tactic:
. exact unprovable_AxiomL_K4;
State after:
no goals

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

State before:
case right.right
α : Type u_1
inst✝¹ : DecidableEq α
p : Formula α
inst✝ : Inhabited α
⊢ 𝐊𝟒 ⊬! Axioms.L (atom default)
Tactic:
exact unprovable_AxiomL_K4
State after:
no goals