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

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x✝ : SizedArray α n
n✝ : Nat
a : α
x : SizedArray α n✝
IH : mapM f x = mapMIdx (fun x => f) x
⊢ mapM f (cons a x) = mapMIdx (fun x => f) (cons a x)
Tactic:
rw [mapM_cons, mapMIdx_cons, IH]
State after:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x✝ : SizedArray α n
n✝ : Nat
a : α
x : SizedArray α n✝
IH : mapM f x = mapMIdx (fun x => f) x
⊢ (do
      let b ← f a
      let y ← mapMIdx (fun x => f) x
      pure (cons b y)) =
    do
    let b ← f a
    let y ← mapMIdx ((fun x => f) ∘ Fin.succ) x
    pure (cons b y)

State before:
α : Type u
β : Type v
γ : Type w
n : Nat
m : Type v → Type w
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
x✝ : SizedArray α n
n✝ : Nat
a : α
x : SizedArray α n✝
IH : mapM f x = mapMIdx (fun x => f) x
⊢ (do
      let b ← f a
      let y ← mapMIdx (fun x => f) x
      pure (cons b y)) =
    do
    let b ← f a
    let y ← mapMIdx ((fun x => f) ∘ Fin.succ) x
    pure (cons b y)
Tactic:
rfl
State after:
no goals