Theorem: List.mapM_eq_some (Lean4Lean/Std/Basic.lean)

State before:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
l' : List β
⊢ mapM f l = some l' ↔ Forall₂ (fun x x_1 => f x = some x_1) l l'
Tactic:
induction l generalizing l' <;>
  simp [List.mapM_nil, List.mapM_cons, bind, List.forall₂_cons_left_iff, *, pure, @eq_comm _ l']
State after:
no goals