Theorem: LO.Modal.Standard.equivalent_GL_K4Loeb (Logic/Modal/Standard/Deduction.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 =ₛ 𝐊𝟒(𝐋)
Tactic:
apply Equiv.antisymm_iff.mpr
State after:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋) ∧ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋

State before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋) ∧ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋
Tactic:
constructor
State after:
case left
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋)

case right
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋

State before:
case left
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋)

case right
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋
Tactic:
. exact reducible_GL_K4Loeb;
State after:
case right
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋

State before:
case right
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋
Tactic:
. exact Reducible.trans (reducible_K4Loeb_K4Henkin) $ Reducible.trans reducible_K4Henkin_K4H reducible_K4Henkin_GL
State after:
no goals

State before:
case left
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐆𝐋 ≤ₛ 𝐊𝟒(𝐋)
Tactic:
exact reducible_GL_K4Loeb
State after:
no goals

State before:
case right
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒(𝐋) ≤ₛ 𝐆𝐋
Tactic:
exact Reducible.trans (reducible_K4Loeb_K4Henkin) $ Reducible.trans reducible_K4Henkin_K4H reducible_K4Henkin_GL
State after:
no goals