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

State before:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
⊢ 𝐒𝟓 =ₛ 𝐊𝐓𝟒𝐁
Tactic:
apply equiv_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:
intros
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:
constructor <;> simp_all [symm_of_refl_eucl, trans_of_refl_eucl, eucl_of_symm_trans]
State after:
no goals