Theorem: LO.Modal.Standard.reducible_S4_S4Grz (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:
simp only [Set.subset_union_left]
State after:
no goals