exact Subgroup.pairwiseDisjoint_smul _ (Set.mem_range_self _) (Set.mem_range_self _)
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ a • ↑(stabilizer α s) ≠ b • ↑(stabilizer α s) → Disjoint (a • ↑(stabilizer α s)) (b • ↑(stabilizer α s))
no goals