if h : n < x.size
then
  rw [dif_pos h]; dsimp
  exists (f x[n] >>= λ v => pure ⟨x.set ⟨n,h⟩ v, x.size_set ⟨n,h⟩ v⟩)
  rw [map_eq_pure_bind, bind_assoc]
  apply bind_congr; intro a
  exact pure_bind ..
else rw [dif_neg h]; exact ⟨pure ⟨x,rfl⟩, map_pure Subtype.val _⟩
α✝ : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u
x : Array α
n : Nat
f : α → m α
⊢ SatisfiesM (fun y => size y = size x)
    (if h : n < size x then
      let idx := { val := n, isLt := h };
      let v := get x idx;
      do
      let v ← f v
      pure (set x idx v)
    else pure x)
no goals