Trigger CI for leanprover-community/batteries#1029

Mathlib.lean

@@ -916,6 +916,7 @@ import Mathlib.AlgebraicGeometry.Morphisms.Basic
 import Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
 import Mathlib.AlgebraicGeometry.Morphisms.Constructors
 import Mathlib.AlgebraicGeometry.Morphisms.Etale
+import Mathlib.AlgebraicGeometry.Morphisms.Finite
 import Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
 import Mathlib.AlgebraicGeometry.Morphisms.FiniteType
 import Mathlib.AlgebraicGeometry.Morphisms.Immersion
@@ -1039,7 +1040,6 @@ import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
-import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.PosPart
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
 import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
@@ -1074,6 +1074,7 @@ import Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
 import Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
 import Mathlib.Analysis.Calculus.ContDiff.RCLike
 import Mathlib.Analysis.Calculus.ContDiff.WithLp
+import Mathlib.Analysis.Calculus.DSlope
 import Mathlib.Analysis.Calculus.Darboux
 import Mathlib.Analysis.Calculus.Deriv.Abs
 import Mathlib.Analysis.Calculus.Deriv.Add
@@ -1094,7 +1095,6 @@ import Mathlib.Analysis.Calculus.Deriv.Star
 import Mathlib.Analysis.Calculus.Deriv.Support
 import Mathlib.Analysis.Calculus.Deriv.ZPow
 import Mathlib.Analysis.Calculus.DiffContOnCl
-import Mathlib.Analysis.Calculus.Dslope
 import Mathlib.Analysis.Calculus.FDeriv.Add
 import Mathlib.Analysis.Calculus.FDeriv.Analytic
 import Mathlib.Analysis.Calculus.FDeriv.Basic
@@ -1426,6 +1426,7 @@ import Mathlib.Analysis.SpecialFunctions.Complex.Log
 import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
 import Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv
 import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog
+import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart
 import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow
 import Mathlib.Analysis.SpecialFunctions.Exp
 import Mathlib.Analysis.SpecialFunctions.ExpDeriv
@@ -1746,6 +1747,7 @@ import Mathlib.CategoryTheory.Limits.HasLimits
 import Mathlib.CategoryTheory.Limits.IndYoneda
 import Mathlib.CategoryTheory.Limits.Indization.FilteredColimits
 import Mathlib.CategoryTheory.Limits.Indization.IndObject
+import Mathlib.CategoryTheory.Limits.Indization.LocallySmall
 import Mathlib.CategoryTheory.Limits.IsConnected
 import Mathlib.CategoryTheory.Limits.IsLimit
 import Mathlib.CategoryTheory.Limits.Lattice
@@ -2316,6 +2318,7 @@ import Mathlib.Data.Fin.Tuple.Sort
 import Mathlib.Data.Fin.Tuple.Take
 import Mathlib.Data.Fin.VecNotation
 import Mathlib.Data.FinEnum
+import Mathlib.Data.FinEnum.Option
 import Mathlib.Data.Finite.Card
 import Mathlib.Data.Finite.Defs
 import Mathlib.Data.Finite.Powerset
@@ -2468,6 +2471,7 @@ import Mathlib.Data.List.EditDistance.Defs
 import Mathlib.Data.List.EditDistance.Estimator
 import Mathlib.Data.List.Enum
 import Mathlib.Data.List.FinRange
+import Mathlib.Data.List.Flatten
 import Mathlib.Data.List.Forall2
 import Mathlib.Data.List.GetD
 import Mathlib.Data.List.Indexes
@@ -2476,7 +2480,6 @@ import Mathlib.Data.List.InsertIdx
 import Mathlib.Data.List.InsertNth
 import Mathlib.Data.List.Intervals
 import Mathlib.Data.List.Iterate
-import Mathlib.Data.List.Join
 import Mathlib.Data.List.Lattice
 import Mathlib.Data.List.Lemmas
 import Mathlib.Data.List.Lex
@@ -4263,6 +4266,7 @@ import Mathlib.RingTheory.MvPowerSeries.Basic
 import Mathlib.RingTheory.MvPowerSeries.Inverse
 import Mathlib.RingTheory.MvPowerSeries.LexOrder
 import Mathlib.RingTheory.MvPowerSeries.NoZeroDivisors
+import Mathlib.RingTheory.MvPowerSeries.Order
 import Mathlib.RingTheory.MvPowerSeries.Trunc
 import Mathlib.RingTheory.Nakayama
 import Mathlib.RingTheory.Nilpotent.Basic

Mathlib/Algebra/Algebra/Basic.lean

@@ -182,7 +182,7 @@ variable {R M}
 theorem End_algebraMap_isUnit_inv_apply_eq_iff {x : R}
     (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) :
     (↑(h.unit⁻¹) : Module.End S M) m = m' ↔ m = x • m' :=
-  { mp := fun H => ((congr_arg h.unit H).symm.trans (End_isUnit_apply_inv_apply_of_isUnit h _)).symm
+  { mp := fun H => H ▸ (End_isUnit_apply_inv_apply_of_isUnit h m).symm
     mpr := fun H =>
       H.symm ▸ by
         apply_fun ⇑h.unit.val using ((Module.End_isUnit_iff _).mp h).injective
@@ -191,7 +191,7 @@ theorem End_algebraMap_isUnit_inv_apply_eq_iff {x : R}
 theorem End_algebraMap_isUnit_inv_apply_eq_iff' {x : R}
     (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) :
     m' = (↑h.unit⁻¹ : Module.End S M) m ↔ m = x • m' :=
-  { mp := fun H => ((congr_arg h.unit H).trans (End_isUnit_apply_inv_apply_of_isUnit h _)).symm
+  { mp := fun H => H ▸ (End_isUnit_apply_inv_apply_of_isUnit h m).symm
     mpr := fun H =>
       H.symm ▸ by
         apply_fun (↑h.unit : M → M) using ((Module.End_isUnit_iff _).mp h).injective

Mathlib/Algebra/Algebra/Equiv.lean

@@ -618,6 +618,7 @@ end OfRingEquiv
 
 -- Porting note: projections mul & one not found, removed [simps] and added theorems manually
 -- @[simps (config := .lemmasOnly) one]
+@[stacks 09HR]
 instance aut : Group (A₁ ≃ₐ[R] A₁) where
   mul ϕ ψ := ψ.trans ϕ
   mul_assoc _ _ _ := rfl

Mathlib/Algebra/Algebra/NonUnitalHom.lean

@@ -448,11 +448,6 @@ instance NonUnitalAlgHom.hasCoe : CoeOut (A →ₐ[R] B) (A →ₙₐ[R] B) :=
 theorem toNonUnitalAlgHom_eq_coe (f : A →ₐ[R] B) : f.toNonUnitalAlgHom = f :=
   rfl
 
--- Note (#6057) : tagging simpNF because linter complains
-@[simp, norm_cast, nolint simpNF]
-theorem coe_to_nonUnitalAlgHom (f : A →ₐ[R] B) : ⇑(f.toNonUnitalAlgHom) = ⇑f :=
-  rfl
-
 end AlgHom
 
 section RestrictScalars

Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean

@@ -976,7 +976,7 @@ noncomputable def iSupLift [Nonempty ι] (K : ι → NonUnitalSubalgebra R A) (d
               simp only
               rw [hf i k hik, hf j k hjk]
               rfl)
-            (↑(iSup K)) (by rw [coe_iSup_of_directed dir])
+            _ (by rw [coe_iSup_of_directed dir])
         map_zero' := by
           dsimp
           exact Set.iUnionLift_const _ (fun i : ι => (0 : K i)) (fun _ => rfl) _ (by simp)

Mathlib/Algebra/Algebra/Subalgebra/Directed.lean

@@ -51,7 +51,7 @@ noncomputable def iSupLift (dir : Directed (· ≤ ·) K) (f : ∀ i, K i →ₐ
           dsimp
           rw [hf i k hik, hf j k hjk]
           rfl)
-        T (by rw [hT, coe_iSup_of_directed dir])
+        (T : Set A) (by rw [hT, coe_iSup_of_directed dir])
     map_one' := by apply Set.iUnionLift_const _ (fun _ => 1) <;> simp
     map_zero' := by dsimp; apply Set.iUnionLift_const _ (fun _ => 0) <;> simp
     map_mul' := by

Mathlib/Algebra/AlgebraicCard.lean

@@ -85,6 +85,7 @@ theorem cardinal_mk_le_mul : #{ x : A // IsAlgebraic R x } ≤ #R[X] * ℵ₀ :=
   rw [← lift_id #_, ← lift_id #R[X]]
   exact cardinal_mk_lift_le_mul R A
 
+@[stacks 09GK]
 theorem cardinal_mk_le_max : #{ x : A // IsAlgebraic R x } ≤ max #R ℵ₀ := by
   rw [← lift_id #_, ← lift_id #R]
   exact cardinal_mk_lift_le_max R A

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -926,9 +926,8 @@ theorem prod_eq_mul {s : Finset α} {f : α → β} (a b : α) (hn : a ≠ b)
           h₀ c hc ⟨ne_of_mem_of_not_mem hc h₁, ne_of_mem_of_not_mem hc h₂⟩)
         prod_const_one
 
--- Porting note: simpNF linter complains that LHS doesn't simplify, but it does
 /-- A product over `s.subtype p` equals one over `{x ∈ s | p x}`. -/
-@[to_additive (attr := simp, nolint simpNF)
+@[to_additive (attr := simp)
 "A sum over `s.subtype p` equals one over `{x ∈ s | p x}`."]
 theorem prod_subtype_eq_prod_filter (f : α → β) {p : α → Prop} [DecidablePred p] :
     ∏ x ∈ s.subtype p, f x = ∏ x ∈ s with p x, f x := by

Mathlib/Algebra/BigOperators/Group/List.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best
 import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Group.Int
 import Mathlib.Data.List.Dedup
-import Mathlib.Data.List.Join
+import Mathlib.Data.List.Flatten
 import Mathlib.Data.List.Pairwise
 import Mathlib.Data.List.Perm.Basic
 import Mathlib.Data.List.ProdSigma

Mathlib/Algebra/Category/BialgebraCat/Basic.lean

@@ -44,6 +44,7 @@ variable (R)
 @[simps]
 def of (X : Type v) [Ring X] [Bialgebra R X] :
     BialgebraCat R where
+  α := X
   instBialgebra := (inferInstance : Bialgebra R X)
 
 variable {R}

Mathlib/Algebra/Category/Grp/Biproducts.lean

@@ -63,14 +63,10 @@ theorem binaryProductLimitCone_cone_π_app_right (G H : AddCommGrp.{u}) :
 /-- We verify that the biproduct in `AddCommGrp` is isomorphic to
 the cartesian product of the underlying types:
 -/
-@[simps! hom_apply]
 noncomputable def biprodIsoProd (G H : AddCommGrp.{u}) :
     (G ⊞ H : AddCommGrp) ≅ AddCommGrp.of (G × H) :=
   IsLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit G H) (binaryProductLimitCone G H).isLimit
 
--- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
-attribute [nolint simpNF] AddCommGrp.biprodIsoProd_hom_apply
-
 @[simp, elementwise]
 theorem biprodIsoProd_inv_comp_fst (G H : AddCommGrp.{u}) :
     (biprodIsoProd G H).inv ≫ biprod.fst = AddMonoidHom.fst G H :=
@@ -127,14 +123,10 @@ variable {J : Type} [Finite J]
 /-- We verify that the biproduct we've just defined is isomorphic to the `AddCommGrp` structure
 on the dependent function type.
 -/
-@[simps! hom_apply]
 noncomputable def biproductIsoPi (f : J → AddCommGrp.{u}) :
     (⨁ f : AddCommGrp) ≅ AddCommGrp.of (∀ j, f j) :=
   IsLimit.conePointUniqueUpToIso (biproduct.isLimit f) (productLimitCone f).isLimit
 
--- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
-attribute [nolint simpNF] AddCommGrp.biproductIsoPi_hom_apply
-
 @[simp, elementwise]
 theorem biproductIsoPi_inv_comp_π (f : J → AddCommGrp.{u}) (j : J) :
     (biproductIsoPi f).inv ≫ biproduct.π f j = Pi.evalAddMonoidHom (fun j => f j) j :=

Mathlib/Algebra/Category/Grp/Limits.lean

@@ -451,13 +451,8 @@ theorem kernelIsoKer_inv_comp_ι {G H : AddCommGrp.{u}} (f : G ⟶ H) :
 /-- The categorical kernel inclusion for `f : G ⟶ H`, as an object over `G`,
 agrees with the `AddSubgroup.subtype` map.
 -/
-@[simps! hom_left_apply_coe inv_left_apply]
 def kernelIsoKerOver {G H : AddCommGrp.{u}} (f : G ⟶ H) :
     Over.mk (kernel.ι f) ≅ @Over.mk _ _ G (AddCommGrp.of f.ker) (AddSubgroup.subtype f.ker) :=
   Over.isoMk (kernelIsoKer f)
 
--- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
-attribute [nolint simpNF] AddCommGrp.kernelIsoKerOver_inv_left_apply
-  AddCommGrp.kernelIsoKerOver_hom_left_apply_coe
-
 end AddCommGrp

Mathlib/Algebra/Category/HopfAlgebraCat/Basic.lean

@@ -43,6 +43,7 @@ variable (R)
 @[simps]
 def of (X : Type v) [Ring X] [HopfAlgebra R X] :
     HopfAlgebraCat R where
+  α := X
   instHopfAlgebra := (inferInstance : HopfAlgebra R X)
 
 variable {R}

Mathlib/Algebra/Category/ModuleCat/Biproducts.lean

@@ -63,14 +63,10 @@ theorem binaryProductLimitCone_cone_π_app_right (M N : ModuleCat.{v} R) :
 /-- We verify that the biproduct in `ModuleCat R` is isomorphic to
 the cartesian product of the underlying types:
 -/
-@[simps! hom_apply]
 noncomputable def biprodIsoProd (M N : ModuleCat.{v} R) :
     (M ⊞ N : ModuleCat.{v} R) ≅ ModuleCat.of R (M × N) :=
   IsLimit.conePointUniqueUpToIso (BinaryBiproduct.isLimit M N) (binaryProductLimitCone M N).isLimit
 
--- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
-attribute [nolint simpNF] ModuleCat.biprodIsoProd_hom_apply
-
 @[simp, elementwise]
 theorem biprodIsoProd_inv_comp_fst (M N : ModuleCat.{v} R) :
     (biprodIsoProd M N).inv ≫ biprod.fst = LinearMap.fst R M N :=
@@ -122,14 +118,10 @@ variable {J : Type} (f : J → ModuleCat.{v} R)
 /-- We verify that the biproduct we've just defined is isomorphic to the `ModuleCat R` structure
 on the dependent function type.
 -/
-@[simps! hom_apply]
 noncomputable def biproductIsoPi [Finite J] (f : J → ModuleCat.{v} R) :
     ((⨁ f) : ModuleCat.{v} R) ≅ ModuleCat.of R (∀ j, f j) :=
   IsLimit.conePointUniqueUpToIso (biproduct.isLimit f) (productLimitCone f).isLimit
 
--- These lemmas have always been bad (#7657), but lean4#2644 made `simp` start noticing
-attribute [nolint simpNF] ModuleCat.biproductIsoPi_hom_apply
-
 @[simp, elementwise]
 theorem biproductIsoPi_inv_comp_π [Finite J] (f : J → ModuleCat.{v} R) (j : J) :
     (biproductIsoPi f).inv ≫ biproduct.π f j = (LinearMap.proj j : (∀ j, f j) →ₗ[R] f j) :=

Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean

@@ -21,7 +21,6 @@ namespace ModuleCat
 
 variable {R : Type u} [CommRing R]
 
--- Porting note: removed @[simps] as the simpNF linter complains
 /-- Auxiliary definition for the `MonoidalClosed` instance on `Module R`.
 (This is only a separate definition in order to speed up typechecking. )
 -/

Mathlib/Algebra/Category/Ring/Adjunctions.lean

@@ -37,8 +37,9 @@ def free : Type u ⥤ CommRingCat.{u} where
 theorem free_obj_coe {α : Type u} : (free.obj α : Type u) = MvPolynomial α ℤ :=
   rfl
 
--- Porting note: `simpNF` should not trigger on `rfl` lemmas.
--- see https://github.com/leanprover/std4/issues/86
+-- The `simpNF` linter complains here, even though it is a `rfl` lemma,
+-- because the implicit arguments on the left-hand side simplify via `dsimp`.
+-- (That is, the left-hand side really is not in simp normal form.)
 @[simp, nolint simpNF]
 theorem free_map_coe {α β : Type u} {f : α → β} : ⇑(free.map f) = ⇑(rename f) :=
   rfl

Mathlib/Algebra/CharP/Basic.lean

@@ -170,6 +170,8 @@ end CharZero
 
 namespace Fin
 
+/-- The characteristic of `F_p` is `p`. -/
+@[stacks 09FS "First part. We don't require `p` to be a prime in mathlib."]
 instance charP (n : ℕ) [NeZero n] : CharP (Fin n) n where cast_eq_zero_iff' _ := natCast_eq_zero
 
 end Fin

Mathlib/Algebra/CharP/LocalRing.lean

@@ -19,12 +19,12 @@ import Mathlib.RingTheory.LocalRing.ResidueField.Defs
 
 
 /-- In a local ring the characteristics is either zero or a prime power. -/
-theorem charP_zero_or_prime_power (R : Type*) [CommRing R] [LocalRing R] (q : ℕ)
+theorem charP_zero_or_prime_power (R : Type*) [CommRing R] [IsLocalRing R] (q : ℕ)
     [char_R_q : CharP R q] : q = 0 ∨ IsPrimePow q := by
   -- Assume `q := char(R)` is not zero.
   apply or_iff_not_imp_left.2
   intro q_pos
-  let K := LocalRing.ResidueField R
+  let K := IsLocalRing.ResidueField R
   haveI RM_char := ringChar.charP K
   let r := ringChar K
   let n := q.factorization r
@@ -40,7 +40,7 @@ theorem charP_zero_or_prime_power (R : Type*) [CommRing R] [LocalRing R] (q : 
     have a_unit : IsUnit (a : R) := by
       by_contra g
       rw [← mem_nonunits_iff] at g
-      rw [← LocalRing.mem_maximalIdeal] at g
+      rw [← IsLocalRing.mem_maximalIdeal] at g
       have a_cast_zero := Ideal.Quotient.eq_zero_iff_mem.2 g
       rw [map_natCast] at a_cast_zero
       have r_dvd_a := (ringChar.spec K a).1 a_cast_zero
@@ -57,7 +57,7 @@ theorem charP_zero_or_prime_power (R : Type*) [CommRing R] [LocalRing R] (q : 
     exact ⟨r, ⟨n, ⟨r_prime.prime, ⟨pos_iff_ne_zero.mpr n_pos, q_eq_rn.symm⟩⟩⟩⟩
   · haveI K_char_p_0 := ringChar.of_eq r_zero
     haveI K_char_zero : CharZero K := CharP.charP_to_charZero K
-    haveI R_char_zero := RingHom.charZero (LocalRing.residue R)
+    haveI R_char_zero := RingHom.charZero (IsLocalRing.residue R)
     -- Finally, `r = 0` would lead to a contradiction:
     have q_zero := CharP.eq R char_R_q (CharP.ofCharZero R)
     exact absurd q_zero q_pos

Mathlib/Algebra/CharP/MixedCharZero.lean

@@ -341,12 +341,12 @@ theorem split_by_characteristic_domain [IsDomain R] (h_pos : ∀ p : ℕ, Nat.Pr
   exact h_pos p p_prime p_char
 
 /--
-In a `LocalRing R`, split any `Prop` over `R` into the three cases:
+In a local ring `R`, split any predicate over `R` into the three cases:
 - *prime power* characteristic.
 - equal characteristic zero.
 - mixed characteristic `(0, p)`.
 -/
-theorem split_by_characteristic_localRing [LocalRing R]
+theorem split_by_characteristic_localRing [IsLocalRing R]
     (h_pos : ∀ p : ℕ, IsPrimePow p → CharP R p → P) (h_equal : Algebra ℚ R → P)
     (h_mixed : ∀ p : ℕ, Nat.Prime p → MixedCharZero R p → P) : P := by
   refine split_by_characteristic R ?_ h_equal h_mixed

Mathlib/Algebra/DirectSum/Internal.lean

@@ -334,13 +334,9 @@ def subsemiring : Subsemiring R where
 /-- The semiring `A 0` inherited from `R` in the presence of `SetLike.GradedMonoid A`. -/
 instance instSemiring : Semiring (A 0) := (subsemiring A).toSemiring
 
-/- The linter message "error: SetLike.GradeZero.coe_natCast.{u_4, u_2, u_1} Left-hand side
-  does not simplify, when using the simp lemma on itself." is wrong. The LHS does simplify. -/
-@[nolint simpNF, simp, norm_cast] theorem coe_natCast (n : ℕ) : (n : A 0) = (n : R) := rfl
+@[simp, norm_cast] theorem coe_natCast (n : ℕ) : (n : A 0) = (n : R) := rfl
 
-/- The linter message "error: SetLike.GradeZero.coe_ofNat.{u_4, u_2, u_1} Left-hand side does
-  not simplify, when using the simp lemma on itself." is wrong. The LHS does simplify. -/
-@[nolint simpNF, simp, norm_cast] theorem coe_ofNat (n : ℕ) [n.AtLeastTwo] :
+@[simp, norm_cast] theorem coe_ofNat (n : ℕ) [n.AtLeastTwo] :
     (no_index (OfNat.ofNat n) : A 0) = (OfNat.ofNat n : R) := rfl
 
 end Semiring
@@ -397,9 +393,7 @@ def subalgebra : Subalgebra S R where
 /-- The `S`-algebra `A 0` inherited from `R` in the presence of `SetLike.GradedMonoid A`. -/
 instance instAlgebra : Algebra S (A 0) := inferInstanceAs <| Algebra S (subalgebra A)
 
-/- The linter message "error: SetLike.GradeZero.coe_algebraMap.{u_4, u_3, u_1} Left-hand side
-  does not simplify, when using the simp lemma on itself." is wrong. The LHS does simplify. -/
-@[nolint simpNF, simp, norm_cast] theorem coe_algebraMap (s : S) :
+@[simp, norm_cast] theorem coe_algebraMap (s : S) :
     ↑(algebraMap _ (A 0) s) = algebraMap _ R s := rfl
 
 end Algebra

Mathlib/Algebra/Field/Basic.lean

@@ -211,6 +211,9 @@ end Field
 
 namespace RingHom
 
+/-- Any ring homomorphism `f : F → R` from a `DivisionRing F` to nonzero ring `R` is injective.
+-/
+@[stacks 09FU]
 protected theorem injective [DivisionRing K] [Semiring L] [Nontrivial L] (f : K →+* L) :
     Injective f :=
   (injective_iff_map_eq_zero f).2 fun _ ↦ (map_eq_zero f).1

Mathlib/Algebra/Field/Defs.lean

@@ -172,6 +172,7 @@ See also note [forgetful inheritance].
 
 If the field has positive characteristic `p`, our division by zero convention forces
 `ratCast (1 / p) = 1 / 0 = 0`. -/
+@[stacks 09FD "first part"]
 class Field (K : Type u) extends CommRing K, DivisionRing K
 
 -- see Note [lower instance priority]

Mathlib/Algebra/Field/Subfield/Defs.lean

@@ -129,6 +129,7 @@ end SubfieldClass
 /-- `Subfield R` is the type of subfields of `R`. A subfield of `R` is a subset `s` that is a
   multiplicative submonoid and an additive subgroup. Note in particular that it shares the
   same 0 and 1 as R. -/
+@[stacks 09FD "second part"]
 structure Subfield (K : Type u) [DivisionRing K] extends Subring K where
   /-- A subfield is closed under multiplicative inverses. -/
   inv_mem' : ∀ x ∈ carrier, x⁻¹ ∈ carrier