M Yields m Tr

@[scoped grind =]theorem mYields_mTr {m : SingleTapeNTM State Symbol} :    m.MYields c c' ↔ ∃ μs, m.MTr c.state μs c'.state ∧    μs.foldl TrLabel.applyToTape (some c.tape) = c'.tape := by  apply Iff.intro <;> intro h  case mp =>    induction h using Relation.ReflTransGen.head_induction_on    case refl =>      exists []      grind    case head _ c cb hred hmred ih =>      rcases ih with ⟨μs, hmtr, ih⟩      have ⟨μ, _⟩ := yields_tr.mp hred      exists μ :: μs      grind  case mpr =>    rcases h with ⟨μs, hmtr, h⟩    induction μs generalizing c    case nil =>      rw [show c = c' by grind [Cfg.ext]]      apply Relation.ReflTransGen.refl    case cons μ μs ih =>      cases hmtr      case stepL sb htr hmtr =>        have hat : ∀ (μ : TrLabel Symbol) t, (μ.applyToTape t).isSome → t.isSome := by grind        have ⟨tb, htb⟩ : ∃ tb, μ.applyToTape c.tape = some tb := by grind [Option.isSome_iff_exists]        let cb := {state := sb, tape := tb : Cfg State Symbol}        have hmyields : m.MYields cb c' := by grind        apply Relation.ReflTransGen.head (b := cb) (by grind)        simp only [MYields] at hmyields        grind