diff --git a/Mathlib.lean b/Mathlib.lean index 1d25f1feb37561..b324d28abf1d95 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -5148,6 +5148,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/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/Exact.lean b/Mathlib/Algebra/Exact.lean index 0a9beae3a2905a..93d70ae8228689 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) rw [← sub_eq_zero, ← hz, ← h₁ z, hz, map_sub, e.1, sub_self, map_zero] · rintro ⟨x, y⟩ diff --git a/Mathlib/Algebra/MvPolynomial/Equiv.lean b/Mathlib/Algebra/MvPolynomial/Equiv.lean index 42533556b7db52..25f48c14e0d504 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/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..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 @@ -26,14 +27,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 diff --git a/Mathlib/Algebra/Star/StarAlgHom.lean b/Mathlib/Algebra/Star/StarAlgHom.lean index 6fb56955d0554d..e2aaf7149ee76b 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/Combinatorics/Nullstellensatz.lean b/Mathlib/Combinatorics/Nullstellensatz.lean index 1b48c9c479a0f9..c58e090a81702c 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/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 new file mode 100644 index 00000000000000..7d1498b797ec19 --- /dev/null +++ b/Mathlib/Logic/Function/Init.lean @@ -0,0 +1,201 @@ +/- +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 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:95 " ▽' " => 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 + +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 + +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 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⟩ + +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 + +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 + +namespace Function + +variable {α β γ δ : Type*} {ι : Sort*} + +/-- The map into a product type built from maps into each component. -/ +protected def prod : (ι → α) → (ι → β) → ι → α × β := (· ▽' ·) + +@[inherit_doc] infixr:95 " ▽ " => Function.prod + +section + +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 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_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_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] + +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 + +@[simp, 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 + +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 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₂⟩ + +end + +/-- 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] 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 + +@[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 + +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] theorem diag_prod_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) + +section + +@[simp, grind =] +theorem prodMap_eq_prod_map {f : α → β} {g : γ → δ} : f.prodMap g = Prod.map f g := rfl + +end + +end Function 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 diff --git a/Mathlib/MeasureTheory/Measure/Prod.lean b/Mathlib/MeasureTheory/Measure/Prod.lean index 8ceecb66a24d8d..f9244fcab9bdb9 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 b2604b01e28d73..8bf674f51f92d8 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/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean index cd2568f0ba7934..01d6cd652f0a33 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 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} :