rcases f a with (_ | b) <;> simp
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.164904 → Type ?u.164906
α : Type u_3
β : Type u_2
inst✝ : Monad m
γ : Type u_1
a : α
as : List α
ih :
  ∀ {f : α → Option β} {g : β → γ},
    mapM' (fun a => Option.map g (f a)) as = Option.map (fun bs => map g bs) (mapM' f as)
f : α → Option β
g : β → γ
⊢ ((Option.map g (f a)).bind fun a =>
      (Option.map (fun bs => map g bs) (mapM' (fun a => f a) as)).bind fun a_1 => some (a :: a_1)) =
    Option.map (fun bs => map g bs)
      ((f a).bind fun __do_lift => (mapM' f as).bind fun __do_lift_1 => some (__do_lift :: __do_lift_1))
case cons.some
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type ?u.164904 → Type ?u.164906
α : Type u_3
β : Type u_2
inst✝ : Monad m
γ : Type u_1
a : α
as : List α
ih :
  ∀ {f : α → Option β} {g : β → γ},
    mapM' (fun a => Option.map g (f a)) as = Option.map (fun bs => map g bs) (mapM' f as)
f : α → Option β
g : β → γ
b : β
⊢ ((Option.map (fun bs => map g bs) (mapM' (fun a => f a) as)).bind fun a => some (g b :: a)) =
    Option.map (fun bs => map g bs) ((mapM' f as).bind fun __do_lift => some (b :: __do_lift))