diff --git a/RELEASES.md b/RELEASES.md
index 0a8d627fde0b..1703a08cdc49 100644
--- a/RELEASES.md
+++ b/RELEASES.md
@@ -57,9 +57,9 @@ v4.8.0 (development in progress)
   rather than `{a := x, b := y, c := z}`.
   This attribute is applied to `Sigma`, `PSigma`, `PProd`, `Subtype`, `And`, and `Fin`.
 
-* Option `pp.structureProjections` is renamed to `pp.fieldNotation`, and there is a new suboption `pp.fieldNotation.generalized`
-  to enable pretty printing function applications using generalized field notation.
-  Field notation can now be disabled function-by-function using the `@[pp_nodot]` attribute.
+* Option `pp.structureProjections` is renamed to `pp.fieldNotation`, and there is now a suboption `pp.fieldNotation.generalized`
+  to enable pretty printing function applications using generalized field notation (defaults to true).
+  Field notation can be disabled on a function-by-function basis using the `@[pp_nodot]` attribute.
 
 Breaking changes:
 
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index b64b1cc60521..7f478004607b 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2755,7 +2755,7 @@ def List.redLength : List α → Nat
 /-- Convert a `List α` into an `Array α`. This is O(n) in the length of the list.  -/
 -- This function is exported to C, where it is called by `Array.mk`
 -- (the constructor) to implement this functionality.
-@[inline, match_pattern, export lean_list_to_array]
+@[inline, match_pattern, pp_nodot, export lean_list_to_array]
 def List.toArray (as : List α) : Array α :=
   as.toArrayAux (Array.mkEmpty as.redLength)
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean b/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean
index 2609f028f972..011eed94012e 100644
--- a/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean
@@ -17,12 +17,12 @@ namespace Lean.PrettyPrinter.Delaborator
 open Meta
 
 /--
-If this is a structure projection that could delaborate using dot notation,
+If this constant is a structure projection that could delaborate using dot notation,
 returns the field name, the number of parameters before the structure argument, and whether this is a parent projection.
 Otherwise it fails.
 -/
-private def projInfo (f : Expr) : MetaM (Name × Nat × Bool) := do
-  let .const c@(.str _ field) _ := f.consumeMData | failure
+private def projInfo (c : Name) : MetaM (Name × Nat × Bool) := do
+  let .str _ field := c | failure
   let field := Name.mkSimple field
   let env ← getEnv
   let some info := env.getProjectionFnInfo? c | failure
@@ -33,32 +33,46 @@ private def projInfo (f : Expr) : MetaM (Name × Nat × Bool) := do
   return (field, info.numParams, isParentProj)
 
 /--
-If this function application could delaborate using generalized field notation,
+Like `Lean.Elab.Term.typeMatchesBaseName` but does not use `Function` for pi types.
+-/
+private def typeMatchesBaseName (type : Expr) (baseName : Name) : MetaM Bool := do
+  if type.cleanupAnnotations.isAppOf baseName then
+    return true
+  else
+    return (← whnfR type).isAppOf baseName
+
+/--
+If this constant application could delaborate using generalized field notation with little confusion,
 returns the field name and the index for the argument to be used as the object of the field notation.
 Otherwise it fails.
 -/
-private def generalizedFieldInfo (f : Expr) (args : Array Expr) : MetaM (Name × Nat) := do
-  let .const name@(.str _ field) .. := f.consumeMData | failure
+private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name × Nat) := do
+  let .str _ field := c | failure
   let field := Name.mkSimple field
-  let baseName := name.getPrefix
+  let baseName := c.getPrefix
   guard <| !baseName.isAnonymous
-  Meta.forallBoundedTelescope (← instantiateMVars <| ← inferType f) args.size fun params _ => do
+  -- Disallow `Function` since it is used for pi types.
+  guard <| baseName != `Function
+  let info ← getConstInfo c
+  -- Search for the first argument that could be used for field notation
+  -- and make sure it is the first explicit argument.
+  Meta.forallBoundedTelescope info.type args.size fun params _ => do
     for i in [0:params.size] do
       let fvarId := params[i]!.fvarId!
-      if (← fvarId.getBinderInfo).isExplicit then
-        -- We only consider the first explicit argument, so fail if the parameter does not have the correct type.
-        guard <| (← fvarId.getType).cleanupAnnotations.isAppOf baseName
-        let argTy ← instantiateMVars <| ← inferType args[i]!
-        -- Generalized field notation allows either an an exact match, or a match after `whnfR`.
-        if argTy.consumeMData.isAppOf baseName then
-          return (field, i)
-        else if (← Meta.whnfR argTy).isAppOf baseName then
-          return (field, i)
-        else
-          failure
+      -- If there is a motive, we will treat this as a sort of control flow structure and so we won't use field notation.
+      -- Plus, recursors tend to be riskier when using dot notation.
+      if (← fvarId.getUserName) == `motive then
+        failure
+      if (← typeMatchesBaseName (← fvarId.getType) baseName) then
+        guard (← fvarId.getBinderInfo).isExplicit
+        -- 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
+        return (field, i)
       else
-        -- If not explicit, then make sure that this parameter can't be used for field notation.
-        guard <| ! (← fvarId.getType).cleanupAnnotations.isAppOf baseName
+        -- We only use the first explicit argument for field notation.
+        guard !(← fvarId.getBinderInfo).isExplicit
     failure
 
 /--
@@ -67,20 +81,20 @@ 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 name .. := f.consumeMData | return none
-  if name.getPrefix.isAnonymous then return none
+  let .const c .. := f.consumeMData | 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 name then
+  if hasPPNoDotAttribute env c then
     return none
   -- Handle structure projections
   try
-    let (field, numParams, _) ← projInfo f
+    let (field, numParams, _) ← projInfo c
     return (field, numParams)
   catch _ => pure ()
   -- Handle generalized field notation
   if useGeneralizedFieldNotation then
     try
-      return ← generalizedFieldInfo f args
+      return ← generalizedFieldInfo c args
     catch _ => pure ()
   -- It's not handled by any of the above.
   return none
@@ -92,7 +106,8 @@ If `explicit` is `true`, then further requires that the structure have no parame
 def isParentProj (explicit : Bool) (e : Expr) : MetaM Bool := do
   unless e.isApp do return false
   try
-    let (_, numParams, isParentProj) ← projInfo e.getAppFn
+    let .const c .. := e.getAppFn | failure
+    let (_, numParams, isParentProj) ← projInfo c
     return isParentProj && (!explicit || numParams == 0) && e.getAppNumArgs == numParams + 1
   catch _ =>
     return false
diff --git a/src/Lean/PrettyPrinter/Delaborator/Options.lean b/src/Lean/PrettyPrinter/Delaborator/Options.lean
index c2cad3bc8b79..e1f88913c844 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Options.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Options.lean
@@ -96,7 +96,7 @@ register_builtin_option pp.fieldNotation : Bool := {
   descr    := "(pretty printer) use field notation when pretty printing, including for structure projections, unless '@[pp_nodot]' is applied"
 }
 register_builtin_option pp.fieldNotation.generalized : Bool := {
-  defValue := false -- TODO(kmill): set to true
+  defValue := true
   group    := "pp"
   descr    := "(pretty printer) when `pp.fieldNotation` is true, enable using generalized field notation when the argument for field notation is the first explicit argument"
 }
diff --git a/tests/lean/1113.lean.expected.out b/tests/lean/1113.lean.expected.out
index e671dcded20a..f530369541ed 100644
--- a/tests/lean/1113.lean.expected.out
+++ b/tests/lean/1113.lean.expected.out
@@ -1,3 +1,3 @@
 n : Nat
-f : Fin (Nat.succ n)
+f : Fin n.succ
 ⊢ foo f = 0
diff --git a/tests/lean/1279.lean.expected.out b/tests/lean/1279.lean.expected.out
index ee35d544e635..204174ebf313 100644
--- a/tests/lean/1279.lean.expected.out
+++ b/tests/lean/1279.lean.expected.out
@@ -3,6 +3,6 @@ fun {α β γ} x x_1 =>
   match β, γ, x, x_1 with
   | β, .(β), Arrow.id, g => g
   | .(α), γ, f, Arrow.id => f
-  | β, γ, Arrow.comp f₁ f₂, g => Arrow.comp f₁ (Arrow.comp f₂ g)
-  | β, γ, f, g => Arrow.comp f g
+  | β, γ, f₁.comp f₂, g => f₁.comp (f₂.comp g)
+  | β, γ, f, g => f.comp g
 Arrow.unit
diff --git a/tests/lean/1616.lean.expected.out b/tests/lean/1616.lean.expected.out
index 0d1b7beca86d..9a4cf95a4402 100644
--- a/tests/lean/1616.lean.expected.out
+++ b/tests/lean/1616.lean.expected.out
@@ -1,5 +1,5 @@
 1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
+  @Linear ?m ?m (?m :: ?m) (?m :: ?m) c.right
 context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
@@ -14,12 +14,12 @@ context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
 1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
-  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
+  @Linear ?m (?m :: ?m) ?m (?m :: ?m) c.left
 context:
 c : Cover ?m ?m ?m
 ⊢ List ?m
 1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
+  @Linear ?m ?m (?m :: ?m) (?m :: ?m) c.right
 context:
 c : Cover ?m ?m ?m
 ⊢ List ?m
@@ -34,17 +34,17 @@ context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
 1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
-  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
+  @Linear ?m (?m :: ?m) ?m (?m :: ?m) c.left
 context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
 1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
+  @Linear ?m ?m (?m :: ?m) (?m :: ?m) c.right
 context:
 c : Cover ?m ?m ?m
 ⊢ List ?m
 1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
-  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
+  @Linear ?m (?m :: ?m) ?m (?m :: ?m) c.left
 context:
 c : Cover ?m ?m ?m
 ⊢ List ?m
diff --git a/tests/lean/1763.lean.expected.out b/tests/lean/1763.lean.expected.out
index b8c481d253f0..db72785c74f9 100644
--- a/tests/lean/1763.lean.expected.out
+++ b/tests/lean/1763.lean.expected.out
@@ -1,4 +1,4 @@
 theorem ex1 : ∀ {p q : Prop}, (p ↔ q) → P q → P p :=
-fun {p q} h h' => Eq.mpr (id (propext (P_congr p q h))) h'
+fun {p q} h h' => (id (propext (P_congr p q h))).mpr h'
 theorem ex2 : ∀ {p q : Prop}, p = q → P q → P p :=
-fun {p q} h h' => Eq.mpr (id (propext (P_congr p q (Iff.of_eq h)))) h'
+fun {p q} h h' => (id (propext (P_congr p q (Iff.of_eq h)))).mpr h'
diff --git a/tests/lean/2161.lean.expected.out b/tests/lean/2161.lean.expected.out
index 0e86d584b12f..17b2696749c1 100644
--- a/tests/lean/2161.lean.expected.out
+++ b/tests/lean/2161.lean.expected.out
@@ -1,12 +1,12 @@
 2161.lean:15:48-15:54: error: tactic 'decide' failed for proposition
-  mul (mul (mul 4 1) 1) 1 = 4
+  ((mul 4 1).mul 1).mul 1 = 4
 since its 'Decidable' instance reduced to
   Decidable.rec (fun h => (fun h => isFalse ⋯) h) (fun h => (fun h => h ▸ isTrue ⋯) h)
-    (instDecidableEqNat (mul (mul (mul 4 1) 1) 1).num 4)
+    (instDecidableEqNat (((mul 4 1).mul 1).mul 1).num 4)
 rather than to the 'isTrue' constructor.
 2161.lean:22:48-22:54: error: tactic 'decide' failed for proposition
-  add (add (add 4 1) 1) 1 = 4
+  ((add 4 1).add 1).add 1 = 4
 since its 'Decidable' instance reduced to
   Decidable.rec (fun h => (fun h => isFalse ⋯) h) (fun h => (fun h => h ▸ isTrue ⋯) h)
-    (instDecidableEqNat (add (add (add 4 1) 1) 1).num 4)
+    (instDecidableEqNat (((add 4 1).add 1).add 1).num 4)
 rather than to the 'isTrue' constructor.
diff --git a/tests/lean/415.lean.expected.out b/tests/lean/415.lean.expected.out
index dd657ca7fb78..acaa51bd6490 100644
--- a/tests/lean/415.lean.expected.out
+++ b/tests/lean/415.lean.expected.out
@@ -1,4 +1,4 @@
-Set.insert (Set.insert (Set.insert Set.empty 1) 2) 3 : Set Nat
+((Set.empty.insert 1).insert 2).insert 3 : Set Nat
 fun x y => g { x := x, y := y } : Nat → Nat → Nat
-fun x y => Set.insert (Set.insert Set.empty x) y : Nat → Nat → Set Nat
+fun x y => (Set.empty.insert x).insert y : Nat → Nat → Set Nat
 fun x y => { x := x, y := y } : Nat → Nat → Point
diff --git a/tests/lean/445.lean.expected.out b/tests/lean/445.lean.expected.out
index 352b58aaafc4..816015d5d61d 100644
--- a/tests/lean/445.lean.expected.out
+++ b/tests/lean/445.lean.expected.out
@@ -1,7 +1,7 @@
 true
 (match i with
   | 0 => true
-  | Nat.succ n => true) &&
+  | n.succ => true) &&
   f i
 if i < 5 then 0 else 1
 if i < 5 then 0 else g i j
diff --git a/tests/lean/449.lean.expected.out b/tests/lean/449.lean.expected.out
index a8d95e3d171f..c4202937f367 100644
--- a/tests/lean/449.lean.expected.out
+++ b/tests/lean/449.lean.expected.out
@@ -2,7 +2,7 @@
 context:
 m n : Nat
 ih : m * n = n * m
-⊢ m * n + m = m * n + succ zero * m
+⊢ m * n + m = m * n + zero.succ * m
 449.lean:13:19-13:20: error: don't know how to synthesize placeholder
 context:
 x y : Prop
diff --git a/tests/lean/474.lean.expected.out b/tests/lean/474.lean.expected.out
index bf8a88bbf79c..b29a7dccf6b2 100644
--- a/tests/lean/474.lean.expected.out
+++ b/tests/lean/474.lean.expected.out
@@ -1,8 +1,8 @@
 let y := Nat.zero;
-Nat.add y y
-fun y_1 => Nat.add y y_1
+y.add y
+fun y_1 => y.add y_1
 fun y => Nat.add _fvar.1 y
 fun (y : Nat) => Nat.add y y
-Nat.add ?m y
+?m.add y
 Nat.add (?m #0) #0
-fun y => Nat.add (Nat.add y y) y
+fun y => (y.add y).add y
diff --git a/tests/lean/550.lean.expected.out b/tests/lean/550.lean.expected.out
index 1cec88d6f11b..cbf447914b74 100644
--- a/tests/lean/550.lean.expected.out
+++ b/tests/lean/550.lean.expected.out
@@ -1,4 +1,4 @@
 550.lean:3:2-3:6: error: unsolved goals
 x : Nat
-h : ∀ (x : Nat), x + 1 = Nat.succ x
-⊢ Nat.succ (x + 1) = 1 + (x + 1)
+h : ∀ (x : Nat), x + 1 = x.succ
+⊢ (x + 1).succ = 1 + (x + 1)
diff --git a/tests/lean/690.lean.expected.out b/tests/lean/690.lean.expected.out
index 96436742c8c4..e0cde260b0eb 100644
--- a/tests/lean/690.lean.expected.out
+++ b/tests/lean/690.lean.expected.out
@@ -2,12 +2,12 @@
 690.lean:6:0-6:7: warning: declaration uses 'sorry'
 case step
 a b m✝ : Nat
-hStep : Nat.le a m✝
-ih : Nat.le a (m✝ + 1)
-⊢ Nat.le a (Nat.succ m✝ + 1)
+hStep : a.le m✝
+ih : a.le (m✝ + 1)
+⊢ a.le (m✝.succ + 1)
 690.lean:11:0-11:7: warning: declaration uses 'sorry'
 case step
 a b x : Nat
-hStep : Nat.le a x
-ih : Nat.le a (x + 1)
-⊢ Nat.le a (Nat.succ x + 1)
+hStep : a.le x
+ih : a.le (x + 1)
+⊢ a.le (x.succ + 1)
diff --git a/tests/lean/arrayGetU.lean.expected.out b/tests/lean/arrayGetU.lean.expected.out
index c24c94975e50..10b4ade166d9 100644
--- a/tests/lean/arrayGetU.lean.expected.out
+++ b/tests/lean/arrayGetU.lean.expected.out
@@ -1,14 +1,14 @@
 i j : Nat
 a : Array Nat
 v : Nat
-h₁ : i < Array.size a
-h₂ : j < Array.size a
+h₁ : i < a.size
+h₂ : j < a.size
 h₃ : i = j
 ⊢ f a i v h₁ = f a j v h₂
 i j : Nat
 a : Array Nat
 v : Nat
-h₁ : 0 + i < Array.size a
-h₂ : j < Array.size a
+h₁ : 0 + i < a.size
+h₂ : j < a.size
 h₃ : i = j
-⊢ f a i v (Nat.zero_add i ▸ h₁) = f a j v h₂
+⊢ f a i v (i.zero_add ▸ h₁) = f a j v h₂
diff --git a/tests/lean/autoImplicitChainNameIssue.lean.expected.out b/tests/lean/autoImplicitChainNameIssue.lean.expected.out
index e6b966055a99..749246019cfd 100644
--- a/tests/lean/autoImplicitChainNameIssue.lean.expected.out
+++ b/tests/lean/autoImplicitChainNameIssue.lean.expected.out
@@ -2,5 +2,5 @@ autoImplicitChainNameIssue.lean:8:11-8:15: error: unsolved goals
 case nil
 α✝ : Type u_1
 as : List α✝
-⊢ Palindrome (List.reverse [])
-palindrome_reverse.{u_1} : ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome (List.reverse as)
+⊢ Palindrome [].reverse
+palindrome_reverse.{u_1} : ∀ {α : Type u_1} {as : List α}, Palindrome as → Palindrome as.reverse
diff --git a/tests/lean/badIhName.lean.expected.out b/tests/lean/badIhName.lean.expected.out
index e613afbf2861..06651d732e1b 100644
--- a/tests/lean/badIhName.lean.expected.out
+++ b/tests/lean/badIhName.lean.expected.out
@@ -5,4 +5,4 @@ case z
 case s
 a✝ : Nat
 a_ih✝ : add Nat.z a✝ = a✝
-⊢ add Nat.z (Nat.s a✝) = Nat.s a✝
+⊢ add Nat.z a✝.s = a✝.s
diff --git a/tests/lean/congrThmIssue.lean.expected.out b/tests/lean/congrThmIssue.lean.expected.out
index 4233da007e03..6ebe5a63472a 100644
--- a/tests/lean/congrThmIssue.lean.expected.out
+++ b/tests/lean/congrThmIssue.lean.expected.out
@@ -4,7 +4,7 @@ cap : Nat
 backing : Fin cap → Option α
 size : Nat
 h_size : size ≤ cap
-h_full : ∀ (i : Nat) (h : i < size), Option.isSome (backing ⟨i, ⋯⟩) = true
+h_full : ∀ (i : Nat) (h : i < size), (backing ⟨i, ⋯⟩).isSome = true
 i : Nat
 h : i < size
-⊢ Option.isSome (if h_1 : i < cap then backing ⟨i, ⋯⟩ else none) = true
+⊢ (if h_1 : i < cap then backing ⟨i, ⋯⟩ else none).isSome = true
diff --git a/tests/lean/conv1.lean.expected.out b/tests/lean/conv1.lean.expected.out
index 55787c781bd1..0044021de23f 100644
--- a/tests/lean/conv1.lean.expected.out
+++ b/tests/lean/conv1.lean.expected.out
@@ -5,10 +5,10 @@ x y : Nat
 x y : Nat
 | x + y = y + x + 0
 x y : Nat
-⊢ x + y = Nat.add y x
+⊢ x + y = y.add x
 case x
 x y : Nat
-⊢ x + y = Nat.add y x
+⊢ x + y = y.add x
 case a
 a b : Nat
 | foo (0 + a) (b + 0)
@@ -48,11 +48,11 @@ case y
 a b : Nat
 | b
 x y : Nat
-⊢ x + y = Nat.add y x
+⊢ x + y = y.add x
 x y : Nat
-⊢ Nat.add x y = Nat.add y x
+⊢ x.add y = y.add x
 x y : Nat
-⊢ f x (Nat.add x y) y = y + x
+⊢ f x (x.add y) y = y + x
 x y : Nat
 | x + y
 case h.h
diff --git a/tests/lean/diamond9.lean.expected.out b/tests/lean/diamond9.lean.expected.out
index ddcb476501e1..cf2bfcd0b34e 100644
--- a/tests/lean/diamond9.lean.expected.out
+++ b/tests/lean/diamond9.lean.expected.out
@@ -1,2 +1,2 @@
 constructor Ring.mk.{u} : {R : Type u} → [toZero : Zero R] → (gsmul : Int → R → R) → (∀ (a : R), gsmul 0 a = 0) → Ring R
-Ring.mk (fun x n => Int.toNat x * n) ⋯ : Ring Nat
+Ring.mk (fun x n => x.toNat * n) ⋯ : Ring Nat
diff --git a/tests/lean/doIssue.lean.expected.out b/tests/lean/doIssue.lean.expected.out
index b7963f5738de..6f54835edb3d 100644
--- a/tests/lean/doIssue.lean.expected.out
+++ b/tests/lean/doIssue.lean.expected.out
@@ -5,15 +5,15 @@ has type
 but is expected to have type
   IO PUnit : Type
 doIssue.lean:10:2-10:13: error: type mismatch
-  Array.set! xs 0 1
+  xs.set! 0 1
 has type
   Array Nat : Type
 but is expected to have type
   IO PUnit : Type
 doIssue.lean:18:7-18:20: error: application type mismatch
-  pure (Array.set! xs 0 1)
+  pure (xs.set! 0 1)
 argument
-  Array.set! xs 0 1
+  xs.set! 0 1
 has type
   Array Nat : Type
 but is expected to have type
diff --git a/tests/lean/eta.lean.expected.out b/tests/lean/eta.lean.expected.out
index f15feb9a36fa..2236df45fd65 100644
--- a/tests/lean/eta.lean.expected.out
+++ b/tests/lean/eta.lean.expected.out
@@ -1,5 +1,5 @@
 [Meta.debug] >> fun x => Nat.add
 [Meta.debug] >> Nat.add
 [Meta.debug] >> HAdd.hAdd 1
-[Meta.debug] >> fun x y z => Nat.add z y
-[Meta.debug] >> fun y => Nat.add y y
+[Meta.debug] >> fun x y z => z.add y
+[Meta.debug] >> fun y => y.add y
diff --git a/tests/lean/etaStructIssue.lean.expected.out b/tests/lean/etaStructIssue.lean.expected.out
index f475f3c0651f..111dd2af8d43 100644
--- a/tests/lean/etaStructIssue.lean.expected.out
+++ b/tests/lean/etaStructIssue.lean.expected.out
@@ -3,4 +3,4 @@ etaStructIssue.lean:20:2-20:5: error: type mismatch
 has type
   mkNat e x₁ = mkNat e x₁ : Prop
 but is expected to have type
-  mkNat e x₁ = mkNat (E.mk e) x₂ : Prop
+  mkNat e x₁ = mkNat e.mk x₂ : Prop
diff --git a/tests/lean/evalWithMVar.lean.expected.out b/tests/lean/evalWithMVar.lean.expected.out
index 388f412569c7..ae1de9e9e5fa 100644
--- a/tests/lean/evalWithMVar.lean.expected.out
+++ b/tests/lean/evalWithMVar.lean.expected.out
@@ -1,4 +1,4 @@
-Sum.someRight c : Option Nat
+c.someRight : Option Nat
 evalWithMVar.lean:13:6-13:21: error: don't know how to synthesize implicit argument
   @Sum.someRight ?m Nat c
 context:
@@ -7,5 +7,5 @@ evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argu
   @c ?m
 context:
 ⊢ Type ?u
-Sum.someRight c : Option Nat
-Sum.someRight c : Option Nat
+c.someRight : Option Nat
+c.someRight : Option Nat
diff --git a/tests/lean/fixedIndexToParamIssue.lean.expected.out b/tests/lean/fixedIndexToParamIssue.lean.expected.out
index d44a29889d24..32157549ef7e 100644
--- a/tests/lean/fixedIndexToParamIssue.lean.expected.out
+++ b/tests/lean/fixedIndexToParamIssue.lean.expected.out
@@ -4,4 +4,4 @@ constructors:
 BST.leaf : ∀ {β : Type u_1}, BST Tree.leaf
 BST.node : ∀ {β : Type u_1} {key : Nat} {left right : Tree β} {value : β},
   ForallTree (fun k v => k < key) left →
-    ForallTree (fun k v => key < k) right → BST left → BST right → BST (Tree.node left key value right)
+    ForallTree (fun k v => key < k) right → BST left → BST right → BST (left.node key value right)
diff --git a/tests/lean/getElem.lean.expected.out b/tests/lean/getElem.lean.expected.out
index 62279417b9cc..ec12477464b6 100644
--- a/tests/lean/getElem.lean.expected.out
+++ b/tests/lean/getElem.lean.expected.out
@@ -5,10 +5,10 @@ getElem.lean:2:2-2:6: error: failed to prove index is valid, possible solutions:
   - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
 a : Array Nat
 i : Nat
-⊢ i < Array.size a
-def f2 : (a : Array Nat) → Fin (Array.size a) → Nat :=
+⊢ i < a.size
+def f2 : (a : Array Nat) → Fin a.size → Nat :=
 fun a i => a[i]
-def f3 : {n : Nat} → (a : Array Nat) → n ≤ Array.size a → Fin n → Nat :=
+def f3 : {n : Nat} → (a : Array Nat) → n ≤ a.size → Fin n → Nat :=
 fun {n} a h i => a[i]
 def f5 : (i : Nat) → i < n → Nat :=
 fun i h => a[i]
diff --git a/tests/lean/guessLexDiff.lean.expected.out b/tests/lean/guessLexDiff.lean.expected.out
index fea34871a136..80d7e694e57e 100644
--- a/tests/lean/guessLexDiff.lean.expected.out
+++ b/tests/lean/guessLexDiff.lean.expected.out
@@ -1,15 +1,15 @@
 Inferred termination argument:
 termination_by n - i
 Inferred termination argument:
-termination_by Array.size xs - i
+termination_by xs.size - i
 Inferred termination argument:
-termination_by Array.size xs - i
+termination_by xs.size - i
 Inferred termination argument:
-termination_by (Array.size xs - i, Array.size ys - j)
+termination_by (xs.size - i, ys.size - j)
 Inferred termination argument:
-termination_by (Array.size xs - i, i - j)
+termination_by (xs.size - i, i - j)
 Inferred termination argument:
-termination_by (Array.size xs - i, i)
+termination_by (xs.size - i, i)
 guessLexDiff.lean:85:26-85:38: error: fail to show termination for
   failure
 with errors
@@ -33,8 +33,8 @@ The arguments relate at each recursive call as follows:
 8) 88:26-42 _  <  _     _
 9) 97:8-20  _  <  _     _
 
-#1: Array.size xs - i
-#2: Array.size xs - (i + 1)
+#1: xs.size - i
+#2: xs.size - (i + 1)
 
 Please use `termination_by` to specify a decreasing measure.
 guessLexDiff.lean:102:4-102:18: error: fail to show termination for
@@ -88,8 +88,8 @@ i  _  _
 #2 _  _
 
 
-#1: Array.size xs - i
-#2: Array.size xs - (i + 1)
-#3: Array.size xs - i
+#1: xs.size - i
+#2: xs.size - (i + 1)
+#3: xs.size - i
 
 Please use `termination_by` to specify a decreasing measure.
diff --git a/tests/lean/guessLexFailures.lean.expected.out b/tests/lean/guessLexFailures.lean.expected.out
index 8aa7ad0dd4a0..6ee1293d4357 100644
--- a/tests/lean/guessLexFailures.lean.expected.out
+++ b/tests/lean/guessLexFailures.lean.expected.out
@@ -3,11 +3,11 @@ guessLexFailures.lean:11:12-11:46: error: fail to show termination for
 with errors
 argument #1 was not used for structural recursion
   failed to eliminate recursive application
-    nonTerminating (Nat.succ n) (Nat.succ m)
+    nonTerminating n.succ m.succ
 
 argument #2 was not used for structural recursion
   failed to eliminate recursive application
-    nonTerminating (Nat.succ n) (Nat.succ m)
+    nonTerminating n.succ m.succ
 
 structural recursion cannot be used
 
diff --git a/tests/lean/inductionErrors.lean.expected.out b/tests/lean/inductionErrors.lean.expected.out
index 5e7fb7096817..e6e762991e1e 100644
--- a/tests/lean/inductionErrors.lean.expected.out
+++ b/tests/lean/inductionErrors.lean.expected.out
@@ -1,11 +1,11 @@
 inductionErrors.lean:11:12-11:27: error: unsolved goals
 case lower.h
 p d : Nat
-⊢ p ≤ p + Nat.succ d
+⊢ p ≤ p + d.succ
 inductionErrors.lean:12:12-12:27: error: unsolved goals
 case upper.h
 q d : Nat
-⊢ q + Nat.succ d > q
+⊢ q + d.succ > q
 inductionErrors.lean:16:19-16:26: error: unknown identifier 'elimEx2'
 inductionErrors.lean:22:2-25:45: error: insufficient number of targets for 'elimEx'
 inductionErrors.lean:28:16-28:23: error: unexpected eliminator resulting type
diff --git a/tests/lean/inductionGen.lean.expected.out b/tests/lean/inductionGen.lean.expected.out
index eb5894e71b63..6c28bbba2193 100644
--- a/tests/lean/inductionGen.lean.expected.out
+++ b/tests/lean/inductionGen.lean.expected.out
@@ -8,7 +8,7 @@ ys : Vec α (n + 1)
 x : α
 xs : Vec α n
 h : Vec.cons x xs = ys
-⊢ Vec.head (Vec.cons x xs) = Vec.head ys
+⊢ (Vec.cons x xs).head = ys.head
 inductionGen.lean:64:8-64:11: warning: declaration uses 'sorry'
 case natVal
 α : ExprType
@@ -30,8 +30,8 @@ a✝¹ a✝ : Expr α✝
 a_ih✝¹ : ∀ (b : Expr α✝), a✝¹ = b → eval (constProp a✝¹) = eval b
 a_ih✝ : ∀ (b : Expr α✝), a✝ = b → eval (constProp a✝) = eval b
 b : Expr ExprType.bool
-h : Expr.eq a✝¹ a✝ = b
-⊢ eval (constProp (Expr.eq a✝¹ a✝)) = eval b
+h : a✝¹.eq a✝ = b
+⊢ eval (constProp (a✝¹.eq a✝)) = eval b
 
 case add
 α : ExprType
@@ -39,7 +39,7 @@ a✝¹ a✝ : Expr ExprType.nat
 a_ih✝¹ : ∀ (b : Expr ExprType.nat), a✝¹ = b → eval (constProp a✝¹) = eval b
 a_ih✝ : ∀ (b : Expr ExprType.nat), a✝ = b → eval (constProp a✝) = eval b
 b : Expr ExprType.nat
-h : Expr.add a✝¹ a✝ = b
-⊢ eval (constProp (Expr.add a✝¹ a✝)) = eval b
+h : a✝¹.add a✝ = b
+⊢ eval (constProp (a✝¹.add a✝)) = eval b
 inductionGen.lean:78:2-78:27: error: target (or one of its indices) occurs more than once
   n
diff --git a/tests/lean/invalidPatternIssue.lean.expected.out b/tests/lean/invalidPatternIssue.lean.expected.out
index 7132eb92e271..4b49f88fc200 100644
--- a/tests/lean/invalidPatternIssue.lean.expected.out
+++ b/tests/lean/invalidPatternIssue.lean.expected.out
@@ -1,2 +1,2 @@
 invalidPatternIssue.lean:13:0-13:20: error: invalid patterns, `x` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
-  { pred := Nat.succ .(x.1) }
+  { pred := .(x.1).succ }
diff --git a/tests/lean/issue2981.lean.expected.out b/tests/lean/issue2981.lean.expected.out
index 8b4e6c591169..14d97db29882 100644
--- a/tests/lean/issue2981.lean.expected.out
+++ b/tests/lean/issue2981.lean.expected.out
@@ -3,9 +3,9 @@ Tactic is run (ideally only twice)
 Tactic is run (ideally only twice)
 Tactic is run (ideally only once, in most general context)
 n : Nat
-⊢ (invImage (fun x => x) instWellFoundedRelation).1 n (Nat.succ n)
+⊢ (invImage (fun x => x) instWellFoundedRelation).1 n n.succ
 Tactic is run (ideally only twice, in most general context)
 Tactic is run (ideally only twice, in most general context)
 n : Nat
-⊢ sizeOf n < sizeOf (Nat.succ n)
-n m : Nat ⊢ (invImage (fun x => PSigma.casesOn x fun a a_1 => a) instWellFoundedRelation).1 ⟨n, m + 1⟩ ⟨Nat.succ n, m⟩
+⊢ sizeOf n < sizeOf n.succ
+n m : Nat ⊢ (invImage (fun x => PSigma.casesOn x fun a a_1 => a) instWellFoundedRelation).1 ⟨n, m + 1⟩ ⟨n.succ, m⟩
diff --git a/tests/lean/letFun.lean.expected.out b/tests/lean/letFun.lean.expected.out
index 04855d77fe15..45b30806e3ee 100644
--- a/tests/lean/letFun.lean.expected.out
+++ b/tests/lean/letFun.lean.expected.out
@@ -15,7 +15,7 @@ a b : Nat
 h : a > b
 ⊢ b < a
 let_fun n := 5;
-⟨[], ⋯⟩ : { as // List.length as ≤ 5 }
+⟨[], ⋯⟩ : { as // as.length ≤ 5 }
 rfl : (let_fun n := 5;
   n) =
   let_fun n := 5;
diff --git a/tests/lean/librarySearch.lean b/tests/lean/librarySearch.lean
index 0f55bc906b64..6d5fe2c3225e 100644
--- a/tests/lean/librarySearch.lean
+++ b/tests/lean/librarySearch.lean
@@ -27,7 +27,7 @@ example : 0 ≠ 1 + 1 := Nat.ne_of_lt (by apply?)
 
 example : 0 ≠ 1 + 1 := Nat.ne_of_lt (by exact Fin.size_pos')
 
-/-- info: Try this: exact Nat.add_comm x y -/
+/-- info: Try this: exact x.add_comm y -/
 #guard_msgs in
 example (x y : Nat) : x + y = y + x := by apply?
 
@@ -37,7 +37,7 @@ example (n m k : Nat) : n ≤ m → n + k ≤ m + k := by apply?
 
 /-- info: Try this: exact Nat.mul_dvd_mul_left a w -/
 #guard_msgs in
-example (ha : a > 0) (w : b ∣ c) : a * b ∣ a * c := by apply?
+example (_ha : a > 0) (w : b ∣ c) : a * b ∣ a * c := by apply?
 
 /-- info: Try this: Nat.lt.base x -/
 #guard_msgs in
@@ -46,7 +46,7 @@ example : x < x + 1 := exact?%
 /-- info: Try this: exact p -/
 #guard_msgs in
 example (P : Prop) (p : P) : P := by apply?
-/-- info: Try this: exact False.elim (np p) -/
+/-- info: Try this: exact (np p).elim -/
 #guard_msgs in
 example (P : Prop) (p : P) (np : ¬P) : false := by apply?
 /-- info: Try this: exact h x rfl -/
@@ -62,19 +62,19 @@ example (α : Prop) : α → α := by apply?
 -- example (a b : Prop) (h : a ∧ b) : a := by apply? -- says: `exact h.left`
 -- example (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) := by apply? -- say: `exact Function.mtr`
 
-/-- info: Try this: exact Nat.add_comm a b -/
+/-- info: Try this: exact a.add_comm b -/
 #guard_msgs in
 example (a b : Nat) : a + b = b + a :=
 by apply?
 
-/-- info: Try this: exact Nat.mul_sub_left_distrib n m k -/
+/-- info: Try this: exact n.mul_sub_left_distrib m k -/
 #guard_msgs in
 example (n m k : Nat) : n * (m - k) = n * m - n * k :=
 by apply?
 
 attribute [symm] Eq.symm
 
-/-- info: Try this: exact Eq.symm (Nat.mul_sub_left_distrib n m k) -/
+/-- info: Try this: exact (n.mul_sub_left_distrib m k).symm -/
 #guard_msgs in
 example (n m k : Nat) : n * m - n * k = n * (m - k) := by
   apply?
@@ -109,10 +109,10 @@ by apply?
 example (a b : Nat) (h : a ∣ b) (w : b > 0) : b ≥ a := by apply?
 
 -- TODO: A lemma with head symbol `¬` can be used to prove `¬ p` or `⊥`
-/-- info: Try this: exact Nat.not_lt_zero a -/
+/-- info: Try this: exact a.not_lt_zero -/
 #guard_msgs in
 example (a : Nat) : ¬ (a < 0) := by apply?
-/-- info: Try this: exact Nat.not_succ_le_zero a h -/
+/-- info: Try this: exact a.not_succ_le_zero h -/
 #guard_msgs in
 example (a : Nat) (h : a < 0) : False := by apply?
 
@@ -165,7 +165,7 @@ axiom F (a b : Nat) : f a ≤ f b ↔ a ≤ b
 #guard_msgs in
 example (a b : Nat) (h : a ≤ b) : f a ≤ f b := by apply?
 
-/-- info: Try this: exact List.join L -/
+/-- info: Try this: exact L.join -/
 #guard_msgs in
 example (L : List (List Nat)) : List Nat := by apply? using L
 
@@ -239,7 +239,7 @@ example {x : Int} (h : x ≠ 0) : 2 * x ≠ 0 := by
 
 -- Check that adding `with_reducible` prevents expensive kernel reductions.
 -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60exact.3F.60.20failure.3A.20.22maximum.20recursion.20depth.20has.20been.20reached.22/near/417649319
-/-- info: Try this: exact Nat.add_comm n m -/
+/-- info: Try this: exact n.add_comm m -/
 #guard_msgs in
 example (_h : List.range 10000 = List.range 10000) (n m : Nat) : n + m = m + n := by
   with_reducible exact?
diff --git a/tests/lean/macroSwizzle.lean.expected.out b/tests/lean/macroSwizzle.lean.expected.out
index d45ec0f9ccbc..3ee7f64c0770 100644
--- a/tests/lean/macroSwizzle.lean.expected.out
+++ b/tests/lean/macroSwizzle.lean.expected.out
@@ -8,4 +8,4 @@ has type
   String : Type
 but is expected to have type
   Nat : Type
-Nat.succ (sorryAx Nat true) : Nat
+(sorryAx Nat true).succ : Nat
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
index 7e2fbddbb467..d816cd23c041 100644
--- a/tests/lean/match1.lean.expected.out
+++ b/tests/lean/match1.lean.expected.out
@@ -38,7 +38,7 @@ fun x x_1 =>
 fun x =>
   (match (motive := Nat → Nat → Nat) x with
     | 0 => id
-    | Nat.succ x => id)
+    | x.succ => id)
     x : Nat → Nat
 fun x =>
   match x with
diff --git a/tests/lean/mutwf1.lean.expected.out b/tests/lean/mutwf1.lean.expected.out
index e0f562e89e25..7ac3508cd80b 100644
--- a/tests/lean/mutwf1.lean.expected.out
+++ b/tests/lean/mutwf1.lean.expected.out
@@ -2,7 +2,7 @@ mutwf1.lean:23:2-23:6: error: unsolved goals
 case h.a
 n : Nat
 h : n ≠ 0
-⊢ Nat.sub n 0 ≠ 0
+⊢ n.sub 0 ≠ 0
 mutwf1.lean:33:22-33:29: error: failed to prove termination, possible solutions:
   - Use `have`-expressions to prove the remaining goals
   - Use `termination_by` to specify a different well-founded relation
diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out
index 201a304788b9..85727ca7ce44 100644
--- a/tests/lean/phashmap_inst_coherence.lean.expected.out
+++ b/tests/lean/phashmap_inst_coherence.lean.expected.out
@@ -1,5 +1,5 @@
 phashmap_inst_coherence.lean:12:53-12:54: error: application type mismatch
-  PersistentHashMap.find? m
+  m.find?
 argument
   m
 has type
diff --git a/tests/lean/ppDeepTerms.lean.expected.out b/tests/lean/ppDeepTerms.lean.expected.out
index a4072a73785e..3bc3c796bfec 100644
--- a/tests/lean/ppDeepTerms.lean.expected.out
+++ b/tests/lean/ppDeepTerms.lean.expected.out
@@ -1,7 +1,6 @@
-Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))))) : Nat
-Nat.succ
-  (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ Nat.zero))))))))) : Nat
-Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ (Nat.succ ⋯)))))))) : Nat
+Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ : Nat
+Nat.zero.succ.succ.succ.succ.succ.succ.succ.succ.succ.succ : Nat
+⋯.succ.succ.succ.succ.succ.succ.succ.succ.succ : Nat
 [1, 2, 3, 4, 5, 6, 7, 8] : List Nat
 [1, 2, 3, 4, 5, 6, 7, 8, ⋯] : List Nat
 ppDeepTerms.lean:39:32-39:33: warning: The '⋯' token is used by the pretty printer to indicate omitted terms, and it should not be used directly. It logs this warning and then elaborates like `_`.
diff --git a/tests/lean/ppMotives.lean.expected.out b/tests/lean/ppMotives.lean.expected.out
index e345ca95d216..6b465d023ce7 100644
--- a/tests/lean/ppMotives.lean.expected.out
+++ b/tests/lean/ppMotives.lean.expected.out
@@ -4,7 +4,7 @@ fun x x_1 =>
     (fun x f x_2 =>
       (match x_2, x with
         | a, Nat.zero => fun x => a
-        | a, Nat.succ b => fun x => Nat.succ (x.fst.fst a))
+        | a, b.succ => fun x => (x.fst.fst a).succ)
         f)
     x
 protected def Nat.add : Nat → Nat → Nat :=
@@ -13,7 +13,7 @@ fun x x_1 =>
     (fun x f x_2 =>
       (match (motive := Nat → (x : Nat) → Nat.below (motive := fun x => Nat → Nat) x → Nat) x_2, x with
         | a, Nat.zero => fun x => a
-        | a, Nat.succ b => fun x => Nat.succ (x.fst.fst a))
+        | a, b.succ => fun x => (x.fst.fst a).succ)
         f)
     x
 theorem ex.{u} : ∀ {α β : Sort u} (h : α = β) (a : α), HEq (cast h a) a :=
diff --git a/tests/lean/ppNotationCode.lean.expected.out b/tests/lean/ppNotationCode.lean.expected.out
index 423aca37319c..dea9d5ca09e2 100644
--- a/tests/lean/ppNotationCode.lean.expected.out
+++ b/tests/lean/ppNotationCode.lean.expected.out
@@ -4,10 +4,10 @@
 [Elab.definition.body] «_aux_ppNotationCode___macroRules_term_+++__1» : Lean.Macro :=
     fun x =>
       let_fun __discr := x;
-      if Lean.Syntax.isOfKind __discr `term_+++_ = true then
-        let_fun __discr_1 := Lean.Syntax.getArg __discr 0;
-        let_fun __discr_2 := Lean.Syntax.getArg __discr 1;
-        let_fun __discr := Lean.Syntax.getArg __discr 2;
+      if __discr.isOfKind `term_+++_ = true then
+        let_fun __discr_1 := __discr.getArg 0;
+        let_fun __discr_2 := __discr.getArg 1;
+        let_fun __discr := __discr.getArg 2;
         let_fun rhs := { raw := __discr };
         let_fun lhs := { raw := __discr_1 };
         do
@@ -18,7 +18,7 @@
             {
                 raw :=
                   Lean.Syntax.node2 info `Lean.Parser.Term.app
-                    (Lean.Syntax.ident info (String.toSubstring' "Nat.add") (Lean.addMacroScope mainModule `Nat.add scp)
+                    (Lean.Syntax.ident info "Nat.add".toSubstring' (Lean.addMacroScope mainModule `Nat.add scp)
                       [Lean.Syntax.Preresolved.decl `Nat.add [], Lean.Syntax.Preresolved.namespace `Nat.add])
                     (Lean.Syntax.node2 info `null lhs.raw rhs.raw) }.raw
       else
@@ -27,13 +27,13 @@
 [Elab.definition.body] _aux_ppNotationCode___unexpand_Nat_add_1 : Lean.PrettyPrinter.Unexpander :=
     fun x =>
       let_fun __discr := x;
-      if Lean.Syntax.isOfKind __discr `Lean.Parser.Term.app = true then
-        let_fun __discr_1 := Lean.Syntax.getArg __discr 0;
-        bif false || Lean.Syntax.isOfKind __discr_1 `ident then
-          let_fun __discr_2 := Lean.Syntax.getArg __discr 1;
-          if Lean.Syntax.matchesNull __discr_2 2 = true then
-            let_fun __discr := Lean.Syntax.getArg __discr_2 0;
-            let_fun __discr_3 := Lean.Syntax.getArg __discr_2 1;
+      if __discr.isOfKind `Lean.Parser.Term.app = true then
+        let_fun __discr_1 := __discr.getArg 0;
+        bif false || __discr_1.isOfKind `ident then
+          let_fun __discr_2 := __discr.getArg 1;
+          if __discr_2.matchesNull 2 = true then
+            let_fun __discr := __discr_2.getArg 0;
+            let_fun __discr_3 := __discr_2.getArg 1;
             let_fun rhs := { raw := __discr_3 };
             let_fun lhs := { raw := __discr };
             let_fun f := { raw := __discr_1 };
@@ -43,11 +43,11 @@
               let _ ← Lean.getMainModule
               pure { raw := Lean.Syntax.node3 info `term_+++_ lhs.raw (Lean.Syntax.atom info "+++") rhs.raw }.raw
           else
-            let_fun __discr := Lean.Syntax.getArg __discr 1;
+            let_fun __discr := __discr.getArg 1;
             throw ()
         else
-          let_fun __discr_2 := Lean.Syntax.getArg __discr 0;
-          let_fun __discr := Lean.Syntax.getArg __discr 1;
+          let_fun __discr_2 := __discr.getArg 0;
+          let_fun __discr := __discr.getArg 1;
           throw ()
       else
         let_fun __discr := x;
diff --git a/tests/lean/ppite.lean.expected.out b/tests/lean/ppite.lean.expected.out
index f13d214f0960..24ef7f853b0a 100644
--- a/tests/lean/ppite.lean.expected.out
+++ b/tests/lean/ppite.lean.expected.out
@@ -1,6 +1,6 @@
 def f : List Nat → IO Unit :=
 fun xs =>
-  List.forM xs fun x =>
+  xs.forM fun x =>
     if (x == 0) = true then do
       IO.println "foo"
       IO.println "zero"
diff --git a/tests/lean/rewrite.lean.expected.out b/tests/lean/rewrite.lean.expected.out
index 2fbe0d6f9e00..d848327ad72e 100644
--- a/tests/lean/rewrite.lean.expected.out
+++ b/tests/lean/rewrite.lean.expected.out
@@ -2,7 +2,7 @@
 as bs : List α
 ⊢ as ++ bs ++ bs = as ++ (bs ++ bs)
 rewrite.lean:18:20-18:29: error: tactic 'rewrite' failed, did not find instance of the pattern in the target expression
-  List.reverse (List.reverse ?as)
+  ?as.reverse.reverse
 α : Type u_1
 as bs : List α
 ⊢ as ++ [] ++ [] ++ bs ++ bs = as ++ (bs ++ bs)
diff --git a/tests/lean/run/1074a.lean b/tests/lean/run/1074a.lean
index 3e5e1c9d9e85..044d6c6c268f 100644
--- a/tests/lean/run/1074a.lean
+++ b/tests/lean/run/1074a.lean
@@ -19,10 +19,10 @@ def Brx.interp_nil (H: Brx a): H.interp = H.interp
   }
 
 /--
-info: Brx.interp.eq_1 (n z : Term) (H_2 : Brx (Term.id2 n z)) :
-  Brx.interp H_2 =
+info: Brx.interp.eq_1 (n z : Term) (H_2 : Brx (n.id2 z)) :
+  H_2.interp =
     match ⋯ with
-    | ⋯ => Brx.interp Hz
+    | ⋯ => Hz.interp
 -/
 #guard_msgs in
 #check Brx.interp.eq_1
diff --git a/tests/lean/run/974.lean b/tests/lean/run/974.lean
index 0077bac03a51..395d1918c23a 100644
--- a/tests/lean/run/974.lean
+++ b/tests/lean/run/974.lean
@@ -12,15 +12,14 @@ attribute [simp] Formula.count_quantifiers
 
 /--
 info: Formula.count_quantifiers.eq_1.{u_1} :
-  ∀ (x : Nat) (f₁ f₂ : Formula x),
-    Formula.count_quantifiers (Formula.imp f₁ f₂) = Formula.count_quantifiers f₁ + Formula.count_quantifiers f₂
+  ∀ (x : Nat) (f₁ f₂ : Formula x), (f₁.imp f₂).count_quantifiers = f₁.count_quantifiers + f₂.count_quantifiers
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_1
 
 /--
 info: Formula.count_quantifiers.eq_2.{u_1} :
-  ∀ (x : Nat) (f : Formula (x + 1)), Formula.count_quantifiers (Formula.all f) = Formula.count_quantifiers f + 1
+  ∀ (x : Nat) (f : Formula (x + 1)), f.all.count_quantifiers = f.count_quantifiers + 1
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_2
@@ -28,8 +27,8 @@ info: Formula.count_quantifiers.eq_2.{u_1} :
 /--
 info: Formula.count_quantifiers.eq_3.{u_1} :
   ∀ (x : Nat) (x_1 : Formula x),
-    (∀ (f₁ f₂ : Formula x), x_1 = Formula.imp f₁ f₂ → False) →
-      (∀ (f : Formula (x + 1)), x_1 = Formula.all f → False) → Formula.count_quantifiers x_1 = 0
+    (∀ (f₁ f₂ : Formula x), x_1 = f₁.imp f₂ → False) →
+      (∀ (f : Formula (x + 1)), x_1 = f.all → False) → x_1.count_quantifiers = 0
 -/
 #guard_msgs in
 #check Formula.count_quantifiers.eq_3
diff --git a/tests/lean/run/986.lean b/tests/lean/run/986.lean
index a04427305a2c..1f73a09aba6d 100644
--- a/tests/lean/run/986.lean
+++ b/tests/lean/run/986.lean
@@ -1,7 +1,7 @@
 attribute [simp] Array.insertionSort.swapLoop
 
 /--
-info: Array.insertionSort.swapLoop.eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (h : 0 < Array.size a) :
+info: Array.insertionSort.swapLoop.eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (h : 0 < a.size) :
   Array.insertionSort.swapLoop lt a 0 h = a
 -/
 #guard_msgs in
@@ -9,11 +9,10 @@ info: Array.insertionSort.swapLoop.eq_1.{u_1} {α : Type u_1} (lt : α → α 
 
 /--
 info: Array.insertionSort.swapLoop.eq_2.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j' : Nat)
-  (h : Nat.succ j' < Array.size a) :
-  Array.insertionSort.swapLoop lt a (Nat.succ j') h =
+  (h : j'.succ < a.size) :
+  Array.insertionSort.swapLoop lt a j'.succ h =
     let_fun h' := ⋯;
-    if lt a[Nat.succ j'] a[j'] = true then Array.insertionSort.swapLoop lt (Array.swap a ⟨Nat.succ j', h⟩ ⟨j', h'⟩) j' ⋯
-    else a
+    if lt a[j'.succ] a[j'] = true then Array.insertionSort.swapLoop lt (a.swap ⟨j'.succ, h⟩ ⟨j', h'⟩) j' ⋯ else a
 -/
 #guard_msgs in
 #check Array.insertionSort.swapLoop.eq_2
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index 0a67c77363c4..34294fa9cad1 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -81,7 +81,7 @@ set_option pp.proofs true
   expecting Nat.brecOn (motive := fun x => Nat → Nat) 0 (fun x ih y => y + x) 0
 
 #testDelab let xs := #[]; xs.push (5 : Nat)
-  expecting let xs : Array Nat := #[]; Array.push xs 5
+  expecting let xs : Array Nat := #[]; xs.push 5
 
 #testDelab let x := Nat.zero; x + Nat.zero
   expecting let x := Nat.zero; x + Nat.zero
@@ -293,7 +293,7 @@ structure SubtypeLike1 {α : Sort u} (p : α → Prop) where
 --Note: currently we do not try "bottom-upping" inside lambdas
 --(so we will always annotate the binder type)
 #testDelab SubtypeLike1 fun (x : Nat) => Nat.succ x = x
-  expecting SubtypeLike1 fun (x : Nat) => Nat.succ x = x
+  expecting SubtypeLike1 fun (x : Nat) => x.succ = x
 
 structure SubtypeLike3 {α β γ : Sort u} (p : α → β → γ → Prop) where
 
@@ -330,7 +330,7 @@ set_option pp.analyze.explicitHoles false in
 
 set_option pp.analyze.trustSubtypeMk true in
 #testDelab fun (n : Nat) (val : List Nat) (property : List.length val = n) => List.length { val := val, property := property : { x : List Nat // List.length x = n } }.val = n
-  expecting fun n val property => List.length (Subtype.val (p := fun x => List.length x = n) (⟨val, property⟩ : { x : List Nat // List.length x = n })) = n
+  expecting fun n val property => (Subtype.val (p := fun x => x.length = n) (⟨val, property⟩ : { x : List Nat // x.length = n })).length = n
 
 #testDelabN Nat.brecOn
 #testDelabN Nat.below
@@ -358,13 +358,7 @@ set_option pp.analyze.trustSubtypeMk true in
 #testDelabN Lean.PersistentHashMap.getCollisionNodeSize.match_1
 #testDelabN Lean.HashMap.size.match_1
 #testDelabN and_false
-
--- TODO: this one prints out a structure instance with keyword field `end`
-set_option pp.structureInstances false in
 #testDelabN Lean.Server.FileWorker.handlePlainTermGoal
-
--- TODO: this one desugars to a `doLet` in an assignment
-set_option pp.notation false in
 #testDelabN Lean.Server.FileWorker.handlePlainGoal
 
 -- TODO: this error occurs because we use a term's type to determine `blockImplicit` (@),
diff --git a/tests/lean/run/delabProjectionApp.lean b/tests/lean/run/delabProjectionApp.lean
index 91f80208e3fb..af3770fd28e5 100644
--- a/tests/lean/run/delabProjectionApp.lean
+++ b/tests/lean/run/delabProjectionApp.lean
@@ -2,9 +2,6 @@
 # Delaboration of projection functions, and generalized field notation
 -/
 
--- TODO(kmill): remove this once this is the default
-set_option pp.fieldNotation.generalized true
-
 structure A where
   x : Nat
 
@@ -40,7 +37,7 @@ end
 
 section
 /-!
-Checking `pp.structureProjections` can turn off this delaborator.
+Checking `pp.fieldNotation` can turn off this delaborator.
 -/
 
 set_option pp.fieldNotation false
diff --git a/tests/lean/run/eqValue.lean b/tests/lean/run/eqValue.lean
index 1e62bc1fabac..d014a3d2e8c2 100644
--- a/tests/lean/run/eqValue.lean
+++ b/tests/lean/run/eqValue.lean
@@ -15,7 +15,7 @@
 #guard_msgs in
 #check f.eq_3
 /--
-info: f.eq_4 (x_2 : Nat) (x_3 : x_2 = 99 → False) (x_4 : x_2 = 999 → False) : f (Nat.succ x_2) = f x_2
+info: f.eq_4 (x_2 : Nat) (x_3 : x_2 = 99 → False) (x_4 : x_2 = 999 → False) : f x_2.succ = f x_2
 -/
 #guard_msgs in
 #check f.eq_4
diff --git a/tests/lean/run/funind_demo.lean b/tests/lean/run/funind_demo.lean
index 8090af4fb59e..acaa5621e526 100644
--- a/tests/lean/run/funind_demo.lean
+++ b/tests/lean/run/funind_demo.lean
@@ -8,8 +8,8 @@ derive_functional_induction ackermann
 
 /--
 info: ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
-  (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
-  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) :
+  (case2 : ∀ (n : Nat), motive n 1 → motive n.succ 0)
+  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) :
   ∀ (a a_1 : Nat), motive a a_1
 -/
 #guard_msgs in
diff --git a/tests/lean/run/funind_expr.lean b/tests/lean/run/funind_expr.lean
index d15fe1bd03a2..0161fef6298e 100644
--- a/tests/lean/run/funind_expr.lean
+++ b/tests/lean/run/funind_expr.lean
@@ -54,22 +54,22 @@ info: Expr.typeCheck.induct (motive : Expr → Prop) (case1 : ∀ (a : Nat), mot
   (case2 : ∀ (a : Bool), motive (Expr.bool a))
   (case3 :
     ∀ (a b : Expr) (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat),
-      Expr.typeCheck b = Maybe.found Ty.nat h₂ →
-        Expr.typeCheck a = Maybe.found Ty.nat h₁ → motive a → motive b → motive (Expr.plus a b))
+      b.typeCheck = Maybe.found Ty.nat h₂ →
+        a.typeCheck = Maybe.found Ty.nat h₁ → motive a → motive b → motive (a.plus b))
   (case4 :
     ∀ (a b : Expr),
       (∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat),
-          Expr.typeCheck a = Maybe.found Ty.nat h₁ → Expr.typeCheck b = Maybe.found Ty.nat h₂ → False) →
-        motive a → motive b → motive (Expr.plus a b))
+          a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → False) →
+        motive a → motive b → motive (a.plus b))
   (case5 :
     ∀ (a b : Expr) (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
-      Expr.typeCheck b = Maybe.found Ty.bool h₂ →
-        Expr.typeCheck a = Maybe.found Ty.bool h₁ → motive a → motive b → motive (Expr.and a b))
+      b.typeCheck = Maybe.found Ty.bool h₂ →
+        a.typeCheck = Maybe.found Ty.bool h₁ → motive a → motive b → motive (a.and b))
   (case6 :
     ∀ (a b : Expr),
       (∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool),
-          Expr.typeCheck a = Maybe.found Ty.bool h₁ → Expr.typeCheck b = Maybe.found Ty.bool h₂ → False) →
-        motive a → motive b → motive (Expr.and a b))
+          a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → False) →
+        motive a → motive b → motive (a.and b))
   (x : Expr) : motive x
 -/
 #guard_msgs in
diff --git a/tests/lean/run/funind_mutual_dep.lean b/tests/lean/run/funind_mutual_dep.lean
index 5efaf51be627..0d7e3192f6f0 100644
--- a/tests/lean/run/funind_mutual_dep.lean
+++ b/tests/lean/run/funind_mutual_dep.lean
@@ -50,21 +50,18 @@ derive_functional_induction Finite.functions
 /--
 info: Finite.functions.induct (motive1 : Finite → Prop) (motive2 : (α : Type) → Finite → List α → Prop)
   (case1 : motive1 Finite.unit) (case2 : motive1 Finite.bool)
-  (case3 : ∀ (t1 t2 : Finite), motive1 t1 → motive1 t2 → motive1 (Finite.pair t1 t2))
-  (case4 :
-    ∀ (t1 t2 : Finite), motive1 t2 → motive2 (Finite.asType t2) t1 (Finite.enumerate t2) → motive1 (Finite.arr t1 t2))
+  (case3 : ∀ (t1 t2 : Finite), motive1 t1 → motive1 t2 → motive1 (t1.pair t2))
+  (case4 : ∀ (t1 t2 : Finite), motive1 t2 → motive2 t2.asType t1 t2.enumerate → motive1 (t1.arr t2))
   (case5 : ∀ (α : Type) (results : List α), motive2 α Finite.unit results)
   (case6 : ∀ (α : Type) (results : List α), motive2 α Finite.bool results)
   (case7 :
     ∀ (α : Type) (results : List α) (t1 t2 : Finite),
-      motive2 α t2 results →
-        motive2 (Finite.asType t2 → α) t1 (Finite.functions t2 results) → motive2 α (Finite.pair t1 t2) results)
+      motive2 α t2 results → motive2 (t2.asType → α) t1 (t2.functions results) → motive2 α (t1.pair t2) results)
   (case8 :
     ∀ (α : Type) (results : List α) (t1 t2 : Finite),
       motive1 t1 →
-        (∀ (rest : List (Finite.asType (Finite.arr t1 t2) → α)),
-            motive2 (Finite.asType (Finite.arr t1 t2) → α) t2 rest) →
-          motive2 α (Finite.arr t1 t2) results)
+        (∀ (rest : List ((t1.arr t2).asType → α)), motive2 ((t1.arr t2).asType → α) t2 rest) →
+          motive2 α (t1.arr t2) results)
   (α : Type) (t : Finite) (results : List α) : motive2 α t results
 -/
 #guard_msgs in
diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean
index 7a1965c7d38e..5253ef5357ef 100644
--- a/tests/lean/run/funind_tests.lean
+++ b/tests/lean/run/funind_tests.lean
@@ -10,8 +10,8 @@ derive_functional_induction ackermann
 
 /--
 info: Unary.ackermann.induct (motive : Nat × Nat → Prop) (case1 : ∀ (m : Nat), motive (0, m))
-  (case2 : ∀ (n : Nat), motive (n, 1) → motive (Nat.succ n, 0))
-  (case3 : ∀ (n m : Nat), motive (n + 1, m) → motive (n, ackermann (n + 1, m)) → motive (Nat.succ n, Nat.succ m))
+  (case2 : ∀ (n : Nat), motive (n, 1) → motive (n.succ, 0))
+  (case3 : ∀ (n m : Nat), motive (n + 1, m) → motive (n, ackermann (n + 1, m)) → motive (n.succ, m.succ))
   (x : Nat × Nat) : motive x
 -/
 #guard_msgs in
@@ -30,8 +30,8 @@ derive_functional_induction ackermann
 
 /--
 info: Binary.ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
-  (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
-  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m)) :
+  (case2 : ∀ (n : Nat), motive n 1 → motive n.succ 0)
+  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive n.succ m.succ) :
   ∀ (a a_1 : Nat), motive a a_1
 -/
 #guard_msgs in
@@ -64,7 +64,7 @@ termination_by n => n
 derive_functional_induction fib
 /--
 info: fib.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
-  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive (Nat.succ (Nat.succ n))) (x : Nat) : motive x
+  (case3 : ∀ (n : Nat), motive n → motive (n + 1) → motive n.succ.succ) (x : Nat) : motive x
 -/
 #guard_msgs in
 #check fib.induct
@@ -79,8 +79,8 @@ termination_by n => n
 derive_functional_induction have_tailrec
 
 /--
-info: have_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive (Nat.succ n)) (x : Nat) : motive x
+info: have_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), n < n + 1 → motive n → motive n.succ)
+  (x : Nat) : motive x
 -/
 #guard_msgs in
 #check have_tailrec.induct
@@ -96,7 +96,7 @@ termination_by n => n
 derive_functional_induction have_non_tailrec
 
 /--
-info: have_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive (Nat.succ n))
+info: have_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
   (x : Nat) : motive x
 -/
 #guard_msgs in
@@ -116,7 +116,7 @@ info: let_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
   (case2 :
     ∀ (n : Nat),
       let h2 := ⋯;
-      motive n → motive (Nat.succ n))
+      motive n → motive n.succ)
   (x : Nat) : motive x
 -/
 #guard_msgs in
@@ -133,7 +133,7 @@ termination_by n => n
 derive_functional_induction let_non_tailrec
 
 /--
-info: let_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive (Nat.succ n))
+info: let_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
   (x : Nat) : motive x
 -/
 #guard_msgs in
@@ -153,8 +153,8 @@ derive_functional_induction with_ite_tailrec
 
 /--
 info: with_ite_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive (Nat.succ n))
-  (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive n → motive (Nat.succ n)) (x : Nat) : motive x
+  (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive n.succ)
+  (case3 : ∀ (n : Nat), ¬n % 2 = 0 → motive n → motive n.succ) (x : Nat) : motive x
 -/
 #guard_msgs in
 #check with_ite_tailrec.induct
@@ -175,7 +175,7 @@ derive_functional_induction with_ite_non_tailrec
 
 /--
 info: with_ite_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1)
-  (case3 : ∀ (n : Nat), motive (n + 1) → motive n → motive (Nat.succ (Nat.succ n))) (x : Nat) : motive x
+  (case3 : ∀ (n : Nat), motive (n + 1) → motive n → motive n.succ.succ) (x : Nat) : motive x
 -/
 #guard_msgs in
 #check with_ite_non_tailrec.induct
@@ -227,7 +227,7 @@ derive_functional_induction with_match_refining_tailrec
 
 /--
 info: with_match_refining_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 0 → motive (Nat.succ 0))
-  (case3 : ∀ (m : Nat), (m = 0 → False) → motive m → motive (Nat.succ m)) (x : Nat) : motive x
+  (case3 : ∀ (m : Nat), (m = 0 → False) → motive m → motive m.succ) (x : Nat) : motive x
 -/
 #guard_msgs in
 #check with_match_refining_tailrec.induct
@@ -243,8 +243,8 @@ derive_functional_induction with_arg_refining_match1
 
 /--
 info: with_arg_refining_match1.induct (motive : Nat → Nat → Prop) (case1 : ∀ (i : Nat), motive i 0)
-  (case2 : ∀ (n : Nat), motive 0 (Nat.succ n))
-  (case3 : ∀ (i n : Nat), ¬i = 0 → motive (i - 1) n → motive i (Nat.succ n)) (i : Nat) : ∀ (a : Nat), motive i a
+  (case2 : ∀ (n : Nat), motive 0 n.succ) (case3 : ∀ (i n : Nat), ¬i = 0 → motive (i - 1) n → motive i n.succ)
+  (i : Nat) : ∀ (a : Nat), motive i a
 -/
 #guard_msgs in
 #check with_arg_refining_match1.induct
@@ -259,7 +259,7 @@ derive_functional_induction with_arg_refining_match2
 /--
 info: with_arg_refining_match2.induct (motive : Nat → Nat → Prop) (case1 : ∀ (n : Nat), motive 0 n)
   (case2 : ∀ (i : Nat), ¬i = 0 → motive i 0)
-  (case3 : ∀ (i : Nat), ¬i = 0 → ∀ (n : Nat), motive (i - 1) n → motive i (Nat.succ n)) (i n : Nat) : motive i n
+  (case3 : ∀ (i : Nat), ¬i = 0 → ∀ (n : Nat), motive (i - 1) n → motive i n.succ) (i n : Nat) : motive i n
 -/
 #guard_msgs in
 #check with_arg_refining_match2.induct
@@ -277,8 +277,8 @@ derive_functional_induction with_other_match_tailrec
 
 /--
 info: with_other_match_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive (Nat.succ n))
-  (case3 : ∀ (n : Nat), (n % 2 = 0 → False) → motive n → motive (Nat.succ n)) (x : Nat) : motive x
+  (case2 : ∀ (n : Nat), n % 2 = 0 → motive n → motive n.succ)
+  (case3 : ∀ (n : Nat), (n % 2 = 0 → False) → motive n → motive n.succ) (x : Nat) : motive x
 -/
 #guard_msgs in
 #check with_other_match_tailrec.induct
@@ -293,7 +293,7 @@ derive_functional_induction with_mixed_match_tailrec
 
 /--
 info: with_mixed_match_tailrec.induct (motive : Nat → Nat → Nat → Nat → Prop) (case1 : ∀ (a a_1 x : Nat), motive 0 x a a_1)
-  (case2 : ∀ (a a_1 a_2 x : Nat), motive a_2 x (a % 2) (a_1 % 2) → motive (Nat.succ a_2) x a a_1) :
+  (case2 : ∀ (a a_1 a_2 x : Nat), motive a_2 x (a % 2) (a_1 % 2) → motive a_2.succ x a a_1) :
   ∀ (a a_1 a_2 a_3 : Nat), motive a a_1 a_2 a_3
 -/
 #guard_msgs in
@@ -312,8 +312,8 @@ derive_functional_induction with_mixed_match_tailrec2
 
 /--
 info: with_mixed_match_tailrec2.induct (motive : Nat → Nat → Nat → Nat → Nat → Prop)
-  (case1 : ∀ (a a_1 a_2 a_3 : Nat), motive 0 a a_1 a_2 a_3) (case2 : ∀ (a a_1 n x : Nat), motive (Nat.succ n) 0 x a a_1)
-  (case3 : ∀ (a a_1 n a_2 x : Nat), motive n a_2 x (a % 2) (a_1 % 2) → motive (Nat.succ n) (Nat.succ a_2) x a a_1) :
+  (case1 : ∀ (a a_1 a_2 a_3 : Nat), motive 0 a a_1 a_2 a_3) (case2 : ∀ (a a_1 n x : Nat), motive n.succ 0 x a a_1)
+  (case3 : ∀ (a a_1 n a_2 x : Nat), motive n a_2 x (a % 2) (a_1 % 2) → motive n.succ a_2.succ x a a_1) :
   ∀ (a a_1 a_2 a_3 a_4 : Nat), motive a a_1 a_2 a_3 a_4
 -/
 #guard_msgs in
@@ -331,8 +331,8 @@ termination_by n => n
 derive_functional_induction with_match_non_tailrec
 
 /--
-info: with_match_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), motive n → motive (Nat.succ n)) (x : Nat) : motive x
+info: with_match_non_tailrec.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
+  (x : Nat) : motive x
 -/
 #guard_msgs in
 #check with_match_non_tailrec.induct
@@ -355,7 +355,7 @@ info: with_match_non_tailrec_refining.induct (motive : Nat → Prop) (case1 : mo
       (match n with
         | 0 => motive 0
         | m => motive m) →
-        motive (Nat.succ n))
+        motive n.succ)
   (x : Nat) : motive x
 -/
 #guard_msgs in
@@ -373,8 +373,8 @@ derive_functional_induction with_overlap
 
 /--
 info: with_overlap.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : motive 1) (case3 : motive 2) (case4 : motive 3)
-  (case5 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → (n = 2 → False) → motive n → motive (Nat.succ n))
-  (x : Nat) : motive x
+  (case5 : ∀ (n : Nat), (n = 0 → False) → (n = 1 → False) → (n = 2 → False) → motive n → motive n.succ) (x : Nat) :
+  motive x
 -/
 #guard_msgs in
 #check with_overlap.induct
@@ -392,7 +392,7 @@ derive_functional_induction unary
 
 /--
 info: UnusedExtraParams.unary.induct (base : Nat) (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), motive n → motive (Nat.succ n)) (x : Nat) : motive x
+  (case2 : ∀ (n : Nat), motive n → motive n.succ) (x : Nat) : motive x
 -/
 #guard_msgs in
 #check unary.induct
@@ -405,7 +405,7 @@ derive_functional_induction binary
 
 /--
 info: UnusedExtraParams.binary.induct (base : Nat) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
-  (case2 : ∀ (n m : Nat), motive n m → motive (Nat.succ n) m) : ∀ (a a_1 : Nat), motive a a_1
+  (case2 : ∀ (n m : Nat), motive n m → motive n.succ m) : ∀ (a a_1 : Nat), motive a a_1
 -/
 #guard_msgs in
 #check binary.induct
@@ -441,7 +441,7 @@ info: NonTailrecMatch.match_non_tail.induct (motive : Nat → Prop)
       (match x with
         | 0 => True
         | 1 => True
-        | Nat.succ (Nat.succ n) => motive n ∧ motive (n + 1)) →
+        | n.succ.succ => motive n ∧ motive (n + 1)) →
         motive x)
   (x : Nat) : motive x
 -/
@@ -468,7 +468,7 @@ termination_by n
 derive_functional_induction foo
 
 /--
-info: AsPattern.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive (Nat.succ n))
+info: AsPattern.foo.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : ∀ (n : Nat), motive n → motive n.succ)
   (x : Nat) : motive x
 -/
 #guard_msgs in
@@ -490,7 +490,7 @@ info: AsPattern.bar.induct (motive : Nat → Prop)
     ∀ (x : Nat),
       (match x with
         | 0 => True
-        | x@h:(Nat.succ n) => motive n) →
+        | x@h:n.succ => motive n) →
         motive x)
   (x : Nat) : motive x
 -/
@@ -578,8 +578,8 @@ derive_functional_induction foo
 
 /--
 info: RecCallInDisrs.foo.induct (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), foo n = 0 → motive n → motive (Nat.succ n))
-  (case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive (Nat.succ n)) (x : Nat) : motive x
+  (case2 : ∀ (n : Nat), foo n = 0 → motive n → motive n.succ)
+  (case3 : ∀ (n : Nat), ¬foo n = 0 → motive n → motive n.succ) (x : Nat) : motive x
 -/
 #guard_msgs in
 #check foo.induct
@@ -597,7 +597,7 @@ derive_functional_induction bar
 /--
 info: RecCallInDisrs.bar.induct (motive : Nat → Prop) (case1 : motive 0) (case2 : bar 0 = 0 → motive 0 → motive (Nat.succ 0))
   (case3 : (bar 0 = 0 → False) → motive 0 → motive (Nat.succ 0))
-  (case4 : ∀ (m : Nat), motive (Nat.succ m) → motive m → motive (Nat.succ (Nat.succ m))) (x : Nat) : motive x
+  (case4 : ∀ (m : Nat), motive m.succ → motive m → motive m.succ.succ) (x : Nat) : motive x
 -/
 #guard_msgs in
 #check bar.induct
@@ -620,7 +620,7 @@ derive_functional_induction even
 
 /--
 info: EvenOdd.even.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : motive2 0)
-  (case3 : ∀ (n : Nat), motive2 n → motive1 (Nat.succ n)) (case4 : ∀ (n : Nat), motive1 n → motive2 (Nat.succ n)) :
+  (case3 : ∀ (n : Nat), motive2 n → motive1 n.succ) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) :
   ∀ (a : Nat), motive1 a
 -/
 #guard_msgs in
@@ -628,7 +628,7 @@ info: EvenOdd.even.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (
 
 /--
 info: EvenOdd.odd.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : motive2 0)
-  (case3 : ∀ (n : Nat), motive2 n → motive1 (Nat.succ n)) (case4 : ∀ (n : Nat), motive1 n → motive2 (Nat.succ n)) :
+  (case3 : ∀ (n : Nat), motive2 n → motive1 n.succ) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) :
   ∀ (a : Nat), motive2 a
 -/
 #guard_msgs in
@@ -681,7 +681,7 @@ derive_functional_induction unary
 
 /--
 info: DefaultArgument.unary.induct (fixed : Bool) (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), motive n → motive (Nat.succ n)) (x : Nat) : motive x
+  (case2 : ∀ (n : Nat), motive n → motive n.succ) (x : Nat) : motive x
 -/
 #guard_msgs in
 #check unary.induct
@@ -695,7 +695,7 @@ derive_functional_induction foo
 
 /--
 info: DefaultArgument.foo.induct (fixed : Bool) (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
-  (case2 : ∀ (m n : Nat), motive n m → motive (Nat.succ n) m) (n m : Nat) : motive n m
+  (case2 : ∀ (m n : Nat), motive n m → motive n.succ m) (n m : Nat) : motive n m
 -/
 #guard_msgs in
 #check foo.induct
@@ -719,9 +719,7 @@ info: Nary.foo.induct (motive : Nat → Nat → (k : Nat) → Fin k → Prop)
   (case2 : ∀ (x x_1 : Nat) (x_2 : Fin x_1), (x = 0 → False) → motive x 0 x_1 x_2)
   (case3 : ∀ (x x_1 : Nat) (x_2 : Fin 0), (x = 0 → False) → (x_1 = 0 → False) → motive x x_1 0 x_2)
   (case4 : ∀ (x x_1 : Nat) (x_2 : Fin 1), (x = 0 → False) → (x_1 = 0 → False) → motive x x_1 1 x_2)
-  (case5 :
-    ∀ (n m k : Nat) (x : Fin (k + 2)),
-      motive n m (k + 1) ⟨0, ⋯⟩ → motive (Nat.succ n) (Nat.succ m) (Nat.succ (Nat.succ k)) x) :
+  (case5 : ∀ (n m k : Nat) (x : Fin (k + 2)), motive n m (k + 1) ⟨0, ⋯⟩ → motive n.succ m.succ k.succ.succ x) :
   ∀ (a a_1 k : Nat) (a_2 : Fin k), motive a a_1 k a_2
 -/
 #guard_msgs in
@@ -775,8 +773,8 @@ derive_functional_induction even._mutual
 
 /--
 info: CommandIdempotence.even._mutual.induct (motive : Nat ⊕' Nat → Prop) (case1 : motive (PSum.inl 0))
-  (case2 : motive (PSum.inr 0)) (case3 : ∀ (n : Nat), motive (PSum.inr n) → motive (PSum.inl (Nat.succ n)))
-  (case4 : ∀ (n : Nat), motive (PSum.inl n) → motive (PSum.inr (Nat.succ n))) (x : Nat ⊕' Nat) : motive x
+  (case2 : motive (PSum.inr 0)) (case3 : ∀ (n : Nat), motive (PSum.inr n) → motive (PSum.inl n.succ))
+  (case4 : ∀ (n : Nat), motive (PSum.inl n) → motive (PSum.inr n.succ)) (x : Nat ⊕' Nat) : motive x
 -/
 #guard_msgs in
 #check even._mutual.induct
@@ -789,15 +787,15 @@ derive_functional_induction even
 
 /--
 info: CommandIdempotence.even._mutual.induct (motive : Nat ⊕' Nat → Prop) (case1 : motive (PSum.inl 0))
-  (case2 : motive (PSum.inr 0)) (case3 : ∀ (n : Nat), motive (PSum.inr n) → motive (PSum.inl (Nat.succ n)))
-  (case4 : ∀ (n : Nat), motive (PSum.inl n) → motive (PSum.inr (Nat.succ n))) (x : Nat ⊕' Nat) : motive x
+  (case2 : motive (PSum.inr 0)) (case3 : ∀ (n : Nat), motive (PSum.inr n) → motive (PSum.inl n.succ))
+  (case4 : ∀ (n : Nat), motive (PSum.inl n) → motive (PSum.inr n.succ)) (x : Nat ⊕' Nat) : motive x
 -/
 #guard_msgs in
 #check even._mutual.induct
 
 /--
 info: CommandIdempotence.even.induct (motive1 motive2 : Nat → Prop) (case1 : motive1 0) (case2 : motive2 0)
-  (case3 : ∀ (n : Nat), motive2 n → motive1 (Nat.succ n)) (case4 : ∀ (n : Nat), motive1 n → motive2 (Nat.succ n)) :
+  (case3 : ∀ (n : Nat), motive2 n → motive1 n.succ) (case4 : ∀ (n : Nat), motive1 n → motive2 n.succ) :
   ∀ (a : Nat), motive1 a
 -/
 #guard_msgs in
@@ -856,8 +854,8 @@ derive_functional_induction foo
 
 /--
 info: PreserveParams.foo.induct (a : Nat) (motive : Nat → Prop) (case1 : motive 0)
-  (case2 : ∀ (n : Nat), a = 23 → motive (Nat.succ n)) (case3 : ¬a = 23 → motive (Nat.succ a))
-  (case4 : ∀ (n : Nat), ¬a = 23 → ¬a = n → motive n → motive (Nat.succ n)) (x : Nat) : motive x
+  (case2 : ∀ (n : Nat), a = 23 → motive n.succ) (case3 : ¬a = 23 → motive a.succ)
+  (case4 : ∀ (n : Nat), ¬a = 23 → ¬a = n → motive n → motive n.succ) (x : Nat) : motive x
 -/
 #guard_msgs in
 #check foo.induct
diff --git a/tests/lean/run/heapSort.lean b/tests/lean/run/heapSort.lean
index 58f7f8157175..fe72a7d9640d 100644
--- a/tests/lean/run/heapSort.lean
+++ b/tests/lean/run/heapSort.lean
@@ -177,11 +177,11 @@ attribute [simp] Array.heapSort.loop
 /--
 info: Array.heapSort.loop.eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : BinaryHeap α fun y x => lt x y) (out : Array α) :
   Array.heapSort.loop lt a out =
-    match e : BinaryHeap.max a with
+    match e : a.max with
     | none => out
     | some x =>
       let_fun this := ⋯;
-      Array.heapSort.loop lt (BinaryHeap.popMax a) (Array.push out x)
+      Array.heapSort.loop lt a.popMax (out.push x)
 -/
 #guard_msgs in
 #check Array.heapSort.loop.eq_1
diff --git a/tests/lean/run/match_lit_fin_cover.lean b/tests/lean/run/match_lit_fin_cover.lean
index 53353cc4d541..f869c9b60610 100644
--- a/tests/lean/run/match_lit_fin_cover.lean
+++ b/tests/lean/run/match_lit_fin_cover.lean
@@ -22,9 +22,7 @@ info: bla.eq_1 (y : Nat) : bla 0 y = 10
 #guard_msgs in
 #check bla.eq_1
 
-/--
-info: bla.eq_4 (y_2 : Nat) : bla 2 (Nat.succ y_2) = bla 2 y_2 + 1
--/
+/-- info: bla.eq_4 (y_2 : Nat) : bla 2 y_2.succ = bla 2 y_2 + 1 -/
 #guard_msgs in
 #check bla.eq_4
 
@@ -67,8 +65,6 @@ info: foo'.eq_2 (y : Nat) : foo' (1#3) y = 6
 #guard_msgs in
 #check foo'.eq_2
 
-/--
-info: foo'.eq_9 (y_2 : Nat) : foo' (7#3) (Nat.succ y_2) = foo' 7 y_2 + 1
--/
+/-- info: foo'.eq_9 (y_2 : Nat) : foo' (7#3) y_2.succ = foo' 7 y_2 + 1 -/
 #guard_msgs in
 #check foo'.eq_9
diff --git a/tests/lean/run/namePatEqThm.lean b/tests/lean/run/namePatEqThm.lean
index 8a627ebeeea7..a618088387fa 100644
--- a/tests/lean/run/namePatEqThm.lean
+++ b/tests/lean/run/namePatEqThm.lean
@@ -6,7 +6,7 @@
 #guard_msgs in
 #check iota.eq_1
 
-/-- info: iota.eq_2 (n : Nat) : iota (Nat.succ n) = Nat.succ n :: iota n -/
+/-- info: iota.eq_2 (n : Nat) : iota n.succ = n.succ :: iota n -/
 #guard_msgs in
 #check iota.eq_2
 
diff --git a/tests/lean/run/printEqns.lean b/tests/lean/run/printEqns.lean
index baa2801b8d9a..42f24d1f19e8 100644
--- a/tests/lean/run/printEqns.lean
+++ b/tests/lean/run/printEqns.lean
@@ -1,17 +1,15 @@
 /--
 info: equations:
-theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
-theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
-  List.append (a :: l) x = a :: List.append l x
+theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), [].append x = x
+theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α), (a :: l).append x = a :: l.append x
 -/
 #guard_msgs in
 #print eqns List.append
 
 /--
 info: equations:
-theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
-theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
-  List.append (a :: l) x = a :: List.append l x
+theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), [].append x = x
+theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α), (a :: l).append x = a :: l.append x
 -/
 #guard_msgs in
 #print equations List.append
@@ -24,8 +22,8 @@ theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : Lis
 /--
 info: equations:
 theorem ack.eq_1 : ∀ (x : Nat), ack 0 x = x + 1
-theorem ack.eq_2 : ∀ (x_2 : Nat), ack (Nat.succ x_2) 0 = ack x_2 1
-theorem ack.eq_3 : ∀ (x_2 y : Nat), ack (Nat.succ x_2) (Nat.succ y) = ack x_2 (ack (x_2 + 1) y)
+theorem ack.eq_2 : ∀ (x_2 : Nat), ack x_2.succ 0 = ack x_2 1
+theorem ack.eq_3 : ∀ (x_2 y : Nat), ack x_2.succ y.succ = ack x_2 (ack (x_2 + 1) y)
 -/
 #guard_msgs in
 #print eqns ack
diff --git a/tests/lean/run/reserved.lean b/tests/lean/run/reserved.lean
index f190b5baa323..9b2770346632 100644
--- a/tests/lean/run/reserved.lean
+++ b/tests/lean/run/reserved.lean
@@ -45,7 +45,7 @@ info: fact.def :
     fact x =
       match x with
       | 0 => 1
-      | Nat.succ n => (n + 1) * fact n
+      | n.succ => (n + 1) * fact n
 -/
 #guard_msgs in
 #check fact.def
@@ -54,7 +54,7 @@ info: fact.def :
 #guard_msgs in
 #check fact.eq_1
 
-/-- info: fact.eq_2 (n : Nat) : fact (Nat.succ n) = (n + 1) * fact n -/
+/-- info: fact.eq_2 (n : Nat) : fact n.succ = (n + 1) * fact n -/
 #guard_msgs in
 #check fact.eq_2
 
diff --git a/tests/lean/rwEqThms.lean.expected.out b/tests/lean/rwEqThms.lean.expected.out
index f4978927ff83..166374b659ff 100644
--- a/tests/lean/rwEqThms.lean.expected.out
+++ b/tests/lean/rwEqThms.lean.expected.out
@@ -2,7 +2,7 @@
 a : α
 as bs : List α
 h : bs = a :: as
-⊢ List.length (?head :: as) = List.length bs
+⊢ (?head :: as).length = bs.length
 
 case head
 α : Type ?u
@@ -14,29 +14,29 @@ h : bs = a :: as
 b a : α
 as bs : List α
 h : as = bs
-⊢ List.length as + 1 + 1 = List.length bs + 2
+⊢ as.length + 1 + 1 = bs.length + 2
 α : Type ?u
 b a : α
 as bs : List α
 h : as = bs
-⊢ List.length as + 1 + 1 = List.length (b :: bs) + 1
+⊢ as.length + 1 + 1 = (b :: bs).length + 1
 α : Type ?u
 b a : α
 as bs : List α
 h : as = bs
-⊢ List.length as + 1 + 1 = List.length bs + 1 + 1
+⊢ as.length + 1 + 1 = bs.length + 1 + 1
 α : Type ?u
 b a : α
 as bs : List α
 h : as = bs
-⊢ id (List.length (a :: b :: as)) = List.length (b :: bs) + 1
+⊢ id (a :: b :: as).length = (b :: bs).length + 1
 α : Type ?u
 b a : α
 as bs : List α
 h : as = bs
-⊢ List.length (a :: b :: as) = List.length (b :: bs) + 1
+⊢ (a :: b :: as).length = (b :: bs).length + 1
 α : Type ?u
 b a : α
 as bs : List α
 h : as = bs
-⊢ List.length as + 1 + 1 = List.length bs + 1 + 1
+⊢ as.length + 1 + 1 = bs.length + 1 + 1
diff --git a/tests/lean/rwWithoutOffsetCnstrs.lean.expected.out b/tests/lean/rwWithoutOffsetCnstrs.lean.expected.out
index 4f9c78616420..2a442e29993c 100644
--- a/tests/lean/rwWithoutOffsetCnstrs.lean.expected.out
+++ b/tests/lean/rwWithoutOffsetCnstrs.lean.expected.out
@@ -1,3 +1,3 @@
 rwWithoutOffsetCnstrs.lean:5:0-5:7: warning: declaration uses 'sorry'
 m n : Nat
-⊢ Nat.ble (n + 1) n = false
+⊢ (n + 1).ble n = false
diff --git a/tests/lean/safeShadowing.lean.expected.out b/tests/lean/safeShadowing.lean.expected.out
index abd376091e6e..08b36e32a128 100644
--- a/tests/lean/safeShadowing.lean.expected.out
+++ b/tests/lean/safeShadowing.lean.expected.out
@@ -5,11 +5,11 @@ def f : Nat → Nat → Nat :=
 fun x x =>
   match x with
   | 0 => x + 1
-  | Nat.succ n => x + 2
+  | n.succ => x + 2
 fun {α_1} a => a : {α_1 : Sort u_1} → α_1 → α_1
 fun x x_1 => x_1 : Nat → Nat → Nat
 def f : Nat → Nat → Nat :=
 fun x x_1 =>
   match x_1 with
   | 0 => x_1 + 1
-  | Nat.succ n => x_1 + 2
+  | n.succ => x_1 + 2
diff --git a/tests/lean/simpZetaFalse.lean.expected.out b/tests/lean/simpZetaFalse.lean.expected.out
index 3e00ee99ccbb..38df4fa0349b 100644
--- a/tests/lean/simpZetaFalse.lean.expected.out
+++ b/tests/lean/simpZetaFalse.lean.expected.out
@@ -9,13 +9,12 @@ theorem ex1 : ∀ (x : Nat),
       if f (f x) = x then 1 else y + 1) =
       1 :=
 fun x h =>
-  Eq.mpr
-    (id
-      (congrArg (fun x => x = 1)
-        (let_congr (Eq.refl (x * x)) fun y =>
-          ite_congr (Eq.trans (congrArg (fun x_1 => x_1 = x) h) (eq_self x)) (fun a => Eq.refl 1) fun a =>
-            Eq.refl (y + 1))))
-    (of_eq_true (Eq.trans (congrArg (fun x => x = 1) (ite_cond_eq_true 1 (x * x + 1) (Eq.refl True))) (eq_self 1)))
+  (id
+        (congrArg (fun x => x = 1)
+          (let_congr (Eq.refl (x * x)) fun y =>
+            ite_congr ((congrArg (fun x_1 => x_1 = x) h).trans (eq_self x)) (fun a => Eq.refl 1) fun a =>
+              Eq.refl (y + 1)))).mpr
+    (of_eq_true ((congrArg (fun x => x = 1) (ite_cond_eq_true 1 (x * x + 1) (Eq.refl True))).trans (eq_self 1)))
 x z : Nat
 h : f (f x) = x
 h' : z = x
@@ -29,8 +28,8 @@ theorem ex2 : ∀ (x z : Nat),
         y) =
         z :=
 fun x z h h' =>
-  Eq.mpr (id (congrArg (fun x => x = z) (let_val_congr (fun y => y) h)))
-    (of_eq_true (Eq.trans (congrArg (Eq x) h') (eq_self x)))
+  (id (congrArg (fun x => x = z) (let_val_congr (fun y => y) h))).mpr
+    (of_eq_true ((congrArg (Eq x) h').trans (eq_self x)))
 x z : Nat
 ⊢ (let α := Nat;
     fun x => 0 + x) =
@@ -46,5 +45,5 @@ theorem ex4 : ∀ (p : Prop),
       fun x => x = x) =
       fun z => p :=
 fun p h =>
-  Eq.mpr (id (congrArg (fun x => x = fun z => p) (let_body_congr 10 fun n => funext fun x => eq_self x)))
-    (of_eq_true (Eq.trans (congrArg (Eq fun x => True) (funext fun z => eq_true h)) (eq_self fun x => True)))
+  (id (congrArg (fun x => x = fun z => p) (let_body_congr 10 fun n => funext fun x => eq_self x))).mpr
+    (of_eq_true ((congrArg (Eq fun x => True) (funext fun z => eq_true h)).trans (eq_self fun x => True)))
diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out
index 081db169c2ab..7905221a93a6 100644
--- a/tests/lean/simp_trace.lean.expected.out
+++ b/tests/lean/simp_trace.lean.expected.out
@@ -19,9 +19,8 @@ Try this: simp only [foo]
 [Meta.Tactic.simp.rewrite] unfold foo, foo ==> 10
 [Meta.Tactic.simp.rewrite] @eq_self:1000, 10 + x = 10 + x ==> True
 Try this: simp only [g, pure]
-[Meta.Tactic.simp.rewrite] unfold g, g x ==> Id.run
-      (let x := x;
-      pure x)
+[Meta.Tactic.simp.rewrite] unfold g, g x ==> (let x := x;
+      pure x).run
 Try this: simp (config := { unfoldPartialApp := true }) only [f1, modify, modifyGet, MonadStateOf.modifyGet,
   StateT.modifyGet, pure, f2, bind, StateT.bind, get, getThe, MonadStateOf.get, StateT.get, set, StateT.set]
 [Meta.Tactic.simp.rewrite] unfold f1, f1 ==> modify fun x => g x
@@ -81,26 +80,26 @@ x y : Nat
 α : Type
 xs ys : List α
 h₁ : x + x = y
-h₂ : List.length xs + List.length ys = y
+h₂ : xs.length + ys.length = y
 ⊢ x = length xs
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-[Meta.Tactic.simp.rewrite] @List.length_append:1000, List.length (xs ++ ys) ==> List.length xs + List.length ys
+[Meta.Tactic.simp.rewrite] @List.length_append:1000, (xs ++ ys).length ==> xs.length + ys.length
 Try this: simp only [bla, h, List.length_append] at *
 simp_trace.lean:103:101-104:53: error: unsolved goals
 x y : Nat
 α : Type
 xs ys : List α
 h₁ : x + x = y
-h₂ : List.length xs + List.length ys = y
+h₂ : xs.length + ys.length = y
 ⊢ x = length xs
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-[Meta.Tactic.simp.rewrite] @List.length_append:1000, List.length (xs ++ ys) ==> List.length xs + List.length ys
+[Meta.Tactic.simp.rewrite] @List.length_append:1000, (xs ++ ys).length ==> xs.length + ys.length
 Try this: simp only [bla, h] at *
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
diff --git a/tests/lean/simprocEval4.lean.expected.out b/tests/lean/simprocEval4.lean.expected.out
index fb03c3101ea3..a549a3908efe 100644
--- a/tests/lean/simprocEval4.lean.expected.out
+++ b/tests/lean/simprocEval4.lean.expected.out
@@ -17,7 +17,7 @@ x : Nat
 x : Nat
 ⊢ foo x = 10
 x : Nat
-⊢ Int.natAbs (foo x) = 10
+⊢ (foo x).natAbs = 10
 x : Nat
 ⊢ boo x
 x : Nat
diff --git a/tests/lean/splitIssue.lean.expected.out b/tests/lean/splitIssue.lean.expected.out
index 1a68f1555d2d..01192f4907aa 100644
--- a/tests/lean/splitIssue.lean.expected.out
+++ b/tests/lean/splitIssue.lean.expected.out
@@ -1,3 +1,3 @@
 x x✝ y : Nat
-h : g x = Nat.succ y
+h : g x = y.succ
 ⊢ g x = 2 * x + 1
diff --git a/tests/lean/unfold1.lean.expected.out b/tests/lean/unfold1.lean.expected.out
index d046ef4aa81a..7fea34ae62d0 100644
--- a/tests/lean/unfold1.lean.expected.out
+++ b/tests/lean/unfold1.lean.expected.out
@@ -4,7 +4,7 @@ x : Nat
 ih : isEven (2 * x) = true
 ⊢ (match 2 * (x + 1) with
     | 0 => true
-    | Nat.succ n => isOdd n) =
+    | n.succ => isOdd n) =
     true
 case succ
 x : Nat
diff --git a/tests/lean/unfoldReduceMatch.lean.expected.out b/tests/lean/unfoldReduceMatch.lean.expected.out
index 5ad21f3c3e7c..72c499c4bbb5 100644
--- a/tests/lean/unfoldReduceMatch.lean.expected.out
+++ b/tests/lean/unfoldReduceMatch.lean.expected.out
@@ -1,3 +1,3 @@
 unfoldReduceMatch.lean:2:0-2:7: warning: declaration uses 'sorry'
 n : Nat
-⊢ Nat.succ (Nat.add Nat.zero n) = Nat.succ n
+⊢ (Nat.zero.add n).succ = n.succ
diff --git a/tests/lean/unnecessaryUnfolding.lean.expected.out b/tests/lean/unnecessaryUnfolding.lean.expected.out
index e930c9721207..7c2a0e888478 100644
--- a/tests/lean/unnecessaryUnfolding.lean.expected.out
+++ b/tests/lean/unnecessaryUnfolding.lean.expected.out
@@ -1 +1 @@
-id (M.run x) : IO Unit
+id x.run : IO Unit
diff --git a/tests/lean/unusedLet.lean.expected.out b/tests/lean/unusedLet.lean.expected.out
index e282187113cc..c33c68f746c4 100644
--- a/tests/lean/unusedLet.lean.expected.out
+++ b/tests/lean/unusedLet.lean.expected.out
@@ -6,7 +6,7 @@ fun x =>
   Nat.brecOn x fun x f =>
     (match (motive := (x : Nat) → Nat.below x → Nat) x with
       | 0 => fun x => 1
-      | Nat.succ n => fun x =>
+      | n.succ => fun x =>
         let y := 42;
         2 * x.fst.fst)
       f
diff --git a/tests/lean/wfrecUnusedLet.lean.expected.out b/tests/lean/wfrecUnusedLet.lean.expected.out
index 254b48353cfa..7fbd9db3dc08 100644
--- a/tests/lean/wfrecUnusedLet.lean.expected.out
+++ b/tests/lean/wfrecUnusedLet.lean.expected.out
@@ -1,5 +1,5 @@
 def f : Nat → Nat :=
-WellFounded.fix f.proof_1 fun n a =>
+f.proof_1.fix fun n a =>
   if h : n = 0 then 1
   else
     let y := 42;
diff --git a/tests/lean/whnfProj.lean.expected.out b/tests/lean/whnfProj.lean.expected.out
index 501a9f374277..d3a8c24ff199 100644
--- a/tests/lean/whnfProj.lean.expected.out
+++ b/tests/lean/whnfProj.lean.expected.out
@@ -1,7 +1,7 @@
 [Meta.debug] 1. x + 1
 [Meta.debug] 2. x + 1
-[Meta.debug] 3. Nat.add x 1
-[Meta.debug] 4. Nat.succ (Nat.add x 0)
+[Meta.debug] 3. x.add 1
+[Meta.debug] 4. (x.add 0).succ
 [Meta.debug] 1. (x, x + 1).fst
 [Meta.debug] 2. x
 [Meta.debug] 3. x