Theorem: SizedArray.map_eq_mapM (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map f x = mapM f x
⊢ map f (push x a) = mapM f (push x a)
Tactic:
rw [map_push, mapM_push, IH]
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map f x = mapM f x
⊢ push (mapM f x) (f a) = do
    let y ← mapM f x
    let b ← f a
    pure (push y b)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
f : α → β
x✝ : SizedArray α n
n✝ : Nat
x : SizedArray α n✝
a : α
IH : map f x = mapM f x
⊢ push (mapM f x) (f a) = do
    let y ← mapM f x
    let b ← f a
    pure (push y b)
Tactic:
rfl
State after:
no goals