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

Mathlib.lean

@@ -5210,6 +5210,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/Algebra/NonUnitalHom.lean

@@ -390,7 +390,7 @@ theorem snd_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : (snd R B C).com
 
 @[simp]
 theorem prod_fst_snd : prod (fst R A B) (snd R A B) = 1 :=
-  coe_injective Function.prod_fst_snd
+  coe_injective Function.fst_prod_snd
 
 /-- Taking the product of two maps with the same domain is equivalent to taking the product of
 their codomains. -/

Mathlib/Algebra/Notation/Pi/Defs.lean

@@ -7,7 +7,7 @@ module
 
 public import Mathlib.Algebra.Notation.Defs
 public import Mathlib.Tactic.Push.Attr
-public import Mathlib.Logic.Function.Defs
+public import Mathlib.Logic.Function.Init
 public import Batteries.Tactic.Alias
 
 /-!
@@ -32,10 +32,10 @@ namespace Pi
 alias prod := Function.prod
 
 @[deprecated (since := "2026-04-21")]
-alias prod_fst_snd := Function.prod_fst_snd
+alias prod_fst_snd := Function.fst_prod_snd
 
 @[deprecated (since := "2026-04-21")]
-alias prod_snd_fst := Function.prod_snd_fst
+alias prod_snd_fst := Function.snd_prod_fst
 
 /-! `1`, `0`, `+`, `*`, `+ᵥ`, `•`, `^`, `-`, `⁻¹`, and `/` are defined pointwise. -/
 

Mathlib/Algebra/Star/StarAlgHom.lean

@@ -507,7 +507,7 @@ theorem snd_prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : (snd R B
 
 @[simp]
 theorem prod_fst_snd : prod (fst R A B) (snd R A B) = 1 :=
-  DFunLike.coe_injective Function.prod_fst_snd
+  DFunLike.coe_injective Function.fst_prod_snd
 
 /-- Taking the product of two maps with the same domain is equivalent to taking the product of
 their codomains. -/
@@ -611,7 +611,7 @@ theorem snd_prod (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : (snd R B C).com
 
 @[simp]
 theorem prod_fst_snd : prod (fst R A B) (snd R A B) = 1 :=
-  DFunLike.coe_injective Function.prod_fst_snd
+  DFunLike.coe_injective Function.fst_prod_snd
 
 /-- Taking the product of two maps with the same domain is equivalent to taking the product of
 their codomains. -/

Mathlib/Data/Fin/Tuple/Curry.lean

@@ -7,6 +7,7 @@ module
 
 public import Mathlib.Data.Fin.Tuple.Basic
 public import Mathlib.Logic.Equiv.Fin.Basic
+public import Mathlib.Logic.Function.Init
 public import Mathlib.Logic.Function.OfArity
 
 /-!

Mathlib/Logic/Function/Defs.lean

@@ -23,27 +23,6 @@ variable {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} {δ : Sort u₄} {ζ
 
 lemma flip_def {f : α → β → φ} : flip f = fun b a => f a b := rfl
 
-/-- Composition of dependent functions: `(f ∘' g) x = f (g x)`, where type of `g x` depends on `x`
-and type of `f (g x)` depends on `x` and `g x`. -/
-@[inline, reducible]
-def dcomp {β : α → Sort u₂} {φ : ∀ {x : α}, β x → Sort u₃} (f : ∀ {x : α} (y : β x), φ y)
-    (g : ∀ x, β x) : ∀ x, φ (g x) := fun x => f (g x)
-
-@[inherit_doc] infixr:80 " ∘' " => Function.dcomp
-
-/-- Product of functions: `Function.prod f g i = (f i, g i)`, where the types of `f i` and
-`g i` may depend on `i`. -/
-protected def prod {ι} {α β : ι → Type*} (f : ∀ i, α i) (g : ∀ i, β i) (i : ι) :
-    α i × β i := (f i, g i)
-
-@[simp] lemma prod_apply {ι} {α β : ι → Type*} (f : ∀ i, α i) (g : ∀ i, β i) (i : ι) :
-    Function.prod f g i = (f i , g i) := rfl
-
-lemma prod_fst_snd {α β} : Function.prod (Prod.fst : α × β → α) (Prod.snd : α × β → β) = id :=
-  rfl
-lemma prod_snd_fst {α β} : Function.prod (Prod.snd : α × β → β) (Prod.fst : α × β → α) = .swap :=
-  rfl
-
 /-- Given functions `f : β → β → φ` and `g : α → β`, produce a function `α → α → φ` that evaluates
 `g` on each argument, then applies `f` to the results. Can be used, e.g., to transfer a relation
 from `β` to `α`. -/

Mathlib/Logic/Function/Init.lean

@@ -0,0 +1,239 @@
+/-
+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
+
+/-!
+# Dependent composition, pairing, and diagonal for functions
+
+This file develops a small API around pairing and diagonal maps on (possibly dependent) functions,
+living in the `Function` namespace so that dot notation is available.
+
+## Main definitions
+
+* `Function.dcomp` (notation `∘'`): dependent composition of functions.
+* `Function.prod` (notation `×ᶠ`): given `f : ∀ i, α i` and `g : ∀ i, β i`, the pointwise pair
+  `fun i ↦ (f i, g i)`.
+* `Function.fstComp`, `Function.sndComp`: the two components of a function `h : ∀ i, α i × β i`,
+  inverse to `Function.prod`.
+* `Function.diag` with notation `△`, so that the diagonal `△(a) = (a, a)`.
+* `Function.prodMap`: `Prod.map` re-exposed under `Function` so that `f.prodMap g` works via dot
+  notation.
+
+This file should not depend on anything defined in Mathlib (other than notation), so that it can
+be upstreamed to Batteries or the Lean standard library easily.
+-/
+
+@[expose] public section
+
+namespace Function
+
+/- ### Dependent composition -/
+
+/-- Composition of dependent functions: `(f ∘' g) i = f (g i)`, where the type of `g i` depends on
+`i` and the type of `f (g i)` depends on `i` and `g i`. -/
+@[inline, reducible] def dcomp {ι} {β : ι → Sort*} {φ : ∀ {i : ι}, β i → Sort*}
+    (f : ∀ {i : ι} (y : β i), φ y) (g : ∀ i, β i) (i : ι) : φ (g i) := f (g i)
+
+@[inherit_doc] infixr:90 " ∘' " => dcomp
+
+section
+
+variable {ι} {β : ι → Sort*} {φ : ∀ {i : ι}, β i → Sort*} (f : ∀ {i : ι} (y : β i), φ y)
+    (g : ∀ i, β i) (i : ι)
+
+theorem dcomp_apply : dcomp f g i = f (g i) := rfl
+
+theorem dcomp_def : f ∘' g = fun i => f (g i) := rfl
+
+@[simp] theorem dcomp_eq_comp {α β γ} (f : β → γ) (g : α → β) : f ∘' g = f ∘ g := rfl
+
+@[simp] theorem id_dcomp {α β} (f : α → β) : (fun {_} => id) ∘' f = f := rfl
+
+@[simp] theorem dcomp_id {α β} (f : α → β) : f ∘' (id : α → α) = f := rfl
+
+theorem dcomp_assoc {κ : Sort*} (h : κ → ι) : f ∘' g ∘' h = (f ∘' g) ∘' h := rfl
+
+@[simp] theorem const_dcomp {α β γ} (a : α) (g : γ → β) :
+    (const β a) ∘' g = const γ a := rfl
+
+@[simp] theorem dcomp_const {α β δ} (f : α → δ) (a : α) :
+    f ∘' (const β a) = const β (f a) := rfl
+
+end
+
+/-- Product of functions: `(f ×ᶠ g) i = (f i, g i)`, where the types of `f i` and `g i`
+may depend on `i`. -/
+@[inline] def prod {ι} {α β : ι → Type*} (f : ∀ i, α i) (g : ∀ i, β i) :
+    (i : ι) → α i × β i := fun i => Prod.mk (f i) (g i)
+
+@[inherit_doc] infixr:95 " ×ᶠ " => prod
+
+/-- The first component of a map into a product. -/
+@[inline] def fstComp {ι} {α β : ι → Type*} (h : (i : ι) → α i × β i) := (h ·|>.1)
+
+@[inherit_doc] postfix:max "₍₁₎" => fstComp
+
+/-- The second component of a map into a product. -/
+@[inline] def sndComp {ι} {α β : ι → Type*} (h : (i : ι) → α i × β i) := (h ·|>.2)
+
+@[inherit_doc] postfix:max "₍₂₎" => sndComp
+
+section
+
+variable {ι κ} {α β : ι → Type*} (f f' : ∀ i, α i) (g g' : ∀ i, β i) (h : ∀ i, α i × β i)
+  (i : ι)
+
+@[simp, grind =] theorem prod_apply : (f ×ᶠ g) i = (f i, g i) := rfl
+@[simp, grind =] theorem fstComp_apply : h₍₁₎ i = (h i).1 := rfl
+@[simp, grind =] theorem sndComp_apply : h₍₂₎ i = (h i).2 := rfl
+
+theorem prod_def : f ×ᶠ g = fun i => (f i, g i) := rfl
+
+theorem fst_dcomp : Prod.fst ∘' h = h₍₁₎ := rfl
+theorem snd_dcomp : Prod.snd ∘' h = h₍₂₎ := rfl
+
+@[simp, grind! .] theorem fstComp_prod {f : ∀ i, α i} {g : ∀ i, β i} :
+    (f ×ᶠ g)₍₁₎ = f := by grind
+@[simp, grind! .] theorem sndComp_prod {f : ∀ i, α i} {g : ∀ i, β i} :
+    (f ×ᶠ g)₍₂₎ = g := rfl
+@[simp, grind! .] theorem fstComp_prod_sndComp {h : ∀ i, α i × β i} :
+  h₍₁₎ ×ᶠ h₍₂₎ = h := rfl
+
+theorem fstComp_sndComp_ext {h h' : ∀ i, α i × β i} (H₁ : h₍₁₎ = h'₍₁₎)
+    (H₂ : h₍₂₎ = h'₍₂₎) : h = h' := by grind
+
+theorem fstComp_sndComp_ext_iff {h h' : ∀ i, α i × β i} :
+    h = h' ↔ h₍₁₎ = h'₍₁₎ ∧ h₍₂₎ = h'₍₂₎ := by grind
+
+theorem left_eq_of_prod_eq (H : f ×ᶠ g = f' ×ᶠ g') : f = f' := by grind
+theorem right_eq_of_prod_eq (H : f ×ᶠ g = f' ×ᶠ g') : g = g' := by grind
+
+@[simp] theorem prod_inj {f f' : ∀ i, α i} {g g' : ∀ i, β i} :
+    f ×ᶠ g = f' ×ᶠ g' ↔ f = f' ∧ g = g' := by grind
+
+theorem prod_eq_iff : f ×ᶠ g = h ↔ f = h₍₁₎ ∧ g = h₍₂₎ := by grind
+theorem eq_prod_iff : h = f ×ᶠ g ↔ h₍₁₎ = f ∧ h₍₂₎ = g := by grind
+
+theorem prod_dcomp (h : κ → ι) : (f ×ᶠ g) ∘' h = (f ∘' h) ×ᶠ (g ∘' h) := rfl
+
+theorem dcomp_prod_dcomp {γ : ∀ {i : ι}, α i → Type*} {δ : ∀ {i : ι}, β i → Type*}
+    (h : ∀ {i : ι}, (a : α i) → γ a) (k : ∀ {i : ι}, (b : β i) → δ b) :
+    (h ∘' f) ×ᶠ (k ∘' g) = (h ∘' Prod.fst) ×ᶠ (k ∘' Prod.snd) ∘' f ×ᶠ g := rfl
+
+@[simp] theorem swap_dcomp_prod : Prod.swap ∘' (f ×ᶠ g) = g ×ᶠ f := rfl
+
+end
+
+section
+
+variable {ι : Type*} {α β : ι → Type*}
+
+theorem leftInverse_uncurry_prod_fstComp_prod_sndComp :
+    LeftInverse prod.uncurry (fstComp (α := α) ×ᶠ sndComp (β := β)) := by
+  simp [LeftInverse]
+
+theorem rightInverse_uncurry_prod_fstComp_prod_sndComp :
+    RightInverse prod.uncurry (fstComp (α := α) ×ᶠ sndComp (β := β)) := by
+  simp [RightInverse, LeftInverse]
+
+theorem uncurry_prod_injective : (prod (α := α) (β := β)).uncurry.Injective :=
+  rightInverse_uncurry_prod_fstComp_prod_sndComp.injective
+
+theorem uncurry_prod_surjective : (prod (α := α) (β := β)).uncurry.Surjective :=
+  RightInverse.surjective leftInverse_uncurry_prod_fstComp_prod_sndComp
+
+end
+
+section
+
+variable {α β γ δ : Type*} {ι κ : Sort*} (f : ι → α) (g : ι → β)
+  (a : α) (b : β) (p : α × β)
+
+theorem fst_comp (h : ι → α × β) : Prod.fst ∘ h = h₍₁₎ := rfl
+theorem snd_comp (h : ι → α × β) : Prod.snd ∘ h = h₍₂₎ := rfl
+
+@[simp] theorem fstComp_mk : (Prod.mk a : β → α × β)₍₁₎ = const β a := rfl
+@[simp] theorem sndComp_mk : (Prod.mk a : β → α × β)₍₂₎ = id := rfl
+
+@[simp] theorem fstComp_mk_flip : ((Prod.mk · b) : α → α × β)₍₁₎ = id := rfl
+@[simp] theorem sndComp_mk_flip : ((Prod.mk · b) : α → α × β)₍₂₎ = const α b := rfl
+
+@[simp] theorem fst_prod_snd : (Prod.fst : _ → α) ×ᶠ (Prod.snd : _ → β) = id := rfl
+@[simp] theorem snd_prod_fst : (Prod.snd : _ → β) ×ᶠ (Prod.fst : _ → α) = .swap := rfl
+
+@[simp] theorem const_prod_const : const ι a ×ᶠ const ι b = const ι (a, b) := rfl
+
+theorem const_of_prod : const ι p = (const ι p.1) ×ᶠ (const ι p.2) := rfl
+
+theorem prod_comp (h : κ → ι) : (f ×ᶠ g) ∘ h = (f ∘ h) ×ᶠ (g ∘ h) := rfl
+
+theorem comp_prod_comp (h : α → γ) (k : β → δ) :
+    (h ∘ f) ×ᶠ (k ∘ g) = (h ∘ Prod.fst) ×ᶠ (k ∘ Prod.snd) ∘ f ×ᶠ g := rfl
+
+theorem map_comp_prod (h : α → γ) (k : β → δ) :
+    Prod.map h k ∘ f ×ᶠ g = (h ∘ f) ×ᶠ (k ∘ g) := rfl
+
+@[simp] theorem swap_comp_prod : Prod.swap ∘ (f ×ᶠ g) = g ×ᶠ f := rfl
+
+end
+
+/-- The diagonal map into `Prod`. -/
+@[inline] def diag {α} : α → α × α := id ×ᶠ id
+
+@[inherit_doc] notation:max "△(" x:max ")" => diag x
+
+section
+
+variable {α β γ} (f : α → β) (g : α → γ) (a b : α)
+
+@[simp, grind =] theorem diag_apply : △(a) = (a, a) := rfl
+
+@[simp] theorem id_prod_id : id ×ᶠ id = diag (α := α) := rfl
+@[simp] theorem fstComp_diag : (diag (α := α))₍₁₎ = id := rfl
+@[simp] theorem sndComp_diag : (diag (α := α))₍₂₎ = id := rfl
+
+@[simp] theorem diag_comp : diag ∘ f = f ×ᶠ f := rfl
+
+@[simp] theorem map_comp_diag : Prod.map f g ∘ diag = f ×ᶠ g := rfl
+
+theorem injective_diag : Injective (α := α) diag := fun _ _ => congrArg Prod.fst
+
+theorem fst_diag_eq_snd_diag : △(a).1 = △(a).2 := rfl
+
+theorem eq_diag_fst_of_fst_eq_snd {p : α × α} (hp : p.1 = p.2) : p = △(p.1) := by
+  simp [Prod.ext_iff, hp]
+
+theorem eq_diag_snd_of_fst_eq_snd {p : α × α} (hp : p.1 = p.2) : p = △(p.2) := by
+  simp [Prod.ext_iff, hp]
+
+@[simp] theorem swap_comp_diag : Prod.swap ∘ diag = diag (α := α) := rfl
+
+end
+
+/-- Dot-notation alias for `Prod.map`. Collapses to `Prod.map` under `simp` via
+`prodMap_eq_prod_map`, so existing `Prod.map` API applies unchanged. -/
+@[inline] def prodMap {α₁ α₂ β₁ β₂} (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂ :=
+  (f ∘ Prod.fst) ×ᶠ (g ∘ Prod.snd)
+
+section
+
+variable {α₁ α₂ α₃ β₁ β₂ β₃} (f f₁ : α₁ → α₂) (f₂ : α₂ → α₃) (g g₁ : β₁ → β₂) (g₂ : β₂ → β₃)
+    (p : α₁ × β₁)
+
+theorem prodMap_apply : f.prodMap g p = (f p.1, g p.2) := rfl
+
+theorem prodMap_comp : f₂.prodMap g₂ ∘ f₁.prodMap g₁ = (f₂ ∘ f₁).prodMap (g₂ ∘ g₁) := rfl
+
+@[simp] theorem prodMap_id : (id : α₁ → α₁).prodMap (id : β₁ → β₁) = id := rfl
+
+@[simp, grind =]
+theorem prodMap_eq_prod_map : f.prodMap g = Prod.map f g := rfl
+
+end
+
+end Function