α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • (x.snd ∩ e⁻¹ • x.fst) ⊆ x.fst ∪ e • x.snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • (mulDysonEtransform e x).snd ⊆ (mulDysonEtransform e x).fst
dsimp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.fst ∩ e • x.snd ⊆ x.fst ∪ e • x.snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • (x.snd ∩ e⁻¹ • x.fst) ⊆ x.fst ∪ e • x.snd
rw [smul_finset_inter, smul_inv_smul, inter_comm]
no goals
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.fst ∩ e • x.snd ⊆ x.fst ∪ e • x.snd
exact inter_subset_union