no goals
α : Type u_2
G : Type u_1
A : Type ?u.151816
S✝ : Type ?u.151819
inst✝³ : Group G
inst✝² : AddGroup A
s : Set G
inst✝¹ : Group α
inst✝ : MulDistribMulAction α G
a : α
S T : Subgroup G
⊢ a • (S ⊓ T) = a • S ⊓ a • T
simp [SetLike.ext_iff, mem_pointwise_smul_iff_inv_smul_mem]