chore: rename away from 'def' (#11548)

This will become an error in 2024-03-16 nightly, possibly not permanently.



Co-authored-by: Scott Morrison <scott@tqft.net>

Archive/Imo/Imo2006Q5.lean

@@ -150,8 +150,9 @@ theorem imo2006_q5' {P : Polynomial ℤ} (hP : 1 < P.natDegree) :
   -- Otherwise, take a, b with P(a) = b, P(b) = a, a ≠ b.
   · rcases Finset.not_subset.1 H with ⟨a, ha, hab⟩
     replace ha := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ha)
-    rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ha
-    rw [Multiset.mem_toFinset, mem_roots hPX', IsRoot.def, eval_sub, eval_X, sub_eq_zero] at hab
+    rw [IsRoot.definition, eval_sub, eval_comp, eval_X, sub_eq_zero] at ha
+    rw [Multiset.mem_toFinset, mem_roots hPX', IsRoot.definition, eval_sub, eval_X, sub_eq_zero]
+      at hab
     set b := P.eval a
     -- More auxiliary lemmas on degrees.
     have hPab : (P + (X : ℤ[X]) - a - b).natDegree = P.natDegree := by
@@ -175,9 +176,9 @@ theorem imo2006_q5' {P : Polynomial ℤ} (hP : 1 < P.natDegree) :
     · -- Let t be a root of P(P(t)) - t, define u = P(t).
       intro t ht
       replace ht := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ht)
-      rw [IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero] at ht
-      simp only [mem_roots hPab', sub_eq_iff_eq_add, Multiset.mem_toFinset, IsRoot.def, eval_sub,
-        eval_add, eval_X, eval_C, eval_int_cast, Int.cast_id, zero_add]
+      rw [IsRoot.definition, eval_sub, eval_comp, eval_X, sub_eq_zero] at ht
+      simp only [mem_roots hPab', sub_eq_iff_eq_add, Multiset.mem_toFinset, IsRoot.definition,
+        eval_sub, eval_add, eval_X, eval_C, eval_int_cast, Int.cast_id, zero_add]
       -- An auxiliary lemma proved earlier implies we only need to show |t - a| = |u - b| and
       -- |t - b| = |u - a|. We prove this by establishing that each side of either equation divides
       -- the other.
@@ -200,7 +201,8 @@ theorem imo2006_q5 {P : Polynomial ℤ} (hP : 1 < P.natDegree) {k : ℕ} (hk : 0
   have hP' : P.comp P - X ≠ 0 := by
     simpa [Nat.iterate] using Polynomial.iterate_comp_sub_X_ne hP zero_lt_two
   replace ht := isRoot_of_mem_roots (Multiset.mem_toFinset.1 ht)
-  rw [IsRoot.def, eval_sub, iterate_comp_eval, eval_X, sub_eq_zero] at ht
-  rw [Multiset.mem_toFinset, mem_roots hP', IsRoot.def, eval_sub, eval_comp, eval_X, sub_eq_zero]
+  rw [IsRoot.definition, eval_sub, iterate_comp_eval, eval_X, sub_eq_zero] at ht
+  rw [Multiset.mem_toFinset, mem_roots hP', IsRoot.definition, eval_sub, eval_comp, eval_X,
+    sub_eq_zero]
   exact Polynomial.isPeriodicPt_eval_two ⟨k, hk, ht⟩
 #align imo2006_q5 imo2006_q5

Mathlib/Algebra/LinearRecurrence.lean

@@ -216,7 +216,7 @@ def charPoly : α[X] :=
   `q` is a root of `E`'s characteristic polynomial. -/
 theorem geom_sol_iff_root_charPoly (q : α) :
     (E.IsSolution fun n ↦ q ^ n) ↔ E.charPoly.IsRoot q := by
-  rw [charPoly, Polynomial.IsRoot.def, Polynomial.eval]
+  rw [charPoly, Polynomial.IsRoot.definition, Polynomial.eval]
   simp only [Polynomial.eval₂_finset_sum, one_mul, RingHom.id_apply, Polynomial.eval₂_monomial,
     Polynomial.eval₂_sub]
   constructor

Mathlib/Analysis/Asymptotics/Asymptotics.lean

@@ -191,16 +191,18 @@ alias ⟨IsLittleO.bound, IsLittleO.of_bound⟩ := isLittleO_iff
 #align asymptotics.is_o.bound Asymptotics.IsLittleO.bound
 #align asymptotics.is_o.of_bound Asymptotics.IsLittleO.of_bound
 
-theorem IsLittleO.def (h : f =o[l] g) (hc : 0 < c) : ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ :=
+-- Adaptation note: 2024-03-15: this was called `def`.
+-- Should lean be changed to allow that as a name again?
+theorem IsLittleO.definition (h : f =o[l] g) (hc : 0 < c) : ∀ᶠ x in l, ‖f x‖ ≤ c * ‖g x‖ :=
   isLittleO_iff.1 h hc
-#align asymptotics.is_o.def Asymptotics.IsLittleO.def
+#align asymptotics.is_o.def Asymptotics.IsLittleO.definition
 
 theorem IsLittleO.def' (h : f =o[l] g) (hc : 0 < c) : IsBigOWith c l f g :=
   isBigOWith_iff.2 <| isLittleO_iff.1 h hc
 #align asymptotics.is_o.def' Asymptotics.IsLittleO.def'
 
 theorem IsLittleO.eventuallyLE (h : f =o[l] g) : ∀ᶠ x in l, ‖f x‖ ≤ ‖g x‖ := by
-  simpa using h.def zero_lt_one
+  simpa using h.definition zero_lt_one
 
 end Defs
 
@@ -278,7 +280,7 @@ theorem isLittleO_iff_nat_mul_le_aux (h₀ : (∀ x, 0 ≤ ‖f x‖) ∨ ∀ x,
     f =o[l] g ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖f x‖ ≤ ‖g x‖ := by
   constructor
   · rintro H (_ | n)
-    · refine' (H.def one_pos).mono fun x h₀' => _
+    · refine' (H.definition one_pos).mono fun x h₀' => _
       rw [Nat.cast_zero, zero_mul]
       refine' h₀.elim (fun hf => (hf x).trans _) fun hg => hg x
       rwa [one_mul] at h₀'

Mathlib/Analysis/BoxIntegral/DivergenceTheorem.lean

@@ -242,8 +242,8 @@ theorem hasIntegral_GP_pderiv (f : (Fin (n + 1) → ℝ) → E)
     /- At a point `x ∉ s`, we unfold the definition of Fréchet differentiability, then use
         an estimate we proved earlier in this file. -/
     rcases exists_pos_mul_lt ε0 (2 * c) with ⟨ε', ε'0, hlt⟩
-    rcases (nhdsWithin_hasBasis nhds_basis_closedBall _).mem_iff.1 ((Hd x hx).isLittleO.def ε'0)
-      with ⟨δ, δ0, Hδ⟩
+    rcases (nhdsWithin_hasBasis nhds_basis_closedBall _).mem_iff.1
+      ((Hd x hx).isLittleO.definition ε'0) with ⟨δ, δ0, Hδ⟩
     refine' ⟨δ, δ0, fun J hle hJδ hxJ hJc => _⟩
     simp only [BoxAdditiveMap.volume_apply, Box.volume_apply, dist_eq_norm]
     refine' (norm_volume_sub_integral_face_upper_sub_lower_smul_le _

Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean

@@ -77,7 +77,7 @@ theorem approximates_deriv_on_nhds {f : E → F} {f' : E →L[𝕜] F} {a : E}
   cases' hc with hE hc
   · refine' ⟨univ, IsOpen.mem_nhds isOpen_univ trivial, fun x _ y _ => _⟩
     simp [@Subsingleton.elim E hE x y]
-  have := hf.def hc
+  have := hf.definition hc
   rw [nhds_prod_eq, Filter.Eventually, mem_prod_same_iff] at this
   rcases this with ⟨s, has, hs⟩
   exact ⟨s, has, fun x hx y hy => hs (mk_mem_prod hx hy)⟩

Mathlib/Analysis/Calculus/Rademacher.lean

@@ -270,7 +270,7 @@ theorem hasFderivAt_of_hasLineDerivAt_of_closure {f : E → F}
     exact (isCompact_sphere 0 1).elim_finite_subcover_image (fun y _hy ↦ isOpen_ball) this
   have I : ∀ᶠ t in 𝓝 (0 : ℝ), ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖ := by
     apply (Finite.eventually_all q_fin).2 (fun v hv ↦ ?_)
-    apply Asymptotics.IsLittleO.def ?_ δpos
+    apply Asymptotics.IsLittleO.definition ?_ δpos
     exact hasLineDerivAt_iff_isLittleO_nhds_zero.1 (hL v (hqs hv))
   obtain ⟨r, r_pos, hr⟩ : ∃ (r : ℝ), 0 < r ∧ ∀ (t : ℝ), ‖t‖ < r →
       ∀ v ∈ q, ‖f (x + t • v) - f x - t • L v‖ ≤ δ * ‖t‖ := by

Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean

@@ -90,7 +90,7 @@ theorem not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux
     _ = ‖∫ x in Ι c d, deriv f x‖ := norm_integral_eq_norm_integral_Ioc _
     _ ≤ ∫ x in Ι c d, ‖deriv f x‖ := norm_integral_le_integral_norm _
     _ ≤ ∫ x in Ι c d, C * ‖g x‖ :=
-      set_integral_mono_on hfi.norm.def (hgi.mono_set hsub') measurableSet_uIoc hg
+      set_integral_mono_on hfi.norm.def' (hgi.mono_set hsub') measurableSet_uIoc hg
     _ ≤ ∫ x in k, C * ‖g x‖ := by
       apply set_integral_mono_set hgi
         (ae_of_all _ fun x => mul_nonneg hC₀ (norm_nonneg _)) hsub'.eventuallyLE

Mathlib/Analysis/SpecificLimits/Normed.lean

@@ -172,7 +172,7 @@ theorem TFAE_exists_lt_isLittleO_pow (f : ℕ → ℝ) (R : ℝ) :
   -- Add 7 and 8 using 2 → 8 → 7 → 3
   tfae_have 2 → 8
   · rintro ⟨a, ha, H⟩
-    refine' ⟨a, ha, (H.def zero_lt_one).mono fun n hn ↦ _⟩
+    refine' ⟨a, ha, (H.definition zero_lt_one).mono fun n hn ↦ _⟩
     rwa [Real.norm_eq_abs, Real.norm_eq_abs, one_mul, abs_pow, abs_of_pos ha.1] at hn
   tfae_have 8 → 7
   exact fun ⟨a, ha, H⟩ ↦ ⟨a, ha.2, H⟩

Mathlib/CategoryTheory/Generator.lean

@@ -460,10 +460,12 @@ theorem isSeparator_def (G : C) :
     fun hG X Y f g hfg => hG _ _ fun h => hfg _ (Set.mem_singleton _) _⟩
 #align category_theory.is_separator_def CategoryTheory.isSeparator_def
 
-theorem IsSeparator.def {G : C} :
+-- Adaptation note: 2024-03-15
+-- Renamed to avoid the reserved name `IsSeparator.def`.
+theorem IsSeparator.def' {G : C} :
     IsSeparator G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : G ⟶ X, h ≫ f = h ≫ g) → f = g :=
   (isSeparator_def _).1
-#align category_theory.is_separator.def CategoryTheory.IsSeparator.def
+#align category_theory.is_separator.def CategoryTheory.IsSeparator.def'
 
 theorem isCoseparator_def (G : C) :
     IsCoseparator G ↔ ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : Y ⟶ G, f ≫ h = g ≫ h) → f = g :=
@@ -474,10 +476,12 @@ theorem isCoseparator_def (G : C) :
     fun hG X Y f g hfg => hG _ _ fun h => hfg _ (Set.mem_singleton _) _⟩
 #align category_theory.is_coseparator_def CategoryTheory.isCoseparator_def
 
-theorem IsCoseparator.def {G : C} :
+-- Adaptation note: 2024-03-15
+-- Renamed to avoid the reserved name `IsCoseparator.def`.
+theorem IsCoseparator.def' {G : C} :
     IsCoseparator G → ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ h : Y ⟶ G, f ≫ h = g ≫ h) → f = g :=
   (isCoseparator_def _).1
-#align category_theory.is_coseparator.def CategoryTheory.IsCoseparator.def
+#align category_theory.is_coseparator.def CategoryTheory.IsCoseparator.def'
 
 theorem isDetector_def (G : C) :
     IsDetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : G ⟶ Y, ∃! h', h' ≫ f = h) → IsIso f :=
@@ -488,10 +492,12 @@ theorem isDetector_def (G : C) :
     fun hG X Y f hf => hG _ fun h => hf _ (Set.mem_singleton _) _⟩
 #align category_theory.is_detector_def CategoryTheory.isDetector_def
 
-theorem IsDetector.def {G : C} :
+-- Adaptation note: 2024-03-15
+-- Renamed to avoid the reserved name `IsDetector.def`.
+theorem IsDetector.def' {G : C} :
     IsDetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : G ⟶ Y, ∃! h', h' ≫ f = h) → IsIso f :=
   (isDetector_def _).1
-#align category_theory.is_detector.def CategoryTheory.IsDetector.def
+#align category_theory.is_detector.def CategoryTheory.IsDetector.def'
 
 theorem isCodetector_def (G : C) :
     IsCodetector G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : X ⟶ G, ∃! h', f ≫ h' = h) → IsIso f :=
@@ -502,19 +508,21 @@ theorem isCodetector_def (G : C) :
     fun hG X Y f hf => hG _ fun h => hf _ (Set.mem_singleton _) _⟩
 #align category_theory.is_codetector_def CategoryTheory.isCodetector_def
 
-theorem IsCodetector.def {G : C} :
+-- Adaptation note: 2024-03-15
+-- Renamed to avoid the reserved name `IsCodetector.def`.
+theorem IsCodetector.def' {G : C} :
     IsCodetector G → ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : X ⟶ G, ∃! h', f ≫ h' = h) → IsIso f :=
   (isCodetector_def _).1
-#align category_theory.is_codetector.def CategoryTheory.IsCodetector.def
+#align category_theory.is_codetector.def CategoryTheory.IsCodetector.def'
 
 theorem isSeparator_iff_faithful_coyoneda_obj (G : C) :
     IsSeparator G ↔ Faithful (coyoneda.obj (op G)) :=
-  ⟨fun hG => ⟨fun hfg => hG.def _ _ (congr_fun hfg)⟩, fun _ =>
+  ⟨fun hG => ⟨fun hfg => hG.def' _ _ (congr_fun hfg)⟩, fun _ =>
     (isSeparator_def _).2 fun _ _ _ _ hfg => (coyoneda.obj (op G)).map_injective (funext hfg)⟩
 #align category_theory.is_separator_iff_faithful_coyoneda_obj CategoryTheory.isSeparator_iff_faithful_coyoneda_obj
 
 theorem isCoseparator_iff_faithful_yoneda_obj (G : C) : IsCoseparator G ↔ Faithful (yoneda.obj G) :=
-  ⟨fun hG => ⟨fun hfg => Quiver.Hom.unop_inj (hG.def _ _ (congr_fun hfg))⟩, fun _ =>
+  ⟨fun hG => ⟨fun hfg => Quiver.Hom.unop_inj (hG.def' _ _ (congr_fun hfg))⟩, fun _ =>
     (isCoseparator_def _).2 fun _ _ _ _ hfg =>
       Quiver.Hom.op_inj <| (yoneda.obj G).map_injective (funext hfg)⟩
 #align category_theory.is_coseparator_iff_faithful_yoneda_obj CategoryTheory.isCoseparator_iff_faithful_yoneda_obj
@@ -548,7 +556,7 @@ theorem isSeparator_coprod (G H : C) [HasBinaryCoproduct G H] :
   refine'
     ⟨fun h X Y u v huv => _, fun h =>
       (isSeparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => _⟩
-  · refine' h.def _ _ fun g => coprod.hom_ext _ _
+  · refine' h.def' _ _ fun g => coprod.hom_ext _ _
     · simpa using huv G (by simp) (coprod.inl ≫ g)
     · simpa using huv H (by simp) (coprod.inr ≫ g)
   · simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ
@@ -572,7 +580,7 @@ theorem isSeparator_sigma {β : Type w} (f : β → C) [HasCoproduct f] :
   refine'
     ⟨fun h X Y u v huv => _, fun h =>
       (isSeparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => _⟩
-  · refine' h.def _ _ fun g => colimit.hom_ext fun b => _
+  · refine' h.def' _ _ fun g => colimit.hom_ext fun b => _
     simpa using huv (f b.as) (by simp) (colimit.ι (Discrete.functor f) _ ≫ g)
   · obtain ⟨b, rfl⟩ := Set.mem_range.1 hZ
     classical simpa using Sigma.ι f b ≫= huv (Sigma.desc (Pi.single b g))
@@ -588,7 +596,7 @@ theorem isCoseparator_prod (G H : C) [HasBinaryProduct G H] :
   refine'
     ⟨fun h X Y u v huv => _, fun h =>
       (isCoseparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => _⟩
-  · refine' h.def _ _ fun g => prod.hom_ext _ _
+  · refine' h.def' _ _ fun g => prod.hom_ext _ _
     · simpa using huv G (by simp) (g ≫ Limits.prod.fst)
     · simpa using huv H (by simp) (g ≫ Limits.prod.snd)
   · simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ
@@ -612,7 +620,7 @@ theorem isCoseparator_pi {β : Type w} (f : β → C) [HasProduct f] :
   refine'
     ⟨fun h X Y u v huv => _, fun h =>
       (isCoseparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => _⟩
-  · refine' h.def _ _ fun g => limit.hom_ext fun b => _
+  · refine' h.def' _ _ fun g => limit.hom_ext fun b => _
     simpa using huv (f b.as) (by simp) (g ≫ limit.π (Discrete.functor f) _)
   · obtain ⟨b, rfl⟩ := Set.mem_range.1 hZ
     classical simpa using huv (Pi.lift (Pi.single b g)) =≫ Pi.π f b
@@ -628,7 +636,7 @@ end ZeroMorphisms
 theorem isDetector_iff_reflectsIsomorphisms_coyoneda_obj (G : C) :
     IsDetector G ↔ ReflectsIsomorphisms (coyoneda.obj (op G)) := by
   refine'
-    ⟨fun hG => ⟨fun f hf => hG.def _ fun h => _⟩, fun h =>
+    ⟨fun hG => ⟨fun f hf => hG.def' _ fun h => _⟩, fun h =>
       (isDetector_def _).2 fun X Y f hf => _⟩
   · rw [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
     exact hf h
@@ -640,7 +648,7 @@ theorem isDetector_iff_reflectsIsomorphisms_coyoneda_obj (G : C) :
 theorem isCodetector_iff_reflectsIsomorphisms_yoneda_obj (G : C) :
     IsCodetector G ↔ ReflectsIsomorphisms (yoneda.obj G) := by
   refine' ⟨fun hG => ⟨fun f hf => _⟩, fun h => (isCodetector_def _).2 fun X Y f hf => _⟩
-  · refine' (isIso_unop_iff _).1 (hG.def _ _)
+  · refine' (isIso_unop_iff _).1 (hG.def' _ _)
     rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
   · rw [← isIso_op_iff]
     suffices IsIso ((yoneda.obj G).map f.op) by

Mathlib/CategoryTheory/Preadditive/Generator.lean

@@ -39,14 +39,14 @@ theorem Preadditive.isCoseparating_iff (𝒢 : Set C) :
 
 theorem Preadditive.isSeparator_iff (G : C) :
     IsSeparator G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : G ⟶ X, h ≫ f = 0) → f = 0 :=
-  ⟨fun hG X Y f hf => hG.def _ _ (by simpa only [Limits.comp_zero] using hf), fun hG =>
+  ⟨fun hG X Y f hf => hG.def' _ _ (by simpa only [Limits.comp_zero] using hf), fun hG =>
     (isSeparator_def _).2 fun X Y f g hfg =>
       sub_eq_zero.1 <| hG _ (by simpa only [Preadditive.comp_sub, sub_eq_zero] using hfg)⟩
 #align category_theory.preadditive.is_separator_iff CategoryTheory.Preadditive.isSeparator_iff
 
 theorem Preadditive.isCoseparator_iff (G : C) :
     IsCoseparator G ↔ ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ h : Y ⟶ G, f ≫ h = 0) → f = 0 :=
-  ⟨fun hG X Y f hf => hG.def _ _ (by simpa only [Limits.zero_comp] using hf), fun hG =>
+  ⟨fun hG X Y f hf => hG.def' _ _ (by simpa only [Limits.zero_comp] using hf), fun hG =>
     (isCoseparator_def _).2 fun X Y f g hfg =>
       sub_eq_zero.1 <| hG _ (by simpa only [Preadditive.sub_comp, sub_eq_zero] using hfg)⟩
 #align category_theory.preadditive.is_coseparator_iff CategoryTheory.Preadditive.isCoseparator_iff

Mathlib/CategoryTheory/Subterminal.lean

@@ -45,9 +45,11 @@ def IsSubterminal (A : C) : Prop :=
   ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g
 #align category_theory.is_subterminal CategoryTheory.IsSubterminal
 
-theorem IsSubterminal.def : IsSubterminal A ↔ ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g :=
+-- Adaptation note: 2024-03-15
+-- Renamed to avoid the reserved name `IsSubterminal.def`.
+theorem IsSubterminal.def' : IsSubterminal A ↔ ∀ ⦃Z : C⦄ (f g : Z ⟶ A), f = g :=
   Iff.rfl
-#align category_theory.is_subterminal.def CategoryTheory.IsSubterminal.def
+#align category_theory.is_subterminal.def CategoryTheory.IsSubterminal.def'
 
 /-- If `A` is subterminal, the unique morphism from it to a terminal object is a monomorphism.
 The converse of `isSubterminal_of_mono_isTerminal_from`.
@@ -97,7 +99,7 @@ The converse of `isSubterminal_of_isIso_diag`.
 theorem IsSubterminal.isIso_diag (hA : IsSubterminal A) [HasBinaryProduct A A] : IsIso (diag A) :=
   ⟨⟨Limits.prod.fst,
       ⟨by simp, by
-        rw [IsSubterminal.def] at hA
+        rw [IsSubterminal.def'] at hA
         aesop_cat⟩⟩⟩
 #align category_theory.is_subterminal.is_iso_diag CategoryTheory.IsSubterminal.isIso_diag
 

Mathlib/Data/Polynomial/Degree/Definitions.lean

@@ -85,9 +85,11 @@ theorem monic_of_subsingleton [Subsingleton R] (p : R[X]) : Monic p :=
   Subsingleton.elim _ _
 #align polynomial.monic_of_subsingleton Polynomial.monic_of_subsingleton
 
-theorem Monic.def : Monic p ↔ leadingCoeff p = 1 :=
+-- Adaptation note: 2024-03-15
+-- Renamed to avoid the reserved name `Monic.def`.
+theorem Monic.def' : Monic p ↔ leadingCoeff p = 1 :=
   Iff.rfl
-#align polynomial.monic.def Polynomial.Monic.def
+#align polynomial.monic.def Polynomial.Monic.def'
 
 instance Monic.decidable [DecidableEq R] : Decidable (Monic p) := by unfold Monic; infer_instance
 #align polynomial.monic.decidable Polynomial.Monic.decidable
@@ -1202,7 +1204,7 @@ theorem eq_C_coeff_zero_iff_natDegree_eq_zero : p = C (p.coeff 0) ↔ p.natDegre
   ⟨fun h ↦ by rw [h, natDegree_C], eq_C_of_natDegree_eq_zero⟩
 
 theorem eq_one_of_monic_natDegree_zero (hf : p.Monic) (hfd : p.natDegree = 0) : p = 1 := by
-  rw [Monic.def, leadingCoeff, hfd] at hf
+  rw [Monic.def', leadingCoeff, hfd] at hf
   rw [eq_C_of_natDegree_eq_zero hfd, hf, map_one]
 
 theorem ne_zero_of_coe_le_degree (hdeg : ↑n ≤ p.degree) : p ≠ 0 :=

Mathlib/Data/Polynomial/Degree/TrailingDegree.lean

@@ -67,9 +67,11 @@ def TrailingMonic (p : R[X]) :=
   trailingCoeff p = (1 : R)
 #align polynomial.trailing_monic Polynomial.TrailingMonic
 
-theorem TrailingMonic.def : TrailingMonic p ↔ trailingCoeff p = 1 :=
+-- Adaptation note: 2024-03-15: this was called `def`.
+-- Should lean be changed to allow that as a name again?
+theorem TrailingMonic.definition : TrailingMonic p ↔ trailingCoeff p = 1 :=
   Iff.rfl
-#align polynomial.trailing_monic.def Polynomial.TrailingMonic.def
+#align polynomial.trailing_monic.def Polynomial.TrailingMonic.definition
 
 instance TrailingMonic.decidable [DecidableEq R] : Decidable (TrailingMonic p) :=
   inferInstanceAs <| Decidable (trailingCoeff p = (1 : R))