[GOAL]
a : ℕ
⊢ Periodic (gcd a) a
[PROOFSTEP]
simp only [forall_const, gcd_add_self_right, eq_self_iff_true, Periodic]
[GOAL]
a : ℕ
⊢ Periodic (coprime a) a
[PROOFSTEP]
simp only [coprime_add_self_right, forall_const, iff_self_iff, eq_iff_iff, Periodic]
[GOAL]
a : ℕ
⊢ Periodic (fun n => n % a) a
[PROOFSTEP]
simp only [forall_const, eq_self_iff_true, add_mod_right, Periodic]
[GOAL]
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
⊢ f (n % a) = f n
[PROOFSTEP]
conv_rhs => rw [← Nat.mod_add_div n a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]
[GOAL]
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f n
[PROOFSTEP]
rw [← Nat.mod_add_div n a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]
[GOAL]
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f n
[PROOFSTEP]
rw [← Nat.mod_add_div n a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]
[GOAL]
α : Type u_1
f : ℕ → α
a : ℕ
hf : Periodic f a
n : ℕ
| f n
[PROOFSTEP]
rw [← Nat.mod_add_div n a, mul_comm, ← Nat.nsmul_eq_mul, hf.nsmul]
[GOAL]
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ ↑card (filter p (Ico n (n + a))) = count p a
[PROOFSTEP]
rw [count_eq_card_filter_range, Finset.card, Finset.filter_val, Finset.range_val, ← multiset_Ico_map_mod n, ←
  map_count_True_eq_filter_card, ← map_count_True_eq_filter_card, map_map]
[GOAL]
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ Multiset.count True (map p (Ico n (n + a))) = Multiset.count True (map (p ∘ fun x => x % a) (Ico n (n + a)))
[PROOFSTEP]
congr
[GOAL]
case e_a.e_f
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ p = p ∘ fun x => x % a
[PROOFSTEP]
funext n
[GOAL]
case e_a.e_f.h
n✝ a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
n : ℕ
⊢ p n = (p ∘ fun x => x % a) n
[PROOFSTEP]
exact (Function.Periodic.map_mod_nat pp n).symm
