rw [mapM_push, ← h]
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ (Subtype.val <$> do
      let y ← y
      push' y <$> f a) =
    mapM f (push x a)
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x✝¹ x : Array α
a : α
x✝ : SatisfiesM (fun y => size y = size x) (mapM f x)
y : m { a // (fun y => size y = size x) a }
h : Subtype.val <$> y = mapM f x
push' : { y // size y = size x } → β → { y // size y = size (push x a) } :=
  fun y b => { val := push y.val b, property := (_ : size (push y.val b) = size (push x a)) }
⊢ (Subtype.val <$> do
      let y ← y
      push' y <$> f a) =
    do
    let y ← Subtype.val <$> y
    let b ← f a
    pure (push y b)