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

State before:
α : Type u_1
inst✝ : DecidableEq α
⊢ 𝐊𝟒 ≤ₛ 𝐒𝟒
Tactic:
apply normal_reducible_subset
State after:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐊𝟒) ⊆ Ax(𝐒𝟒)

State before:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
⊢ Ax(𝐊𝟒) ⊆ Ax(𝐒𝟒)
Tactic:
intro
State after:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
a✝ : Formula α
⊢ a✝ ∈ Ax(𝐊𝟒) → a✝ ∈ Ax(𝐒𝟒)

State before:
case hSubset
α : Type u_1
inst✝ : DecidableEq α
a✝ : Formula α
⊢ a✝ ∈ Ax(𝐊𝟒) → a✝ ∈ Ax(𝐒𝟒)
Tactic:
aesop
State after:
no goals