fix: PProdN.reduceProjs to also look for projection functions (#9464)

This PR makes `PProdN.reduceProjs` also look for projection functions.
Previously, all redexes were created by the functions in `PProdN`, which
used primitive projections. But with `mkAdmProj` the projection
functions creep in via the types of the `admissible_pprod_fst` theorem.
So let's just reduce both of them.

Fixes #9462.

src/Lean/Meta/PProdN.lean

@@ -182,18 +182,29 @@ def stripProjs (e : Expr) : Expr :=
   | e => e
 
 /--
-Reduces `⟨x,y⟩.1` redexes for `PProd` and `And`
+Reduces `⟨x,y⟩.1` or `⟨x,y⟩.fst` redexes for `PProd` and `And`
 -/
-def reduceProjs (e : Expr) : CoreM Expr := do
+def reduceProjs (e : Expr) : MetaM Expr := do
   Core.transform e (post := fun e => do
-    if e.isProj then
-      if e.projExpr!.isAppOfArity ``PProd.mk 4 || e.projExpr!.isAppOfArity ``And.intro 2 then
-        if e.projIdx! == 0 then
-          return .continue e.projExpr!.appFn!.appArg!
+    match_expr e with
+    | PProd.fst _ _ e' => reduce e' 0
+    | And.left _ _ e'  => reduce e' 0
+    | PProd.snd _ _ e' => reduce e' 1
+    | And.right _ _ e' => reduce e' 1
+    | _ =>
+        if e.isProj then
+          reduce e.projExpr! e.projIdx!
         else
-          return .continue e.projExpr!.appArg!
-    return .continue
+          return .continue
   )
+where
+  reduce (e : Expr) (i : Nat) : MetaM TransformStep := do
+    if e.isAppOfArity ``PProd.mk 4 || e.isAppOfArity ``And.intro 2 then
+      if i = 0 then
+        return .continue e.appFn!.appArg!
+      else
+        return .continue e.appArg!
+    return .continue
 
 end PProdN
 

tests/lean/run/issue9462.lean

@@ -0,0 +1,31 @@
+mutual
+def a : Nat := b
+partial_fixpoint
+def b : Nat := a
+partial_fixpoint
+end
+
+
+/--
+info: a.fixpoint_induct (motive_1 motive_2 : Nat → Prop) (adm_1 : Lean.Order.admissible motive_1)
+  (adm_2 : Lean.Order.admissible motive_2) (h_1 : ∀ (b : Nat), motive_2 b → motive_1 b)
+  (h_2 : ∀ (a : Nat), motive_1 a → motive_2 a) : motive_1 a ∧ motive_2 b
+-/
+#guard_msgs(pass trace, all) in
+#check a.fixpoint_induct
+
+
+mutual
+def c (n : Nat) : Nat := d (n + 1)
+partial_fixpoint
+def d (n : Nat) : Nat := c (n + 2)
+partial_fixpoint
+end
+
+/--
+info: c.fixpoint_induct (motive_1 motive_2 : (Nat → Nat) → Prop) (adm_1 : Lean.Order.admissible motive_1)
+  (adm_2 : Lean.Order.admissible motive_2) (h_1 : ∀ (d : Nat → Nat), motive_2 d → motive_1 fun n => d (n + 1))
+  (h_2 : ∀ (c : Nat → Nat), motive_1 c → motive_2 fun n => c (n + 2)) : motive_1 c ∧ motive_2 d
+-/
+#guard_msgs(pass trace, all) in
+#check c.fixpoint_induct