Totalize nonsink mtr iff

@[simp]theorem totalize.nonsink_mtr_iff {μs : List Label} {s t : State} :    lts.totalize.MTr (some s) μs (some t) ↔ lts.MTr s μs t := by  constructor <;> intro h  · generalize h_s : (some s : Option State) = s'    generalize h_t : (some t : Option State) = t'    rw [h_s, h_t] at h    induction h generalizing s    case refl _ => grind [MTr]    case stepL t1' μ t2' μs t3' h_tr h_mtr h_ind =>      obtain ⟨rfl⟩ := h_s      cases t2'      case some t2 => grind [MTr, totalize.nonsink_tr_iff.mp h_tr]      case none => grind [totalize.no_sink_to_nonsink]  · induction h    case refl _ => grind [MTr]    case stepL t1 μ t2 μs t3 h_tr h_mtr h_ind =>      grind [MTr, totalize.nonsink_tr_iff.mpr h_tr]