feat: add Function.{prod,diag,fstComp,sndComp,prodMap}

Mathlib.lean

@@ -5118,6 +5118,7 @@ public import Mathlib.Logic.Function.Defs
 public import Mathlib.Logic.Function.DependsOn
 public import Mathlib.Logic.Function.FiberPartition
 public import Mathlib.Logic.Function.FromTypes
+public import Mathlib.Logic.Function.Init
 public import Mathlib.Logic.Function.Iterate
 public import Mathlib.Logic.Function.OfArity
 public import Mathlib.Logic.Function.ULift

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -277,7 +277,7 @@ lemma one_le_finprod {M : Type*} [CommMonoidWithZero M] [Preorder M] [ZeroLEOneC
 theorem MonoidHom.map_finprod_plift (f : M →* N) (g : α → M)
     (h : HasFiniteMulSupport <| g ∘ PLift.down) : f (∏ᶠ x, g x) = ∏ᶠ x, f (g x) := by
   rw [finprod_eq_prod_plift_of_mulSupport_subset h.coe_toFinset.ge,
-    finprod_eq_prod_plift_of_mulSupport_subset, map_prod]
+    finprod_eq_prod_plift_of_mulSupport_subset, _root_.map_prod]
   rw [h.coe_toFinset]
   exact mulSupport_comp_subset f.map_one (g ∘ PLift.down)
 

Mathlib/Algebra/Exact.lean

@@ -428,7 +428,7 @@ def Exact.splitInjectiveEquiv
     have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero
     constructor
     · intro x y e
-      simp only [prod_apply, Pi.prod, Prod.mk.injEq] at e
+      simp only [LinearMap.prod_apply, Pi.prod, Prod.mk.injEq] at e
       obtain ⟨z, hz⟩ := (h (x - y)).mp (by simpa [sub_eq_zero] using e.2)
       suffices z = 0 by rw [← sub_eq_zero, ← hz, this, map_zero]
       rw [← h₁ z, hz, map_sub, e.1, sub_self]

Mathlib/Algebra/MvPolynomial/Equiv.lean

@@ -582,7 +582,7 @@ theorem finSuccEquiv_coeff_coeff (m : Fin n →₀ ℕ) (f : MvPolynomial (Fin (
   | monomial j r =>
     simp only [finSuccEquiv_apply, coe_eval₂Hom, eval₂_monomial, RingHom.coe_comp, Finsupp.prod_pow,
       Polynomial.coeff_C_mul, coeff_C_mul, coeff_monomial, Fin.prod_univ_succ, Fin.cases_zero,
-      Fin.cases_succ, ← map_prod, ← map_pow, Function.comp_apply]
+      Fin.cases_succ, ← _root_.map_prod, ← map_pow, Function.comp_apply]
     rw [← mul_boole, mul_comm (Polynomial.X ^ j 0), Polynomial.coeff_C_mul_X_pow]; congr 1
     obtain rfl | hjmi := eq_or_ne j (m.cons i)
     · simpa only [cons_zero, cons_succ, if_pos rfl, monomial_eq, C_1, one_mul,

Mathlib/Algebra/MvPolynomial/Eval.lean

@@ -197,7 +197,7 @@ theorem map_eval₂Hom [CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁)
 
 theorem eval₂Hom_monomial (f : R →+* S₁) (g : σ → S₁) (d : σ →₀ ℕ) (r : R) :
     eval₂Hom f g (monomial d r) = f r * d.prod fun i k => g i ^ k := by
-  simp only [monomial_eq, map_mul, eval₂Hom_C, Finsupp.prod, map_prod, map_pow, eval₂Hom_X']
+  simp only [coe_eval₂Hom, eval₂_monomial]
 
 @[simp]
 theorem eval₂Hom_smul (f : R →+* S₁) (g : σ → S₁) (r : R) (P : MvPolynomial σ R) :

Mathlib/Algebra/Notation/Pi/Defs.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Algebra.Notation.Defs
 public import Mathlib.Tactic.Push.Attr
+public import Mathlib.Logic.Function.Init
 
 /-!
 # Notation for algebraic operators on pi types
@@ -26,14 +27,6 @@ variable {ι α β : Type*} {G M R : ι → Type*}
 
 namespace Pi
 
--- TODO: Do we really need this definition? If so, where to put it?
-/-- The mapping into a product type built from maps into each component. -/
-@[simp]
-protected def prod {α β : ι → Type*} (f : ∀ i, α i) (g : ∀ i, β i) (i : ι) : α i × β i := (f i, g i)
-
-lemma prod_fst_snd : Pi.prod (Prod.fst : α × β → α) (Prod.snd : α × β → β) = id := rfl
-lemma prod_snd_fst : Pi.prod (Prod.snd : α × β → β) (Prod.fst : α × β → α) = .swap := rfl
-
 /-! `1`, `0`, `+`, `*`, `+ᵥ`, `•`, `^`, `-`, `⁻¹`, and `/` are defined pointwise. -/
 
 section One

Mathlib/Algebra/Star/StarAlgHom.lean

@@ -489,7 +489,7 @@ variable {R A B C}
 @[simps!]
 def prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : A →⋆ₙₐ[R] B × C :=
   { f.toNonUnitalAlgHom.prod g.toNonUnitalAlgHom with
-    map_star' := fun x => by simp [map_star, Prod.star_def] }
+    map_star' := fun x => by simp [map_star, Prod.ext_iff] }
 
 theorem coe_prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : ⇑(f.prod g) = Pi.prod f g :=
   rfl

Mathlib/CategoryTheory/Bicategory/Extension.lean

@@ -163,11 +163,11 @@ end LeftExtension
 /-- Triangle diagrams for (left) lifts.
 ```
             b
-          ◹ |
-   lift /   |      △
+          ◥ |
+   lift /   |      ▲
       /     | f    | unit
-    /       ▽
-  c - - - ▷ a
+    /       ▼
+  c - - - ▶ a
        g
 ```
 -/
@@ -212,11 +212,11 @@ def ofIdComp (t : LeftLift f (𝟙 c ≫ g)) : LeftLift f g :=
 /-- Whisker a 1-morphism to a lift.
 ```
                     b
-                  ◹ |
-           lift /   |      △
+                  ◥ |
+           lift /   |      ▲
               /     | f    | unit
-            /       ▽
-x - - - ▷ c - - - ▷ a
+            /       ▼
+x - - - ▶ c - - - ▶ a
      h         g
 ```
 -/
@@ -330,7 +330,7 @@ end RightExtension
 /-- Triangle diagrams for (right) lifts.
 ```
             b
-          ◹ |
+          ◥ |
    lift /   |      | counit
       /     | f    ▽
     /       ▽

Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean

@@ -217,11 +217,11 @@ def lanLift (f : b ⟶ a) (g : c ⟶ a) [HasLeftKanLift f g] : c ⟶ b :=
 /-- `f₊ g` is the left Kan lift of `g` along `f`.
 ```
             b
-          ◹ |
+          ◥ |
    f₊ g /   |
       /     | f
-    /       ▽
-  c - - - ▷ a
+    /       ▼
+  c - - - ▶ a
        g
 ```
 -/

Mathlib/Combinatorics/Nullstellensatz.lean

@@ -174,7 +174,7 @@ private lemma Alon.of_mem_P_support {ι : Type*} (i : ι) (S : Finset R) (m : ι
     (hm : m ∈ (Alon.P S i).support) :
     ∃ e ≤ S.card, m = single i e := by
   classical
-  have hP : Alon.P S i = .rename (fun _ ↦ i) (Alon.P S ()) := by simp [Alon.P, map_prod]
+  have hP : Alon.P S i = .rename (fun _ ↦ i) (Alon.P S ()) := by simp [Alon.P]
   rw [hP, support_rename_of_injective (Function.injective_of_subsingleton _)] at hm
   simp only [Finset.mem_image, mem_support_iff, ne_eq] at hm
   obtain ⟨e, he, hm⟩ := hm
@@ -237,7 +237,7 @@ theorem combinatorial_nullstellensatz_exists_linearCombination
     intro i _
     rw [smul_eq_mul, map_mul]
     convert mul_zero _
-    rw [Alon.P, map_prod]
+    rw [Alon.P, _root_.map_prod]
     apply Finset.prod_eq_zero (hx i)
     simp
 

Mathlib/LinearAlgebra/Goursat.lean

@@ -119,24 +119,20 @@ lemma goursat : ∃ (M' : Submodule R M) (N' : Submodule R N) (M'' : Submodule R
   obtain ⟨e, he⟩ := goursat_surjective hL₁' hL₂'
   use M', N', L'.goursatFst, L'.goursatSnd, e
   rw [← he]
-  simp only [LinearMap.range_comp, Submodule.range_subtype, L']
+  simp only [LinearMap.range_comp, Submodule.range_subtype, L', M', N', P, Q]
   rw [comap_map_eq_self]
   · ext ⟨m, n⟩
     constructor
-    · intro hmn
-      simp only [mem_map, LinearMap.mem_range, prod_apply, Subtype.exists, Prod.exists, coe_prodMap,
-        coe_subtype, Prod.map_apply, Prod.mk.injEq, exists_and_right, exists_eq_right_right,
-        exists_eq_right, M', N', fst_apply, snd_apply]
-      exact ⟨⟨n, hmn⟩, ⟨m, hmn⟩, ⟨m, n, hmn, rfl⟩⟩
-    · simp only [mem_map, LinearMap.mem_range, prod_apply, Subtype.exists, Prod.exists,
-        coe_prodMap, coe_subtype, Prod.map_apply, Prod.mk.injEq, exists_and_right,
-        exists_eq_right_right, exists_eq_right, forall_exists_index, Pi.prod]
-      rintro hm hn m₁ n₁ hm₁n₁ ⟨hP, hQ⟩
-      simp only [Subtype.ext_iff] at hP hQ
-      rwa [← hP, ← hQ]
+    · simp only [mem_map, LinearMap.mem_range, LinearMap.prod_apply, Pi.prod_apply, Subtype.exists,
+      Prod.exists, prodMap_apply, subtype_apply, Prod.mk.injEq, Subtype.ext_iff,
+      submoduleMap_coe_apply, fst_apply, snd_apply]
+      grind
+    · simp only [mem_map, LinearMap.mem_range, LinearMap.prod_apply, Pi.prod_apply, Subtype.exists,
+      Prod.exists, prodMap_apply, subtype_apply, Prod.mk.injEq, snd_apply, fst_apply,
+      Subtype.ext_iff, submoduleMap_coe_apply]
+      grind
   · convert goursatFst_prod_goursatSnd_le (range <| P.prod Q)
-    ext ⟨m, n⟩
-    simp_rw [mem_ker, coe_prodMap, Prod.map_apply, Submodule.mem_prod, Prod.zero_eq_mk,
-      Prod.ext_iff, ← mem_ker, ker_mkQ]
+    simp only [ker_prodMap, ker_mkQ, Submodule.ext_iff]
+    grind
 
 end Submodule

Mathlib/Logic/Function/Init.lean

@@ -0,0 +1,201 @@
+/-
+Copyright (c) 2026 Wrenna Robson. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wrenna Robson
+-/
+module
+
+public import Mathlib.Init
+
+/-!
+
+This file defines `(f ▽ g)`, the operation that pairs two functions `f : ι → α` and
+`g : ι → β` into a function `ι → α × β`.
+
+It also defines the special case when `f = g = id`, `Function.diag`. This is the canonical injection
+of a type into its prouduct with itself onto its diagonal.
+
+
+This file should not depend on anything defined in Mathlib (except for notation), so that it can be
+upstreamed to Batteries or the Lean standard library easily.
+
+-/
+
+@[expose] public section
+
+namespace Pi
+
+/-- The dependent mapping into a product type built from dependent maps into each component. -/
+protected def prod {ι} {α β : ι → Type*} (f : ∀ i, α i) (g : ∀ i, β i) (i : ι) : α i × β i :=
+    Prod.mk (f i) (g i)
+
+@[inherit_doc] infixr:95 " ▽' " => Pi.prod
+
+section
+
+variable {ι} {α β : ι → Type*} (f f' : ∀ i, α i) (g g' : ∀ i, β i) {c}
+
+@[simp, grind =] theorem prod_apply : (f ▽' g) c = (f c, g c) := rfl
+
+theorem fst_prod : ((f ▽' g) c).fst = f c := rfl
+theorem snd_prod : ((f ▽' g) c).snd = g c := rfl
+
+@[simp] theorem prod_fst_snd {α β} : (Prod.fst : _ → α) ▽' (Prod.snd : _ → β) = id := rfl
+@[simp] theorem prod_snd_fst {α β} : (Prod.snd : _ → β) ▽' (Prod.fst : _ → α) = .swap := rfl
+
+theorem prod_fst_snd_comp {h : ∀ i, α i × β i} :
+   (Prod.fst <| h ·) ▽' (Prod.snd <| h ·) = h := rfl
+
+theorem fst_comp_prod {f : ∀ i, α i} {g : ∀ i, β i} : (Prod.fst <| (f ▽' g) ·) = f := rfl
+theorem snd_comp_prod {f : ∀ i, α i} {g : ∀ i, β i} : (Prod.snd <| (f ▽' g) ·) = g := rfl
+
+@[simp]
+theorem prod_eq_iff {f : ∀ i, α i} {g : ∀ i, β i} :
+    f ▽' g = f' ▽' g' ↔ f = f' ∧ g = g' := by simp [funext_iff, Prod.ext_iff, forall_and]
+
+theorem prod_ext_iff {h h' : ∀ i, α i × β i} : h = h' ↔
+    (Prod.fst <| h ·) = (Prod.fst <| h' ·) ∧ (Prod.snd <| h ·) = (Prod.snd <| h' ·) := by
+  simp [funext_iff, Prod.ext_iff, forall_and]
+
+theorem prod_ext {h h' : ∀ i, α i × β i} (h₁ : (Prod.fst <| h ·) = (Prod.fst <| h' ·))
+    (h₂ : (Prod.snd <| h ·) = (Prod.snd <| h' ·)) : h = h' := prod_ext_iff.mpr ⟨h₁, h₂⟩
+
+theorem exists_prod_apply_eq (h : ∀ i, α i × β i) : ∃ f g, (f ▽' g) = h :=
+  ⟨(Prod.fst <| h ·), (Prod.snd <| h ·), prod_fst_snd_comp⟩
+
+theorem exists_fst_comp (f : ∀ i, α i) (g : ∀ i, β i) :
+    ∃ h : ∀ i, α i × β i, (Prod.fst <| h ·) = f := ⟨(f ▽' g), fst_comp_prod⟩
+theorem exists_snd_comp (f : ∀ i, α i) (g : ∀ i, β i) :
+    ∃ h : ∀ i, α i × β i, (Prod.snd <| h ·) = g := ⟨(f ▽' g), snd_comp_prod⟩
+
+@[grind =]
+theorem prod_const_const {ι} {α β} {a : α} {b : β} :
+    (Function.const ι a) ▽' (Function.const ι b) = Function.const ι (a, b) := rfl
+
+theorem eq_prod_iff_fst_comp_snd_comp {f g} {h : ∀ i, α i × β i} :
+    h = f ▽' g ↔ (Prod.fst <| h ·) = f ∧ (Prod.snd <| h ·) = g := by simp [prod_ext_iff]
+
+theorem eq_prod_of_fst_comp_snd_comp {f g} {h : ∀ i, α i × β i} (h₁ : (Prod.fst <| h ·) = f)
+    (h₂ : (Prod.snd <| h ·) = g) : h = f ▽' g := eq_prod_iff_fst_comp_snd_comp.mpr ⟨h₁, h₂⟩
+
+end
+
+end Pi
+
+namespace Function
+
+variable {α β γ δ : Type*} {ι : Sort*}
+
+/-- The map into a product type built from maps into each component. -/
+protected def prod : (ι → α) → (ι → β) → ι → α × β := (· ▽' ·)
+
+@[inherit_doc] infixr:95 " ▽ " => Function.prod
+
+section
+
+variable (f : ι → α) (g : ι → β)
+
+@[simp, grind =] theorem prod_apply (c : ι) : (f.prod g) c = (f c, g c) := rfl
+
+theorem prod_comp {γ} {h : γ → ι} : (f ▽ g) ∘ h = (f ∘ h) ▽ (g ∘ h) := rfl
+
+theorem fst_prod {c} : ((f ▽ g) c).fst = f c := by simp
+theorem snd_prod {c} : ((f ▽ g) c).snd = g c := by simp
+
+@[simp] theorem prod_fst_snd : Prod.fst (α := α) ▽ Prod.snd (β := β) = id := rfl
+@[simp] theorem prod_snd_fst : Prod.snd (β := β) ▽ Prod.fst (α := α) = .swap := rfl
+
+@[simp] theorem prod_fst_snd_comp {f : ι → α × β} : (Prod.fst ∘ f) ▽ (Prod.snd ∘ f) = f := rfl
+
+@[simp] theorem fst_comp_prod {f : ι → α} {g : ι → β} : Prod.fst ∘ (f ▽ g) = f := rfl
+@[simp] theorem snd_comp_prod {f : ι → α} {g : ι → β} : Prod.snd ∘ (f ▽ g) = g := rfl
+
+theorem prod_comp_prod {f : ι → α} {g : ι → β} {h : α × β → γ} {k : α × β → δ} :
+    (h ▽ k) ∘ (f ▽ g) = (h ∘ (f ▽ g)) ▽ (k ∘ (f ▽ g)) := rfl
+
+theorem comp_prod_comp {f : ι → α} {g : ι → β} {h : α → γ} {k : β → δ} :
+    (h ∘ f) ▽ (k ∘ g) = (h ∘ Prod.fst) ▽ (k ∘ Prod.snd) ∘ f ▽ g := rfl
+
+theorem map_comp_prod {f : ι → α} {g : ι → β} {h : α → γ} {k : β → δ} :
+    Prod.map h k ∘ f ▽ g = (h ∘ f) ▽ (k ∘ g) := rfl
+
+theorem prod_eq_iff {f f' : ι → α} {g g' : ι → β} : f ▽ g = f' ▽ g' ↔
+    f = f' ∧ g = g' := by simp [funext_iff, Prod.ext_iff, forall_and]
+
+theorem prod_ext_iff {h h' : ι → α × β} : h = h' ↔
+    Prod.fst ∘ h = Prod.fst ∘ h' ∧ Prod.snd ∘ h = (Prod.snd ∘ h') := by
+  simp [funext_iff, Prod.ext_iff, forall_and]
+
+theorem exists_prod_apply_eq (h : ι → α × β) : ∃ f g, f ▽ g = h :=
+  ⟨Prod.fst ∘ h, Prod.snd ∘ h, prod_fst_snd_comp⟩
+
+theorem exists_fst_comp (f : ι → α) (g : ι → β) :
+    ∃ h : ι → α × β, Prod.fst ∘ h = f := ⟨f ▽ g, fst_comp_prod⟩
+theorem exists_snd_comp (f : ι → α) (g : ι → β) :
+    ∃ h : ι → α × β, Prod.snd ∘ h = g := ⟨f ▽ g, snd_comp_prod⟩
+
+theorem leftInverse_uncurry_prod_prod_fst_comp_snd_comp : Function.LeftInverse
+    (Function.prod (ι := γ)).uncurry ((Prod.fst (α := α) ∘ ·) ▽ (Prod.snd (β := β) ∘ ·)) :=
+  fun _ => rfl
+
+theorem rightInverse_uncurry_prod_prod_fst_comp_snd_comp : Function.RightInverse
+    (Function.prod (ι := γ)).uncurry ((Prod.fst (α := α) ∘ ·) ▽ (Prod.snd (β := β) ∘ ·)) :=
+  fun _ => rfl
+
+@[simp, grind =]
+theorem prod_const_const (a : α) (b : β) :
+    (Function.const ι a) ▽ (Function.const ι b) = Function.const ι (a, b) := rfl
+
+theorem const_prod {ι} {α β} {p : α × β} :
+    Function.const ι p = (Function.const ι p.1) ▽ (Function.const ι p.2) := rfl
+
+theorem eq_prod_iff_fst_comp_snd_comp {f g} {h : ι → α × β} :
+    h = f ▽ g ↔ Prod.fst ∘ h = f ∧ Prod.snd ∘ h = g := by simp [prod_ext_iff]
+
+theorem eq_prod_of_fst_comp_snd_comp {f g} {h : ι → α × β} (h₁ : Prod.fst ∘ h = f)
+    (h₂ : Prod.snd ∘ h = g) : h = f ▽ g := eq_prod_iff_fst_comp_snd_comp.mpr ⟨h₁, h₂⟩
+
+end
+
+/-- The diagonal map into `Prod`. -/
+protected def diag : α → α × α := id ▽ id
+
+@[inherit_doc] prefix:max "⟋" => Function.diag
+
+section
+
+variable {a b : α}
+
+@[grind =] theorem diag_apply : ⟋a = (a, a) := rfl
+
+@[simp] theorem fst_diag : (⟋a).1 = a := rfl
+@[simp] theorem snd_diag : (⟋a).2 = a := rfl
+
+theorem map_diag {f : α → β} {g : α → γ} : Prod.map f g ⟋a = (f ▽ g) a := rfl
+
+@[simp] theorem map_comp_diag {f : α → β} {g : α → γ} :
+  Prod.map f g ∘ Function.diag = f ▽ g := rfl
+
+theorem injective_diag : Function.Injective (α := α) Function.diag := fun _ _ => congrArg Prod.fst
+
+theorem exists_diag_apply_iff (p : α × α) : (∃ a, ⟋a = p) ↔ p.1 = p.2 := by
+  simp [Prod.ext_iff, eq_comm]
+
+theorem diag_eq_iff : ⟋a = ⟋b ↔ a = b := injective_diag.eq_iff
+
+@[simp] theorem diag_prod_diag : Function.diag ▽ Function.diag (α := α) =
+    Function.diag ∘ Function.diag := rfl
+
+end
+
+/-- `Function.prodMap` is `Prod.map` in the `Function` namespace. -/
+def prodMap (f : α → β) (g : γ → δ) := (f ∘ Prod.fst) ▽ (g ∘ Prod.snd)
+
+section
+
+@[simp, grind =]
+theorem prodMap_eq_prod_map {f : α → β} {g : γ → δ} : f.prodMap g = Prod.map f g := rfl
+
+end
+
+end Function

Mathlib/MeasureTheory/Integral/Prod.lean

@@ -502,7 +502,7 @@ theorem integral_prod (f : α × β → E) (hf : Integrable f (μ.prod ν)) :
       measureReal_def,
       integral_toReal (measurable_measure_prodMk_left hs).aemeasurable
         (ae_measure_lt_top hs h2s.ne)]
-    rw [prod_apply hs]
+    rw [Measure.prod_apply hs]
   · rintro f g - i_f i_g hf hg
     simp_rw [integral_add' i_f i_g, integral_integral_add' i_f i_g, hf, hg]
   · exact isClosed_eq continuous_integral continuous_integral_integral