fix: do not pretty print theorems with generalized field notation

src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
 prelude
-import Lean.Meta.Basic
+import Lean.Meta.InferType
 import Lean.PrettyPrinter.Delaborator.Attributes
 import Lean.PrettyPrinter.Delaborator.Options
 import Lean.Structure
@@ -56,7 +56,7 @@ private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name ×
   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
+  forallBoundedTelescope info.type args.size fun params _ => do
     for i in [0:params.size] do
       let fvarId := params[i]!.fvarId!
       -- If there is a motive, we will treat this as a sort of control flow structure and so we won't use field notation.
@@ -94,6 +94,8 @@ def fieldNotationCandidate? (f : Expr) (args : Array Expr) (useGeneralizedFieldN
   -- Handle generalized field notation
   if useGeneralizedFieldNotation then
     try
+      -- Avoid field notation for theorems
+      guard !(← isProof f)
       return ← generalizedFieldInfo c args
     catch _ => pure ()
   -- It's not handled by any of the above.

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' => (id (propext (P_congr p q h))).mpr h'
+fun {p q} h h' => Eq.mpr (id (propext (P_congr p q h))) h'
 theorem ex2 : ∀ {p q : Prop}, p = q → P q → P p :=
-fun {p q} h h' => (id (propext (P_congr p q (Iff.of_eq h)))).mpr h'
+fun {p q} h h' => Eq.mpr (id (propext (P_congr p q (Iff.of_eq h)))) h'

tests/lean/arrayGetU.lean.expected.out

@@ -11,4 +11,4 @@ v : Nat
 h₁ : 0 + i < a.size
 h₂ : j < a.size
 h₃ : i = j
-⊢ f a i v (i.zero_add ▸ h₁) = f a j v h₂
+⊢ f a i v (Nat.zero_add i ▸ h₁) = f a j v h₂

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 x.add_comm y -/
+/-- info: Try this: exact Nat.add_comm x y -/
 #guard_msgs in
 example (x y : Nat) : x + y = y + x := by apply?
 
@@ -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 (np p).elim -/
+/-- info: Try this: exact False.elim (np p) -/
 #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 a.add_comm b -/
+/-- info: Try this: exact Nat.add_comm a b -/
 #guard_msgs in
 example (a b : Nat) : a + b = b + a :=
 by apply?
 
-/-- info: Try this: exact n.mul_sub_left_distrib m k -/
+/-- info: Try this: exact Nat.mul_sub_left_distrib n 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 (n.mul_sub_left_distrib m k).symm -/
+/-- info: Try this: exact Eq.symm (Nat.mul_sub_left_distrib n m k) -/
 #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 a.not_lt_zero -/
+/-- info: Try this: exact Nat.not_lt_zero a -/
 #guard_msgs in
 example (a : Nat) : ¬ (a < 0) := by apply?
-/-- info: Try this: exact a.not_succ_le_zero h -/
+/-- info: Try this: exact Nat.not_succ_le_zero a h -/
 #guard_msgs in
 example (a : Nat) (h : a < 0) : False := by apply?
 
@@ -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 n.add_comm m -/
+/-- info: Try this: exact Nat.add_comm n m -/
 #guard_msgs in
 example (_h : List.range 10000 = List.range 10000) (n m : Nat) : n + m = m + n := by
   with_reducible exact?

tests/lean/simpZetaFalse.lean.expected.out

@@ -9,12 +9,13 @@ theorem ex1 : ∀ (x : Nat),
       if f (f x) = x then 1 else y + 1) =
       1 :=
 fun x h =>
-  (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)))
+  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)))
 x z : Nat
 h : f (f x) = x
 h' : z = x
@@ -28,8 +29,8 @@ theorem ex2 : ∀ (x z : Nat),
         y) =
         z :=
 fun x z h h' =>
-  (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)))
+  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)))
 x z : Nat
 ⊢ (let α := Nat;
     fun x => 0 + x) =
@@ -45,5 +46,5 @@ theorem ex4 : ∀ (p : Prop),
       fun x => x = x) =
       fun z => p :=
 fun p h =>
-  (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)))
+  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)))