Theorem: List.mapM'_option_map (Logic/Vorspiel/Vorspiel.lean)

State before:
α✝ : 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
f : α → Option β
g : β → γ
as : List α
⊢ mapM' (fun a => Option.map g (f a)) as = Option.map (fun bs => map g bs) (mapM' f as)
Tactic:
induction' as with a as ih generalizing f g <;> simp[Option.pure_eq_some, Option.bind_eq_bind, Function.comp]
State after:
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 __do_lift =>
      (mapM' (fun a => Option.map g (f a)) as).bind fun __do_lift_1 => some (__do_lift :: __do_lift_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))

State before:
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 __do_lift =>
      (mapM' (fun a => Option.map g (f a)) as).bind fun __do_lift_1 => some (__do_lift :: __do_lift_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))
Tactic:
{ simp[ih]
  rcases f a with (_ | b) <;> simp
  rcases mapM' f as with (_ | bs) <;> simp }
State after:
no goals

State before:
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 __do_lift =>
      (mapM' (fun a => Option.map g (f a)) as).bind fun __do_lift_1 => some (__do_lift :: __do_lift_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))
Tactic:
simp[ih]
State after:
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))

State before:
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))
Tactic:
rcases f a with (_ | b) <;> simp
State after:
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))

State before:
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))
Tactic:
rcases mapM' f as with (_ | bs) <;> simp
State after:
no goals