From 49c10909cf40bf43c6257ed74933dd0fd0c0435c Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Wed, 8 May 2024 13:44:41 +0000 Subject: [PATCH 01/15] chore(Order/Interval/Finset/Defs): golf (#12752) Co-authored-by: Moritz Firsching --- Mathlib/Order/Interval/Finset/Defs.lean | 98 +++++++------------------ 1 file changed, 26 insertions(+), 72 deletions(-) diff --git a/Mathlib/Order/Interval/Finset/Defs.lean b/Mathlib/Order/Interval/Finset/Defs.lean index 6a459d37b15d9..810717c7a9eea 100644 --- a/Mathlib/Order/Interval/Finset/Defs.lean +++ b/Mathlib/Order/Interval/Finset/Defs.lean @@ -710,60 +710,32 @@ instance OrderDual.instLocallyFiniteOrder : LocallyFiniteOrder αᵒᵈ where finset_mem_Ioc _ _ _ := (mem_Ico (α := α)).trans and_comm finset_mem_Ioo _ _ _ := (mem_Ioo (α := α)).trans and_comm -theorem Icc_toDual : Icc (toDual a) (toDual b) = (Icc b a).map toDual.toEmbedding := by - refine' Eq.trans _ map_refl.symm - ext c - rw [mem_Icc, mem_Icc (α := α)] - exact and_comm +theorem Icc_toDual : Icc (toDual a) (toDual b) = (Icc b a).map toDual.toEmbedding := map_refl.symm #align Icc_to_dual Icc_toDual -theorem Ico_toDual : Ico (toDual a) (toDual b) = (Ioc b a).map toDual.toEmbedding := by - refine' Eq.trans _ map_refl.symm - ext c - rw [mem_Ico, mem_Ioc (α := α)] - exact and_comm +theorem Ico_toDual : Ico (toDual a) (toDual b) = (Ioc b a).map toDual.toEmbedding := map_refl.symm #align Ico_to_dual Ico_toDual -theorem Ioc_toDual : Ioc (toDual a) (toDual b) = (Ico b a).map toDual.toEmbedding := by - refine' Eq.trans _ map_refl.symm - ext c - rw [mem_Ioc, mem_Ico (α := α)] - exact and_comm +theorem Ioc_toDual : Ioc (toDual a) (toDual b) = (Ico b a).map toDual.toEmbedding := map_refl.symm #align Ioc_to_dual Ioc_toDual -theorem Ioo_toDual : Ioo (toDual a) (toDual b) = (Ioo b a).map toDual.toEmbedding := by - refine' Eq.trans _ map_refl.symm - ext c - rw [mem_Ioo, mem_Ioo (α := α)] - exact and_comm +theorem Ioo_toDual : Ioo (toDual a) (toDual b) = (Ioo b a).map toDual.toEmbedding := map_refl.symm #align Ioo_to_dual Ioo_toDual -theorem Icc_ofDual (a b : αᵒᵈ) : Icc (ofDual a) (ofDual b) = (Icc b a).map ofDual.toEmbedding := by - refine' Eq.trans _ map_refl.symm - ext c - rw [mem_Icc, mem_Icc (α := αᵒᵈ)] - exact and_comm +theorem Icc_ofDual (a b : αᵒᵈ) : Icc (ofDual a) (ofDual b) = (Icc b a).map ofDual.toEmbedding := + map_refl.symm #align Icc_of_dual Icc_ofDual -theorem Ico_ofDual (a b : αᵒᵈ) : Ico (ofDual a) (ofDual b) = (Ioc b a).map ofDual.toEmbedding := by - refine' Eq.trans _ map_refl.symm - ext c - rw [mem_Ico, mem_Ioc (α := αᵒᵈ)] - exact and_comm +theorem Ico_ofDual (a b : αᵒᵈ) : Ico (ofDual a) (ofDual b) = (Ioc b a).map ofDual.toEmbedding := + map_refl.symm #align Ico_of_dual Ico_ofDual -theorem Ioc_ofDual (a b : αᵒᵈ) : Ioc (ofDual a) (ofDual b) = (Ico b a).map ofDual.toEmbedding := by - refine' Eq.trans _ map_refl.symm - ext c - rw [mem_Ioc, mem_Ico (α := αᵒᵈ)] - exact and_comm +theorem Ioc_ofDual (a b : αᵒᵈ) : Ioc (ofDual a) (ofDual b) = (Ico b a).map ofDual.toEmbedding := + map_refl.symm #align Ioc_of_dual Ioc_ofDual -theorem Ioo_ofDual (a b : αᵒᵈ) : Ioo (ofDual a) (ofDual b) = (Ioo b a).map ofDual.toEmbedding := by - refine' Eq.trans _ map_refl.symm - ext c - rw [mem_Ioo, mem_Ioo (α := αᵒᵈ)] - exact and_comm +theorem Ioo_ofDual (a b : αᵒᵈ) : Ioo (ofDual a) (ofDual b) = (Ioo b a).map ofDual.toEmbedding := + map_refl.symm #align Ioo_of_dual Ioo_ofDual end LocallyFiniteOrder @@ -841,20 +813,17 @@ namespace Prod instance [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableRel ((· ≤ ·) : α × β → α × β → Prop)] : LocallyFiniteOrder (α × β) := LocallyFiniteOrder.ofIcc' (α × β) (fun a b => Icc a.fst b.fst ×ˢ Icc a.snd b.snd) fun a b x => by - rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm] - rfl + rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm, le_def, le_def] instance [LocallyFiniteOrderTop α] [LocallyFiniteOrderTop β] [DecidableRel ((· ≤ ·) : α × β → α × β → Prop)] : LocallyFiniteOrderTop (α × β) := LocallyFiniteOrderTop.ofIci' (α × β) (fun a => Ici a.fst ×ˢ Ici a.snd) fun a x => by - rw [mem_product, mem_Ici, mem_Ici] - rfl + rw [mem_product, mem_Ici, mem_Ici, le_def] instance [LocallyFiniteOrderBot α] [LocallyFiniteOrderBot β] [DecidableRel ((· ≤ ·) : α × β → α × β → Prop)] : LocallyFiniteOrderBot (α × β) := LocallyFiniteOrderBot.ofIic' (α × β) (fun a => Iic a.fst ×ˢ Iic a.snd) fun a x => by - rw [mem_product, mem_Iic, mem_Iic] - rfl + rw [mem_product, mem_Iic, mem_Iic, le_def] theorem Icc_eq [LocallyFiniteOrder α] [LocallyFiniteOrder β] [DecidableRel ((· ≤ ·) : α × β → α × β → Prop)] (p q : α × β) : @@ -960,8 +929,7 @@ instance locallyFiniteOrder : LocallyFiniteOrder (WithTop α) where | (a : α), ⊤, ⊤ => by simp [WithTop.some, WithTop.top, insertNone] | (a : α), ⊤, (x : α) => by simp only [some, le_eq_subset, some_le_some, le_top, and_true] - rw [some_mem_insertNone] - simp + rw [some_mem_insertNone, mem_Ici] | (a : α), (b : α), ⊤ => by simp only [Embedding.some, mem_map, mem_Icc, and_false, exists_const, some, le_top, top_le_iff] @@ -1285,8 +1253,8 @@ theorem BddBelow.finite_of_bddAbove [Preorder α] [LocallyFiniteOrder α] theorem Set.finite_iff_bddAbove [SemilatticeSup α] [LocallyFiniteOrder α] [OrderBot α] : s.Finite ↔ BddAbove s := - ⟨fun h ↦ ⟨h.toFinset.sup id, fun x hx ↦ Finset.le_sup (f := id) (by simpa)⟩, - fun ⟨m, hm⟩ ↦ (Set.finite_Icc ⊥ m).subset (fun x hx ↦ ⟨bot_le, hm hx⟩)⟩ + ⟨fun h ↦ ⟨h.toFinset.sup id, fun _ hx ↦ Finset.le_sup (f := id) ((Finite.mem_toFinset h).mpr hx)⟩, + fun ⟨m, hm⟩ ↦ (Set.finite_Icc ⊥ m).subset (fun _ hx ↦ ⟨bot_le, hm hx⟩)⟩ theorem Set.finite_iff_bddBelow [SemilatticeInf α] [LocallyFiniteOrder α] [OrderTop α] : s.Finite ↔ BddBelow s := @@ -1296,8 +1264,10 @@ theorem Set.finite_iff_bddBelow_bddAbove [Nonempty α] [Lattice α] [LocallyFini s.Finite ↔ BddBelow s ∧ BddAbove s := by obtain (rfl | hs) := s.eq_empty_or_nonempty · simp only [Set.finite_empty, bddBelow_empty, bddAbove_empty, and_self] - exact ⟨fun h ↦ ⟨⟨h.toFinset.inf' (by simpa) id, fun x hx ↦ Finset.inf'_le id (by simpa)⟩, - ⟨h.toFinset.sup' (by simpa) id, fun x hx ↦ Finset.le_sup' id (by simpa)⟩⟩, + exact ⟨fun h ↦ ⟨⟨h.toFinset.inf' ((Finite.toFinset_nonempty h).mpr hs) id, + fun x hx ↦ Finset.inf'_le id ((Finite.mem_toFinset h).mpr hx)⟩, + ⟨h.toFinset.sup' ((Finite.toFinset_nonempty h).mpr hs) id, fun x hx ↦ Finset.le_sup' id + ((Finite.mem_toFinset h).mpr hx)⟩⟩, fun ⟨h₀, h₁⟩ ↦ BddBelow.finite_of_bddAbove h₀ h₁⟩ end Finite @@ -1350,32 +1320,16 @@ instance (priority := low) [Preorder α] [DecidableRel ((· : α) < ·)] [Locall exact fun _ => b.property instance [Preorder α] [LocallyFiniteOrderBot α] : Finite { x : α // x ≤ y } := by - apply Set.Finite.to_subtype - convert (Finset.Iic y).finite_toSet using 1 - ext - simp - rfl + simpa only [coe_Iic] using (Finset.Iic y).finite_toSet instance [Preorder α] [LocallyFiniteOrderBot α] : Finite { x : α // x < y } := by - apply Set.Finite.to_subtype - convert (Finset.Iio y).finite_toSet using 1 - ext - simp - rfl + simpa only [coe_Iio] using (Finset.Iio y).finite_toSet instance [Preorder α] [LocallyFiniteOrderTop α] : Finite { x : α // y ≤ x } := by - apply Set.Finite.to_subtype - convert (Finset.Ici y).finite_toSet using 1 - ext - simp - rfl + simpa only [coe_Ici] using (Finset.Ici y).finite_toSet instance [Preorder α] [LocallyFiniteOrderTop α] : Finite { x : α // y < x } := by - apply Set.Finite.to_subtype - convert (Finset.Ioi y).finite_toSet using 1 - ext - simp - rfl + simpa only [coe_Ioi] using (Finset.Ioi y).finite_toSet namespace Set variable {α : Type*} [Preorder α] From 063b1255bfc75dd729a3f168dbf1838a55213f49 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Wed, 8 May 2024 15:10:41 +0000 Subject: [PATCH 02/15] fix: typo in polyrith (#12754) --- Mathlib/Tactic/Polyrith.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Tactic/Polyrith.lean b/Mathlib/Tactic/Polyrith.lean index 7acbd079047ff..92ab11e3d03ad 100644 --- a/Mathlib/Tactic/Polyrith.lean +++ b/Mathlib/Tactic/Polyrith.lean @@ -422,7 +422,7 @@ elab_rules : tactic | `(tactic| polyrith%$tk $[only%$onlyTk]? $[[$hyps,*]]?) => do let hyps ← hyps.map (·.getElems) |>.getD #[] |>.mapM (elabTerm · none) let traceMe ← Lean.isTracingEnabledFor `Meta.Tactic.polyrith - match ← polyrith (← getMainGoal) onlyTk.isNone hyps traceMe with + match ← polyrith (← getMainGoal) onlyTk.isSome hyps traceMe with | .ok stx => replaceMainGoal [] if !traceMe then Lean.Meta.Tactic.TryThis.addSuggestion tk stx From 9d8f6783f64176fcf8a328020945b9d79f3a8711 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Wed, 8 May 2024 15:35:53 +0000 Subject: [PATCH 03/15] feat(Algebra/Category/ModuleCat): the category of presheaves of modules has colimits (#12713) --- Mathlib.lean | 1 + .../Category/ModuleCat/ChangeOfRings.lean | 13 ++ .../Algebra/Category/ModuleCat/Colimits.lean | 7 + .../Category/ModuleCat/Presheaf/Colimits.lean | 159 ++++++++++++++++++ .../Category/ModuleCat/Presheaf/Limits.lean | 3 - 5 files changed, 180 insertions(+), 3 deletions(-) create mode 100644 Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean diff --git a/Mathlib.lean b/Mathlib.lean index ee72500dd3ea7..25ce23f473fdb 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -88,6 +88,7 @@ import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic import Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric import Mathlib.Algebra.Category.ModuleCat.Presheaf +import Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits import Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits import Mathlib.Algebra.Category.ModuleCat.Products import Mathlib.Algebra.Category.ModuleCat.Projective diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean index 9daa574cffe25..2221518135dcb 100644 --- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean +++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jujian Zhang -/ import Mathlib.Algebra.Category.ModuleCat.EpiMono +import Mathlib.Algebra.Category.ModuleCat.Colimits import Mathlib.Algebra.Category.ModuleCat.Limits import Mathlib.RingTheory.TensorProduct.Basic @@ -873,4 +874,16 @@ noncomputable instance preservesLimitRestrictScalars have hc' := isLimitOfPreserves (forget₂ _ AddCommGroupCat) hc exact isLimitOfReflects (forget₂ _ AddCommGroupCat) hc'⟩ +instance preservesColimitRestrictScalars {R S : Type*} [Ring R] [Ring S] + (f : R →+* S) {J : Type*} [Category J] (F : J ⥤ ModuleCat.{v} S) + [HasColimit (F ⋙ forget₂ _ AddCommGroupCat)] : + PreservesColimit F (ModuleCat.restrictScalars.{v} f) := by + have : HasColimit ((F ⋙ restrictScalars f) ⋙ forget₂ (ModuleCat R) AddCommGroupCat) := + inferInstanceAs (HasColimit (F ⋙ forget₂ _ AddCommGroupCat)) + apply preservesColimitOfPreservesColimitCocone (HasColimit.isColimitColimitCocone F) + apply isColimitOfReflects (forget₂ _ AddCommGroupCat) + apply isColimitOfPreserves (forget₂ (ModuleCat.{v} S) AddCommGroupCat.{v}) + exact HasColimit.isColimitColimitCocone F + + end ModuleCat diff --git a/Mathlib/Algebra/Category/ModuleCat/Colimits.lean b/Mathlib/Algebra/Category/ModuleCat/Colimits.lean index 3ca028fe8d29e..1c452e36296f8 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Colimits.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Colimits.lean @@ -101,6 +101,10 @@ instance : HasColimit F := ⟨_, isColimitColimitCocone F⟩ noncomputable instance : PreservesColimit F (forget₂ _ AddCommGroupCat) := preservesColimitOfPreservesColimitCocone (isColimitColimitCocone F) (colimit.isColimit _) +noncomputable instance reflectsColimit : + ReflectsColimit F (forget₂ (ModuleCat.{w'} R) AddCommGroupCat) := + reflectsColimitOfReflectsIsomorphisms _ _ + end HasColimit variable (J R) @@ -108,6 +112,9 @@ variable (J R) instance hasColimitsOfShape [HasColimitsOfShape J AddCommGroupCat.{w'}] : HasColimitsOfShape J (ModuleCat.{w'} R) where +noncomputable instance reflectsColimitsOfShape [HasColimitsOfShape J AddCommGroupCat.{w'}] : + ReflectsColimitsOfShape J (forget₂ (ModuleCat.{w'} R) AddCommGroupCat) where + instance hasColimitsOfSize [HasColimitsOfSize.{v, u} AddCommGroupCat.{w'}] : HasColimitsOfSize.{v, u} (ModuleCat.{w'} R) where diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean new file mode 100644 index 0000000000000..fefcc51f4fd18 --- /dev/null +++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Colimits.lean @@ -0,0 +1,159 @@ +/- +Copyright (c) 2024 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +import Mathlib.Algebra.Category.ModuleCat.Presheaf +import Mathlib.Algebra.Category.ModuleCat.Colimits + +/-! # Colimits in categories of presheaves of modules + +In this file, it is shown that under suitable assumptions, +colimits exist in the category `PresheafOfModules R`. + +-/ + +universe v v₁ v₂ u₁ u₂ u u' + +open CategoryTheory Category Limits + +namespace PresheafOfModules + +variable {C : Type u₁} [Category.{v₁} C] {R : Cᵒᵖ ⥤ RingCat.{u}} + {J : Type u₂} [Category.{v₂} J] + (F : J ⥤ PresheafOfModules.{v} R) + +section Colimits + +variable [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y), PreservesColimit (F ⋙ evaluation R Y) + (ModuleCat.restrictScalars (R.map f))] + +/-- A cocone in the category `PresheafOfModules R` is colimit if it is so after the application +of the functors `evaluation R X` for all `X`. -/ +def evaluationJointlyReflectsColimits (c : Cocone F) + (hc : ∀ (X : Cᵒᵖ), IsColimit ((evaluation R X).mapCocone c)) : IsColimit c where + desc s := Hom.mk'' (fun X => (hc X).desc ((evaluation R X).mapCocone s)) (fun X Y f => by + apply (hc X).hom_ext + intro j + erw [(hc X).fac_assoc ((evaluation R X).mapCocone s) j, ← restrictionApp_naturality_assoc] + rw [← Functor.map_comp] + erw [(hc Y).fac ((evaluation R Y).mapCocone s), restrictionApp_naturality] + rfl) + fac s j := by + ext1 X + exact (hc X).fac ((evaluation R X).mapCocone s) j + uniq s m hm := by + ext1 X + apply (hc X).uniq ((evaluation R X).mapCocone s) + intro j + dsimp + rw [← hm] + rfl + +variable [∀ X, HasColimit (F ⋙ evaluation R X)] + +instance {X Y : Cᵒᵖ} (f : X ⟶ Y) : + HasColimit (F ⋙ evaluation R Y ⋙ (ModuleCat.restrictScalars (R.map f))) := + ⟨_, isColimitOfPreserves (ModuleCat.restrictScalars (R.map f)) + (colimit.isColimit (F ⋙ evaluation R Y))⟩ + +/-- Given `F : J ⥤ PresheafOfModules.{v} R`, this is the `BundledCorePresheafOfModules R` which +corresponds to the presheaf of modules which sends `X` to the colimit of `F ⋙ evaluation R X`. -/ +@[simps] +noncomputable def colimitBundledCore : BundledCorePresheafOfModules R where + obj X := colimit (F ⋙ evaluation R X) + map {X Y} f := colimMap (whiskerLeft F (restriction R f)) ≫ + (preservesColimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv + map_id X := colimit.hom_ext (fun j => by + dsimp + rw [ι_colimMap_assoc, whiskerLeft_app, restriction_app] + erw [ι_preservesColimitsIso_inv (G := ModuleCat.restrictScalars (R.map (𝟙 X))), + ModuleCat.restrictScalarsId'App_inv_naturality] + rw [restrictionApp_id] + rfl) + map_comp {X Y Z} f g := colimit.hom_ext (fun j => by + dsimp + rw [ι_colimMap_assoc, whiskerLeft_app, restriction_app, assoc, ι_colimMap_assoc] + erw [ι_preservesColimitsIso_inv (G := ModuleCat.restrictScalars (R.map (f ≫ g))), + ι_preservesColimitsIso_inv_assoc (G := ModuleCat.restrictScalars (R.map f))] + rw [← Functor.map_comp_assoc, ι_colimMap_assoc] + erw [ι_preservesColimitsIso_inv (G := ModuleCat.restrictScalars (R.map g))] + rw [restrictionApp_comp, ModuleCat.restrictScalarsComp'_inv_app, assoc, assoc, + whiskerLeft_app, whiskerLeft_app, restriction_app, restriction_app] + simp only [Functor.map_comp, assoc] + rfl) + +/-- Given `F : J ⥤ PresheafOfModules.{v} R`, this is the canonical map +`F.obj j ⟶ (colimitBundledCore F).toPresheafOfModules` for all `j : J`. -/ +noncomputable def colimitCoconeιApp (j : J) : + F.obj j ⟶ (colimitBundledCore F).toPresheafOfModules := + PresheafOfModules.Hom.mk'' (fun X => colimit.ι (F ⋙ evaluation R X) j) (fun X Y f => by + dsimp + erw [colimit.ι_desc_assoc, assoc, ← ι_preservesColimitsIso_inv] + rfl) + +@[reassoc (attr := simp)] +lemma colimitCoconeιApp_naturality {i j : J} (f : i ⟶ j) : + F.map f ≫ colimitCoconeιApp F j = colimitCoconeιApp F i := by + ext1 X + exact colimit.w (F ⋙ evaluation R X) f + +/-- The (colimit) cocone for `F : J ⥤ PresheafOfModules.{v} R` that is constructed from +the colimit of `F ⋙ evaluation R X` for all `X`. -/ +@[simps] +noncomputable def colimitCocone : Cocone F where + pt := (colimitBundledCore F).toPresheafOfModules + ι := { app := colimitCoconeιApp F } + +/-- The cocone `colimitCocone F` is colimit for any `F : J ⥤ PresheafOfModules.{v} R`. -/ +noncomputable def isColimitColimitCocone : IsColimit (colimitCocone F) := + evaluationJointlyReflectsColimits _ _ (fun _ => colimit.isColimit _) + +instance hasColimit : HasColimit F := ⟨_, isColimitColimitCocone F⟩ + +noncomputable instance evaluationPreservesColimit (X : Cᵒᵖ) : + PreservesColimit F (evaluation R X) := + preservesColimitOfPreservesColimitCocone (isColimitColimitCocone F) (colimit.isColimit _) + +variable [∀ X, PreservesColimit F + (evaluation R X ⋙ forget₂ (ModuleCat (R.obj X)) AddCommGroupCat)] + +noncomputable instance toPresheafPreservesColimit : + PreservesColimit F (toPresheaf R) := + preservesColimitOfPreservesColimitCocone (isColimitColimitCocone F) + (Limits.evaluationJointlyReflectsColimits _ + (fun X => isColimitOfPreserves (evaluation R X ⋙ forget₂ _ AddCommGroupCat) + (isColimitColimitCocone F))) + +end Colimits + +variable (R J) + +section HasColimitsOfShape + +variable [HasColimitsOfShape J AddCommGroupCat.{v}] + +instance hasColimitsOfShape : HasColimitsOfShape J (PresheafOfModules.{v} R) where + +noncomputable instance evaluationPreservesColimitsOfShape (X : Cᵒᵖ) : + PreservesColimitsOfShape J (evaluation R X : PresheafOfModules.{v} R ⥤ _) where + +noncomputable instance toPresheafPreservesColimitsOfShape : + PreservesColimitsOfShape J (toPresheaf.{v} R) where + +end HasColimitsOfShape + +namespace Finite + +instance hasFiniteColimits : HasFiniteColimits (PresheafOfModules.{v} R) := + ⟨fun _ => inferInstance⟩ + +noncomputable instance evaluationPreservesFiniteColimits (X : Cᵒᵖ) : + PreservesFiniteColimits (evaluation.{v} R X) where + +noncomputable instance toPresheafPreservesFiniteColimits : + PreservesFiniteColimits (toPresheaf R) where + +end Finite + +end PresheafOfModules diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean index c5b87e8127cbf..b5cb79ba5c6b5 100644 --- a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean +++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean @@ -13,9 +13,6 @@ import Mathlib.CategoryTheory.Limits.FunctorCategory In this file, it is shown that under suitable assumptions, limits exist in the category `PresheafOfModules R`. -## TODO -* do the same for colimits - -/ universe v v₁ v₂ u₁ u₂ u u' From 54a54ded180ca32fdc608779ed3447c213dc3a76 Mon Sep 17 00:00:00 2001 From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Date: Wed, 8 May 2024 15:35:54 +0000 Subject: [PATCH 04/15] fix: remove MathlibExtras from mk_all.sh (#12763) This directory was removed in #12548. --- scripts/mk_all.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_all.sh b/scripts/mk_all.sh index cd69ce8ef2641..d5712ee52b116 100755 --- a/scripts/mk_all.sh +++ b/scripts/mk_all.sh @@ -1,6 +1,6 @@ #! /usr/bin/env bash cd "$(git rev-parse --show-toplevel)" || exit 1 -for gp in Mathlib MathlibExtras Mathlib/Tactic Counterexamples Archive +for gp in Mathlib Mathlib/Tactic Counterexamples Archive do git ls-files "$gp/*.lean" | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > "$gp.lean" done From e6ea7987e2bef631d2be529252a5ff581e12362e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 8 May 2024 16:11:19 +0000 Subject: [PATCH 05/15] feat: `positivity` extension for `posPart`, `negPart` (#10681) --- Mathlib/Tactic/Positivity/Basic.lean | 23 +++++++++++++++++++++++ scripts/noshake.json | 1 + test/positivity.lean | 4 ++++ 3 files changed, 28 insertions(+) diff --git a/Mathlib/Tactic/Positivity/Basic.lean b/Mathlib/Tactic/Positivity/Basic.lean index d10e7f4edc057..ef67fdf4e2bbc 100644 --- a/Mathlib/Tactic/Positivity/Basic.lean +++ b/Mathlib/Tactic/Positivity/Basic.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, Heather Macbeth, Yaël Dillies -/ import Mathlib.Algebra.GroupPower.Order +import Mathlib.Algebra.Order.Group.PosPart import Mathlib.Data.Int.CharZero import Mathlib.Algebra.Order.Ring.Int import Mathlib.Data.Nat.Factorial.Basic @@ -450,3 +451,25 @@ def evalRatDen : PositivityExt where eval {u α} _ _ e := do assumeInstancesCommute pure $ .positive q(den_pos $a) | _, _ => throwError "not Rat.num" + +/-- Extension for `posPart`. `a⁺` is always nonegative, and positive if `a` is. -/ +@[positivity _⁺] +def evalPosPart : PositivityExt where eval zα pα e := do + match e with + | ~q(@posPart _ $instαlat $instαgrp $a) => + assertInstancesCommute + -- FIXME: There seems to be a bug in `Positivity.core` that makes it fail (instead of returning + -- `.none`) here sometimes. See eg the first test for `posPart`. This is why we need `catchNone` + match ← catchNone (core zα pα a) with + | .positive pf => return .positive q(posPart_pos $pf) + | _ => return .nonnegative q(posPart_nonneg $a) + | _ => throwError "not `posPart`" + +/-- Extension for `negPart`. `a⁻` is always nonegative. -/ +@[positivity _⁻] +def evalNegPart : PositivityExt where eval _ _ e := do + match e with + | ~q(@negPart _ $instαlat $instαgrp $a) => + assertInstancesCommute + return .nonnegative q(negPart_nonneg $a) + | _ => throwError "not `negPart`" diff --git a/scripts/noshake.json b/scripts/noshake.json index 08fa3decea166..69ec9572e9508 100644 --- a/scripts/noshake.json +++ b/scripts/noshake.json @@ -222,6 +222,7 @@ "Mathlib.Tactic.Positivity.Finset": ["Mathlib.Data.Fintype.Card"], "Mathlib.Tactic.Positivity.Basic": ["Mathlib.Algebra.GroupPower.Order", + "Mathlib.Algebra.Order.Group.PosPart", "Mathlib.Data.Int.CharZero", "Mathlib.Data.Nat.Factorial.Basic"], "Mathlib.Tactic.NormNum.Ineq": diff --git a/test/positivity.lean b/test/positivity.lean index 5e58a2e5776d3..decca1cf3385c 100644 --- a/test/positivity.lean +++ b/test/positivity.lean @@ -196,6 +196,10 @@ example (hq : 0 ≤ q) : 0 ≤ q.num := by positivity end +example (a : ℤ) : 0 ≤ a⁺ := by positivity +example (a : ℤ) (ha : 0 < a) : 0 < a⁺ := by positivity +example (a : ℤ) : 0 ≤ a⁻ := by positivity + /-! ### Exponentiation -/ example [OrderedSemiring α] [Nontrivial α] (a : α) : 0 < a ^ 0 := by positivity From 59b7bc4871691da68166f821185b40bf5fb9240a Mon Sep 17 00:00:00 2001 From: Matthew Robert Ballard Date: Wed, 8 May 2024 18:28:53 +0000 Subject: [PATCH 06/15] refactor(Opposite): `Opposite.mk` -> `Opposite.op` (#12636) It was observed on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/making.20.60op.60.20irreducible) that we should really have `op` as the custom name for the `Opposite` constructor as long as it remains a structure. --- .../Morphisms/RingHomProperties.lean | 3 ++- Mathlib/CategoryTheory/Preadditive/Injective.lean | 4 ++-- Mathlib/CategoryTheory/Sites/CompatiblePlus.lean | 9 +++------ Mathlib/Data/Opposite.lean | 13 +++++-------- Mathlib/Geometry/RingedSpace/OpenImmersion.lean | 8 +++++--- Mathlib/Topology/Sheaves/Skyscraper.lean | 1 - 6 files changed, 17 insertions(+), 21 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean index 6b5eb8f6e83fd..cf5af48cd1f0c 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean @@ -308,7 +308,8 @@ theorem sourceAffineLocally_of_source_openCover {X Y : Scheme.{u}} (f : X ⟶ Y) swap · refine' X.presheaf.map (@homOfLE _ _ ((IsOpenMap.functor _).obj _) ((IsOpenMap.functor _).obj _) _).op - rw [unop_op, unop_op, Opens.openEmbedding_obj_top, Opens.openEmbedding_obj_top] + dsimp + rw [Opens.openEmbedding_obj_top, Opens.openEmbedding_obj_top] exact X.basicOpen_le _ · rw [op_comp, op_comp, Functor.map_comp, Functor.map_comp] refine' (Eq.trans _ (Category.assoc (obj := CommRingCat) _ _ _).symm : _) diff --git a/Mathlib/CategoryTheory/Preadditive/Injective.lean b/Mathlib/CategoryTheory/Preadditive/Injective.lean index da4f68035a0ea..cccd3796845bd 100644 --- a/Mathlib/CategoryTheory/Preadditive/Injective.lean +++ b/Mathlib/CategoryTheory/Preadditive/Injective.lean @@ -161,11 +161,11 @@ instance {β : Type v} (c : β → C) [HasZeroMorphisms C] [HasBiproduct c] [∀ ext simp only [Category.assoc, biproduct.lift_π, comp_factorThru] -instance {P : Cᵒᵖ} [Projective P] : Injective (unop P) where +instance {P : Cᵒᵖ} [Projective P] : Injective no_index (unop P) where factors g f mono := ⟨(@Projective.factorThru Cᵒᵖ _ P _ _ _ g.op f.op _).unop, Quiver.Hom.op_inj (by simp)⟩ -instance {J : Cᵒᵖ} [Injective J] : Projective (unop J) where +instance {J : Cᵒᵖ} [Injective J] : Projective no_index (unop J) where factors f e he := ⟨(@factorThru Cᵒᵖ _ J _ _ _ f.op e.op _).unop, Quiver.Hom.op_inj (by simp)⟩ diff --git a/Mathlib/CategoryTheory/Sites/CompatiblePlus.lean b/Mathlib/CategoryTheory/Sites/CompatiblePlus.lean index 86291a996dfe0..fa9080af35d54 100644 --- a/Mathlib/CategoryTheory/Sites/CompatiblePlus.lean +++ b/Mathlib/CategoryTheory/Sites/CompatiblePlus.lean @@ -207,13 +207,10 @@ theorem whiskerRight_toPlus_comp_plusCompIso_hom : simp only [ι_plusCompIso_hom, Functor.map_comp, Category.assoc] simp only [← Category.assoc] congr 1 - -- Porting note: this used to work with `ext` -- See https://github.com/leanprover-community/mathlib4/issues/5229 - apply Multiequalizer.hom_ext - delta Cover.toMultiequalizer - simp only [diagramCompIso_hom_ι, Category.assoc, ← F.map_comp] - simp only [unop_op, limit.lift_π, Multifork.ofι_π_app, Functor.comp_obj, Functor.comp_map, - implies_true] + apply Multiequalizer.hom_ext; intro a + rw [Category.assoc, diagramCompIso_hom_ι, ← F.map_comp] + simp only [unop_op, limit.lift_π, Multifork.ofι_π_app, Functor.comp_obj, Functor.comp_map] #align category_theory.grothendieck_topology.whisker_right_to_plus_comp_plus_comp_iso_hom CategoryTheory.GrothendieckTopology.whiskerRight_toPlus_comp_plusCompIso_hom @[simp] diff --git a/Mathlib/Data/Opposite.lean b/Mathlib/Data/Opposite.lean index 27fb4a76304df..ecf0018e7b25e 100644 --- a/Mathlib/Data/Opposite.lean +++ b/Mathlib/Data/Opposite.lean @@ -33,10 +33,15 @@ variable (α : Sort u) -/ structure Opposite := + /-- The canonical map `α → αᵒᵖ`. -/ + op :: /-- The canonical map `αᵒᵖ → α`. -/ unop : α #align opposite Opposite #align opposite.unop Opposite.unop +#align opposite.op Opposite.op + +-- Porting note: pp_nodot has not been implemented for Opposite.op @[inherit_doc] notation:max -- Use a high right binding power (like that of postfix ⁻¹) so that, for example, @@ -47,12 +52,6 @@ namespace Opposite variable {α} -/-- The canonical map `α → αᵒᵖ`. -/ --- Porting note: pp_nodot has not been implemented. ---@[pp_nodot] -def op (x : α) : αᵒᵖ := ⟨x⟩ -#align opposite.op Opposite.op - theorem op_injective : Function.Injective (op : α → αᵒᵖ) := fun _ _ => congr_arg Opposite.unop #align opposite.op_injective Opposite.op_injective @@ -64,14 +63,12 @@ theorem op_unop (x : αᵒᵖ) : op (unop x) = x := rfl #align opposite.op_unop Opposite.op_unop -@[simp] theorem unop_op (x : α) : unop (op x) = x := rfl #align opposite.unop_op Opposite.unop_op -- We could prove these by `Iff.rfl`, but that would make these eligible for `dsimp`. That would be -- a bad idea because `Opposite` is irreducible. -@[simp] theorem op_inj_iff (x y : α) : op x = op y ↔ x = y := op_injective.eq_iff #align opposite.op_inj_iff Opposite.op_inj_iff diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean index feb2c4d771bf2..469c8cef45550 100644 --- a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean +++ b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean @@ -64,7 +64,7 @@ namespace AlgebraicGeometry universe v v₁ v₂ u -variable {C : Type*} [Category C] +variable {C : Type u} [Category.{v} C] /-- An open immersion of PresheafedSpaces is an open embedding `f : X ⟶ U ⊆ Y` of the underlying spaces, such that the sheaf map `Y(V) ⟶ f _* X(V)` is an iso for each `V ⊆ U`. @@ -295,7 +295,6 @@ instance ofRestrict {X : TopCat} (Y : PresheafedSpace C) {f : X ⟶ Y.carrier} congr apply Subsingleton.helim rw [this] - rfl · infer_instance #align algebraic_geometry.PresheafedSpace.is_open_immersion.of_restrict AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.ofRestrict @@ -373,7 +372,10 @@ def pullbackConeOfLeftFst : intro U V i induction U using Opposite.rec' induction V using Opposite.rec' - simp only [Quiver.Hom.unop_op, Category.assoc, Functor.op_map, inv_naturality_assoc] + simp only [Quiver.Hom.unop_op, Category.assoc, Functor.op_map] + -- Note: this doesn't fire in `simp` because of reduction of the term via structure eta + -- before discrimination tree key generation + rw [inv_naturality_assoc] -- Porting note: the following lemmas are not picked up by `simp` -- See https://github.com/leanprover-community/mathlib4/issues/5026 erw [g.c.naturality_assoc, TopCat.Presheaf.pushforwardObj_map, ← Y.presheaf.map_comp, diff --git a/Mathlib/Topology/Sheaves/Skyscraper.lean b/Mathlib/Topology/Sheaves/Skyscraper.lean index f7e5199691e64..a861e784e9f3e 100644 --- a/Mathlib/Topology/Sheaves/Skyscraper.lean +++ b/Mathlib/Topology/Sheaves/Skyscraper.lean @@ -307,7 +307,6 @@ theorem to_skyscraper_fromStalk {𝓕 : Presheaf C X} {c : C} (f : 𝓕 ⟶ skys split_ifs with h · erw [← Category.assoc, colimit.ι_desc, Category.assoc, eqToHom_trans, eqToHom_refl, Category.comp_id] - simp only [unop_op, op_unop] · exact ((if_neg h).symm.ndrec terminalIsTerminal).hom_ext .. #align stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_from_stalk StalkSkyscraperPresheafAdjunctionAuxs.to_skyscraper_fromStalk From ba7e114658fe6add6aad39c24a6b499101de60e1 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Thu, 9 May 2024 00:52:22 +0000 Subject: [PATCH 07/15] feat(Data/Nat/Digits): `digits_head` and `ofDigits_mod_eq_head` (#11129) Co-authored-by: Moritz Firsching --- Mathlib/Algebra/BigOperators/List/Basic.lean | 2 +- Mathlib/Computability/TMToPartrec.lean | 2 -- Mathlib/Data/List/Basic.lean | 3 +++ Mathlib/Data/Nat/Defs.lean | 2 ++ Mathlib/Data/Nat/Digits.lean | 16 ++++++++++++++++ 5 files changed, 22 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/BigOperators/List/Basic.lean b/Mathlib/Algebra/BigOperators/List/Basic.lean index 68e5c7958861d..4ff97ad3c3ff3 100644 --- a/Mathlib/Algebra/BigOperators/List/Basic.lean +++ b/Mathlib/Algebra/BigOperators/List/Basic.lean @@ -574,7 +574,7 @@ If desired, we could add a class stating that `default = 0`. /-- This relies on `default ℕ = 0`. -/ theorem headI_add_tail_sum (L : List ℕ) : L.headI + L.tail.sum = L.sum := by - cases L <;> simp; rfl + cases L <;> simp #align list.head_add_tail_sum List.headI_add_tail_sum /-- This relies on `default ℕ = 0`. -/ diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean index 481b0c322c45c..75c3db48727e2 100644 --- a/Mathlib/Computability/TMToPartrec.lean +++ b/Mathlib/Computability/TMToPartrec.lean @@ -1182,7 +1182,6 @@ def trNat (n : ℕ) : List Γ' := theorem trNat_zero : trNat 0 = [] := by rw [trNat, Nat.cast_zero]; rfl #align turing.partrec_to_TM2.tr_nat_zero Turing.PartrecToTM2.trNat_zero -@[simp] theorem trNat_default : trNat default = [] := trNat_zero #align turing.partrec_to_TM2.tr_nat_default Turing.PartrecToTM2.trNat_default @@ -1550,7 +1549,6 @@ theorem pred_ok (q₁ q₂ s v) (c d : List Γ') : ∃ s', rcases v with (_ | ⟨_ | n, v⟩) · refine' ⟨none, TransGen.single _⟩ simp - rfl · refine' ⟨some Γ'.cons, TransGen.single _⟩ simp refine' ⟨none, _⟩ diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index db21afe70a8eb..22eb8d4054b1d 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -764,6 +764,9 @@ theorem getLast?_append {l₁ l₂ : List α} {x : α} (h : x ∈ l₂.getLast?) /-! ### head(!?) and tail -/ +@[simp] +theorem head!_nil [Inhabited α] : ([] : List α).head! = default := rfl + @[simp] theorem head_cons_tail (x : List α) (h : x ≠ []) : x.head h :: x.tail = x := by cases x <;> simp at h ⊢ diff --git a/Mathlib/Data/Nat/Defs.lean b/Mathlib/Data/Nat/Defs.lean index 4acfababd4f88..f499725a23f49 100644 --- a/Mathlib/Data/Nat/Defs.lean +++ b/Mathlib/Data/Nat/Defs.lean @@ -66,6 +66,8 @@ variable {a b c d m n k : ℕ} {p q : ℕ → Prop} instance instNontrivial : Nontrivial ℕ := ⟨⟨0, 1, Nat.zero_ne_one⟩⟩ +@[simp] theorem default_eq_zero : default = 0 := rfl + attribute [gcongr] Nat.succ_le_succ attribute [simp] Nat.not_lt_zero Nat.succ_ne_zero Nat.succ_ne_self Nat.zero_ne_one Nat.one_ne_zero Nat.min_eq_left Nat.min_eq_right Nat.max_eq_left Nat.max_eq_right diff --git a/Mathlib/Data/Nat/Digits.lean b/Mathlib/Data/Nat/Digits.lean index 06347ebbab00a..c6619ce27948b 100644 --- a/Mathlib/Data/Nat/Digits.lean +++ b/Mathlib/Data/Nat/Digits.lean @@ -192,6 +192,9 @@ theorem ofDigits_eq_sum_mapIdx (b : ℕ) (L : List ℕ) : Or.inl hl #align nat.of_digits_eq_sum_map_with_index Nat.ofDigits_eq_sum_mapIdx +@[simp] +theorem ofDigits_nil {b : ℕ} : ofDigits b [] = 0 := rfl + @[simp] theorem ofDigits_singleton {b n : ℕ} : ofDigits b [n] = n := by simp [ofDigits] #align nat.of_digits_singleton Nat.ofDigits_singleton @@ -660,6 +663,19 @@ theorem ofDigits_mod (b k : ℕ) (L : List ℕ) : ofDigits b L % k = ofDigits (b ofDigits_modEq b k L #align nat.of_digits_mod Nat.ofDigits_mod +theorem ofDigits_mod_eq_head! (b : ℕ) (l : List ℕ) : ofDigits b l % b = l.head! % b := by + induction l <;> simp [Nat.ofDigits, Int.ModEq] + +theorem head!_digits {b n : ℕ} (h : b ≠ 1) : (Nat.digits b n).head! = n % b := by + by_cases hb : 1 < b + · rcases n with _ | n + · simp + · nth_rw 2 [← Nat.ofDigits_digits b (n + 1)] + rw [Nat.ofDigits_mod_eq_head! _ _] + exact (Nat.mod_eq_of_lt (Nat.digits_lt_base hb <| List.head!_mem_self <| + Nat.digits_ne_nil_iff_ne_zero.mpr <| Nat.succ_ne_zero n)).symm + · rcases n with _ | _ <;> simp_all [show b = 0 by omega] + theorem ofDigits_zmodeq' (b b' : ℤ) (k : ℕ) (h : b ≡ b' [ZMOD k]) (L : List ℕ) : ofDigits b L ≡ ofDigits b' L [ZMOD k] := by induction' L with d L ih From 47d4fa91aedcbd429282046dd1e8c80404a13afc Mon Sep 17 00:00:00 2001 From: Raghuram <102684766+raghuram-13@users.noreply.github.com> Date: Thu, 9 May 2024 04:14:54 +0000 Subject: [PATCH 08/15] feat(Algebra/Ring/Ext): prove extensionality lemmas for Ring and similar typeclasses (#9511) Add a file `Algebra/Ring/Ext`, proving `ext` lemmas for all of the ring-like classes (for example, anything from `NonUnitalNonAssocSemiring` to `CommRing`), stating that two instances of such a class are equal if they define the same addition and multiplication operations. Also prove `ext_iff` variants for each class, and injectivity lemmas for projections from classes to parent classes. --- Mathlib.lean | 1 + Mathlib/Algebra/Ring/Ext.lean | 534 ++++++++++++++++++++++++++++++++++ 2 files changed, 535 insertions(+) create mode 100644 Mathlib/Algebra/Ring/Ext.lean diff --git a/Mathlib.lean b/Mathlib.lean index 25ce23f473fdb..d10438cf9a07b 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -612,6 +612,7 @@ import Mathlib.Algebra.Ring.Defs import Mathlib.Algebra.Ring.Divisibility.Basic import Mathlib.Algebra.Ring.Divisibility.Lemmas import Mathlib.Algebra.Ring.Equiv +import Mathlib.Algebra.Ring.Ext import Mathlib.Algebra.Ring.Fin import Mathlib.Algebra.Ring.Hom.Basic import Mathlib.Algebra.Ring.Hom.Defs diff --git a/Mathlib/Algebra/Ring/Ext.lean b/Mathlib/Algebra/Ring/Ext.lean new file mode 100644 index 0000000000000..9d38fa233e300 --- /dev/null +++ b/Mathlib/Algebra/Ring/Ext.lean @@ -0,0 +1,534 @@ +/- +Copyright (c) 2024 Raghuram Sundararajan. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Raghuram Sundararajan +-/ +import Mathlib.Algebra.Ring.Defs +import Mathlib.Algebra.Group.Ext + +/-! +# Extensionality lemmas for rings and similar structures + +In this file we prove extensionality lemmas for the ring-like structures defined in +`Mathlib/Algebra/Ring/Defs.lean`, ranging from `NonUnitalNonAssocSemiring` to `CommRing`. These +extensionality lemmas take the form of asserting that two algebraic structures on a type are equal +whenever the addition and multiplication defined by them are both the same. + +## Implementation details + +We follow `Mathlib/Algebra/Group/Ext.lean` in using the term `(letI := i; HMul.hMul : R → R → R)` to +refer to the multiplication specified by a typeclass instance `i` on a type `R` (and similarly for +addition). We abbreviate these using some local notations. + +Since `Mathlib/Algebra/Group/Ext.lean` proved several injectivity lemmas, we do so as well — even if +sometimes we don't need them to prove extensionality. + +## Tags +semiring, ring, extensionality +-/ + +local macro:max "local_hAdd[" type:term ", " inst:term "]" : term => + `(term| (letI := $inst; HAdd.hAdd : $type → $type → $type)) +local macro:max "local_hMul[" type:term ", " inst:term "]" : term => + `(term| (letI := $inst; HMul.hMul : $type → $type → $type)) + +universe u + +variable {R : Type u} + +/-! ### Distrib -/ +namespace Distrib + +@[ext] theorem ext ⦃inst₁ inst₂ : Distrib R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := by + -- Split into `add` and `mul` functions and properties. + rcases inst₁ with @⟨⟨⟩, ⟨⟩⟩ + rcases inst₂ with @⟨⟨⟩, ⟨⟩⟩ + -- Prove equality of parts using function extensionality. + congr + +theorem ext_iff {inst₁ inst₂ : Distrib R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext · ·)⟩ + +end Distrib + +/-! ### NonUnitalNonAssocSemiring -/ +namespace NonUnitalNonAssocSemiring + +@[ext] theorem ext ⦃inst₁ inst₂ : NonUnitalNonAssocSemiring R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := by + -- Split into `AddMonoid` instance, `mul` function and properties. + rcases inst₁ with @⟨_, ⟨⟩⟩ + rcases inst₂ with @⟨_, ⟨⟩⟩ + -- Prove equality of parts using already-proved extensionality lemmas. + congr; ext : 1; assumption + +theorem toDistrib_injective : Function.Injective (@toDistrib R) := by + intro _ _ h + ext x y + · exact congrArg (·.toAdd.add x y) h + · exact congrArg (·.toMul.mul x y) h + +theorem ext_iff {inst₁ inst₂ : NonUnitalNonAssocSemiring R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext · ·)⟩ + +end NonUnitalNonAssocSemiring + +/-! ### NonUnitalSemiring -/ +namespace NonUnitalSemiring + +theorem toNonUnitalNonAssocSemiring_injective : + Function.Injective (@toNonUnitalNonAssocSemiring R) := by + rintro ⟨⟩ ⟨⟩ _; congr + +@[ext] theorem ext ⦃inst₁ inst₂ : NonUnitalSemiring R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := + toNonUnitalNonAssocSemiring_injective <| + NonUnitalNonAssocSemiring.ext h_add h_mul + +theorem ext_iff {inst₁ inst₂ : NonUnitalSemiring R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext · ·)⟩ + +end NonUnitalSemiring + +/-! ### NonAssocSemiring and its ancestors + +This section also includes results for `AddMonoidWithOne`, `AddCommMonoidWithOne`, etc. +as these are considered implementation detail of the ring classes. +TODO consider relocating these lemmas. +-/ +/- TODO consider relocating these lemmas. -/ +@[ext] theorem AddMonoidWithOne.ext ⦃inst₁ inst₂ : AddMonoidWithOne R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_one : (letI := inst₁; One.one : R) = (letI := inst₂; One.one : R)) : + inst₁ = inst₂ := by + have h_monoid : inst₁.toAddMonoid = inst₂.toAddMonoid := by ext : 1; exact h_add + have h_zero' : inst₁.toZero = inst₂.toZero := congrArg (·.toZero) h_monoid + have h_one' : inst₁.toOne = inst₂.toOne := + congrArg One.mk h_one + have h_natCast : inst₁.toNatCast.natCast = inst₂.toNatCast.natCast := by + funext n; induction n with + | zero => rewrite [inst₁.natCast_zero, inst₂.natCast_zero] + exact congrArg (@Zero.zero R) h_zero' + | succ n h => rw [inst₁.natCast_succ, inst₂.natCast_succ, h_add] + exact congrArg₂ _ h h_one + rcases inst₁ with @⟨⟨⟩⟩; rcases inst₂ with @⟨⟨⟩⟩ + congr + +theorem AddCommMonoidWithOne.toAddMonoidWithOne_injective : + Function.Injective (@AddCommMonoidWithOne.toAddMonoidWithOne R) := by + rintro ⟨⟩ ⟨⟩ _; congr + +@[ext] theorem AddCommMonoidWithOne.ext ⦃inst₁ inst₂ : AddCommMonoidWithOne R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_one : (letI := inst₁; One.one : R) = (letI := inst₂; One.one : R)) : + inst₁ = inst₂ := + AddCommMonoidWithOne.toAddMonoidWithOne_injective <| + AddMonoidWithOne.ext h_add h_one + +namespace NonAssocSemiring + +/- The best place to prove that the `NatCast` is determined by the other operations is probably in +an extensionality lemma for `AddMonoidWithOne`, in which case we may as well do the typeclasses +defined in `Mathlib/Algebra/GroupWithZero/Defs.lean` as well. -/ +@[ext] theorem ext ⦃inst₁ inst₂ : NonAssocSemiring R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := by + have h : inst₁.toNonUnitalNonAssocSemiring = inst₂.toNonUnitalNonAssocSemiring := by + ext : 1 <;> assumption + have h_zero : (inst₁.toMulZeroClass).toZero.zero = (inst₂.toMulZeroClass).toZero.zero := + congrArg (fun inst => (inst.toMulZeroClass).toZero.zero) h + have h_one' : (inst₁.toMulZeroOneClass).toMulOneClass.toOne + = (inst₂.toMulZeroOneClass).toMulOneClass.toOne := + congrArg (@MulOneClass.toOne R) <| by ext : 1; exact h_mul + have h_one : (inst₁.toMulZeroOneClass).toMulOneClass.toOne.one + = (inst₂.toMulZeroOneClass).toMulOneClass.toOne.one := + congrArg (@One.one R) h_one' + have : inst₁.toAddCommMonoidWithOne = inst₂.toAddCommMonoidWithOne := + by ext : 1 <;> assumption + have : inst₁.toNatCast = inst₂.toNatCast := + congrArg (·.toNatCast) this + -- Split into `NonUnitalNonAssocSemiring`, `One` and `natCast` instances. + cases inst₁; cases inst₂ + congr + +theorem toNonUnitalNonAssocSemiring_injective : + Function.Injective (@toNonUnitalNonAssocSemiring R) := by + intro _ _ _ + ext <;> congr + +theorem ext_iff {inst₁ inst₂ : NonAssocSemiring R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext · ·)⟩ + +end NonAssocSemiring + +/-! ### NonUnitalNonAssocRing -/ +namespace NonUnitalNonAssocRing + +@[ext] theorem ext ⦃inst₁ inst₂ : NonUnitalNonAssocRing R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := by + -- Split into `AddCommGroup` instance, `mul` function and properties. + rcases inst₁ with @⟨_, ⟨⟩⟩; rcases inst₂ with @⟨_, ⟨⟩⟩ + congr; (ext : 1; assumption) + +theorem toNonUnitalNonAssocSemiring_injective : + Function.Injective (@toNonUnitalNonAssocSemiring R) := by + intro _ _ h + -- Use above extensionality lemma to prove injectivity by showing that `h_add` and `h_mul` hold. + ext x y + · exact congrArg (·.toAdd.add x y) h + · exact congrArg (·.toMul.mul x y) h + +theorem ext_iff {inst₁ inst₂ : NonUnitalNonAssocRing R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext · ·)⟩ + +end NonUnitalNonAssocRing + +/-! ### NonUnitalRing -/ +namespace NonUnitalRing + +@[ext] theorem ext ⦃inst₁ inst₂ : NonUnitalRing R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := by + have : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing := by + ext : 1 <;> assumption + -- Split into fields and prove they are equal using the above. + cases inst₁; cases inst₂ + congr + +theorem toNonUnitalSemiring_injective : + Function.Injective (@toNonUnitalSemiring R) := by + intro _ _ h + ext x y + · exact congrArg (·.toAdd.add x y) h + · exact congrArg (·.toMul.mul x y) h + +theorem toNonUnitalNonAssocring_injective : + Function.Injective (@toNonUnitalNonAssocRing R) := by + intro _ _ _ + ext <;> congr + +theorem ext_iff {inst₁ inst₂ : NonUnitalRing R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext · ·)⟩ + +end NonUnitalRing + +/-! ### NonAssocRing and its ancestors + +This section also includes results for `AddGroupWithOne`, `AddCommGroupWithOne`, etc. +as these are considered implementation detail of the ring classes. +TODO consider relocating these lemmas. -/ +@[ext] theorem AddGroupWithOne.ext ⦃inst₁ inst₂ : AddGroupWithOne R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_one : (letI := inst₁; One.one : R) = (letI := inst₂; One.one)) : + inst₁ = inst₂ := by + have : inst₁.toAddMonoidWithOne = inst₂.toAddMonoidWithOne := + AddMonoidWithOne.ext h_add h_one + have : inst₁.toNatCast = inst₂.toNatCast := congrArg (·.toNatCast) this + have h_group : inst₁.toAddGroup = inst₂.toAddGroup := by ext : 1; exact h_add + -- Extract equality of necessary substructures from h_group + injection h_group with h_group; injection h_group + have : inst₁.toIntCast.intCast = inst₂.toIntCast.intCast := by + funext n; cases n with + | ofNat n => rewrite [Int.ofNat_eq_coe, inst₁.intCast_ofNat, inst₂.intCast_ofNat]; congr + | negSucc n => rewrite [inst₁.intCast_negSucc, inst₂.intCast_negSucc]; congr + rcases inst₁ with @⟨⟨⟩⟩; rcases inst₂ with @⟨⟨⟩⟩ + congr + +@[ext] theorem AddCommGroupWithOne.ext ⦃inst₁ inst₂ : AddCommGroupWithOne R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_one : (letI := inst₁; One.one : R) = (letI := inst₂; One.one)) : + inst₁ = inst₂ := by + have : inst₁.toAddCommGroup = inst₂.toAddCommGroup := + AddCommGroup.ext h_add + have : inst₁.toAddGroupWithOne = inst₂.toAddGroupWithOne := + AddGroupWithOne.ext h_add h_one + injection this with _ h_addMonoidWithOne; injection h_addMonoidWithOne + cases inst₁; cases inst₂ + congr + +namespace NonAssocRing + +@[ext] theorem ext ⦃inst₁ inst₂ : NonAssocRing R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := by + have h₁ : inst₁.toNonUnitalNonAssocRing = inst₂.toNonUnitalNonAssocRing := by + ext : 1 <;> assumption + have h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring := by + ext : 1 <;> assumption + -- Mathematically non-trivial fact: `intCast` is determined by the rest. + have h₃ : inst₁.toAddCommGroupWithOne = inst₂.toAddCommGroupWithOne := + AddCommGroupWithOne.ext h_add (congrArg (·.toOne.one) h₂) + cases inst₁; cases inst₂ + congr <;> solve| injection h₁ | injection h₂ | injection h₃ + +theorem toNonAssocSemiring_injective : + Function.Injective (@toNonAssocSemiring R) := by + intro _ _ h + ext x y + · exact congrArg (·.toAdd.add x y) h + · exact congrArg (·.toMul.mul x y) h + +theorem toNonUnitalNonAssocring_injective : + Function.Injective (@toNonUnitalNonAssocRing R) := by + intro _ _ _ + ext <;> congr + +theorem ext_iff {inst₁ inst₂ : NonAssocRing R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext · ·)⟩ + +end NonAssocRing + +/-! ### Semiring -/ +namespace Semiring + +@[ext] theorem ext ⦃inst₁ inst₂ : Semiring R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := by + -- Show that enough substructures are equal. + have h₁ : inst₁.toNonUnitalSemiring = inst₂.toNonUnitalSemiring := by + ext : 1 <;> assumption + have h₂ : inst₁.toNonAssocSemiring = inst₂.toNonAssocSemiring := by + ext : 1 <;> assumption + have h₃ : (inst₁.toMonoidWithZero).toMonoid = (inst₂.toMonoidWithZero).toMonoid := by + ext : 1; exact h_mul + -- Split into fields and prove they are equal using the above. + cases inst₁; cases inst₂ + congr <;> solve| injection h₁ | injection h₂ | injection h₃ + +theorem toNonUnitalSemiring_injective : + Function.Injective (@toNonUnitalSemiring R) := by + intro _ _ h + ext x y + · exact congrArg (·.toAdd.add x y) h + · exact congrArg (·.toMul.mul x y) h + +theorem toNonAssocSemiring_injective : + Function.Injective (@toNonAssocSemiring R) := by + intro _ _ h + ext x y + · exact congrArg (·.toAdd.add x y) h + · exact congrArg (·.toMul.mul x y) h + +theorem ext_iff {inst₁ inst₂ : Semiring R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext · ·)⟩ + +end Semiring + +/-! ### Ring -/ +namespace Ring + +@[ext] theorem ext ⦃inst₁ inst₂ : Ring R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := by + -- Show that enough substructures are equal. + have h₁ : inst₁.toSemiring = inst₂.toSemiring := by + ext : 1 <;> assumption + have h₂ : inst₁.toNonAssocRing = inst₂.toNonAssocRing := by + ext : 1 <;> assumption + /- We prove that the `SubNegMonoid`s are equal because they are one + field away from `Sub` and `Neg`, enabling use of `injection`. -/ + have h₃ : (inst₁.toAddCommGroup).toAddGroup.toSubNegMonoid + = (inst₂.toAddCommGroup).toAddGroup.toSubNegMonoid := + congrArg (@AddGroup.toSubNegMonoid R) <| by ext : 1; exact h_add + -- Split into fields and prove they are equal using the above. + cases inst₁; cases inst₂ + congr <;> solve | injection h₂ | injection h₃ + +theorem toNonUnitalRing_injective : + Function.Injective (@toNonUnitalRing R) := by + intro _ _ h + ext x y + · exact congrArg (·.toAdd.add x y) h + · exact congrArg (·.toMul.mul x y) h + +theorem toNonAssocRing_injective : + Function.Injective (@toNonAssocRing R) := by + intro _ _ _ + ext <;> congr + +theorem toSemiring_injective : + Function.Injective (@toSemiring R) := by + intro _ _ h + ext x y + · exact congrArg (·.toAdd.add x y) h + · exact congrArg (·.toMul.mul x y) h + +theorem ext_iff {inst₁ inst₂ : Ring R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext ·)⟩ + +end Ring + +/-! ### NonUnitalNonAssocCommSemiring -/ +namespace NonUnitalNonAssocCommSemiring + +theorem toNonUnitalNonAssocSemiring_injective : + Function.Injective (@toNonUnitalNonAssocSemiring R) := by + rintro ⟨⟩ ⟨⟩ _; congr + +@[ext] theorem ext ⦃inst₁ inst₂ : NonUnitalNonAssocCommSemiring R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := + toNonUnitalNonAssocSemiring_injective <| + NonUnitalNonAssocSemiring.ext h_add h_mul + +theorem ext_iff {inst₁ inst₂ : NonUnitalNonAssocCommSemiring R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext · ·)⟩ + +end NonUnitalNonAssocCommSemiring + +/-! ### NonUnitalCommSemiring -/ +namespace NonUnitalCommSemiring + +theorem toNonUnitalSemiring_injective : + Function.Injective (@toNonUnitalSemiring R) := by + rintro ⟨⟩ ⟨⟩ _; congr + +@[ext] theorem ext ⦃inst₁ inst₂ : NonUnitalCommSemiring R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := + toNonUnitalSemiring_injective <| + NonUnitalSemiring.ext h_add h_mul + +theorem ext_iff {inst₁ inst₂ : NonUnitalCommSemiring R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext · ·)⟩ + +end NonUnitalCommSemiring + +-- At present, there is no `NonAssocCommSemiring` in Mathlib. + +/-! ### NonUnitalNonAssocCommRing -/ +namespace NonUnitalNonAssocCommRing + +theorem toNonUnitalNonAssocRing_injective : + Function.Injective (@toNonUnitalNonAssocRing R) := by + rintro ⟨⟩ ⟨⟩ _; congr + +@[ext] theorem ext ⦃inst₁ inst₂ : NonUnitalNonAssocCommRing R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := + toNonUnitalNonAssocRing_injective <| + NonUnitalNonAssocRing.ext h_add h_mul + +theorem ext_iff {inst₁ inst₂ : NonUnitalNonAssocCommRing R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext · ·)⟩ + +end NonUnitalNonAssocCommRing + +/-! ### NonUnitalCommRing -/ +namespace NonUnitalCommRing + +theorem toNonUnitalRing_injective : + Function.Injective (@toNonUnitalRing R) := by + rintro ⟨⟩ ⟨⟩ _; congr + +@[ext] theorem ext ⦃inst₁ inst₂ : NonUnitalCommRing R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := + toNonUnitalRing_injective <| + NonUnitalRing.ext h_add h_mul + +theorem ext_iff {inst₁ inst₂ : NonUnitalCommRing R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext · ·)⟩ + +end NonUnitalCommRing + +-- At present, there is no `NonAssocCommRing` in Mathlib. + +/-! ### CommSemiring -/ +namespace CommSemiring + +theorem toSemiring_injective : + Function.Injective (@toSemiring R) := by + rintro ⟨⟩ ⟨⟩ _; congr + +@[ext] theorem ext ⦃inst₁ inst₂ : CommSemiring R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := + toSemiring_injective <| + Semiring.ext h_add h_mul + +theorem ext_iff {inst₁ inst₂ : CommSemiring R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext · ·)⟩ + +end CommSemiring + +/-! ### CommRing -/ +namespace CommRing + +theorem toRing_injective : Function.Injective (@toRing R) := by + rintro ⟨⟩ ⟨⟩ _; congr + +@[ext] theorem ext ⦃inst₁ inst₂ : CommRing R⦄ + (h_add : local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) + (h_mul : local_hMul[R, inst₁] = local_hMul[R, inst₂]) : + inst₁ = inst₂ := + toRing_injective <| Ring.ext h_add h_mul + +theorem ext_iff {inst₁ inst₂ : CommRing R} : + inst₁ = inst₂ ↔ + (local_hAdd[R, inst₁] = local_hAdd[R, inst₂]) ∧ + (local_hMul[R, inst₁] = local_hMul[R, inst₂]) := + ⟨by rintro rfl; constructor <;> rfl, And.elim (ext ·)⟩ + +end CommRing From b72ddd8f67eba47cffd3f3422d6c01f1e666c23f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 9 May 2024 05:29:02 +0000 Subject: [PATCH 09/15] feat: backport changes from lean-pr-testing-4096 (#12772) These changes will be required after https://github.com/leanprover/lean4/pull/4096, but they all look like positive readability changes to me anyway (the things being filled in are sort of hard to work out with time travelling to later lines in the proofs!), so I think we can backport them all to `master`. Co-authored-by: Scott Morrison --- Mathlib/Algebra/Order/CauSeq/Completion.lean | 2 +- Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean | 4 ++-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean | 2 +- Mathlib/Computability/AkraBazzi/AkraBazzi.lean | 2 +- Mathlib/GroupTheory/Coset.lean | 2 +- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean | 2 +- Mathlib/MeasureTheory/Measure/Haar/Unique.lean | 2 +- Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean | 2 +- Mathlib/Order/PrimeIdeal.lean | 2 +- Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean | 2 +- Mathlib/Topology/ContinuousFunction/Bounded.lean | 2 +- 11 files changed, 12 insertions(+), 12 deletions(-) diff --git a/Mathlib/Algebra/Order/CauSeq/Completion.lean b/Mathlib/Algebra/Order/CauSeq/Completion.lean index e835ea0fc6a27..43f63c26c1587 100644 --- a/Mathlib/Algebra/Order/CauSeq/Completion.lean +++ b/Mathlib/Algebra/Order/CauSeq/Completion.lean @@ -236,7 +236,7 @@ theorem inv_mk {f} (hf) : (@mk α _ β _ abv _ f)⁻¹ = mk (inv f hf) := #align cau_seq.completion.inv_mk CauSeq.Completion.inv_mk theorem cau_seq_zero_ne_one : ¬(0 : CauSeq _ abv) ≈ 1 := fun h => - have : LimZero (1 - 0) := Setoid.symm h + have : LimZero (1 - 0 : CauSeq _ abv) := Setoid.symm h have : LimZero 1 := by simpa by apply one_ne_zero <| const_limZero.1 this #align cau_seq.completion.cau_seq_zero_ne_one CauSeq.Completion.cau_seq_zero_ne_one diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean index 06304fe75c151..e63fdf1c2ad26 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean @@ -160,7 +160,7 @@ variable (𝕜 E F) ‖fst 𝕜 E F‖ = 1 := by refine le_antisymm (norm_fst_le ..) ?_ let ⟨e, he⟩ := exists_ne (0 : E) - have : ‖e‖ ≤ _ * max ‖e‖ ‖0‖ := (fst 𝕜 E F).le_opNorm (e, 0) + have : ‖e‖ ≤ _ * max ‖e‖ ‖(0 : F)‖ := (fst 𝕜 E F).le_opNorm (e, 0) rw [norm_zero, max_eq_left (norm_nonneg e)] at this rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr he), one_mul] @@ -170,7 +170,7 @@ variable (𝕜 E F) ‖snd 𝕜 E F‖ = 1 := by refine le_antisymm (norm_snd_le ..) ?_ let ⟨f, hf⟩ := exists_ne (0 : F) - have : ‖f‖ ≤ _ * max ‖0‖ ‖f‖ := (snd 𝕜 E F).le_opNorm (0, f) + have : ‖f‖ ≤ _ * max ‖(0 : E)‖ ‖f‖ := (snd 𝕜 E F).le_opNorm (0, f) rw [norm_zero, max_eq_right (norm_nonneg f)] at this rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr hf), one_mul] diff --git a/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean b/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean index 35b5932ff26a3..60ffd6fc7e1e9 100644 --- a/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean +++ b/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean @@ -96,7 +96,7 @@ theorem not_integrableOn_Ioi_rpow (s : ℝ) : ¬ IntegrableOn (fun x ↦ x ^ s) · have : IntegrableOn (fun x ↦ x ^ s) (Ioo (0 : ℝ) 1) := h.mono Ioo_subset_Ioi_self le_rfl rw [integrableOn_Ioo_rpow_iff zero_lt_one] at this exact hs.not_lt this - · have : IntegrableOn (fun x ↦ x ^ s) (Ioi 1) := h.mono (Ioi_subset_Ioi zero_le_one) le_rfl + · have : IntegrableOn (fun x ↦ x ^ s) (Ioi (1 : ℝ)) := h.mono (Ioi_subset_Ioi zero_le_one) le_rfl rw [integrableOn_Ioi_rpow_iff zero_lt_one] at this exact hs.not_lt this diff --git a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean index ab91ba6657b6b..914f92776b9ff 100644 --- a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean +++ b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean @@ -520,7 +520,7 @@ lemma tendsto_zero_sumCoeffsExp : Tendsto (fun (p : ℝ) => ∑ i, a i * (b i) ^ linarith lemma tendsto_atTop_sumCoeffsExp : Tendsto (fun (p : ℝ) => ∑ i, a i * (b i) ^ p) atBot atTop := by - have h₁ : Tendsto (fun p => (a (max_bi b) : ℝ) * b (max_bi b) ^ p) atBot atTop := + have h₁ : Tendsto (fun p : ℝ => (a (max_bi b) : ℝ) * b (max_bi b) ^ p) atBot atTop := Tendsto.mul_atTop (R.a_pos (max_bi b)) (by simp) <| tendsto_rpow_atBot_of_base_lt_one _ (by have := R.b_pos (max_bi b); linarith) (R.b_lt_one _) diff --git a/Mathlib/GroupTheory/Coset.lean b/Mathlib/GroupTheory/Coset.lean index 3e22b20e912cd..0f4b46c1664b1 100644 --- a/Mathlib/GroupTheory/Coset.lean +++ b/Mathlib/GroupTheory/Coset.lean @@ -148,7 +148,7 @@ variable [Monoid α] (s : Submonoid α) @[to_additive mem_own_leftAddCoset] theorem mem_own_leftCoset (a : α) : a ∈ a • (s : Set α) := - suffices a * 1 ∈ a • ↑s by simpa + suffices a * 1 ∈ a • (s : Set α) by simpa mem_leftCoset a (one_mem s : 1 ∈ s) #align mem_own_left_coset mem_own_leftCoset #align mem_own_left_add_coset mem_own_leftAddCoset diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 6a5351e8839ba..b7885fae4ed40 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -118,7 +118,7 @@ def invertibleEquivDetInvertible : Invertible A ≃ Invertible A.det where variable {A B} theorem mul_eq_one_comm : A * B = 1 ↔ B * A = 1 := - suffices ∀ A B, A * B = 1 → B * A = 1 from ⟨this A B, this B A⟩ + suffices ∀ A B : Matrix n n α, A * B = 1 → B * A = 1 from ⟨this A B, this B A⟩ fun A B h => by letI : Invertible B.det := detInvertibleOfLeftInverse _ _ h letI : Invertible B := invertibleOfDetInvertible B diff --git a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean index 6a74cbf3e0ea6..39ef8d37ab32f 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean @@ -492,7 +492,7 @@ lemma measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport · simpa using (u_mem n).2.le have I1 := I μ' (by infer_instance) simp_rw [M] at I1 - have J1 : ∫ (x : G), indicator {1} (fun _ ↦ 1) (f x) ∂μ' + have J1 : ∫ (x : G), indicator {1} (fun _ ↦ (1 : ℝ)) (f x) ∂μ' = ∫ (x : G), indicator {1} (fun _ ↦ 1) (f x) ∂(haarScalarFactor μ' μ • μ) := tendsto_nhds_unique I1 (I (haarScalarFactor μ' μ • μ) (by infer_instance)) have J2 : ENNReal.toReal (μ' (f ⁻¹' {1})) diff --git a/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean b/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean index 9a94e2cc82300..1e5a747035295 100644 --- a/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean +++ b/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean @@ -88,7 +88,7 @@ theorem prime_of_nat_prime_of_mod_four_eq_three (p : ℕ) [hp : Fact p.Prime] (h irreducible_iff_prime.1 <| by_contradiction fun hpi => let ⟨a, b, hab⟩ := sq_add_sq_of_nat_prime_of_not_irreducible p hpi - have : ∀ a b : ZMod 4, a ^ 2 + b ^ 2 ≠ ↑p := by + have : ∀ a b : ZMod 4, a ^ 2 + b ^ 2 ≠ (p : ZMod 4) := by erw [← ZMod.natCast_mod p 4, hp3]; decide this a b (hab ▸ by simp) #align gaussian_int.prime_of_nat_prime_of_mod_four_eq_three GaussianInt.prime_of_nat_prime_of_mod_four_eq_three diff --git a/Mathlib/Order/PrimeIdeal.lean b/Mathlib/Order/PrimeIdeal.lean index 00ca6fc656f29..137da1310f5c3 100644 --- a/Mathlib/Order/PrimeIdeal.lean +++ b/Mathlib/Order/PrimeIdeal.lean @@ -158,7 +158,7 @@ instance (priority := 100) IsMaximal.isPrime [IsMaximal I] : IsPrime I := by let J := I ⊔ principal x have hJuniv : (J : Set P) = Set.univ := IsMaximal.maximal_proper (lt_sup_principal_of_not_mem ‹_›) - have hyJ : y ∈ ↑J := Set.eq_univ_iff_forall.mp hJuniv y + have hyJ : y ∈ (J : Set P) := Set.eq_univ_iff_forall.mp hJuniv y rw [coe_sup_eq] at hyJ rcases hyJ with ⟨a, ha, b, hb, hy⟩ rw [hy] diff --git a/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean b/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean index 21b12711a50b1..86bc20cf4ce1f 100644 --- a/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean @@ -175,7 +175,7 @@ theorem dvd_pow_natDegree_of_eval₂_eq_zero {f : R →+* A} (hf : Function.Inje (Ideal.mem_span_singleton.mpr <| dvd_refl x)).pow_natDegree_le_of_root_of_monic_mem _ ((monic_scaleRoots_iff x).mpr hp) _ le_rfl rw [injective_iff_map_eq_zero'] at hf - have : eval₂ _ _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h + have : eval₂ f _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h rwa [hz, Polynomial.eval₂_at_apply, hf] at this #align polynomial.dvd_pow_nat_degree_of_eval₂_eq_zero Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero diff --git a/Mathlib/Topology/ContinuousFunction/Bounded.lean b/Mathlib/Topology/ContinuousFunction/Bounded.lean index c37c0582b37d3..39ec9997fa04d 100644 --- a/Mathlib/Topology/ContinuousFunction/Bounded.lean +++ b/Mathlib/Topology/ContinuousFunction/Bounded.lean @@ -581,7 +581,7 @@ theorem arzela_ascoli₂ (s : Set β) (hs : IsCompact s) (A : Set (α →ᵇ β) IsCompact A := by /- This version is deduced from the previous one by restricting to the compact type in the target, using compactness there and then lifting everything to the original space. -/ - have M : LipschitzWith 1 (↑) := LipschitzWith.subtype_val s + have M : LipschitzWith 1 Subtype.val := LipschitzWith.subtype_val s let F : (α →ᵇ s) → α →ᵇ β := comp (↑) M refine' IsCompact.of_isClosed_subset ((_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed fun f hf => _ From ad9935b346590a398c264d9b4bb33f3b6f1928ae Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 9 May 2024 08:07:51 +0000 Subject: [PATCH 10/15] chore: fix deprecation warnings (#12775) In preparation for https://github.com/leanprover/lean4/pull/3969 landing, we fix some deprecation warnings. --- Mathlib/Algebra/Algebra/Equiv.lean | 2 +- Mathlib/Algebra/DirectSum/Algebra.lean | 2 +- Mathlib/Algebra/Group/Submonoid/Units.lean | 4 ++-- .../Algebra/GroupWithZero/Units/Basic.lean | 2 ++ Mathlib/AlgebraicGeometry/Pullbacks.lean | 2 +- .../AlgebraicTopology/DoldKan/GammaCompN.lean | 2 +- Mathlib/Analysis/Calculus/ContDiff/Basic.lean | 10 +++++----- Mathlib/Analysis/Calculus/ContDiff/Defs.lean | 6 +++--- Mathlib/Analysis/Calculus/Darboux.lean | 2 +- Mathlib/Analysis/Complex/AbsMax.lean | 2 +- .../Analysis/Complex/LocallyUniformLimit.lean | 2 +- Mathlib/Analysis/Complex/OpenMapping.lean | 4 ++-- .../Analysis/Complex/PhragmenLindelof.lean | 2 +- Mathlib/Analysis/Convex/Gauge.lean | 4 ++-- Mathlib/Analysis/Convex/KreinMilman.lean | 4 ++-- Mathlib/Analysis/Convolution.lean | 13 ++++++------ .../Analysis/Distribution/SchwartzSpace.lean | 2 +- .../Analysis/InnerProductSpace/Rayleigh.lean | 4 ++-- .../Analysis/NormedSpace/FiniteDimension.lean | 2 +- .../NormedSpace/HahnBanach/Separation.lean | 8 +++++--- Mathlib/Analysis/NormedSpace/Spectrum.lean | 2 +- Mathlib/Analysis/Seminorm.lean | 6 +++--- .../CategoryTheory/Comma/StructuredArrow.lean | 4 ++-- Mathlib/CategoryTheory/Monoidal/Discrete.lean | 2 +- Mathlib/Data/Finset/Sort.lean | 20 +++++++++---------- Mathlib/Data/Finsupp/Basic.lean | 2 +- Mathlib/Data/List/Basic.lean | 4 ++++ Mathlib/Data/List/DropRight.lean | 10 +++++----- Mathlib/Data/List/Forall2.lean | 3 +++ Mathlib/Data/List/Indexes.lean | 1 + Mathlib/Data/List/Infix.lean | 2 +- Mathlib/Data/List/InsertNth.lean | 2 ++ Mathlib/Data/List/NodupEquivFin.lean | 3 ++- Mathlib/Data/List/Perm.lean | 1 + Mathlib/Data/List/Sort.lean | 6 +++++- Mathlib/Data/List/Zip.lean | 6 ++++-- Mathlib/Data/MLList/BestFirst.lean | 4 ++-- Mathlib/Data/Nat/Nth.lean | 2 +- .../RotationNumber/TranslationNumber.lean | 4 ++-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean | 10 ++++++++++ Mathlib/GroupTheory/Perm/List.lean | 1 + .../Function/LpSeminorm/Basic.lean | 2 +- .../Function/StronglyMeasurable/Basic.lean | 2 +- Mathlib/MeasureTheory/Measure/Haar/Basic.lean | 2 +- .../NumberTheory/LSeries/HurwitzZetaEven.lean | 6 +++--- .../ModularForms/JacobiTheta/OneVariable.lean | 2 +- Mathlib/NumberTheory/NumberField/Basic.lean | 2 +- Mathlib/NumberTheory/ZetaValues.lean | 2 +- Mathlib/Probability/Density.lean | 5 +++-- Mathlib/RingTheory/FreeCommRing.lean | 2 +- Mathlib/RingTheory/Trace.lean | 2 +- Mathlib/Topology/Algebra/Order/Compact.lean | 10 +++++----- Mathlib/Topology/Algebra/Order/Rolle.lean | 4 ++-- .../Topology/ContinuousFunction/Ideals.lean | 2 +- .../MetricSpace/GromovHausdorffRealized.lean | 2 +- .../MetricSpace/HausdorffDistance.lean | 8 +++----- Mathlib/Topology/MetricSpace/ProperSpace.lean | 2 +- Mathlib/Topology/ProperMap.lean | 6 ++++-- Mathlib/Topology/UniformSpace/Basic.lean | 2 ++ 59 files changed, 137 insertions(+), 100 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Equiv.lean b/Mathlib/Algebra/Algebra/Equiv.lean index 228041aff0e15..45e7651e606fb 100644 --- a/Mathlib/Algebra/Algebra/Equiv.lean +++ b/Mathlib/Algebra/Algebra/Equiv.lean @@ -232,7 +232,7 @@ nonrec theorem map_sum {ι : Type*} (f : ι → A₁) (s : Finset ι) : theorem map_finsupp_sum {α : Type*} [Zero α] {ι : Type*} (f : ι →₀ α) (g : ι → α → A₁) : e (f.sum g) = f.sum fun i b => e (g i b) := - e.map_sum _ _ + _root_.map_sum e _ _ #align alg_equiv.map_finsupp_sum AlgEquiv.map_finsupp_sum -- Porting note: Added [coe] attribute diff --git a/Mathlib/Algebra/DirectSum/Algebra.lean b/Mathlib/Algebra/DirectSum/Algebra.lean index fdb8c89aaca47..85b2c03bf1b09 100644 --- a/Mathlib/Algebra/DirectSum/Algebra.lean +++ b/Mathlib/Algebra/DirectSum/Algebra.lean @@ -72,7 +72,7 @@ instance : Algebra R (⨁ i, A i) where toFun := (DirectSum.of A 0).comp GAlgebra.toFun map_zero' := AddMonoidHom.map_zero _ map_add' := AddMonoidHom.map_add _ - map_one' := (DirectSum.of A 0).congr_arg GAlgebra.map_one + map_one' := DFunLike.congr_arg (DirectSum.of A 0) GAlgebra.map_one map_mul' a b := by simp only [AddMonoidHom.comp_apply] rw [of_mul_of] diff --git a/Mathlib/Algebra/Group/Submonoid/Units.lean b/Mathlib/Algebra/Group/Submonoid/Units.lean index 89e48fc8afa75..ef959d7f891e4 100644 --- a/Mathlib/Algebra/Group/Submonoid/Units.lean +++ b/Mathlib/Algebra/Group/Submonoid/Units.lean @@ -105,11 +105,11 @@ lemma inv_val_mem_of_mem_units (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units) : @[to_additive] lemma coe_inv_val_mul_coe_val (S : Submonoid M) {x : Sˣ} : - ((x⁻¹ : Sˣ) : M) * ((x : Sˣ) : M) = 1 := S.subtype.congr_arg x.inv_mul + ((x⁻¹ : Sˣ) : M) * ((x : Sˣ) : M) = 1 := DFunLike.congr_arg S.subtype x.inv_mul @[to_additive] lemma coe_val_mul_coe_inv_val (S : Submonoid M) {x : Sˣ} : - ((x : Sˣ) : M) * ((x⁻¹ : Sˣ) : M) = 1 := S.subtype.congr_arg x.mul_inv + ((x : Sˣ) : M) * ((x⁻¹ : Sˣ) : M) = 1 := DFunLike.congr_arg S.subtype x.mul_inv @[to_additive] lemma mk_inv_mul_mk_eq_one (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units) : diff --git a/Mathlib/Algebra/GroupWithZero/Units/Basic.lean b/Mathlib/Algebra/GroupWithZero/Units/Basic.lean index 0cc69ff3a8732..5125c1cbbbac5 100644 --- a/Mathlib/Algebra/GroupWithZero/Units/Basic.lean +++ b/Mathlib/Algebra/GroupWithZero/Units/Basic.lean @@ -375,6 +375,7 @@ lemma div_eq_one_iff_eq (hb : b ≠ 0) : a / b = 1 ↔ a = b := hb.isUnit.div_eq lemma div_mul_cancel_right₀ (hb : b ≠ 0) (a : G₀) : b / (a * b) = a⁻¹ := hb.isUnit.div_mul_cancel_right _ +set_option linter.deprecated false in @[deprecated div_mul_cancel_right₀] -- 2024-03-20 lemma div_mul_left (hb : b ≠ 0) : b / (a * b) = 1 / a := hb.isUnit.div_mul_left #align div_mul_left div_mul_left @@ -441,6 +442,7 @@ instance (priority := 100) CommGroupWithZero.toDivisionCommMonoid : lemma div_mul_cancel_left₀ (ha : a ≠ 0) (b : G₀) : a / (a * b) = b⁻¹ := ha.isUnit.div_mul_cancel_left _ +set_option linter.deprecated false in @[deprecated div_mul_cancel_left₀] -- 2024-03-22 lemma div_mul_right (b : G₀) (ha : a ≠ 0) : a / (a * b) = 1 / b := ha.isUnit.div_mul_right _ #align div_mul_right div_mul_right diff --git a/Mathlib/AlgebraicGeometry/Pullbacks.lean b/Mathlib/AlgebraicGeometry/Pullbacks.lean index 60dd064391dfb..938258158822b 100644 --- a/Mathlib/AlgebraicGeometry/Pullbacks.lean +++ b/Mathlib/AlgebraicGeometry/Pullbacks.lean @@ -550,7 +550,7 @@ theorem hasPullback_of_cover : HasPullback f g := instance affine_hasPullback {A B C : CommRingCat} (f : Spec.obj (Opposite.op A) ⟶ Spec.obj (Opposite.op C)) (g : Spec.obj (Opposite.op B) ⟶ Spec.obj (Opposite.op C)) : HasPullback f g := by - rw [← Spec.image_preimage f, ← Spec.image_preimage g] + rw [← Spec.map_preimage f, ← Spec.map_preimage g] exact ⟨⟨⟨_, isLimitOfHasPullbackOfPreservesLimit Spec (Spec.preimage f) (Spec.preimage g)⟩⟩⟩ #align algebraic_geometry.Scheme.pullback.affine_has_pullback AlgebraicGeometry.Scheme.Pullback.affine_hasPullback diff --git a/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean b/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean index 2199904012cb0..1b129df80bd1a 100644 --- a/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean +++ b/Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean @@ -191,7 +191,7 @@ lemma whiskerLeft_toKaroubi_N₂Γ₂_hom : whiskerLeft (toKaroubi (ChainComplex C ℕ)) N₂Γ₂.hom = N₂Γ₂ToKaroubiIso.hom ≫ N₁Γ₀.hom := by let e : _ ≅ toKaroubi (ChainComplex C ℕ) ⋙ 𝟭 _ := N₂Γ₂ToKaroubiIso ≪≫ N₁Γ₀ have h := ((whiskeringLeft _ _ (Karoubi (ChainComplex C ℕ))).obj - (toKaroubi (ChainComplex C ℕ))).image_preimage e.hom + (toKaroubi (ChainComplex C ℕ))).map_preimage e.hom dsimp only [whiskeringLeft, N₂Γ₂, Functor.preimageIso] at h ⊢ exact h diff --git a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean index 08c46af2a81c0..a3fa496d55be6 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Basic.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Basic.lean @@ -250,8 +250,8 @@ theorem ContinuousLinearMap.iteratedFDerivWithin_comp_left {f : E → F} (g : F (hf : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {i : ℕ} (hi : (i : ℕ∞) ≤ n) : iteratedFDerivWithin 𝕜 i (g ∘ f) s x = g.compContinuousMultilinearMap (iteratedFDerivWithin 𝕜 i f s x) := - (((hf.ftaylorSeriesWithin hs).continuousLinearMap_comp g).eq_ftaylor_series_of_uniqueDiffOn hi hs - hx).symm + (((hf.ftaylorSeriesWithin hs).continuousLinearMap_comp g).eq_iteratedFDerivWithin_of_uniqueDiffOn + hi hs hx).symm #align continuous_linear_map.iterated_fderiv_within_comp_left ContinuousLinearMap.iteratedFDerivWithin_comp_left /-- The iterated derivative of the composition with a linear map on the left is @@ -416,8 +416,8 @@ theorem ContinuousLinearMap.iteratedFDerivWithin_comp_right {f : E → F} (g : G (hx : g x ∈ s) {i : ℕ} (hi : (i : ℕ∞) ≤ n) : iteratedFDerivWithin 𝕜 i (f ∘ g) (g ⁻¹' s) x = (iteratedFDerivWithin 𝕜 i f s (g x)).compContinuousLinearMap fun _ => g := - (((hf.ftaylorSeriesWithin hs).compContinuousLinearMap g).eq_ftaylor_series_of_uniqueDiffOn hi h's - hx).symm + (((hf.ftaylorSeriesWithin hs).compContinuousLinearMap g).eq_iteratedFDerivWithin_of_uniqueDiffOn + hi h's hx).symm #align continuous_linear_map.iterated_fderiv_within_comp_right ContinuousLinearMap.iteratedFDerivWithin_comp_right /-- The iterated derivative within a set of the composition with a linear equiv on the right is @@ -1304,7 +1304,7 @@ theorem iteratedFDerivWithin_add_apply {f g : E → F} (hf : ContDiffOn 𝕜 i f iteratedFDerivWithin 𝕜 i (f + g) s x = iteratedFDerivWithin 𝕜 i f s x + iteratedFDerivWithin 𝕜 i g s x := Eq.symm <| ((hf.ftaylorSeriesWithin hu).add - (hg.ftaylorSeriesWithin hu)).eq_ftaylor_series_of_uniqueDiffOn le_rfl hu hx + (hg.ftaylorSeriesWithin hu)).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl hu hx #align iterated_fderiv_within_add_apply iteratedFDerivWithin_add_apply /-- The iterated derivative of the sum of two functions is the sum of the iterated derivatives. diff --git a/Mathlib/Analysis/Calculus/ContDiff/Defs.lean b/Mathlib/Analysis/Calculus/ContDiff/Defs.lean index c5cd200530eab..73133a99cd043 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Defs.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Defs.lean @@ -1036,14 +1036,14 @@ protected theorem ContDiffOn.ftaylorSeriesWithin (h : ContDiffOn 𝕜 n f s) (hs have : p x m.succ = ftaylorSeriesWithin 𝕜 f s x m.succ := by change p x m.succ = iteratedFDerivWithin 𝕜 m.succ f s x rw [← iteratedFDerivWithin_inter_open o_open xo] - exact (Hp.mono ho).eq_ftaylor_series_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hx, xo⟩ + exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hx, xo⟩ rw [← this, ← hasFDerivWithinAt_inter (IsOpen.mem_nhds o_open xo)] have A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m := by rintro y ⟨hy, yo⟩ change p y m = iteratedFDerivWithin 𝕜 m f s y rw [← iteratedFDerivWithin_inter_open o_open yo] exact - (Hp.mono ho).eq_ftaylor_series_of_uniqueDiffOn (WithTop.coe_le_coe.2 (Nat.le_succ m)) + (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn (WithTop.coe_le_coe.2 (Nat.le_succ m)) (hs.inter o_open) ⟨hy, yo⟩ exact ((Hp.mono ho).fderivWithin m (WithTop.coe_lt_coe.2 (lt_add_one m)) x ⟨hx, xo⟩).congr @@ -1060,7 +1060,7 @@ protected theorem ContDiffOn.ftaylorSeriesWithin (h : ContDiffOn 𝕜 n f s) (hs rintro y ⟨hy, yo⟩ change p y m = iteratedFDerivWithin 𝕜 m f s y rw [← iteratedFDerivWithin_inter_open o_open yo] - exact (Hp.mono ho).eq_ftaylor_series_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hy, yo⟩ + exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hy, yo⟩ exact ((Hp.mono ho).cont m le_rfl).congr fun y hy => (A y hy).symm #align cont_diff_on.ftaylor_series_within ContDiffOn.ftaylorSeriesWithin diff --git a/Mathlib/Analysis/Calculus/Darboux.lean b/Mathlib/Analysis/Calculus/Darboux.lean index 9dbf2e7479411..728683cf11792 100644 --- a/Mathlib/Analysis/Calculus/Darboux.lean +++ b/Mathlib/Analysis/Calculus/Darboux.lean @@ -35,7 +35,7 @@ theorem exists_hasDerivWithinAt_eq_of_gt_of_lt (hab : a ≤ b) intro x hx simpa using (hf x hx).sub ((hasDerivWithinAt_id x _).const_mul m) obtain ⟨c, cmem, hc⟩ : ∃ c ∈ Icc a b, IsMinOn g (Icc a b) c := - isCompact_Icc.exists_forall_le (nonempty_Icc.2 <| hab) fun x hx => (hg x hx).continuousWithinAt + isCompact_Icc.exists_isMinOn (nonempty_Icc.2 <| hab) fun x hx => (hg x hx).continuousWithinAt have cmem' : c ∈ Ioo a b := by rcases cmem.1.eq_or_lt with (rfl | hac) -- Show that `c` can't be equal to `a` diff --git a/Mathlib/Analysis/Complex/AbsMax.lean b/Mathlib/Analysis/Complex/AbsMax.lean index f72aca855c3a3..faaee5d29fc46 100644 --- a/Mathlib/Analysis/Complex/AbsMax.lean +++ b/Mathlib/Analysis/Complex/AbsMax.lean @@ -371,7 +371,7 @@ theorem exists_mem_frontier_isMaxOn_norm [FiniteDimensional ℂ E] {f : E → F} ∃ z ∈ frontier U, IsMaxOn (norm ∘ f) (closure U) z := by have hc : IsCompact (closure U) := hb.isCompact_closure obtain ⟨w, hwU, hle⟩ : ∃ w ∈ closure U, IsMaxOn (norm ∘ f) (closure U) w := - hc.exists_forall_ge hne.closure hd.continuousOn.norm + hc.exists_isMaxOn hne.closure hd.continuousOn.norm rw [closure_eq_interior_union_frontier, mem_union] at hwU cases' hwU with hwU hwU; rotate_left; · exact ⟨w, hwU, hle⟩ have : interior U ≠ univ := ne_top_of_le_ne_top hc.ne_univ interior_subset_closure diff --git a/Mathlib/Analysis/Complex/LocallyUniformLimit.lean b/Mathlib/Analysis/Complex/LocallyUniformLimit.lean index 4b16c0b5ae4dc..0979b0dd21cd6 100644 --- a/Mathlib/Analysis/Complex/LocallyUniformLimit.lean +++ b/Mathlib/Analysis/Complex/LocallyUniformLimit.lean @@ -81,7 +81,7 @@ theorem norm_cderiv_lt (hr : 0 < r) (hfM : ∀ w ∈ sphere z r, ‖f w‖ < M) obtain ⟨L, hL1, hL2⟩ : ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L := by have e1 : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le have e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r) := continuous_norm.comp_continuousOn hf - obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_forall_ge e1 e2 + obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_isMaxOn e1 e2 exact ⟨‖f x‖, hfM x hx, hx'⟩ exact (norm_cderiv_le hr hL2).trans_lt ((div_lt_div_right hr).mpr hL1) #align complex.norm_cderiv_lt Complex.norm_cderiv_lt diff --git a/Mathlib/Analysis/Complex/OpenMapping.lean b/Mathlib/Analysis/Complex/OpenMapping.lean index 74c43bfa7ebcd..6e7a5cc3cb48f 100644 --- a/Mathlib/Analysis/Complex/OpenMapping.lean +++ b/Mathlib/Analysis/Complex/OpenMapping.lean @@ -100,9 +100,9 @@ theorem AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux (hf : AnalyticAt have h8 : (sphere z₀ r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le have h9 : ContinuousOn (fun x => ‖f x - f z₀‖) (sphere z₀ r) := continuous_norm.comp_continuousOn ((h6.sub_const (f z₀)).continuousOn_ball.mono sphere_subset_closedBall) - obtain ⟨x, hx, hfx⟩ := (isCompact_sphere z₀ r).exists_forall_le h8 h9 + obtain ⟨x, hx, hfx⟩ := (isCompact_sphere z₀ r).exists_isMinOn h8 h9 refine ⟨‖f x - f z₀‖ / 2, half_pos (norm_sub_pos_iff.mpr (h7 x hx)), ?_⟩ - exact (h6.ball_subset_image_closedBall hr (fun z hz => hfx z hz) (not_eventually.mp h)).trans + exact (h6.ball_subset_image_closedBall hr (fun z hz => hfx hz) (not_eventually.mp h)).trans (image_subset f (closedBall_subset_closedBall inf_le_right)) #align analytic_at.eventually_constant_or_nhds_le_map_nhds_aux AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux diff --git a/Mathlib/Analysis/Complex/PhragmenLindelof.lean b/Mathlib/Analysis/Complex/PhragmenLindelof.lean index 6c136ca454d19..e0941b88b8f74 100644 --- a/Mathlib/Analysis/Complex/PhragmenLindelof.lean +++ b/Mathlib/Analysis/Complex/PhragmenLindelof.lean @@ -709,7 +709,7 @@ theorem right_half_plane_of_tendsto_zero_on_real (hd : DiffContOnCl ℂ f {z | 0 rcases h₀ with ⟨x₀, hx₀, hne⟩ have hlt : ‖(0 : E)‖ < ‖f x₀‖ := by rwa [norm_zero, norm_pos_iff] suffices ∀ᶠ x : ℝ in cocompact ℝ ⊓ 𝓟 (Ici 0), ‖f x‖ ≤ ‖f x₀‖ by - simpa only [exists_prop] using hfc.norm.exists_forall_ge' isClosed_Ici hx₀ this + simpa only [exists_prop] using hfc.norm.exists_isMaxOn' isClosed_Ici hx₀ this rw [cocompact_eq_atBot_atTop, inf_sup_right, (disjoint_atBot_principal_Ici (0 : ℝ)).eq_bot, bot_sup_eq] exact (hre.norm.eventually <| ge_mem_nhds hlt).filter_mono inf_le_left diff --git a/Mathlib/Analysis/Convex/Gauge.lean b/Mathlib/Analysis/Convex/Gauge.lean index 2987e2c9d1500..09cc83ae21ae7 100644 --- a/Mathlib/Analysis/Convex/Gauge.lean +++ b/Mathlib/Analysis/Convex/Gauge.lean @@ -609,7 +609,7 @@ theorem gauge_closedBall (hr : 0 ≤ r) (x : E) : gauge (closedBall (0 : E) r) x filter_upwards [self_mem_nhdsWithin] with R hR rw [← gauge_ball (hr.trans hR.out.le)] refine gauge_mono ?_ (closedBall_subset_ball hR) _ - exact (absorbent_ball_zero hr').subset ball_subset_closedBall + exact (absorbent_ball_zero hr').mono ball_subset_closedBall theorem mul_gauge_le_norm (hs : Metric.ball (0 : E) r ⊆ s) : r * gauge s x ≤ ‖x‖ := by obtain hr | hr := le_or_lt r 0 @@ -624,7 +624,7 @@ theorem Convex.lipschitzWith_gauge {r : ℝ≥0} (hc : Convex ℝ s) (hr : 0 < r LipschitzWith.of_le_add_mul _ fun x y => calc gauge s x = gauge s (y + (x - y)) := by simp - _ ≤ gauge s y + gauge s (x - y) := gauge_add_le hc (this.subset hs) _ _ + _ ≤ gauge s y + gauge s (x - y) := gauge_add_le hc (this.mono hs) _ _ _ ≤ gauge s y + ‖x - y‖ / r := add_le_add_left ((gauge_mono this hs (x - y)).trans_eq (gauge_ball hr.le _)) _ _ = gauge s y + r⁻¹ * dist x y := by rw [dist_eq_norm, div_eq_inv_mul, NNReal.coe_inv] diff --git a/Mathlib/Analysis/Convex/KreinMilman.lean b/Mathlib/Analysis/Convex/KreinMilman.lean index 3c8d0a4cab7a4..551032d8bda83 100644 --- a/Mathlib/Analysis/Convex/KreinMilman.lean +++ b/Mathlib/Analysis/Convex/KreinMilman.lean @@ -69,7 +69,7 @@ theorem IsCompact.extremePoints_nonempty (hscomp : IsCompact s) (hsnemp : s.None by_contra hyx obtain ⟨l, hl⟩ := geometric_hahn_banach_point_point hyx obtain ⟨z, hzt, hz⟩ := - (hscomp.of_isClosed_subset htclos hst.1).exists_forall_ge ⟨x, hxt⟩ + (hscomp.of_isClosed_subset htclos hst.1).exists_isMaxOn ⟨x, hxt⟩ l.continuous.continuousOn have h : IsExposed ℝ t ({ z ∈ t | ∀ w ∈ t, l w ≤ l z }) := fun _ => ⟨l, rfl⟩ rw [← hBmin ({ z ∈ t | ∀ w ∈ t, l w ≤ l z }) @@ -100,7 +100,7 @@ theorem closure_convexHull_extremePoints (hscomp : IsCompact s) (hAconv : Convex obtain ⟨l, r, hlr, hrx⟩ := geometric_hahn_banach_closed_point (convex_convexHull _ _).closure isClosed_closure hxt have h : IsExposed ℝ s ({ y ∈ s | ∀ z ∈ s, l z ≤ l y }) := fun _ => ⟨l, rfl⟩ - obtain ⟨z, hzA, hz⟩ := hscomp.exists_forall_ge ⟨x, hxA⟩ l.continuous.continuousOn + obtain ⟨z, hzA, hz⟩ := hscomp.exists_isMaxOn ⟨x, hxA⟩ l.continuous.continuousOn obtain ⟨y, hy⟩ := (h.isCompact hscomp).extremePoints_nonempty ⟨z, hzA, hz⟩ linarith [hlr _ (subset_closure <| subset_convexHull _ _ <| h.isExtreme.extremePoints_subset_extremePoints hy), hy.1.2 x hxA] diff --git a/Mathlib/Analysis/Convolution.lean b/Mathlib/Analysis/Convolution.lean index 25c6a6d22b838..430c3b34d436f 100644 --- a/Mathlib/Analysis/Convolution.lean +++ b/Mathlib/Analysis/Convolution.lean @@ -256,13 +256,13 @@ theorem AEStronglyMeasurable.convolution_integrand_snd (hf : AEStronglyMeasurabl (hg : AEStronglyMeasurable g μ) (x : G) : AEStronglyMeasurable (fun t => L (f t) (g (x - t))) μ := hf.convolution_integrand_snd' L <| - hg.mono' <| (quasiMeasurePreserving_sub_left_of_right_invariant μ x).absolutelyContinuous + hg.mono_ac <| (quasiMeasurePreserving_sub_left_of_right_invariant μ x).absolutelyContinuous #align measure_theory.ae_strongly_measurable.convolution_integrand_snd MeasureTheory.AEStronglyMeasurable.convolution_integrand_snd theorem AEStronglyMeasurable.convolution_integrand_swap_snd (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) (x : G) : AEStronglyMeasurable (fun t => L (f (x - t)) (g t)) μ := - (hf.mono' + (hf.mono_ac (quasiMeasurePreserving_sub_left_of_right_invariant μ x).absolutelyContinuous).convolution_integrand_swap_snd' L hg @@ -274,7 +274,7 @@ theorem ConvolutionExistsAt.ofNorm {x₀ : G} (hmf : AEStronglyMeasurable f μ) (hmg : AEStronglyMeasurable g μ) : ConvolutionExistsAt f g x₀ L μ := h.ofNorm' L hmf <| - hmg.mono' (quasiMeasurePreserving_sub_left_of_right_invariant μ x₀).absolutelyContinuous + hmg.mono_ac (quasiMeasurePreserving_sub_left_of_right_invariant μ x₀).absolutelyContinuous #align convolution_exists_at.of_norm MeasureTheory.ConvolutionExistsAt.ofNorm end Left @@ -288,7 +288,7 @@ theorem AEStronglyMeasurable.convolution_integrand (hf : AEStronglyMeasurable f (hg : AEStronglyMeasurable g μ) : AEStronglyMeasurable (fun p : G × G => L (f p.2) (g (p.1 - p.2))) (μ.prod ν) := hf.convolution_integrand' L <| - hg.mono' (quasiMeasurePreserving_sub_of_right_invariant μ ν).absolutelyContinuous + hg.mono_ac (quasiMeasurePreserving_sub_of_right_invariant μ ν).absolutelyContinuous #align measure_theory.ae_strongly_measurable.convolution_integrand MeasureTheory.AEStronglyMeasurable.convolution_integrand theorem Integrable.convolution_integrand (hf : Integrable f ν) (hg : Integrable g μ) : @@ -383,7 +383,7 @@ theorem _root_.BddAbove.convolutionExistsAt [MeasurableAdd₂ G] [SigmaFinite μ refine' BddAbove.convolutionExistsAt' L _ hs h2s hf _ · simp_rw [← sub_eq_neg_add, hbg] · have : AEStronglyMeasurable g (map (fun t : G => x₀ - t) μ) := - hmg.mono' (quasiMeasurePreserving_sub_left_of_right_invariant μ x₀).absolutelyContinuous + hmg.mono_ac (quasiMeasurePreserving_sub_left_of_right_invariant μ x₀).absolutelyContinuous apply this.mono_measure exact map_mono restrict_le_self (measurable_const.sub measurable_id') #align bdd_above.convolution_exists_at BddAbove.convolutionExistsAt @@ -968,7 +968,8 @@ theorem convolution_assoc (hL : ∀ (x : E) (y : E') (z : E''), L₂ (L x y) z = (μ.prod ν) := by refine' L₃.aestronglyMeasurable_comp₂ hf.snd _ refine' L₄.aestronglyMeasurable_comp₂ hg.fst _ - refine' (hk.mono' _).comp_measurable ((measurable_const.sub measurable_snd).sub measurable_fst) + refine' (hk.mono_ac _).comp_measurable + ((measurable_const.sub measurable_snd).sub measurable_fst) refine' QuasiMeasurePreserving.absolutelyContinuous _ refine' QuasiMeasurePreserving.prod_of_left ((measurable_const.sub measurable_snd).sub measurable_fst) (eventually_of_forall fun y => _) diff --git a/Mathlib/Analysis/Distribution/SchwartzSpace.lean b/Mathlib/Analysis/Distribution/SchwartzSpace.lean index 03266bd2403e6..5f251ff7d496f 100644 --- a/Mathlib/Analysis/Distribution/SchwartzSpace.lean +++ b/Mathlib/Analysis/Distribution/SchwartzSpace.lean @@ -655,7 +655,7 @@ lemma _root_.ContinuousLinearMap.hasTemperateGrowth (f : E →L[ℝ] F) : apply Function.HasTemperateGrowth.of_fderiv ?_ f.differentiable (k := 1) (C := ‖f‖) (fun x ↦ ?_) · have : fderiv ℝ f = fun _ ↦ f := by ext1 v; simp only [ContinuousLinearMap.fderiv] simpa [this] using .const _ - · exact (f.le_op_norm x).trans (by simp [mul_add]) + · exact (f.le_opNorm x).trans (by simp [mul_add]) variable [NormedAddCommGroup D] [NormedSpace ℝ D] variable [MeasurableSpace D] [BorelSpace D] [SecondCountableTopology D] [FiniteDimensional ℝ D] diff --git a/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean b/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean index 73535314f7688..bf25b941f24f8 100644 --- a/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean +++ b/Mathlib/Analysis/InnerProductSpace/Rayleigh.lean @@ -248,7 +248,7 @@ theorem hasEigenvalue_iSup_of_finiteDimensional (hT : T.IsSymmetric) : have H₂ : (sphere (0 : E) ‖x‖).Nonempty := ⟨x, by simp⟩ -- key point: in finite dimension, a continuous function on the sphere has a max obtain ⟨x₀, hx₀', hTx₀⟩ := - H₁.exists_forall_ge H₂ T'.val.reApplyInnerSelf_continuous.continuousOn + H₁.exists_isMaxOn H₂ T'.val.reApplyInnerSelf_continuous.continuousOn have hx₀ : ‖x₀‖ = ‖x‖ := by simpa using hx₀' have : IsMaxOn T'.val.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀ := by simpa only [← hx₀] using hTx₀ have hx₀_ne : x₀ ≠ 0 := by @@ -268,7 +268,7 @@ theorem hasEigenvalue_iInf_of_finiteDimensional (hT : T.IsSymmetric) : have H₂ : (sphere (0 : E) ‖x‖).Nonempty := ⟨x, by simp⟩ -- key point: in finite dimension, a continuous function on the sphere has a min obtain ⟨x₀, hx₀', hTx₀⟩ := - H₁.exists_forall_le H₂ T'.val.reApplyInnerSelf_continuous.continuousOn + H₁.exists_isMinOn H₂ T'.val.reApplyInnerSelf_continuous.continuousOn have hx₀ : ‖x₀‖ = ‖x‖ := by simpa using hx₀' have : IsMinOn T'.val.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀ := by simpa only [← hx₀] using hTx₀ have hx₀_ne : x₀ ≠ 0 := by diff --git a/Mathlib/Analysis/NormedSpace/FiniteDimension.lean b/Mathlib/Analysis/NormedSpace/FiniteDimension.lean index ebee3f70a8cf9..38fd38c9c5392 100644 --- a/Mathlib/Analysis/NormedSpace/FiniteDimension.lean +++ b/Mathlib/Analysis/NormedSpace/FiniteDimension.lean @@ -299,7 +299,7 @@ theorem Basis.opNNNorm_le {ι : Type*} [Fintype ι] (v : Basis ι 𝕜 E) {u : E set φ := v.equivFunL.toContinuousLinearMap calc ‖u e‖₊ = ‖u (∑ i, v.equivFun e i • v i)‖₊ := by rw [v.sum_equivFun] - _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp [u.map_sum, LinearMap.map_smul] + _ = ‖∑ i, v.equivFun e i • (u <| v i)‖₊ := by simp [map_sum, LinearMap.map_smul] _ ≤ ∑ i, ‖v.equivFun e i • (u <| v i)‖₊ := nnnorm_sum_le _ _ _ = ∑ i, ‖v.equivFun e i‖₊ * ‖u (v i)‖₊ := by simp only [nnnorm_smul] _ ≤ ∑ i, ‖v.equivFun e i‖₊ * M := by gcongr; apply hu diff --git a/Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean b/Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean index 6bd45c3b2ace0..4da5ec28f5b95 100644 --- a/Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean +++ b/Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean @@ -159,11 +159,13 @@ theorem geometric_hahn_banach_compact_closed (hs₁ : Convex ℝ s) (hs₂ : IsC · exact ⟨0, 1, 2, fun a _ha => by norm_num, by norm_num, by simp⟩ obtain ⟨U, V, hU, hV, hU₁, hV₁, sU, tV, disj'⟩ := disj.exists_open_convexes hs₁ hs₂ ht₁ ht₂ obtain ⟨f, u, hf₁, hf₂⟩ := geometric_hahn_banach_open_open hU₁ hU hV₁ hV disj' - obtain ⟨x, hx₁, hx₂⟩ := hs₂.exists_forall_ge hs f.continuous.continuousOn + obtain ⟨x, hx₁, hx₂⟩ := hs₂.exists_isMaxOn hs f.continuous.continuousOn have : f x < u := hf₁ x (sU hx₁) exact - ⟨f, (f x + u) / 2, u, fun a ha => by linarith [hx₂ a ha], by linarith, fun b hb => - hf₂ b (tV hb)⟩ + ⟨f, (f x + u) / 2, u, + fun a ha => by have := hx₂ ha; dsimp at this; linarith, + by linarith, + fun b hb => hf₂ b (tV hb)⟩ #align geometric_hahn_banach_compact_closed geometric_hahn_banach_compact_closed /-- A version of the **Hahn-Banach theorem**: given disjoint convex sets `s`, `t` where `s` is diff --git a/Mathlib/Analysis/NormedSpace/Spectrum.lean b/Mathlib/Analysis/NormedSpace/Spectrum.lean index 8b495d9258443..0b1c6b19c56f1 100644 --- a/Mathlib/Analysis/NormedSpace/Spectrum.lean +++ b/Mathlib/Analysis/NormedSpace/Spectrum.lean @@ -156,7 +156,7 @@ theorem spectralRadius_le_nnnorm [NormOneClass A] (a : A) : spectralRadius 𝕜 theorem exists_nnnorm_eq_spectralRadius_of_nonempty [ProperSpace 𝕜] {a : A} (ha : (σ a).Nonempty) : ∃ k ∈ σ a, (‖k‖₊ : ℝ≥0∞) = spectralRadius 𝕜 a := by - obtain ⟨k, hk, h⟩ := (spectrum.isCompact a).exists_forall_ge ha continuous_nnnorm.continuousOn + obtain ⟨k, hk, h⟩ := (spectrum.isCompact a).exists_isMaxOn ha continuous_nnnorm.continuousOn exact ⟨k, hk, le_antisymm (le_iSup₂ (α := ℝ≥0∞) k hk) (iSup₂_le <| mod_cast h)⟩ #align spectrum.exists_nnnorm_eq_spectral_radius_of_nonempty spectrum.exists_nnnorm_eq_spectralRadius_of_nonempty diff --git a/Mathlib/Analysis/Seminorm.lean b/Mathlib/Analysis/Seminorm.lean index d4a529b5d3f83..04f163f4ddd60 100644 --- a/Mathlib/Analysis/Seminorm.lean +++ b/Mathlib/Analysis/Seminorm.lean @@ -1039,19 +1039,19 @@ protected theorem absorbent_ball_zero (hr : 0 < r) : Absorbent 𝕜 (ball p (0 : /-- Closed seminorm-balls at the origin are absorbent. -/ protected theorem absorbent_closedBall_zero (hr : 0 < r) : Absorbent 𝕜 (closedBall p (0 : E) r) := - (p.absorbent_ball_zero hr).subset (p.ball_subset_closedBall _ _) + (p.absorbent_ball_zero hr).mono (p.ball_subset_closedBall _ _) #align seminorm.absorbent_closed_ball_zero Seminorm.absorbent_closedBall_zero /-- Seminorm-balls containing the origin are absorbent. -/ protected theorem absorbent_ball (hpr : p x < r) : Absorbent 𝕜 (ball p x r) := by - refine' (p.absorbent_ball_zero <| sub_pos.2 hpr).subset fun y hy => _ + refine' (p.absorbent_ball_zero <| sub_pos.2 hpr).mono fun y hy => _ rw [p.mem_ball_zero] at hy exact p.mem_ball.2 ((map_sub_le_add p _ _).trans_lt <| add_lt_of_lt_sub_right hy) #align seminorm.absorbent_ball Seminorm.absorbent_ball /-- Seminorm-balls containing the origin are absorbent. -/ protected theorem absorbent_closedBall (hpr : p x < r) : Absorbent 𝕜 (closedBall p x r) := by - refine' (p.absorbent_closedBall_zero <| sub_pos.2 hpr).subset fun y hy => _ + refine' (p.absorbent_closedBall_zero <| sub_pos.2 hpr).mono fun y hy => _ rw [p.mem_closedBall_zero] at hy exact p.mem_closedBall.2 ((map_sub_le_add p _ _).trans <| add_le_of_le_sub_right hy) #align seminorm.absorbent_closed_ball Seminorm.absorbent_closedBall diff --git a/Mathlib/CategoryTheory/Comma/StructuredArrow.lean b/Mathlib/CategoryTheory/Comma/StructuredArrow.lean index 8fd6a313f1491..e3b3defc53be6 100644 --- a/Mathlib/CategoryTheory/Comma/StructuredArrow.lean +++ b/Mathlib/CategoryTheory/Comma/StructuredArrow.lean @@ -281,7 +281,7 @@ noncomputable def mkIdInitial [T.Full] [T.Faithful] : IsInitial (mk (𝟙 (T.obj apply CommaMorphism.ext · aesop_cat · apply T.map_injective - simpa only [homMk_right, T.image_preimage, ← w m] using (Category.id_comp _).symm + simpa only [homMk_right, T.map_preimage, ← w m] using (Category.id_comp _).symm #align category_theory.structured_arrow.mk_id_initial CategoryTheory.StructuredArrow.mkIdInitial variable {A : Type u₃} [Category.{v₃} A] {B : Type u₄} [Category.{v₄} B] @@ -645,7 +645,7 @@ noncomputable def mkIdTerminal [S.Full] [S.Faithful] : IsTerminal (mk (𝟙 (S.o rintro c m - ext apply S.map_injective - simpa only [homMk_left, S.image_preimage, ← w m] using (Category.comp_id _).symm + simpa only [homMk_left, S.map_preimage, ← w m] using (Category.comp_id _).symm #align category_theory.costructured_arrow.mk_id_terminal CategoryTheory.CostructuredArrow.mkIdTerminal variable {A : Type u₃} [Category.{v₃} A] {B : Type u₄} [Category.{v₄} B] diff --git a/Mathlib/CategoryTheory/Monoidal/Discrete.lean b/Mathlib/CategoryTheory/Monoidal/Discrete.lean index 641d322d3126d..b3920af26f985 100644 --- a/Mathlib/CategoryTheory/Monoidal/Discrete.lean +++ b/Mathlib/CategoryTheory/Monoidal/Discrete.lean @@ -51,7 +51,7 @@ discrete monoidal categories. def Discrete.monoidalFunctor (F : M →* N) : MonoidalFunctor (Discrete M) (Discrete N) where obj X := Discrete.mk (F X.as) - map f := Discrete.eqToHom (F.congr_arg (eq_of_hom f)) + map f := Discrete.eqToHom (DFunLike.congr_arg F (eq_of_hom f)) ε := Discrete.eqToHom F.map_one.symm μ X Y := Discrete.eqToHom (F.map_mul X.as Y.as).symm #align category_theory.discrete.monoidal_functor CategoryTheory.Discrete.monoidalFunctor diff --git a/Mathlib/Data/Finset/Sort.lean b/Mathlib/Data/Finset/Sort.lean index 5630aedf19407..192127da3295e 100644 --- a/Mathlib/Data/Finset/Sort.lean +++ b/Mathlib/Data/Finset/Sort.lean @@ -95,30 +95,30 @@ theorem sort_sorted_gt (s : Finset α) : List.Sorted (· > ·) (sort (· ≥ ·) (sort_sorted _ _).gt_of_ge (sort_nodup _ _) theorem sorted_zero_eq_min'_aux (s : Finset α) (h : 0 < (s.sort (· ≤ ·)).length) (H : s.Nonempty) : - (s.sort (· ≤ ·)).nthLe 0 h = s.min' H := by + (s.sort (· ≤ ·)).get ⟨0, h⟩ = s.min' H := by let l := s.sort (· ≤ ·) apply le_antisymm · have : s.min' H ∈ l := (Finset.mem_sort (α := α) (· ≤ ·)).mpr (s.min'_mem H) obtain ⟨i, hi⟩ : ∃ i, l.get i = s.min' H := List.mem_iff_get.1 this rw [← hi] - exact (s.sort_sorted (· ≤ ·)).rel_nthLe_of_le _ _ (Nat.zero_le i) + exact (s.sort_sorted (· ≤ ·)).rel_get_of_le (Nat.zero_le i) · have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l 0 h) exact s.min'_le _ this #align finset.sorted_zero_eq_min'_aux Finset.sorted_zero_eq_min'_aux theorem sorted_zero_eq_min' {s : Finset α} {h : 0 < (s.sort (· ≤ ·)).length} : - (s.sort (· ≤ ·)).nthLe 0 h = s.min' (card_pos.1 <| by rwa [length_sort] at h) := + (s.sort (· ≤ ·)).get ⟨0, h⟩ = s.min' (card_pos.1 <| by rwa [length_sort] at h) := sorted_zero_eq_min'_aux _ _ _ #align finset.sorted_zero_eq_min' Finset.sorted_zero_eq_min' theorem min'_eq_sorted_zero {s : Finset α} {h : s.Nonempty} : - s.min' h = (s.sort (· ≤ ·)).nthLe 0 (by rw [length_sort]; exact card_pos.2 h) := + s.min' h = (s.sort (· ≤ ·)).get ⟨0, (by rw [length_sort]; exact card_pos.2 h)⟩ := (sorted_zero_eq_min'_aux _ _ _).symm #align finset.min'_eq_sorted_zero Finset.min'_eq_sorted_zero theorem sorted_last_eq_max'_aux (s : Finset α) (h : (s.sort (· ≤ ·)).length - 1 < (s.sort (· ≤ ·)).length) (H : s.Nonempty) : - (s.sort (· ≤ ·)).nthLe ((s.sort (· ≤ ·)).length - 1) h = s.max' H := by + (s.sort (· ≤ ·)).get ⟨(s.sort (· ≤ ·)).length - 1, h⟩ = s.max' H := by let l := s.sort (· ≤ ·) apply le_antisymm · have : l.get ⟨(s.sort (· ≤ ·)).length - 1, h⟩ ∈ s := @@ -127,20 +127,20 @@ theorem sorted_last_eq_max'_aux (s : Finset α) · have : s.max' H ∈ l := (Finset.mem_sort (α := α) (· ≤ ·)).mpr (s.max'_mem H) obtain ⟨i, hi⟩ : ∃ i, l.get i = s.max' H := List.mem_iff_get.1 this rw [← hi] - exact (s.sort_sorted (· ≤ ·)).rel_nthLe_of_le _ _ (Nat.le_sub_one_of_lt i.prop) + exact (s.sort_sorted (· ≤ ·)).rel_get_of_le (Nat.le_sub_one_of_lt i.prop) #align finset.sorted_last_eq_max'_aux Finset.sorted_last_eq_max'_aux theorem sorted_last_eq_max' {s : Finset α} {h : (s.sort (· ≤ ·)).length - 1 < (s.sort (· ≤ ·)).length} : - (s.sort (· ≤ ·)).nthLe ((s.sort (· ≤ ·)).length - 1) h = + (s.sort (· ≤ ·)).get ⟨(s.sort (· ≤ ·)).length - 1, h⟩ = s.max' (by rw [length_sort] at h; exact card_pos.1 (lt_of_le_of_lt bot_le h)) := sorted_last_eq_max'_aux _ _ _ #align finset.sorted_last_eq_max' Finset.sorted_last_eq_max' theorem max'_eq_sorted_last {s : Finset α} {h : s.Nonempty} : s.max' h = - (s.sort (· ≤ ·)).nthLe ((s.sort (· ≤ ·)).length - 1) - (by simpa using Nat.sub_lt (card_pos.mpr h) zero_lt_one) := + (s.sort (· ≤ ·)).get ⟨(s.sort (· ≤ ·)).length - 1, + by simpa using Nat.sub_lt (card_pos.mpr h) zero_lt_one⟩ := (sorted_last_eq_max'_aux _ _ _).symm #align finset.max'_eq_sorted_last Finset.max'_eq_sorted_last @@ -174,7 +174,7 @@ theorem orderIsoOfFin_symm_apply (s : Finset α) {k : ℕ} (h : s.card = k) (x : theorem orderEmbOfFin_apply (s : Finset α) {k : ℕ} (h : s.card = k) (i : Fin k) : s.orderEmbOfFin h i = - (s.sort (· ≤ ·)).nthLe i (by rw [length_sort, h]; exact i.2) := + (s.sort (· ≤ ·)).get ⟨i, by rw [length_sort, h]; exact i.2⟩ := rfl #align finset.order_emb_of_fin_apply Finset.orderEmbOfFin_apply diff --git a/Mathlib/Data/Finsupp/Basic.lean b/Mathlib/Data/Finsupp/Basic.lean index 832b4e69a179c..d394b5dcb2069 100644 --- a/Mathlib/Data/Finsupp/Basic.lean +++ b/Mathlib/Data/Finsupp/Basic.lean @@ -538,7 +538,7 @@ theorem mapDomain_finset_sum {f : α → β} {s : Finset ι} {v : ι → α → theorem mapDomain_sum [Zero N] {f : α → β} {s : α →₀ N} {v : α → N → α →₀ M} : mapDomain f (s.sum v) = s.sum fun a b => mapDomain f (v a b) := - (mapDomain.addMonoidHom f : (α →₀ M) →+ β →₀ M).map_finsupp_sum _ _ + map_finsupp_sum (mapDomain.addMonoidHom f : (α →₀ M) →+ β →₀ M) _ _ #align finsupp.map_domain_sum Finsupp.mapDomain_sum theorem mapDomain_support [DecidableEq β] {f : α → β} {s : α →₀ M} : diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 22eb8d4054b1d..ad7740ee54045 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -2949,6 +2949,8 @@ theorem span_eq_take_drop (l : List α) : span p l = (takeWhile p l, dropWhile p #align list.take_while_append_drop List.takeWhile_append_dropWhile +-- TODO update to use `get` instead of `nthLe` +set_option linter.deprecated false in theorem dropWhile_nthLe_zero_not (l : List α) (hl : 0 < (l.dropWhile p).length) : ¬p ((l.dropWhile p).nthLe 0 hl) := by induction' l with hd tl IH @@ -2994,6 +2996,8 @@ theorem takeWhile_eq_self_iff : takeWhile p l = l ↔ ∀ x ∈ l, p x := by · by_cases hp : p x <;> simp [hp, takeWhile_cons, IH] #align list.take_while_eq_self_iff List.takeWhile_eq_self_iff +-- TODO update to use `get` instead of `nthLe` +set_option linter.deprecated false in @[simp] theorem takeWhile_eq_nil_iff : takeWhile p l = [] ↔ ∀ hl : 0 < l.length, ¬p (l.nthLe 0 hl) := by induction' l with x xs IH diff --git a/Mathlib/Data/List/DropRight.lean b/Mathlib/Data/List/DropRight.lean index af4e4af4df329..d6ff682d0a3c2 100644 --- a/Mathlib/Data/List/DropRight.lean +++ b/Mathlib/Data/List/DropRight.lean @@ -141,7 +141,7 @@ theorem rdropWhile_eq_nil_iff : rdropWhile p l = [] ↔ ∀ x ∈ l, p x := by s -- it is in this file because it requires `List.Infix` @[simp] -theorem dropWhile_eq_self_iff : dropWhile p l = l ↔ ∀ hl : 0 < l.length, ¬p (l.nthLe 0 hl) := by +theorem dropWhile_eq_self_iff : dropWhile p l = l ↔ ∀ hl : 0 < l.length, ¬p (l.get ⟨0, hl⟩) := by cases' l with hd tl · simp only [dropWhile, true_iff] intro h @@ -150,13 +150,13 @@ theorem dropWhile_eq_self_iff : dropWhile p l = l ↔ ∀ hl : 0 < l.length, ¬p · rw [dropWhile] refine' ⟨fun h => _, fun h => _⟩ · intro _ H - rw [nthLe, get] at H + rw [get] at H refine' (cons_ne_self hd tl) (Sublist.antisymm _ (sublist_cons _ _)) rw [← h] simp only [H] exact List.IsSuffix.sublist (dropWhile_suffix p) · have := h (by simp only [length, Nat.succ_pos]) - rw [nthLe, get] at this + rw [get] at this simp_rw [this] #align list.drop_while_eq_self_iff List.dropWhile_eq_self_iff @@ -168,10 +168,10 @@ theorem rdropWhile_eq_self_iff : rdropWhile p l = l ↔ ∀ hl : l ≠ [], ¬p ( refine' ⟨fun h hl => _, fun h hl => _⟩ · rw [← length_pos, ← length_reverse] at hl have := h hl - rwa [nthLe, get_reverse'] at this + rwa [get_reverse'] at this · rw [length_reverse, length_pos] at hl have := h hl - rwa [nthLe, get_reverse'] + rwa [get_reverse'] #align list.rdrop_while_eq_self_iff List.rdropWhile_eq_self_iff variable (p) (l) diff --git a/Mathlib/Data/List/Forall2.lean b/Mathlib/Data/List/Forall2.lean index 9b6a5ddd36f3d..492b6d05737e8 100644 --- a/Mathlib/Data/List/Forall2.lean +++ b/Mathlib/Data/List/Forall2.lean @@ -162,6 +162,7 @@ theorem Forall₂.get : | _, _, Forall₂.cons ha _, 0, _, _ => ha | _, _, Forall₂.cons _ hl, succ _, _, _ => hl.get _ _ +set_option linter.deprecated false in @[deprecated (since := "2024-05-05")] theorem Forall₂.nthLe {x y} (h : Forall₂ R x y) ⦃i : ℕ⦄ (hx : i < x.length) (hy : i < y.length) : R (x.nthLe i hx) (y.nthLe i hy) := h.get hx hy #align list.forall₂.nth_le List.Forall₂.nthLe @@ -175,6 +176,7 @@ theorem forall₂_of_length_eq_of_get : (forall₂_of_length_eq_of_get (succ.inj hl) fun i h₁ h₂ => h i.succ (succ_lt_succ h₁) (succ_lt_succ h₂)) +set_option linter.deprecated false in @[deprecated (since := "2024-05-05")] theorem forall₂_of_length_eq_of_nthLe {x y} (H : x.length = y.length) (H' : ∀ i h₁ h₂, R (x.nthLe i h₁) (y.nthLe i h₂)) : Forall₂ R x y := forall₂_of_length_eq_of_get H H' @@ -184,6 +186,7 @@ theorem forall₂_iff_get {l₁ : List α} {l₂ : List β} : Forall₂ R l₁ l₂ ↔ l₁.length = l₂.length ∧ ∀ i h₁ h₂, R (l₁.get ⟨i, h₁⟩) (l₂.get ⟨i, h₂⟩) := ⟨fun h => ⟨h.length_eq, h.get⟩, fun h => forall₂_of_length_eq_of_get h.1 h.2⟩ +set_option linter.deprecated false in @[deprecated (since := "2024-05-05")] theorem forall₂_iff_nthLe {l₁ : List α} {l₂ : List β} : Forall₂ R l₁ l₂ ↔ l₁.length = l₂.length ∧ ∀ i h₁ h₂, R (l₁.nthLe i h₁) (l₂.nthLe i h₂) := forall₂_iff_get diff --git a/Mathlib/Data/List/Indexes.lean b/Mathlib/Data/List/Indexes.lean index c88ed84cd6e44..91f3b8c66cf09 100644 --- a/Mathlib/Data/List/Indexes.lean +++ b/Mathlib/Data/List/Indexes.lean @@ -211,6 +211,7 @@ theorem length_mapIdx {α β} (l : List α) (f : ℕ → α → β) : (l.mapIdx theorem mapIdx_eq_nil {α β} {f : ℕ → α → β} {l : List α} : List.mapIdx f l = [] ↔ l = [] := by rw [List.mapIdx_eq_enum_map, List.map_eq_nil, List.enum_eq_nil] +set_option linter.deprecated false in @[simp, deprecated] -- 2023-02-11 theorem nthLe_mapIdx {α β} (l : List α) (f : ℕ → α → β) (i : ℕ) (h : i < l.length) (h' : i < (l.mapIdx f).length := h.trans_le (l.length_mapIdx f).ge) : diff --git a/Mathlib/Data/List/Infix.lean b/Mathlib/Data/List/Infix.lean index 286fce2e7ccd5..35cf3193ba862 100644 --- a/Mathlib/Data/List/Infix.lean +++ b/Mathlib/Data/List/Infix.lean @@ -335,7 +335,7 @@ protected theorem IsPrefix.filterMap (h : l₁ <+: l₂) (f : α → Option β) protected theorem IsPrefix.reduceOption {l₁ l₂ : List (Option α)} (h : l₁ <+: l₂) : l₁.reduceOption <+: l₂.reduceOption := - h.filter_map id + h.filterMap id #align list.is_prefix.reduce_option List.IsPrefix.reduceOption #align list.is_prefix.filter List.IsPrefix.filter diff --git a/Mathlib/Data/List/InsertNth.lean b/Mathlib/Data/List/InsertNth.lean index 5b5fd11213e8b..561811b6a0b3e 100644 --- a/Mathlib/Data/List/InsertNth.lean +++ b/Mathlib/Data/List/InsertNth.lean @@ -147,6 +147,7 @@ theorem get_insertNth_of_lt (l : List α) (x : α) (n k : ℕ) (hn : k < n) (hk · rw [Nat.succ_lt_succ_iff] at hn simpa using IH _ _ hn _ +set_option linter.deprecated false in @[deprecated get_insertNth_of_lt] -- 2023-01-05 theorem nthLe_insertNth_of_lt : ∀ (l : List α) (x : α) (n k : ℕ), k < n → ∀ (hk : k < l.length) (hk' : k < (insertNth n x l).length := hk.trans_le (length_le_length_insertNth _ _ _)), @@ -166,6 +167,7 @@ theorem get_insertNth_self (l : List α) (x : α) (n : ℕ) (hn : n ≤ l.length · simp only [Nat.succ_le_succ_iff, length] at hn simpa using IH _ hn +set_option linter.deprecated false in @[simp, deprecated get_insertNth_self] theorem nthLe_insertNth_self (l : List α) (x : α) (n : ℕ) (hn : n ≤ l.length) (hn' : n < (insertNth n x l).length := (by rwa [length_insertNth _ _ hn, Nat.lt_succ_iff])) : diff --git a/Mathlib/Data/List/NodupEquivFin.lean b/Mathlib/Data/List/NodupEquivFin.lean index a39b9497f5244..dd276cc229bdb 100644 --- a/Mathlib/Data/List/NodupEquivFin.lean +++ b/Mathlib/Data/List/NodupEquivFin.lean @@ -40,7 +40,7 @@ for a version giving an equivalence when there is decidable equality. -/ @[simps] def getBijectionOfForallMemList (l : List α) (nd : l.Nodup) (h : ∀ x : α, x ∈ l) : { f : Fin l.length → α // Function.Bijective f } := - ⟨fun i => l.get i, fun _ _ h => Fin.ext <| (nd.nthLe_inj_iff _ _).1 h, + ⟨fun i => l.get i, fun _ _ h => nd.get_inj_iff.1 h, fun x => let ⟨i, hl⟩ := List.mem_iff_get.1 (h x) ⟨i, hl⟩⟩ @@ -233,6 +233,7 @@ theorem duplicate_iff_exists_distinct_get {l : List α} {x : α} : · simpa using h · simpa using h' +set_option linter.deprecated false in /-- An element `x : α` of `l : List α` is a duplicate iff it can be found at two distinct indices `n m : ℕ` inside the list `l`. -/ diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean index 956bfc3a26b09..e167aebee84d8 100644 --- a/Mathlib/Data/List/Perm.lean +++ b/Mathlib/Data/List/Perm.lean @@ -778,6 +778,7 @@ theorem get_permutations'Aux (s : List α) (x : α) (n : ℕ) · simpa [get] using IH _ _ #align list.nth_le_permutations'_aux List.get_permutations'Aux +set_option linter.deprecated false in @[deprecated get_permutations'Aux] -- 2024-04-23 theorem nthLe_permutations'Aux (s : List α) (x : α) (n : ℕ) (hn : n < length (permutations'Aux x s)) : diff --git a/Mathlib/Data/List/Sort.lean b/Mathlib/Data/List/Sort.lean index 4986a37274d06..7440e39aa3309 100644 --- a/Mathlib/Data/List/Sort.lean +++ b/Mathlib/Data/List/Sort.lean @@ -135,6 +135,8 @@ theorem Sorted.rel_get_of_lt {l : List α} (h : l.Sorted r) {a b : Fin l.length} r (l.get a) (l.get b) := List.pairwise_iff_get.1 h _ _ hab +set_option linter.deprecated false in +@[deprecated Sorted.rel_get_of_lt (since := "2024-05-08")] theorem Sorted.rel_nthLe_of_lt {l : List α} (h : l.Sorted r) {a b : ℕ} (ha : a < l.length) (hb : b < l.length) (hab : a < b) : r (l.nthLe a ha) (l.nthLe b hb) := List.pairwise_iff_get.1 h ⟨a, ha⟩ ⟨b, hb⟩ hab @@ -145,6 +147,8 @@ theorem Sorted.rel_get_of_le [IsRefl α r] {l : List α} (h : l.Sorted r) {a b : rcases hab.eq_or_lt with (rfl | hlt) exacts [refl _, h.rel_get_of_lt hlt] +set_option linter.deprecated false in +@[deprecated Sorted.rel_get_of_le (since := "2024-05-08")] theorem Sorted.rel_nthLe_of_le [IsRefl α r] {l : List α} (h : l.Sorted r) {a b : ℕ} (ha : a < l.length) (hb : b < l.length) (hab : a ≤ b) : r (l.nthLe a ha) (l.nthLe b hb) := h.rel_get_of_le hab @@ -156,7 +160,7 @@ theorem Sorted.rel_of_mem_take_of_mem_drop {l : List α} (h : List.Sorted r l) { obtain ⟨⟨ix, hix⟩, rfl⟩ := get_of_mem hx rw [get_take', get_drop'] rw [length_take] at hix - exact h.rel_nthLe_of_lt _ _ (Nat.lt_add_right _ (lt_min_iff.mp hix).left) + exact h.rel_get_of_lt (Nat.lt_add_right _ (lt_min_iff.mp hix).left) #align list.sorted.rel_of_mem_take_of_mem_drop List.Sorted.rel_of_mem_take_of_mem_drop end Sorted diff --git a/Mathlib/Data/List/Zip.lean b/Mathlib/Data/List/Zip.lean index 630085df1d021..f994967d1f71b 100644 --- a/Mathlib/Data/List/Zip.lean +++ b/Mathlib/Data/List/Zip.lean @@ -298,7 +298,8 @@ theorem get_zipWith {f : α → β → γ} {l : List α} {l' : List β} {i : Fin ⟨l.get ⟨i, lt_length_left_of_zipWith i.isLt⟩, l'.get ⟨i, lt_length_right_of_zipWith i.isLt⟩, by rw [get?_eq_get], by rw [get?_eq_get]; exact ⟨rfl, rfl⟩⟩ -@[simp] +set_option linter.deprecated false in +@[simp, deprecated get_zipWith (since := "2024-05-09")] theorem nthLe_zipWith {f : α → β → γ} {l : List α} {l' : List β} {i : ℕ} {h : i < (zipWith f l l').length} : (zipWith f l l').nthLe i h = @@ -312,7 +313,8 @@ theorem get_zip {l : List α} {l' : List β} {i : Fin (zip l l').length} : (l.get ⟨i, lt_length_left_of_zip i.isLt⟩, l'.get ⟨i, lt_length_right_of_zip i.isLt⟩) := get_zipWith -@[simp] +set_option linter.deprecated false in +@[simp, deprecated get_zip (since := "2024-05-09")] theorem nthLe_zip {l : List α} {l' : List β} {i : ℕ} {h : i < (zip l l').length} : (zip l l').nthLe i h = (l.nthLe i (lt_length_left_of_zip h), l'.nthLe i (lt_length_right_of_zip h)) := diff --git a/Mathlib/Data/MLList/BestFirst.lean b/Mathlib/Data/MLList/BestFirst.lean index 20030696241d3..8ec003793df80 100644 --- a/Mathlib/Data/MLList/BestFirst.lean +++ b/Mathlib/Data/MLList/BestFirst.lean @@ -128,7 +128,7 @@ def insertAndEject if q.size < max then q.insert n l else - match q.max with + match q.max? with | none => RBMap.empty | some m => q.insert n l |>.erase m.1 @@ -172,7 +172,7 @@ This may require improving estimates of priorities and shuffling the queue. partial def popWithBound (q : BestFirstQueue prio ε m β maxSize) : m (Option (((a : α) × (ε a) × β) × BestFirstQueue prio ε m β maxSize)) := do let q' ← ensureFirstIsBest q - match q'.min with + match q'.min? with | none => -- The queue is empty, nothing to return. return none diff --git a/Mathlib/Data/Nat/Nth.lean b/Mathlib/Data/Nat/Nth.lean index b12759c1b8da6..88020efde8bce 100644 --- a/Mathlib/Data/Nat/Nth.lean +++ b/Mathlib/Data/Nat/Nth.lean @@ -70,7 +70,7 @@ theorem nth_eq_getD_sort (h : (setOf p).Finite) (n : ℕ) : theorem nth_eq_orderEmbOfFin (hf : (setOf p).Finite) {n : ℕ} (hn : n < hf.toFinset.card) : nth p n = hf.toFinset.orderEmbOfFin rfl ⟨n, hn⟩ := by - rw [nth_eq_getD_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_get]; rfl + rw [nth_eq_getD_sort hf, Finset.orderEmbOfFin_apply, List.getD_eq_get] #align nat.nth_eq_order_emb_of_fin Nat.nth_eq_orderEmbOfFin theorem nth_strictMonoOn (hf : (setOf p).Finite) : diff --git a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean index 87ff6338a46af..b055590be4486 100644 --- a/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean +++ b/Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean @@ -906,7 +906,7 @@ theorem forall_map_sub_of_Icc (P : ℝ → Prop) (h : ∀ x ∈ Icc (0 : ℝ) 1, theorem translationNumber_lt_of_forall_lt_add (hf : Continuous f) {z : ℝ} (hz : ∀ x, f x < x + z) : τ f < z := by obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f y - y ≤ f x - x := - isCompact_Icc.exists_forall_ge (nonempty_Icc.2 zero_le_one) + isCompact_Icc.exists_isMaxOn (nonempty_Icc.2 zero_le_one) (hf.sub continuous_id).continuousOn refine' lt_of_le_of_lt _ (sub_lt_iff_lt_add'.2 <| hz x) apply translationNumber_le_of_le_add @@ -917,7 +917,7 @@ theorem translationNumber_lt_of_forall_lt_add (hf : Continuous f) {z : ℝ} (hz theorem lt_translationNumber_of_forall_add_lt (hf : Continuous f) {z : ℝ} (hz : ∀ x, x + z < f x) : z < τ f := by obtain ⟨x, -, hx⟩ : ∃ x ∈ Icc (0 : ℝ) 1, ∀ y ∈ Icc (0 : ℝ) 1, f x - x ≤ f y - y - exact isCompact_Icc.exists_forall_le (nonempty_Icc.2 zero_le_one) + exact isCompact_Icc.exists_isMinOn (nonempty_Icc.2 zero_le_one) (hf.sub continuous_id).continuousOn refine' lt_of_lt_of_le (lt_sub_iff_add_lt'.2 <| hz x) _ apply le_translationNumber_of_add_le diff --git a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean index 78ef46bb81629..71239953bbf7e 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean @@ -242,10 +242,20 @@ theorem length_toList_pos_of_mem_support (h : x ∈ p.support) : 0 < length (toL zero_lt_two.trans_le (two_le_length_toList_iff_mem_support.mpr h) #align equiv.perm.length_to_list_pos_of_mem_support Equiv.Perm.length_toList_pos_of_mem_support +theorem get_toList (n : ℕ) (hn : n < length (toList p x)) : (toList p x).get ⟨n, hn⟩ = (p ^ n) x := + by simp [toList] + +theorem toList_get_zero (h : x ∈ p.support) : + (toList p x).get ⟨0, (length_toList_pos_of_mem_support _ _ h)⟩ = x := by simp [toList] + +set_option linter.deprecated false in +@[deprecated get_toList (since := "2024-05-08")] theorem nthLe_toList (n : ℕ) (hn : n < length (toList p x)) : (toList p x).nthLe n hn = (p ^ n) x := by simp [toList] #align equiv.perm.nth_le_to_list Equiv.Perm.nthLe_toList +set_option linter.deprecated false in +@[deprecated toList_get_zero (since := "2024-05-08")] theorem toList_nthLe_zero (h : x ∈ p.support) : (toList p x).nthLe 0 (length_toList_pos_of_mem_support _ _ h) = x := by simp [toList] #align equiv.perm.to_list_nth_le_zero Equiv.Perm.toList_nthLe_zero diff --git a/Mathlib/GroupTheory/Perm/List.lean b/Mathlib/GroupTheory/Perm/List.lean index 0c8aa822834c5..4559c0eb5442d 100644 --- a/Mathlib/GroupTheory/Perm/List.lean +++ b/Mathlib/GroupTheory/Perm/List.lean @@ -294,6 +294,7 @@ theorem formPerm_pow_apply_get (l : List α) (h : Nodup l) (n k : ℕ) (hk : k < · simp [Nat.mod_eq_of_lt hk] · simp [pow_succ', mul_apply, hn, formPerm_apply_get _ h, Nat.succ_eq_add_one, ← Nat.add_assoc] +set_option linter.deprecated false in @[deprecated formPerm_pow_apply_get] -- 2024-04-23 theorem formPerm_pow_apply_nthLe (l : List α) (h : Nodup l) (n k : ℕ) (hk : k < l.length) : (formPerm l ^ n) (l.nthLe k hk) = diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean index b23e303e70054..c236aa8a6a895 100644 --- a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean +++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean @@ -667,7 +667,7 @@ theorem snorm_one_smul_measure {f : α → F} (c : ℝ≥0∞) : snorm f 1 (c theorem Memℒp.of_measure_le_smul {μ' : Measure α} (c : ℝ≥0∞) (hc : c ≠ ∞) (hμ'_le : μ' ≤ c • μ) {f : α → E} (hf : Memℒp f p μ) : Memℒp f p μ' := by - refine' ⟨hf.1.mono' (Measure.absolutelyContinuous_of_le_smul hμ'_le), _⟩ + refine' ⟨hf.1.mono_ac (Measure.absolutelyContinuous_of_le_smul hμ'_le), _⟩ refine' (snorm_mono_measure f hμ'_le).trans_lt _ by_cases hc0 : c = 0 · simp [hc0] diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean index 26b2dce43935f..305a88d8e5327 100644 --- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean +++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean @@ -1617,7 +1617,7 @@ theorem comp_measurable {γ : Type*} {_ : MeasurableSpace γ} {_ : MeasurableSpa theorem comp_quasiMeasurePreserving {γ : Type*} {_ : MeasurableSpace γ} {_ : MeasurableSpace α} {f : γ → α} {μ : Measure γ} {ν : Measure α} (hg : AEStronglyMeasurable g ν) (hf : QuasiMeasurePreserving f μ ν) : AEStronglyMeasurable (g ∘ f) μ := - (hg.mono' hf.absolutelyContinuous).comp_measurable hf.measurable + (hg.mono_ac hf.absolutelyContinuous).comp_measurable hf.measurable #align measure_theory.ae_strongly_measurable.comp_quasi_measure_preserving MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving theorem comp_measurePreserving {γ : Type*} {_ : MeasurableSpace γ} {_ : MeasurableSpace α} diff --git a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean index e05f00c0f8532..cdf98ee54ced5 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean @@ -718,7 +718,7 @@ theorem div_mem_nhds_one_of_haar_pos (μ : Measure G) [IsHaarMeasure μ] [Locall rcases MeasurableSet.exists_lt_isCompact hE hEpos with ⟨K, KE, K_comp, K_meas⟩ refine ⟨closure K, ?_, K_comp.closure, isClosed_closure, ?_⟩ · exact K_comp.closure_subset_measurableSet hE KE - · rwa [K_comp.measure_closure_eq_of_group] + · rwa [K_comp.measure_closure] filter_upwards [eventually_nhds_one_measure_smul_diff_lt hK K_closed hKpos.ne' (μ := μ)] with g hg have : ¬Disjoint (g • K) K := fun hd ↦ by rw [hd.symm.sdiff_eq_right, measure_smul] at hg diff --git a/Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean b/Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean index a4d15512078e7..794b169139f81 100644 --- a/Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean +++ b/Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean @@ -218,7 +218,7 @@ lemma hasSum_nat_cosKernel₀ (a : ℝ) {t : ℝ} (ht : 0 < t) : HasSum (fun n : ℕ ↦ 2 * Real.cos (2 * π * a * (n + 1)) * rexp (-π * (n + 1) ^ 2 * t)) (cosKernel a t - 1) := by rw [← hasSum_ofReal, ofReal_sub, ofReal_one] - have := (hasSum_int_cosKernel a ht).sum_nat_of_sum_int + have := (hasSum_int_cosKernel a ht).nat_add_neg rw [← hasSum_nat_add_iff' 1] at this simp_rw [Finset.sum_range_one, Nat.cast_zero, neg_zero, Int.cast_zero, zero_pow two_ne_zero, mul_zero, zero_mul, Complex.exp_zero, Real.exp_zero, ofReal_one, mul_one, Int.cast_neg, @@ -531,7 +531,7 @@ lemma hasSum_nat_completedCosZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) : (completedCosZeta a s) := by have aux : ((|0| : ℤ) : ℂ) ^ s = 0 := by rw [abs_zero, Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs)] - have hint := (hasSum_int_completedCosZeta a hs).sum_nat_of_sum_int + have hint := (hasSum_int_completedCosZeta a hs).nat_add_neg rw [aux, div_zero, zero_div, add_zero] at hint refine hint.congr_fun fun n ↦ ?_ split_ifs with h @@ -757,7 +757,7 @@ lemma hasSum_int_cosZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) : /-- Formula for `cosZeta` as a Dirichlet series in the convergence range, with sum over `ℕ`. -/ lemma hasSum_nat_cosZeta (a : ℝ) {s : ℂ} (hs : 1 < re s) : HasSum (fun n : ℕ ↦ Real.cos (2 * π * a * n) / (n : ℂ) ^ s) (cosZeta a s) := by - have := (hasSum_int_cosZeta a hs).sum_nat_of_sum_int + have := (hasSum_int_cosZeta a hs).nat_add_neg simp_rw [abs_neg, Int.cast_neg, Nat.abs_cast, Int.cast_natCast, mul_neg, abs_zero, Int.cast_zero, zero_cpow (ne_zero_of_one_lt_re hs), div_zero, zero_div, add_zero, ← add_div, div_right_comm _ _ (2 : ℂ)] at this diff --git a/Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean b/Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean index 9d2d5aa9cab3b..bbcba8b9c8509 100644 --- a/Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean +++ b/Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean @@ -76,7 +76,7 @@ theorem hasSum_nat_jacobiTheta {τ : ℂ} (hτ : 0 < im τ) : HasSum (fun n : ℕ => cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2) := by have := hasSum_jacobiTheta₂_term 0 hτ simp_rw [jacobiTheta₂_term, mul_zero, zero_add, ← jacobiTheta_eq_jacobiTheta₂] at this - have := this.sum_nat_of_sum_int + have := this.nat_add_neg rw [← hasSum_nat_add_iff' 1] at this simp_rw [Finset.sum_range_one, Int.cast_neg, Int.cast_natCast, Nat.cast_zero, neg_zero, Int.cast_zero, sq (0 : ℂ), mul_zero, zero_mul, neg_sq, ← mul_two, diff --git a/Mathlib/NumberTheory/NumberField/Basic.lean b/Mathlib/NumberTheory/NumberField/Basic.lean index 47cc68d615b02..550d74faf9e78 100644 --- a/Mathlib/NumberTheory/NumberField/Basic.lean +++ b/Mathlib/NumberTheory/NumberField/Basic.lean @@ -329,7 +329,7 @@ attribute [-instance] algebraRat is a number field. -/ instance {f : Polynomial ℚ} [hf : Fact (Irreducible f)] : NumberField (AdjoinRoot f) where to_charZero := charZero_of_injective_algebraMap (algebraMap ℚ _).injective - to_finiteDimensional := by convert (AdjoinRoot.powerBasis hf.out.ne_zero).finiteDimensional + to_finiteDimensional := by convert (AdjoinRoot.powerBasis hf.out.ne_zero).finite end diff --git a/Mathlib/NumberTheory/ZetaValues.lean b/Mathlib/NumberTheory/ZetaValues.lean index 677e7d3ab4029..a2bd05342743a 100644 --- a/Mathlib/NumberTheory/ZetaValues.lean +++ b/Mathlib/NumberTheory/ZetaValues.lean @@ -236,7 +236,7 @@ theorem hasSum_one_div_nat_pow_mul_fourier {k : ℕ} (hk : 2 ≤ k) {x : ℝ} (h (fun n : ℕ => (1 : ℂ) / (n : ℂ) ^ k * (fourier n (x : 𝕌) + (-1 : ℂ) ^ k * fourier (-n) (x : 𝕌))) (-(2 * π * I) ^ k / k ! * bernoulliFun k x) := by - convert (hasSum_one_div_pow_mul_fourier_mul_bernoulliFun hk hx).sum_nat_of_sum_int using 1 + convert (hasSum_one_div_pow_mul_fourier_mul_bernoulliFun hk hx).nat_add_neg using 1 · ext1 n rw [Int.cast_neg, mul_add, ← mul_assoc] conv_rhs => rw [neg_eq_neg_one_mul, mul_pow, ← div_div] diff --git a/Mathlib/Probability/Density.lean b/Mathlib/Probability/Density.lean index d7bbc3a0eec1b..83854775aec31 100644 --- a/Mathlib/Probability/Density.lean +++ b/Mathlib/Probability/Density.lean @@ -243,7 +243,8 @@ theorem integrable_pdf_smul_iff [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X Integrable (fun x => (pdf X ℙ μ x).toReal • f x) μ ↔ Integrable (fun x => f (X x)) ℙ := by -- Porting note: using `erw` because `rw` doesn't recognize `(f <| X ·)` as `f ∘ X` -- https://github.com/leanprover-community/mathlib4/issues/5164 - erw [← integrable_map_measure (hf.mono' HasPDF.absolutelyContinuous) (HasPDF.aemeasurable X ℙ μ), + erw [← integrable_map_measure (hf.mono_ac HasPDF.absolutelyContinuous) + (HasPDF.aemeasurable X ℙ μ), map_eq_withDensity_pdf X ℙ μ, pdf_def, integrable_rnDeriv_smul_iff HasPDF.absolutelyContinuous] eta_reduce rw [withDensity_rnDeriv_eq _ _ HasPDF.absolutelyContinuous] @@ -254,7 +255,7 @@ function `f`, `f ∘ X` is a random variable with expectation `∫ x, pdf X x where `μ` is a measure on the codomain of `X`. -/ theorem integral_pdf_smul [IsFiniteMeasure ℙ] {X : Ω → E} [HasPDF X ℙ μ] {f : E → F} (hf : AEStronglyMeasurable f μ) : ∫ x, (pdf X ℙ μ x).toReal • f x ∂μ = ∫ x, f (X x) ∂ℙ := by - rw [← integral_map (HasPDF.aemeasurable X ℙ μ) (hf.mono' HasPDF.absolutelyContinuous), + rw [← integral_map (HasPDF.aemeasurable X ℙ μ) (hf.mono_ac HasPDF.absolutelyContinuous), map_eq_withDensity_pdf X ℙ μ, pdf_def, integral_rnDeriv_smul HasPDF.absolutelyContinuous, withDensity_rnDeriv_eq _ _ HasPDF.absolutelyContinuous] #align measure_theory.pdf.integral_fun_mul_eq_integral MeasureTheory.pdf.integral_pdf_smul diff --git a/Mathlib/RingTheory/FreeCommRing.lean b/Mathlib/RingTheory/FreeCommRing.lean index 9763da662034e..86dad072d2c13 100644 --- a/Mathlib/RingTheory/FreeCommRing.lean +++ b/Mathlib/RingTheory/FreeCommRing.lean @@ -131,7 +131,7 @@ private def liftToMultiset : (α → R) ≃ (Multiplicative (Multiset α) →* R let x' := Multiplicative.toAdd x show (Multiset.map (fun a => F' {a}) x').sum = F' x' by erw [← Multiset.map_map (fun x => F' x) (fun x => {x}), ← AddMonoidHom.map_multiset_sum] - exact F.congr_arg (Multiset.sum_map_singleton x') + exact DFunLike.congr_arg F (Multiset.sum_map_singleton x') /-- Lift a map `α → R` to an additive group homomorphism `FreeCommRing α → R`. -/ def lift : (α → R) ≃ (FreeCommRing α →+* R) := diff --git a/Mathlib/RingTheory/Trace.lean b/Mathlib/RingTheory/Trace.lean index 6152d9aa25897..259a62dedfc8b 100644 --- a/Mathlib/RingTheory/Trace.lean +++ b/Mathlib/RingTheory/Trace.lean @@ -589,7 +589,7 @@ theorem det_traceMatrix_ne_zero' [IsSeparable K L] : det (traceMatrix K pb.basis suffices algebraMap K (AlgebraicClosure L) (det (traceMatrix K pb.basis)) ≠ 0 by refine' mt (fun ht => _) this rw [ht, RingHom.map_zero] - haveI : FiniteDimensional K L := pb.finiteDimensional + haveI : FiniteDimensional K L := pb.finite let e : Fin pb.dim ≃ (L →ₐ[K] AlgebraicClosure L) := (Fintype.equivFinOfCardEq ?_).symm · rw [RingHom.map_det, RingHom.mapMatrix_apply, traceMatrix_eq_embeddingsMatrixReindex_mul_trans K _ _ e, diff --git a/Mathlib/Topology/Algebra/Order/Compact.lean b/Mathlib/Topology/Algebra/Order/Compact.lean index 6420b2aff8c57..d0e57479b2550 100644 --- a/Mathlib/Topology/Algebra/Order/Compact.lean +++ b/Mathlib/Topology/Algebra/Order/Compact.lean @@ -306,7 +306,7 @@ theorem ContinuousOn.exists_isMinOn' [ClosedIicTopology α] {s : Set β} {f : β rcases (hasBasis_cocompact.inf_principal _).eventually_iff.1 hc with ⟨K, hK, hKf⟩ have hsub : insert x₀ (K ∩ s) ⊆ s := insert_subset_iff.2 ⟨h₀, inter_subset_right _ _⟩ obtain ⟨x, hx, hxf⟩ : ∃ x ∈ insert x₀ (K ∩ s), ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y := - ((hK.inter_right hsc).insert x₀).exists_forall_le (insert_nonempty _ _) (hf.mono hsub) + ((hK.inter_right hsc).insert x₀).exists_isMinOn (insert_nonempty _ _) (hf.mono hsub) refine' ⟨x, hsub hx, fun y hy => _⟩ by_cases hyK : y ∈ K exacts [hxf _ (Or.inr ⟨hyK, hy⟩), (hxf _ (Or.inl rfl)).trans (hKf ⟨hyK, hy⟩)] @@ -340,9 +340,9 @@ theorem ContinuousOn.exists_forall_ge' [ClosedIciTopology α] {s : Set β} {f : away from compact sets, then it has a global minimum. -/ theorem Continuous.exists_forall_le' [ClosedIicTopology α] {f : β → α} (hf : Continuous f) (x₀ : β) (h : ∀ᶠ x in cocompact β, f x₀ ≤ f x) : ∃ x : β, ∀ y : β, f x ≤ f y := - let ⟨x, _, hx⟩ := hf.continuousOn.exists_forall_le' isClosed_univ (mem_univ x₀) + let ⟨x, _, hx⟩ := hf.continuousOn.exists_isMinOn' isClosed_univ (mem_univ x₀) (by rwa [principal_univ, inf_top_eq]) - ⟨x, fun y => hx y (mem_univ y)⟩ + ⟨x, fun y => hx (mem_univ y)⟩ #align continuous.exists_forall_le' Continuous.exists_forall_le' /-- The **extreme value theorem**: if a continuous function `f` is smaller than a value in its range @@ -442,9 +442,9 @@ theorem IsCompact.sSup_lt_iff_of_continuous [ClosedIciTopology α] {f : β → sSup (f '' K) < y ↔ ∀ x ∈ K, f x < y := by refine' ⟨fun h x hx => (le_csSup (hK.bddAbove_image hf) <| mem_image_of_mem f hx).trans_lt h, fun h => _⟩ - obtain ⟨x, hx, h2x⟩ := hK.exists_forall_ge h0K hf + obtain ⟨x, hx, h2x⟩ := hK.exists_isMaxOn h0K hf refine' (csSup_le (h0K.image f) _).trans_lt (h x hx) - rintro _ ⟨x', hx', rfl⟩; exact h2x x' hx' + rintro _ ⟨x', hx', rfl⟩; exact h2x hx' #align is_compact.Sup_lt_iff_of_continuous IsCompact.sSup_lt_iff_of_continuous theorem IsCompact.lt_sInf_iff_of_continuous [ClosedIicTopology α] {f : β → α} {K : Set β} diff --git a/Mathlib/Topology/Algebra/Order/Rolle.lean b/Mathlib/Topology/Algebra/Order/Rolle.lean index 4e304d734ef42..5223e414bf609 100644 --- a/Mathlib/Topology/Algebra/Order/Rolle.lean +++ b/Mathlib/Topology/Algebra/Order/Rolle.lean @@ -39,9 +39,9 @@ theorem exists_Ioo_extr_on_Icc (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (h have ne : (Icc a b).Nonempty := nonempty_Icc.2 (le_of_lt hab) -- Consider absolute min and max points obtain ⟨c, cmem, cle⟩ : ∃ c ∈ Icc a b, ∀ x ∈ Icc a b, f c ≤ f x := - isCompact_Icc.exists_forall_le ne hfc + isCompact_Icc.exists_isMinOn ne hfc obtain ⟨C, Cmem, Cge⟩ : ∃ C ∈ Icc a b, ∀ x ∈ Icc a b, f x ≤ f C := - isCompact_Icc.exists_forall_ge ne hfc + isCompact_Icc.exists_isMaxOn ne hfc by_cases hc : f c = f a · by_cases hC : f C = f a · have : ∀ x ∈ Icc a b, f x = f a := fun x hx => le_antisymm (hC ▸ Cge x hx) (hc ▸ cle x hx) diff --git a/Mathlib/Topology/ContinuousFunction/Ideals.lean b/Mathlib/Topology/ContinuousFunction/Ideals.lean index 9998ad746b4b0..61c6589779785 100644 --- a/Mathlib/Topology/ContinuousFunction/Ideals.lean +++ b/Mathlib/Topology/ContinuousFunction/Ideals.lean @@ -292,7 +292,7 @@ theorem idealOfSet_ofIdeal_eq_closure (I : Ideal C(X, 𝕜)) : obtain ⟨c, hc, hgc'⟩ : ∃ c > 0, ∀ y : X, y ∈ t → c ≤ g' y := t.eq_empty_or_nonempty.elim (fun ht' => ⟨1, zero_lt_one, fun y hy => False.elim (by rwa [ht'] at hy)⟩) fun ht' => - let ⟨x, hx, hx'⟩ := ht.isCompact.exists_forall_le ht' (map_continuous g').continuousOn + let ⟨x, hx, hx'⟩ := ht.isCompact.exists_isMinOn ht' (map_continuous g').continuousOn ⟨g' x, hgt' x hx, hx'⟩ obtain ⟨g, hg, hgc⟩ := exists_mul_le_one_eqOn_ge g' hc refine' ⟨g * g', _, hg, hgc.mono hgc'⟩ diff --git a/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean b/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean index ba5a30f1c4272..fc68f42a36698 100644 --- a/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean +++ b/Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean @@ -420,7 +420,7 @@ variable (X : Type u) (Y : Type v) [MetricSpace X] [CompactSpace X] [Nonempty X] we can finally select a candidate minimizing `HD`. This will be the candidate realizing the optimal coupling. -/ private theorem exists_minimizer : ∃ f ∈ candidatesB X Y, ∀ g ∈ candidatesB X Y, HD f ≤ HD g := - isCompact_candidatesB.exists_forall_le candidatesB_nonempty HD_continuous.continuousOn + isCompact_candidatesB.exists_isMinOn candidatesB_nonempty HD_continuous.continuousOn private def optimalGHDist : Cb X Y := Classical.choose (exists_minimizer X Y) diff --git a/Mathlib/Topology/MetricSpace/HausdorffDistance.lean b/Mathlib/Topology/MetricSpace/HausdorffDistance.lean index 3158193259e03..9051564b58808 100644 --- a/Mathlib/Topology/MetricSpace/HausdorffDistance.lean +++ b/Mathlib/Topology/MetricSpace/HausdorffDistance.lean @@ -248,8 +248,7 @@ theorem _root_.IsOpen.exists_iUnion_isClosed {U : Set α} (hU : IsOpen U) : theorem _root_.IsCompact.exists_infEdist_eq_edist (hs : IsCompact s) (hne : s.Nonempty) (x : α) : ∃ y ∈ s, infEdist x s = edist x y := by have A : Continuous fun y => edist x y := continuous_const.edist continuous_id - obtain ⟨y, ys, hy⟩ : ∃ y ∈ s, ∀ z, z ∈ s → edist x y ≤ edist x z := - hs.exists_forall_le hne A.continuousOn + obtain ⟨y, ys, hy⟩ := hs.exists_isMinOn hne A.continuousOn exact ⟨y, ys, le_antisymm (infEdist_le_edist_of_mem ys) (by rwa [le_infEdist])⟩ #align is_compact.exists_inf_edist_eq_edist IsCompact.exists_infEdist_eq_edist @@ -258,12 +257,11 @@ theorem exists_pos_forall_lt_edist (hs : IsCompact s) (ht : IsClosed t) (hst : D rcases s.eq_empty_or_nonempty with (rfl | hne) · use 1 simp - obtain ⟨x, hx, h⟩ : ∃ x ∈ s, ∀ y ∈ s, infEdist x t ≤ infEdist y t := - hs.exists_forall_le hne continuous_infEdist.continuousOn + obtain ⟨x, hx, h⟩ := hs.exists_isMinOn hne continuous_infEdist.continuousOn have : 0 < infEdist x t := pos_iff_ne_zero.2 fun H => hst.le_bot ⟨hx, (mem_iff_infEdist_zero_of_closed ht).mpr H⟩ rcases ENNReal.lt_iff_exists_nnreal_btwn.1 this with ⟨r, h₀, hr⟩ - exact ⟨r, ENNReal.coe_pos.mp h₀, fun y hy z hz => hr.trans_le <| le_infEdist.1 (h y hy) z hz⟩ + exact ⟨r, ENNReal.coe_pos.mp h₀, fun y hy z hz => hr.trans_le <| le_infEdist.1 (h hy) z hz⟩ #align emetric.exists_pos_forall_lt_edist EMetric.exists_pos_forall_lt_edist end InfEdist diff --git a/Mathlib/Topology/MetricSpace/ProperSpace.lean b/Mathlib/Topology/MetricSpace/ProperSpace.lean index 70d387f4ba3d8..6b0a54f53afaa 100644 --- a/Mathlib/Topology/MetricSpace/ProperSpace.lean +++ b/Mathlib/Topology/MetricSpace/ProperSpace.lean @@ -137,7 +137,7 @@ theorem exists_pos_lt_subset_ball (hr : 0 < r) (hs : IsClosed s) (h : s ⊆ ball have : IsCompact s := (isCompact_closedBall x r).of_isClosed_subset hs (h.trans ball_subset_closedBall) obtain ⟨y, hys, hy⟩ : ∃ y ∈ s, s ⊆ closedBall x (dist y x) := - this.exists_forall_ge hne (continuous_id.dist continuous_const).continuousOn + this.exists_isMaxOn hne (continuous_id.dist continuous_const).continuousOn have hyr : dist y x < r := h hys rcases exists_between hyr with ⟨r', hyr', hrr'⟩ exact ⟨r', ⟨dist_nonneg.trans_lt hyr', hrr'⟩, hy.trans <| closedBall_subset_ball hyr'⟩ diff --git a/Mathlib/Topology/ProperMap.lean b/Mathlib/Topology/ProperMap.lean index 6b56d7288c21e..0d0a9397445f2 100644 --- a/Mathlib/Topology/ProperMap.lean +++ b/Mathlib/Topology/ProperMap.lean @@ -287,8 +287,10 @@ lemma isProperMap_restr_of_proper_of_closed {U : Set X} (hf : IsProperMap f) (hU IsProperMap.comp (isProperMap_subtype_val_of_closed hU) hf /-- The range of a proper map is closed. -/ -lemma IsProperMap.closed_range (hf : IsProperMap f) : IsClosed (range f) := - hf.isClosedMap.closed_range +lemma IsProperMap.isClosed_range (hf : IsProperMap f) : IsClosed (range f) := + hf.isClosedMap.isClosed_range + +@[deprecated (since := "2024-05-08")] alias IsProperMap.closed_range := IsProperMap.isClosed_range /-- Version of `isProperMap_iff_isClosedMap_and_compact_fibers` in terms of `cofinite` and `cocompact`. Only works when the codomain is `T1`. -/ diff --git a/Mathlib/Topology/UniformSpace/Basic.lean b/Mathlib/Topology/UniformSpace/Basic.lean index 6185fbc96c308..40356cdf45df6 100644 --- a/Mathlib/Topology/UniformSpace/Basic.lean +++ b/Mathlib/Topology/UniformSpace/Basic.lean @@ -1157,6 +1157,8 @@ protected theorem UniformSpace.le_sInf {tt : Set (UniformSpace α)} {t : Uniform (h : ∀ t' ∈ tt, t ≤ t') : t ≤ sInf tt := show 𝓤[t] ≤ ⨅ u ∈ tt, 𝓤[u] from le_iInf₂ h +set_option linter.deprecated false in +-- TODO update this code to avoid the deprecation instance : Top (UniformSpace α) := ⟨.ofNhdsEqComap ⟨⊤, le_top, le_top, le_top⟩ ⊤ fun x ↦ by simp only [nhds_top, comap_top]⟩ From e50d4102559e198e35fb447e995021e680656385 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 9 May 2024 09:01:36 +0000 Subject: [PATCH 11/15] feat(Rat, NNRat): `q * q.den = q.num` (#12739) and a few other lemmas. From LeanAPAP --- Archive/Imo/Imo2013Q5.lean | 2 +- Mathlib/Data/NNRat/Defs.lean | 22 +++++++++++++++++++ Mathlib/Data/Rat/Defs.lean | 10 +++++++++ Mathlib/Data/Rat/Lemmas.lean | 9 -------- .../RingTheory/Localization/FractionRing.lean | 2 +- 5 files changed, 34 insertions(+), 11 deletions(-) diff --git a/Archive/Imo/Imo2013Q5.lean b/Archive/Imo/Imo2013Q5.lean index 4b439868c75db..9d549f5d85d2e 100644 --- a/Archive/Imo/Imo2013Q5.lean +++ b/Archive/Imo/Imo2013Q5.lean @@ -241,7 +241,7 @@ theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y -- we need the top of the fraction to be strictly greater than 1 in order -- to apply `fixed_point_of_gt_1`. intro x hx - have H₀ : x * x.den = x.num := Rat.mul_den_eq_num + have H₀ : x * x.den = x.num := x.mul_den_eq_num have H : x * (↑(2 * x.den) : ℚ) = (↑(2 * x.num) : ℚ) := by push_cast; linear_combination 2 * H₀ set x2denom := 2 * x.den set x2num := 2 * x.num diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean index 7a4718a258894..79eb0c1ba042b 100644 --- a/Mathlib/Data/NNRat/Defs.lean +++ b/Mathlib/Data/NNRat/Defs.lean @@ -403,9 +403,31 @@ lemma mk_divInt (n d : ℕ) : lemma divNat_inj (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) : divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁ := by rw [← coe_inj]; simp [Rat.mkRat_eq_iff, h₁, h₂]; norm_cast +@[simp] lemma divNat_zero (n : ℕ) : divNat n 0 = 0 := by simp [divNat]; rfl + @[simp] lemma num_divNat_den (q : ℚ≥0) : divNat q.num q.den = q := ext $ by rw [← (q : ℚ).mkRat_num_den']; simp [num_coe, den_coe] +lemma natCast_eq_divNat (n : ℕ) : (n : ℚ≥0) = divNat n 1 := (num_divNat_den _).symm + +lemma divNat_mul_divNat (n₁ n₂ : ℕ) {d₁ d₂} (hd₁ : d₁ ≠ 0) (hd₂ : d₂ ≠ 0) : + divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂) := by + ext; push_cast; exact Rat.divInt_mul_divInt _ _ (mod_cast hd₁) (mod_cast hd₂) + +lemma divNat_mul_left {a : ℕ} (ha : a ≠ 0) (n d : ℕ) : divNat (a * n) (a * d) = divNat n d := by + ext; push_cast; exact Rat.divInt_mul_left (mod_cast ha) + +lemma divNat_mul_right {a : ℕ} (ha : a ≠ 0) (n d : ℕ) : divNat (n * a) (d * a) = divNat n d := by + ext; push_cast; exact Rat.divInt_mul_right (mod_cast ha) + +@[simp] lemma mul_den_eq_num (q : ℚ≥0) : q * q.den = q.num := by + ext + push_cast + rw [← Int.cast_natCast, ← den_coe, ← Int.cast_natCast q.num, ← num_coe] + exact Rat.mul_den_eq_num _ + +@[simp] lemma den_mul_eq_num (q : ℚ≥0) : q.den * q = q.num := by rw [mul_comm, mul_den_eq_num] + /-- Define a (dependent) function or prove `∀ r : ℚ, p r` by dealing with nonnegative rational numbers of the form `n / d` with `d ≠ 0` and `n`, `d` coprime. -/ @[elab_as_elim] diff --git a/Mathlib/Data/Rat/Defs.lean b/Mathlib/Data/Rat/Defs.lean index 4327a6a199946..d9c55a22faa14 100644 --- a/Mathlib/Data/Rat/Defs.lean +++ b/Mathlib/Data/Rat/Defs.lean @@ -574,6 +574,16 @@ theorem natCast_eq_divInt (n : ℕ) : ↑n = n /. 1 := by rw [← Int.cast_natCast, intCast_eq_divInt] #align rat.coe_nat_eq_mk Rat.natCast_eq_divInt +@[simp] lemma mul_den_eq_num (q : ℚ) : q * q.den = q.num := by + suffices (q.num /. ↑q.den) * (↑q.den /. 1) = q.num /. 1 by + conv => pattern (occs := 1) q; (rw [← num_divInt_den q]) + simp only [intCast_eq_divInt, natCast_eq_divInt, num_divInt_den] at this ⊢; assumption + have : (q.den : ℤ) ≠ 0 := mod_cast q.den_ne_zero + rw [divInt_mul_divInt _ _ this one_ne_zero, mul_comm (q.den : ℤ) 1, divInt_mul_right this] +#align rat.mul_denom_eq_num Rat.mul_den_eq_num + +@[simp] lemma den_mul_eq_num (q : ℚ) : q.den * q = q.num := by rw [mul_comm, mul_den_eq_num] + -- 2024-04-05 @[deprecated] alias coe_int_eq_divInt := intCast_eq_divInt @[deprecated] alias coe_int_div_eq_divInt := intCast_div_eq_divInt diff --git a/Mathlib/Data/Rat/Lemmas.lean b/Mathlib/Data/Rat/Lemmas.lean index b9472c869999c..ab92ae5f0d070 100644 --- a/Mathlib/Data/Rat/Lemmas.lean +++ b/Mathlib/Data/Rat/Lemmas.lean @@ -177,15 +177,6 @@ protected theorem inv_neg (q : ℚ) : (-q)⁻¹ = -q⁻¹ := by simp only [Rat.neg_divInt, Rat.inv_divInt', eq_self_iff_true, Rat.divInt_neg] #align rat.inv_neg Rat.inv_neg -@[simp] -theorem mul_den_eq_num {q : ℚ} : q * q.den = q.num := by - suffices (q.num /. ↑q.den) * (↑q.den /. 1) = q.num /. 1 by - conv => pattern (occs := 1) q; (rw [← num_divInt_den q]) - simp only [intCast_eq_divInt, natCast_eq_divInt, num_divInt_den] at this ⊢; assumption - have : (q.den : ℤ) ≠ 0 := ne_of_gt (mod_cast q.pos) - rw [Rat.divInt_mul_divInt _ _ this one_ne_zero, mul_comm (q.den : ℤ) 1, divInt_mul_right this] -#align rat.mul_denom_eq_num Rat.mul_den_eq_num - theorem den_div_cast_eq_one_iff (m n : ℤ) (hn : n ≠ 0) : ((m : ℚ) / n).den = 1 ↔ n ∣ m := by replace hn : (n : ℚ) ≠ 0 := by rwa [Ne, ← Int.cast_zero, coe_int_inj] constructor diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean index b2ccdc82dccca..83b8e46fa66b3 100644 --- a/Mathlib/RingTheory/Localization/FractionRing.lean +++ b/Mathlib/RingTheory/Localization/FractionRing.lean @@ -54,7 +54,7 @@ instance Rat.isFractionRing : IsFractionRing ℤ ℚ where simpa only [eq_intCast, isUnit_iff_ne_zero, Int.cast_eq_zero, Ne, Subtype.coe_mk] using hx surj' := by rintro ⟨n, d, hd, h⟩ - refine' ⟨⟨n, ⟨d, _⟩⟩, Rat.mul_den_eq_num⟩ + refine' ⟨⟨n, ⟨d, _⟩⟩, Rat.mul_den_eq_num _⟩ rw [mem_nonZeroDivisors_iff_ne_zero, Int.natCast_ne_zero_iff_pos] exact Nat.zero_lt_of_ne_zero hd exists_of_eq {x y} := by From 51625e908ad8a7478f13ad7a109d3bb32c2d610d Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 9 May 2024 10:48:39 +0000 Subject: [PATCH 12/15] refactor(Measure): use FunLike (#12684) Co-authored-by: Eric Wieser --- Mathlib/MeasureTheory/Constructions/Pi.lean | 16 ++++--- .../MeasureTheory/Decomposition/Jordan.lean | 4 +- .../MeasureTheory/Decomposition/Lebesgue.lean | 2 +- .../Group/FundamentalDomain.lean | 2 +- Mathlib/MeasureTheory/Measure/Dirac.lean | 4 +- .../MeasureTheory/Measure/EverywherePos.lean | 4 +- .../MeasureTheory/Measure/FiniteMeasure.lean | 8 ++-- .../Measure/FiniteMeasureProd.lean | 5 +-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean | 3 +- Mathlib/MeasureTheory/Measure/Hausdorff.lean | 10 ++--- .../Measure/Lebesgue/EqHaar.lean | 3 +- .../MeasureTheory/Measure/MeasureSpace.lean | 35 +++++---------- .../Measure/MeasureSpaceDef.lean | 45 +++++++++---------- .../Measure/ProbabilityMeasure.lean | 13 ++---- Mathlib/MeasureTheory/Measure/Restrict.lean | 14 +++--- Mathlib/MeasureTheory/Measure/Tilted.lean | 9 ++-- Mathlib/MeasureTheory/Measure/Trim.lean | 2 +- .../MeasureTheory/Measure/Typeclasses.lean | 7 ++- .../Probability/ConditionalProbability.lean | 13 +++--- Mathlib/Probability/Kernel/Composition.lean | 3 +- .../Kernel/Disintegration/Density.lean | 5 +-- Mathlib/Probability/Kernel/RadonNikodym.lean | 10 ++--- Mathlib/Probability/Variance.lean | 2 +- 23 files changed, 91 insertions(+), 128 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean index 5668bf5e83b4b..6e9521f349db8 100644 --- a/Mathlib/MeasureTheory/Constructions/Pi.lean +++ b/Mathlib/MeasureTheory/Constructions/Pi.lean @@ -249,10 +249,12 @@ instance sigmaFinite_tprod (l : List δ) (μ : ∀ i, Measure (π i)) [∀ i, Si theorem tprod_tprod (l : List δ) (μ : ∀ i, Measure (π i)) [∀ i, SigmaFinite (μ i)] (s : ∀ i, Set (π i)) : Measure.tprod l μ (Set.tprod l s) = (l.map fun i => (μ i) (s i)).prod := by - induction' l with i l ih; · simp - rw [tprod_cons, Set.tprod] - erw [prod_prod] -- TODO: why `rw` fails? - rw [map_cons, prod_cons, ih] + induction l with + | nil => simp + | cons a l ih => + rw [tprod_cons, Set.tprod] + erw [prod_prod] -- TODO: why `rw` fails? + rw [map_cons, prod_cons, ih] #align measure_theory.measure.tprod_tprod MeasureTheory.Measure.tprod_tprod end Tprod @@ -843,10 +845,10 @@ theorem measurePreserving_piUnique {π : ι → Type*} [Unique ι] {m : ∀ i, M set e := MeasurableEquiv.piUnique π have : (piPremeasure fun i => (μ i).toOuterMeasure) = Measure.map e.symm (μ default) := by ext1 s - rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply] + rw [piPremeasure, Fintype.prod_unique, e.symm.map_apply, coe_toOuterMeasure] congr 1; exact e.toEquiv.image_eq_preimage s - simp_rw [Measure.pi, OuterMeasure.pi, this, boundedBy_eq_self, toOuterMeasure_toMeasure, - MeasurableEquiv.map_map_symm] + simp_rw [Measure.pi, OuterMeasure.pi, this, ← coe_toOuterMeasure, boundedBy_eq_self, + toOuterMeasure_toMeasure, MeasurableEquiv.map_map_symm] theorem volume_preserving_piUnique (π : ι → Type*) [Unique ι] [∀ i, MeasureSpace (π i)] : MeasurePreserving (MeasurableEquiv.piUnique π) volume volume := diff --git a/Mathlib/MeasureTheory/Decomposition/Jordan.lean b/Mathlib/MeasureTheory/Decomposition/Jordan.lean index 6ecaf800b86fe..d7582de3f324b 100644 --- a/Mathlib/MeasureTheory/Decomposition/Jordan.lean +++ b/Mathlib/MeasureTheory/Decomposition/Jordan.lean @@ -189,8 +189,8 @@ theorem toSignedMeasure_smul (r : ℝ≥0) : (r • j).toSignedMeasure = r • j -- Porting note: removed `rfl` after the `rw` by adding further steps. rw [VectorMeasure.smul_apply, toSignedMeasure, toSignedMeasure, toSignedMeasure_sub_apply hi, toSignedMeasure_sub_apply hi, smul_sub, smul_posPart, - smul_negPart, ← ENNReal.toReal_smul, ← ENNReal.toReal_smul, smul_toOuterMeasure, - OuterMeasure.coe_smul, Pi.smul_apply, smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply] + smul_negPart, ← ENNReal.toReal_smul, ← ENNReal.toReal_smul, Measure.smul_apply, + Measure.smul_apply] #align measure_theory.jordan_decomposition.to_signed_measure_smul MeasureTheory.JordanDecomposition.toSignedMeasure_smul /-- A Jordan decomposition provides a Hahn decomposition. -/ diff --git a/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean b/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean index 10f4536cb90d5..873bdf8e97303 100644 --- a/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean +++ b/Mathlib/MeasureTheory/Decomposition/Lebesgue.lean @@ -221,7 +221,7 @@ lemma absolutelyContinuous_withDensity_rnDeriv [HaveLebesgueDecomposition ν μ] simp only [nonpos_iff_eq_zero, add_eq_zero] constructor · refine hμν ?_ - simp only [add_toOuterMeasure, OuterMeasure.coe_add, Pi.add_apply, add_eq_zero] + simp only [coe_add, Pi.add_apply, add_eq_zero] constructor · exact measure_mono_null (Set.inter_subset_right _ _) ht1 · exact measure_mono_null (Set.inter_subset_left _ _) hνs diff --git a/Mathlib/MeasureTheory/Group/FundamentalDomain.lean b/Mathlib/MeasureTheory/Group/FundamentalDomain.lean index 8c1567590ea69..8870735d06e9a 100644 --- a/Mathlib/MeasureTheory/Group/FundamentalDomain.lean +++ b/Mathlib/MeasureTheory/Group/FundamentalDomain.lean @@ -942,7 +942,7 @@ theorem IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_zero QuotientMeasureEqMeasurePreimage ν (0 : Measure (Quotient α_mod_G)) := by apply fund_dom_s.quotientMeasureEqMeasurePreimage ext U meas_U - simp only [zero_toOuterMeasure, OuterMeasure.coe_zero, Pi.zero_apply] + simp only [Measure.coe_zero, Pi.zero_apply] convert (measure_inter_null_of_null_right (h := vol_s) (Quotient.mk α_mod_G ⁻¹' U)).symm rw [measure_map_restrict_apply (meas_U := meas_U)] diff --git a/Mathlib/MeasureTheory/Measure/Dirac.lean b/Mathlib/MeasureTheory/Measure/Dirac.lean index ffead1aa256a9..9f8549aacfff7 100644 --- a/Mathlib/MeasureTheory/Measure/Dirac.lean +++ b/Mathlib/MeasureTheory/Measure/Dirac.lean @@ -65,8 +65,8 @@ theorem map_dirac {f : α → β} (hf : Measurable f) (a : α) : (dirac a).map f lemma map_const (μ : Measure α) (c : β) : μ.map (fun _ ↦ c) = (μ Set.univ) • dirac c := by ext s hs - simp only [aemeasurable_const, measurable_const, smul_toOuterMeasure, OuterMeasure.coe_smul, - Pi.smul_apply, dirac_apply' _ hs, smul_eq_mul] + simp only [aemeasurable_const, measurable_const, Measure.coe_smul, Pi.smul_apply, + dirac_apply' _ hs, smul_eq_mul] classical rw [Measure.map_apply measurable_const hs, Set.preimage_const] by_cases hsc : c ∈ s diff --git a/Mathlib/MeasureTheory/Measure/EverywherePos.lean b/Mathlib/MeasureTheory/Measure/EverywherePos.lean index a13922b5c1831..ce97a307136dd 100644 --- a/Mathlib/MeasureTheory/Measure/EverywherePos.lean +++ b/Mathlib/MeasureTheory/Measure/EverywherePos.lean @@ -109,7 +109,7 @@ lemma measure_eq_zero_of_subset_diff_everywherePosSubset its everywhere positive subset. -/ lemma everywherePosSubset_ae_eq [OpensMeasurableSpace α] [InnerRegular μ] (hs : MeasurableSet s) : μ.everywherePosSubset s =ᵐ[μ] s := by - simp only [ae_eq_set, diff_eq_empty.mpr (everywherePosSubset_subset μ s), OuterMeasure.empty', + simp only [ae_eq_set, diff_eq_empty.mpr (everywherePosSubset_subset μ s), measure_empty, true_and, (hs.diff hs.everywherePosSubset).measure_eq_iSup_isCompact, ENNReal.iSup_eq_zero] intro k hk h'k exact measure_eq_zero_of_subset_diff_everywherePosSubset h'k hk @@ -121,7 +121,7 @@ lemma everywherePosSubset_ae_eq_of_measure_ne_top μ.everywherePosSubset s =ᵐ[μ] s := by have A : μ (s \ μ.everywherePosSubset s) ≠ ∞ := ((measure_mono (diff_subset _ _ )).trans_lt h's.lt_top).ne - simp only [ae_eq_set, diff_eq_empty.mpr (everywherePosSubset_subset μ s), OuterMeasure.empty', + simp only [ae_eq_set, diff_eq_empty.mpr (everywherePosSubset_subset μ s), measure_empty, true_and, (hs.diff hs.everywherePosSubset).measure_eq_iSup_isCompact_of_ne_top A, ENNReal.iSup_eq_zero] intro k hk h'k diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean index 6f83a54a485eb..657fa9af35145 100644 --- a/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/FiniteMeasure.lean @@ -222,8 +222,7 @@ variable {R : Type*} [SMul R ℝ≥0] [SMul R ℝ≥0∞] [IsScalarTower R ℝ instance instSMul : SMul R (FiniteMeasure Ω) where smul (c : R) μ := ⟨c • (μ : Measure Ω), MeasureTheory.isFiniteMeasureSMulOfNNRealTower⟩ --- Porting note: with `simp` here the `coeFn` lemmas below fall prey to `simpNF`: the LHS simplifies -@[norm_cast] +@[simp, norm_cast] theorem toMeasure_zero : ((↑) : FiniteMeasure Ω → Measure Ω) 0 = 0 := rfl #align measure_theory.finite_measure.coe_zero MeasureTheory.FiniteMeasure.toMeasure_zero @@ -240,9 +239,8 @@ theorem toMeasure_smul (c : R) (μ : FiniteMeasure Ω) : ↑(c • μ) = c • ( rfl #align measure_theory.finite_measure.coe_smul MeasureTheory.FiniteMeasure.toMeasure_smul -@[simp, norm_cast] -theorem coeFn_zero : (⇑(0 : FiniteMeasure Ω) : Set Ω → ℝ≥0) = (0 : Set Ω → ℝ≥0) := by - funext; rfl +@[norm_cast] +theorem coeFn_zero : (⇑(0 : FiniteMeasure Ω) : Set Ω → ℝ≥0) = (0 : Set Ω → ℝ≥0) := rfl #align measure_theory.finite_measure.coe_fn_zero MeasureTheory.FiniteMeasure.coeFn_zero @[simp, norm_cast] diff --git a/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean b/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean index b32e05b93ac83..bd80ac705eea2 100644 --- a/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean +++ b/Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean @@ -71,7 +71,7 @@ lemma prod_prod (s : Set α) (t : Set β) : μ.prod ν (s ×ˢ t) = μ s * ν t apply Subtype.ext simp only [val_eq_toMeasure, toMeasure_map, toMeasure_prod, Measure.map_fst_prod] ext s _ - simp only [Measure.smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply, smul_eq_mul] + simp only [Measure.coe_smul, Pi.smul_apply, smul_eq_mul] have aux := coeFn_smul_apply (ν univ) μ s simpa using congr_arg ENNReal.ofNNReal aux.symm @@ -79,8 +79,7 @@ lemma prod_prod (s : Set α) (t : Set β) : μ.prod ν (s ×ˢ t) = μ s * ν t apply Subtype.ext simp only [val_eq_toMeasure, toMeasure_map, toMeasure_prod, Measure.map_fst_prod] ext s _ - simp only [Measure.map_snd_prod, Measure.smul_toOuterMeasure, OuterMeasure.coe_smul, - Pi.smul_apply, smul_eq_mul] + simp only [Measure.map_snd_prod, Measure.coe_smul, Pi.smul_apply, smul_eq_mul] have aux := coeFn_smul_apply (μ univ) ν s simpa using congr_arg ENNReal.ofNNReal aux.symm diff --git a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean index cdf98ee54ced5..8688faf459444 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean @@ -636,8 +636,7 @@ instance isMulLeftInvariant_haarMeasure (K₀ : PositiveCompacts G) : @[to_additive] theorem haarMeasure_self {K₀ : PositiveCompacts G} : haarMeasure K₀ K₀ = 1 := by haveI : LocallyCompactSpace G := K₀.locallyCompactSpace_of_group - simp only [haarMeasure, smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply, - smul_eq_mul] + simp only [haarMeasure, coe_smul, Pi.smul_apply, smul_eq_mul] rw [← OuterRegular.measure_closure_eq_of_isCompact K₀.isCompact, Content.measure_apply _ isClosed_closure.measurableSet, ENNReal.inv_mul_cancel] · exact (haarContent_outerMeasure_closure_pos K₀).ne' diff --git a/Mathlib/MeasureTheory/Measure/Hausdorff.lean b/Mathlib/MeasureTheory/Measure/Hausdorff.lean index 7159602d76a95..9c9f1e13c2463 100644 --- a/Mathlib/MeasureTheory/Measure/Hausdorff.lean +++ b/Mathlib/MeasureTheory/Measure/Hausdorff.lean @@ -468,7 +468,7 @@ end Measure theorem OuterMeasure.coe_mkMetric [MeasurableSpace X] [BorelSpace X] (m : ℝ≥0∞ → ℝ≥0∞) : ⇑(OuterMeasure.mkMetric m : OuterMeasure X) = Measure.mkMetric m := by - rw [← Measure.mkMetric_toOuterMeasure] + rw [← Measure.mkMetric_toOuterMeasure, Measure.coe_toOuterMeasure] #align measure_theory.outer_measure.coe_mk_metric MeasureTheory.OuterMeasure.coe_mkMetric namespace Measure @@ -870,12 +870,8 @@ variable {f : X → Y} {d : ℝ} theorem hausdorffMeasure_image (hf : Isometry f) (hd : 0 ≤ d ∨ Surjective f) (s : Set X) : μH[d] (f '' s) = μH[d] s := by simp only [hausdorffMeasure, ← OuterMeasure.coe_mkMetric, ← OuterMeasure.comap_apply] - -- Porting note: this proof was slightly nicer before the port - simp only [mkMetric_toOuterMeasure] - have : 0 ≤ d → Monotone fun r : ℝ≥0∞ ↦ r ^ d := by - exact fun hd x y hxy => ENNReal.rpow_le_rpow hxy hd - have := OuterMeasure.isometry_comap_mkMetric (fun (r : ℝ≥0∞) => r ^ d) hf (hd.imp_left this) - congr + rw [OuterMeasure.isometry_comap_mkMetric _ hf (hd.imp_left _)] + exact ENNReal.monotone_rpow_of_nonneg #align isometry.hausdorff_measure_image Isometry.hausdorffMeasure_image theorem hausdorffMeasure_preimage (hf : Isometry f) (hd : 0 ≤ d ∨ Surjective f) (s : Set Y) : diff --git a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean index 4e09341327e38..08209cec60ce9 100644 --- a/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean +++ b/Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean @@ -377,8 +377,7 @@ theorem addHaar_preimage_smul {r : ℝ} (hr : r ≠ 0) (s : Set E) : μ ((r • ·) ⁻¹' s) = Measure.map (r • ·) μ s := ((Homeomorph.smul (isUnit_iff_ne_zero.2 hr).unit).toMeasurableEquiv.map_apply s).symm _ = ENNReal.ofReal (abs (r ^ finrank ℝ E)⁻¹) * μ s := by - rw [map_addHaar_smul μ hr, smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply, - smul_eq_mul] + rw [map_addHaar_smul μ hr, coe_smul, Pi.smul_apply, smul_eq_mul] #align measure_theory.measure.add_haar_preimage_smul MeasureTheory.Measure.addHaar_preimage_smul /-- Rescaling a set by a factor `r` multiplies its measure by `abs (r ^ dim)`. -/ diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean index cde400cdee133..660870a1fd67e 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean +++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean @@ -745,10 +745,7 @@ theorem toMeasure_toOuterMeasure (m : OuterMeasure α) (h : ms ≤ m.caratheodor rfl #align measure_theory.to_measure_to_outer_measure MeasureTheory.toMeasure_toOuterMeasure --- Porting note: A coercion is directly elaborated in Lean4, so the LHS is simplified by --- `toMeasure_toOuterMeasure` even if this theorem has high priority. --- Instead of this theorem, we give `simp` attr to `OuterMeasure.trim_eq`. --- @[simp] +@[simp] theorem toMeasure_apply (m : OuterMeasure α) (h : ms ≤ m.caratheodory) {s : Set α} (hs : MeasurableSet s) : m.toMeasure h s = m s := m.trim_eq hs @@ -890,7 +887,7 @@ instance instSMul [MeasurableSpace α] : SMul R (Measure α) := ⟨fun c μ => { toOuterMeasure := c • μ.toOuterMeasure m_iUnion := fun s hs hd => by - simp_rw [OuterMeasure.smul_apply, measure_iUnion hd hs] + simp_rw [OuterMeasure.smul_apply, coe_toOuterMeasure, measure_iUnion hd hs] simpa using (ENNReal.tsum_mul_left (a := c • 1)).symm trimmed := by rw [OuterMeasure.trim_smul, μ.trimmed] }⟩ #align measure_theory.measure.has_smul MeasureTheory.Measure.instSMul @@ -971,10 +968,7 @@ instance instModule [Semiring R] [Module R ℝ≥0∞] [IsScalarTower R ℝ≥0 toOuterMeasure_injective smul_toOuterMeasure #align measure_theory.measure.module MeasureTheory.Measure.instModule --- Porting note: A coercion is directly elaborated in Lean4, so the LHS is simplified by --- `smul_toOuterMeasure` even if this theorem has high priority. --- Instead of this theorem, we give `simp` attr to `nnreal_smul_coe_apply`. --- @[simp] +@[simp] theorem coe_nnreal_smul_apply {_m : MeasurableSpace α} (c : ℝ≥0) (μ : Measure α) (s : Set α) : (c • μ) s = c * μ s := rfl @@ -1041,7 +1035,7 @@ theorem toOuterMeasure_le : μ₁.toOuterMeasure ≤ μ₂.toOuterMeasure ↔ μ #align measure_theory.measure.to_outer_measure_le MeasureTheory.Measure.toOuterMeasure_le theorem le_iff : μ₁ ≤ μ₂ ↔ ∀ s, MeasurableSet s → μ₁ s ≤ μ₂ s := by - rw [← toOuterMeasure_le, ← OuterMeasure.le_trim_iff, μ₂.trimmed] + erw [← toOuterMeasure_le, ← OuterMeasure.le_trim_iff, μ₂.trimmed] #align measure_theory.measure.le_iff MeasureTheory.Measure.le_iff theorem le_intro (h : ∀ s, MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s) : μ₁ ≤ μ₂ := @@ -1078,8 +1072,8 @@ theorem sInf_caratheodory (s : Set α) (hs : MeasurableSet s) : MeasurableSet[(sInf (toOuterMeasure '' m)).caratheodory] s := by rw [OuterMeasure.sInf_eq_boundedBy_sInfGen] refine' OuterMeasure.boundedBy_caratheodory fun t => _ - simp only [OuterMeasure.sInfGen, le_iInf_iff, forall_mem_image, - measure_eq_iInf t] + simp only [OuterMeasure.sInfGen, le_iInf_iff, forall_mem_image, measure_eq_iInf t, + coe_toOuterMeasure] intro μ hμ u htu _hu have hm : ∀ {s t}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t := by intro s t hst @@ -1320,7 +1314,7 @@ theorem map_toOuterMeasure (hf : AEMeasurable f μ) : (μ.map f).toOuterMeasure = (OuterMeasure.map f μ.toOuterMeasure).trim := by rw [← trimmed, OuterMeasure.trim_eq_trim_iff] intro s hs - rw [map_apply_of_aemeasurable hf hs, OuterMeasure.map_apply] + simp [hf, hs] #align measure_theory.measure.map_to_outer_measure MeasureTheory.Measure.map_toOuterMeasure @[simp] lemma map_eq_zero_iff (hf : AEMeasurable f μ) : μ.map f = 0 ↔ μ = 0 := by @@ -1395,7 +1389,7 @@ def comapₗ [MeasurableSpace α] (f : α → β) : Measure β →ₗ[ℝ≥0∞ theorem comapₗ_apply {β} [MeasurableSpace α] {mβ : MeasurableSpace β} (f : α → β) (hfi : Injective f) (hf : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) (μ : Measure β) (hs : MeasurableSet s) : comapₗ f μ s = μ (f '' s) := by - rw [comapₗ, dif_pos, liftLinear_apply _ hs, OuterMeasure.comap_apply] + rw [comapₗ, dif_pos, liftLinear_apply _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure] exact ⟨hfi, hf⟩ #align measure_theory.measure.comapₗ_apply MeasureTheory.Measure.comapₗ_apply @@ -1413,7 +1407,7 @@ theorem comap_apply₀ [MeasurableSpace α] (f : α → β) (μ : Measure β) (h (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) (hs : NullMeasurableSet s (comap f μ)) : comap f μ s = μ (f '' s) := by rw [comap, dif_pos (And.intro hfi hf)] at hs ⊢ - rw [toMeasure_apply₀ _ _ hs, OuterMeasure.comap_apply] + rw [toMeasure_apply₀ _ _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure] #align measure_theory.measure.comap_apply₀ MeasureTheory.Measure.comap_apply₀ theorem le_comap_apply {β} [MeasurableSpace α] {mβ : MeasurableSpace β} (f : α → β) (μ : Measure β) @@ -1572,9 +1566,6 @@ theorem sum_fintype [Fintype ι] (μ : ι → Measure α) : sum μ = ∑ i, μ i simp only [sum_apply, finset_sum_apply, hs, tsum_fintype] #align measure_theory.measure.sum_fintype MeasureTheory.Measure.sum_fintype --- Porting note: The LHS is simplified by --- `sum_fintype` even if this theorem has high priority. -@[simp, nolint simpNF] theorem sum_coe_finset (s : Finset ι) (μ : ι → Measure α) : (sum fun i : s => μ i) = ∑ i in s, μ i := by rw [sum_fintype, Finset.sum_coe_sort s μ] #align measure_theory.measure.sum_coe_finset MeasureTheory.Measure.sum_coe_finset @@ -1584,17 +1575,15 @@ theorem ae_sum_eq [Countable ι] (μ : ι → Measure α) : (sum μ).ae = ⨆ i, Filter.ext fun _ => ae_sum_iff.trans mem_iSup.symm #align measure_theory.measure.ae_sum_eq MeasureTheory.Measure.ae_sum_eq --- @[simp] -- Porting note (#10618): simp can prove this theorem sum_bool (f : Bool → Measure α) : sum f = f true + f false := by rw [sum_fintype, Fintype.sum_bool] #align measure_theory.measure.sum_bool MeasureTheory.Measure.sum_bool --- @[simp] -- Porting note (#10618): simp can prove this theorem sum_cond (μ ν : Measure α) : (sum fun b => cond b μ ν) = μ + ν := sum_bool _ #align measure_theory.measure.sum_cond MeasureTheory.Measure.sum_cond --- @[simp] -- Porting note (#10618): simp can prove this +@[simp] theorem sum_of_empty [IsEmpty ι] (μ : ι → Measure α) : sum μ = 0 := by rw [← measure_univ_eq_zero, sum_apply _ MeasurableSet.univ, tsum_empty] #align measure_theory.measure.sum_of_empty MeasureTheory.Measure.sum_of_empty @@ -1691,7 +1680,7 @@ protected theorem smul [Monoid R] [DistribMulAction R ℝ≥0∞] [IsScalarTower protected lemma add (h1 : μ₁ ≪ ν) (h2 : μ₂ ≪ ν') : μ₁ + μ₂ ≪ ν + ν' := by intro s hs - simp only [add_toOuterMeasure, OuterMeasure.coe_add, Pi.add_apply, add_eq_zero] at hs ⊢ + simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢ exact ⟨h1 hs.1, h2 hs.2⟩ lemma add_left_iff {μ₁ μ₂ ν : Measure α} : @@ -1705,7 +1694,7 @@ lemma add_left_iff {μ₁ μ₂ ν : Measure α} : lemma add_right (h1 : μ ≪ ν) (ν' : Measure α) : μ ≪ ν + ν' := by intro s hs - simp only [add_toOuterMeasure, OuterMeasure.coe_add, Pi.add_apply, add_eq_zero] at hs ⊢ + simp only [coe_add, Pi.add_apply, add_eq_zero] at hs ⊢ exact h1 hs.1 end AbsolutelyContinuous diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean b/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean index 8bd7408a411c1..20ac9032356b6 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean +++ b/Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean @@ -78,23 +78,21 @@ namespace MeasureTheory measurable sets, with the additional assumption that the outer measure is the canonical extension of the restricted measure. -/ structure Measure (α : Type*) [MeasurableSpace α] extends OuterMeasure α where - m_iUnion ⦃f : ℕ → Set α⦄ : - (∀ i, MeasurableSet (f i)) → - Pairwise (Disjoint on f) → toOuterMeasure (⋃ i, f i) = ∑' i, toOuterMeasure (f i) + m_iUnion ⦃f : ℕ → Set α⦄ : (∀ i, MeasurableSet (f i)) → Pairwise (Disjoint on f) → + toOuterMeasure (⋃ i, f i) = ∑' i, toOuterMeasure (f i) trimmed : toOuterMeasure.trim = toOuterMeasure #align measure_theory.measure MeasureTheory.Measure -/-- Measure projections for a measure space. +theorem Measure.toOuterMeasure_injective [MeasurableSpace α] : + Injective (toOuterMeasure : Measure α → OuterMeasure α) + | ⟨_, _, _⟩, ⟨_, _, _⟩, rfl => rfl +#align measure_theory.measure.to_outer_measure_injective MeasureTheory.Measure.toOuterMeasure_injective -For measurable sets this returns the measure assigned by the `measureOf` field in `Measure`. -But we can extend this to _all_ sets, but using the outer measure. This gives us monotonicity and -subadditivity for all sets. --/ -instance Measure.instCoeFun [MeasurableSpace α] : CoeFun (Measure α) fun _ => Set α → ℝ≥0∞ := - ⟨fun m => m.toOuterMeasure⟩ -#align measure_theory.measure.has_coe_to_fun MeasureTheory.Measure.instCoeFun +instance Measure.instFunLike [MeasurableSpace α] : FunLike (Measure α) (Set α) ℝ≥0∞ where + coe μ := μ.toOuterMeasure + coe_injective' | ⟨_, _, _⟩, ⟨_, _, _⟩, h => toOuterMeasure_injective <| DFunLike.coe_injective h -attribute [coe] Measure.toOuterMeasure +#noalign measure_theory.measure.has_coe_to_fun section @@ -104,7 +102,6 @@ namespace Measure /-! ### General facts about measures -/ - /-- Obtain a measure by giving a countably additive function that sends `∅` to `0`. -/ def ofMeasurable (m : ∀ s : Set α, MeasurableSet s → ℝ≥0∞) (m0 : m ∅ MeasurableSet.empty = 0) (mU : @@ -132,11 +129,6 @@ theorem ofMeasurable_apply {m : ∀ s : Set α, MeasurableSet s → ℝ≥0∞} inducedOuterMeasure_eq m0 mU hs #align measure_theory.measure.of_measurable_apply MeasureTheory.Measure.ofMeasurable_apply -theorem toOuterMeasure_injective : Injective (toOuterMeasure : Measure α → OuterMeasure α) := - fun ⟨m₁, u₁, h₁⟩ ⟨m₂, _u₂, _h₂⟩ _h => by - congr -#align measure_theory.measure.to_outer_measure_injective MeasureTheory.Measure.toOuterMeasure_injective - @[ext] theorem ext (h : ∀ s, MeasurableSet s → μ₁ s = μ₂ s) : μ₁ = μ₂ := toOuterMeasure_injective <| by @@ -152,15 +144,20 @@ theorem ext_iff' : μ₁ = μ₂ ↔ ∀ s, μ₁ s = μ₂ s := end Measure -#noalign measure_theory.coe_to_outer_measure +@[simp] theorem Measure.coe_toOuterMeasure (μ : Measure α) : ⇑μ.toOuterMeasure = μ := rfl +#align measure_theory.coe_to_outer_measure MeasureTheory.Measure.coe_toOuterMeasure -#noalign measure_theory.to_outer_measure_apply +theorem Measure.toOuterMeasure_apply (μ : Measure α) (s : Set α) : + μ.toOuterMeasure s = μ s := + rfl +#align measure_theory.to_outer_measure_apply MeasureTheory.Measure.toOuterMeasure_apply -theorem measure_eq_trim (s : Set α) : μ s = μ.toOuterMeasure.trim s := by rw [μ.trimmed] +theorem measure_eq_trim (s : Set α) : μ s = μ.toOuterMeasure.trim s := by + rw [μ.trimmed, μ.coe_toOuterMeasure] #align measure_theory.measure_eq_trim MeasureTheory.measure_eq_trim theorem measure_eq_iInf (s : Set α) : μ s = ⨅ (t) (_ : s ⊆ t) (_ : MeasurableSet t), μ t := by - rw [measure_eq_trim, OuterMeasure.trim_eq_iInf] + rw [measure_eq_trim, OuterMeasure.trim_eq_iInf, μ.coe_toOuterMeasure] #align measure_theory.measure_eq_infi MeasureTheory.measure_eq_iInf /-- A variant of `measure_eq_iInf` which has a single `iInf`. This is useful when applying a @@ -187,7 +184,7 @@ theorem measure_eq_extend (hs : MeasurableSet s) : exact hs #align measure_theory.measure_eq_extend MeasureTheory.measure_eq_extend --- @[simp] -- Porting note (#10618): simp can prove this +@[simp] theorem measure_empty : μ ∅ = 0 := μ.empty #align measure_theory.measure_empty MeasureTheory.measure_empty @@ -277,7 +274,7 @@ theorem measure_iUnion_null [Countable ι] {s : ι → Set α} : (∀ i, μ (s i μ.toOuterMeasure.iUnion_null #align measure_theory.measure_Union_null MeasureTheory.measure_iUnion_null --- @[simp] -- Porting note (#10618): simp can prove this +@[simp] theorem measure_iUnion_null_iff [Countable ι] {s : ι → Set α} : μ (⋃ i, s i) = 0 ↔ ∀ i, μ (s i) = 0 := μ.toOuterMeasure.iUnion_null_iff diff --git a/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean b/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean index 4dfaaf65579a3..5600282f7b004 100644 --- a/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean +++ b/Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean @@ -353,8 +353,8 @@ def normalize : ProbabilityMeasure Ω := refine' ⟨_⟩ -- Porting note: paying the price that this isn't `simp` lemma now. rw [FiniteMeasure.toMeasure_smul] - simp only [Measure.smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply, - Measure.nnreal_smul_coe_apply, ne_eq, mass_zero_iff, ENNReal.coe_inv zero, ennreal_mass] + simp only [Measure.coe_smul, Pi.smul_apply, Measure.nnreal_smul_coe_apply, ne_eq, + mass_zero_iff, ENNReal.coe_inv zero, ennreal_mass] rw [← Ne, ← ENNReal.coe_ne_zero, ennreal_mass] at zero exact ENNReal.inv_mul_cancel zero μ.prop.measure_univ_lt_top.ne } #align measure_theory.finite_measure.normalize MeasureTheory.FiniteMeasure.normalize @@ -362,15 +362,10 @@ def normalize : ProbabilityMeasure Ω := @[simp] theorem self_eq_mass_mul_normalize (s : Set Ω) : μ s = μ.mass * μ.normalize s := by obtain rfl | h := eq_or_ne μ 0 - · simp only [zero_mass, coeFn_zero, Pi.zero_apply, zero_mul] - rfl + · simp have mass_nonzero : μ.mass ≠ 0 := by rwa [μ.mass_nonzero_iff] simp only [normalize, dif_neg mass_nonzero] - change μ s = mass μ * ((mass μ)⁻¹ • μ) s - -- Porting note: this `change` is a hack, but I had trouble coming up with something better - simp only [toMeasure_smul, Measure.smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply, - Measure.nnreal_smul_coe_apply, ne_eq, mass_zero_iff, ENNReal.toNNReal_mul, ENNReal.toNNReal_coe, - mul_inv_cancel_left₀ mass_nonzero] + simp [ProbabilityMeasure.coe_mk, toMeasure_smul, mul_inv_cancel_left₀ mass_nonzero] #align measure_theory.finite_measure.self_eq_mass_mul_normalize MeasureTheory.FiniteMeasure.self_eq_mass_mul_normalize theorem self_eq_mass_smul_normalize : μ = μ.mass • μ.normalize.toFiniteMeasure := by diff --git a/Mathlib/MeasureTheory/Measure/Restrict.lean b/Mathlib/MeasureTheory/Measure/Restrict.lean index 0f3b8268c8317..6580dba0637d0 100644 --- a/Mathlib/MeasureTheory/Measure/Restrict.lean +++ b/Mathlib/MeasureTheory/Measure/Restrict.lean @@ -60,12 +60,9 @@ theorem restrict_toOuterMeasure_eq_toOuterMeasure_restrict (h : MeasurableSet s) toMeasure_toOuterMeasure, OuterMeasure.restrict_trim h, μ.trimmed] #align measure_theory.measure.restrict_to_outer_measure_eq_to_outer_measure_restrict MeasureTheory.Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict -theorem restrict_apply₀ (ht : NullMeasurableSet t (μ.restrict s)) : μ.restrict s t = μ (t ∩ s) := - (toMeasure_apply₀ _ (fun s' hs' t => by - suffices μ (s ∩ t) = μ (s ∩ t ∩ s') + μ ((s ∩ t) \ s') by - simpa [← Set.inter_assoc, Set.inter_comm _ s, ← inter_diff_assoc] - exact le_toOuterMeasure_caratheodory _ _ hs' _) ht).trans <| by - simp only [OuterMeasure.restrict_apply] +theorem restrict_apply₀ (ht : NullMeasurableSet t (μ.restrict s)) : μ.restrict s t = μ (t ∩ s) := by + rw [← restrictₗ_apply, restrictₗ, liftLinear_apply₀ _ ht, OuterMeasure.restrict_apply, + coe_toOuterMeasure] #align measure_theory.measure.restrict_apply₀ MeasureTheory.Measure.restrict_apply₀ /-- If `t` is a measurable set, then the measure of `t` with respect to the restriction of @@ -106,8 +103,9 @@ the measure to `s` equals the outer measure of `t ∩ s`. This is an alternate v `Measure.restrict_apply`, requiring that `s` is measurable instead of `t`. -/ @[simp] theorem restrict_apply' (hs : MeasurableSet s) : μ.restrict s t = μ (t ∩ s) := by - rw [Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs, - OuterMeasure.restrict_apply s t _] + rw [← toOuterMeasure_apply, + Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict hs, + OuterMeasure.restrict_apply s t _, toOuterMeasure_apply] #align measure_theory.measure.restrict_apply' MeasureTheory.Measure.restrict_apply' theorem restrict_apply₀' (hs : NullMeasurableSet s μ) : μ.restrict s t = μ (t ∩ s) := by diff --git a/Mathlib/MeasureTheory/Measure/Tilted.lean b/Mathlib/MeasureTheory/Measure/Tilted.lean index e35bdb7e197e2..a69aec40e9d30 100644 --- a/Mathlib/MeasureTheory/Measure/Tilted.lean +++ b/Mathlib/MeasureTheory/Measure/Tilted.lean @@ -109,9 +109,8 @@ lemma tilted_apply_eq_ofReal_integral' {s : Set α} (f : α → ℝ) (hs : Measu · rw [tilted_apply' _ _ hs, ← ofReal_integral_eq_lintegral_ofReal] · exact hf.integrableOn.div_const _ · exact ae_of_all _ (fun _ ↦ by positivity) - · simp only [hf, not_false_eq_true, tilted_of_not_integrable, Measure.zero_toOuterMeasure, - OuterMeasure.coe_zero, Pi.zero_apply, integral_undef hf, div_zero, integral_zero, - ENNReal.ofReal_zero] + · simp only [hf, not_false_eq_true, tilted_of_not_integrable, Measure.coe_zero, + Pi.zero_apply, integral_undef hf, div_zero, integral_zero, ENNReal.ofReal_zero] lemma tilted_apply_eq_ofReal_integral [SFinite μ] (f : α → ℝ) (s : Set α) : μ.tilted f s = ENNReal.ofReal (∫ a in s, exp (f a) / ∫ x, exp (f x) ∂μ ∂μ) := by @@ -119,9 +118,7 @@ lemma tilted_apply_eq_ofReal_integral [SFinite μ] (f : α → ℝ) (s : Set α) · rw [tilted_apply _ _, ← ofReal_integral_eq_lintegral_ofReal] · exact hf.integrableOn.div_const _ · exact ae_of_all _ (fun _ ↦ by positivity) - · simp only [hf, not_false_eq_true, tilted_of_not_integrable, Measure.zero_toOuterMeasure, - OuterMeasure.coe_zero, Pi.zero_apply, integral_undef hf, div_zero, integral_zero, - ENNReal.ofReal_zero] + · simp [tilted_of_not_integrable hf, integral_undef hf] instance isFiniteMeasure_tilted : IsFiniteMeasure (μ.tilted f) := by by_cases hf : Integrable (fun x ↦ exp (f x)) μ diff --git a/Mathlib/MeasureTheory/Measure/Trim.lean b/Mathlib/MeasureTheory/Measure/Trim.lean index f836cf45d904b..b7782d9dbb9f0 100644 --- a/Mathlib/MeasureTheory/Measure/Trim.lean +++ b/Mathlib/MeasureTheory/Measure/Trim.lean @@ -52,7 +52,7 @@ theorem zero_trim (hm : m ≤ m0) : (0 : Measure α).trim hm = (0 : @Measure α #align measure_theory.zero_trim MeasureTheory.zero_trim theorem trim_measurableSet_eq (hm : m ≤ m0) (hs : @MeasurableSet α m s) : μ.trim hm s = μ s := by - rw [Measure.trim, toMeasure_apply (ms := m) _ _ hs] + rw [Measure.trim, toMeasure_apply (ms := m) _ _ hs, Measure.coe_toOuterMeasure] #align measure_theory.trim_measurable_set_eq MeasureTheory.trim_measurableSet_eq theorem le_trim (hm : m ≤ m0) : μ s ≤ μ.trim hm s := by diff --git a/Mathlib/MeasureTheory/Measure/Typeclasses.lean b/Mathlib/MeasureTheory/Measure/Typeclasses.lean index 1e585b62cb9c7..eec9c96cea0b6 100644 --- a/Mathlib/MeasureTheory/Measure/Typeclasses.lean +++ b/Mathlib/MeasureTheory/Measure/Typeclasses.lean @@ -498,7 +498,7 @@ theorem FiniteAtFilter.exists_mem_basis {f : Filter α} (hμ : FiniteAtFilter μ #align measure_theory.measure.finite_at_filter.exists_mem_basis MeasureTheory.Measure.FiniteAtFilter.exists_mem_basis theorem finiteAtBot {m0 : MeasurableSpace α} (μ : Measure α) : μ.FiniteAtFilter ⊥ := - ⟨∅, mem_bot, by simp only [OuterMeasure.empty', zero_lt_top]⟩ + ⟨∅, mem_bot, by simp only [measure_empty, zero_lt_top]⟩ #align measure_theory.measure.finite_at_bot MeasureTheory.Measure.finiteAtBot /-- `μ` has finite spanning sets in `C` if there is a countable sequence of sets in `C` that have @@ -1026,7 +1026,7 @@ theorem sigmaFinite_of_le (μ : Measure α) [hs : SigmaFinite μ] (h : ν ≤ μ ext s hs rw [← ENNReal.add_right_inj (measure_mono (inter_subset_right s _) |>.trans_lt <| measure_spanningSets_lt_top μ i).ne] - simp only [ext_iff', add_toOuterMeasure, OuterMeasure.coe_add, Pi.add_apply] at h + simp only [ext_iff', coe_add, Pi.add_apply] at h simp [hs, h] @[simp] lemma add_left_inj (μ ν₁ ν₂ : Measure α) [SigmaFinite μ] : @@ -1096,8 +1096,7 @@ instance SMul.sigmaFinite {μ : Measure α} [SigmaFinite μ] (c : ℝ≥0) : set_mem := fun _ ↦ trivial finite := by intro i - simp only [smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply, - nnreal_smul_coe_apply] + simp only [Measure.coe_smul, Pi.smul_apply, nnreal_smul_coe_apply] exact ENNReal.mul_lt_top ENNReal.coe_ne_top (measure_spanningSets_lt_top μ i).ne spanning := iUnion_spanningSets μ }⟩ diff --git a/Mathlib/Probability/ConditionalProbability.lean b/Mathlib/Probability/ConditionalProbability.lean index 24612c177be55..3bb4930797efb 100644 --- a/Mathlib/Probability/ConditionalProbability.lean +++ b/Mathlib/Probability/ConditionalProbability.lean @@ -92,8 +92,8 @@ theorem cond_isProbabilityMeasure_of_finite (hcs : μ s ≠ 0) (hs : μ s ≠ IsProbabilityMeasure μ[|s] := ⟨by unfold ProbabilityTheory.cond - simp only [Measure.smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply, - MeasurableSet.univ, Measure.restrict_apply, Set.univ_inter, smul_eq_mul] + simp only [Measure.coe_smul, Pi.smul_apply, MeasurableSet.univ, Measure.restrict_apply, + Set.univ_inter, smul_eq_mul] exact ENNReal.inv_mul_cancel hcs hs⟩ /-- The conditional probability measure of any finite measure on any set of positive measure @@ -104,9 +104,8 @@ theorem cond_isProbabilityMeasure [IsFiniteMeasure μ] (hcs : μ s ≠ 0) : instance cond_isFiniteMeasure : IsFiniteMeasure μ[|s] := by constructor - simp only [Measure.smul_toOuterMeasure, OuterMeasure.coe_smul, Pi.smul_apply, MeasurableSet.univ, - Measure.restrict_apply, Set.univ_inter, smul_eq_mul, ProbabilityTheory.cond, - ← ENNReal.div_eq_inv_mul] + simp only [Measure.coe_smul, Pi.smul_apply, MeasurableSet.univ, Measure.restrict_apply, + Set.univ_inter, smul_eq_mul, ProbabilityTheory.cond, ← ENNReal.div_eq_inv_mul] exact ENNReal.div_self_le_one.trans_lt ENNReal.one_lt_top theorem cond_toMeasurable_eq : @@ -234,8 +233,8 @@ lemma sum_meas_smul_cond_fiber {X : Ω → α} (hX : Measurable X) (μ : Measure ext E hE calc _ = ∑ x, μ (X ⁻¹' {x} ∩ E) := by - simp only [Measure.coe_finset_sum, smul_toOuterMeasure, OuterMeasure.coe_smul, - Finset.sum_apply, Pi.smul_apply, smul_eq_mul] + simp only [Measure.coe_finset_sum, Measure.coe_smul, Finset.sum_apply, + Pi.smul_apply, smul_eq_mul] simp_rw [mul_comm (μ _), cond_mul_eq_inter _ (hX (.singleton _))] _ = _ := by have : ⋃ x ∈ Finset.univ, X ⁻¹' {x} ∩ E = E := by simp; ext _; simp diff --git a/Mathlib/Probability/Kernel/Composition.lean b/Mathlib/Probability/Kernel/Composition.lean index 43cb16faff4c0..0afae13eb3457 100644 --- a/Mathlib/Probability/Kernel/Composition.lean +++ b/Mathlib/Probability/Kernel/Composition.lean @@ -580,8 +580,7 @@ lemma compProd_add_right (μ : kernel α β) (κ η : kernel (α × β) γ) [IsSFiniteKernel μ] [IsSFiniteKernel κ] [IsSFiniteKernel η] : μ ⊗ₖ (κ + η) = μ ⊗ₖ κ + μ ⊗ₖ η := by ext a s hs - simp only [compProd_apply _ _ _ hs, coeFn_add, Pi.add_apply, Measure.add_toOuterMeasure, - OuterMeasure.coe_add] + simp only [compProd_apply _ _ _ hs, coeFn_add, Pi.add_apply, Measure.coe_add] rw [lintegral_add_left] exact measurable_kernel_prod_mk_left' hs a diff --git a/Mathlib/Probability/Kernel/Disintegration/Density.lean b/Mathlib/Probability/Kernel/Disintegration/Density.lean index b7a7918012a99..81c302631d139 100644 --- a/Mathlib/Probability/Kernel/Disintegration/Density.lean +++ b/Mathlib/Probability/Kernel/Disintegration/Density.lean @@ -391,8 +391,7 @@ lemma tendsto_densityProcess_atTop_empty_of_antitone (κ : kernel α (γ × β)) simp only [le_eq_subset, prod_subset_prod_iff, subset_rfl, true_and] exact Or.inl <| hseq hmm' · exact ⟨0, measure_ne_top _ _⟩ - · simp only [prod_empty, OuterMeasure.empty', ne_eq, not_true_eq_false, false_or, h0, - not_false_iff] + · exact .inr h0 lemma tendsto_densityProcess_atTop_of_antitone (κ : kernel α (γ × β)) (ν : kernel α γ) [IsFiniteKernel κ] (n : ℕ) (a : α) (x : γ) @@ -674,7 +673,7 @@ lemma tendsto_integral_density_of_antitone (hκν : fst κ ≤ ν) [IsFiniteKern · refine ⟨0, measure_ne_top _ _⟩ convert h rw [← prod_iInter, hseq_iInter] - simp only [ne_eq, prod_empty, OuterMeasure.empty', forall_exists_index] + simp lemma tendsto_density_atTop_ae_of_antitone (hκν : fst κ ≤ ν) [IsFiniteKernel ν] (a : α) (seq : ℕ → Set β) (hseq : Antitone seq) (hseq_iInter : ⋂ i, seq i = ∅) diff --git a/Mathlib/Probability/Kernel/RadonNikodym.lean b/Mathlib/Probability/Kernel/RadonNikodym.lean index e89500c10fb88..d4b6b25a2c4a4 100644 --- a/Mathlib/Probability/Kernel/RadonNikodym.lean +++ b/Mathlib/Probability/Kernel/RadonNikodym.lean @@ -170,8 +170,7 @@ lemma withDensity_one_sub_rnDerivAux (κ η : kernel α γ) [IsFiniteKernel κ] = κ a s + η a s := by rw [this] simp - simp only [coeFn_add, Pi.add_apply, Measure.add_toOuterMeasure, OuterMeasure.coe_add] - at h + simp only [coeFn_add, Pi.add_apply, Measure.coe_add] at h rwa [withDensity_rnDerivAux, add_comm, ENNReal.add_right_inj (measure_ne_top _ _)] at h have : ∀ b, (Real.toNNReal b : ℝ≥0∞) = ENNReal.ofReal b := fun _ ↦ rfl simp_rw [this, ENNReal.ofReal_sub _ (rnDerivAux_nonneg h_le), ENNReal.ofReal_one] @@ -401,8 +400,7 @@ lemma rnDeriv_add_singularPart (κ η : kernel α γ) [IsFiniteKernel κ] [IsFin withDensity η (rnDeriv κ η) + singularPart κ η = κ := by ext a s hs rw [← inter_union_diff s (mutuallySingularSetSlice κ η a)] - simp only [coeFn_add, Pi.add_apply, Measure.add_toOuterMeasure, - OuterMeasure.coe_add] + simp only [coeFn_add, Pi.add_apply, Measure.coe_add] have hm := measurableSet_mutuallySingularSetSlice κ η a simp only [measure_union (Disjoint.mono (inter_subset_right _ _) subset_rfl disjoint_sdiff_right) (hs.diff hm)] @@ -459,7 +457,7 @@ lemma singularPart_eq_zero_iff_measure_eq_zero (κ η : kernel α γ) simp_rw [ext_iff, Measure.ext_iff] at h_eq_add specialize h_eq_add a (mutuallySingularSetSlice κ η a) (measurableSet_mutuallySingularSetSlice κ η a) - simp only [coeFn_add, Pi.add_apply, Measure.add_toOuterMeasure, OuterMeasure.coe_add, + simp only [coeFn_add, Pi.add_apply, Measure.coe_add, withDensity_rnDeriv_mutuallySingularSetSlice κ η, zero_add] at h_eq_add rw [← h_eq_add] exact singularPart_eq_zero_iff_apply_eq_zero κ η a @@ -471,7 +469,7 @@ lemma withDensity_rnDeriv_eq_zero_iff_measure_eq_zero (κ η : kernel α γ) simp_rw [ext_iff, Measure.ext_iff] at h_eq_add specialize h_eq_add a (mutuallySingularSetSlice κ η a)ᶜ (measurableSet_mutuallySingularSetSlice κ η a).compl - simp only [coeFn_add, Pi.add_apply, Measure.add_toOuterMeasure, OuterMeasure.coe_add, + simp only [coeFn_add, Pi.add_apply, Measure.coe_add, singularPart_compl_mutuallySingularSetSlice κ η, add_zero] at h_eq_add rw [← h_eq_add] exact withDensity_rnDeriv_eq_zero_iff_apply_eq_zero κ η a diff --git a/Mathlib/Probability/Variance.lean b/Mathlib/Probability/Variance.lean index 2109e0867211b..1ad72c6f4cecd 100644 --- a/Mathlib/Probability/Variance.lean +++ b/Mathlib/Probability/Variance.lean @@ -151,7 +151,7 @@ theorem evariance_eq_zero_iff (hX : AEMeasurable X μ) : using hω · rw [hω] simp - · measurability + · exact (hX.sub_const _).ennnorm.pow_const _ -- TODO `measurability` and `fun_prop` fail #align probability_theory.evariance_eq_zero_iff ProbabilityTheory.evariance_eq_zero_iff theorem evariance_mul (c : ℝ) (X : Ω → ℝ) (μ : Measure Ω) : From fcceeb1dd138f3969ddff60db830c196ae1b761f Mon Sep 17 00:00:00 2001 From: kkytola Date: Thu, 9 May 2024 11:24:52 +0000 Subject: [PATCH 13/15] feat: BoundedSub class to generalize subtraction of bounded continuous functions. (#12559) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Introduce type class `BoundedSub`, which allows to generalize subtraction of `BoundedContinuousFunction` to the case where the values are not necessarily in `SeminormedAddGroup`. The most important case for measure theory applications that is allowed by the generalization is bounded continuous functions with values in `ℝ≥0`. Co-authored-by: kkytola <39528102+kkytola@users.noreply.github.com> --- Mathlib.lean | 1 + .../Topology/Bornology/BoundedOperation.lean | 110 ++++++++++++++++++ .../Topology/ContinuousFunction/Bounded.lean | 37 +++--- .../Topology/MetricSpace/PseudoMetric.lean | 18 +++ 4 files changed, 151 insertions(+), 15 deletions(-) create mode 100644 Mathlib/Topology/Bornology/BoundedOperation.lean diff --git a/Mathlib.lean b/Mathlib.lean index d10438cf9a07b..298c2347f5bd7 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3904,6 +3904,7 @@ import Mathlib.Topology.Bases import Mathlib.Topology.Basic import Mathlib.Topology.Bornology.Absorbs import Mathlib.Topology.Bornology.Basic +import Mathlib.Topology.Bornology.BoundedOperation import Mathlib.Topology.Bornology.Constructions import Mathlib.Topology.Bornology.Hom import Mathlib.Topology.Category.Born diff --git a/Mathlib/Topology/Bornology/BoundedOperation.lean b/Mathlib/Topology/Bornology/BoundedOperation.lean new file mode 100644 index 0000000000000..e84b8fd1366b6 --- /dev/null +++ b/Mathlib/Topology/Bornology/BoundedOperation.lean @@ -0,0 +1,110 @@ +/- +Copyright (c) 2024 Kalle Kytölä +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kalle Kytölä +-/ +import Mathlib.Analysis.Normed.Group.Basic + +/-! +# Bounded operations + +This file introduces type classes for bornologically bounded operations. + +In particular, when combined with type classes which guarantee continuity of the same operations, +we can equip bounded continuous functions with the corresponding operations. + +## Main definitions + +* `BoundedSub R`: a class guaranteeing boundedness of subtraction. + +TODO: +* Add bounded multiplication. (So that, e.g., multiplication works in `X →ᵇ ℝ≥0`.) + +-/ + +section bounded_sub +/-! +### Bounded subtraction +-/ + +open Pointwise + +/-- A typeclass saying that `(p : R × R) ↦ p.1 - p.2` maps any pair of bounded sets to a bounded +set. This property automatically holds for seminormed additive groups, but it also holds, e.g., +for `ℝ≥0`. -/ +class BoundedSub (R : Type*) [Bornology R] [Sub R] : Prop where + isBounded_sub : ∀ {s t : Set R}, + Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s - t) + +variable {R : Type*} + +lemma isBounded_sub [Bornology R] [Sub R] [BoundedSub R] {s t : Set R} + (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) : + Bornology.IsBounded (s - t) := BoundedSub.isBounded_sub hs ht + +lemma sub_bounded_of_bounded_of_bounded {X : Type*} [PseudoMetricSpace R] [Sub R] [BoundedSub R] + {f g : X → R} (f_bdd : ∃ C, ∀ x y, dist (f x) (f y) ≤ C) + (g_bdd : ∃ C, ∀ x y, dist (g x) (g y) ≤ C) : + ∃ C, ∀ x y, dist ((f - g) x) ((f - g) y) ≤ C := by + obtain ⟨C, hC⟩ := Metric.isBounded_iff.mp <| + isBounded_sub (Metric.isBounded_range_iff.mpr f_bdd) (Metric.isBounded_range_iff.mpr g_bdd) + use C + intro x y + exact hC (Set.sub_mem_sub (Set.mem_range_self (f := f) x) (Set.mem_range_self (f := g) x)) + (Set.sub_mem_sub (Set.mem_range_self (f := f) y) (Set.mem_range_self (f := g) y)) + +end bounded_sub + +section SeminormedAddCommGroup +/-! +### Bounded operations in seminormed additive commutative groups +-/ + +variable {R : Type*} [SeminormedAddCommGroup R] + +lemma SeminormedAddCommGroup.lipschitzWith_sub : + LipschitzWith 2 (fun (p : R × R) ↦ p.1 - p.2) := by + convert LipschitzWith.prod_fst.sub LipschitzWith.prod_snd + norm_num + +instance : BoundedSub R where + isBounded_sub := by + intro s t hs ht + rw [Metric.isBounded_iff] at hs ht ⊢ + obtain ⟨Cf, hf⟩ := hs + obtain ⟨Cg, hg⟩ := ht + use Cf + Cg + intro z hz w hw + obtain ⟨x₁, hx₁, y₁, hy₁, z_eq⟩ := Set.mem_sub.mp hz + obtain ⟨x₂, hx₂, y₂, hy₂, w_eq⟩ := Set.mem_sub.mp hw + rw [← w_eq, ← z_eq, dist_eq_norm] + calc ‖x₁ - y₁ - (x₂ - y₂)‖ + _ = ‖x₁ - x₂ + (y₂ - y₁)‖ := by + rw [sub_sub_sub_comm, sub_eq_add_neg, neg_sub] + _ ≤ ‖x₁ - x₂‖ + ‖y₂ - y₁‖ := norm_add_le _ _ + _ ≤ Cf + Cg := + add_le_add (mem_closedBall_iff_norm.mp (hf hx₁ hx₂)) + (mem_closedBall_iff_norm.mp (hg hy₂ hy₁)) + +end SeminormedAddCommGroup + +section NNReal +/-! +### Bounded operations in ℝ≥0 +-/ + +open scoped NNReal + +noncomputable instance : BoundedSub ℝ≥0 where + isBounded_sub := by + intro s t hs _ + obtain ⟨c, hc⟩ := (Metric.isBounded_iff_subset_ball 0).mp hs + apply (Metric.isBounded_iff_subset_ball 0).mpr + use c + intro z hz + obtain ⟨a, a_in_s, b, _, z_eq⟩ := Set.mem_sub.mp hz + have key := hc a_in_s + simp only [NNReal.ball_zero_eq_Ico, ← z_eq, Set.mem_Ico, zero_le, true_and, gt_iff_lt] at * + exact tsub_lt_of_lt key + +end NNReal diff --git a/Mathlib/Topology/ContinuousFunction/Bounded.lean b/Mathlib/Topology/ContinuousFunction/Bounded.lean index 39ec9997fa04d..1367c04083dcc 100644 --- a/Mathlib/Topology/ContinuousFunction/Bounded.lean +++ b/Mathlib/Topology/ContinuousFunction/Bounded.lean @@ -9,6 +9,7 @@ import Mathlib.Analysis.Normed.Order.Lattice import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic import Mathlib.Analysis.NormedSpace.Star.Basic import Mathlib.Analysis.NormedSpace.ContinuousLinearMap +import Mathlib.Topology.Bornology.BoundedOperation #align_import topology.continuous_function.bounded from "leanprover-community/mathlib"@"5dc275ec639221ca4d5f56938eb966f6ad9bc89f" @@ -767,6 +768,27 @@ theorem sum_apply {ι : Type*} (s : Finset ι) (f : ι → α →ᵇ β) (a : α end CommHasLipschitzAdd +section sub + +variable [TopologicalSpace α] +variable {R : Type*} [PseudoMetricSpace R] [Sub R] [BoundedSub R] [ContinuousSub R] +variable (f g : α →ᵇ R) + +/-- The pointwise difference of two bounded continuous functions is again bounded continuous. -/ +instance instSub : Sub (α →ᵇ R) where + sub f g := + { toFun := fun x ↦ (f x - g x), + map_bounded' := sub_bounded_of_bounded_of_bounded f.map_bounded' g.map_bounded' } + +theorem sub_apply {x : α} : (f - g) x = f x - g x := rfl +#align bounded_continuous_function.sub_apply BoundedContinuousFunction.sub_apply + +@[simp] +theorem coe_sub : ⇑(f - g) = f - g := rfl +#align bounded_continuous_function.coe_sub BoundedContinuousFunction.coe_sub + +end sub + section NormedAddCommGroup /- In this section, if `β` is a normed group, then we show that the space of bounded @@ -928,14 +950,6 @@ instance : Neg (α →ᵇ β) := ofNormedAddCommGroup (-f) f.continuous.neg ‖f‖ fun x => norm_neg ((⇑f) x) ▸ f.norm_coe_le_norm x⟩ -/-- The pointwise difference of two bounded continuous functions is again bounded continuous. -/ -instance instSub : Sub (α →ᵇ β) := - ⟨fun f g => - ofNormedAddCommGroup (f - g) (f.continuous.sub g.continuous) (‖f‖ + ‖g‖) fun x => by - simp only [sub_eq_add_neg] - exact le_trans (norm_add_le _ _) - (add_le_add (f.norm_coe_le_norm x) <| norm_neg ((⇑g) x) ▸ g.norm_coe_le_norm x)⟩ - @[simp] theorem coe_neg : ⇑(-f) = -f := rfl #align bounded_continuous_function.coe_neg BoundedContinuousFunction.coe_neg @@ -943,13 +957,6 @@ theorem coe_neg : ⇑(-f) = -f := rfl theorem neg_apply : (-f) x = -f x := rfl #align bounded_continuous_function.neg_apply BoundedContinuousFunction.neg_apply -@[simp] -theorem coe_sub : ⇑(f - g) = f - g := rfl -#align bounded_continuous_function.coe_sub BoundedContinuousFunction.coe_sub - -theorem sub_apply : (f - g) x = f x - g x := rfl -#align bounded_continuous_function.sub_apply BoundedContinuousFunction.sub_apply - @[simp] theorem mkOfCompact_neg [CompactSpace α] (f : C(α, β)) : mkOfCompact (-f) = -mkOfCompact f := rfl #align bounded_continuous_function.mk_of_compact_neg BoundedContinuousFunction.mkOfCompact_neg diff --git a/Mathlib/Topology/MetricSpace/PseudoMetric.lean b/Mathlib/Topology/MetricSpace/PseudoMetric.lean index d68b679507d24..3df6331ced896 100644 --- a/Mathlib/Topology/MetricSpace/PseudoMetric.lean +++ b/Mathlib/Topology/MetricSpace/PseudoMetric.lean @@ -1592,6 +1592,24 @@ theorem NNReal.le_add_nndist (a b : ℝ≥0) : a ≤ b + nndist a b := by exact le_of_abs_le (dist_eq a b).ge #align nnreal.le_add_nndist NNReal.le_add_nndist +lemma NNReal.ball_zero_eq_Ico' (c : ℝ≥0) : + Metric.ball (0 : ℝ≥0) c.toReal = Set.Ico 0 c := by ext x; simp + +lemma NNReal.ball_zero_eq_Ico (c : ℝ) : + Metric.ball (0 : ℝ≥0) c = Set.Ico 0 c.toNNReal := by + by_cases c_pos : 0 < c + · convert NNReal.ball_zero_eq_Ico' ⟨c, c_pos.le⟩ + simp [Real.toNNReal, c_pos.le] + simp [not_lt.mp c_pos] + +lemma NNReal.closedBall_zero_eq_Icc' (c : ℝ≥0) : + Metric.closedBall (0 : ℝ≥0) c.toReal = Set.Icc 0 c := by ext x; simp + +lemma NNReal.closedBall_zero_eq_Icc {c : ℝ} (c_nn : 0 ≤ c) : + Metric.closedBall (0 : ℝ≥0) c = Set.Icc 0 c.toNNReal := by + convert NNReal.closedBall_zero_eq_Icc' ⟨c, c_nn⟩ + simp [Real.toNNReal, c_nn] + end NNReal section ULift From 690d741a2041d5670fd10338b772280cca9b47cd Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 9 May 2024 12:14:53 +0000 Subject: [PATCH 14/15] chore: more deprecations (#12783) --- Mathlib/CategoryTheory/Comma/Basic.lean | 2 +- Mathlib/NumberTheory/Cyclotomic/Discriminant.lean | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/CategoryTheory/Comma/Basic.lean b/Mathlib/CategoryTheory/Comma/Basic.lean index f4eba4336d152..d8940c2f3c405 100644 --- a/Mathlib/CategoryTheory/Comma/Basic.lean +++ b/Mathlib/CategoryTheory/Comma/Basic.lean @@ -239,7 +239,7 @@ instance full_map [F.Faithful] [F₁.Full] [F₂.Full] [IsIso α] [IsIso β] : ( assoc, assoc] erw [← α.naturality_assoc, β.naturality] dsimp - rw [F₁.image_preimage, F₂.image_preimage] + rw [F₁.map_preimage, F₂.map_preimage] simpa using φ.w) }, by aesop_cat⟩ instance essSurj_map [F₁.EssSurj] [F₂.EssSurj] [F.Full] [IsIso α] [IsIso β] : diff --git a/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean b/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean index fe2b8906b5426..9103e79d5a238 100644 --- a/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean +++ b/Mathlib/NumberTheory/Cyclotomic/Discriminant.lean @@ -102,8 +102,8 @@ theorem discr_prime_pow_ne_two [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : F replace H := congr_arg (Algebra.norm K) H have hnorm : (norm K) (ζ ^ (p : ℕ) ^ k - 1) = (p : K) ^ (p : ℕ) ^ k := by by_cases hp : p = 2 - · exact mod_cast hζ.pow_sub_one_norm_prime_pow_of_ne_zero hirr le_rfl (hp2 hp) - · exact mod_cast hζ.pow_sub_one_norm_prime_ne_two hirr le_rfl hp + · exact mod_cast hζ.norm_pow_sub_one_eq_prime_pow_of_ne_zero hirr le_rfl (hp2 hp) + · exact mod_cast hζ.norm_pow_sub_one_of_prime_ne_two hirr le_rfl hp rw [MonoidHom.map_mul, hnorm, MonoidHom.map_mul, ← map_natCast (algebraMap K L), Algebra.norm_algebraMap, finrank L hirr] at H conv_rhs at H => -- Porting note: need to drill down to successfully rewrite the totient From fa33d89fc6f3890f5bf7188abae01b6baacab8d5 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 9 May 2024 16:03:52 +0000 Subject: [PATCH 15/15] feat: basic definition of comonoid objects (#10091) Co-authored-by: Scott Morrison Co-authored-by: Scott Morrison --- Mathlib.lean | 1 + Mathlib/CategoryTheory/Monoidal/Comon_.lean | 171 ++++++++++++++++++++ 2 files changed, 172 insertions(+) create mode 100644 Mathlib/CategoryTheory/Monoidal/Comon_.lean diff --git a/Mathlib.lean b/Mathlib.lean index 298c2347f5bd7..b4f5569dc57c5 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1442,6 +1442,7 @@ import Mathlib.CategoryTheory.Monoidal.Category import Mathlib.CategoryTheory.Monoidal.Center import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas import Mathlib.CategoryTheory.Monoidal.CommMon_ +import Mathlib.CategoryTheory.Monoidal.Comon_ import Mathlib.CategoryTheory.Monoidal.Discrete import Mathlib.CategoryTheory.Monoidal.End import Mathlib.CategoryTheory.Monoidal.Free.Basic diff --git a/Mathlib/CategoryTheory/Monoidal/Comon_.lean b/Mathlib/CategoryTheory/Monoidal/Comon_.lean new file mode 100644 index 0000000000000..85fd2f2198266 --- /dev/null +++ b/Mathlib/CategoryTheory/Monoidal/Comon_.lean @@ -0,0 +1,171 @@ +/- +Copyright (c) 2024 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Kim Morrison +-/ +import Mathlib.CategoryTheory.Monoidal.CoherenceLemmas +import Mathlib.CategoryTheory.Limits.Shapes.Terminal + +/-! +# The category of comonoids in a monoidal category. + +We define comonoids in a monoidal category `C`. + +## TODO +* `Comon_ C ≌ Mon_ (Cᵒᵖ)` +* An oplax monoidal functor takes comonoid objects to comonoid objects. + That is, a oplax monoidal functor `F : C ⥤ D` induces a functor `Comon_ C ⥤ Comon_ D`. +* Comonoid objects in `C` are "just" + oplax monoidal functors from the trivial monoidal category to `C`. +* The category of comonoids in a braided monoidal category is monoidal. + (It may suffice to transfer this across the equivalent to monoids in the opposite category.) + +-/ + +universe v₁ v₂ u₁ u₂ u + +open CategoryTheory MonoidalCategory + +variable (C : Type u₁) [Category.{v₁} C] [MonoidalCategory.{v₁} C] + +/-- A comonoid object internal to a monoidal category. + +When the monoidal category is preadditive, this is also sometimes called a "coalgebra object". +-/ +structure Comon_ where + /-- The underlying object of a comonoid object. -/ + X : C + /-- The counit of a comonoid object. -/ + counit : X ⟶ 𝟙_ C + /-- The comultiplication morphism of a comonoid object. -/ + comul : X ⟶ X ⊗ X + counit_comul : comul ≫ (counit ▷ X) = (λ_ X).inv := by aesop_cat + comul_counit : comul ≫ (X ◁ counit) = (ρ_ X).inv := by aesop_cat + comul_assoc : comul ≫ (X ◁ comul) ≫ (α_ X X X).inv = comul ≫ (comul ▷ X) := by aesop_cat + +attribute [reassoc] Comon_.counit_comul Comon_.comul_counit + +attribute [reassoc (attr := simp)] Comon_.comul_assoc + +namespace Comon_ + +/-- The trivial comonoid object. We later show this is terminal in `Comon_ C`. +-/ +@[simps] +def trivial : Comon_ C where + X := 𝟙_ C + counit := 𝟙 _ + comul := (λ_ _).inv + comul_assoc := by coherence + counit_comul := by coherence + comul_counit := by coherence + +instance : Inhabited (Comon_ C) := + ⟨trivial C⟩ + +variable {C} +variable {M : Comon_ C} + +@[reassoc (attr := simp)] +theorem counit_comul_hom {Z : C} (f : M.X ⟶ Z) : M.comul ≫ (M.counit ⊗ f) = f ≫ (λ_ Z).inv := by + rw [leftUnitor_inv_naturality, tensorHom_def, counit_comul_assoc] + +@[reassoc (attr := simp)] +theorem comul_counit_hom {Z : C} (f : M.X ⟶ Z) : M.comul ≫ (f ⊗ M.counit) = f ≫ (ρ_ Z).inv := by + rw [rightUnitor_inv_naturality, tensorHom_def', comul_counit_assoc] + +@[reassoc (attr := simp)] theorem comul_assoc_flip : + M.comul ≫ (M.comul ▷ M.X) ≫ (α_ M.X M.X M.X).hom = M.comul ≫ (M.X ◁ M.comul) := by + simp [← comul_assoc_assoc] + +/-- A morphism of comonoid objects. -/ +@[ext] +structure Hom (M N : Comon_ C) where + /-- The underlying morphism of a morphism of comonoid objects. -/ + hom : M.X ⟶ N.X + hom_counit : hom ≫ N.counit = M.counit := by aesop_cat + hom_comul : hom ≫ N.comul = M.comul ≫ (hom ⊗ hom) := by aesop_cat + +attribute [reassoc (attr := simp)] Hom.hom_counit Hom.hom_comul + +/-- The identity morphism on a comonoid object. -/ +@[simps] +def id (M : Comon_ C) : Hom M M where + hom := 𝟙 M.X + +instance homInhabited (M : Comon_ C) : Inhabited (Hom M M) := + ⟨id M⟩ + +/-- Composition of morphisms of monoid objects. -/ +@[simps] +def comp {M N O : Comon_ C} (f : Hom M N) (g : Hom N O) : Hom M O where + hom := f.hom ≫ g.hom + +instance : Category (Comon_ C) where + Hom M N := Hom M N + id := id + comp f g := comp f g + +@[ext] lemma ext {X Y : Comon_ C} {f g : X ⟶ Y} (w : f.hom = g.hom) : f = g := Hom.ext _ _ w + +@[simp] theorem id_hom' (M : Comon_ C) : (𝟙 M : Hom M M).hom = 𝟙 M.X := rfl + +@[simp] +theorem comp_hom' {M N K : Comon_ C} (f : M ⟶ N) (g : N ⟶ K) : (f ≫ g).hom = f.hom ≫ g.hom := + rfl + +section + +variable (C) + +/-- The forgetful functor from comonoid objects to the ambient category. -/ +@[simps] +def forget : Comon_ C ⥤ C where + obj A := A.X + map f := f.hom + +end + +instance forget_faithful : (@forget C _ _).Faithful where + +instance {A B : Comon_ C} (f : A ⟶ B) [e : IsIso ((forget C).map f)] : IsIso f.hom := e + +/-- The forgetful functor from comonoid objects to the ambient category reflects isomorphisms. -/ +instance : (forget C).ReflectsIsomorphisms where + reflects f e := + ⟨⟨{ hom := inv f.hom }, by aesop_cat⟩⟩ + +/-- Construct an isomorphism of monoids by giving an isomorphism between the underlying objects +and checking compatibility with unit and multiplication only in the forward direction. +-/ +@[simps] +def mkIso {M N : Comon_ C} (f : M.X ≅ N.X) (f_counit : f.hom ≫ N.counit = M.counit) + (f_comul : f.hom ≫ N.comul = M.comul ≫ (f.hom ⊗ f.hom)) : M ≅ N where + hom := + { hom := f.hom + hom_counit := f_counit + hom_comul := f_comul } + inv := + { hom := f.inv + hom_counit := by rw [← f_counit]; simp + hom_comul := by + rw [← cancel_epi f.hom] + slice_rhs 1 2 => rw [f_comul] + simp } + +instance uniqueHomToTrivial (A : Comon_ C) : Unique (A ⟶ trivial C) where + default := + { hom := A.counit + hom_counit := by dsimp; simp + hom_comul := by dsimp; simp [A.comul_counit, unitors_inv_equal] } + uniq f := by + ext; simp + rw [← Category.comp_id f.hom] + erw [f.hom_counit] + +open CategoryTheory.Limits + +instance : HasTerminal (Comon_ C) := + hasTerminal_of_unique (trivial C) + +end Comon_