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)))
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ ↑card (filter p (Ico n (n + a))) = count p a
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]
case e_a.e_f
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ p = p ∘ fun x => x % a
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)))
congr
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
case e_a.e_f
n a : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
pp : Periodic p a
⊢ p = p ∘ fun x => x % a
funext n
no goals
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
exact (Function.Periodic.map_mod_nat pp n).symm