α : Type u
n : ℕ
c : α
⊢ (ofFn fun x => c) = c :: ofFn fun x => c
α : Type u
n : ℕ
c : α
⊢ (ofFn fun x => c) = replicate (n + 1) c
rw [replicate, ← ofFn_const n]
no goals
α : Type u
n : ℕ
c : α
⊢ (ofFn fun x => c) = c :: ofFn fun x => c
simp