have ha' : a' n = 0 := by
  have : a' n = ⟨a n % 7, Nat.mod_lt _ (Nat.succ_pos _)⟩ := by simp[a']
  rw [this]
  simp only [Nat.mod_eq_zero_of_dvd hn, Fin.mk_zero]
n : ℕ
hn : 7 ∣ a n
⊢ ∃ M, n < M ∧ 7 ∣ a M
n : ℕ
hn : 7 ∣ a n
ha' : a' n = 0
⊢ ∃ M, n < M ∧ 7 ∣ a M