feat: Add Function.prod and Function.diag

Mathlib.lean

@@ -5117,6 +5117,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

@@ -371,11 +371,11 @@ variable [DistribMulAction R C]
 /-- The prod of two morphisms is a morphism. -/
 @[simps]
 def prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : A →ₙₐ[R] B × C where
-  toFun := Pi.prod f g
-  map_zero' := by simp only [Pi.prod, Prod.mk_zero_zero, map_zero]
-  map_add' x y := by simp only [Pi.prod, Prod.mk_add_mk, map_add]
-  map_mul' x y := by simp only [Pi.prod, Prod.mk_mul_mk, map_mul]
-  map_smul' c x := by simp only [Pi.prod, map_smul, MonoidHom.id_apply, Prod.smul_mk]
+  toFun := Function.prod f g
+  map_zero' := by simp only [Function.prod, Prod.mk_zero_zero, map_zero]
+  map_add' x y := by simp only [Function.prod, Prod.mk_add_mk, map_add]
+  map_mul' x y := by simp only [Function.prod, Prod.mk_mul_mk, map_mul]
+  map_smul' c x := by simp only [Function.prod, map_smul, MonoidHom.id_apply, Prod.smul_mk]
 
 theorem coe_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : ⇑(f.prod g) = Pi.prod f g :=
   rfl

Mathlib/Algebra/Algebra/Prod.lean

@@ -77,15 +77,15 @@ theorem snd_apply (a) : snd R A B a = a.2 := rfl
 
 variable {R}
 
-/-- The `Pi.prod` of two morphisms is a morphism. -/
+/-- The `Function.prod` of two morphisms is a morphism. -/
 @[simps!]
 def prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : A →ₐ[R] B × C :=
   { f.toRingHom.prod g.toRingHom with
     commutes' := fun r => by
       simp only [toRingHom_eq_coe, RingHom.toFun_eq_coe, RingHom.prod_apply, coe_toRingHom,
         commutes, Prod.algebraMap_apply] }
 
-theorem coe_prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : ⇑(f.prod g) = Pi.prod f g :=
+theorem coe_prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : ⇑(f.prod g) = Function.prod f g :=
   rfl
 
 @[simp]

Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

@@ -283,8 +283,8 @@ end bij
 
 @[to_additive (attr := simp)]
 lemma prod_diag (s : Finset ι) (f : ι × ι → M) :
-    ∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i) := by
-  simp [diag]
+    ∏ i ∈ s.diag, f i = ∏ i ∈ s, (f ∘ Function.diag) i := by
+  simp [diag, Function.diag_apply]
 
 @[to_additive]
 theorem prod_image' [DecidableEq ι] {s : Finset κ} {g : κ → ι} (h : κ → M)

Mathlib/Algebra/FiniteSupport/Basic.lean

@@ -55,7 +55,7 @@ lemma HasFiniteMulSupport.snd {M' : Type*} [One M'] {f : α → M × M'} (hf : H
 @[to_additive (attr := fun_prop)]
 lemma HasFiniteMulSupport.prodMk {M' : Type*} [One M'] {f : α → M} {g : α → M'}
     (hf : HasFiniteMulSupport f) (hg : HasFiniteMulSupport g) :
-    HasFiniteMulSupport fun a ↦ (f a, g a) := by
+    HasFiniteMulSupport (Function.prod f g) := by
   simp only [HasFiniteMulSupport] at hf hg ⊢
   rw [mulSupport_prodMk f g]
   exact hf.union hg

Mathlib/Algebra/Group/Prod.lean

@@ -221,11 +221,11 @@ theorem coe_snd : ⇑(snd M N) = Prod.snd :=
       `f.prod g : AddHom M (N × P)` given by `(f.prod g) x = (f x, g x)` -/]
 protected def prod (f : M →ₙ* N) (g : M →ₙ* P) :
     M →ₙ* N × P where
-  toFun := Pi.prod f g
+  toFun := Function.prod f g
   map_mul' x y := Prod.ext (f.map_mul x y) (g.map_mul x y)
 
 @[to_additive coe_prod]
-theorem coe_prod (f : M →ₙ* N) (g : M →ₙ* P) : ⇑(f.prod g) = Pi.prod f g :=
+theorem coe_prod (f : M →ₙ* N) (g : M →ₙ* P) : ⇑(f.prod g) = Function.prod f g :=
   rfl
 
 @[to_additive (attr := simp) prod_apply]
@@ -387,12 +387,12 @@ given by `(f.prod g) x = (f x, g x)`. -/
       `f.prod g : M →+ N × P` given by `(f.prod g) x = (f x, g x)` -/]
 protected def prod (f : M →* N) (g : M →* P) :
     M →* N × P where
-  toFun := Pi.prod f g
+  toFun := Function.prod f g
   map_one' := Prod.ext f.map_one g.map_one
   map_mul' x y := Prod.ext (f.map_mul x y) (g.map_mul x y)
 
 @[to_additive coe_prod]
-theorem coe_prod (f : M →* N) (g : M →* P) : ⇑(f.prod g) = Pi.prod f g :=
+theorem coe_prod (f : M →* N) (g : M →* P) : ⇑(f.prod g) = Function.prod f g :=
   rfl
 
 @[to_additive (attr := simp) prod_apply]

Mathlib/Algebra/Lie/Prod.lean

@@ -99,7 +99,7 @@ def prod (f : L →ₗ⁅R⁆ L₁) (g : L →ₗ⁅R⁆ L₂) : L →ₗ⁅R⁆
   toLinearMap := LinearMap.prod f g
   map_lie' := by simp
 
-theorem coe_prod (f : L →ₗ⁅R⁆ L₁) (g : L →ₗ⁅R⁆ L₂) : ⇑(f.prod g) = Pi.prod f g :=
+theorem coe_prod (f : L →ₗ⁅R⁆ L₁) (g : L →ₗ⁅R⁆ L₂) : ⇑(f.prod g) = Function.prod f g :=
   rfl
 
 @[simp]

Mathlib/Algebra/Notation/Pi/Defs.lean

@@ -26,14 +26,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/Notation/Support.lean

@@ -173,14 +173,13 @@ lemma mulSupport_comp_eq_preimage (g : κ → M) (f : ι → κ) :
 
 @[to_additive support_prodMk]
 lemma mulSupport_prodMk (f : ι → M) (g : ι → N) :
-    mulSupport (fun x ↦ (f x, g x)) = mulSupport f ∪ mulSupport g :=
-  Set.ext fun x ↦ by
-    simp only [mulSupport, not_and_or, mem_union, mem_setOf_eq, Prod.mk_eq_one, Ne]
+    mulSupport (f ⇊ g) = mulSupport f ∪ mulSupport g :=
+  Set.ext fun x ↦ by simp [mulSupport, Prod.ext_iff, imp_iff_not_or]
 
 @[to_additive support_prodMk']
 lemma mulSupport_prodMk' (f : ι → M × N) :
-    mulSupport f = (mulSupport fun x ↦ (f x).1) ∪ mulSupport fun x ↦ (f x).2 := by
-  simp only [← mulSupport_prodMk]
+    mulSupport f = (mulSupport (Prod.fst ∘ f)) ∪ mulSupport (Prod.snd ∘ f) := by
+  simp [← mulSupport_prodMk]
 
 @[to_additive]
 lemma mulSupport_along_fiber_subset (f : ι × κ → M) (i : ι) :

Mathlib/Algebra/Order/Antidiag/Pi.lean

@@ -149,10 +149,7 @@ lemma piAntidiag_empty (n : μ) : piAntidiag (∅ : Finset ι) n = if n = 0 then
 
 lemma finsetCongr_piAntidiag_eq_antidiag (n : μ) :
     Equiv.finsetCongr (Equiv.boolArrowEquivProd _) (piAntidiag univ n) = antidiagonal n := by
-  ext ⟨x₁, x₂⟩
-  simp_rw [Equiv.finsetCongr_apply, mem_map, Equiv.toEmbedding, Function.Embedding.coeFn_mk,
-    ← Equiv.eq_symm_apply]
-  simp [add_comm]
+  simp [Finset.ext_iff, flip, add_comm]
 
 end AddCommMonoid
 

Mathlib/Algebra/Ring/Prod.lean

@@ -132,7 +132,7 @@ variable [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T)
 `f.prod g : R →ₙ+* S × T` given by `(f.prod g) x = (f x, g x)` -/
 protected def prod (f : R →ₙ+* S) (g : R →ₙ+* T) : R →ₙ+* S × T :=
   { MulHom.prod (f : MulHom R S) (g : MulHom R T), AddMonoidHom.prod (f : R →+ S) (g : R →+ T) with
-    toFun := fun x => (f x, g x) }
+    toFun := Function.prod f g }
 
 @[simp]
 theorem prod_apply (x) : f.prod g x = (f x, g x) :=
@@ -208,7 +208,7 @@ variable [NonAssocSemiring T] (f : R →+* S) (g : R →+* T)
 given by `(f.prod g) x = (f x, g x)` -/
 protected def prod (f : R →+* S) (g : R →+* T) : R →+* S × T :=
   { MonoidHom.prod (f : R →* S) (g : R →* T), AddMonoidHom.prod (f : R →+ S) (g : R →+ T) with
-    toFun := fun x => (f x, g x) }
+    toFun := Function.prod f g }
 
 @[simp]
 theorem prod_apply (x) : f.prod g x = (f x, g x) :=

Mathlib/Algebra/Star/StarAlgHom.lean

@@ -485,13 +485,13 @@ def snd : A × B →⋆ₙₐ[R] B :=
 
 variable {R A B C}
 
-/-- The `Pi.prod` of two morphisms is a morphism. -/
+/-- The `Function.prod` of two morphisms is a morphism. -/
 @[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] }
 
-theorem coe_prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : ⇑(f.prod g) = Pi.prod f g :=
+theorem coe_prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : ⇑(f.prod g) = Function.prod f g :=
   rfl
 
 @[simp]
@@ -504,7 +504,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 Pi.prod_fst_snd
+  DFunLike.coe_injective Function.prod_fst_snd
 
 /-- Taking the product of two maps with the same domain is equivalent to taking the product of
 their codomains. -/
@@ -590,12 +590,12 @@ def snd : A × B →⋆ₐ[R] B :=
 
 variable {R A B C}
 
-/-- The `Pi.prod` of two morphisms is a morphism. -/
+/-- The `Function.prod` of two morphisms is a morphism. -/
 @[simps!]
 def prod (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : A →⋆ₐ[R] B × C :=
-  { f.toAlgHom.prod g.toAlgHom with map_star' := fun x => by simp [Prod.star_def, map_star] }
+  { f.toAlgHom.prod g.toAlgHom with map_star' := by simp [Prod.star_def, map_star, Prod.ext_iff] }
 
-theorem coe_prod (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : ⇑(f.prod g) = Pi.prod f g :=
+theorem coe_prod (f : A →⋆ₐ[R] B) (g : A →⋆ₐ[R] C) : ⇑(f.prod g) = Function.prod f g :=
   rfl
 
 @[simp]
@@ -608,7 +608,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 Pi.prod_fst_snd
+  DFunLike.coe_injective Function.prod_fst_snd
 
 /-- Taking the product of two maps with the same domain is equivalent to taking the product of
 their codomains. -/

Mathlib/Analysis/Analytic/Constructions.lean

@@ -290,7 +290,7 @@ lemma FormalMultilinearSeries.radius_prod_eq_min
 lemma HasFPowerSeriesWithinOnBall.prod {e : E} {f : E → F} {g : E → G} {r s : ℝ≥0∞} {t : Set E}
     {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
     (hf : HasFPowerSeriesWithinOnBall f p t e r) (hg : HasFPowerSeriesWithinOnBall g q t e s) :
-    HasFPowerSeriesWithinOnBall (fun x ↦ (f x, g x)) (p.prod q) t e (min r s) where
+    HasFPowerSeriesWithinOnBall (f ⇊ g) (p.prod q) t e (min r s) where
   r_le := by
     rw [p.radius_prod_eq_min]
     exact min_le_min hf.r_le hg.r_le
@@ -305,30 +305,30 @@ lemma HasFPowerSeriesWithinOnBall.prod {e : E} {f : E → F} {g : E → G} {r s
 lemma HasFPowerSeriesOnBall.prod {e : E} {f : E → F} {g : E → G} {r s : ℝ≥0∞}
     {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
     (hf : HasFPowerSeriesOnBall f p e r) (hg : HasFPowerSeriesOnBall g q e s) :
-    HasFPowerSeriesOnBall (fun x ↦ (f x, g x)) (p.prod q) e (min r s) := by
+    HasFPowerSeriesOnBall (f ⇊ g) (p.prod q) e (min r s) := by
   rw [← hasFPowerSeriesWithinOnBall_univ] at hf hg ⊢
   exact hf.prod hg
 
 lemma HasFPowerSeriesWithinAt.prod {e : E} {f : E → F} {g : E → G} {s : Set E}
     {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
     (hf : HasFPowerSeriesWithinAt f p s e) (hg : HasFPowerSeriesWithinAt g q s e) :
-    HasFPowerSeriesWithinAt (fun x ↦ (f x, g x)) (p.prod q) s e := by
+    HasFPowerSeriesWithinAt (f ⇊ g) (p.prod q) s e := by
   rcases hf with ⟨_, hf⟩
   rcases hg with ⟨_, hg⟩
   exact ⟨_, hf.prod hg⟩
 
 lemma HasFPowerSeriesAt.prod {e : E} {f : E → F} {g : E → G}
     {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G}
     (hf : HasFPowerSeriesAt f p e) (hg : HasFPowerSeriesAt g q e) :
-    HasFPowerSeriesAt (fun x ↦ (f x, g x)) (p.prod q) e := by
+    HasFPowerSeriesAt (f ⇊ g) (p.prod q) e := by
   rcases hf with ⟨_, hf⟩
   rcases hg with ⟨_, hg⟩
   exact ⟨_, hf.prod hg⟩
 
 /-- The Cartesian product of analytic functions is analytic. -/
 lemma AnalyticWithinAt.prod {e : E} {f : E → F} {g : E → G} {s : Set E}
     (hf : AnalyticWithinAt 𝕜 f s e) (hg : AnalyticWithinAt 𝕜 g s e) :
-    AnalyticWithinAt 𝕜 (fun x ↦ (f x, g x)) s e := by
+    AnalyticWithinAt 𝕜 (f ⇊ g) s e := by
   rcases hf with ⟨_, hf⟩
   rcases hg with ⟨_, hg⟩
   exact ⟨_, hf.prod hg⟩
@@ -337,21 +337,21 @@ lemma AnalyticWithinAt.prod {e : E} {f : E → F} {g : E → G} {s : Set E}
 @[fun_prop]
 lemma AnalyticAt.prod {e : E} {f : E → F} {g : E → G}
     (hf : AnalyticAt 𝕜 f e) (hg : AnalyticAt 𝕜 g e) :
-    AnalyticAt 𝕜 (fun x ↦ (f x, g x)) e := by
+    AnalyticAt 𝕜 (f ⇊ g) e := by
   rcases hf with ⟨_, hf⟩
   rcases hg with ⟨_, hg⟩
   exact ⟨_, hf.prod hg⟩
 
 /-- The Cartesian product of analytic functions within a set is analytic. -/
 lemma AnalyticOn.prod {f : E → F} {g : E → G} {s : Set E}
     (hf : AnalyticOn 𝕜 f s) (hg : AnalyticOn 𝕜 g s) :
-    AnalyticOn 𝕜 (fun x ↦ (f x, g x)) s :=
+    AnalyticOn 𝕜 (f ⇊ g) s :=
   fun x hx ↦ (hf x hx).prod (hg x hx)
 
 /-- The Cartesian product of analytic functions is analytic. -/
 lemma AnalyticOnNhd.prod {f : E → F} {g : E → G} {s : Set E}
     (hf : AnalyticOnNhd 𝕜 f s) (hg : AnalyticOnNhd 𝕜 g s) :
-    AnalyticOnNhd 𝕜 (fun x ↦ (f x, g x)) s :=
+    AnalyticOnNhd 𝕜 (f ⇊ g) s :=
   fun x hx ↦ (hf x hx).prod (hg x hx)
 
 /-- `AnalyticAt.comp` for functions on product spaces -/

Mathlib/Analysis/Asymptotics/TVS.lean

@@ -464,7 +464,7 @@ lemma IsLittleOTVS.bot : f =o[𝕜; ⊥] g :=
   ⟨fun u hU ↦ ⟨univ, by simp [EventuallyLE]⟩⟩
 
 theorem IsLittleOTVS.prodMk [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G}
-    (hf : f =o[𝕜; l] k) (hg : g =o[𝕜; l] k) : (fun x ↦ (f x, g x)) =o[𝕜; l] k := by
+    (hf : f =o[𝕜; l] k) (hg : g =o[𝕜; l] k) : (f ⇊ g) =o[𝕜; l] k := by
   rw [((nhds_basis_balanced 𝕜 E).prod_nhds (nhds_basis_balanced 𝕜 F)).isLittleOTVS_iff
     (basis_sets _)]
   rintro ⟨U, V⟩ ⟨⟨hU, hUb⟩, hV, hVb⟩
@@ -484,11 +484,11 @@ protected theorem IsLittleOTVS.snd {f : α → E × F} {g : α → G} (h : f =o[
 
 @[simp]
 theorem isLittleOTVS_prodMk_left [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G} :
-    (fun x ↦ (f x, g x)) =o[𝕜; l] k ↔ f =o[𝕜; l] k ∧ g =o[𝕜; l] k :=
+    (f ⇊ g) =o[𝕜; l] k ↔ f =o[𝕜; l] k ∧ g =o[𝕜; l] k :=
   ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.elim .prodMk⟩
 
 theorem IsBigOTVS.prodMk [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G}
-    (hf : f =O[𝕜; l] k) (hg : g =O[𝕜; l] k) : (fun x ↦ (f x, g x)) =O[𝕜; l] k := by
+    (hf : f =O[𝕜; l] k) (hg : g =O[𝕜; l] k) : (f ⇊ g) =O[𝕜; l] k := by
   rw [((nhds_basis_balanced 𝕜 E).prod_nhds (nhds_basis_balanced 𝕜 F)).isBigOTVS_iff (basis_sets _)]
   rintro ⟨U, V⟩ ⟨⟨hU, hUb⟩, hV, hVb⟩
   rcases ((hf.eventually_smallSets U hU).and (hg.eventually_smallSets V hV)).exists_mem_of_smallSets
@@ -507,7 +507,7 @@ protected theorem IsBigOTVS.snd {f : α → E × F} {g : α → G} (h : f =O[
 
 @[simp]
 theorem isBigOTVS_prodMk_left [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G} :
-    (fun x ↦ (f x, g x)) =O[𝕜; l] k ↔ f =O[𝕜; l] k ∧ g =O[𝕜; l] k :=
+    (f ⇊ g) =O[𝕜; l] k ↔ f =O[𝕜; l] k ∧ g =O[𝕜; l] k :=
   ⟨fun h ↦ ⟨h.fst, h.snd⟩, fun h ↦ h.elim .prodMk⟩
 
 @[to_fun]

Mathlib/Analysis/Calculus/ContDiff/Basic.lean

@@ -588,15 +588,15 @@ theorem ContDiff.prodMk {f : E → F} {g : E → G} (hf : ContDiff 𝕜 n f) (hg
 
 theorem iteratedFDerivWithin_prodMk {f : E → F} {g : E → G} (hf : ContDiffWithinAt 𝕜 n f s x)
     (hg : ContDiffWithinAt 𝕜 n g s x) (hs : UniqueDiffOn 𝕜 s) (ha : x ∈ s) {i : ℕ} (hi : i ≤ n) :
-    iteratedFDerivWithin 𝕜 i (fun x ↦ (f x, g x)) s x =
+    iteratedFDerivWithin 𝕜 i (f ⇊ g) s x =
       (iteratedFDerivWithin 𝕜 i f s x).prod (iteratedFDerivWithin 𝕜 i g s x) := by
   ext <;>
   · rw [← ContinuousLinearMap.iteratedFDerivWithin_comp_left _ (hf.prodMk hg) hs ha hi]
     simp [Function.comp_def]
 
 theorem iteratedFDeriv_prodMk {f : E → F} {g : E → G} (hf : ContDiffAt 𝕜 n f x)
     (hg : ContDiffAt 𝕜 n g x) {i : ℕ} (hi : i ≤ n) :
-    iteratedFDeriv 𝕜 i (fun x ↦ (f x, g x)) x =
+    iteratedFDeriv 𝕜 i (f ⇊ g) x =
       (iteratedFDeriv 𝕜 i f x).prod (iteratedFDeriv 𝕜 i g x) := by
   simp only [← iteratedFDerivWithin_univ]
   exact iteratedFDerivWithin_prodMk hf.contDiffWithinAt hg.contDiffWithinAt uniqueDiffOn_univ

Mathlib/Analysis/Calculus/ContDiffHolder/Pointwise.lean

@@ -134,7 +134,7 @@ theorem snd {a : E × F} : ContDiffPointwiseHolderAt k α Prod.snd a :=
 
 theorem prodMk {g : E → G} (hf : ContDiffPointwiseHolderAt k α f a)
     (hg : ContDiffPointwiseHolderAt k α g a) :
-    ContDiffPointwiseHolderAt k α (fun x ↦ (f x, g x)) a where
+    ContDiffPointwiseHolderAt k α (f ⇊ g) a where
   contDiffAt := hf.contDiffAt.prodMk hg.contDiffAt
   isBigO := calc
     _ =ᶠ[𝓝 a] (fun x ↦ (iteratedFDeriv ℝ k f x - iteratedFDeriv ℝ k f a).prod

Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean

@@ -85,7 +85,7 @@ theorem HasStrictFDerivAt.const_cpow (hf : HasStrictFDerivAt f f' x) (h0 : c ≠
 theorem HasFDerivAt.cpow (hf : HasFDerivAt f f' x) (hg : HasFDerivAt g g' x)
     (h0 : f x ∈ slitPlane) : HasFDerivAt (fun x => f x ^ g x)
       ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') x := by
-  convert (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp x (hf.prodMk hg)
+  convert (@Complex.hasFDerivAt_cpow ((Function.prod f g) x) h0).comp x (hf.prodMk hg)
 
 theorem HasFDerivAt.const_cpow (hf : HasFDerivAt f f' x) (h0 : c ≠ 0 ∨ f x ≠ 0) :
     HasFDerivAt (fun x => c ^ f x) ((c ^ f x * Complex.log c) • f') x :=
@@ -94,7 +94,7 @@ theorem HasFDerivAt.const_cpow (hf : HasFDerivAt f f' x) (h0 : c ≠ 0 ∨ f x 
 theorem HasFDerivWithinAt.cpow (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x)
     (h0 : f x ∈ slitPlane) : HasFDerivWithinAt (fun x => f x ^ g x)
       ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') s x := by
-  convert (@Complex.hasFDerivAt_cpow ((fun x => (f x, g x)) x) h0).comp_hasFDerivWithinAt x
+  convert (@Complex.hasFDerivAt_cpow ((Function.prod f g) x) h0).comp_hasFDerivWithinAt x
     (hf.prodMk hg)
 
 theorem HasFDerivWithinAt.const_cpow (hf : HasFDerivWithinAt f f' s x) (h0 : c ≠ 0 ∨ f x ≠ 0) :
@@ -387,7 +387,7 @@ theorem differentiableAt_rpow_of_ne (p : ℝ × ℝ) (hp : p.1 ≠ 0) :
 theorem _root_.HasStrictDerivAt.rpow {f g : ℝ → ℝ} {f' g' : ℝ} (hf : HasStrictDerivAt f f' x)
     (hg : HasStrictDerivAt g g' x) (h : 0 < f x) : HasStrictDerivAt (fun x => f x ^ g x)
       (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x := by
-  convert (hasStrictFDerivAt_rpow_of_pos ((fun x => (f x, g x)) x) h).comp_hasStrictDerivAt x
+  convert (hasStrictFDerivAt_rpow_of_pos ((Function.prod f g) x) h).comp_hasStrictDerivAt x
     (hf.prodMk hg) using 1
   simp [mul_assoc, mul_comm]
 

Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean

@@ -73,7 +73,7 @@ def lan (f : a ⟶ b) (g : a ⟶ c) [HasLeftKanExtension f g] : b ⟶ c :=
 /-- `f⁺ g` is the left Kan extension of `g` along `f`.
 ```
   b
-  △ \
+  ⇊ \
   |   \ f⁺ g
 f |     \
   |       ◿

Mathlib/Combinatorics/Enumerative/Catalan.lean

@@ -142,7 +142,7 @@ namespace Tree
 /-- Given two finsets, find all trees that can be formed with
   left child in `a` and right child in `b` -/
 abbrev pairwiseNode (a b : Finset (Tree Unit)) : Finset (Tree Unit) :=
-  (a ×ˢ b).map ⟨fun x => x.1 △ x.2, fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ => fun h => by simpa using h⟩
+  (a ×ˢ b).map ⟨fun x => x.1 ⇊ x.2, fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ => fun h => by simpa using h⟩
 
 /-- A Finset of all trees with `n` nodes. See `mem_treesOfNodesEq` -/
 def treesOfNumNodesEq : ℕ → Finset (Tree Unit)