feat(Logic/Function/Defs): add Function.diag

Mathlib/Data/Finset/Prod.lean

@@ -248,8 +248,7 @@ variable (s t : Finset α)
 
 /-- Given a finite set `s`, the diagonal, `s.diag` is the set of pairs of the form `(a, a)` for
 `a ∈ s`. -/
-def diag : Finset (α × α) :=
-  s.map ⟨fun a ↦ (a, a), by simp [Function.Injective]⟩
+def diag : Finset (α × α) := s.map ⟨Function.diag, Function.injective_diag⟩
 
 -- TODO: define `Multiset.offDiag`, provide basic API, use it here
 /-- Given a finite set `s`, the off-diagonal, `s.offDiag` is the set of pairs `(a, b)` with `a ≠ b`

Mathlib/Data/Int/Cast/Prod.lean

@@ -21,7 +21,7 @@ variable {α β : Type*} [AddGroupWithOne α] [AddGroupWithOne β]
 
 instance : AddGroupWithOne (α × β) :=
   { Prod.instAddMonoidWithOne, Prod.instAddGroup with
-    intCast := fun n => (n, n)
+    intCast := fun n => (↑n, ↑n)
     intCast_ofNat := fun _ => by ext <;> simp
     intCast_negSucc := fun _ => by ext <;> simp }
 

Mathlib/Data/Nat/Cast/Prod.lean

@@ -24,7 +24,7 @@ variable [AddMonoidWithOne α] [AddMonoidWithOne β]
 
 instance instAddMonoidWithOne : AddMonoidWithOne (α × β) :=
   { Prod.instAddMonoid, @Prod.instOne α β _ _ with
-    natCast := fun n => (n, n)
+    natCast := fun n => (↑n, ↑n)
     natCast_zero := congr_arg₂ Prod.mk Nat.cast_zero Nat.cast_zero
     natCast_succ := fun _ => congr_arg₂ Prod.mk (Nat.cast_succ _) (Nat.cast_succ _) }
 

Mathlib/Data/Set/Prod.lean

@@ -430,25 +430,24 @@ theorem preimage_coe_coe_diagonal (s : Set α) :
   simp [Set.diagonal]
 
 @[simp]
-theorem range_diag : (range fun x => (x, x)) = diagonal α := by
+theorem range_diag : range Function.diag = diagonal α := by
   ext ⟨x, y⟩
   simp [diagonal, eq_comm]
 
-theorem diagonal_subset_iff {s} : diagonal α ⊆ s ↔ ∀ x, (x, x) ∈ s := by
-  rw [← range_diag, range_subset_iff]
+theorem diagonal_subset_iff {s} : diagonal α ⊆ s ↔ ∀ x, (x, x) ∈ s := by grind
 
 @[simp]
 theorem prod_subset_compl_diagonal_iff_disjoint : s ×ˢ t ⊆ (diagonal α)ᶜ ↔ Disjoint s t :=
   prod_subset_iff.trans disjoint_iff_forall_ne.symm
 
 @[simp]
-theorem diag_preimage_prod (s t : Set α) : (fun x => (x, x)) ⁻¹' s ×ˢ t = s ∩ t :=
+theorem diag_preimage_prod (s t : Set α) : Function.diag ⁻¹' s ×ˢ t = s ∩ t :=
   rfl
 
-theorem diag_preimage_prod_self (s : Set α) : (fun x => (x, x)) ⁻¹' s ×ˢ s = s :=
+theorem diag_preimage_prod_self (s : Set α) : Function.diag ⁻¹' s ×ˢ s = s :=
   inter_self s
 
-theorem diag_image (s : Set α) : (fun x => (x, x)) '' s = diagonal α ∩ s ×ˢ s := by
+theorem diag_image (s : Set α) : Function.diag '' s = diagonal α ∩ s ×ˢ s := by
   rw [← range_diag, ← image_preimage_eq_range_inter, diag_preimage_prod_self]
 
 theorem diagonal_eq_univ_iff : diagonal α = univ ↔ Subsingleton α := by

Mathlib/Logic/Function/Defs.lean

@@ -44,6 +44,8 @@ theorem dcomp_apply : dcomp @f g i = f (g i) := rfl
 
 end DComp
 
+/- ### The function product -/
+
 /-- 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 : ι) :
@@ -57,6 +59,35 @@ lemma prod_fst_snd {α β} : Function.prod (Prod.fst : α × β → α) (Prod.sn
 lemma prod_snd_fst {α β} : Function.prod (Prod.snd : α × β → β) (Prod.fst : α × β → α) = .swap :=
   rfl
 
+/- ### The diagonal map -/
+
+/-- The diagonal map into `Prod`. -/
+@[inline] protected def diag {α} : α → α × α := Function.prod id id
+
+@[inherit_doc] notation:max "△(" x:min ")" => Function.diag x
+
+section Diag
+
+variable {α β γ : Type*} (f : α → β) (g : α → γ) (a b : α)
+
+theorem diag_def : Function.diag = fun a : α => (a, a) := rfl
+
+@[simp, grind =] theorem diag_apply : △(a) = (a, a) := rfl
+
+@[simp] theorem prod_id_id : Function.prod id id = Function.diag (α := α) := rfl
+@[simp] theorem fst_comp_diag : Prod.fst ∘ Function.diag (α := α) = id := rfl
+@[simp] theorem snd_comp_diag : Prod.snd ∘ Function.diag (α := α) = id := rfl
+
+@[simp] theorem diag_comp : Function.diag ∘ f = Function.prod f f := rfl
+
+@[simp] theorem map_comp_diag : Prod.map f g ∘ Function.diag = Function.prod f g := rfl
+
+theorem injective_diag : Injective (α := α) Function.diag := fun _ _ => congrArg Prod.fst
+
+@[simp] theorem swap_comp_diag : Prod.swap ∘ Function.diag = Function.diag (α := α) := rfl
+
+end Diag
+
 /-- 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/MeasureTheory/MeasurableSpace/Constructions.lean

@@ -417,6 +417,13 @@ theorem measurable_prodMk_left {x : α} : Measurable (@Prod.mk _ β x) :=
 theorem measurable_prodMk_right {y : β} : Measurable fun x : α => (x, y) :=
   measurable_id.prodMk measurable_const
 
+@[fun_prop]
+theorem measurable_diag : @Measurable α (α × α) m (m.prod m) Function.diag :=
+  measurable_id.prodMk measurable_id
+
+theorem measurable_diag' {m'} (h : m' ≤ m) : @Measurable α (α × α) m (m.prod m') Function.diag :=
+  measurable_id.prodMk (measurable_id'' h)
+
 theorem Measurable.of_uncurry_left {f : α → β → γ} (hf : Measurable (uncurry f)) {x : α} :
     Measurable (f x) :=
   hf.comp measurable_prodMk_left

Mathlib/NumberTheory/Height/Basic.lean

@@ -759,7 +759,7 @@ lemma mulHeight_mul_le (x y : ι → K) : mulHeight (x * y) ≤ mulHeight x * mu
   rcases eq_or_ne y 0 with rfl | hy
   · simpa using one_le_mulHeight x
   rw [← mulHeight_fun_mul_eq hx hy,
-    show x * y = (fun a ↦ x a.1 * y a.2) ∘ fun i ↦ (i, i) by ext1; simp]
+    show x * y = (fun a ↦ x a.1 * y a.2) ∘ Function.diag by ext1; simp]
   exact mulHeight_comp_le ..
 
 open Real in

Mathlib/Order/Filter/Prod.lean

@@ -202,7 +202,7 @@ theorem Eventually.diag_of_prod_right {f : Filter α} {g : Filter γ} {p : α ×
   obtain ⟨t, ht, s, hs, hst⟩ := eventually_prod_iff.1 h
   exact (ht.prod_mk hs.diag_of_prod).mono fun x hx => by simp only [hst hx.1 hx.2]
 
-theorem tendsto_diag : Tendsto (fun i => (i, i)) f (f ×ˢ f) :=
+theorem tendsto_diag : Tendsto Function.diag f (f ×ˢ f) :=
   tendsto_iff_eventually.mpr fun _ hpr => hpr.diag_of_prod
 
 theorem prod_iInf_left [Nonempty ι] {f : ι → Filter α} {g : Filter β} :

Mathlib/Probability/Independence/Conditional.lean

@@ -804,9 +804,8 @@ lemma condIndepFun_iff_map_prod_eq_prod_comp_trim
           ∘ₘ μ.trim hm' := by
   rw [condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map hf hg]
   congr!
-  · rw [Measure.compProd_map (by fun_prop), compProd_trim_condExpKernel,
-      Measure.map_map (by fun_prop) ((measurable_id.mono le_rfl hm').prodMk measurable_id)]
-    rfl
+  · rw [Measure.compProd_map (by fun_prop), compProd_trim_condExpKernel]
+    exact Measure.map_map (by fun_prop) ((measurable_id.mono le_rfl hm').prodMk measurable_id)
   · rw [Measure.compProd_eq_comp_prod]
 
 /-- Two random variables `f, g` are conditionally independent given a third `k` iff the

Mathlib/Probability/Kernel/Basic.lean

@@ -130,7 +130,7 @@ section Copy
 /-- The deterministic kernel that maps `x : α` to the Dirac measure at `(x, x) : α × α`. -/
 noncomputable
 def copy (α : Type*) [MeasurableSpace α] : Kernel α (α × α) :=
-  Kernel.deterministic (fun x ↦ (x, x)) (measurable_id.prod measurable_id)
+  Kernel.deterministic Function.diag (measurable_id.prod measurable_id)
 
 instance : IsMarkovKernel (copy α) := by rw [copy]; infer_instance
 

Mathlib/Probability/Kernel/Composition/MeasureComp.lean

@@ -95,8 +95,9 @@ lemma discard_comp (μ : Measure α) : Kernel.discard α ∘ₘ μ = μ .univ 
 
 lemma copy_comp_map {f : α → β} (hf : AEMeasurable f μ) :
     Kernel.copy β ∘ₘ (μ.map f) = μ.map (fun a ↦ (f a, f a)) := by
-  rw [Kernel.copy, deterministic_comp_eq_map, AEMeasurable.map_map_of_aemeasurable (by fun_prop) hf]
-  rfl
+  simp_rw [Kernel.copy, deterministic_comp_eq_map, Function.diag_def,
+    AEMeasurable.map_map_of_aemeasurable
+    (AEMeasurable.prodMk (aemeasurable_id') (aemeasurable_id')) hf, Function.comp_def]
 
 section CompProd
 

Mathlib/Probability/Kernel/Composition/MeasureCompProd.lean

@@ -99,14 +99,14 @@ lemma _root_.ProbabilityTheory.Kernel.compProd_apply_eq_compProd_sectR {γ : Typ
   ext s hs
   simp_rw [Kernel.compProd_apply hs, compProd_apply hs, Kernel.sectR_apply]
 
-lemma compProd_id [SFinite μ] : μ ⊗ₘ Kernel.id = μ.map (fun x ↦ (x, x)) := by
+lemma compProd_id [SFinite μ] : μ ⊗ₘ Kernel.id = μ.map Function.diag := by
   ext s hs
   rw [compProd_apply hs, map_apply (measurable_id.prod measurable_id) hs]
   have h_meas a : MeasurableSet (Prod.mk a ⁻¹' s) := measurable_prodMk_left hs
   simp_rw [Kernel.id_apply, dirac_apply' _ (h_meas _)]
   calc ∫⁻ a, (Prod.mk a ⁻¹' s).indicator 1 a ∂μ
-  _ = ∫⁻ a, ((fun x ↦ (x, x)) ⁻¹' s).indicator 1 a ∂μ := rfl
-  _ = μ ((fun x ↦ (x, x)) ⁻¹' s) := by
+  _ = ∫⁻ a, ((Function.diag) ⁻¹' s).indicator 1 a ∂μ := rfl
+  _ = μ (Function.diag ⁻¹' s) := by
     rw [lintegral_indicator_one]
     exact (measurable_id.prod measurable_id) hs
 

Mathlib/Probability/Kernel/Condexp.lean

@@ -46,15 +46,14 @@ section AuxLemmas
 variable {Ω F : Type*} {m mΩ : MeasurableSpace Ω} {μ : Measure Ω} {f : Ω → F}
 
 theorem _root_.MeasureTheory.AEStronglyMeasurable.comp_snd_map_prod_id [TopologicalSpace F]
-    (hm : m ≤ mΩ) (hf : AEStronglyMeasurable f μ) :
+    (hf : AEStronglyMeasurable f μ) :
     AEStronglyMeasurable[m.prod mΩ] (fun x : Ω × Ω => f x.2)
-      (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω => (id ω, id ω)) μ) := by
-  simpa using (aestronglyMeasurable_comp_snd_map_prodMk_iff hm).mpr hf
+      (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) Function.diag μ) := hf.comp_snd_map_prodMk id
 
 theorem _root_.MeasureTheory.Integrable.comp_snd_map_prod_id [NormedAddCommGroup F]
     (hf : Integrable f μ) : Integrable (fun x : Ω × Ω => f x.2)
-      (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω => (id ω, id ω)) μ) := by
-  simpa using Integrable.comp_snd_map_prodMk id hf
+      (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) Function.diag μ) :=
+  hf.comp_snd_map_prodMk id
 
 end AuxLemmas
 
@@ -92,21 +91,21 @@ instance : IsMarkovKernel (condExpKernel μ m) := by
 
 lemma compProd_trim_condExpKernel (hm : m ≤ mΩ) :
     (μ.trim hm) ⊗ₘ condExpKernel μ m
-      = @Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω ↦ (id ω, id ω)) μ := by
+      = @Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) Function.diag μ := by
   rcases isEmpty_or_nonempty Ω with h | h
   · simp [Measure.eq_zero_of_isEmpty μ]
-  rw [condExpKernel_eq]
+  rw [condExpKernel_eq, trim_eq_map hm]
   have : m ⊓ mΩ = m := inf_of_le_left hm
-  have h := compProd_map_condDistrib (mβ := m) (μ := μ) (X := id) measurable_id.aemeasurable
-  rw [← h, trim_eq_map hm]
-  congr 1
-  ext a s hs
+  refine (congrArg _ (Kernel.ext fun a => Measure.ext fun s hs => ?_)).trans
+    (compProd_map_condDistrib measurable_id.aemeasurable)
   simp only [Kernel.coe_comap, Function.comp_apply, id_eq]
   congr
 
 lemma condExpKernel_comp_trim (hm : m ≤ mΩ) : condExpKernel μ m ∘ₘ μ.trim hm = μ := by
-  rw [← Measure.snd_compProd, compProd_trim_condExpKernel, @Measure.snd_map_prodMk, Measure.map_id]
-  exact measurable_id'' hm
+  rw [← Measure.snd_compProd, compProd_trim_condExpKernel, @Measure.snd_map_prodMk]
+  · simp_rw [Function.diag_apply]
+    exact Measure.map_id'
+  · exact measurable_id'' hm
 
 section Measurability
 
@@ -139,16 +138,15 @@ theorem _root_.MeasureTheory.AEStronglyMeasurable.integral_condExpKernel [Normed
   simp_rw [condExpKernel_apply_eq_condDistrib]
   exact AEStronglyMeasurable.integral_condDistrib
     (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
-    (hf.comp_snd_map_prod_id inf_le_right)
+    hf.comp_snd_map_prod_id
 
 theorem aestronglyMeasurable_integral_condExpKernel [NormedSpace ℝ F]
     (hf : AEStronglyMeasurable f μ) :
     AEStronglyMeasurable[m] (fun ω => ∫ y, f y ∂condExpKernel μ m ω) μ := by
   nontriviality Ω
   rw [condExpKernel_eq]
   have h := aestronglyMeasurable_integral_condDistrib
-    (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id
-    (hf.comp_snd_map_prod_id (inf_le_right : m ⊓ mΩ ≤ mΩ))
+    (aemeasurable_id'' μ (inf_le_right : m ⊓ mΩ ≤ mΩ)) aemeasurable_id hf.comp_snd_map_prod_id
   rw [MeasurableSpace.comap_id] at h
   exact h.mono inf_le_left
 

Mathlib/Probability/Kernel/Deterministic.lean

@@ -68,7 +68,7 @@ lemma parallelComp_self_comp_copy {κ : Kernel α β} [IsDeterministic κ] :
 instance {f : α → β} (hf : Measurable f) : IsDeterministic (deterministic f hf) where
   parallelComp_self_comp_copy' := by
     simp_rw [parallelComp_comp_copy, deterministic_prod_deterministic, copy,
-      deterministic_comp_deterministic, Function.comp_def]
+      deterministic_comp_deterministic, Function.comp_def, Function.diag_def]
 
 instance : IsDeterministic (mβ := mα) (Kernel.id (α := α)) := by unfold Kernel.id; infer_instance
 

Mathlib/Probability/Moments/SubGaussian.lean

@@ -882,8 +882,8 @@ lemma HasSubgaussianMGF.add_of_hasCondSubgaussianMGF [IsFiniteMeasure μ]
     (hX : HasSubgaussianMGF X cX (μ.trim hm)) (hY : HasCondSubgaussianMGF m hm Y cY μ) :
     HasSubgaussianMGF (X + Y) (cX + cY) μ := by
   suffices HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (cX + cY)
-      (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω ↦ (id ω, id ω)) μ) by
-    have h_eq : X + Y = (fun p ↦ X p.1 + Y p.2) ∘ (fun ω ↦ (id ω, id ω)) := rfl
+      (@Measure.map Ω (Ω × Ω) mΩ (m.prod mΩ) Function.diag μ) by
+    have h_eq : X + Y = (fun p ↦ X p.1 + Y p.2) ∘ Function.diag := rfl
     rw [h_eq]
     refine HasSubgaussianMGF.of_map ?_ this
     exact @Measurable.aemeasurable _ _ _ (m.prod mΩ) _ _

Mathlib/Topology/Algebra/ProperAction/Basic.lean

@@ -139,7 +139,7 @@ theorem t2Space_of_properSMul_of_t1Group [h_proper : ProperSMul G X] [T1Space G]
   rw [t2_iff_isClosed_diagonal]
   let g := fun gx : G × X ↦ (gx.1 • gx.2, gx.2)
   have proper_g : IsProperMap g := (properSMul_iff G X).1 h_proper
-  have : g ∘ f = fun x ↦ (x, x) := by ext x <;> simp [f, g]
+  have : g ∘ f = Function.diag := by ext x <;> simp [f, g]
   have range_gf : range (g ∘ f) = diagonal X := by simp [this]
   rw [← range_gf]
   exact (proper_g.comp proper_f).isClosed_range

Mathlib/Topology/Compactness/Compact.lean

@@ -428,7 +428,7 @@ theorem IsCompact.mem_prod_nhdsSet_of_forall {K : Set Y} {X} {l : Filter X} {s :
 -- That would seem a bit more natural.
 theorem IsCompact.nhdsSet_inf_eq_biSup {K : Set X} (hK : IsCompact K) (l : Filter X) :
     (𝓝ˢ K) ⊓ l = ⨆ x ∈ K, 𝓝 x ⊓ l := by
-  have : ∀ f : Filter X, f ⊓ l = comap (fun x ↦ (x, x)) (f ×ˢ l) := fun f ↦ by
+  have : ∀ f : Filter X, f ⊓ l = comap Function.diag (f ×ˢ l) := fun f ↦ by
     simpa only [comap_prod] using! congrArg₂ (· ⊓ ·) comap_id.symm comap_id.symm
   simp_rw [this, ← comap_iSup, hK.nhdsSet_prod_eq_biSup]
 

Mathlib/Topology/Constructions/SumProd.lean

@@ -147,6 +147,10 @@ theorem Continuous.prodMk_right (x : X) : Continuous fun y : Y => (x, y) := by f
 @[continuity]
 theorem Continuous.prodMk_left (y : Y) : Continuous fun x : X => (x, y) := by fun_prop
 
+@[continuity, fun_prop]
+theorem continuous_diag : Continuous (Function.diag : X → X × X) :=
+  continuous_id.prodMk continuous_id
+
 /-- If `f x y` is continuous in `x` for all `y ∈ s`,
 then the set of `x` such that `f x` maps `s` to `t` is closed. -/
 lemma IsClosed.setOf_mapsTo {α : Type*} {f : X → α → Z} {s : Set α} {t : Set Z} (ht : IsClosed t)

Mathlib/Topology/UniformSpace/UniformConvergence.lean

@@ -292,12 +292,12 @@ protected theorem TendstoUniformlyOn.prodMk {ι' β' : Type*} [UniformSpace β']
     (h' : TendstoUniformlyOn F' f' p' s) :
     TendstoUniformlyOn (fun (i : ι × ι') a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ p')
       s :=
-  (congr_arg _ s.inter_self).mp ((h.prodMap h').comp fun a => (a, a))
+  (congr_arg _ s.inter_self).mp ((h.prodMap h').comp Function.diag)
 
 theorem TendstoUniformly.prodMk {ι' β' : Type*} [UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'}
     {p' : Filter ι'} (h : TendstoUniformly F f p) (h' : TendstoUniformly F' f' p') :
     TendstoUniformly (fun (i : ι × ι') a => (F i.1 a, F' i.2 a)) (fun a => (f a, f' a)) (p ×ˢ p') :=
-  (h.prodMap h').comp fun a => (a, a)
+  (h.prodMap h').comp Function.diag
 
 /-- Uniform convergence on a filter `p'` to a constant function is equivalent to convergence in
 `p ×ˢ p'`. -/
@@ -550,7 +550,7 @@ theorem UniformCauchySeqOn.prodMap {ι' α' β' : Type*} [UniformSpace β'] {F'
 theorem UniformCauchySeqOn.prod {ι' β' : Type*} [UniformSpace β'] {F' : ι' → α → β'}
     {p' : Filter ι'} (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p' s) :
     UniformCauchySeqOn (fun (i : ι × ι') a => (F i.fst a, F' i.snd a)) (p ×ˢ p') s :=
-  (congr_arg _ s.inter_self).mp ((h.prodMap h').comp fun a => (a, a))
+  (congr_arg _ s.inter_self).mp ((h.prodMap h').comp Function.diag)
 
 theorem UniformCauchySeqOn.prod' {β' : Type*} [UniformSpace β'] {F' : ι → α → β'}
     (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p s) :