From 51f5ca3efbca6cc86530cd6eb950bb31b771e16b Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Tue, 8 Dec 2020 10:43:00 +0000
Subject: [PATCH] chore(group_theory/perm): Add alternate formulation of
 (sum|sigma)_congr lemmas (#5260)

These lemmas existed already for `equiv`, but not for `perm` or for `perm` via group structures.
---
 src/data/equiv/basic.lean        | 49 +++++++++++++++++++++++++++++++-
 src/group_theory/perm/basic.lean | 29 +++++++++++++++++++
 2 files changed, 77 insertions(+), 1 deletion(-)

diff --git a/src/data/equiv/basic.lean b/src/data/equiv/basic.lean
index 0847ddceac687..6e9d6e557e820 100644
--- a/src/data/equiv/basic.lean
+++ b/src/data/equiv/basic.lean
@@ -500,7 +500,7 @@ def sum_congr {α₁ β₁ α₂ β₂ : Type*} (ea : α₁ ≃ α₂) (eb : β
   (equiv.sum_congr e f).trans (equiv.sum_congr g h) = (equiv.sum_congr (e.trans g) (f.trans h)) :=
 by { ext i, cases i; refl }
 
-@[simp] lemma sum_congr_symm {α β γ δ : Type u} (e : α ≃ β) (f : γ ≃ δ) :
+@[simp] lemma sum_congr_symm {α β γ δ : Sort*} (e : α ≃ β) (f : γ ≃ δ) :
   (equiv.sum_congr e f).symm = (equiv.sum_congr (e.symm) (f.symm)) :=
 rfl
 
@@ -508,6 +508,31 @@ rfl
   equiv.sum_congr (equiv.refl α) (equiv.refl β) = equiv.refl (α ⊕ β) :=
 by { ext i, cases i; refl }
 
+namespace perm
+
+/-- Combine a permutation of `α` and of `β` into a permutation of `α ⊕ β`. -/
+@[reducible]
+def sum_congr {α β : Type*} (ea : equiv.perm α) (eb : equiv.perm β) : equiv.perm (α ⊕ β) :=
+equiv.sum_congr ea eb
+
+@[simp] lemma sum_congr_apply {α β : Type*} (ea : equiv.perm α) (eb : equiv.perm β) (x : α ⊕ β) :
+  sum_congr ea eb x = sum.map ⇑ea ⇑eb x := equiv.sum_congr_apply ea eb x
+
+@[simp] lemma sum_congr_trans {α β : Sort*}
+  (e : equiv.perm α) (f : equiv.perm β) (g : equiv.perm α) (h : equiv.perm β) :
+  (sum_congr e f).trans (sum_congr g h) = sum_congr (e.trans g) (f.trans h) :=
+equiv.sum_congr_trans e f g h
+
+@[simp] lemma sum_congr_symm {α β : Sort*} (e : equiv.perm α) (f : equiv.perm β) :
+  (sum_congr e f).symm = sum_congr (e.symm) (f.symm) :=
+equiv.sum_congr_symm e f
+
+@[simp] lemma sum_congr_refl {α β : Sort*} :
+  sum_congr (equiv.refl α) (equiv.refl β) = equiv.refl (α ⊕ β) :=
+equiv.sum_congr_refl
+
+end perm
+
 /-- `bool` is equivalent the sum of two `punit`s. -/
 def bool_equiv_punit_sum_punit : bool ≃ punit.{u+1} ⊕ punit.{v+1} :=
 ⟨λ b, cond b (inr punit.star) (inl punit.star),
@@ -741,6 +766,28 @@ by { ext1 x, cases x, refl }
   (sigma_congr_right (λ a, equiv.refl (β a))) = equiv.refl (Σ a, β a) :=
 by { ext1 x, cases x, refl }
 
+namespace perm
+
+/-- A family of permutations `Π a, perm (β a)` generates a permuation `perm (Σ a, β₁ a)`. -/
+@[reducible]
+def sigma_congr_right {α} {β : α → Sort*} (F : Π a, perm (β a)) : perm (Σ a, β a) :=
+equiv.sigma_congr_right F
+
+@[simp] lemma sigma_congr_right_trans {α} {β : α → Sort*}
+  (F : Π a, perm (β a)) (G : Π a, perm (β a)) :
+  (sigma_congr_right F).trans (sigma_congr_right G) = sigma_congr_right (λ a, (F a).trans (G a)) :=
+equiv.sigma_congr_right_trans F G
+
+@[simp] lemma sigma_congr_right_symm {α} {β : α → Sort*} (F : Π a, perm (β a)) :
+  (sigma_congr_right F).symm = sigma_congr_right (λ a, (F a).symm) :=
+equiv.sigma_congr_right_symm F
+
+@[simp] lemma sigma_congr_right_refl {α} {β : α → Sort*} :
+  (sigma_congr_right (λ a, equiv.refl (β a))) = equiv.refl (Σ a, β a) :=
+equiv.sigma_congr_right_refl
+
+end perm
+
 /-- An equivalence `f : α₁ ≃ α₂` generates an equivalence between `Σ a, β (f a)` and `Σ a, β a`. -/
 @[simps apply]
 def sigma_congr_left {α₁ α₂} {β : α₂ → Sort*} (e : α₁ ≃ α₂) : (Σ a:α₁, β (e a)) ≃ (Σ a:α₂, β a) :=
diff --git a/src/group_theory/perm/basic.lean b/src/group_theory/perm/basic.lean
index e0d7ead7d9681..664ffee919fb9 100644
--- a/src/group_theory/perm/basic.lean
+++ b/src/group_theory/perm/basic.lean
@@ -48,6 +48,35 @@ lemma eq_inv_iff_eq {f : perm α} {x y : α} : x = f⁻¹ y ↔ f x = y := f.eq_
 
 lemma inv_eq_iff_eq {f : perm α} {x y : α} : f⁻¹ x = y ↔ x = f y := f.symm_apply_eq
 
+/-! Lemmas about `equiv.perm.sum_congr` re-expressed via the group structure. -/
+
+@[simp] lemma sum_congr_mul {α β : Type*} (e : perm α) (f : perm β) (g : perm α) (h : perm β) :
+  sum_congr e f * sum_congr g h = sum_congr (e * g) (f * h) :=
+sum_congr_trans g h e f
+
+@[simp] lemma sum_congr_inv {α β : Type*} (e : perm α) (f : perm β) :
+  (sum_congr e f)⁻¹ = sum_congr e⁻¹ f⁻¹ :=
+sum_congr_symm e f
+
+@[simp] lemma sum_congr_one {α β : Type*} :
+  sum_congr (1 : perm α) (1 : perm β) = 1 :=
+sum_congr_refl
+
+/-! Lemmas about `equiv.perm.sigma_congr_right` re-expressed via the group structure. -/
+
+@[simp] lemma sigma_congr_right_mul {α} {β : α → Type*}
+  (F : Π a, perm (β a)) (G : Π a, perm (β a)) :
+  sigma_congr_right F * sigma_congr_right G = sigma_congr_right (λ a, F a * G a) :=
+sigma_congr_right_trans G F
+
+@[simp] lemma sigma_congr_right_inv {α} {β : α → Type*} (F : Π a, perm (β a)) :
+  (sigma_congr_right F)⁻¹ = sigma_congr_right (λ a, (F a)⁻¹) :=
+sigma_congr_right_symm F
+
+@[simp] lemma sigma_congr_right_one {α} {β : α → Type*} :
+  (sigma_congr_right (λ a, (1 : equiv.perm $ β a))) = 1 :=
+sigma_congr_right_refl
+
 end perm
 
 section swap