α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • x.snd * e⁻¹ • x.fst ⊆ x.fst * x.snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ (mulDysonEtransform e x).fst * (mulDysonEtransform e x).snd ⊆ x.fst * x.snd
refine' union_mul_inter_subset_union.trans (union_subset Subset.rfl _)
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • x.snd * e⁻¹ • x.fst ⊆ x.fst * x.snd
rw [mul_smul_comm, smul_mul_assoc, inv_smul_smul, mul_comm]