case h₁
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.fst ∪ e • x.snd ∪ e • (x.snd ∩ e⁻¹ • x.fst) = x.fst ∪ e • x.snd

case h₂
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.snd ∩ e⁻¹ • x.fst ∩ e⁻¹ • (x.fst ∪ e • x.snd) = x.snd ∩ e⁻¹ • x.fst
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulDysonEtransform e (mulDysonEtransform e x) = mulDysonEtransform e x
ext : 1 <;> dsimp
case h₁
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.fst ∩ e • x.snd ⊆ x.fst ∪ e • x.snd
case h₁
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.fst ∪ e • x.snd ∪ e • (x.snd ∩ e⁻¹ • x.fst) = x.fst ∪ e • x.snd
rw [smul_finset_inter, smul_inv_smul, inter_comm, union_eq_left_iff_subset]
no goals
case h₁
α : 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
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.snd ∩ e⁻¹ • x.fst ⊆ x.snd ∪ e⁻¹ • x.fst
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.snd ∩ e⁻¹ • x.fst ∩ e⁻¹ • (x.fst ∪ e • x.snd) = x.snd ∩ e⁻¹ • x.fst
rw [smul_finset_union, inv_smul_smul, union_comm, inter_eq_left_iff_subset]
no goals
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.snd ∩ e⁻¹ • x.fst ⊆ x.snd ∪ e⁻¹ • x.fst
exact inter_subset_union