Fix errors

Mathlib/RingTheory/Localization/Cardinality.lean

@@ -16,13 +16,13 @@ import Mathlib.RingTheory.Artinian
 
 In this file, we establish the cardinality of localizations. In most cases, a localization has
 cardinality equal to the base ring. If there are zero-divisors, however, this is no longer true -
-for example, `zmod 6` localized at `{2, 4}` is equal to `zmod 3`, and if you have zero in your
-submonoid, then your localization is trivial (see `is_localization.unique_of_zero_mem`).
+for example, `ZMod 6` localized at `{2, 4}` is equal to `ZMod 3`, and if you have zero in your
+submonoid, then your localization is trivial (see `IsLocalization.uniqueOfZeroMem`).
 
 ## Main statements
 
-* `is_localization.card_le`: A localization has cardinality no larger than the base ring.
-* `is_localization.card`: If you don't localize at zero-divisors, the localization of a ring has
+* `IsLocalization.card_le`: A localization has cardinality no larger than the base ring.
+* `IsLocalization.card`: If you don't localize at zero-divisors, the localization of a ring has
   cardinality equal to its base ring,
 
 -/
@@ -37,8 +37,6 @@ namespace IsLocalization
 variable {R : Type u} [CommRing R] (S : Submonoid R) {L : Type u} [CommRing L] [Algebra R L]
   [IsLocalization S L]
 
-include S
-
 /-- A localization always has cardinality less than or equal to the base ring. -/
 theorem card_le : (#L) ≤ (#R) := by
   classical
@@ -49,7 +47,7 @@ theorem card_le : (#L) ≤ (#R) := by
     refine' @Cardinal.mk_le_of_surjective _ _ f fun a => _
     obtain ⟨x, y, h⟩ := IsLocalization.mk'_surjective S a
     use (x, y)
-    dsimp [f]
+    dsimp
     rwa [dif_pos <| show ↑y ∈ S from y.2, SetLike.eta]
 #align is_localization.card_le IsLocalization.card_le
 
@@ -61,4 +59,3 @@ theorem card (hS : S ≤ R⁰) : (#R) = (#L) :=
 #align is_localization.card IsLocalization.card
 
 end IsLocalization
-