no goals
α : Type u
β : Type v
γ : Type w
a : α
m n : Nat
⊢ replicateTR.loop a n (replicate m a) = replicate (n + m) a
induction n generalizing m with simp [replicateTR.loop]
| succ n ih => simp [Nat.succ_add]; exact ih (m+1)
case succ
α : Type u
β : Type v
γ : Type w
a : α
n : Nat
ih : ∀ (m : Nat), replicateTR.loop a n (replicate m a) = replicate (n + m) a
m : Nat
⊢ replicateTR.loop a n (a :: replicate m a) = a :: replicate (n + m) a
case succ
α : Type u
β : Type v
γ : Type w
a : α
n : Nat
ih : ∀ (m : Nat), replicateTR.loop a n (replicate m a) = replicate (n + m) a
m : Nat
⊢ replicateTR.loop a n (a :: replicate m a) = replicate (Nat.succ n + m) a
simp [Nat.succ_add]
no goals
case succ
α : Type u
β : Type v
γ : Type w
a : α
n : Nat
ih : ∀ (m : Nat), replicateTR.loop a n (replicate m a) = replicate (n + m) a
m : Nat
⊢ replicateTR.loop a n (a :: replicate m a) = a :: replicate (n + m) a
exact ih (m+1)