From 81721a451f6e76593ac70a73f689a8be2b71f5b4 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 25 Feb 2025 07:51:19 -0600
Subject: [PATCH 1/2] feat(List/Perm): add lemmas

- Add `List.map_perm_map_iff` and `List.Perm.flatMap`.
- Add some `@[gcongr]` and `@[simp]` attrs.
- Add `Relation.comp_fun_eq` and `Relation.fun_eq_comp`.
---
 Mathlib/Data/List/Perm/Basic.lean | 20 ++++++++++++++++++++
 Mathlib/Logic/Relation.lean       | 22 ++++++++++++++++------
 2 files changed, 36 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Data/List/Perm/Basic.lean b/Mathlib/Data/List/Perm/Basic.lean
index 59c2261615aff..1b26c58a3c347 100644
--- a/Mathlib/Data/List/Perm/Basic.lean
+++ b/Mathlib/Data/List/Perm/Basic.lean
@@ -139,6 +139,10 @@ theorem forall₂_comp_perm_eq_perm_comp_forall₂ : Forall₂ r ∘r Perm = Per
     exact ⟨l', h₂.symm, h₁.flip⟩
   · exact fun ⟨l₂, h₁₂, h₂₃⟩ => perm_comp_forall₂ h₁₂ h₂₃
 
+theorem eq_map_comp_perm (f : α → β) : (· = map f ·) ∘r (· ~ ·) = (· ~ map f ·) := by
+  conv_rhs => rw [← Relation.comp_eq_fun (map f)]
+  simp only [← forall₂_eq_eq_eq, forall₂_map_right_iff, forall₂_comp_perm_eq_perm_comp_forall₂]
+
 theorem rel_perm_imp (hr : RightUnique r) : (Forall₂ r ⇒ Forall₂ r ⇒ (· → ·)) Perm Perm :=
   fun a b h₁ c d h₂ h =>
   have : (flip (Forall₂ r) ∘r Perm ∘r Forall₂ r) b d := ⟨a, h₁, c, h, h₂⟩
@@ -210,6 +214,12 @@ theorem perm_replicate_append_replicate
   · simp [subset_def, or_comm]
   · exact forall_congr' fun _ => by rw [← and_imp, ← not_or, not_imp_not]
 
+theorem map_perm_map_iff {l' : List α} {f : α → β} (hf : f.Injective) :
+    map f l ~ map f l' ↔ l ~ l' := calc
+  map f l ~ map f l' ↔ Relation.Comp (· = map f ·) (· ~ ·) (map f l) l' := by rw [eq_map_comp_perm]
+  _ ↔ l ~ l' := by simp [Relation.Comp, map_inj_right hf]
+
+@[gcongr]
 theorem Perm.flatMap_left (l : List α) {f g : α → List β} (h : ∀ a ∈ l, f a ~ g a) :
     l.flatMap f ~ l.flatMap g :=
   Perm.flatten_congr <| by
@@ -217,6 +227,13 @@ theorem Perm.flatMap_left (l : List α) {f g : α → List β} (h : ∀ a ∈ l,
 
 @[deprecated (since := "2024-10-16")] alias Perm.bind_left := Perm.flatMap_left
 
+attribute [gcongr] Perm.flatMap_right
+
+@[gcongr]
+protected theorem Perm.flatMap {l₁ l₂ : List α} {f g : α → List β} (h : l₁ ~ l₂)
+    (hfg : ∀ a ∈ l₁, f a ~ g a) : l₁.flatMap f ~ l₂.flatMap g :=
+  .trans (.flatMap_left _ hfg) (h.flatMap_right _)
+
 theorem flatMap_append_perm (l : List α) (f g : α → List β) :
     l.flatMap f ++ l.flatMap g ~ l.flatMap fun x => f x ++ g x := by
   induction' l with a l IH
@@ -234,14 +251,17 @@ theorem map_append_flatMap_perm (l : List α) (f : α → β) (g : α → List 
 
 @[deprecated (since := "2024-10-16")] alias map_append_bind_perm := map_append_flatMap_perm
 
+@[gcongr]
 theorem Perm.product_right {l₁ l₂ : List α} (t₁ : List β) (p : l₁ ~ l₂) :
     product l₁ t₁ ~ product l₂ t₁ :=
   p.flatMap_right _
 
+@[gcongr]
 theorem Perm.product_left (l : List α) {t₁ t₂ : List β} (p : t₁ ~ t₂) :
     product l t₁ ~ product l t₂ :=
   (Perm.flatMap_left _) fun _ _ => p.map _
 
+@[gcongr]
 theorem Perm.product {l₁ l₂ : List α} {t₁ t₂ : List β} (p₁ : l₁ ~ l₂) (p₂ : t₁ ~ t₂) :
     product l₁ t₁ ~ product l₂ t₂ :=
   (p₁.product_right t₁).trans (p₂.product_left l₂)
diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index 0e8c56a80eb73..caa0f9e15e0c2 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -120,18 +120,28 @@ def Comp (r : α → β → Prop) (p : β → γ → Prop) (a : α) (c : γ) : P
 @[inherit_doc]
 local infixr:80 " ∘r " => Relation.Comp
 
-theorem comp_eq : r ∘r (· = ·) = r :=
-  funext fun _ ↦ funext fun b ↦ propext <|
-  Iff.intro (fun ⟨_, h, Eq⟩ ↦ Eq ▸ h) fun h ↦ ⟨b, h, rfl⟩
+@[simp]
+theorem comp_eq_fun (f : γ → β) : r ∘r (· = f ·) = (r · <| f ·) := by
+  ext x y
+  simp [Comp]
+
+@[simp]
+theorem comp_eq : r ∘r (· = ·) = r := comp_eq_fun ..
+
+@[simp]
+theorem fun_eq_comp (f : γ → α) : (f · = ·) ∘r r = (f · |> r <| ·) := by
+  ext x y
+  simp [Comp]
 
-theorem eq_comp : (· = ·) ∘r r = r :=
-  funext fun a ↦ funext fun _ ↦ propext <|
-  Iff.intro (fun ⟨_, Eq, h⟩ ↦ Eq.symm ▸ h) fun h ↦ ⟨a, rfl, h⟩
+@[simp]
+theorem eq_comp : (· = ·) ∘r r = r := fun_eq_comp ..
 
+@[simp]
 theorem iff_comp {r : Prop → α → Prop} : (· ↔ ·) ∘r r = r := by
   have : (· ↔ ·) = (· = ·) := by funext a b; exact iff_eq_eq
   rw [this, eq_comp]
 
+@[simp]
 theorem comp_iff {r : α → Prop → Prop} : r ∘r (· ↔ ·) = r := by
   have : (· ↔ ·) = (· = ·) := by funext a b; exact iff_eq_eq
   rw [this, comp_eq]

From fd7af8bba91f9c5de5d89b77bc6e5c7092887e77 Mon Sep 17 00:00:00 2001
From: "Yury G. Kudryashov" <urkud@urkud.name>
Date: Tue, 25 Feb 2025 18:40:19 -0600
Subject: [PATCH 2/2] Update Mathlib/Logic/Relation.lean

Co-authored-by: Eric Wieser <efw@google.com>
---
 Mathlib/Logic/Relation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Logic/Relation.lean b/Mathlib/Logic/Relation.lean
index caa0f9e15e0c2..c37e317a3ee61 100644
--- a/Mathlib/Logic/Relation.lean
+++ b/Mathlib/Logic/Relation.lean
@@ -129,7 +129,7 @@ theorem comp_eq_fun (f : γ → β) : r ∘r (· = f ·) = (r · <| f ·) := by
 theorem comp_eq : r ∘r (· = ·) = r := comp_eq_fun ..
 
 @[simp]
-theorem fun_eq_comp (f : γ → α) : (f · = ·) ∘r r = (f · |> r <| ·) := by
+theorem fun_eq_comp (f : γ → α) : (f · = ·) ∘r r = (r <| f ·) := by
   ext x y
   simp [Comp]