Foldl M of assoc some

public theorem foldlM_of_assoc_some (f : α → α → Option α) (x₀ x₁ x₂ x₃ : α) (xs : List α)  (h₁ : ∀ x₁ x₂ x₃,    (do let x₄ ← f x₁ x₂ ; f x₄ x₃) =    (do let x₄ ← f x₂ x₃ ; f x₁ x₄))  (h₂ : f x₀ x₁ = some x₂)  (h₃ : List.foldlM f x₂ xs = some x₃):  (do let y ← List.foldlM f x₁ xs ; f x₀ y) = some x₃:= by  cases xs  case nil =>    simp only [Option.bind_eq_bind, List.foldlM, pure, Option.some.injEq, Option.bind_some_fun] at *    subst h₃; exact h₂  case cons hd tl =>    simp only [Option.bind_eq_bind, List.foldlM, Option.bind_eq_some_iff] at *    cases h₄ : f x₂ hd <;> simp only [h₄, false_and, exists_false, Option.some.injEq, exists_eq_left', reduceCtorEq] at h₃    case some x₄ =>    have h₅ := h₁ x₀ x₁ hd    simp only [h₂, h₄, Option.bind_some] at h₅    cases h₆ : f x₁ hd <;> simp only [h₆, Option.bind_some, Option.bind_none, reduceCtorEq] at h₅    case some x₅ =>    have h₇ := List.foldlM_of_assoc_some f x₂ hd x₄ x₃ tl h₁ h₄ h₃    cases h₈ : List.foldlM f hd tl <;> simp only [h₈, Option.bind_some_fun, Option.bind_none_fun, reduceCtorEq] at h₇    case some x₆ =>    rw [eq_comm] at h₅    cases h₉ : List.foldlM f x₅ tl <;> simp only [h₉, Option.some.injEq, exists_eq_left']    case none =>      have h₁₀ := List.foldlM_of_assoc_some f x₀ x₅ x₄ x₃ tl h₁ h₅ h₃      simp [h₉] at h₁₀    case some x₇ =>      have h₁₀ := List.foldlM_of_assoc_some f x₁ hd x₅ x₇ tl h₁ h₆ h₉      simp only [h₈, Option.bind_some_fun] at h₁₀      specialize h₁ x₀ x₁ x₆      simp only [h₂, h₁₀, Option.bind_some] at h₁      simp [←h₁, h₇]