[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ (mulDysonEtransform e x).fst * (mulDysonEtransform e x).snd ⊆ x.fst * x.snd
[PROOFSTEP]
refine' union_mul_inter_subset_union.trans (union_subset Subset.rfl _)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • x.snd * e⁻¹ • x.fst ⊆ x.fst * x.snd
[PROOFSTEP]
rw [mul_smul_comm, smul_mul_assoc, inv_smul_smul, mul_comm]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ Finset.card (mulDysonEtransform e x).fst + Finset.card (mulDysonEtransform e x).snd =
    Finset.card x.fst + Finset.card x.snd
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ Finset.card (x.fst ∪ e • x.snd) + Finset.card (x.snd ∩ e⁻¹ • x.fst) = Finset.card x.fst + Finset.card x.snd
[PROOFSTEP]
rw [← card_smul_finset e (_ ∩ _), smul_finset_inter, smul_inv_smul, inter_comm, card_union_add_card_inter,
  card_smul_finset]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulDysonEtransform e (mulDysonEtransform e x) = mulDysonEtransform e x
[PROOFSTEP]
ext : 1
[GOAL]
case h₁
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ (mulDysonEtransform e (mulDysonEtransform e x)).fst = (mulDysonEtransform e x).fst
[PROOFSTEP]
dsimp
[GOAL]
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ (mulDysonEtransform e (mulDysonEtransform e x)).snd = (mulDysonEtransform e x).snd
[PROOFSTEP]
dsimp
[GOAL]
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
[PROOFSTEP]
rw [smul_finset_inter, smul_inv_smul, inter_comm, union_eq_left_iff_subset]
[GOAL]
case h₁
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.fst ∩ e • x.snd ⊆ x.fst ∪ e • x.snd
[PROOFSTEP]
exact inter_subset_union
[GOAL]
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
[PROOFSTEP]
rw [smul_finset_union, inv_smul_smul, union_comm, inter_eq_left_iff_subset]
[GOAL]
case h₂
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.snd ∩ e⁻¹ • x.fst ⊆ x.snd ∪ e⁻¹ • x.fst
[PROOFSTEP]
exact inter_subset_union
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • (mulDysonEtransform e x).snd ⊆ (mulDysonEtransform e x).fst
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ e • (x.snd ∩ e⁻¹ • x.fst) ⊆ x.fst ∪ e • x.snd
[PROOFSTEP]
rw [smul_finset_inter, smul_inv_smul, inter_comm]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.fst ∩ e • x.snd ⊆ x.fst ∪ e • x.snd
[PROOFSTEP]
exact inter_subset_union
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ mulEtransformLeft 1 x = x
[PROOFSTEP]
simp [mulEtransformLeft]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ mulEtransformRight 1 x = x
[PROOFSTEP]
simp [mulEtransformRight]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ (mulEtransformLeft e x).fst * (mulEtransformLeft e x).snd ⊆ x.fst * x.snd
[PROOFSTEP]
refine' inter_mul_union_subset_union.trans (union_subset Subset.rfl _)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ op e • x.fst * e⁻¹ • x.snd ⊆ x.fst * x.snd
[PROOFSTEP]
rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ (mulEtransformRight e x).fst * (mulEtransformRight e x).snd ⊆ x.fst * x.snd
[PROOFSTEP]
refine' union_mul_inter_subset_union.trans (union_subset Subset.rfl _)
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ op e • x.fst * e⁻¹ • x.snd ⊆ x.fst * x.snd
[PROOFSTEP]
rw [op_smul_finset_mul_eq_mul_smul_finset, smul_inv_smul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ Finset.card x.fst + Finset.card (op e • x.fst) = 2 * Finset.card x.fst
[PROOFSTEP]
rw [card_smul_finset, two_mul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ Finset.card x.snd + Finset.card (e⁻¹ • x.snd) = 2 * Finset.card x.snd
[PROOFSTEP]
rw [card_smul_finset, two_mul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Group α
e : α
x : Finset α × Finset α
⊢ card (mulEtransformLeft e x).fst + card (mulEtransformLeft e x).snd +
      (card (mulEtransformRight e x).fst + card (mulEtransformRight e x).snd) =
    card x.fst + card x.snd + (card x.fst + card x.snd)
[PROOFSTEP]
rw [add_add_add_comm, mulEtransformLeft.card, mulEtransformRight.card, ← mul_add, two_mul]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulEtransformLeft e⁻¹ x = Prod.swap (mulEtransformRight e (Prod.swap x))
[PROOFSTEP]
simp [-op_inv, op_smul_eq_smul, mulEtransformLeft, mulEtransformRight]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ mulEtransformRight e⁻¹ x = Prod.swap (mulEtransformLeft e (Prod.swap x))
[PROOFSTEP]
simp [-op_inv, op_smul_eq_smul, mulEtransformLeft, mulEtransformRight]
