no goals
F : Type ?u.780136
α : Type u_1
β : Type ?u.780142
γ : Type ?u.780145
inst✝¹ : LeftCancelSemigroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Set α
t : Finset α
⊢ (Set.PairwiseDisjoint s fun x => x • t) ↔ Set.InjOn (fun p => p.fst * p.snd) (s ×ˢ ↑t)
simp_rw [← pairwiseDisjoint_coe, coe_smul_finset, Set.pairwiseDisjoint_smul_iff]