From 1720cfdbe3d9bc246707ced88c1fea2f630c9f31 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Sat, 4 Apr 2026 16:15:37 +0100 Subject: [PATCH 01/23] Simply add the new functions --- Mathlib.lean | 1 + Mathlib/Logic/Function/Init.lean | 180 +++++++++++++++++++++++++++++++ 2 files changed, 181 insertions(+) create mode 100644 Mathlib/Logic/Function/Init.lean diff --git a/Mathlib.lean b/Mathlib.lean index 896c561fa97d3c..ed5cd718e178b1 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean new file mode 100644 index 00000000000000..b10bfb4442d606 --- /dev/null +++ b/Mathlib/Logic/Function/Init.lean @@ -0,0 +1,180 @@ +/- +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 mapping into a product type built from 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:65 " ⇊' " => Pi.prod + +section + +variable {ι} {α β : ι → Type*} (f f' : ∀ i, α i) (g g' : ∀ i, β i) {c} + +@[grind =] theorem prod_apply : (f ⇊' g) c = (f c, g c) := rfl + +@[simp] theorem fst_prod : ((f ⇊' g) c).fst = f c := rfl +@[simp] 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 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 + +end + +end Pi + +namespace Function + +variable {α β γ δ : Type*} {ι : Sort*} + +/-- This is the pairing operation on functions, dual to `Sum.elim`. -/ +protected def prod : (ι → α) → (ι → β) → ι → α × β := (· ⇊' ·) + +@[inherit_doc] infixr:65 " ⇊ " => Function.prod + +section + +variable (f : ι → α) (g : ι → β) + +@[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 + +@[simp] theorem fst_prod {c} : ((f ⇊ g) c).fst = f c := rfl +@[simp] theorem snd_prod {c} : ((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 + +@[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_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 + +@[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 + +end + +/-- `Function.prodMap` is `Prod.map` in the `Function` namespace. -/ +def prodMap (f : α → β) (g : γ → δ) := (f ∘ Prod.fst) ⇊ (g ∘ Prod.snd) + +@[simp, grind =] +theorem prodMap_eq_prod_map {f : α → β} {g : γ → δ} : f.prodMap g = Prod.map f g := rfl + +@[grind _=_] +theorem map_prod {f : α → β} {g : ι → α} {h : γ → δ} {k : ι → γ} {c} : + Prod.map f h ((g ⇊ k) c) = ((f ∘ g) ⇊ (h ∘ k)) c := rfl + +theorem map_comp_prod {f : α → β} {g : ι → α} {h : γ → δ} {k : ι → γ} : + Prod.map f h ∘ (g ⇊ k) = (f ∘ g) ⇊ (h ∘ k) := rfl + +/-- 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, grind =] theorem fst_diag : (⇗a).1 = a := rfl +@[simp, grind =] theorem snd_diag : (⇗a).2 = a := rfl + +@[simp, grind =] 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 + +@[simp] theorem exists_diag_apply_iff (p : α × α) : (∃ a, ⇗a = p) ↔ p.1 = p.2 := by + simp [Prod.ext_iff, eq_comm] + +@[simp] theorem diag_eq_iff : ⇗a = ⇗b ↔ a = b := injective_diag.eq_iff + +@[simp] theorem prod_diag_diag : Function.diag ⇊ Function.diag (α := α) = + Function.diag ∘ Function.diag := rfl + +end + + +end Function From 81d11ca2a12fa1a5a5281b3d452605be2cd6fc6a Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Sat, 4 Apr 2026 16:17:18 +0100 Subject: [PATCH 02/23] Remove old Pi.prod --- Mathlib/Algebra/Notation/Pi/Defs.lean | 8 -------- 1 file changed, 8 deletions(-) diff --git a/Mathlib/Algebra/Notation/Pi/Defs.lean b/Mathlib/Algebra/Notation/Pi/Defs.lean index 56fb6e87726968..68580139f65f3e 100644 --- a/Mathlib/Algebra/Notation/Pi/Defs.lean +++ b/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 From 262a3d45a870c95e14200373e29b5498d00ec665 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Sat, 4 Apr 2026 16:38:49 +0100 Subject: [PATCH 03/23] Improve lemmas --- Mathlib/Logic/Function/Init.lean | 44 ++++++++++++++++++++++---------- 1 file changed, 31 insertions(+), 13 deletions(-) diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index b10bfb4442d606..352c44e6e6057a 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -57,6 +57,9 @@ 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⟩ @@ -69,6 +72,12 @@ theorem exists_snd_comp (f : ∀ i, α i) (g : ∀ i, β i) : 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 @@ -126,25 +135,18 @@ theorem rightInverse_uncurry_prod_prod_fst_comp_snd_comp : Function.RightInverse @[grind =] theorem prod_const_const (a : α) (b : β) : - (Function.const ι a) ⇊ (Function.const ι b) = Function.const ι (a, b) := rfl + (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 -end - -/-- `Function.prodMap` is `Prod.map` in the `Function` namespace. -/ -def prodMap (f : α → β) (g : γ → δ) := (f ∘ Prod.fst) ⇊ (g ∘ Prod.snd) - -@[simp, grind =] -theorem prodMap_eq_prod_map {f : α → β} {g : γ → δ} : f.prodMap g = Prod.map f g := 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] -@[grind _=_] -theorem map_prod {f : α → β} {g : ι → α} {h : γ → δ} {k : ι → γ} {c} : - Prod.map f h ((g ⇊ k) c) = ((f ∘ g) ⇊ (h ∘ k)) c := rfl +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₂⟩ -theorem map_comp_prod {f : α → β} {g : ι → α} {h : γ → δ} {k : ι → γ} : - Prod.map f h ∘ (g ⇊ k) = (f ∘ g) ⇊ (h ∘ k) := rfl +end /-- The diagonal map into `Prod`. -/ protected def diag : α → α × α := id ⇊ id @@ -176,5 +178,21 @@ theorem injective_diag : Function.Injective (α := α) Function.diag := fun _ _ 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 + +@[grind _=_] +theorem map_prod {f : α → β} {g : ι → α} {h : γ → δ} {k : ι → γ} {c} : + Prod.map f h ((g ⇊ k) c) = ((f ∘ g) ⇊ (h ∘ k)) c := rfl + +theorem map_comp_prod {f : α → β} {g : ι → α} {h : γ → δ} {k : ι → γ} : + Prod.map f h ∘ (g ⇊ k) = (f ∘ g) ⇊ (h ∘ k) := rfl + +end end Function From 584c8217d5fcb666aa22149f63d81dbae3cbc9e4 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Sat, 4 Apr 2026 16:40:15 +0100 Subject: [PATCH 04/23] Add dependency --- Mathlib/Algebra/Notation/Pi/Defs.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Algebra/Notation/Pi/Defs.lean b/Mathlib/Algebra/Notation/Pi/Defs.lean index 68580139f65f3e..56b421196ac5aa 100644 --- a/Mathlib/Algebra/Notation/Pi/Defs.lean +++ b/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 From 66defff648b708e46610516adc3e0e45d146e22f Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Sat, 4 Apr 2026 18:14:28 +0100 Subject: [PATCH 05/23] Fix proofs --- Mathlib/Algebra/BigOperators/Finprod.lean | 2 +- Mathlib/Algebra/Star/StarAlgHom.lean | 2 +- Mathlib/LinearAlgebra/Prod.lean | 2 +- Mathlib/SetTheory/Cardinal/Finite.lean | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean index 7945e7f8c79545..b843e07b231354 100644 --- a/Mathlib/Algebra/BigOperators/Finprod.lean +++ b/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) diff --git a/Mathlib/Algebra/Star/StarAlgHom.lean b/Mathlib/Algebra/Star/StarAlgHom.lean index 2ef669e39999ad..364b5f40a0d143 100644 --- a/Mathlib/Algebra/Star/StarAlgHom.lean +++ b/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 diff --git a/Mathlib/LinearAlgebra/Prod.lean b/Mathlib/LinearAlgebra/Prod.lean index 6416808409864e..a02771c94b807b 100644 --- a/Mathlib/LinearAlgebra/Prod.lean +++ b/Mathlib/LinearAlgebra/Prod.lean @@ -795,7 +795,7 @@ protected def skewProd (f : M →ₗ[R] M₄) : (M × M₃) ≃ₗ[R] M₂ × M f.comp (LinearMap.fst R M M₃)) with invFun := fun p : M₂ × M₄ => (e₁.symm p.1, e₂.symm (p.2 - f (e₁.symm p.1))) left_inv := fun p => by simp - right_inv := fun p => by simp } + right_inv := fun p => by simp [Prod.ext_iff] } @[simp] theorem skewProd_apply (f : M →ₗ[R] M₄) (x) : e₁.skewProd e₂ f x = (e₁ x.1, e₂ x.2 + f x.1) := diff --git a/Mathlib/SetTheory/Cardinal/Finite.lean b/Mathlib/SetTheory/Cardinal/Finite.lean index a5a8ff16138638..9a618a494b8171 100644 --- a/Mathlib/SetTheory/Cardinal/Finite.lean +++ b/Mathlib/SetTheory/Cardinal/Finite.lean @@ -237,7 +237,7 @@ theorem card_sigma {β : α → Type*} [Fintype α] [∀ a, Finite (β a)] : simp_rw [Nat.card_eq_fintype_card, Fintype.card_sigma] theorem card_pi {β : α → Type*} [Fintype α] : Nat.card (∀ a, β a) = ∏ a, Nat.card (β a) := by - simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, map_prod] + simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, _root_.map_prod] theorem card_fun [Finite α] : Nat.card (α → β) = Nat.card β ^ Nat.card α := by haveI := Fintype.ofFinite α From b893bfdd79feeba0bf787f9072070d7f0b30a2c9 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Sat, 4 Apr 2026 19:37:33 +0100 Subject: [PATCH 06/23] Fix issues --- Mathlib/Algebra/Exact.lean | 2 +- Mathlib/LinearAlgebra/Goursat.lean | 26 +++++++---------- Mathlib/Logic/Function/Init.lean | 29 ++++++++++--------- .../Topology/Algebra/InfiniteSum/Basic.lean | 6 ++-- 4 files changed, 30 insertions(+), 33 deletions(-) diff --git a/Mathlib/Algebra/Exact.lean b/Mathlib/Algebra/Exact.lean index ebc1d5bc983f25..c0e7e44ce161bf 100644 --- a/Mathlib/Algebra/Exact.lean +++ b/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] diff --git a/Mathlib/LinearAlgebra/Goursat.lean b/Mathlib/LinearAlgebra/Goursat.lean index 4090de1ada933a..56378065f5a1a0 100644 --- a/Mathlib/LinearAlgebra/Goursat.lean +++ b/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 diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index 352c44e6e6057a..139e8ab2c10638 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -35,10 +35,10 @@ section variable {ι} {α β : ι → Type*} (f f' : ∀ i, α i) (g g' : ∀ i, β i) {c} -@[grind =] theorem prod_apply : (f ⇊' g) c = (f c, g c) := rfl +@[simp, grind =] theorem prod_apply : (f ⇊' g) c = (f c, g c) := rfl -@[simp] theorem fst_prod : ((f ⇊' g) c).fst = f c := rfl -@[simp] theorem snd_prod : ((f ⇊' g) c).snd = 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 @@ -95,12 +95,12 @@ section variable (f : ι → α) (g : ι → β) -@[grind =] theorem prod_apply (c : ι) : (f.prod g) c = (f c, g c) := rfl +@[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 -@[simp] theorem fst_prod {c} : ((f ⇊ g) c).fst = f c := rfl -@[simp] theorem snd_prod {c} : ((f ⇊ g) c).snd = g c := 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 @@ -133,7 +133,7 @@ theorem rightInverse_uncurry_prod_prod_fst_comp_snd_comp : Function.RightInverse (Function.prod (ι := γ)).uncurry ((Prod.fst (α := α) ∘ ·) ⇊ (Prod.snd (β := β) ∘ ·)) := fun _ => rfl -@[grind =] +@[simp, grind =] theorem prod_const_const (a : α) (b : β) : (Function.const ι a) ⇊ (Function.const ι b) = Function.const ι (a, b) := rfl @@ -157,21 +157,22 @@ section variable {a b : α} -@[grind =] theorem diag_apply : ⇗a = (a, a) := rfl +@[simp, grind =] theorem diag_apply : ⇗a = (a, a) := rfl -@[simp, grind =] theorem fst_diag : (⇗a).1 = a := rfl -@[simp, grind =] theorem snd_diag : (⇗a).2 = a := rfl +theorem fst_diag : (⇗a).1 = a := rfl +theorem snd_diag : (⇗a).2 = a := rfl -@[simp, grind =] theorem map_diag {f : α → β} {g : α → γ} : Prod.map f g ⇗a = (f ⇊ g) 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 +@[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 -@[simp] theorem exists_diag_apply_iff (p : α × α) : (∃ a, ⇗a = p) ↔ p.1 = p.2 := by +theorem exists_diag_apply_iff (p : α × α) : (∃ a, ⇗a = p) ↔ p.1 = p.2 := by simp [Prod.ext_iff, eq_comm] -@[simp] theorem diag_eq_iff : ⇗a = ⇗b ↔ a = b := injective_diag.eq_iff +theorem diag_eq_iff : ⇗a = ⇗b ↔ a = b := injective_diag.eq_iff @[simp] theorem prod_diag_diag : Function.diag ⇊ Function.diag (α := α) = Function.diag ∘ Function.diag := rfl diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean index f58b4b5fd42f4b..ffd6230289c916 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean @@ -221,7 +221,7 @@ protected theorem HasProd.map [CommMonoid γ] [TopologicalSpace γ] (hf : HasPro protected theorem Topology.IsInducing.hasProd_iff [CommMonoid γ] [TopologicalSpace γ] {G} [FunLike G α γ] [MonoidHomClass G α γ] {g : G} (hg : IsInducing g) (f : β → α) (a : α) : HasProd (g ∘ f) (g a) L ↔ HasProd f a L := by - simp_rw [HasProd, comp_apply, ← map_prod] + simp_rw [HasProd, comp_apply, ← _root_.map_prod] exact hg.tendsto_nhds_iff.symm @[to_additive] @@ -261,7 +261,7 @@ lemma Topology.IsClosedEmbedding.map_tprod {ι α α' G : Type*} simp only [Multipliable, HasProd] at h ⊢ obtain ⟨b, hb⟩ := h obtain ⟨a, ha⟩ : b ∈ Set.range g := - hge.isClosed_range.mem_of_tendsto hb (.of_forall <| by simp [← map_prod]) + hge.isClosed_range.mem_of_tendsto hb (.of_forall <| by simp [← _root_.map_prod]) use a simp [hge.tendsto_nhds_iff, Function.comp_def, ha, hb] · simpa [tprod_bot hL] using @@ -288,7 +288,7 @@ lemma Topology.IsInducing.multipliable_iff_tprod_comp_mem_range [CommMonoid γ] · by_cases hL : L.NeBot · exact ⟨_, hf.map_tprod g hg.continuous⟩ · by_cases hfs : (mulSupport fun x ↦ g (f x)).Finite - · simp [tprod_bot hL, finprod_eq_prod _ hfs, ← map_prod] + · simp [tprod_bot hL, finprod_eq_prod _ hfs, ← _root_.map_prod] · exact ⟨1, by simp [tprod_bot hL, finprod_of_infinite_mulSupport hfs]⟩ · rintro ⟨hgf, a, ha⟩ use a From 6e4be8dc37d6d62deaa3eaff44b8465ced5f0628 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Sat, 4 Apr 2026 20:25:09 +0100 Subject: [PATCH 07/23] Add fixes --- Mathlib/Algebra/MvPolynomial/Eval.lean | 2 +- .../CategoryTheory/Bicategory/Extension.lean | 18 +-- .../CategoryTheory/Bicategory/Kan/HasKan.lean | 6 +- Mathlib/LinearAlgebra/Prod.lean | 2 +- Mathlib/Logic/Function/Init.lean | 104 +++++++++--------- .../Algebra/InfiniteSum/Constructions.lean | 2 +- 6 files changed, 67 insertions(+), 67 deletions(-) diff --git a/Mathlib/Algebra/MvPolynomial/Eval.lean b/Mathlib/Algebra/MvPolynomial/Eval.lean index 359c2a071f2435..d8e5c3941b70df 100644 --- a/Mathlib/Algebra/MvPolynomial/Eval.lean +++ b/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) : diff --git a/Mathlib/CategoryTheory/Bicategory/Extension.lean b/Mathlib/CategoryTheory/Bicategory/Extension.lean index 544da9e4986eb0..b4c9b65840c2d5 100644 --- a/Mathlib/CategoryTheory/Bicategory/Extension.lean +++ b/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 ▽ / ▽ diff --git a/Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean b/Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean index b1ddc68a75543a..c4c1ac07706075 100644 --- a/Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean +++ b/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 ``` -/ diff --git a/Mathlib/LinearAlgebra/Prod.lean b/Mathlib/LinearAlgebra/Prod.lean index a02771c94b807b..6416808409864e 100644 --- a/Mathlib/LinearAlgebra/Prod.lean +++ b/Mathlib/LinearAlgebra/Prod.lean @@ -795,7 +795,7 @@ protected def skewProd (f : M →ₗ[R] M₄) : (M × M₃) ≃ₗ[R] M₂ × M f.comp (LinearMap.fst R M M₃)) with invFun := fun p : M₂ × M₄ => (e₁.symm p.1, e₂.symm (p.2 - f (e₁.symm p.1))) left_inv := fun p => by simp - right_inv := fun p => by simp [Prod.ext_iff] } + right_inv := fun p => by simp } @[simp] theorem skewProd_apply (f : M →ₗ[R] M₄) (x) : e₁.skewProd e₂ f x = (e₁ x.1, e₂ x.2 + f x.1) := diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index 139e8ab2c10638..d8d1511875744f 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -9,7 +9,7 @@ public import Mathlib.Init /-! -This file defines `(f ⇊ g)`, the operation that pairs two functions `f : ι → α` and +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 @@ -25,33 +25,33 @@ upstreamed to Batteries or the Lean standard library easily. namespace Pi -/-- The mapping into a product type built from maps into each component. -/ +/-- 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:65 " ⇊' " => Pi.prod +@[inherit_doc] infixr:65 " ▽' " => 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 +@[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 +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 +@[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 + (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 +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] + 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 @@ -60,23 +60,23 @@ theorem prod_ext_iff {h h' : ∀ i, α i × β i} : h = h' ↔ 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 := +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⟩ + ∃ 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⟩ + ∃ 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 + (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] + 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₂⟩ + (h₂ : (Prod.snd <| h ·) = g) : h = f ▽' g := eq_prod_iff_fst_comp_snd_comp.mpr ⟨h₁, h₂⟩ end @@ -86,10 +86,10 @@ namespace Function variable {α β γ δ : Type*} {ι : Sort*} -/-- This is the pairing operation on functions, dual to `Sum.elim`. -/ -protected def prod : (ι → α) → (ι → β) → ι → α × β := (· ⇊' ·) +/-- The map into a product type built from maps into each component. -/ +protected def prod : (ι → α) → (ι → β) → ι → α × β := (· ▽' ·) -@[inherit_doc] infixr:65 " ⇊ " => Function.prod +@[inherit_doc] infixr:65 " ▽ " => Function.prod section @@ -97,90 +97,90 @@ 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 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 +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 : 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 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 +@[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_eq_iff {f f' : ι → α} {g g' : ι → β} : f ⇊ g = f' ⇊ g' ↔ +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 := +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⟩ + ∃ 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⟩ + ∃ 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 (β := β) ∘ ·)) := + (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 (β := β) ∘ ·)) := + (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 + (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 + 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] + 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₂⟩ + (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 +protected def diag : α → α × α := id ▽ id -@[inherit_doc] prefix:max "⇗" => Function.diag +@[inherit_doc] prefix:max "⟋" => Function.diag section variable {a b : α} -@[simp, grind =] theorem diag_apply : ⇗a = (a, a) := rfl +@[grind =] theorem diag_apply : ⟋a = (a, a) := rfl -theorem fst_diag : (⇗a).1 = a := rfl -theorem snd_diag : (⇗a).2 = 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 +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 + 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 +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 +theorem diag_eq_iff : ⟋a = ⟋b ↔ a = b := injective_diag.eq_iff -@[simp] theorem prod_diag_diag : Function.diag ⇊ Function.diag (α := α) = +@[simp] theorem prod_diag_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) +def prodMap (f : α → β) (g : γ → δ) := (f ∘ Prod.fst) ▽ (g ∘ Prod.snd) section @@ -189,10 +189,10 @@ theorem prodMap_eq_prod_map {f : α → β} {g : γ → δ} : f.prodMap g = Prod @[grind _=_] theorem map_prod {f : α → β} {g : ι → α} {h : γ → δ} {k : ι → γ} {c} : - Prod.map f h ((g ⇊ k) c) = ((f ∘ g) ⇊ (h ∘ k)) c := rfl + Prod.map f h ((g ▽ k) c) = ((f ∘ g) ▽ (h ∘ k)) c := rfl theorem map_comp_prod {f : α → β} {g : ι → α} {h : γ → δ} {k : ι → γ} : - Prod.map f h ∘ (g ⇊ k) = (f ∘ g) ⇊ (h ∘ k) := rfl + Prod.map f h ∘ (g ▽ k) = (f ∘ g) ▽ (h ∘ k) := rfl end diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean index dd08bd9caf1a31..2aa17a66aac2b1 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean @@ -274,7 +274,7 @@ variable {ι : Type*} {X : α → Type*} [∀ x, CommMonoid (X x)] [∀ x, Topol @[to_additive] theorem Pi.hasProd {f : ι → ∀ x, X x} {g : ∀ x, X x} : HasProd f g L ↔ ∀ x, HasProd (fun i ↦ f i x) (g x) L := by - simp only [HasProd, tendsto_pi_nhds, prod_apply] + simp only [HasProd, tendsto_pi_nhds, Finset.prod_apply] @[to_additive] theorem Pi.multipliable {f : ι → ∀ x, X x} : From 0869be604fbd55708310318158ffc6276cf1177e Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Sat, 4 Apr 2026 20:57:58 +0100 Subject: [PATCH 08/23] Final fixes? --- Mathlib/Algebra/MvPolynomial/Equiv.lean | 2 +- Mathlib/MeasureTheory/Measure/Prod.lean | 11 ++++++----- Mathlib/NumberTheory/Height/Basic.lean | 2 +- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/Mathlib/Algebra/MvPolynomial/Equiv.lean b/Mathlib/Algebra/MvPolynomial/Equiv.lean index 71e9d4d79f3873..19da7650094fdb 100644 --- a/Mathlib/Algebra/MvPolynomial/Equiv.lean +++ b/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, diff --git a/Mathlib/MeasureTheory/Measure/Prod.lean b/Mathlib/MeasureTheory/Measure/Prod.lean index 487fe7fd620c50..213eb7bcdb4589 100644 --- a/Mathlib/MeasureTheory/Measure/Prod.lean +++ b/Mathlib/MeasureTheory/Measure/Prod.lean @@ -841,7 +841,7 @@ theorem map_prod_map {δ} [MeasurableSpace δ] {f : α → β} {g : γ → δ} ( -- hence it is placed in the `WithDensity` file, where the instance is defined. lemma prod_smul_left {μ : Measure α} (c : ℝ≥0∞) : (c • μ).prod ν = c • (μ.prod ν) := by ext s hs - rw [Measure.prod_apply hs, Measure.smul_apply, Measure.prod_apply hs] + rw [prod_apply hs, Measure.smul_apply, prod_apply hs] simp end Measure @@ -877,7 +877,7 @@ theorem skew_product [SFinite μa] [SFinite μc] {f : α → β} (hf : MeasurePr infer_instance -- Thus we can use the integral formula for the product measure, and compute things explicitly ext s hs - rw [map_apply this hs, prod_apply (this hs), prod_apply hs, + rw [map_apply this hs, Measure.prod_apply (this hs), Measure.prod_apply hs, ← hf.lintegral_comp (measurable_measure_prodMk_left hs)] apply lintegral_congr_ae filter_upwards [hg] with a ha @@ -902,7 +902,7 @@ theorem prod_of_right {f : α × β → γ} {μ : Measure α} {ν : Measure β} QuasiMeasurePreserving f (μ.prod ν) τ := by refine ⟨hf, ?_⟩ refine AbsolutelyContinuous.mk fun s hs h2s => ?_ - rw [map_apply hf hs, prod_apply (hf hs)]; simp_rw [preimage_preimage] + rw [map_apply hf hs, Measure.prod_apply (hf hs)]; simp_rw [preimage_preimage] rw [lintegral_congr_ae (h2f.mono fun x hx => hx.preimage_null h2s), lintegral_zero] theorem prod_of_left {α β γ} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] @@ -1228,8 +1228,9 @@ theorem _root_.MeasureTheory.measurePreserving_prodAssoc (μa : Measure α) (μb have A (x : α) : MeasurableSet (Prod.mk x ⁻¹' s) := measurable_prodMk_left hs have B : MeasurableSet (MeasurableEquiv.prodAssoc ⁻¹' s) := MeasurableEquiv.prodAssoc.measurable hs - simp_rw [map_apply MeasurableEquiv.prodAssoc.measurable hs, prod_apply hs, prod_apply (A _), - prod_apply B, lintegral_prod _ (measurable_measure_prodMk_left B).aemeasurable] + simp_rw [map_apply MeasurableEquiv.prodAssoc.measurable hs, Measure.prod_apply hs, + Measure.prod_apply (A _), Measure.prod_apply B, + lintegral_prod _ (measurable_measure_prodMk_left B).aemeasurable] rfl theorem _root_.MeasureTheory.volume_preserving_prodAssoc {α₁ β₁ γ₁ : Type*} [MeasureSpace α₁] diff --git a/Mathlib/NumberTheory/Height/Basic.lean b/Mathlib/NumberTheory/Height/Basic.lean index 5366554e2b265f..75760ab28e1bfe 100644 --- a/Mathlib/NumberTheory/Height/Basic.lean +++ b/Mathlib/NumberTheory/Height/Basic.lean @@ -667,7 +667,7 @@ lemma mulHeight_fun_prod_eq {x : (a : α) → ι a → K} (hx : ∀ a, x a ≠ 0 simp_rw [ne_iff, Pi.zero_def] at hx ⊢ choose f hf using hx exact ⟨f, prod_ne_zero_iff.mpr fun a _ ↦ hf a⟩ - simp_rw [map_prod, Real.iSup_prod_eq_prod_iSup_of_nonnegHomClass] + simp_rw [_root_.map_prod, Real.iSup_prod_eq_prod_iSup_of_nonnegHomClass] rw [Multiset.prod_map_prod, finprod_prod_comm _ _ fun b _ ↦ hasFiniteMulSupport_iSup_nonarchAbsVal (hx b), ← prod_mul_distrib] From 3af101f551f49348940afce16556260a73f57e88 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Sat, 4 Apr 2026 21:26:16 +0100 Subject: [PATCH 09/23] Final fixes --- Mathlib/Combinatorics/Nullstellensatz.lean | 4 ++-- Mathlib/MeasureTheory/Integral/Prod.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Combinatorics/Nullstellensatz.lean b/Mathlib/Combinatorics/Nullstellensatz.lean index 457202856602dd..822cd6edadc591 100644 --- a/Mathlib/Combinatorics/Nullstellensatz.lean +++ b/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 diff --git a/Mathlib/MeasureTheory/Integral/Prod.lean b/Mathlib/MeasureTheory/Integral/Prod.lean index 184104dac5a778..d88a161eef0c89 100644 --- a/Mathlib/MeasureTheory/Integral/Prod.lean +++ b/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 From 5dd45bac3a5ad8aeb014b96e79eed0b8af791a41 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Sat, 4 Apr 2026 21:33:56 +0100 Subject: [PATCH 10/23] Fiddle with notation and lemmas --- Mathlib/Logic/Function/Init.lean | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index d8d1511875744f..7d1498b797ec19 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -29,7 +29,7 @@ namespace Pi protected def prod {ι} {α β : ι → Type*} (f : ∀ i, α i) (g : ∀ i, β i) (i : ι) : α i × β i := Prod.mk (f i) (g i) -@[inherit_doc] infixr:65 " ▽' " => Pi.prod +@[inherit_doc] infixr:95 " ▽' " => Pi.prod section @@ -89,7 +89,7 @@ variable {α β γ δ : Type*} {ι : Sort*} /-- The map into a product type built from maps into each component. -/ protected def prod : (ι → α) → (ι → β) → ι → α × β := (· ▽' ·) -@[inherit_doc] infixr:65 " ▽ " => Function.prod +@[inherit_doc] infixr:95 " ▽ " => Function.prod section @@ -110,6 +110,15 @@ theorem snd_prod {c} : ((f ▽ g) c).snd = g c := by simp @[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] @@ -174,7 +183,7 @@ theorem exists_diag_apply_iff (p : α × α) : (∃ a, ⟋a = p) ↔ p.1 = p.2 : theorem diag_eq_iff : ⟋a = ⟋b ↔ a = b := injective_diag.eq_iff -@[simp] theorem prod_diag_diag : Function.diag ▽ Function.diag (α := α) = +@[simp] theorem diag_prod_diag : Function.diag ▽ Function.diag (α := α) = Function.diag ∘ Function.diag := rfl end @@ -187,13 +196,6 @@ section @[simp, grind =] theorem prodMap_eq_prod_map {f : α → β} {g : γ → δ} : f.prodMap g = Prod.map f g := rfl -@[grind _=_] -theorem map_prod {f : α → β} {g : ι → α} {h : γ → δ} {k : ι → γ} {c} : - Prod.map f h ((g ▽ k) c) = ((f ∘ g) ▽ (h ∘ k)) c := rfl - -theorem map_comp_prod {f : α → β} {g : ι → α} {h : γ → δ} {k : ι → γ} : - Prod.map f h ∘ (g ▽ k) = (f ∘ g) ▽ (h ∘ k) := rfl - end end Function From 0d618f277b66e8fea90363becd3ac681a1e0bff8 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Mon, 20 Apr 2026 10:40:22 +0100 Subject: [PATCH 11/23] Restore diagrams --- .../CategoryTheory/Bicategory/Extension.lean | 18 +++++++++--------- .../CategoryTheory/Bicategory/Kan/HasKan.lean | 6 +++--- 2 files changed, 12 insertions(+), 12 deletions(-) diff --git a/Mathlib/CategoryTheory/Bicategory/Extension.lean b/Mathlib/CategoryTheory/Bicategory/Extension.lean index b4c9b65840c2d5..544da9e4986eb0 100644 --- a/Mathlib/CategoryTheory/Bicategory/Extension.lean +++ b/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 ▽ / ▽ diff --git a/Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean b/Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean index c4c1ac07706075..b1ddc68a75543a 100644 --- a/Mathlib/CategoryTheory/Bicategory/Kan/HasKan.lean +++ b/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 ``` -/ From 97aa62284938b04249104a882e765d0a8405d25c Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Tue, 21 Apr 2026 10:34:17 +0100 Subject: [PATCH 12/23] Update file --- Mathlib/Logic/Function/Defs.lean | 8 -- Mathlib/Logic/Function/Init.lean | 227 +++++++++++++++++-------------- 2 files changed, 122 insertions(+), 113 deletions(-) diff --git a/Mathlib/Logic/Function/Defs.lean b/Mathlib/Logic/Function/Defs.lean index 496fb5ef4729af..b4fda774f321d3 100644 --- a/Mathlib/Logic/Function/Defs.lean +++ b/Mathlib/Logic/Function/Defs.lean @@ -23,14 +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 - /-- 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 `α`. -/ diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index 7d1498b797ec19..42332a62c0f8a8 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -12,7 +12,7 @@ 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 +It also defines the special case when `f = g = id`, `diag`. This is the canonical injection of a type into its prouduct with itself onto its diagonal. @@ -23,178 +23,195 @@ upstreamed to Batteries or the Lean standard library easily. @[expose] public section -namespace Pi +namespace Function + +/- ### Dependent composition -/ -/-- 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) +/-- 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] def dcomp {ι} {β : ι → Sort*} {φ : ∀ {i : ι}, β i → Sort*} + (f : ∀ {i : ι} (y : β i), φ y) (g : ∀ i, β i) (i : ι) : φ (g i) := f (g i) -@[inherit_doc] infixr:95 " ▽' " => Pi.prod +@[inherit_doc] infixr:90 " ∘' " => dcomp section -variable {ι} {α β : ι → Type*} (f f' : ∀ i, α i) (g g' : ∀ i, β i) {c} +variable {ι} {β : ι → Sort*} {φ : ∀ {i : ι}, β i → Sort*} (f : ∀ {i : ι} (y : β i), φ y) + (g : ∀ i, β i) (i : ι) -@[simp, grind =] theorem prod_apply : (f ▽' g) c = (f c, g c) := rfl +@[simp] theorem dcomp_apply : dcomp f g i = f (g i) := rfl -theorem fst_prod : ((f ▽' g) c).fst = f c := rfl -theorem snd_prod : ((f ▽' g) c).snd = g c := rfl +theorem dcomp_def : f ∘' g = fun i => f (g i) := rfl -@[simp] theorem prod_fst_snd {α β} : (Prod.fst : _ → α) ▽' (Prod.snd : _ → β) = id := rfl -@[simp] theorem prod_snd_fst {α β} : (Prod.snd : _ → β) ▽' (Prod.fst : _ → α) = .swap := rfl +@[simp] theorem dcomp_eq_comp {α β γ} (f : β → γ) (g : α → β) : f ∘' g = f ∘ g := rfl -theorem prod_fst_snd_comp {h : ∀ i, α i × β i} : - (Prod.fst <| h ·) ▽' (Prod.snd <| h ·) = h := rfl +end -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 +/-- Product of functions: `(f ▽ g) x = (f i, g i)`, where the types of `f i` and `g i` +depend on `i`. -/ +@[inline] def prod {ι} {α β : ι → Type*} (f : ∀ i, α i) (g : ∀ i, β i) (i : ι) : + α i × β i := ⟨f i, g i⟩ -@[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] +/-- The first component of a map into a product. -/ +@[inline] def fstComp {ι} {α β : ι → Type*} (h : (i : ι) → α i × β i) (i : ι) : + α i := (h i).1 -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] +/-- The second component of a map into a product. -/ +@[inline] def sndComp {ι} {α β : ι → Type*} (h : (i : ι) → α i × β i) (i : ι) : + β i := (h i).2 -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₂⟩ +@[inherit_doc] infixr:95 " ▽ " => prod -theorem exists_prod_apply_eq (h : ∀ i, α i × β i) : ∃ f g, (f ▽' g) = h := - ⟨(Prod.fst <| h ·), (Prod.snd <| h ·), prod_fst_snd_comp⟩ +section -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⟩ +variable {ι κ} {α β : ι → Type*} (f f' : ∀ i, α i) (g g' : ∀ i, β i) (h : ∀ i, α i × β i) + (i : ι) -@[grind =] -theorem prod_const_const {ι} {α β} {a : α} {b : β} : - (Function.const ι a) ▽' (Function.const ι b) = Function.const ι (a, b) := rfl +@[simp, grind =] theorem prod_apply : (f ▽ g) i = (f i, g i) := rfl +@[simp, grind =] theorem fstComp_apply : fstComp h i = (h i).1 := rfl +@[simp, grind =] theorem sndComp_apply : fstComp h i = (h i).1 := 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 prod_def : f ▽ g = fun i => (f i, g i) := rfl -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₂⟩ +@[simp] theorem fst_dcomp : Prod.fst ∘' h = fstComp h := rfl +@[simp] theorem snd_dcomp : Prod.snd ∘' h = sndComp h := rfl -end +@[simp, grind! .] theorem fstComp_prod {f : ∀ i, α i} {g : ∀ i, β i} : + fstComp (f ▽ g) = f := rfl +@[simp, grind! .] theorem sndComp_prod {f : ∀ i, α i} {g : ∀ i, β i} : + sndComp (f ▽ g) = g := rfl +@[simp, grind! .] theorem fstComp_prod_sndComp {h : ∀ i, α i × β i} : + fstComp h ▽ sndComp h = h := rfl -end Pi +theorem fstComp_sndComp_ext {h h' : ∀ i, α i × β i} (H₁ : fstComp h = fstComp h') + (H₂ : sndComp h = sndComp h') : h = h' := by grind -namespace Function +theorem fstComp_sndComp_ext_iff {h h' : ∀ i, α i × β i} : + h = h' ↔ fstComp h = fstComp h' ∧ sndComp h = sndComp h' := by grind -variable {α β γ δ : Type*} {ι : Sort*} +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 -/-- The map into a product type built from maps into each component. -/ -protected def prod : (ι → α) → (ι → β) → ι → α × β := (· ▽' ·) +@[simp] theorem prod_inj {f f' : ∀ i, α i} {g g' : ∀ i, β i} : + f ▽ g = f' ▽ g' ↔ f = f' ∧ g = g' := by grind -@[inherit_doc] infixr:95 " ▽ " => Function.prod +theorem exists_pair_prod : ∃ f g, f ▽ g = h := + ⟨fstComp h, sndComp h, fstComp_prod_sndComp⟩ +theorem exists_fstComp [Nonempty (∀ i, β i)] : ∃ h : ∀ i, α i × β i, fstComp h = f := + ⟨f ▽ Classical.ofNonempty, fstComp_prod⟩ +theorem exists_sndComp [Nonempty (∀ i, α i)] : ∃ h : ∀ i, α i × β i, sndComp h = g := + ⟨Classical.ofNonempty ▽ g, sndComp_prod⟩ -section +theorem prod_eq_iff : f ▽ g = h ↔ f = fstComp h ∧ g = sndComp h := by grind +theorem eq_prod_iff : h = f ▽ g ↔ fstComp h = f ∧ sndComp h = g := by grind -variable (f : ι → α) (g : ι → β) +theorem prod_dcomp (h : κ → ι) : (f ▽ g) ∘' h = (f ∘' h) ▽ (g ∘' h) := rfl -@[simp, grind =] theorem prod_apply (c : ι) : (f.prod g) c = (f c, g c) := rfl +theorem prod_dcomp_prod {γ δ : ∀ {i : ι}, α i × β i → Type*} + (h : {i : ι} → (ab : α i × β i) → γ ab) (k : {i : ι} → (ab : α i × β i) → δ ab) : + (h ▽ k) ∘' (f ▽ g) = (h ∘' (f ▽ g)) ▽ (k ∘' (f ▽ g)) := rfl -theorem prod_comp {γ} {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 -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 swap_dcomp_prod : Prod.swap ∘' (f ▽ g) = g ▽ f := rfl -@[simp] theorem prod_fst_snd : Prod.fst (α := α) ▽ Prod.snd (β := β) = id := rfl -@[simp] theorem prod_snd_fst : Prod.snd (β := β) ▽ Prod.fst (α := α) = .swap := rfl +end -@[simp] theorem prod_fst_snd_comp {f : ι → α × β} : (Prod.fst ∘ f) ▽ (Prod.snd ∘ f) = f := rfl +section -@[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 +variable {ι : Type*} {α β : ι → Type*} -theorem prod_comp_prod {f : ι → α} {g : ι → β} {h : α × β → γ} {k : α × β → δ} : - (h ▽ k) ∘ (f ▽ g) = (h ∘ (f ▽ g)) ▽ (k ∘ (f ▽ g)) := rfl +theorem leftInverse_uncurry_prod_fstComp_prod_sndComp : + LeftInverse prod.uncurry (fstComp (α := α) ▽ sndComp (β := β)) := by + simp [LeftInverse] -theorem comp_prod_comp {f : ι → α} {g : ι → β} {h : α → γ} {k : β → δ} : - (h ∘ f) ▽ (k ∘ g) = (h ∘ Prod.fst) ▽ (k ∘ Prod.snd) ∘ f ▽ g := rfl +theorem rightInverse_uncurry_prod_fstComp_prod_sndComp : + RightInverse prod.uncurry (fstComp (α := α) ▽ sndComp (β := β)) := by + simp [RightInverse, LeftInverse] -theorem map_comp_prod {f : ι → α} {g : ι → β} {h : α → γ} {k : β → δ} : - Prod.map h k ∘ f ▽ g = (h ∘ f) ▽ (k ∘ g) := rfl +theorem uncurry_prod_injective : (prod (α := α) (β := β)).uncurry.Injective := + rightInverse_uncurry_prod_fstComp_prod_sndComp.injective -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 uncurry_prod_surjective : (prod (α := α) (β := β)).uncurry.Surjective := + RightInverse.surjective leftInverse_uncurry_prod_fstComp_prod_sndComp -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] +end -theorem exists_prod_apply_eq (h : ι → α × β) : ∃ f g, f ▽ g = h := - ⟨Prod.fst ∘ h, Prod.snd ∘ h, prod_fst_snd_comp⟩ +section -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⟩ +variable {α β γ δ : Type*} {ι κ : Sort*} (f : ι → α) (g : ι → β) + (a : α) (b : β) (p : α × β) -theorem leftInverse_uncurry_prod_prod_fst_comp_snd_comp : Function.LeftInverse - (Function.prod (ι := γ)).uncurry ((Prod.fst (α := α) ∘ ·) ▽ (Prod.snd (β := β) ∘ ·)) := - fun _ => rfl +@[simp] theorem fst_comp (h : ι → α × β) : Prod.fst ∘ h = fstComp h := rfl +@[simp] theorem snd_comp (h : ι → α × β) : Prod.snd ∘ h = sndComp h := rfl -theorem rightInverse_uncurry_prod_prod_fst_comp_snd_comp : Function.RightInverse - (Function.prod (ι := γ)).uncurry ((Prod.fst (α := α) ∘ ·) ▽ (Prod.snd (β := β) ∘ ·)) := - fun _ => rfl +@[simp] theorem fst_prod_snd : (Prod.fst : _ → α) ▽ (Prod.snd : _ → β) = id := rfl +@[simp] theorem snd_prod_fst : (Prod.snd : _ → β) ▽ (Prod.fst : _ → α) = .swap := rfl -@[simp, grind =] -theorem prod_const_const (a : α) (b : β) : - (Function.const ι a) ▽ (Function.const ι b) = Function.const ι (a, b) := 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 prod_comp_prod (h : α × β → γ) (k : α × β → δ) : + (h ▽ k) ∘ (f ▽ g) = (h ∘ (f ▽ g)) ▽ (k ∘ (f ▽ g)) := rfl -theorem const_prod {ι} {α β} {p : α × β} : - Function.const ι p = (Function.const ι p.1) ▽ (Function.const ι p.2) := rfl +theorem comp_prod_comp (h : α → γ) (k : β → δ) : + (h ∘ f) ▽ (k ∘ g) = (h ∘ Prod.fst) ▽ (k ∘ Prod.snd) ∘ f ▽ g := 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 map_comp_prod (h : α → γ) (k : β → δ) : + Prod.map h k ∘ f ▽ g = (h ∘ f) ▽ (k ∘ g) := rfl -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₂⟩ +@[simp] theorem swap_comp_prod : Prod.swap ∘ (f ▽ g) = g ▽ f := rfl end /-- The diagonal map into `Prod`. -/ -protected def diag : α → α × α := id ▽ id +@[inline] def diag {α} : α → α × α := id ▽ id -@[inherit_doc] prefix:max "⟋" => Function.diag +@[inherit_doc] prefix:max "⟋" => diag section -variable {a b : α} +variable {α β γ} (f : α → β) (g : α → γ) (a b : α) -@[grind =] theorem diag_apply : ⟋a = (a, a) := rfl +@[simp, grind =] theorem diag_apply : ⟋a = (a, a) := rfl -@[simp] theorem fst_diag : (⟋a).1 = a := rfl -@[simp] theorem snd_diag : (⟋a).2 = a := rfl +@[simp] theorem id_prod_id : id ▽ id = diag (α := α) := rfl +@[simp] theorem fstComp_diag : fstComp (diag (α := α)) = id := rfl +@[simp] theorem sndComp_diag : fstComp (diag (α := α)) = id := rfl -theorem map_diag {f : α → β} {g : α → γ} : Prod.map f g ⟋a = (f ▽ g) a := rfl +@[simp] theorem diag_comp : diag ∘ f = f ▽ f := rfl -@[simp] theorem map_comp_diag {f : α → β} {g : α → γ} : - Prod.map f g ∘ Function.diag = f ▽ g := rfl +@[simp] theorem map_comp_diag : Prod.map f g ∘ diag = f ▽ g := rfl -theorem injective_diag : Function.Injective (α := α) Function.diag := fun _ _ => congrArg Prod.fst +theorem injective_diag : Injective (α := α) 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 [Prod.ext_iff] -@[simp] theorem diag_prod_diag : Function.diag ▽ Function.diag (α := α) = - Function.diag ∘ Function.diag := rfl +@[simp] theorem swap_comp_diag : Prod.swap ∘ diag = diag (α := α) := rfl end -/-- `Function.prodMap` is `Prod.map` in the `Function` namespace. -/ -def prodMap (f : α → β) (g : γ → δ) := (f ∘ Prod.fst) ▽ (g ∘ Prod.snd) +/-- `prodMap` is `Prod.map` in the `Function` namespace. -/ +@[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, grind =] -theorem prodMap_eq_prod_map {f : α → β} {g : γ → δ} : f.prodMap g = Prod.map f g := rfl +theorem prodMap_eq_prod_map : f.prodMap g = Prod.map f g := rfl end From 71986cfd3126e1601b0ea20c181e3dd1e45cbfec Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Tue, 21 Apr 2026 11:11:46 +0100 Subject: [PATCH 13/23] Review pass on Function.prod API - Fix sndComp_apply and sndComp_diag copy-paste bugs (rfl proved trivial restatements of the fstComp versions) - Fix typo in prod docstring; rewrite file-level docstring - Drop redundant prod_dcomp_prod and prod_comp_prod (trivial specializations of prod_dcomp / prod_comp) - Add id_dcomp, dcomp_id, dcomp_assoc - Add const_dcomp, dcomp_const - Add prodMap_id - Tighten prodMap docstring --- Mathlib/Logic/Function/Init.lean | 57 +++++++++++++++++++++----------- 1 file changed, 38 insertions(+), 19 deletions(-) diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index 42332a62c0f8a8..6bb9b2cf76bcf6 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -6,19 +6,27 @@ Authors: Wrenna Robson module public import Mathlib.Init +public import Batteries.Tactic.Alias /-! +# Dependent composition, pairing, and diagonal for functions -This file defines `(f ▽ g)`, the operation that pairs two functions `f : ι → α` and -`g : ι → β` into a function `ι → α × β`. +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. -It also defines the special case when `f = g = id`, `diag`. This is the canonical injection -of a type into its prouduct with itself onto its diagonal. +## 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` (notation `⟋`): the diagonal `a ↦ (a, a)`, i.e. `id ▽ id`. +* `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 (except for notation), so that it can be -upstreamed to Batteries or the Lean standard library easily. - +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 @@ -45,10 +53,22 @@ 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) x = (f i, g i)`, where the types of `f i` and `g i` -depend on `i`. -/ +/-- 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 := ⟨f i, g i⟩ @@ -69,7 +89,7 @@ variable {ι κ} {α β : ι → Type*} (f f' : ∀ i, α i) (g g' : ∀ i, β i @[simp, grind =] theorem prod_apply : (f ▽ g) i = (f i, g i) := rfl @[simp, grind =] theorem fstComp_apply : fstComp h i = (h i).1 := rfl -@[simp, grind =] theorem sndComp_apply : fstComp h i = (h i).1 := rfl +@[simp, grind =] theorem sndComp_apply : sndComp h i = (h i).2 := rfl theorem prod_def : f ▽ g = fun i => (f i, g i) := rfl @@ -107,10 +127,6 @@ theorem eq_prod_iff : h = f ▽ g ↔ fstComp h = f ∧ sndComp h = g := by grin theorem prod_dcomp (h : κ → ι) : (f ▽ g) ∘' h = (f ∘' h) ▽ (g ∘' h) := rfl -theorem prod_dcomp_prod {γ δ : ∀ {i : ι}, α i × β i → Type*} - (h : {i : ι} → (ab : α i × β i) → γ ab) (k : {i : ι} → (ab : α i × β i) → δ ab) : - (h ▽ k) ∘' (f ▽ g) = (h ∘' (f ▽ g)) ▽ (k ∘' (f ▽ g)) := 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 @@ -156,9 +172,6 @@ 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 prod_comp_prod (h : α × β → γ) (k : α × β → δ) : - (h ▽ k) ∘ (f ▽ g) = (h ∘ (f ▽ g)) ▽ (k ∘ (f ▽ g)) := rfl - theorem comp_prod_comp (h : α → γ) (k : β → δ) : (h ∘ f) ▽ (k ∘ g) = (h ∘ Prod.fst) ▽ (k ∘ Prod.snd) ∘ f ▽ g := rfl @@ -182,7 +195,7 @@ variable {α β γ} (f : α → β) (g : α → γ) (a b : α) @[simp] theorem id_prod_id : id ▽ id = diag (α := α) := rfl @[simp] theorem fstComp_diag : fstComp (diag (α := α)) = id := rfl -@[simp] theorem sndComp_diag : fstComp (diag (α := α)) = id := rfl +@[simp] theorem sndComp_diag : sndComp (diag (α := α)) = id := rfl @[simp] theorem diag_comp : diag ∘ f = f ▽ f := rfl @@ -197,7 +210,8 @@ theorem exists_diag_apply_iff (p : α × α) : (∃ a, ⟋a = p) ↔ p.1 = p.2 : end -/-- `prodMap` is `Prod.map` in the `Function` namespace. -/ +/-- 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) @@ -210,9 +224,14 @@ 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 + +@[deprecated (since := "2026-04-21")] +alias Pi.prod := Function.prod From 4bd1e2ec7dfa1f069430e7ca7aff6e88961a9d76 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Tue, 21 Apr 2026 15:17:44 +0100 Subject: [PATCH 14/23] Fix downstream callers of Pi.prod and add sndComp/fstComp mk lemmas --- Archive/Sensitivity.lean | 2 +- Mathlib/Algebra/Algebra/NonUnitalHom.lean | 14 ++++++------- Mathlib/Algebra/Algebra/Prod.lean | 4 ++-- Mathlib/Algebra/Exact.lean | 2 +- Mathlib/Algebra/Group/Prod.lean | 8 ++++---- Mathlib/Algebra/Lie/Prod.lean | 2 +- Mathlib/Algebra/Star/StarAlgHom.lean | 12 +++++------ Mathlib/Data/Fin/Tuple/Curry.lean | 1 + .../LinearAlgebra/AffineSpace/AffineMap.lean | 4 ++-- .../LinearAlgebra/Dimension/DivisionRing.lean | 2 +- Mathlib/LinearAlgebra/Goursat.lean | 12 +++++------ Mathlib/LinearAlgebra/Prod.lean | 10 +++++----- Mathlib/LinearAlgebra/QuadraticForm/Dual.lean | 2 +- Mathlib/Logic/Function/Init.lean | 20 +++++++++++++++---- .../Topology/Algebra/ContinuousAffineMap.lean | 2 +- Mathlib/Topology/Inseparable.lean | 2 +- .../LocallyUniformConvergence.lean | 4 ++-- 17 files changed, 58 insertions(+), 45 deletions(-) diff --git a/Archive/Sensitivity.lean b/Archive/Sensitivity.lean index a7fddf3e39c46c..59bb9f05b469ba 100644 --- a/Archive/Sensitivity.lean +++ b/Archive/Sensitivity.lean @@ -329,7 +329,7 @@ set_option backward.isDefEq.respectTransparency false in theorem g_injective : Injective (g m) := by rw [g] intro x₁ x₂ h - simp only [V, LinearMap.prod_apply, LinearMap.id_apply, Prod.mk_inj, Pi.prod] at h + simp only [V, LinearMap.prod_apply, LinearMap.id_apply, Prod.mk_inj, Function.prod_apply] at h exact h.right set_option backward.isDefEq.respectTransparency false in diff --git a/Mathlib/Algebra/Algebra/NonUnitalHom.lean b/Mathlib/Algebra/Algebra/NonUnitalHom.lean index d3986be73bd13b..43df13949bd3fe 100644 --- a/Mathlib/Algebra/Algebra/NonUnitalHom.lean +++ b/Mathlib/Algebra/Algebra/NonUnitalHom.lean @@ -371,13 +371,13 @@ 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_apply, Prod.mk_zero_zero, map_zero] + map_add' x y := by simp only [Function.prod_apply, Prod.mk_add_mk, map_add] + map_mul' x y := by simp only [Function.prod_apply, Prod.mk_mul_mk, map_mul] + map_smul' c x := by simp only [Function.prod_apply, 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 := +theorem coe_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : ⇑(f.prod g) = Function.prod f g := rfl @[simp] @@ -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 Pi.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. -/ diff --git a/Mathlib/Algebra/Algebra/Prod.lean b/Mathlib/Algebra/Algebra/Prod.lean index 46058dff5af82d..66cd3bf80c06aa 100644 --- a/Mathlib/Algebra/Algebra/Prod.lean +++ b/Mathlib/Algebra/Algebra/Prod.lean @@ -77,7 +77,7 @@ 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 @@ -85,7 +85,7 @@ def prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : A →ₐ[R] B × C := 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] diff --git a/Mathlib/Algebra/Exact.lean b/Mathlib/Algebra/Exact.lean index 93d70ae8228689..b54d95f0300371 100644 --- a/Mathlib/Algebra/Exact.lean +++ b/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 [LinearMap.prod_apply, Pi.prod, Prod.mk.injEq] at e + simp only [LinearMap.prod_apply, Function.prod_apply, Prod.mk.injEq] at e obtain ⟨z, hz⟩ := (h (x - y)).mp (by simpa [sub_eq_zero] using e.2) rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero] · rintro ⟨x, y⟩ diff --git a/Mathlib/Algebra/Group/Prod.lean b/Mathlib/Algebra/Group/Prod.lean index 7b6de8812c6ba1..2b516ede3c9d4d 100644 --- a/Mathlib/Algebra/Group/Prod.lean +++ b/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] diff --git a/Mathlib/Algebra/Lie/Prod.lean b/Mathlib/Algebra/Lie/Prod.lean index 21936d6d5d5dc3..48e9844cd6766e 100644 --- a/Mathlib/Algebra/Lie/Prod.lean +++ b/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] diff --git a/Mathlib/Algebra/Star/StarAlgHom.lean b/Mathlib/Algebra/Star/StarAlgHom.lean index e2aaf7149ee76b..c7f063eda91b4c 100644 --- a/Mathlib/Algebra/Star/StarAlgHom.lean +++ b/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.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] @@ -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.fst_prod_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] } -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.fst_prod_snd /-- Taking the product of two maps with the same domain is equivalent to taking the product of their codomains. -/ diff --git a/Mathlib/Data/Fin/Tuple/Curry.lean b/Mathlib/Data/Fin/Tuple/Curry.lean index be43addbaa66ed..53c2e14a7129db 100644 --- a/Mathlib/Data/Fin/Tuple/Curry.lean +++ b/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 /-! diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean index bb6718dfd542da..63be48109f2d6d 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean @@ -451,11 +451,11 @@ theorem image_vsub_image {s t : Set P1} (f : P1 →ᵃ[k] P2) : /-- The product of two affine maps is an affine map. -/ @[simps linear] def prod (f : P1 →ᵃ[k] P2) (g : P1 →ᵃ[k] P3) : P1 →ᵃ[k] P2 × P3 where - toFun := Pi.prod f g + toFun := Function.prod f g linear := f.linear.prod g.linear map_vadd' := by simp -theorem coe_prod (f : P1 →ᵃ[k] P2) (g : P1 →ᵃ[k] P3) : prod f g = Pi.prod f g := +theorem coe_prod (f : P1 →ᵃ[k] P2) (g : P1 →ᵃ[k] P3) : prod f g = Function.prod f g := rfl @[simp] diff --git a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean index 5d895922609122..6d04acb4101982 100644 --- a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean +++ b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean @@ -97,7 +97,7 @@ theorem rank_add_rank_split (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd rintro ⟨d, e⟩ have h := eq₂ d (-e) simp only [add_eq_zero_iff_eq_neg, LinearMap.prod_apply, mem_ker, - Prod.mk_inj, coprod_apply, map_neg, neg_apply, LinearMap.mem_range, Pi.prod] at h ⊢ + Prod.mk_inj, coprod_apply, map_neg, neg_apply, LinearMap.mem_range] at h ⊢ grind end diff --git a/Mathlib/LinearAlgebra/Goursat.lean b/Mathlib/LinearAlgebra/Goursat.lean index 56378065f5a1a0..b39c302ba97412 100644 --- a/Mathlib/LinearAlgebra/Goursat.lean +++ b/Mathlib/LinearAlgebra/Goursat.lean @@ -123,13 +123,13 @@ lemma goursat : ∃ (M' : Submodule R M) (N' : Submodule R N) (M'' : Submodule R rw [comap_map_eq_self] · ext ⟨m, n⟩ constructor - · 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] + · simp only [mem_map, LinearMap.mem_range, LinearMap.prod_apply, Function.prod_apply, + Subtype.exists, Prod.exists, LinearMap.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] + · simp only [mem_map, LinearMap.mem_range, LinearMap.prod_apply, Function.prod_apply, + Subtype.exists, Prod.exists, LinearMap.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) simp only [ker_prodMap, ker_mkQ, Submodule.ext_iff] diff --git a/Mathlib/LinearAlgebra/Prod.lean b/Mathlib/LinearAlgebra/Prod.lean index 6416808409864e..21f532a1db5fc0 100644 --- a/Mathlib/LinearAlgebra/Prod.lean +++ b/Mathlib/LinearAlgebra/Prod.lean @@ -93,11 +93,11 @@ theorem snd_surjective : Function.Surjective (snd R M M₂) := fun x => ⟨(0, x /-- The prod of two linear maps is a linear map. -/ @[simps] def prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : M →ₗ[R] M₂ × M₃ where - toFun := Pi.prod f g - map_add' x y := by simp only [Pi.prod, Prod.mk_add_mk, map_add] - map_smul' c x := by simp only [Pi.prod, Prod.smul_mk, map_smul, RingHom.id_apply] + toFun := Function.prod f g + map_add' x y := by simp only [Function.prod_apply, Prod.mk_add_mk, map_add] + map_smul' c x := by simp only [Function.prod_apply, Prod.smul_mk, map_smul, RingHom.id_apply] -theorem coe_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : ⇑(f.prod g) = Pi.prod f g := +theorem coe_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : ⇑(f.prod g) = Function.prod f g := rfl @[simp] @@ -850,7 +850,7 @@ theorem range_prod_eq {f : M →ₗ[R] M₂} {g : M →ₗ[R] M₃} (h : ker f range (prod f g) = (range f).prod (range g) := by refine le_antisymm (f.range_prod_le g) ?_ simp only [SetLike.le_def, prod_apply, mem_range, mem_prod, exists_imp, and_imp, - Prod.forall, Pi.prod] + Prod.forall, Function.prod_apply] rintro _ _ x rfl y rfl -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify `(f := f)` simp only [Prod.mk_inj, ← sub_mem_ker_iff (f := f)] diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean b/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean index e607498ea392aa..f4f8519a9af008 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean @@ -140,7 +140,7 @@ def toDualProd (Q : QuadraticForm R M) [Invertible (2 : R)] : map_app' x := by dsimp only [associated, associatedHom] dsimp only [LinearMap.smul_apply, LinearMap.coe_mk, AddHom.coe_mk, AddHom.toFun_eq_coe, - LinearMap.coe_toAddHom, LinearMap.prod_apply, Pi.prod, LinearMap.add_apply, + LinearMap.coe_toAddHom, LinearMap.prod_apply, Function.prod_apply, LinearMap.add_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.fst_apply, LinearMap.snd_apply, LinearMap.sub_apply, dualProd_apply, polarBilin_apply_apply, prod_apply, neg_apply] simp only [polar_sub_right, polar_self, nsmul_eq_mul, Nat.cast_ofNat, polar_comm _ x.1 x.2, diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index 6bb9b2cf76bcf6..08a05b7fda71d7 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -93,8 +93,8 @@ variable {ι κ} {α β : ι → Type*} (f f' : ∀ i, α i) (g g' : ∀ i, β i theorem prod_def : f ▽ g = fun i => (f i, g i) := rfl -@[simp] theorem fst_dcomp : Prod.fst ∘' h = fstComp h := rfl -@[simp] theorem snd_dcomp : Prod.snd ∘' h = sndComp h := rfl +theorem fst_dcomp : Prod.fst ∘' h = fstComp h := rfl +theorem snd_dcomp : Prod.snd ∘' h = sndComp h := rfl @[simp, grind! .] theorem fstComp_prod {f : ∀ i, α i} {g : ∀ i, β i} : fstComp (f ▽ g) = f := rfl @@ -160,8 +160,14 @@ section variable {α β γ δ : Type*} {ι κ : Sort*} (f : ι → α) (g : ι → β) (a : α) (b : β) (p : α × β) -@[simp] theorem fst_comp (h : ι → α × β) : Prod.fst ∘ h = fstComp h := rfl -@[simp] theorem snd_comp (h : ι → α × β) : Prod.snd ∘ h = sndComp h := rfl +theorem fst_comp (h : ι → α × β) : Prod.fst ∘ h = fstComp h := rfl +theorem snd_comp (h : ι → α × β) : Prod.snd ∘ h = sndComp h := rfl + +@[simp] theorem fstComp_mk : fstComp (Prod.mk a : β → α × β) = const β a := rfl +@[simp] theorem sndComp_mk : sndComp (Prod.mk a : β → α × β) = id := rfl + +@[simp] theorem fstComp_mk_flip : fstComp ((Prod.mk · b) : α → α × β) = id := rfl +@[simp] theorem sndComp_mk_flip : sndComp ((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 @@ -235,3 +241,9 @@ end Function @[deprecated (since := "2026-04-21")] alias Pi.prod := Function.prod + +@[deprecated (since := "2026-04-21")] +alias Pi.prod_fst_snd := Function.fst_prod_snd + +@[deprecated (since := "2026-04-21")] +alias Pi.prod_snd_fst := Function.snd_prod_fst diff --git a/Mathlib/Topology/Algebra/ContinuousAffineMap.lean b/Mathlib/Topology/Algebra/ContinuousAffineMap.lean index 8d123a766054d6..901f4bf7b59131 100644 --- a/Mathlib/Topology/Algebra/ContinuousAffineMap.lean +++ b/Mathlib/Topology/Algebra/ContinuousAffineMap.lean @@ -400,7 +400,7 @@ def prod (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃) : P₁ →ᴬ[k] P __ := AffineMap.prod f g cont := by eta_expand; dsimp; fun_prop -theorem coe_prod (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃) : prod f g = Pi.prod f g := +theorem coe_prod (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃) : prod f g = Function.prod f g := rfl @[simp] diff --git a/Mathlib/Topology/Inseparable.lean b/Mathlib/Topology/Inseparable.lean index 49536ae6c422c5..9a646d95222a04 100644 --- a/Mathlib/Topology/Inseparable.lean +++ b/Mathlib/Topology/Inseparable.lean @@ -483,7 +483,7 @@ theorem subtype_inseparable_iff {p : X → Prop} (x y : Subtype p) : (x ~ᵢ y) @[simp] theorem inseparable_prod {x₁ x₂ : X} {y₁ y₂ : Y} : ((x₁, y₁) ~ᵢ (x₂, y₂)) ↔ (x₁ ~ᵢ x₂) ∧ (y₁ ~ᵢ y₂) := by - simp only [Inseparable, nhds_prod_eq, prod_inj] + simp only [Inseparable, nhds_prod_eq, Filter.prod_inj] theorem Inseparable.prod {x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₁ ~ᵢ x₂) (hy : y₁ ~ᵢ y₂) : (x₁, y₁) ~ᵢ (x₂, y₂) := diff --git a/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean b/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean index 2170661fd474fb..c86814c50bb786 100644 --- a/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean +++ b/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean @@ -208,7 +208,7 @@ theorem TendstoLocallyUniformlyOn.prodMk [UniformSpace γ] {G : ι → α → γ theorem TendstoLocallyUniformlyOn.piProd [UniformSpace γ] {G : ι → α → γ} {g : α → γ} (hF : TendstoLocallyUniformlyOn F f p s) (hG : TendstoLocallyUniformlyOn G g p s) : - TendstoLocallyUniformlyOn (fun n ↦ Pi.prod (F n) (G n)) (Pi.prod f g) p s := + TendstoLocallyUniformlyOn (fun n ↦ Function.prod (F n) (G n)) (Function.prod f g) p s := hF.prodMk hG theorem TendstoLocallyUniformly.prodMk [UniformSpace γ] {G : ι → α → γ} {g : α → γ} @@ -219,7 +219,7 @@ theorem TendstoLocallyUniformly.prodMk [UniformSpace γ] {G : ι → α → γ} theorem TendstoLocallyUniformly.piProd [UniformSpace γ] {G : ι → α → γ} {g : α → γ} (hF : TendstoLocallyUniformly F f p) (hG : TendstoLocallyUniformly G g p) : - TendstoLocallyUniformly (fun n ↦ Pi.prod (F n) (G n)) (Pi.prod f g) p := + TendstoLocallyUniformly (fun n ↦ Function.prod (F n) (G n)) (Function.prod f g) p := hF.prodMk hG /-- If every `x ∈ s` has a neighbourhood within `s` on which `F i` tends uniformly to `f`, then From 452fe9373e6e2fd133c3953c23e1632934f5df78 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Tue, 21 Apr 2026 16:30:50 +0100 Subject: [PATCH 15/23] Restore Function.prod_apply in DivisionRing simp call --- Mathlib/LinearAlgebra/Dimension/DivisionRing.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean index 6d04acb4101982..6d801fae448f57 100644 --- a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean +++ b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean @@ -97,7 +97,8 @@ theorem rank_add_rank_split (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd rintro ⟨d, e⟩ have h := eq₂ d (-e) simp only [add_eq_zero_iff_eq_neg, LinearMap.prod_apply, mem_ker, - Prod.mk_inj, coprod_apply, map_neg, neg_apply, LinearMap.mem_range] at h ⊢ + Prod.mk_inj, coprod_apply, map_neg, neg_apply, LinearMap.mem_range, + Function.prod_apply] at h ⊢ grind end From 0830cd67d1dea9beb6a307f3b506a740b40099eb Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Tue, 21 Apr 2026 16:42:27 +0100 Subject: [PATCH 16/23] Change to adapt --- Mathlib/Logic/Function/Init.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index 08a05b7fda71d7..ceafdbfb260889 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -6,7 +6,7 @@ Authors: Wrenna Robson module public import Mathlib.Init -public import Batteries.Tactic.Alias +import Batteries.Tactic.Alias /-! # Dependent composition, pairing, and diagonal for functions @@ -37,7 +37,7 @@ namespace Function /-- 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] def dcomp {ι} {β : ι → Sort*} {φ : ∀ {i : ι}, β i → Sort*} +@[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 @@ -47,7 +47,7 @@ section variable {ι} {β : ι → Sort*} {φ : ∀ {i : ι}, β i → Sort*} (f : ∀ {i : ι} (y : β i), φ y) (g : ∀ i, β i) (i : ι) -@[simp] theorem dcomp_apply : dcomp f g i = f (g i) := rfl +theorem dcomp_apply : dcomp f g i = f (g i) := rfl theorem dcomp_def : f ∘' g = fun i => f (g i) := rfl From a48541777c0bf3f9d1367c628fe6fa6fc68f5e7b Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Wed, 22 Apr 2026 11:39:01 +0100 Subject: [PATCH 17/23] Try to fix large import --- Mathlib/Algebra/Notation/Pi/Defs.lean | 10 ++++++++++ Mathlib/Logic/Function/Init.lean | 10 ---------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Mathlib/Algebra/Notation/Pi/Defs.lean b/Mathlib/Algebra/Notation/Pi/Defs.lean index 56b421196ac5aa..d401581f5bcf35 100644 --- a/Mathlib/Algebra/Notation/Pi/Defs.lean +++ b/Mathlib/Algebra/Notation/Pi/Defs.lean @@ -8,6 +8,7 @@ module public import Mathlib.Algebra.Notation.Defs public import Mathlib.Tactic.Push.Attr public import Mathlib.Logic.Function.Init +public import Batteries.Tactic.Alias /-! # Notation for algebraic operators on pi types @@ -27,6 +28,15 @@ variable {ι α β : Type*} {G M R : ι → Type*} namespace Pi +@[deprecated (since := "2026-04-21")] +alias prod := Function.prod + +@[deprecated (since := "2026-04-21")] +alias prod_fst_snd := Function.fst_prod_snd + +@[deprecated (since := "2026-04-21")] +alias prod_snd_fst := Function.snd_prod_fst + /-! `1`, `0`, `+`, `*`, `+ᵥ`, `•`, `^`, `-`, `⁻¹`, and `/` are defined pointwise. -/ section One diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index ceafdbfb260889..72b860bf98d036 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -6,7 +6,6 @@ Authors: Wrenna Robson module public import Mathlib.Init -import Batteries.Tactic.Alias /-! # Dependent composition, pairing, and diagonal for functions @@ -238,12 +237,3 @@ theorem prodMap_eq_prod_map : f.prodMap g = Prod.map f g := rfl end end Function - -@[deprecated (since := "2026-04-21")] -alias Pi.prod := Function.prod - -@[deprecated (since := "2026-04-21")] -alias Pi.prod_fst_snd := Function.fst_prod_snd - -@[deprecated (since := "2026-04-21")] -alias Pi.prod_snd_fst := Function.snd_prod_fst From 3da5cd3a4ccc5f3741bead5aba9b07b833bbf907 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Wed, 22 Apr 2026 12:53:43 +0100 Subject: [PATCH 18/23] Change notation --- Mathlib/Logic/Function/Init.lean | 86 +++++++++++++++++--------------- 1 file changed, 46 insertions(+), 40 deletions(-) diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index 72b860bf98d036..6677ecd52b4d9b 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -16,14 +16,20 @@ 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 +* `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` (notation `⟋`): the diagonal `a ↦ (a, a)`, i.e. `id ▽ id`. +* `Function.diag` (notation `△`): the diagonal `a ↦ (a, a)`, i.e. `id ⋏ id`. * `Function.prodMap`: `Prod.map` re-exposed under `Function` so that `f.prodMap g` works via dot notation. +## Notation + +The infix `⋏` for `Function.prod` mirrors `∧`: pairing is the propositions-as-types conjunction +(`f ⋏ g` reads as "both `f` and `g`"). The prefix `△` for `Function.diag` depicts the fan-out +shape of `a ↦ (a, a)`: apex-up for one-to-two. + 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. -/ @@ -66,10 +72,10 @@ theorem dcomp_assoc {κ : Sort*} (h : κ → ι) : f ∘' g ∘' h = (f ∘' g) end -/-- Product of functions: `(f ▽ g) i = (f i, g i)`, where the types of `f i` and `g i` +/-- 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 := ⟨f i, g i⟩ +@[inline] def prod {ι} {α β : ι → Type*} (f : ∀ i, α i) (g : ∀ i, β i) : + (i : ι) → α i × β i := fun i => Prod.mk (f i) (g i) /-- The first component of a map into a product. -/ @[inline] def fstComp {ι} {α β : ι → Type*} (h : (i : ι) → α i × β i) (i : ι) : @@ -79,28 +85,28 @@ may depend on `i`. -/ @[inline] def sndComp {ι} {α β : ι → Type*} (h : (i : ι) → α i × β i) (i : ι) : β i := (h i).2 -@[inherit_doc] infixr:95 " ▽ " => prod +@[inherit_doc] infixr:95 " ⋏ " => prod 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 prod_apply : (f ⋏ g) i = (f i, g i) := rfl @[simp, grind =] theorem fstComp_apply : fstComp h i = (h i).1 := rfl @[simp, grind =] theorem sndComp_apply : sndComp h i = (h i).2 := rfl -theorem prod_def : f ▽ g = fun i => (f i, g i) := rfl +theorem prod_def : f ⋏ g = fun i => (f i, g i) := rfl theorem fst_dcomp : Prod.fst ∘' h = fstComp h := rfl theorem snd_dcomp : Prod.snd ∘' h = sndComp h := rfl @[simp, grind! .] theorem fstComp_prod {f : ∀ i, α i} {g : ∀ i, β i} : - fstComp (f ▽ g) = f := rfl + fstComp (f ⋏ g) = f := rfl @[simp, grind! .] theorem sndComp_prod {f : ∀ i, α i} {g : ∀ i, β i} : - sndComp (f ▽ g) = g := rfl + sndComp (f ⋏ g) = g := rfl @[simp, grind! .] theorem fstComp_prod_sndComp {h : ∀ i, α i × β i} : - fstComp h ▽ sndComp h = h := rfl + fstComp h ⋏ sndComp h = h := rfl theorem fstComp_sndComp_ext {h h' : ∀ i, α i × β i} (H₁ : fstComp h = fstComp h') (H₂ : sndComp h = sndComp h') : h = h' := by grind @@ -108,29 +114,29 @@ theorem fstComp_sndComp_ext {h h' : ∀ i, α i × β i} (H₁ : fstComp h = fst theorem fstComp_sndComp_ext_iff {h h' : ∀ i, α i × β i} : h = h' ↔ fstComp h = fstComp h' ∧ sndComp h = sndComp 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 +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 + f ⋏ g = f' ⋏ g' ↔ f = f' ∧ g = g' := by grind -theorem exists_pair_prod : ∃ f g, f ▽ g = h := +theorem exists_pair_prod : ∃ f g, f ⋏ g = h := ⟨fstComp h, sndComp h, fstComp_prod_sndComp⟩ theorem exists_fstComp [Nonempty (∀ i, β i)] : ∃ h : ∀ i, α i × β i, fstComp h = f := - ⟨f ▽ Classical.ofNonempty, fstComp_prod⟩ + ⟨f ⋏ Classical.ofNonempty, fstComp_prod⟩ theorem exists_sndComp [Nonempty (∀ i, α i)] : ∃ h : ∀ i, α i × β i, sndComp h = g := - ⟨Classical.ofNonempty ▽ g, sndComp_prod⟩ + ⟨Classical.ofNonempty ⋏ g, sndComp_prod⟩ -theorem prod_eq_iff : f ▽ g = h ↔ f = fstComp h ∧ g = sndComp h := by grind -theorem eq_prod_iff : h = f ▽ g ↔ fstComp h = f ∧ sndComp h = g := by grind +theorem prod_eq_iff : f ⋏ g = h ↔ f = fstComp h ∧ g = sndComp h := by grind +theorem eq_prod_iff : h = f ⋏ g ↔ fstComp h = f ∧ sndComp h = g := by grind -theorem prod_dcomp (h : κ → ι) : (f ▽ g) ∘' h = (f ∘' h) ▽ (g ∘' h) := rfl +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 + (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 +@[simp] theorem swap_dcomp_prod : Prod.swap ∘' (f ⋏ g) = g ⋏ f := rfl end @@ -139,11 +145,11 @@ section variable {ι : Type*} {α β : ι → Type*} theorem leftInverse_uncurry_prod_fstComp_prod_sndComp : - LeftInverse prod.uncurry (fstComp (α := α) ▽ sndComp (β := β)) := by + LeftInverse prod.uncurry (fstComp (α := α) ⋏ sndComp (β := β)) := by simp [LeftInverse] theorem rightInverse_uncurry_prod_fstComp_prod_sndComp : - RightInverse prod.uncurry (fstComp (α := α) ▽ sndComp (β := β)) := by + RightInverse prod.uncurry (fstComp (α := α) ⋏ sndComp (β := β)) := by simp [RightInverse, LeftInverse] theorem uncurry_prod_injective : (prod (α := α) (β := β)).uncurry.Injective := @@ -168,47 +174,47 @@ theorem snd_comp (h : ι → α × β) : Prod.snd ∘ h = sndComp h := rfl @[simp] theorem fstComp_mk_flip : fstComp ((Prod.mk · b) : α → α × β) = id := rfl @[simp] theorem sndComp_mk_flip : sndComp ((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 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 +@[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 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 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 + (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 + Prod.map h k ∘ f ⋏ g = (h ∘ f) ⋏ (k ∘ g) := rfl -@[simp] theorem swap_comp_prod : Prod.swap ∘ (f ▽ g) = g ▽ f := rfl +@[simp] theorem swap_comp_prod : Prod.swap ∘ (f ⋏ g) = g ⋏ f := rfl end /-- The diagonal map into `Prod`. -/ -@[inline] def diag {α} : α → α × α := id ▽ id +@[inline] def diag {α} : α → α × α := id ⋏ id -@[inherit_doc] prefix:max "⟋" => diag +@[inherit_doc] prefix:max "△" => diag section variable {α β γ} (f : α → β) (g : α → γ) (a b : α) -@[simp, grind =] theorem diag_apply : ⟋a = (a, a) := rfl +@[simp, grind =] theorem diag_apply : △a = (a, a) := rfl -@[simp] theorem id_prod_id : id ▽ id = diag (α := α) := rfl +@[simp] theorem id_prod_id : id ⋏ id = diag (α := α) := rfl @[simp] theorem fstComp_diag : fstComp (diag (α := α)) = id := rfl @[simp] theorem sndComp_diag : sndComp (diag (α := α)) = id := rfl -@[simp] theorem diag_comp : diag ∘ f = f ▽ f := rfl +@[simp] theorem diag_comp : diag ∘ f = f ⋏ f := rfl -@[simp] theorem map_comp_diag : Prod.map f g ∘ diag = f ▽ g := rfl +@[simp] theorem map_comp_diag : Prod.map f g ∘ diag = f ⋏ g := rfl theorem injective_diag : Injective (α := α) diag := fun _ _ => congrArg Prod.fst -theorem exists_diag_apply_iff (p : α × α) : (∃ a, ⟋a = p) ↔ p.1 = p.2 := by +theorem exists_diag_apply_iff (p : α × α) : (∃ a, △a = p) ↔ p.1 = p.2 := by simp [Prod.ext_iff] @[simp] theorem swap_comp_diag : Prod.swap ∘ diag = diag (α := α) := rfl @@ -218,7 +224,7 @@ 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) + (f ∘ Prod.fst) ⋏ (g ∘ Prod.snd) section From aa35b23ccc813f13a518aef88bffc19453c5fc2a Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Sat, 4 Apr 2026 16:15:37 +0100 Subject: [PATCH 19/23] Execute rename --- Archive/Sensitivity.lean | 2 +- Mathlib/Algebra/Algebra/NonUnitalHom.lean | 14 +++++----- Mathlib/Algebra/Algebra/Prod.lean | 4 +-- Mathlib/Algebra/BigOperators/Finprod.lean | 2 +- Mathlib/Algebra/Exact.lean | 2 +- Mathlib/Algebra/Group/Prod.lean | 8 +++--- Mathlib/Algebra/Lie/Prod.lean | 2 +- Mathlib/Algebra/MvPolynomial/Equiv.lean | 2 +- Mathlib/Algebra/MvPolynomial/Eval.lean | 2 +- Mathlib/Algebra/Notation/Pi/Defs.lean | 15 ++++++----- Mathlib/Algebra/Star/StarAlgHom.lean | 14 +++++----- Mathlib/Combinatorics/Nullstellensatz.lean | 4 +-- .../LinearAlgebra/AffineSpace/AffineMap.lean | 4 +-- .../LinearAlgebra/Dimension/DivisionRing.lean | 3 ++- Mathlib/LinearAlgebra/Goursat.lean | 26 ++++++++----------- Mathlib/LinearAlgebra/Prod.lean | 10 +++---- Mathlib/LinearAlgebra/QuadraticForm/Dual.lean | 2 +- Mathlib/Logic/Function/Defs.lean | 8 ++++++ Mathlib/MeasureTheory/Integral/Prod.lean | 2 +- Mathlib/MeasureTheory/Measure/Prod.lean | 11 ++++---- Mathlib/NumberTheory/Height/Basic.lean | 2 +- Mathlib/SetTheory/Cardinal/Finite.lean | 2 +- .../Topology/Algebra/ContinuousAffineMap.lean | 2 +- .../Topology/Algebra/InfiniteSum/Basic.lean | 6 ++--- .../Algebra/InfiniteSum/Constructions.lean | 2 +- Mathlib/Topology/Inseparable.lean | 2 +- .../LocallyUniformConvergence.lean | 4 +-- 27 files changed, 83 insertions(+), 74 deletions(-) diff --git a/Archive/Sensitivity.lean b/Archive/Sensitivity.lean index 53a2ef0b6f27e1..b48847812ab9a1 100644 --- a/Archive/Sensitivity.lean +++ b/Archive/Sensitivity.lean @@ -329,7 +329,7 @@ set_option backward.isDefEq.respectTransparency false in theorem g_injective : Injective (g m) := by rw [g] intro x₁ x₂ h - simp only [V, LinearMap.prod_apply, LinearMap.id_apply, Prod.mk_inj, Pi.prod] at h + simp only [V, LinearMap.prod_apply, LinearMap.id_apply, Prod.mk_inj, Function.prod_apply] at h exact h.right set_option backward.isDefEq.respectTransparency false in diff --git a/Mathlib/Algebra/Algebra/NonUnitalHom.lean b/Mathlib/Algebra/Algebra/NonUnitalHom.lean index d3986be73bd13b..43df13949bd3fe 100644 --- a/Mathlib/Algebra/Algebra/NonUnitalHom.lean +++ b/Mathlib/Algebra/Algebra/NonUnitalHom.lean @@ -371,13 +371,13 @@ 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_apply, Prod.mk_zero_zero, map_zero] + map_add' x y := by simp only [Function.prod_apply, Prod.mk_add_mk, map_add] + map_mul' x y := by simp only [Function.prod_apply, Prod.mk_mul_mk, map_mul] + map_smul' c x := by simp only [Function.prod_apply, 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 := +theorem coe_prod (f : A →ₙₐ[R] B) (g : A →ₙₐ[R] C) : ⇑(f.prod g) = Function.prod f g := rfl @[simp] @@ -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 Pi.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. -/ diff --git a/Mathlib/Algebra/Algebra/Prod.lean b/Mathlib/Algebra/Algebra/Prod.lean index 46058dff5af82d..66cd3bf80c06aa 100644 --- a/Mathlib/Algebra/Algebra/Prod.lean +++ b/Mathlib/Algebra/Algebra/Prod.lean @@ -77,7 +77,7 @@ 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 @@ -85,7 +85,7 @@ def prod (f : A →ₐ[R] B) (g : A →ₐ[R] C) : A →ₐ[R] B × C := 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] diff --git a/Mathlib/Algebra/BigOperators/Finprod.lean b/Mathlib/Algebra/BigOperators/Finprod.lean index f18d5152f4b81a..e32dbca7710725 100644 --- a/Mathlib/Algebra/BigOperators/Finprod.lean +++ b/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) diff --git a/Mathlib/Algebra/Exact.lean b/Mathlib/Algebra/Exact.lean index 0a9beae3a2905a..b54d95f0300371 100644 --- a/Mathlib/Algebra/Exact.lean +++ b/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, Function.prod_apply, Prod.mk.injEq] at e obtain ⟨z, hz⟩ := (h (x - y)).mp (by simpa [sub_eq_zero] using e.2) rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero] · rintro ⟨x, y⟩ diff --git a/Mathlib/Algebra/Group/Prod.lean b/Mathlib/Algebra/Group/Prod.lean index 7b6de8812c6ba1..2b516ede3c9d4d 100644 --- a/Mathlib/Algebra/Group/Prod.lean +++ b/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] diff --git a/Mathlib/Algebra/Lie/Prod.lean b/Mathlib/Algebra/Lie/Prod.lean index 21936d6d5d5dc3..48e9844cd6766e 100644 --- a/Mathlib/Algebra/Lie/Prod.lean +++ b/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] diff --git a/Mathlib/Algebra/MvPolynomial/Equiv.lean b/Mathlib/Algebra/MvPolynomial/Equiv.lean index 674bcf626ba5a5..a66ed7724352c9 100644 --- a/Mathlib/Algebra/MvPolynomial/Equiv.lean +++ b/Mathlib/Algebra/MvPolynomial/Equiv.lean @@ -639,7 +639,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, diff --git a/Mathlib/Algebra/MvPolynomial/Eval.lean b/Mathlib/Algebra/MvPolynomial/Eval.lean index 574e7e2fc76f42..0e13948de38b25 100644 --- a/Mathlib/Algebra/MvPolynomial/Eval.lean +++ b/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) : diff --git a/Mathlib/Algebra/Notation/Pi/Defs.lean b/Mathlib/Algebra/Notation/Pi/Defs.lean index 56fb6e87726968..77be7fd2c8ebe0 100644 --- a/Mathlib/Algebra/Notation/Pi/Defs.lean +++ b/Mathlib/Algebra/Notation/Pi/Defs.lean @@ -7,6 +7,8 @@ module public import Mathlib.Algebra.Notation.Defs public import Mathlib.Tactic.Push.Attr +public import Mathlib.Logic.Function.Defs +public import Batteries.Tactic.Alias /-! # Notation for algebraic operators on pi types @@ -26,13 +28,14 @@ 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) +@[deprecated (since := "2026-04-21")] +alias prod := Function.prod + +@[deprecated (since := "2026-04-21")] +alias prod_fst_snd := Function.prod_fst_snd -lemma prod_fst_snd : Pi.prod (Prod.fst : α × β → α) (Prod.snd : α × β → β) = id := rfl -lemma prod_snd_fst : Pi.prod (Prod.snd : α × β → β) (Prod.fst : α × β → α) = .swap := rfl +@[deprecated (since := "2026-04-21")] +alias prod_snd_fst := Function.prod_snd_fst /-! `1`, `0`, `+`, `*`, `+ᵥ`, `•`, `^`, `-`, `⁻¹`, and `/` are defined pointwise. -/ diff --git a/Mathlib/Algebra/Star/StarAlgHom.lean b/Mathlib/Algebra/Star/StarAlgHom.lean index c72de1d2cab968..902276474188f9 100644 --- a/Mathlib/Algebra/Star/StarAlgHom.lean +++ b/Mathlib/Algebra/Star/StarAlgHom.lean @@ -488,13 +488,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] } + 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 := +theorem coe_prod (f : A →⋆ₙₐ[R] B) (g : A →⋆ₙₐ[R] C) : ⇑(f.prod g) = Function.prod f g := rfl @[simp] @@ -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 Pi.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. -/ @@ -593,12 +593,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] } -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] @@ -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 Pi.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. -/ diff --git a/Mathlib/Combinatorics/Nullstellensatz.lean b/Mathlib/Combinatorics/Nullstellensatz.lean index 59fee42216d37d..12ebec3ddbbb7c 100644 --- a/Mathlib/Combinatorics/Nullstellensatz.lean +++ b/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 @@ -228,7 +228,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 diff --git a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean b/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean index bb6718dfd542da..63be48109f2d6d 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean @@ -451,11 +451,11 @@ theorem image_vsub_image {s t : Set P1} (f : P1 →ᵃ[k] P2) : /-- The product of two affine maps is an affine map. -/ @[simps linear] def prod (f : P1 →ᵃ[k] P2) (g : P1 →ᵃ[k] P3) : P1 →ᵃ[k] P2 × P3 where - toFun := Pi.prod f g + toFun := Function.prod f g linear := f.linear.prod g.linear map_vadd' := by simp -theorem coe_prod (f : P1 →ᵃ[k] P2) (g : P1 →ᵃ[k] P3) : prod f g = Pi.prod f g := +theorem coe_prod (f : P1 →ᵃ[k] P2) (g : P1 →ᵃ[k] P3) : prod f g = Function.prod f g := rfl @[simp] diff --git a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean index b37b76bb2f9da7..b01b9a20735fb0 100644 --- a/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean +++ b/Mathlib/LinearAlgebra/Dimension/DivisionRing.lean @@ -97,7 +97,8 @@ theorem rank_add_rank_split (db : V₂ →ₗ[K] V) (eb : V₃ →ₗ[K] V) (cd rintro ⟨d, e⟩ have h := eq₂ d (-e) simp only [add_eq_zero_iff_eq_neg, LinearMap.prod_apply, mem_ker, - Prod.mk_inj, coprod_apply, map_neg, neg_apply, LinearMap.mem_range, Pi.prod] at h ⊢ + Prod.mk_inj, coprod_apply, map_neg, neg_apply, LinearMap.mem_range, + Function.prod_apply] at h ⊢ grind end diff --git a/Mathlib/LinearAlgebra/Goursat.lean b/Mathlib/LinearAlgebra/Goursat.lean index 4090de1ada933a..b39c302ba97412 100644 --- a/Mathlib/LinearAlgebra/Goursat.lean +++ b/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, Function.prod_apply, + Subtype.exists, Prod.exists, LinearMap.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, Function.prod_apply, + Subtype.exists, Prod.exists, LinearMap.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 diff --git a/Mathlib/LinearAlgebra/Prod.lean b/Mathlib/LinearAlgebra/Prod.lean index 6416808409864e..21f532a1db5fc0 100644 --- a/Mathlib/LinearAlgebra/Prod.lean +++ b/Mathlib/LinearAlgebra/Prod.lean @@ -93,11 +93,11 @@ theorem snd_surjective : Function.Surjective (snd R M M₂) := fun x => ⟨(0, x /-- The prod of two linear maps is a linear map. -/ @[simps] def prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : M →ₗ[R] M₂ × M₃ where - toFun := Pi.prod f g - map_add' x y := by simp only [Pi.prod, Prod.mk_add_mk, map_add] - map_smul' c x := by simp only [Pi.prod, Prod.smul_mk, map_smul, RingHom.id_apply] + toFun := Function.prod f g + map_add' x y := by simp only [Function.prod_apply, Prod.mk_add_mk, map_add] + map_smul' c x := by simp only [Function.prod_apply, Prod.smul_mk, map_smul, RingHom.id_apply] -theorem coe_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : ⇑(f.prod g) = Pi.prod f g := +theorem coe_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : ⇑(f.prod g) = Function.prod f g := rfl @[simp] @@ -850,7 +850,7 @@ theorem range_prod_eq {f : M →ₗ[R] M₂} {g : M →ₗ[R] M₃} (h : ker f range (prod f g) = (range f).prod (range g) := by refine le_antisymm (f.range_prod_le g) ?_ simp only [SetLike.le_def, prod_apply, mem_range, mem_prod, exists_imp, and_imp, - Prod.forall, Pi.prod] + Prod.forall, Function.prod_apply] rintro _ _ x rfl y rfl -- Note: https://github.com/leanprover-community/mathlib4/pull/8386 had to specify `(f := f)` simp only [Prod.mk_inj, ← sub_mem_ker_iff (f := f)] diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean b/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean index e607498ea392aa..f4f8519a9af008 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Dual.lean @@ -140,7 +140,7 @@ def toDualProd (Q : QuadraticForm R M) [Invertible (2 : R)] : map_app' x := by dsimp only [associated, associatedHom] dsimp only [LinearMap.smul_apply, LinearMap.coe_mk, AddHom.coe_mk, AddHom.toFun_eq_coe, - LinearMap.coe_toAddHom, LinearMap.prod_apply, Pi.prod, LinearMap.add_apply, + LinearMap.coe_toAddHom, LinearMap.prod_apply, Function.prod_apply, LinearMap.add_apply, LinearMap.coe_comp, Function.comp_apply, LinearMap.fst_apply, LinearMap.snd_apply, LinearMap.sub_apply, dualProd_apply, polarBilin_apply_apply, prod_apply, neg_apply] simp only [polar_sub_right, polar_self, nsmul_eq_mul, Nat.cast_ofNat, polar_comm _ x.1 x.2, diff --git a/Mathlib/Logic/Function/Defs.lean b/Mathlib/Logic/Function/Defs.lean index 2d7cf78fb0a363..c08aade421e2ea 100644 --- a/Mathlib/Logic/Function/Defs.lean +++ b/Mathlib/Logic/Function/Defs.lean @@ -31,6 +31,14 @@ def dcomp {β : α → Sort u₂} {φ : ∀ {x : α}, β x → Sort u₃} (f : @[inherit_doc] infixr:80 " ∘' " => Function.dcomp +@[simp] protected def prod {ι} {α β : ι → Type*} (f : ∀ i, α i) (g : ∀ i, β i) (i : ι) : + α i × β i := (f i, g i) + +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 `α`. -/ diff --git a/Mathlib/MeasureTheory/Integral/Prod.lean b/Mathlib/MeasureTheory/Integral/Prod.lean index 6c872f1d9a8b54..7f3f98fb7fd90b 100644 --- a/Mathlib/MeasureTheory/Integral/Prod.lean +++ b/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 diff --git a/Mathlib/MeasureTheory/Measure/Prod.lean b/Mathlib/MeasureTheory/Measure/Prod.lean index 6ccbdf61d6394e..e14709c68ecd9c 100644 --- a/Mathlib/MeasureTheory/Measure/Prod.lean +++ b/Mathlib/MeasureTheory/Measure/Prod.lean @@ -837,7 +837,7 @@ theorem map_prod_map {δ} [MeasurableSpace δ] {f : α → β} {g : γ → δ} ( -- hence it is placed in the `WithDensity` file, where the instance is defined. lemma prod_smul_left {μ : Measure α} (c : ℝ≥0∞) : (c • μ).prod ν = c • (μ.prod ν) := by ext s hs - rw [Measure.prod_apply hs, Measure.smul_apply, Measure.prod_apply hs] + rw [prod_apply hs, Measure.smul_apply, prod_apply hs] simp end Measure @@ -873,7 +873,7 @@ theorem skew_product [SFinite μa] [SFinite μc] {f : α → β} (hf : MeasurePr infer_instance -- Thus we can use the integral formula for the product measure, and compute things explicitly ext s hs - rw [map_apply this hs, prod_apply (this hs), prod_apply hs, + rw [map_apply this hs, Measure.prod_apply (this hs), Measure.prod_apply hs, ← hf.lintegral_comp (measurable_measure_prodMk_left hs)] apply lintegral_congr_ae filter_upwards [hg] with a ha @@ -898,7 +898,7 @@ theorem prod_of_right {f : α × β → γ} {μ : Measure α} {ν : Measure β} QuasiMeasurePreserving f (μ.prod ν) τ := by refine ⟨hf, ?_⟩ refine AbsolutelyContinuous.mk fun s hs h2s => ?_ - rw [map_apply hf hs, prod_apply (hf hs)]; simp_rw [preimage_preimage] + rw [map_apply hf hs, Measure.prod_apply (hf hs)]; simp_rw [preimage_preimage] rw [lintegral_congr_ae (h2f.mono fun x hx => hx.preimage_null h2s), lintegral_zero] theorem prod_of_left {α β γ} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] @@ -1222,8 +1222,9 @@ theorem _root_.MeasureTheory.measurePreserving_prodAssoc (μa : Measure α) (μb have A (x : α) : MeasurableSet (Prod.mk x ⁻¹' s) := measurable_prodMk_left hs have B : MeasurableSet (MeasurableEquiv.prodAssoc ⁻¹' s) := MeasurableEquiv.prodAssoc.measurable hs - simp_rw [map_apply MeasurableEquiv.prodAssoc.measurable hs, prod_apply hs, prod_apply (A _), - prod_apply B, lintegral_prod _ (measurable_measure_prodMk_left B).aemeasurable] + simp_rw [map_apply MeasurableEquiv.prodAssoc.measurable hs, Measure.prod_apply hs, + Measure.prod_apply (A _), Measure.prod_apply B, + lintegral_prod _ (measurable_measure_prodMk_left B).aemeasurable] rfl theorem _root_.MeasureTheory.volume_preserving_prodAssoc {α₁ β₁ γ₁ : Type*} [MeasureSpace α₁] diff --git a/Mathlib/NumberTheory/Height/Basic.lean b/Mathlib/NumberTheory/Height/Basic.lean index f8e6f016da506b..3e1eb2e95a4e1b 100644 --- a/Mathlib/NumberTheory/Height/Basic.lean +++ b/Mathlib/NumberTheory/Height/Basic.lean @@ -667,7 +667,7 @@ lemma mulHeight_fun_prod_eq {x : (a : α) → ι a → K} (hx : ∀ a, x a ≠ 0 simp_rw [ne_iff, Pi.zero_def] at hx ⊢ choose f hf using hx exact ⟨f, prod_ne_zero_iff.mpr fun a _ ↦ hf a⟩ - simp_rw [map_prod, Real.iSup_prod_eq_prod_iSup_of_nonnegHomClass] + simp_rw [_root_.map_prod, Real.iSup_prod_eq_prod_iSup_of_nonnegHomClass] rw [Multiset.prod_map_prod, finprod_prod_comm _ _ fun b _ ↦ hasFiniteMulSupport_iSup_nonarchAbsVal (hx b), ← prod_mul_distrib] diff --git a/Mathlib/SetTheory/Cardinal/Finite.lean b/Mathlib/SetTheory/Cardinal/Finite.lean index a5a8ff16138638..9a618a494b8171 100644 --- a/Mathlib/SetTheory/Cardinal/Finite.lean +++ b/Mathlib/SetTheory/Cardinal/Finite.lean @@ -237,7 +237,7 @@ theorem card_sigma {β : α → Type*} [Fintype α] [∀ a, Finite (β a)] : simp_rw [Nat.card_eq_fintype_card, Fintype.card_sigma] theorem card_pi {β : α → Type*} [Fintype α] : Nat.card (∀ a, β a) = ∏ a, Nat.card (β a) := by - simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, map_prod] + simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, _root_.map_prod] theorem card_fun [Finite α] : Nat.card (α → β) = Nat.card β ^ Nat.card α := by haveI := Fintype.ofFinite α diff --git a/Mathlib/Topology/Algebra/ContinuousAffineMap.lean b/Mathlib/Topology/Algebra/ContinuousAffineMap.lean index 8d123a766054d6..901f4bf7b59131 100644 --- a/Mathlib/Topology/Algebra/ContinuousAffineMap.lean +++ b/Mathlib/Topology/Algebra/ContinuousAffineMap.lean @@ -400,7 +400,7 @@ def prod (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃) : P₁ →ᴬ[k] P __ := AffineMap.prod f g cont := by eta_expand; dsimp; fun_prop -theorem coe_prod (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃) : prod f g = Pi.prod f g := +theorem coe_prod (f : P₁ →ᴬ[k] P₂) (g : P₁ →ᴬ[k] P₃) : prod f g = Function.prod f g := rfl @[simp] diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean index 76df744cc7a2ea..9e003c7c1295f8 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean @@ -221,7 +221,7 @@ protected theorem HasProd.map [CommMonoid γ] [TopologicalSpace γ] (hf : HasPro protected theorem Topology.IsInducing.hasProd_iff [CommMonoid γ] [TopologicalSpace γ] {G} [FunLike G α γ] [MonoidHomClass G α γ] {g : G} (hg : IsInducing g) (f : β → α) (a : α) : HasProd (g ∘ f) (g a) L ↔ HasProd f a L := by - simp_rw [HasProd, comp_apply, ← map_prod] + simp_rw [HasProd, comp_apply, ← _root_.map_prod] exact hg.tendsto_nhds_iff.symm @[to_additive] @@ -261,7 +261,7 @@ lemma Topology.IsClosedEmbedding.map_tprod {ι α α' G : Type*} simp only [Multipliable, HasProd] at h ⊢ obtain ⟨b, hb⟩ := h obtain ⟨a, ha⟩ : b ∈ Set.range g := - hge.isClosed_range.mem_of_tendsto hb (.of_forall <| by simp [← map_prod]) + hge.isClosed_range.mem_of_tendsto hb (.of_forall <| by simp [← _root_.map_prod]) use a simp [hge.tendsto_nhds_iff, Function.comp_def, ha, hb] · simpa [tprod_bot hL] using @@ -288,7 +288,7 @@ lemma Topology.IsInducing.multipliable_iff_tprod_comp_mem_range [CommMonoid γ] · by_cases hL : L.NeBot · exact ⟨_, hf.map_tprod g hg.continuous⟩ · by_cases hfs : (mulSupport fun x ↦ g (f x)).Finite - · simp [tprod_bot hL, finprod_eq_prod _ hfs, ← map_prod] + · simp [tprod_bot hL, finprod_eq_prod _ hfs, ← _root_.map_prod] · exact ⟨1, by simp [tprod_bot hL, finprod_of_infinite_mulSupport hfs]⟩ · rintro ⟨hgf, a, ha⟩ use a diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean index 1be2234cb609ad..0f29cf7e430d4e 100644 --- a/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean +++ b/Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean @@ -274,7 +274,7 @@ variable {ι : Type*} {X : α → Type*} [∀ x, CommMonoid (X x)] [∀ x, Topol @[to_additive] theorem Pi.hasProd {f : ι → ∀ x, X x} {g : ∀ x, X x} : HasProd f g L ↔ ∀ x, HasProd (fun i ↦ f i x) (g x) L := by - simp only [HasProd, tendsto_pi_nhds, prod_apply] + simp only [HasProd, tendsto_pi_nhds, Finset.prod_apply] @[to_additive] theorem Pi.multipliable {f : ι → ∀ x, X x} : diff --git a/Mathlib/Topology/Inseparable.lean b/Mathlib/Topology/Inseparable.lean index 956b0bfc78b695..ec597005b3e71a 100644 --- a/Mathlib/Topology/Inseparable.lean +++ b/Mathlib/Topology/Inseparable.lean @@ -483,7 +483,7 @@ theorem subtype_inseparable_iff {p : X → Prop} (x y : Subtype p) : (x ~ᵢ y) @[simp] theorem inseparable_prod {x₁ x₂ : X} {y₁ y₂ : Y} : ((x₁, y₁) ~ᵢ (x₂, y₂)) ↔ (x₁ ~ᵢ x₂) ∧ (y₁ ~ᵢ y₂) := by - simp only [Inseparable, nhds_prod_eq, prod_inj] + simp only [Inseparable, nhds_prod_eq, Filter.prod_inj] theorem Inseparable.prod {x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₁ ~ᵢ x₂) (hy : y₁ ~ᵢ y₂) : (x₁, y₁) ~ᵢ (x₂, y₂) := diff --git a/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean b/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean index 2170661fd474fb..c86814c50bb786 100644 --- a/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean +++ b/Mathlib/Topology/UniformSpace/LocallyUniformConvergence.lean @@ -208,7 +208,7 @@ theorem TendstoLocallyUniformlyOn.prodMk [UniformSpace γ] {G : ι → α → γ theorem TendstoLocallyUniformlyOn.piProd [UniformSpace γ] {G : ι → α → γ} {g : α → γ} (hF : TendstoLocallyUniformlyOn F f p s) (hG : TendstoLocallyUniformlyOn G g p s) : - TendstoLocallyUniformlyOn (fun n ↦ Pi.prod (F n) (G n)) (Pi.prod f g) p s := + TendstoLocallyUniformlyOn (fun n ↦ Function.prod (F n) (G n)) (Function.prod f g) p s := hF.prodMk hG theorem TendstoLocallyUniformly.prodMk [UniformSpace γ] {G : ι → α → γ} {g : α → γ} @@ -219,7 +219,7 @@ theorem TendstoLocallyUniformly.prodMk [UniformSpace γ] {G : ι → α → γ} theorem TendstoLocallyUniformly.piProd [UniformSpace γ] {G : ι → α → γ} {g : α → γ} (hF : TendstoLocallyUniformly F f p) (hG : TendstoLocallyUniformly G g p) : - TendstoLocallyUniformly (fun n ↦ Pi.prod (F n) (G n)) (Pi.prod f g) p := + TendstoLocallyUniformly (fun n ↦ Function.prod (F n) (G n)) (Function.prod f g) p := hF.prodMk hG /-- If every `x ∈ s` has a neighbourhood within `s` on which `F i` tends uniformly to `f`, then From 3898f3824d33190856f4d6308c3e132296a01ade Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Wed, 6 May 2026 12:05:56 +0100 Subject: [PATCH 20/23] Add superscript to notation --- Mathlib/Logic/Function/Init.lean | 88 ++++++++++++++++---------------- 1 file changed, 43 insertions(+), 45 deletions(-) diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index 6677ecd52b4d9b..ef9a830bee74ce 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -16,18 +16,18 @@ 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 +* `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` (notation `△`): the diagonal `a ↦ (a, a)`, i.e. `id ⋏ id`. +* `Function.diag` (notation `△ᶠ`): the diagonal `a ↦ (a, a)`, i.e. `id ×ᶠ id`. * `Function.prodMap`: `Prod.map` re-exposed under `Function` so that `f.prodMap g` works via dot notation. ## Notation -The infix `⋏` for `Function.prod` mirrors `∧`: pairing is the propositions-as-types conjunction -(`f ⋏ g` reads as "both `f` and `g`"). The prefix `△` for `Function.diag` depicts the fan-out +The infix notation `×ᶠ` for `Function.prod` pairs two functions. +The prefix `△ᶠ` notation for `Function.diag` depicts the fan-out shape of `a ↦ (a, a)`: apex-up for one-to-two. This file should not depend on anything defined in Mathlib (other than notation), so that it can @@ -72,7 +72,7 @@ theorem dcomp_assoc {κ : Sort*} (h : κ → ι) : f ∘' g ∘' h = (f ∘' g) end -/-- Product of functions: `(f ⋏ g) i = (f i, g i)`, where the types of `f i` and `g i` +/-- 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) @@ -85,28 +85,28 @@ may depend on `i`. -/ @[inline] def sndComp {ι} {α β : ι → Type*} (h : (i : ι) → α i × β i) (i : ι) : β i := (h i).2 -@[inherit_doc] infixr:95 " ⋏ " => prod +@[inherit_doc] infixr:95 " ×ᶠ " => prod 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 prod_apply : (f ×ᶠ g) i = (f i, g i) := rfl @[simp, grind =] theorem fstComp_apply : fstComp h i = (h i).1 := rfl @[simp, grind =] theorem sndComp_apply : sndComp h i = (h i).2 := rfl -theorem prod_def : f ⋏ g = fun i => (f i, g i) := rfl +theorem prod_def : f ×ᶠ g = fun i => (f i, g i) := rfl theorem fst_dcomp : Prod.fst ∘' h = fstComp h := rfl theorem snd_dcomp : Prod.snd ∘' h = sndComp h := rfl @[simp, grind! .] theorem fstComp_prod {f : ∀ i, α i} {g : ∀ i, β i} : - fstComp (f ⋏ g) = f := rfl + fstComp (f ×ᶠ g) = f := rfl @[simp, grind! .] theorem sndComp_prod {f : ∀ i, α i} {g : ∀ i, β i} : - sndComp (f ⋏ g) = g := rfl + sndComp (f ×ᶠ g) = g := rfl @[simp, grind! .] theorem fstComp_prod_sndComp {h : ∀ i, α i × β i} : - fstComp h ⋏ sndComp h = h := rfl + fstComp h ×ᶠ sndComp h = h := rfl theorem fstComp_sndComp_ext {h h' : ∀ i, α i × β i} (H₁ : fstComp h = fstComp h') (H₂ : sndComp h = sndComp h') : h = h' := by grind @@ -114,29 +114,22 @@ theorem fstComp_sndComp_ext {h h' : ∀ i, α i × β i} (H₁ : fstComp h = fst theorem fstComp_sndComp_ext_iff {h h' : ∀ i, α i × β i} : h = h' ↔ fstComp h = fstComp h' ∧ sndComp h = sndComp 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 +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 + f ×ᶠ g = f' ×ᶠ g' ↔ f = f' ∧ g = g' := by grind -theorem exists_pair_prod : ∃ f g, f ⋏ g = h := - ⟨fstComp h, sndComp h, fstComp_prod_sndComp⟩ -theorem exists_fstComp [Nonempty (∀ i, β i)] : ∃ h : ∀ i, α i × β i, fstComp h = f := - ⟨f ⋏ Classical.ofNonempty, fstComp_prod⟩ -theorem exists_sndComp [Nonempty (∀ i, α i)] : ∃ h : ∀ i, α i × β i, sndComp h = g := - ⟨Classical.ofNonempty ⋏ g, sndComp_prod⟩ +theorem prod_eq_iff : f ×ᶠ g = h ↔ f = fstComp h ∧ g = sndComp h := by grind +theorem eq_prod_iff : h = f ×ᶠ g ↔ fstComp h = f ∧ sndComp h = g := by grind -theorem prod_eq_iff : f ⋏ g = h ↔ f = fstComp h ∧ g = sndComp h := by grind -theorem eq_prod_iff : h = f ⋏ g ↔ fstComp h = f ∧ sndComp h = g := by grind - -theorem prod_dcomp (h : κ → ι) : (f ⋏ g) ∘' h = (f ∘' h) ⋏ (g ∘' h) := rfl +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 + (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 +@[simp] theorem swap_dcomp_prod : Prod.swap ∘' (f ×ᶠ g) = g ×ᶠ f := rfl end @@ -145,11 +138,11 @@ section variable {ι : Type*} {α β : ι → Type*} theorem leftInverse_uncurry_prod_fstComp_prod_sndComp : - LeftInverse prod.uncurry (fstComp (α := α) ⋏ sndComp (β := β)) := by + LeftInverse prod.uncurry (fstComp (α := α) ×ᶠ sndComp (β := β)) := by simp [LeftInverse] theorem rightInverse_uncurry_prod_fstComp_prod_sndComp : - RightInverse prod.uncurry (fstComp (α := α) ⋏ sndComp (β := β)) := by + RightInverse prod.uncurry (fstComp (α := α) ×ᶠ sndComp (β := β)) := by simp [RightInverse, LeftInverse] theorem uncurry_prod_injective : (prod (α := α) (β := β)).uncurry.Injective := @@ -174,48 +167,53 @@ theorem snd_comp (h : ι → α × β) : Prod.snd ∘ h = sndComp h := rfl @[simp] theorem fstComp_mk_flip : fstComp ((Prod.mk · b) : α → α × β) = id := rfl @[simp] theorem sndComp_mk_flip : sndComp ((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 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 +@[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 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 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 + (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 + Prod.map h k ∘ f ×ᶠ g = (h ∘ f) ×ᶠ (k ∘ g) := rfl -@[simp] theorem swap_comp_prod : Prod.swap ∘ (f ⋏ g) = g ⋏ f := rfl +@[simp] theorem swap_comp_prod : Prod.swap ∘ (f ×ᶠ g) = g ×ᶠ f := rfl end /-- The diagonal map into `Prod`. -/ -@[inline] def diag {α} : α → α × α := id ⋏ id +@[inline] def diag {α} : α → α × α := id ×ᶠ id -@[inherit_doc] prefix:max "△" => diag +@[inherit_doc] prefix:max "△ᶠ" => diag section variable {α β γ} (f : α → β) (g : α → γ) (a b : α) -@[simp, grind =] theorem diag_apply : △a = (a, a) := rfl +@[simp, grind =] theorem diag_apply : △ᶠa = (a, a) := rfl -@[simp] theorem id_prod_id : id ⋏ id = diag (α := α) := rfl +@[simp] theorem id_prod_id : id ×ᶠ id = diag (α := α) := rfl @[simp] theorem fstComp_diag : fstComp (diag (α := α)) = id := rfl @[simp] theorem sndComp_diag : sndComp (diag (α := α)) = id := rfl -@[simp] theorem diag_comp : diag ∘ f = f ⋏ f := rfl +@[simp] theorem diag_comp : diag ∘ f = f ×ᶠ f := rfl -@[simp] theorem map_comp_diag : Prod.map f g ∘ diag = f ⋏ g := rfl +@[simp] theorem map_comp_diag : Prod.map f g ∘ diag = f ×ᶠ g := rfl theorem injective_diag : Injective (α := α) diag := fun _ _ => congrArg Prod.fst -theorem exists_diag_apply_iff (p : α × α) : (∃ a, △a = p) ↔ p.1 = p.2 := by - simp [Prod.ext_iff] +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 @@ -224,7 +222,7 @@ 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) + (f ∘ Prod.fst) ×ᶠ (g ∘ Prod.snd) section From d7636e818b6344fdc804e7d1190ada4d76986f8d Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Wed, 6 May 2026 17:00:20 +0100 Subject: [PATCH 21/23] Tweak notation --- Mathlib/Logic/Function/Init.lean | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index ef9a830bee74ce..15ebe49971c841 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -20,16 +20,10 @@ living in the `Function` namespace so that dot notation is available. `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` (notation `△ᶠ`): the diagonal `a ↦ (a, a)`, i.e. `id ×ᶠ id`. +* `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. -## Notation - -The infix notation `×ᶠ` for `Function.prod` pairs two functions. -The prefix `△ᶠ` notation for `Function.diag` depicts the fan-out -shape of `a ↦ (a, a)`: apex-up for one-to-two. - 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. -/ @@ -189,13 +183,13 @@ end /-- The diagonal map into `Prod`. -/ @[inline] def diag {α} : α → α × α := id ×ᶠ id -@[inherit_doc] prefix:max "△ᶠ" => diag +@[inherit_doc] notation:max "△(" x:max ")" => diag x section variable {α β γ} (f : α → β) (g : α → γ) (a b : α) -@[simp, grind =] theorem diag_apply : △ᶠa = (a, a) := rfl +@[simp, grind =] theorem diag_apply : △(a) = (a, a) := rfl @[simp] theorem id_prod_id : id ×ᶠ id = diag (α := α) := rfl @[simp] theorem fstComp_diag : fstComp (diag (α := α)) = id := rfl @@ -207,12 +201,12 @@ variable {α β γ} (f : α → β) (g : α → γ) (a b : α) theorem injective_diag : Injective (α := α) diag := fun _ _ => congrArg Prod.fst -theorem fst_diag_eq_snd_diag : (△ᶠa).1 = (△ᶠa).2 := rfl +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 +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 +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 From 540ead947fa9f9c18a5049804cf260ed07b47ef7 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Thu, 7 May 2026 11:18:12 +0100 Subject: [PATCH 22/23] Notation tweak --- Mathlib/Logic/Function/Init.lean | 46 +++++++++++++++++--------------- 1 file changed, 24 insertions(+), 22 deletions(-) diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index 15ebe49971c841..3d2084745bf596 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -72,14 +72,16 @@ may depend on `i`. -/ (i : ι) → α i × β i := fun i => Prod.mk (f i) (g i) /-- The first component of a map into a product. -/ -@[inline] def fstComp {ι} {α β : ι → Type*} (h : (i : ι) → α i × β i) (i : ι) : - α i := (h i).1 +@[inline] def fstComp {ι} {α β : ι → Type*} (h : (i : ι) → α i × β i) : + ∀ i, α i := (h ·|>.1) /-- The second component of a map into a product. -/ @[inline] def sndComp {ι} {α β : ι → Type*} (h : (i : ι) → α i × β i) (i : ι) : β i := (h i).2 @[inherit_doc] infixr:95 " ×ᶠ " => prod +@[inherit_doc] notation:max x:max "₍₁₎" => fstComp x +@[inherit_doc] notation:max x:max "₍₂₎" => sndComp x section @@ -87,26 +89,26 @@ variable {ι κ} {α β : ι → Type*} (f f' : ∀ i, α i) (g g' : ∀ i, β i (i : ι) @[simp, grind =] theorem prod_apply : (f ×ᶠ g) i = (f i, g i) := rfl -@[simp, grind =] theorem fstComp_apply : fstComp h i = (h i).1 := rfl -@[simp, grind =] theorem sndComp_apply : sndComp h i = (h i).2 := 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 = fstComp h := rfl -theorem snd_dcomp : Prod.snd ∘' h = sndComp h := 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} : - fstComp (f ×ᶠ g) = f := rfl + (f ×ᶠ g)₍₁₎ = f := by grind @[simp, grind! .] theorem sndComp_prod {f : ∀ i, α i} {g : ∀ i, β i} : - sndComp (f ×ᶠ g) = g := rfl + (f ×ᶠ g)₍₂₎ = g := rfl @[simp, grind! .] theorem fstComp_prod_sndComp {h : ∀ i, α i × β i} : - fstComp h ×ᶠ sndComp h = h := rfl + h₍₁₎ ×ᶠ h₍₂₎ = h := rfl -theorem fstComp_sndComp_ext {h h' : ∀ i, α i × β i} (H₁ : fstComp h = fstComp h') - (H₂ : sndComp h = sndComp h') : h = h' := by grind +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' ↔ fstComp h = fstComp h' ∧ sndComp h = sndComp h' := by grind + 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 @@ -114,8 +116,8 @@ 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 = fstComp h ∧ g = sndComp h := by grind -theorem eq_prod_iff : h = f ×ᶠ g ↔ fstComp h = f ∧ sndComp h = 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 @@ -152,14 +154,14 @@ section variable {α β γ δ : Type*} {ι κ : Sort*} (f : ι → α) (g : ι → β) (a : α) (b : β) (p : α × β) -theorem fst_comp (h : ι → α × β) : Prod.fst ∘ h = fstComp h := rfl -theorem snd_comp (h : ι → α × β) : Prod.snd ∘ h = sndComp h := rfl +theorem fst_comp (h : ι → α × β) : Prod.fst ∘ h = h₍₁₎ := rfl +theorem snd_comp (h : ι → α × β) : Prod.snd ∘ h = h₍₂₎ := rfl -@[simp] theorem fstComp_mk : fstComp (Prod.mk a : β → α × β) = const β a := rfl -@[simp] theorem sndComp_mk : sndComp (Prod.mk a : β → α × β) = id := 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 : fstComp ((Prod.mk · b) : α → α × β) = id := rfl -@[simp] theorem sndComp_mk_flip : sndComp ((Prod.mk · b) : α → α × β) = const α b := 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 @@ -192,8 +194,8 @@ 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 : fstComp (diag (α := α)) = id := rfl -@[simp] theorem sndComp_diag : sndComp (diag (α := α)) = id := rfl +@[simp] theorem fstComp_diag : (diag (α := α))₍₁₎ = id := rfl +@[simp] theorem sndComp_diag : (diag (α := α))₍₂₎ = id := rfl @[simp] theorem diag_comp : diag ∘ f = f ×ᶠ f := rfl From 59c5bba53200ec6a87dc7fb44dca67f3a28bfdae Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Mon, 11 May 2026 13:10:14 +0100 Subject: [PATCH 23/23] Update notation --- Mathlib/Logic/Function/Init.lean | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/Mathlib/Logic/Function/Init.lean b/Mathlib/Logic/Function/Init.lean index 3d2084745bf596..24829c88f1fe1b 100644 --- a/Mathlib/Logic/Function/Init.lean +++ b/Mathlib/Logic/Function/Init.lean @@ -71,17 +71,17 @@ 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) : - ∀ i, α i := (h ·|>.1) +@[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) (i : ι) : - β i := (h i).2 +@[inline] def sndComp {ι} {α β : ι → Type*} (h : (i : ι) → α i × β i) := (h ·|>.2) -@[inherit_doc] infixr:95 " ×ᶠ " => prod -@[inherit_doc] notation:max x:max "₍₁₎" => fstComp x -@[inherit_doc] notation:max x:max "₍₂₎" => sndComp x +@[inherit_doc] postfix:max "₍₂₎" => sndComp section