Theory Eq is Bisimulation

@[scoped grind ⇒]theorem theoryEq_isBisimulation (lts : LTS State Label)    [image_finite : ∀ s μ, Finite (lts.image s μ)] :    lts.IsHomBisimulation (TheoryEq lts) := by  intro s1 s2 h μ  let (s : State) := @Fintype.ofFinite (lts.image s μ) (image_finite s μ)  constructor  case left =>    intro s1' htr    by_contra    have hdist : ∀ s2' : lts.image s2 μ, ∃ a, Satisfies lts s1' a ∧ ¬Satisfies lts s2'.val a := by      intro ⟨s2', hs2'⟩      apply not_theoryEq_satisfies      grind    choose dist_formula hdist_spec using hdist    let conjunction := Proposition.finiteAnd (propositions dist_formula)    have hs1_diamond : Satisfies lts s1 (.diamond μ conjunction) := by      grind [propositions_satisfies_conjunction]    cases (theoryEq_satisfies h hs1_diamond) with | @diamond _ s2'' _ _ htr2 hsat =>    grind [propositions_complete dist_formula ⟨s2'', htr2⟩]  case right =>    -- Symmetric to left case    intro s2' htr    by_contra    have hdist : ∀ s1' : lts.image s1 μ, ∃ a, Satisfies lts s2' a ∧ ¬Satisfies lts s1'.val a := by      intro ⟨s1', hs1'⟩      apply not_theoryEq_satisfies      grind    choose dist_formula hdist_spec using hdist    let conjunction := Proposition.finiteAnd (propositions dist_formula)    have hs2_diamond : Satisfies lts s2 (.diamond μ conjunction) := by      grind [propositions_satisfies_conjunction]    cases (theoryEq_satisfies h.symm hs2_diamond) with | @diamond _ s1'' _ _ htr1 hsat =>    grind [propositions_complete dist_formula ⟨s1'', htr1⟩]