case h.e'_2
a✝ b c n a : ℕ
⊢ Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = (image (fun x => x % a) (Finset.Ico n (n + a))).val
a✝ b c n a : ℕ
⊢ Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = Multiset.range a
convert congr_arg Finset.val (image_Ico_mod n a)
case h.e'_2
a✝ b c n a : ℕ
⊢ ∀ (x : ℕ), x ∈ (Finset.Ico n (n + a)).val → ∀ (y : ℕ), y ∈ (Finset.Ico n (n + a)).val → x % a = y % a → x = y
case h.e'_2
a✝ b c n a : ℕ
⊢ Multiset.map (fun x => x % a) (Multiset.Ico n (n + a)) = (image (fun x => x % a) (Finset.Ico n (n + a))).val
refine' ((nodup_map_iff_inj_on (Finset.Ico _ _).nodup).2 <| _).dedup.symm
no goals
case h.e'_2
a✝ b c n a : ℕ
⊢ ∀ (x : ℕ), x ∈ (Finset.Ico n (n + a)).val → ∀ (y : ℕ), y ∈ (Finset.Ico n (n + a)).val → x % a = y % a → x = y
exact mod_injOn_Ico _ _