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

State before:
α : Type u
n✝ : Nat
a : α
i✝ n i : Nat
h : i + 1 < n + 1
⊢ (replicate (n + 1) a)[i + 1] = a
Tactic:
simp only [replicate_succ_eq_cons, get_cons_succ (hi₁:=h) (hi₂:=Nat.lt_of_succ_lt_succ h)]
State after:
α : Type u
n✝ : Nat
a : α
i✝ n i : Nat
h : i + 1 < n + 1
⊢ (replicate n a)[i] = a

State before:
α : Type u
n✝ : Nat
a : α
i✝ n i : Nat
h : i + 1 < n + 1
⊢ (replicate n a)[i] = a
Tactic:
exact get_replicate (a:=a) (i:=i) (h:=Nat.lt_of_succ_lt_succ h)
State after:
no goals