Is Bisimulation Up To is Bisimulation

@[scoped grind →]theorem IsBisimulationUpTo.isBisimulation (h : IsBisimulationUpTo lts₁ lts₂ r) :    IsBisimulation lts₁ lts₂ (UpToHomBisimilarity lts₁ lts₂ r) := by  intro s₁ s₂ hr μ  rcases hr with ⟨s₁b, hr1b, s₂b, hrb, hr2b⟩  constructor  case left =>    intro s₁' htr1    obtain ⟨s₁b', hs₁b'tr, hs₁b'r⟩ := hr1b.follow_fst htr1    obtain ⟨s₂b', hs₂b'tr, hs₂b'r⟩ := (h hrb μ).1 s₁b' hs₁b'tr    obtain ⟨s₂', hs₂btr, hs₂br⟩ := hr2b.follow_fst hs₂b'tr    use s₂', hs₂btr    obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs₂b'r    use smid1, hs₁b'r.trans hsmidb, smid2, hsmidr    exact hsmidrb.trans hs₂br  case right =>    intro s₂' htr2    obtain ⟨s₂b', hs₂b'tr, hs₂b'r⟩ := hr2b.follow_snd htr2    obtain ⟨s₁b', hs₁b'tr, hs₁b'r⟩ := (h hrb μ).2 s₂b' hs₂b'tr    obtain ⟨s₁', hs₁btr, hs₁br⟩ := hr1b.follow_snd hs₁b'tr    use s₁', hs₁btr    obtain ⟨smid1, hsmidb, smid2, hsmidr, hsmidrb⟩ := hs₁b'r    use smid1, hs₁br.trans hsmidb, smid2, hsmidr    exact hsmidrb.trans hs₂b'r