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

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

State before:
case h
α : Type u_1
n : Nat
a : α
⊢ (mkArray (n + 1) a).data = (push (mkArray n a) a).data
Tactic:
simp [mkArray_data, List.replicate]
State after:
case h
α : Type u_1
n : Nat
a : α
⊢ a :: List.replicate n a = List.replicate n a ++ [a]

State before:
case h
α : Type u_1
n : Nat
a : α
⊢ a :: List.replicate n a = List.replicate n a ++ [a]
Tactic:
induction n with
| zero => rfl
| succ n ih => simp; exact ih
State after:
no goals

State before:
case h.zero
α : Type u_1
a : α
⊢ a :: List.replicate Nat.zero a = List.replicate Nat.zero a ++ [a]
Tactic:
rfl
State after:
no goals

State before:
case h.succ
α : Type u_1
a : α
n : Nat
ih : a :: List.replicate n a = List.replicate n a ++ [a]
⊢ a :: List.replicate (Nat.succ n) a = List.replicate (Nat.succ n) a ++ [a]
Tactic:
simp
State after:
case h.succ
α : Type u_1
a : α
n : Nat
ih : a :: List.replicate n a = List.replicate n a ++ [a]
⊢ a :: List.replicate n a = List.replicate n a ++ [a]

State before:
case h.succ
α : Type u_1
a : α
n : Nat
ih : a :: List.replicate n a = List.replicate n a ++ [a]
⊢ a :: List.replicate n a = List.replicate n a ++ [a]
Tactic:
exact ih
State after:
no goals