From 1720cfdbe3d9bc246707ced88c1fea2f630c9f31 Mon Sep 17 00:00:00 2001 From: Wrenna Robson Date: Sat, 4 Apr 2026 16:15:37 +0100 Subject: [PATCH 01/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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/11] 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 ``` -/