Theorem: LO.Modal.Standard.reducible_S4_S5 (Logic/Modal/Standard/Kripke/Geach/Reducible.lean)

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ 𝐒𝟒 ≤ₛ 𝐒𝟓
Tactic:
apply reducible_of_geach_defnability
State after:
case hs
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ ∀ {F : Frame},
    MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟓) F →
      MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟒) F

State before:
case hs
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ ∀ {F : Frame},
    MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟓) F →
      MultiGeachConfluent (DeductionParameter.IsGeach.taples 𝐒𝟒) F
Tactic:
simp_all [trans_of_refl_eucl]
State after:
no goals