refactor(Data/Sym/Sym2): curry mk (#34803)

Curry `Sym2.mk` from `Sym2.mk (p : α × α)` to `Sym2.mk (a b : α)`. This matches the `s(a, b)` notation and reduce the uncertainty about simp normal form.

Author: YaelDillies

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -333,7 +333,7 @@ lemma IsTree.card_edgeFinset [Fintype V] [Fintype G.edgeSet] (hG : G.IsTree) :
           length_cons, length_nil] at h'
       simp at h'
     rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
-    · simp only [firstDart_toProd, getVert_cons_succ, getVert_zero, Prod.swap_prod_mk]
+    · simp
     case contra =>
       suffices (f x).takeUntil y hy = .cons h .nil by
         rw [← take_spec _ hy] at h'

Mathlib/Combinatorics/SimpleGraph/Dart.lean

@@ -58,11 +58,10 @@ instance Dart.fintype [Fintype V] [DecidableRel G.Adj] : Fintype G.Dart :=
       invFun := fun d => ⟨d.fst, d.snd, d.adj⟩ }
 
 /-- The edge associated to the dart. -/
-def Dart.edge (d : G.Dart) : Sym2 V :=
-  Sym2.mk d.toProd
+def Dart.edge (d : G.Dart) : Sym2 V := s(d.fst, d.snd)
 
 @[simp]
-theorem Dart.edge_mk {p : V × V} (h : G.Adj p.1 p.2) : (Dart.mk p h).edge = Sym2.mk p :=
+theorem Dart.edge_mk {p : V × V} (h : G.Adj p.1 p.2) : (Dart.mk p h).edge = s(p.1, p.2) :=
   rfl
 
 @[simp]
@@ -80,7 +79,7 @@ theorem Dart.symm_mk {p : V × V} (h : G.Adj p.1 p.2) : (Dart.mk p h).symm = Dar
 
 @[simp]
 theorem Dart.edge_symm (d : G.Dart) : d.symm.edge = d.edge :=
-  Sym2.mk_prod_swap_eq
+  Sym2.eq_swap
 
 @[simp]
 theorem Dart.edge_comp_symm : Dart.edge ∘ Dart.symm = (Dart.edge : G.Dart → Sym2 V) :=
@@ -102,9 +101,9 @@ theorem dart_edge_eq_iff : ∀ d₁ d₂ : G.Dart, d₁.edge = d₂.edge ↔ d
   simp
 
 theorem dart_edge_eq_mk'_iff :
-    ∀ {d : G.Dart} {p : V × V}, d.edge = Sym2.mk p ↔ d.toProd = p ∨ d.toProd = p.swap := by
-  rintro ⟨p, h⟩
-  apply Sym2.mk_eq_mk_iff
+    ∀ {d : G.Dart} {u v : V}, d.edge = s(u, v) ↔ d.toProd = (u, v) ∨ d.toProd = (v, u) := by
+  rintro ⟨p, h⟩ _ _
+  simp
 
 theorem dart_edge_eq_mk'_iff' :
     ∀ {d : G.Dart} {u v : V},

Mathlib/Combinatorics/SimpleGraph/EdgeLabeling.lean

@@ -123,7 +123,7 @@ def mk (f : ∀ x y : V, G.Adj x y → K)
     (f_symm : ∀ (x y : V) (H : G.Adj x y), f y x H.symm = f x y H) : EdgeLabeling G K
   | ⟨e, he⟩ => by
     revert he
-    refine Sym2.hrec (fun xy ↦ f xy.1 xy.2) (fun a b ↦ ?_) e
+    refine Sym2.hrec f (fun a b ↦ ?_) e
     apply Function.hfunext (by simp [adj_comm])
     grind
 

Mathlib/Combinatorics/SimpleGraph/Maps.lean

@@ -77,10 +77,10 @@ theorem edgeSet_map (f : V ↪ W) (G : SimpleGraph V) :
   constructor
   · intro ⟨a, b, hadj, ha, hb⟩
     use s(a, b), hadj
-    rw [Embedding.sym2Map_apply, Sym2.map_pair_eq, ha, hb]
+    rw [Embedding.sym2Map_apply, Sym2.map_mk, ha, hb]
   · intro ⟨e, hadj, he⟩
     induction e
-    rw [Embedding.sym2Map_apply, Sym2.map_pair_eq, Sym2.eq_iff] at he
+    rw [Embedding.sym2Map_apply, Sym2.map_mk, Sym2.eq_iff] at he
     exact he.elim (fun ⟨h, h'⟩ ↦ ⟨_, _, hadj, h, h'⟩) (fun ⟨h', h⟩ ↦ ⟨_, _, hadj.symm, h, h'⟩)
 
 lemma map_adj_apply {G : SimpleGraph V} {f : V ↪ W} {a b : V} :

Mathlib/Combinatorics/SimpleGraph/Paths.lean

@@ -822,7 +822,7 @@ theorem map_isTrail_iff_of_injective (hinj : Function.Injective f) :
   | cons _ _ ih =>
     rw [map_cons, isTrail_cons, ih, isTrail_cons]
     apply and_congr_right'
-    rw [← Sym2.map_pair_eq, edges_map, ← List.mem_map_of_injective (Sym2.map.injective hinj)]
+    rw [← Sym2.map_mk, edges_map, ← List.mem_map_of_injective (Sym2.map.injective hinj)]
 
 alias ⟨_, map_isTrail_of_injective⟩ := map_isTrail_iff_of_injective
 

Mathlib/Combinatorics/SimpleGraph/Subgraph.lean

@@ -254,7 +254,7 @@ lemma image_coe_edgeSet_coe (G' : G.Subgraph) : Sym2.map (↑) '' G'.coe.edgeSet
   rintro e he
   induction e using Sym2.ind with | h a b =>
   rw [Subgraph.mem_edgeSet] at he
-  exact ⟨s(⟨a, edge_vert _ he⟩, ⟨b, edge_vert _ he.symm⟩), Sym2.map_pair_eq ..⟩
+  exact ⟨s(⟨a, edge_vert _ he⟩, ⟨b, edge_vert _ he.symm⟩), Sym2.map_mk ..⟩
 
 theorem mem_verts_of_mem_edge {G' : Subgraph G} {e : Sym2 V} {v : V} (he : e ∈ G'.edgeSet)
     (hv : v ∈ e) : v ∈ G'.verts := by
@@ -1099,7 +1099,7 @@ theorem deleteEdges_coe_eq (s : Set (Sym2 G'.verts)) :
   · intro hs
     refine Sym2.ind ?_
     rintro ⟨v', hv'⟩ ⟨w', hw'⟩
-    simp only [Sym2.map_pair_eq, Sym2.eq]
+    simp only [Sym2.map_mk, Sym2.eq]
     contrapose!
     rintro (_ | _) <;> simpa only [Sym2.eq_swap]
   · intro h' hs

Mathlib/Combinatorics/SimpleGraph/Triangle/Basic.lean

@@ -119,7 +119,7 @@ lemma edgeDisjointTriangles_iff_mem_sym2_subsingleton :
   constructor
   · rw [Sym2.forall]
     rintro hG a b hab
-    simp only [Sym2.isDiag_iff_proj_eq] at hab
+    simp only [Sym2.mk_isDiag_iff] at hab
     rw [this _ _ (Sym2.mk_isDiag_iff.not.2 hab)]
     rintro _ ⟨hab, c, hac, hbc, rfl⟩ _ ⟨-, d, had, hbd, rfl⟩
     refine hG.eq ?_ ?_ (Set.Nontrivial.not_subsingleton ⟨a, ?_, b, ?_, hab.ne⟩) <;>

Mathlib/Data/Finset/Sym.lean

@@ -130,18 +130,14 @@ end
 
 variable {s t : Finset α} {a b : α}
 
-theorem sym2_eq_image [DecidableEq α] : s.sym2 = (s ×ˢ s).image Sym2.mk := by
-  ext z
-  refine z.ind fun x y ↦ ?_
-  grind
+theorem sym2_eq_image [DecidableEq α] : s.sym2 = (s ×ˢ s).image Sym2.mk.uncurry := by
+  ext ⟨a, b⟩; simp; grind
 
-theorem isDiag_mk_of_mem_diag {a : α × α} (h : a ∈ s.diag) : (Sym2.mk a).IsDiag :=
-  (Sym2.isDiag_iff_proj_eq _).2 (mem_diag.1 h).2
+theorem isDiag_mk_of_mem_diag {a b : α} (h : (a, b) ∈ s.diag) : s(a, b).IsDiag := by
+  simp at *; grind
 
-theorem not_isDiag_mk_of_mem_offDiag {a : α × α} (h : a ∈ s.offDiag) :
-    ¬ (Sym2.mk a).IsDiag := by
-  rw [Sym2.isDiag_iff_proj_eq]
-  exact (mem_offDiag.1 h).2.2
+theorem not_isDiag_mk_of_mem_offDiag {a b : α} (h : (a, b) ∈ s.offDiag) : ¬ s(a, b).IsDiag := by
+  simp at *; grind
 
 section Sym2
 
@@ -155,7 +151,7 @@ theorem diag_mem_sym2_mem_iff : (∀ b, b ∈ Sym2.diag a → b ∈ s) ↔ a ∈
 theorem diag_mem_sym2_iff : Sym2.diag a ∈ s.sym2 ↔ a ∈ s := by simp [diag_mem_sym2_mem_iff]
 
 theorem image_diag_union_image_offDiag [DecidableEq α] :
-    s.diag.image Sym2.mk ∪ s.offDiag.image Sym2.mk = s.sym2 := by
+    s.diag.image Sym2.mk.uncurry ∪ s.offDiag.image Sym2.mk.uncurry = s.sym2 := by
   rw [← image_union, diag_union_offDiag, sym2_eq_image]
 
 end Sym2

Mathlib/Data/List/Sym.lean

@@ -141,30 +141,7 @@ theorem map_mk_disjoint_sym2 (x : α) (xs : List α) (h : x ∉ xs) :
     (map (fun y ↦ s(x, y)) xs).Disjoint xs.sym2 := by
   induction xs with
   | nil => simp
-  | cons x' xs ih =>
-    simp only [mem_cons, not_or] at h
-    rw [List.sym2, map_cons, map_cons, disjoint_cons_left, disjoint_append_right,
-      disjoint_cons_right]
-    refine ⟨?_, ⟨?_, ?_⟩, ?_⟩
-    · refine not_mem_cons_of_ne_of_not_mem ?_ (not_mem_append ?_ ?_)
-      · simp [h.1]
-      · simp_rw [mem_map, not_exists, not_and]
-        intro x'' hx
-        simp_rw [Sym2.mk_eq_mk_iff, Prod.swap_prod_mk, Prod.mk.injEq, true_and]
-        rintro (⟨rfl, rfl⟩ | rfl)
-        · exact h.2 hx
-        · exact h.2 hx
-      · simp [mk_mem_sym2_iff, h.2]
-    · simp [h.1]
-    · intro z hx hy
-      rw [List.mem_map] at hx hy
-      obtain ⟨a, hx, rfl⟩ := hx
-      obtain ⟨b, hy, hx⟩ := hy
-      simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Ne.symm h.1, false_and, Prod.swap_prod_mk,
-        false_or] at hx
-      obtain ⟨rfl, rfl⟩ := hx
-      exact h.2 hy
-    · exact ih h.2
+  | cons x' xs ih => aesop (add simp mk_mem_sym2_iff, unfold safe List.Disjoint)
 
 theorem dedup_sym2 [DecidableEq α] (xs : List α) : xs.sym2.dedup = xs.dedup.sym2 := by
   induction xs with

Mathlib/Data/Sym/Card.lean

@@ -123,37 +123,23 @@ namespace Sym2
 variable [DecidableEq α]
 
 /-- The `diag` of `s : Finset α` is sent on a finset of `Sym2 α` of card `#s`. -/
-theorem card_image_diag (s : Finset α) : #(s.diag.image Sym2.mk) = #s := by
-  rw [card_image_of_injOn, diag_card]
-  rintro ⟨x₀, x₁⟩ hx _ _ h
-  cases Sym2.eq.1 h
-  · rfl
-  · simp only [mem_coe, mem_diag] at hx
-    rw [hx.2]
-
-lemma two_mul_card_image_offDiag (s : Finset α) : 2 * #(s.offDiag.image Sym2.mk) = #s.offDiag := by
-  rw [card_eq_sum_card_image (Sym2.mk : α × α → _), sum_const_nat (Sym2.ind _), mul_comm]
-  rintro x y hxy
-  simp_rw [mem_image, mem_offDiag] at hxy
-  obtain ⟨a, ⟨ha₁, ha₂, ha⟩, h⟩ := hxy
-  replace h := Sym2.eq.1 h
-  obtain ⟨hx, hy, hxy⟩ : x ∈ s ∧ y ∈ s ∧ x ≠ y := by
-    cases h <;> refine ⟨‹_›, ‹_›, ?_⟩ <;> [exact ha; exact ha.symm]
-  have hxy' : y ≠ x := hxy.symm
-  have : {z ∈ s.offDiag | Sym2.mk z = s(x, y)} = {(x, y), (y, x)} := by
-    ext ⟨x₁, y₁⟩
-    rw [mem_filter, mem_insert, mem_singleton, Sym2.eq_iff, Prod.mk_inj, Prod.mk_inj,
-      and_iff_right_iff_imp]
-    -- `hxy'` is used in `exact`
-    rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;> rw [mem_offDiag] <;> exact ⟨‹_›, ‹_›, ‹_›⟩
-  rw [this, card_insert_of_notMem, card_singleton]
-  simp only [not_and, Prod.mk_inj, mem_singleton]
-  exact fun _ => hxy'
+theorem card_image_diag (s : Finset α) : #(s.diag.image Sym2.mk.uncurry) = #s := by
+  simp [card_image_of_injOn]
+
+lemma two_mul_card_image_offDiag (s : Finset α) :
+    2 * #(s.offDiag.image Sym2.mk.uncurry) = #s.offDiag := by
+  rw [card_eq_sum_card_image (Sym2.mk.uncurry : α × α → _), sum_const_nat (Sym2.ind _), mul_comm]
+  -- FIXME: Would be cool for the final `aesop` call not to require this `a ≠ b ∨ b ≠ a` trick.
+  have (a b : α) (ha : a ∈ s) (hb : b ∈ s) (hab : a ≠ b ∨ b ≠ a) :
+      {z ∈ s.offDiag | Sym2.mk.uncurry z = s(a, b)} = .cons (a, b) {(b, a)}
+        (by simpa [eq_comm] using hab) := by aesop
+  aesop
 
 /-- The `offDiag` of `s : Finset α` is sent on a finset of `Sym2 α` of card `#s.offDiag / 2`.
 This is because every element `s(x, y)` of `Sym2 α` not on the diagonal comes from exactly two
 pairs: `(x, y)` and `(y, x)`. -/
-theorem card_image_offDiag (s : Finset α) : #(s.offDiag.image Sym2.mk) = (#s).choose 2 := by
+theorem card_image_offDiag (s : Finset α) :
+    #(s.offDiag.image Sym2.mk.uncurry) = (#s).choose 2 := by
   rw [Nat.choose_two_right, Nat.mul_sub_left_distrib, mul_one, ← offDiag_card,
     Nat.div_eq_of_eq_mul_right Nat.zero_lt_two (two_mul_card_image_offDiag s).symm]