[GOAL]
n : ℕ
h : n ≠ 0
d m : ℕ
⊢ ((fun a => a + d) ∘ fun x => n • id x) m ≡ d [MOD n]
[PROOFSTEP]
simp [Nat.modEq_iff_dvd, ← sub_sub]
[GOAL]
d n : ℕ
h : d < n
⊢ ∃ᶠ (m : ℕ) in atTop, m % n = d
[PROOFSTEP]
simpa only [Nat.ModEq, mod_eq_of_lt h] using frequently_modEq h.ne_bot d
[GOAL]
⊢ ∃ᶠ (m : ℕ) in atTop, Even m
[PROOFSTEP]
simpa only [even_iff] using frequently_mod_eq zero_lt_two
[GOAL]
⊢ ∃ᶠ (m : ℕ) in atTop, Odd m
[PROOFSTEP]
simpa only [odd_iff] using frequently_mod_eq one_lt_two
