Map M' some iff forall₂

public theorem mapM'_some_iff_forall₂ {α β} {f : α → Option β} {xs : List α} {ys : List β} :  List.mapM' f xs = .some ys ↔  List.Forall₂ (λ x y => f x = .some y) xs ys:= by  constructor  case mp =>    intro h₁    induction xs generalizing ys    case nil =>      simp only [mapM'_nil, pure] at h₁      injection h₁; rename_i h₁      subst h₁      exact List.Forall₂.nil    case cons xhd xtl ih =>      simp only [mapM'_cons, pure] at h₁      cases h₂ : f xhd <;>      simp only [h₂, Option.bind_eq_bind, Option.bind, Option.bind_none_fun, reduceCtorEq] at h₁      rename_i yhd      cases mapM' f xtl      · split at h₁        . contradiction        . simp at h₁          rename_i a h₂          rw [← h₁]          specialize ih h₂          apply Forall₂.cons          . rename_i h₃ h₄ h₅            exact h₃          . exact ih      · split at h₁        . contradiction        . simp at h₁          rename_i a h₂          rw [← h₁]          specialize ih h₂          apply Forall₂.cons          . rename_i h₃ h₄ h₅ h₆            exact h₃          . exact ih  case mpr =>    intro h₁    induction xs generalizing ys    case nil =>      simp only [forall₂_nil_left_iff] at h₁      simp only [mapM'_nil, pure, h₁]    case cons xhd xtl ih =>      simp only [mapM'_cons, pure]      replace ⟨yhd, ytl, h₁, h₃, h₄⟩ := forall₂_cons_left_iff.mp h₁      subst ys      cases h₂ : f xhd      case none => simp [h₁] at h₂      case some y' =>        simp [h₁] at h₂        specialize ih h₃        simp only [ih]        simp [Option.bind_some_fun, Option.some.injEq, cons.injEq, and_true]        rw [h₂]