diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index bd6c8afe02..050581e1b6 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -1270,7 +1270,7 @@ If it resolves to `name`, returns `(S', name)`.
 private partial def findMethod? (structName fieldName : Name) : MetaM (Option (Name × Name)) := do
   let env ← getEnv
   let find? structName' : MetaM (Option (Name × Name)) := do
-    let fullName := structName' ++ fieldName
+    let fullName := privateToUserName structName' ++ fieldName
     -- We do not want to make use of the current namespace for resolution.
     let candidates := ResolveName.resolveGlobalName (← getEnv) Name.anonymous (← getOpenDecls) fullName
       |>.filter (fun (_, fieldList) => fieldList.isEmpty)
diff --git a/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean b/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean
index 2affb6634d..dee0ec76e0 100644
--- a/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean
@@ -44,16 +44,25 @@ private def projInfo (c : Name) : MetaM (Option (Name × Nat × Bool × Bool ×
   else
     return none
 
+/--
+Checks that `e` is an application of a constant that equals `baseName`, taking into consideration private name mangling.
+-/
+private def isAppOfBaseName (env : Environment) (e : Expr) (baseName : Name) : Bool :=
+  if let some c := e.cleanupAnnotations.getAppFn.constName? then
+    privateToUserName c == baseName && !isInaccessiblePrivateName env c
+  else
+    false
+
 /--
 Like `Lean.Elab.Term.typeMatchesBaseName` but does not use `Function` for pi types.
 -/
 private partial def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do
   withReducibleAndInstances do
-    if type.cleanupAnnotations.isAppOf baseName then
+    if isAppOfBaseName (← getEnv) type baseName then
       return true
     else
       let type ← whnfCore type
-      if type.isAppOf baseName then
+      if isAppOfBaseName (← getEnv) type baseName then
         return true
       else
         match ← unfoldDefinition? type with
@@ -66,10 +75,10 @@ returns the field name and the index for the argument to be used as the object o
 Otherwise it fails.
 -/
 private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name × Nat) := do
-  let .str _ field := c | failure
-  let field := Name.mkSimple field
-  let baseName := c.getPrefix
+  let .str baseName field := c | failure
+  let baseName := privateToUserName baseName
   guard <| !baseName.isAnonymous
+  let field := Name.mkSimple field
   -- Disallow `Function` since it is used for pi types.
   guard <| baseName != `Function
   let info ← getConstInfo c
@@ -87,7 +96,7 @@ private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name ×
         -- We require an exact match for the base name.
         -- While `Lean.Elab.Term.resolveLValLoop` is able to unfold the type and iterate, we do not attempt to exploit this feature.
         -- (To get it right, we would need to check that each relevant namespace does not contain a declaration named `field`.)
-        guard <| (← instantiateMVars <| ← inferType args[i]!).consumeMData.isAppOf baseName
+        guard <| isAppOfBaseName (← getEnv) (← instantiateMVars <| ← inferType args[i]!) baseName
         return (field, i)
       else
         -- We only use the first explicit argument for field notation.
@@ -107,6 +116,8 @@ returns the field name to use and the argument index for the object of the field
 def fieldNotationCandidate? (f : Expr) (args : Array Expr) (useGeneralizedFieldNotation : Bool) : MetaM (Option (Name × Nat)) := do
   let env ← getEnv
   let .const c .. := f.consumeMData | return none
+  if isInaccessiblePrivateName (← getEnv) c then
+    return none
   if c.getPrefix.isAnonymous then return none
   -- If there is `pp_nodot` on this function, then don't use field notation for it.
   if hasPPNoDotAttribute env c then
diff --git a/tests/lean/private.lean.expected.out b/tests/lean/private.lean.expected.out
index adb893faeb..a12cfe4ae2 100644
--- a/tests/lean/private.lean.expected.out
+++ b/tests/lean/private.lean.expected.out
@@ -8,6 +8,6 @@ Boo.Bla.boo == "world" : Bool
 Boo.boo == 100 : Bool
 Boo.Bla.boo == "world" : Bool
 Boo.boo == 100 : Bool
-Nat.mul10 x : Nat
+x.mul10 : Nat
 private.lean:65:12-65:13: error: a non-private declaration `y` has already been declared
 private.lean:68:4-68:5: error: a private declaration `z` has already been declared
diff --git a/tests/lean/run/cleanupTypeAnnotations.lean b/tests/lean/run/cleanupTypeAnnotations.lean
index 1a391fc6d4..a98674f60e 100644
--- a/tests/lean/run/cleanupTypeAnnotations.lean
+++ b/tests/lean/run/cleanupTypeAnnotations.lean
@@ -49,7 +49,7 @@ instance i1 (b := 0) : Decidable (a.toNat = b) :=
   have : True := by trace_state; trivial
   inferInstance
 
-/-- info: i1 (a : Bool := true) (b : Nat := 0) : Decidable (Bool.toNat a = b) -/
+/-- info: i1 (a : Bool := true) (b : Nat := 0) : Decidable (a.toNat = b) -/
 #guard_msgs in #check i1
 
 /-!
diff --git a/tests/lean/run/delabProjectionApp.lean b/tests/lean/run/delabProjectionApp.lean
index 452e9a53c1..624e412a20 100644
--- a/tests/lean/run/delabProjectionApp.lean
+++ b/tests/lean/run/delabProjectionApp.lean
@@ -184,3 +184,36 @@ set_option pp.notation false in
 set_option pp.notation false in set_option pp.fieldNotation.generalized false in
 /-- info: ∀ {α : Type} (s t : MySet α), MySet.MySubset s t : Prop -/
 #guard_msgs in #check ∀ {α : Type} (s t : MySet α), s ⊆⊆ t
+
+/-!
+Private definition on public type.
+-/
+private def Char.MyIsA (c : Char) : Prop := c = 'A'
+
+/-- info: ∀ (c : Char), c.MyIsA : Prop -/
+#guard_msgs in #check ∀ (c : Char), c.MyIsA
+
+/-!
+Public definition on public type.
+-/
+def Char.MyIsA' (c : Char) : Prop := c = 'A'
+
+/-- info: ∀ (c : Char), c.MyIsA' : Prop -/
+#guard_msgs in #check ∀ (c : Char), c.MyIsA'
+
+/-!
+Private definition on private type.
+-/
+private structure Char'
+private def Char'.MyIsA (_ : Char') : Prop := true
+
+/-- info: ∀ (c : Char'), c.MyIsA : Prop -/
+#guard_msgs in #check ∀ (c : Char'), c.MyIsA
+
+/-!
+Public definition on private type.
+-/
+def Char'.MyIsA' (_ : Char') : Prop := true
+
+/-- info: ∀ (c : Char'), c.MyIsA' : Prop -/
+#guard_msgs in #check ∀ (c : Char'), c.MyIsA'
diff --git a/tests/lean/run/grind_9572.lean b/tests/lean/run/grind_9572.lean
index f1bc1cff43..0bfc0c5aac 100644
--- a/tests/lean/run/grind_9572.lean
+++ b/tests/lean/run/grind_9572.lean
@@ -12,7 +12,7 @@ l : List Nat
 h :
   ¬List.Pairwise
       (fun x y =>
-        List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else [])
+        (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
           (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
       l
 ⊢ False
@@ -20,13 +20,13 @@ h :
   [facts] Asserted facts
     [prop] ¬List.Pairwise
             (fun x y =>
-              List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else [])
+              (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
                 (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
             l
   [eqc] False propositions
     [prop] List.Pairwise
           (fun x y =>
-            List.Disjoint (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else [])
+            (if x ^ i ≤ n then List.map (fun m => x :: m) (f x) else []).Disjoint
               (if y ^ i ≤ n then List.map (fun m => y :: m) (f y) else []))
           l
 -/