α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ op e • x.fst * e⁻¹ • x.snd ⊆ x.fst * x.snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ (mulEtransformLeft e x).fst * (mulEtransformLeft e x).snd ⊆ x.fst * x.snd
refine' inter_mul_union_subset_union.trans (union_subset Subset.rfl _)
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ op e • x.fst * e⁻¹ • x.snd ⊆ x.fst * x.snd
rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]