Theorem: Array.mkArray_succ (LeanSAT/Upstream/ToStd.lean)

State before:
α : Type u_1
n : Nat
a : α
⊢ mkArray (n + 1) a = #[a] ++ mkArray n a
Tactic:
apply Array.ext'
State after:
case h
α : Type u_1
n : Nat
a : α
⊢ (mkArray (n + 1) a).data = (#[a] ++ mkArray n a).data

State before:
case h
α : Type u_1
n : Nat
a : α
⊢ (mkArray (n + 1) a).data = (#[a] ++ mkArray n a).data
Tactic:
simp
State after:
no goals