diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean
index 6e351bb8a017b..8e91f9921edad 100644
--- a/Mathlib/Algebra/BigOperators/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/Basic.lean
@@ -279,7 +279,7 @@ end Deprecated
 
 @[to_additive]
 theorem MonoidHom.coe_finset_prod [MulOneClass β] [CommMonoid γ] (f : α → β →* γ) (s : Finset α) :
-    ⇑(∏ x in s, f x) = ∏ x in s, ⇑f x :=
+    ⇑(∏ x in s, f x) = ∏ x in s, ⇑(f x) :=
   (MonoidHom.coeFn β γ).map_prod _ _
 #align monoid_hom.coe_finset_prod MonoidHom.coe_finset_prod
 #align add_monoid_hom.coe_finset_sum AddMonoidHom.coe_finset_sum
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean b/Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean
index 86f7212fd49bb..a803a38428174 100644
--- a/Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean
+++ b/Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean
@@ -92,7 +92,7 @@ attribute [local instance] ConcreteCategory.funLike
 def mkHasForget₂ {d : Type u → Type u} {hom_d : ∀ ⦃α β : Type u⦄ (_ : d α) (_ : d β), Type u}
     [BundledHom hom_d] (obj : ∀ ⦃α⦄, c α → d α)
     (map : ∀ {X Y : Bundled c}, (X ⟶ Y) → (Bundled.map @obj X ⟶ (Bundled.map @obj Y)))
-    (h_map : ∀ {X Y : Bundled c} (f : X ⟶ Y), ⇑map f = ⇑f) :
+    (h_map : ∀ {X Y : Bundled c} (f : X ⟶ Y), ⇑(map f) = ⇑f) :
     HasForget₂ (Bundled c) (Bundled d) :=
   HasForget₂.mk' (Bundled.map @obj) (fun _ => rfl) map (by
     intros X Y f
diff --git a/Mathlib/Data/DFinsupp/Basic.lean b/Mathlib/Data/DFinsupp/Basic.lean
index 1113e53e44ecb..705fbee0000a5 100644
--- a/Mathlib/Data/DFinsupp/Basic.lean
+++ b/Mathlib/Data/DFinsupp/Basic.lean
@@ -295,7 +295,7 @@ instance addCommMonoid [∀ i, AddCommMonoid (β i)] : AddCommMonoid (Π₀ i, 
 
 @[simp]
 theorem coe_finset_sum {α} [∀ i, AddCommMonoid (β i)] (s : Finset α) (g : α → Π₀ i, β i) :
-    ⇑(∑ a in s, g a) = ∑ a in s, ⇑g a :=
+    ⇑(∑ a in s, g a) = ∑ a in s, ⇑(g a) :=
   (coeFnAddMonoidHom : _ →+ ∀ i, β i).map_sum g s
 #align dfinsupp.coe_finset_sum DFinsupp.coe_finset_sum
 
@@ -2272,7 +2272,7 @@ variable [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
 
 @[to_additive]
 theorem coe_dfinsupp_prod [Monoid R] [CommMonoid S] (f : Π₀ i, β i) (g : ∀ i, β i → R →* S) :
-    ⇑(f.prod g) = f.prod fun a b => ⇑g a b :=
+    ⇑(f.prod g) = f.prod fun a b => ⇑(g a b) :=
   coe_finset_prod _ _
 #align monoid_hom.coe_dfinsupp_prod MonoidHom.coe_dfinsupp_prod
 #align add_monoid_hom.coe_dfinsupp_sum AddMonoidHom.coe_dfinsupp_sum
diff --git a/Mathlib/LinearAlgebra/Ray.lean b/Mathlib/LinearAlgebra/Ray.lean
index cc3ac441c34d1..ac70bc5f0308a 100644
--- a/Mathlib/LinearAlgebra/Ray.lean
+++ b/Mathlib/LinearAlgebra/Ray.lean
@@ -507,7 +507,7 @@ variable {M : Type*} [AddCommGroup M] [Module R M]
 
 -- Porting note: Needed to add coercion ↥ below
 /-- `SameRay` follows from membership of `MulAction.orbit` for the `Units.posSubgroup`. -/
-theorem sameRay_of_mem_orbit {v₁ v₂ : M} (h : v₁ ∈ MulAction.orbit (↥Units.posSubgroup R) v₂) :
+theorem sameRay_of_mem_orbit {v₁ v₂ : M} (h : v₁ ∈ MulAction.orbit ↥(Units.posSubgroup R) v₂) :
     SameRay R v₁ v₂ := by
   rcases h with ⟨⟨r, hr : 0 < r.1⟩, rfl : r • v₂ = v₁⟩
   exact SameRay.sameRay_pos_smul_left _ hr
diff --git a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
index bdaea4e4863fa..6dc3fe1552f50 100644
--- a/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
+++ b/Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
@@ -1619,7 +1619,7 @@ def piCongrLeft (f : δ ≃ δ') : (∀ b, π (f b)) ≃ᵐ ∀ a, π a := by
   exact fun i => measurable_pi_apply (f i)
 
 theorem coe_piCongrLeft (f : δ ≃ δ') :
-    ⇑MeasurableEquiv.piCongrLeft π f = f.piCongrLeft π := by rfl
+    ⇑(MeasurableEquiv.piCongrLeft π f) = f.piCongrLeft π := by rfl
 
 /-- Pi-types are measurably equivalent to iterated products. -/
 @[simps! (config := .asFn)]
@@ -1690,7 +1690,7 @@ def sumPiEquivProdPi (α : δ ⊕ δ' → Type*) [∀ i, MeasurableSpace (α i)]
     exact measurable_pi_iff.1 measurable_snd _
 
 theorem coe_sumPiEquivProdPi (α : δ ⊕ δ' → Type*) [∀ i, MeasurableSpace (α i)] :
-    ⇑MeasurableEquiv.sumPiEquivProdPi α = Equiv.sumPiEquivProdPi α := by rfl
+    ⇑(MeasurableEquiv.sumPiEquivProdPi α) = Equiv.sumPiEquivProdPi α := by rfl
 
 theorem coe_sumPiEquivProdPi_symm (α : δ ⊕ δ' → Type*) [∀ i, MeasurableSpace (α i)] :
     ⇑(MeasurableEquiv.sumPiEquivProdPi α).symm = (Equiv.sumPiEquivProdPi α).symm := by rfl
diff --git a/Mathlib/Order/Hom/Basic.lean b/Mathlib/Order/Hom/Basic.lean
index 4cf179a2f4040..13d8af2094d55 100644
--- a/Mathlib/Order/Hom/Basic.lean
+++ b/Mathlib/Order/Hom/Basic.lean
@@ -709,7 +709,7 @@ def ofMapLEIff {α β} [PartialOrder α] [Preorder β] (f : α → β) (hf : ∀
 
 @[simp]
 theorem coe_ofMapLEIff {α β} [PartialOrder α] [Preorder β] {f : α → β} (h) :
-    ⇑ofMapLEIff f h = f :=
+    ⇑(ofMapLEIff f h) = f :=
   rfl
 #align order_embedding.coe_of_map_le_iff OrderEmbedding.coe_ofMapLEIff
 
@@ -720,7 +720,7 @@ def ofStrictMono {α β} [LinearOrder α] [Preorder β] (f : α → β) (h : Str
 
 @[simp]
 theorem coe_ofStrictMono {α β} [LinearOrder α] [Preorder β] {f : α → β} (h : StrictMono f) :
-    ⇑ofStrictMono f h = f :=
+    ⇑(ofStrictMono f h) = f :=
   rfl
 #align order_embedding.coe_of_strict_mono OrderEmbedding.coe_ofStrictMono
 
@@ -839,7 +839,7 @@ def refl (α : Type*) [LE α] : α ≃o α :=
 #align order_iso.refl OrderIso.refl
 
 @[simp]
-theorem coe_refl : ⇑refl α = id :=
+theorem coe_refl : ⇑(refl α) = id :=
   rfl
 #align order_iso.coe_refl OrderIso.coe_refl
 
@@ -902,7 +902,7 @@ def trans (e : α ≃o β) (e' : β ≃o γ) : α ≃o γ :=
 #align order_iso.trans OrderIso.trans
 
 @[simp]
-theorem coe_trans (e : α ≃o β) (e' : β ≃o γ) : ⇑e.trans e' = e' ∘ e :=
+theorem coe_trans (e : α ≃o β) (e' : β ≃o γ) : ⇑(e.trans e') = e' ∘ e :=
   rfl
 #align order_iso.coe_trans OrderIso.coe_trans
 
@@ -957,7 +957,7 @@ def dualDual : α ≃o αᵒᵈᵒᵈ :=
 #align order_iso.dual_dual OrderIso.dualDual
 
 @[simp]
-theorem coe_dualDual : ⇑dualDual α = toDual ∘ toDual :=
+theorem coe_dualDual : ⇑(dualDual α) = toDual ∘ toDual :=
   rfl
 #align order_iso.coe_dual_dual OrderIso.coe_dualDual
 
@@ -1129,7 +1129,7 @@ def toOrderIso (e : α ≃ β) (h₁ : Monotone e) (h₂ : Monotone e.symm) : α
 
 @[simp]
 theorem coe_toOrderIso (e : α ≃ β) (h₁ : Monotone e) (h₂ : Monotone e.symm) :
-    ⇑e.toOrderIso h₁ h₂ = e :=
+    ⇑(e.toOrderIso h₁ h₂) = e :=
   rfl
 #align equiv.coe_to_order_iso Equiv.coe_toOrderIso
 
diff --git a/Mathlib/Tactic/Coe.lean b/Mathlib/Tactic/Coe.lean
index 37b09bfa4be40..5c9fe13825b5d 100644
--- a/Mathlib/Tactic/Coe.lean
+++ b/Mathlib/Tactic/Coe.lean
@@ -44,9 +44,8 @@ elab "(" "↑" ")" : term <= expectedType =>
       throwError "cannot coerce{indentExpr x}\nto type{indentExpr b}"
 
 /-- `⇑ t` coerces `t` to a function. -/
--- We increase the right precedence so this goes above most binary operators.
--- Otherwise `⇑f = g` will parse as `⇑(f = g)`.
-elab "⇑" m:term:80 : term => do
+-- the precedence matches that of `coeNotation`
+elab:1024 (name := coeFunNotation) "⇑" m:term:1024 : term => do
   let x ← elabTerm m none
   if let some ty ← coerceToFunction? x then
     return ty
@@ -62,7 +61,7 @@ elab "(" "⇑" ")" : term <= expectedType =>
       throwError "cannot coerce to function{indentExpr x}"
 
 /-- `↥ t` coerces `t` to a type. -/
-elab "↥" t:term:80 : term => do
+elab:1024 (name := coeSortNotation) "↥" t:term:1024 : term => do
   let x ← elabTerm t none
   if let some ty ← coerceToSort? x then
     return ty