have : f a = g a := hf a (by simp)
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
this : mapM' f as = mapM' g as
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)
case cons
α✝ : Type u
inst✝² : DecidableEq α✝
β✝ : Type v
inst✝¹ : DecidableEq β✝
m : Type u_3 → Type u_2
α : Type u_1
β : Type u_3
inst✝ : Monad m
f g : α → m β
a : α
as : List α
ih : (∀ a ∈ as, f a = g a) → mapM' f as = mapM' g as
hf : ∀ a_1 ∈ a :: as, f a_1 = g a_1
this✝ : mapM' f as = mapM' g as
this : f a = g a
⊢ (do
      let __do_lift ← f a
      let __do_lift_1 ← mapM' f as
      pure (__do_lift :: __do_lift_1)) =
    do
    let __do_lift ← g a
    let __do_lift_1 ← mapM' g as
    pure (__do_lift :: __do_lift_1)