Is Simulation is Simulation saturate left

theorem IsSimulation.isSimulation_saturate_left [HasTau Label] {lts₁ : LTS State₁ Label}    {lts₂ : LTS State₂ Label} (h : IsSimulation lts₁ lts₂.saturate r) :    IsSimulation lts₁.saturate lts₂.saturate r := by  intro s₁ s₂ hr μ s₁' h  cases h  case refl =>    use s₂, .refl, hr  case tr sb sb' hstr1 htr hstr2 =>    obtain ⟨sb1, hstr1b, hrb⟩ := IsSimulation.follow_internal h hr hstr1    obtain ⟨sb2', hstr1b', hrb'⟩ := h _ _ hrb μ _ htr    obtain ⟨s₁', hstr1', hrb2⟩ := IsSimulation.follow_internal h hrb' hstr2    rw [←sTr_τSTr_iff] at hstr1' hstr1b    use s₁', STr.comp hstr1b hstr1b' hstr1', hrb2