Halting step unique

lemma halting_step_unique    {tm : MultiTapeTM k Symbol State}    {input : List Symbol}    {t₁ t₂ : ℕ}    (h_halts₁ : tm.haltsAtStep input t₁)    (h_halts₂ : tm.haltsAtStep input t₂) :    t₁ = t₂ := by  wlog h : t₁ ≤ t₂  · exact (this h_halts₂ h_halts₁ (Nat.le_of_not_le h)).symm  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le h  cases d with  | zero => rfl  | succ d =>    have halts₁ : (tm.step^[t₁] (tm.initCfg input)).state = none := by      simp [haltsAtStep, configs] at h_halts₁      exact h_halts₁.left    have halts₂ : (tm.step^[d + t₁] (tm.initCfg input)).state ≠ none := by      grind [haltsAtStep, configs]    refine absurd ?_ halts₂    rw [Function.iterate_add_apply, tm.iter_step_eq_of_halt halts₁]    exact halts₁