fix(*): fix padding around notations (#16333)

I noticed a bunch of issues around padding in mathport, so I went through and fixed all the padding issues I could find in mathlib.

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

archive/examples/prop_encodable.lean

@@ -61,7 +61,7 @@ namespace prop_form
 
 private def constructors (α : Type*) := α ⊕ unit ⊕ unit ⊕ unit
 
-local notation `cvar` a := sum.inl a
+local notation `cvar ` a := sum.inl a
 local notation `cnot`   := sum.inr (sum.inl unit.star)
 local notation `cand`   := sum.inr (sum.inr (sum.inr unit.star))
 local notation `cor`    := sum.inr (sum.inr (sum.inl unit.star))

archive/sensitivity.lean

@@ -332,7 +332,7 @@ In this section, in order to enforce that `n` is positive, we write it as
 `m + 1` for some natural number `m`. -/
 
 /-! `dim X` will denote the dimension of a subspace `X` as a cardinal. -/
-notation `dim` X:70 := module.rank ℝ ↥X
+notation `dim ` X:70 := module.rank ℝ ↥X
 /-! `fdim X` will denote the (finite) dimension of a subspace `X` as a natural number. -/
 notation `fdim` := finrank ℝ
 
@@ -341,7 +341,7 @@ notation `Span` := submodule.span ℝ
 
 /-! `Card X` will denote the cardinal of a subset of a finite type, as a
 natural number. -/
-notation `Card` X:70 := X.to_finset.card
+notation `Card ` X:70 := X.to_finset.card
 
 /-! In the following, `⊓` and `⊔` will denote intersection and sums of ℝ-subspaces,
 equipped with their subspace structures. The notations come from the general

src/algebra/big_operators/intervals.lean

@@ -234,7 +234,7 @@ section module
 variables {R M : Type*} [ring R] [add_comm_group M] [module R M] (f : ℕ → R) (g : ℕ → M) {m n : ℕ}
 open finset
 -- The partial sum of `g`, starting from zero
-local notation `G` n:80 := ∑ i in range n, g i
+local notation `G ` n:80 := ∑ i in range n, g i
 
 /-- **Summation by parts**, also known as **Abel's lemma** or an **Abel transformation** -/
 theorem sum_Ico_by_parts (hmn : m < n) :

src/algebraic_geometry/presheafed_space/gluing.lean

@@ -98,11 +98,11 @@ namespace glue_data
 variables {C} (D : glue_data C)
 
 local notation `𝖣` := D.to_glue_data
-local notation `π₁` i `,` j `,` k := @pullback.fst _ _ _ _ _ (D.f i j) (D.f i k) _
-local notation `π₂` i `,` j `,` k := @pullback.snd _ _ _ _ _ (D.f i j) (D.f i k) _
-local notation `π₁⁻¹` i `,` j `,` k :=
+local notation `π₁ `i`, `j`, `k := @pullback.fst _ _ _ _ _ (D.f i j) (D.f i k) _
+local notation `π₂ `i`, `j`, `k := @pullback.snd _ _ _ _ _ (D.f i j) (D.f i k) _
+local notation `π₁⁻¹ `i`, `j`, `k :=
 (PresheafedSpace.is_open_immersion.pullback_fst_of_right (D.f i j) (D.f i k)).inv_app
-local notation `π₂⁻¹` i `,` j `,` k :=
+local notation `π₂⁻¹ `i`, `j`, `k :=
 (PresheafedSpace.is_open_immersion.pullback_snd_of_left (D.f i j) (D.f i k)).inv_app
 
 /-- The glue data of topological spaces associated to a family of glue data of PresheafedSpaces. -/

src/algebraic_geometry/projective_spectrum/scheme.lean

@@ -79,13 +79,13 @@ local notation `Proj| ` U := Proj .restrict (opens.open_embedding (U : opens Pro
 local notation `Proj.T| ` U :=
   (Proj .restrict (opens.open_embedding (U : opens Proj.T))).to_SheafedSpace.to_PresheafedSpace.1
 -- the underlying topological space of `Proj` restricted to some open set
-local notation `pbo` x := projective_spectrum.basic_open 𝒜 x
+local notation `pbo ` x := projective_spectrum.basic_open 𝒜 x
 -- basic open sets in `Proj`
-local notation `sbo` f := prime_spectrum.basic_open f
+local notation `sbo ` f := prime_spectrum.basic_open f
 -- basic open sets in `Spec`
-local notation `Spec` ring := Spec.LocallyRingedSpace_obj (CommRing.of ring)
+local notation `Spec ` ring := Spec.LocallyRingedSpace_obj (CommRing.of ring)
 -- `Spec` as a locally ringed space
-local notation `Spec.T` ring :=
+local notation `Spec.T ` ring :=
   (Spec.LocallyRingedSpace_obj (CommRing.of ring)).to_SheafedSpace.to_PresheafedSpace.1
 -- the underlying topological space of `Spec`
 
@@ -121,7 +121,7 @@ def degree_zero_part {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) : subring (away f)
 
 end
 
-local notation `A⁰_` f_deg := degree_zero_part f_deg
+local notation `A⁰_ ` f_deg := degree_zero_part f_deg
 
 section
 

src/algebraic_topology/simplicial_object.lean

@@ -36,7 +36,7 @@ def simplicial_object := simplex_categoryᵒᵖ ⥤ C
 
 namespace simplicial_object
 
-localized "notation (name := simplicial_object.at) X `_[`:1000 n `]` :=
+localized "notation (name := simplicial_object.at) X ` _[`:1000 n `]` :=
   (X : category_theory.simplicial_object hole!).obj (opposite.op (simplex_category.mk n))"
   in simplicial
 
@@ -265,7 +265,7 @@ def cosimplicial_object := simplex_category ⥤ C
 
 namespace cosimplicial_object
 
-localized "notation (name := cosimplicial_object.at) X `_[`:1000 n `]` :=
+localized "notation (name := cosimplicial_object.at) X ` _[`:1000 n `]` :=
   (X : category_theory.cosimplicial_object hole!).obj (simplex_category.mk n)" in simplicial
 
 instance {J : Type v} [small_category J] [has_limits_of_shape J C] :

src/analysis/inner_product_space/l2_space.lean

@@ -89,7 +89,7 @@ variables {𝕜 : Type*} [is_R_or_C 𝕜] {E : Type*} [inner_product_space 𝕜
 variables {G : ι → Type*} [Π i, inner_product_space 𝕜 (G i)]
 local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y
 
-notation `ℓ²(` ι `,` 𝕜 `)` := lp (λ i : ι, 𝕜) 2
+notation `ℓ²(`ι`, `𝕜`)` := lp (λ i : ι, 𝕜) 2
 
 /-! ### Inner product space structure on `lp G 2` -/
 

src/data/bracket.lean

@@ -34,4 +34,4 @@ these are the Unicode "square with quill" brackets rather than the usual square
      `K` of a group. -/
 class has_bracket (L M : Type*) := (bracket : L → M → M)
 
-notation `⁅`x`,` y`⁆` := has_bracket.bracket x y
+notation `⁅`x`, `y`⁆` := has_bracket.bracket x y

src/data/bundle.lean

@@ -73,7 +73,7 @@ instance {x : B} : has_coe_t (E x) (total_space E) := ⟨total_space_mk x⟩
 lemma to_total_space_coe {x : B} (v : E x) : (v : total_space E) = total_space_mk x v := rfl
 
 -- notation for the direct sum of two bundles over the same base
-notation E₁ `×ᵇ`:100 E₂ := λ x, E₁ x × E₂ x
+notation E₁ ` ×ᵇ `:100 E₂ := λ x, E₁ x × E₂ x
 
 /-- `bundle.trivial B F` is the trivial bundle over `B` of fiber `F`. -/
 def trivial (B : Type*) (F : Type*) : B → Type* := function.const B F

src/data/finset/fold.lean

@@ -18,7 +18,7 @@ variables {α β γ : Type*}
 /-! ### fold -/
 section fold
 variables (op : β → β → β) [hc : is_commutative β op] [ha : is_associative β op]
-local notation (name := op) a * b := op a b
+local notation (name := op) a ` * ` b := op a b
 include hc ha
 
 /-- `fold op b f s` folds the commutative associative operation `op` over the

src/data/list/basic.lean

@@ -2459,8 +2459,8 @@ end foldl_eq_foldlr'
 
 section
 variables {op : α → α → α} [ha : is_associative α op] [hc : is_commutative α op]
-local notation (name := op) a * b := op a b
-local notation (name := foldl) l <*> a := foldl op a l
+local notation (name := op) a ` * ` b := op a b
+local notation (name := foldl) l ` <*> ` a := foldl op a l
 
 include ha
 

src/data/list/perm.lean

@@ -457,8 +457,8 @@ end
 
 section
 variables {op : α → α → α} [is_associative α op] [is_commutative α op]
-local notation (name := op) a * b := op a b
-local notation (name := foldl) l <*> a := foldl op a l
+local notation (name := op) a ` * ` b := op a b
+local notation (name := foldl) l ` <*> ` a := foldl op a l
 
 lemma perm.fold_op_eq {l₁ l₂ : list α} {a : α} (h : l₁ ~ l₂) : l₁ <*> a = l₂ <*> a :=
 h.foldl_eq (right_comm _ is_commutative.comm is_associative.assoc) _

src/data/multiset/fold.lean

@@ -16,7 +16,7 @@ variables {α β : Type*}
 /-! ### fold -/
 section fold
 variables (op : α → α → α) [hc : is_commutative α op] [ha : is_associative α op]
-local notation (name := op) a * b := op a b
+local notation (name := op) a ` * ` b := op a b
 include hc ha
 
 /-- `fold op b s` folds a commutative associative operation `op` over

src/data/nat/factorization/basic.lean

@@ -291,8 +291,8 @@ the $p$-adic order/valuation of a number, and `proj` and `compl` are for the pro
 complementary projection. The term `n.factorization p` is the $p$-adic order itself.
 For example, `ord_proj[2] n` is the even part of `n` and `ord_compl[2] n` is the odd part. -/
 
-notation `ord_proj[` p `]` n:max := p ^ (nat.factorization n p)
-notation `ord_compl[` p `]` n:max := n / ord_proj[p] n
+notation `ord_proj[` p `] ` n:max := p ^ (nat.factorization n p)
+notation `ord_compl[` p `] ` n:max := n / ord_proj[p] n
 
 @[simp] lemma ord_proj_of_not_prime (n p : ℕ) (hp : ¬ p.prime) : ord_proj[p] n = 1 :=
 by simp [factorization_eq_zero_of_non_prime n hp]

src/data/rat/nnrat.lean

@@ -31,7 +31,7 @@ open_locale big_operators
   densely_ordered, archimedean, inhabited]]
 def nnrat := {q : ℚ // 0 ≤ q}
 
-localized "notation ` ℚ≥0 ` := nnrat" in nnrat
+localized "notation (name := nnrat) `ℚ≥0` := nnrat" in nnrat
 
 namespace nnrat
 variables {α : Type*} {p q : ℚ≥0}

src/data/rbtree/insert.lean

@@ -188,7 +188,7 @@ parameters {α : Type u} (lt : α → α → Prop)
 
 local attribute [simp] mem balance1_node balance2_node
 
-local infix (name := mem) `∈` := mem lt
+local infix (name := mem) ` ∈ ` := mem lt
 
 lemma mem_balance1_node_of_mem_left {x s} (v) (t : rbnode α) : x ∈ s → x ∈ balance1_node s v t :=
 begin

src/data/real/nnreal.lean

@@ -59,7 +59,7 @@ open_locale classical big_operators
   linear_ordered_semiring, ordered_comm_semiring, canonically_ordered_comm_semiring,
   has_sub, has_ordered_sub, has_div, inhabited]]
 def nnreal := {r : ℝ // 0 ≤ r}
-localized "notation (name := nnreal) ` ℝ≥0 ` := nnreal" in nnreal
+localized "notation (name := nnreal) `ℝ≥0` := nnreal" in nnreal
 
 namespace nnreal
 

src/geometry/manifold/derivation_bundle.lean

@@ -35,7 +35,7 @@ instance smooth_functions_tower : is_scalar_tower 𝕜 C^∞⟮I, M; 𝕜⟯ C^
 which is defined as `f • r = f(x) * r`. -/
 @[nolint unused_arguments] def pointed_smooth_map (x : M) := C^n⟮I, M; 𝕜⟯
 
-localized "notation (name := pointed_smooth_map) `C^` n `⟮` I `,` M `;` 𝕜 `⟯⟨` x `⟩` :=
+localized "notation (name := pointed_smooth_map) `C^` n `⟮` I `, ` M `; ` 𝕜 `⟯⟨` x `⟩` :=
   pointed_smooth_map 𝕜 I M n x" in derivation
 
 variables {𝕜 M}

src/geometry/manifold/diffeomorph.lean

@@ -77,9 +77,9 @@ structure diffeomorph extends M ≃ M' :=
 
 end defs
 
-localized "notation (name := diffeomorph) M ` ≃ₘ^` n:1000 `⟮`:50 I `,` J `⟯ ` N :=
+localized "notation (name := diffeomorph) M ` ≃ₘ^` n:1000 `⟮`:50 I `, ` J `⟯ ` N :=
   diffeomorph I J M N n" in manifold
-localized "notation (name := diffeomorph.top) M ` ≃ₘ⟮` I `,` J `⟯ ` N :=
+localized "notation (name := diffeomorph.top) M ` ≃ₘ⟮` I `, ` J `⟯ ` N :=
   diffeomorph I J M N ⊤" in manifold
 localized "notation (name := diffeomorph.self) E ` ≃ₘ^` n:1000 `[`:50 𝕜 `] ` E' :=
   diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' n" in manifold

src/group_theory/eckmann_hilton.lean

@@ -27,7 +27,7 @@ universe u
 namespace eckmann_hilton
 variables {X : Type u}
 
-local notation a `<`m`>` b := m a b
+local notation a ` <`m`> ` b := m a b
 
 /-- `is_unital m e` expresses that `e : X` is a left and right unit
 for the binary operation `m : X → X → X`. -/

src/linear_algebra/matrix/determinant.lean

@@ -47,7 +47,7 @@ open_locale matrix big_operators
 variables {m n : Type*} [decidable_eq n] [fintype n] [decidable_eq m] [fintype m]
 variables {R : Type v} [comm_ring R]
 
-local notation `ε` σ:max := ((sign σ : ℤ ) : R)
+local notation `ε ` σ:max := ((sign σ : ℤ) : R)
 
 
 /-- `det` is an `alternating_map` in the rows of the matrix. -/

src/linear_algebra/span.lean

@@ -202,7 +202,7 @@ by rw [submodule.span_union, p.span_eq]
 
 /- Note that the character `∙` U+2219 used below is different from the scalar multiplication
 character `•` U+2022 and the matrix multiplication character `⬝` U+2B1D. -/
-notation R`∙`:1000 x := span R (@singleton _ _ set.has_singleton x)
+notation R` ∙ `:1000 x := span R (@singleton _ _ set.has_singleton x)
 
 lemma span_eq_supr_of_singleton_spans (s : set M) : span R s = ⨆ x ∈ s, R ∙ x :=
 by simp only [←span_Union, set.bUnion_of_singleton s]

src/linear_algebra/special_linear_group.lean

@@ -63,7 +63,7 @@ def special_linear_group := { A : matrix n n R // A.det = 1 }
 end
 
 localized "notation (name := special_linear_group.fin)
-  `SL(` n `,` R `)`:= matrix.special_linear_group (fin n) R" in matrix_groups
+  `SL(`n`, `R`)`:= matrix.special_linear_group (fin n) R" in matrix_groups
 
 namespace special_linear_group
 

src/linear_algebra/tensor_power.lean

@@ -66,7 +66,7 @@ def mul_equiv {n m : ℕ} : (⨂[R]^n M) ⊗[R] (⨂[R]^m M) ≃ₗ[R] ⨂[R]^(n
 instance ghas_mul : graded_monoid.ghas_mul (λ i, ⨂[R]^i M) :=
 { mul := λ i j a b, mul_equiv (a ⊗ₜ b) }
 
-local infix `ₜ*`:70 := @graded_monoid.ghas_mul.mul ℕ (λ i, ⨂[R]^i M) _ _ _ _
+local infix ` ₜ* `:70 := @graded_monoid.ghas_mul.mul ℕ (λ i, ⨂[R]^i M) _ _ _ _
 
 lemma ghas_mul_def {i j} (a : ⨂[R]^i M) (b : ⨂[R]^j M) : a ₜ* b = mul_equiv (a ⊗ₜ b) := rfl
 

src/logic/function/basic.lean

@@ -622,7 +622,7 @@ def bicompr (f : γ → δ) (g : α → β → γ) (a b) :=
 f (g a b)
 
 -- Suggested local notation:
-local notation f `∘₂` g := bicompr f g
+local notation f ` ∘₂ ` g := bicompr f g
 
 lemma uncurry_bicompr (f : α → β → γ) (g : γ → δ) :
   uncurry (g ∘₂ f) = (g ∘ uncurry f) := rfl

src/logic/relator.lean

@@ -26,7 +26,7 @@ variables (R : α → β → Prop) (S : γ → δ → Prop)
 def lift_fun (f : α → γ) (g : β → δ) : Prop :=
 ∀⦃a b⦄, R a b → S (f a) (g b)
 
-infixr ⇒ := lift_fun
+infixr ` ⇒ ` := lift_fun
 
 end
 

src/measure_theory/integral/divergence_theorem.lean

@@ -61,7 +61,7 @@ variables {n : ℕ}
 local notation `ℝⁿ` := fin n → ℝ
 local notation `ℝⁿ⁺¹` := fin (n + 1) → ℝ
 local notation `Eⁿ⁺¹` := fin (n + 1) → E
-local notation `e` i := pi.single i 1
+local notation `e ` i := pi.single i 1
 
 section
 
@@ -230,9 +230,9 @@ end
 
 variables (a b : ℝⁿ⁺¹)
 
-local notation `face` i := set.Icc (a ∘ fin.succ_above i) (b ∘ fin.succ_above i)
-local notation `front_face` i:2000 := fin.insert_nth i (b i)
-local notation `back_face` i:2000 := fin.insert_nth i (a i)
+local notation `face ` i := set.Icc (a ∘ fin.succ_above i) (b ∘ fin.succ_above i)
+local notation `front_face ` i:2000 := fin.insert_nth i (b i)
+local notation `back_face ` i:2000 := fin.insert_nth i (a i)
 
 /-- **Divergence theorem** for Bochner integral. If `f : ℝⁿ⁺¹ → Eⁿ⁺¹` is continuous on a rectangular
 box `[a, b] : set ℝⁿ⁺¹`, `a ≤ b`, is differentiable on its interior with derivative

src/measure_theory/integral/torus_integral.lean

@@ -60,14 +60,14 @@ noncomputable theory
 open complex set measure_theory function filter topological_space
 open_locale real big_operators
 
-local notation `ℝ⁰`:= fin 0 → ℝ
-local notation `ℂ⁰`:= fin 0 → ℂ
-local notation `ℝ¹`:= fin 1 → ℝ
-local notation `ℂ¹`:= fin 1 → ℂ
-local notation `ℝⁿ`:= fin n → ℝ
-local notation `ℂⁿ`:= fin n → ℂ
-local notation `ℝⁿ⁺¹`:= fin (n + 1) → ℝ
-local notation `ℂⁿ⁺¹`:= fin (n + 1) → ℂ
+local notation `ℝ⁰` := fin 0 → ℝ
+local notation `ℂ⁰` := fin 0 → ℂ
+local notation `ℝ¹` := fin 1 → ℝ
+local notation `ℂ¹` := fin 1 → ℂ
+local notation `ℝⁿ` := fin n → ℝ
+local notation `ℂⁿ` := fin n → ℂ
+local notation `ℝⁿ⁺¹` := fin (n + 1) → ℝ
+local notation `ℂⁿ⁺¹` := fin (n + 1) → ℂ
 
 /-!
 ### `torus_map`, a generalization of a torus

src/order/basic.lean

@@ -555,8 +555,8 @@ end min_max_rec
 /-- Typeclass for the `⊓` (`\glb`) notation -/
 @[notation_class] class has_inf (α : Type u) := (inf : α → α → α)
 
-infix ⊔ := has_sup.sup
-infix ⊓ := has_inf.inf
+infix ` ⊔ ` := has_sup.sup
+infix ` ⊓ ` := has_inf.inf
 
 /-! ### Lifts of order instances -/
 

src/ring_theory/derivation.lean

@@ -563,7 +563,7 @@ Note that the slash is `\textfractionsolidus`.
 @[derive [add_comm_group, module R, module S, module (S ⊗[R] S)]]
 def kaehler_differential : Type* := (kaehler_differential.ideal R S).cotangent
 
-notation `Ω[ `:100 S ` ⁄ `:0 R ` ]`:0 := kaehler_differential R S
+notation `Ω[`:100 S `⁄`:0 R `]`:0 := kaehler_differential R S
 
 instance : nonempty Ω[S⁄R] := ⟨0⟩
 

src/ring_theory/witt_vector/isocrystal.lean

@@ -59,7 +59,7 @@ namespace witt_vector
 variables (p : ℕ) [fact p.prime]
 variables (k : Type*) [comm_ring k]
 localized "notation (name := witt_vector.fraction_ring)
-  `K(` p`,` k`)` := fraction_ring (witt_vector p k)" in isocrystal
+  `K(`p`, `k`)` := fraction_ring (witt_vector p k)" in isocrystal
 
 section perfect_ring
 variables [is_domain k] [char_p k p] [perfect_ring k p]
@@ -74,7 +74,7 @@ is_fraction_ring.field_equiv_of_ring_equiv (frobenius_equiv p k)
 def fraction_ring.frobenius_ring_hom : K(p, k) →+* K(p, k) := fraction_ring.frobenius p k
 
 localized "notation (name := witt_vector.frobenius_ring_hom)
-  `φ(` p`,` k`)` := witt_vector.fraction_ring.frobenius_ring_hom p k" in isocrystal
+  `φ(`p`, `k`)` := witt_vector.fraction_ring.frobenius_ring_hom p k" in isocrystal
 
 instance inv_pair₁ : ring_hom_inv_pair (φ(p, k)) _ :=
 ring_hom_inv_pair.of_ring_equiv (fraction_ring.frobenius p k)
@@ -83,9 +83,9 @@ instance inv_pair₂ :
   ring_hom_inv_pair ((fraction_ring.frobenius p k).symm : K(p, k) →+* K(p, k)) _ :=
 ring_hom_inv_pair.of_ring_equiv (fraction_ring.frobenius p k).symm
 
-localized "notation (name := frobenius_ring_hom.linear_map) M ` →ᶠˡ[`:50 p `,` k `] ` M₂ :=
+localized "notation (name := frobenius_ring_hom.linear_map) M ` →ᶠˡ[`:50 p `, ` k `] ` M₂ :=
   linear_map (witt_vector.fraction_ring.frobenius_ring_hom p k) M M₂" in isocrystal
-localized "notation (name := frobenius_ring_hom.linear_equiv) M ` ≃ᶠˡ[`:50 p `,` k `] ` M₂ :=
+localized "notation (name := frobenius_ring_hom.linear_equiv) M ` ≃ᶠˡ[`:50 p `, ` k `] ` M₂ :=
   linear_equiv (witt_vector.fraction_ring.frobenius_ring_hom p k) M M₂" in isocrystal
 
 /-! ### Isocrystals -/
@@ -108,7 +108,7 @@ Project the Frobenius automorphism from an isocrystal. Denoted by `Φ(p, k)` whe
 def isocrystal.frobenius : V ≃ᶠˡ[p, k] V := @isocrystal.frob p _ k _ _ _ _ _ _ _
 variables (V)
 
-localized "notation `Φ(` p`,` k`)` := witt_vector.isocrystal.frobenius p k" in isocrystal
+localized "notation `Φ(`p`, `k`)` := witt_vector.isocrystal.frobenius p k" in isocrystal
 
 /-- A homomorphism between isocrystals respects the Frobenius map. -/
 @[nolint has_nonempty_instance]
@@ -121,9 +121,9 @@ structure isocrystal_equiv extends V ≃ₗ[K(p, k)] V₂ :=
 ( frob_equivariant : ∀ x : V, Φ(p, k) (to_linear_equiv x) = to_linear_equiv (Φ(p, k) x) )
 
 localized "notation (name := isocrystal_hom)
-  M ` →ᶠⁱ[`:50 p `,` k `] ` M₂ := witt_vector.isocrystal_hom p k M M₂" in isocrystal
+  M ` →ᶠⁱ[`:50 p `, ` k `] ` M₂ := witt_vector.isocrystal_hom p k M M₂" in isocrystal
 localized "notation (name := isocrystal_equiv)
-  M ` ≃ᶠⁱ[`:50 p `,` k `] ` M₂ := witt_vector.isocrystal_equiv p k M M₂" in isocrystal
+  M ` ≃ᶠⁱ[`:50 p `, ` k `] ` M₂ := witt_vector.isocrystal_equiv p k M M₂" in isocrystal
 
 
 end perfect_ring