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

State before:
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
⊢ (replicate (n + 1) a)[i] = (push (replicate n a) a)[i]
Tactic:
simp only [get_replicate, get_push]
State after:
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
⊢ a = if h : i < n then a else a

State before:
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
⊢ a = if h : i < n then a else a
Tactic:
apply dite (i < n) <;> (intro h; simp only [h]; rfl)
State after:
no goals

State before:
case e
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
⊢ ¬i < n → a = if h : i < n then a else a
Tactic:
intro h
State after:
case e
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
h : ¬i < n
⊢ a = if h : i < n then a else a

State before:
case e
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
h : ¬i < n
⊢ a = if h : i < n then a else a
Tactic:
simp only [h]
State after:
case e
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
h : ¬i < n
⊢ a = if h : False then a else a

State before:
case e
α : Type u
n : Nat
a : α
i : Nat
hi : i < n + 1
h : ¬i < n
⊢ a = if h : False then a else a
Tactic:
rfl
State after:
no goals