no goals
α : Type u
m : ℕ
a : Fin m → α
n : ℕ
⊢ ofFn (Fin.repeat n a) = join (replicate n (ofFn a))
simp_rw [ofFn_mul, ← ofFn_const, Fin.repeat, Fin.modNat, add_comm,
  Nat.add_mul_mod_self_right, Nat.mod_eq_of_lt (Fin.is_lt _)]