bump to nightly-2023-06-01-09

mathlib commit leanprover-community/mathlib@cca4078

Mathbin/Algebra/Category/Module/Images.lean

@@ -38,41 +38,32 @@ attribute [local ext] Subtype.ext_val
 
 section
 
-#print ModuleCat.image /-
 -- implementation details of `has_image` for Module; use the API, not these
 /-- The image of a morphism in `Module R` is just the bundling of `linear_map.range f` -/
 def image : ModuleCat R :=
   ModuleCat.of R (LinearMap.range f)
 #align Module.image ModuleCat.image
--/
 
-#print ModuleCat.image.ι /-
 /-- The inclusion of `image f` into the target -/
 def image.ι : image f ⟶ H :=
   f.range.Subtype
 #align Module.image.ι ModuleCat.image.ι
--/
 
 instance : Mono (image.ι f) :=
   ConcreteCategory.mono_of_injective (image.ι f) Subtype.val_injective
 
-#print ModuleCat.factorThruImage /-
 /-- The corestriction map to the image -/
 def factorThruImage : G ⟶ image f :=
   f.range_restrict
 #align Module.factor_thru_image ModuleCat.factorThruImage
--/
 
-#print ModuleCat.image.fac /-
 theorem image.fac : factorThruImage f ≫ image.ι f = f := by ext; rfl
 #align Module.image.fac ModuleCat.image.fac
--/
 
 attribute [local simp] image.fac
 
 variable {f}
 
-#print ModuleCat.image.lift /-
 /-- The universal property for the image factorisation -/
 noncomputable def image.lift (F' : MonoFactorisation f) : image f ⟶ F'.i
     where
@@ -98,39 +89,32 @@ noncomputable def image.lift (F' : MonoFactorisation f) : image f ⟶ F'.i
     rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
     rfl
 #align Module.image.lift ModuleCat.image.lift
--/
 
-#print ModuleCat.image.lift_fac /-
 theorem image.lift_fac (F' : MonoFactorisation f) : image.lift F' ≫ F'.m = image.ι f :=
   by
   ext x
   change (F'.e ≫ F'.m) _ = _
   rw [F'.fac, (Classical.indefiniteDescription _ x.2).2]
   rfl
 #align Module.image.lift_fac ModuleCat.image.lift_fac
--/
 
 end
 
-#print ModuleCat.monoFactorisation /-
 /-- The factorisation of any morphism in `Module R` through a mono. -/
 def monoFactorisation : MonoFactorisation f
     where
   i := image f
   m := image.ι f
   e := factorThruImage f
 #align Module.mono_factorisation ModuleCat.monoFactorisation
--/
 
-#print ModuleCat.isImage /-
 /-- The factorisation of any morphism in `Module R` through a mono has the universal property of
 the image. -/
 noncomputable def isImage : IsImage (monoFactorisation f)
     where
   lift := image.lift
   lift_fac := image.lift_fac
 #align Module.is_image ModuleCat.isImage
--/
 
 /-- The categorical image of a morphism in `Module R`
 agrees with the linear algebraic range.
@@ -146,13 +130,11 @@ theorem imageIsoRange_inv_image_ι {G H : ModuleCat.{v} R} (f : G ⟶ H) :
   IsImage.isoExt_inv_m _ _
 #align Module.image_iso_range_inv_image_ι ModuleCat.imageIsoRange_inv_image_ι
 
-#print ModuleCat.imageIsoRange_hom_subtype /-
 @[simp, reassoc, elementwise]
 theorem imageIsoRange_hom_subtype {G H : ModuleCat.{v} R} (f : G ⟶ H) :
     (imageIsoRange f).hom ≫ ModuleCat.ofHom f.range.Subtype = Limits.image.ι f := by
   erw [← image_iso_range_inv_image_ι f, iso.hom_inv_id_assoc]
 #align Module.image_iso_range_hom_subtype ModuleCat.imageIsoRange_hom_subtype
--/
 
 end ModuleCat
 

Mathbin/Analysis/Calculus/BumpFunctionFindim.lean

@@ -137,18 +137,18 @@ theorem IsOpen.exists_smooth_support_eq {s : Set E} (hs : IsOpen s) :
   obtain ⟨δ, δpos, c, δc, c_lt⟩ :
     ∃ δ : ℕ → ℝ≥0, (∀ i : ℕ, 0 < δ i) ∧ ∃ c : NNReal, HasSum δ c ∧ c < 1
   exact NNReal.exists_pos_sum_of_countable one_ne_zero ℕ
-  have : ∀ n : ℕ, ∃ r : ℝ, 0 < r ∧ ∀ i ≤ n, ∀ x, ‖iteratedFderiv ℝ i (r • g n) x‖ ≤ δ n :=
+  have : ∀ n : ℕ, ∃ r : ℝ, 0 < r ∧ ∀ i ≤ n, ∀ x, ‖iteratedFDeriv ℝ i (r • g n) x‖ ≤ δ n :=
     by
     intro n
-    have : ∀ i, ∃ R, ∀ x, ‖iteratedFderiv ℝ i (fun x => g n x) x‖ ≤ R :=
+    have : ∀ i, ∃ R, ∀ x, ‖iteratedFDeriv ℝ i (fun x => g n x) x‖ ≤ R :=
       by
       intro i
-      have : BddAbove (range fun x => ‖iteratedFderiv ℝ i (fun x : E => g n x) x‖) :=
+      have : BddAbove (range fun x => ‖iteratedFDeriv ℝ i (fun x : E => g n x) x‖) :=
         by
         apply
-          ((g_smooth n).continuous_iteratedFderiv le_top).norm.bddAbove_range_of_hasCompactSupport
+          ((g_smooth n).continuous_iteratedFDeriv le_top).norm.bddAbove_range_of_hasCompactSupport
         apply HasCompactSupport.comp_left _ norm_zero
-        apply (g_comp_supp n).iteratedFderiv
+        apply (g_comp_supp n).iteratedFDeriv
       rcases this with ⟨R, hR⟩
       exact ⟨R, fun x => hR (mem_range_self _)⟩
     choose R hR using this
@@ -164,9 +164,9 @@ theorem IsOpen.exists_smooth_support_eq {s : Set E} (hs : IsOpen s) :
       linarith
     refine' ⟨M⁻¹ * δ n, by positivity, fun i hi x => _⟩
     calc
-      ‖iteratedFderiv ℝ i ((M⁻¹ * δ n) • g n) x‖ = ‖(M⁻¹ * δ n) • iteratedFderiv ℝ i (g n) x‖ := by
-        rw [iteratedFderiv_const_smul_apply]; exact (g_smooth n).of_le le_top
-      _ = M⁻¹ * δ n * ‖iteratedFderiv ℝ i (g n) x‖ := by rw [norm_smul, Real.norm_of_nonneg];
+      ‖iteratedFDeriv ℝ i ((M⁻¹ * δ n) • g n) x‖ = ‖(M⁻¹ * δ n) • iteratedFDeriv ℝ i (g n) x‖ := by
+        rw [iteratedFDeriv_const_smul_apply]; exact (g_smooth n).of_le le_top
+      _ = M⁻¹ * δ n * ‖iteratedFDeriv ℝ i (g n) x‖ := by rw [norm_smul, Real.norm_of_nonneg];
         positivity
       _ ≤ M⁻¹ * δ n * M := (mul_le_mul_of_nonneg_left ((hR i x).trans (IR i hi)) (by positivity))
       _ = δ n := by field_simp [M_pos.ne']
@@ -177,7 +177,7 @@ theorem IsOpen.exists_smooth_support_eq {s : Set E} (hs : IsOpen s) :
     intro x
     refine' summable_of_nnnorm_bounded _ δc.summable fun n => _
     rw [← NNReal.coe_le_coe, coe_nnnorm]
-    simpa only [norm_iteratedFderiv_zero] using hr n 0 (zero_le n) x
+    simpa only [norm_iteratedFDeriv_zero] using hr n 0 (zero_le n) x
   refine' ⟨fun x => ∑' n, (r n • g n) x, _, _, _⟩
   · apply subset.antisymm
     · intro x hx
@@ -206,7 +206,7 @@ theorem IsOpen.exists_smooth_support_eq {s : Set E} (hs : IsOpen s) :
     apply tsum_le_tsum _ (S y) A.summable
     intro n
     apply (le_abs_self _).trans
-    simpa only [norm_iteratedFderiv_zero] using hr n 0 (zero_le n) y
+    simpa only [norm_iteratedFDeriv_zero] using hr n 0 (zero_le n) y
 #align is_open.exists_smooth_support_eq IsOpen.exists_smooth_support_eq
 
 end