From 3a4d2cded30beb3343ba0e13a3ddb2809703e26d Mon Sep 17 00:00:00 2001
From: Joachim Breitner <mail@joachim-breitner.de>
Date: Mon, 22 Jul 2024 13:56:50 +0200
Subject: [PATCH] refactor: Introduce PProdN module (#4807)

code to create nested `PProd`s, and project out, and related functions
were scattered in variuos places. This unifies them in
`Lean.Meta.PProdN`.

It also consistently avoids the terminal `True` or `PUnit`, for slightly
easier to read constructions.
---
 .../Elab/PreDefinition/Structural/BRecOn.lean |  19 ++-
 .../PreDefinition/Structural/FunPacker.lean   | 126 ---------------
 src/Lean/Meta/AppBuilder.lean                 |  21 ---
 src/Lean/Meta/ArgsPacker.lean                 |   5 +-
 src/Lean/Meta/Constructions/BRecOn.lean       |  79 ++--------
 src/Lean/Meta/PProdN.lean                     | 145 ++++++++++++++++++
 src/Lean/Meta/Tactic/FunInd.lean              |  30 +---
 tests/lean/run/letrecInProofs.lean            |  13 +-
 .../run/nestedInductiveConstructions.lean     |  47 +++---
 tests/lean/unusedLet.lean.expected.out        |   2 +-
 10 files changed, 201 insertions(+), 286 deletions(-)
 delete mode 100644 src/Lean/Elab/PreDefinition/Structural/FunPacker.lean
 create mode 100644 src/Lean/Meta/PProdN.lean

diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
index 96f742b747..4bb591844f 100644
--- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
+++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean
@@ -5,11 +5,11 @@ Authors: Leonardo de Moura, Joachim Breitner
 -/
 prelude
 import Lean.Util.HasConstCache
+import Lean.Meta.PProdN
 import Lean.Meta.Match.MatcherApp.Transform
 import Lean.Elab.RecAppSyntax
 import Lean.Elab.PreDefinition.Basic
 import Lean.Elab.PreDefinition.Structural.Basic
-import Lean.Elab.PreDefinition.Structural.FunPacker
 import Lean.Elab.PreDefinition.Structural.RecArgInfo
 
 namespace Lean.Elab.Structural
@@ -21,11 +21,11 @@ private def throwToBelowFailed : MetaM α :=
 partial def searchPProd (e : Expr) (F : Expr) (k : Expr → Expr → MetaM α) : MetaM α := do
   match (← whnf e) with
   | .app (.app (.const `PProd _) d1) d2 =>
-        (do searchPProd d1 (← mkAppM ``PProd.fst #[F]) k)
-    <|> (do searchPProd d2 (← mkAppM `PProd.snd #[F]) k)
+        (do searchPProd d1 (.proj ``PProd 0 F) k)
+    <|> (do searchPProd d2 (.proj ``PProd 1 F) k)
   | .app (.app (.const `And _) d1) d2 =>
-        (do searchPProd d1 (← mkAppM `And.left #[F]) k)
-    <|> (do searchPProd d2 (← mkAppM `And.right #[F]) k)
+        (do searchPProd d1 (.proj `And 0 F) k)
+    <|> (do searchPProd d2 (.proj `And 1 F) k)
   | .const `PUnit _
   | .const `True _ => throwToBelowFailed
   | _ => k e F
@@ -85,7 +85,7 @@ private def withBelowDict [Inhabited α] (below : Expr) (numIndParams : Nat)
         return ((← mkFreshUserName `C), fun _ => pure t)
     withLocalDeclsD CDecls fun Cs => do
       -- We have to pack these canary motives like we packed the real motives
-      let packedCs ← positions.mapMwith packMotives motiveTypes Cs
+      let packedCs ← positions.mapMwith PProdN.packLambdas motiveTypes Cs
       let belowDict := mkAppN pre packedCs
       let belowDict := mkAppN belowDict finalArgs
       trace[Elab.definition.structural] "initial belowDict for {Cs}:{indentExpr belowDict}"
@@ -250,7 +250,7 @@ def mkBRecOnConst (recArgInfos : Array RecArgInfo) (positions : Positions)
   let brecOnAux := brecOnCons 0
   -- Infer the type of the packed motive arguments
   let packedMotiveTypes ← inferArgumentTypesN indGroup.numMotives brecOnAux
-  let packedMotives ← positions.mapMwith packMotives packedMotiveTypes motives
+  let packedMotives ← positions.mapMwith PProdN.packLambdas packedMotiveTypes motives
 
   return fun n => mkAppN (brecOnCons n) packedMotives
 
@@ -289,12 +289,11 @@ def mkBrecOnApp (positions : Positions) (fnIdx : Nat) (brecOnConst : Nat → Exp
     let brecOn := brecOnConst recArgInfo.indIdx
     let brecOn := mkAppN brecOn indexMajorArgs
     let packedFTypes ← inferArgumentTypesN positions.size brecOn
-    let packedFArgs ← positions.mapMwith packFArgs packedFTypes FArgs
+    let packedFArgs ← positions.mapMwith PProdN.mkLambdas packedFTypes FArgs
     let brecOn := mkAppN brecOn packedFArgs
     let some poss := positions.find? (·.contains fnIdx)
       | throwError "mkBrecOnApp: Could not find {fnIdx} in {positions}"
-    let brecOn ← if poss.size = 1 then pure brecOn else
-      mkPProdProjN (poss.getIdx? fnIdx).get! brecOn
+    let brecOn ← PProdN.proj poss.size (poss.getIdx? fnIdx).get! brecOn
     mkLambdaFVars ys (mkAppN brecOn otherArgs)
 
 end Lean.Elab.Structural
diff --git a/src/Lean/Elab/PreDefinition/Structural/FunPacker.lean b/src/Lean/Elab/PreDefinition/Structural/FunPacker.lean
deleted file mode 100644
index 7ef1262313..0000000000
--- a/src/Lean/Elab/PreDefinition/Structural/FunPacker.lean
+++ /dev/null
@@ -1,126 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Joachim Breitner
--/
-prelude
-import Lean.Meta.InferType
-
-/-!
-This module contains the logic that packs the motives and FArgs of multiple functions into one,
-to allow structural mutual recursion where the number of functions is not exactly the same
-as the number of inductive data types in the mutual inductive group.
-
-The private helper functions related to `PProd` here should at some point be moved to their own
-module, so that they can be used elsewhere (e.g. `FunInd`), and possibly unified with the similar
-constructions for well-founded recursion (see `ArgsPacker` module).
--/
-
-namespace Lean.Elab.Structural
-open Meta
-
-private def mkPUnit : Level → Expr
-  | .zero => .const ``True []
-  | lvl   => .const ``PUnit [lvl]
-
-private def mkPProd (e1 e2 : Expr) : MetaM Expr := do
-  let lvl1 ← getLevel e1
-  let lvl2 ← getLevel e2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp2 (.const `And []) e1 e2
-  else
-    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
-
-private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnit lvl) mkPProd
-
-private def mkPUnitMk : Level → Expr
-  | .zero => .const ``True.intro []
-  | lvl   => .const ``PUnit.unit [lvl]
-
-private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
-  let t1 ← inferType e1
-  let t2 ← inferType e2
-  let lvl1 ← getLevel t1
-  let lvl2 ← getLevel t2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
-  else
-    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
-
-private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnitMk lvl) mkPProdMk
-
-/-- `PProd.fst` or `And.left` (as projections) -/
-private def mkPProdFst (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 0 e
-  | And _ _ =>   return .proj ``And 0 e
-  | _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- `PProd.snd` or `And.right` (as projections) -/
-private def mkPProdSnd (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 1 e
-  | And _ _ =>   return .proj ``And 1 e
-  | _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- Given a proof of `P₁ ∧ … ∧ Pᵢ ∧ … ∧ Pₙ ∧ True`, return the proof of `Pᵢ` -/
-def mkPProdProjN (i : Nat) (e : Expr) : MetaM Expr := do
-  let mut value := e
-  for _ in [:i] do
-      value ← mkPProdSnd value
-  value ← mkPProdFst value
-  return value
-
-/--
-Combines motives from different functions that recurse on the same parameter type into a single
-function returning a `PProd` type.
-
-For example
-```
-packMotives (Nat → Sort u) #[(fun (n : Nat) => Nat), (fun (n : Nat) => Fin n -> Fin n )]
-```
-will return
-```
-fun (n : Nat) (PProd Nat (Fin n → Fin n))
-```
-
-It is the identity if `motives.size = 1`.
-
-It returns a dummy motive `(xs : ) → PUnit` or `(xs : … ) → True` if no motive is given.
-(this is the reason we need the expected type in the `motiveType` parameter).
-
--/
-def packMotives (motiveType : Expr) (motives : Array Expr) : MetaM Expr := do
-  if motives.size = 1 then
-    return motives[0]!
-  trace[Elab.definition.structural] "packing Motives\nexpected: {motiveType}\nmotives: {motives}"
-  forallTelescope motiveType fun xs sort => do
-    unless sort.isSort do
-      throwError "packMotives: Unexpected motiveType {motiveType}"
-    -- NB: Use beta, not instantiateLambda; when constructing the belowDict below
-    -- we pass `C`, a plain FVar, here
-    let motives := motives.map (·.beta xs)
-    let packedMotives ← mkNProd sort.sortLevel! motives
-    mkLambdaFVars xs packedMotives
-
-/--
-Combines the F-args from different functions that recurse on the same parameter type into a single
-function returning a `PProd` value. See `packMotives`
-
-It is the identity if `motives.size = 1`.
--/
-def packFArgs (FArgType : Expr) (FArgs : Array Expr) : MetaM Expr := do
-  if FArgs.size = 1 then
-    return FArgs[0]!
-  forallTelescope FArgType fun xs body => do
-    let lvl ← getLevel body
-    let FArgs := FArgs.map (·.beta xs)
-    let packedFArgs ← mkNProdMk lvl FArgs
-    mkLambdaFVars xs packedFArgs
-
-
-end Lean.Elab.Structural
diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean
index 41a7ea2f1f..898b59abee 100644
--- a/src/Lean/Meta/AppBuilder.lean
+++ b/src/Lean/Meta/AppBuilder.lean
@@ -665,27 +665,6 @@ def mkIffOfEq (h : Expr) : MetaM Expr := do
   else
     mkAppM ``Iff.of_eq #[h]
 
-/--
-Given proofs of `P₁`, …, `Pₙ`, returns a proof of `P₁ ∧ … ∧ Pₙ`.
-If `n = 0` returns a proof of `True`.
-If `n = 1` returns the proof of `P₁`.
--/
-def mkAndIntroN : Array Expr → MetaM Expr
-| #[] => return mkConst ``True.intro []
-| #[e] => return e
-| es => es.foldrM (start := es.size - 1) (fun a b => mkAppM ``And.intro #[a,b]) es.back
-
-
-/-- Given a proof of `P₁ ∧ … ∧ Pᵢ ∧ … ∧ Pₙ`, return the proof of `Pᵢ` -/
-def mkProjAndN (n i : Nat) (e : Expr) : Expr := Id.run do
-  let mut value := e
-  for _ in [:i] do
-      value := mkProj ``And 1 value
-  if i + 1 < n then
-      value := mkProj ``And 0 value
-  return value
-
-
 builtin_initialize do
   registerTraceClass `Meta.appBuilder
   registerTraceClass `Meta.appBuilder.result (inherited := true)
diff --git a/src/Lean/Meta/ArgsPacker.lean b/src/Lean/Meta/ArgsPacker.lean
index d871e97c97..2b2b26d471 100644
--- a/src/Lean/Meta/ArgsPacker.lean
+++ b/src/Lean/Meta/ArgsPacker.lean
@@ -6,6 +6,7 @@ Authors: Joachim Breitner
 
 prelude
 import Lean.Meta.AppBuilder
+import Lean.Meta.PProdN
 import Lean.Meta.ArgsPacker.Basic
 
 /-!
@@ -518,7 +519,7 @@ def curry (argsPacker : ArgsPacker) (e : Expr) : MetaM Expr := do
   let mut es := #[]
   for i in [:argsPacker.numFuncs] do
     es := es.push (← argsPacker.curryProj e i)
-  mkAndIntroN es
+  PProdN.mk 0 es
 
 /--
 Given type `(a ⊗' b ⊕' c ⊗' d) → e`, brings `a → b → e` and `c → d → e`
@@ -533,7 +534,7 @@ where
   | [], acc => k acc
   | t::ts, acc => do
     let name := if argsPacker.numFuncs = 1 then name else .mkSimple s!"{name}{acc.size+1}"
-    withLocalDecl name .default t fun x => do
+    withLocalDeclD name t fun x => do
       go ts (acc.push x)
 
 /--
diff --git a/src/Lean/Meta/Constructions/BRecOn.lean b/src/Lean/Meta/Constructions/BRecOn.lean
index bee7244a54..52e4297d78 100644
--- a/src/Lean/Meta/Constructions/BRecOn.lean
+++ b/src/Lean/Meta/Constructions/BRecOn.lean
@@ -8,67 +8,18 @@ import Lean.Meta.InferType
 import Lean.AuxRecursor
 import Lean.AddDecl
 import Lean.Meta.CompletionName
+import Lean.Meta.PProdN
 
 namespace Lean
 open Meta
 
-section PProd
-
-/--!
-Helpers to construct types and values of `PProd` and project out of them, set up to use `And`
-instead of `PProd` if the universes allow. Maybe be extracted into a Utils module when useful
-elsewhere.
--/
-
-private def mkPUnit : Level → Expr
-  | .zero => .const ``True []
-  | lvl   => .const ``PUnit [lvl]
-
-private def mkPProd (e1 e2 : Expr) : MetaM Expr := do
-  let lvl1 ← getLevel e1
-  let lvl2 ← getLevel e2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp2 (.const `And []) e1 e2
-  else
-    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
-
-private def mkNProd (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnit lvl) mkPProd
-
-private def mkPUnitMk : Level → Expr
-  | .zero => .const ``True.intro []
-  | lvl   => .const ``PUnit.unit [lvl]
-
-private def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
-  let t1 ← inferType e1
-  let t2 ← inferType e2
-  let lvl1 ← getLevel t1
-  let lvl2 ← getLevel t2
-  if lvl1 matches .zero && lvl2 matches .zero then
-    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
-  else
-    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
-
-private def mkNProdMk (lvl : Level) (es : Array Expr) : MetaM Expr :=
-  es.foldrM (init := mkPUnitMk lvl) mkPProdMk
-
-/-- `PProd.fst` or `And.left` (as projections) -/
-private def mkPProdFst (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 0 e
-  | And _ _ =>   return .proj ``And 0 e
-  | _ => throwError "Cannot project .1 out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- `PProd.snd` or `And.right` (as projections) -/
-private def mkPProdSnd (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd _ _ => return .proj ``PProd 1 e
-  | And _ _ =>   return .proj ``And 1 e
-  | _ => throwError "Cannot project .2 out of{indentExpr e}\nof type{indentExpr t}"
-
-end PProd
+/-- Transforms `e : xᵢ → (t₁ ×' t₂)` into `(xᵢ → t₁) ×' (xᵢ → t₂) -/
+private def etaPProd (xs : Array Expr) (e : Expr) : MetaM Expr := do
+  if xs.isEmpty then return e
+  let r := mkAppN e xs
+  let r₁ ← mkLambdaFVars xs (← mkPProdFst r)
+  let r₂ ← mkLambdaFVars xs (← mkPProdSnd r)
+  mkPProdMk r₁ r₂
 
 /--
 If `minorType` is the type of a minor premies of a recursor, such as
@@ -91,7 +42,7 @@ private def buildBelowMinorPremise (rlvl : Level) (motives : Array Expr) (minorT
 where
   ibelow := rlvl matches .zero
   go (prods : Array Expr) : List Expr → MetaM Expr
-  | [] => mkNProd rlvl prods
+  | [] => PProdN.pack rlvl prods
   | arg::args => do
     let argType ← inferType arg
     forallTelescope argType fun arg_args arg_type => do
@@ -243,7 +194,7 @@ private def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr)
   forallTelescope minorType fun minor_args minor_type => do
     let rec go (prods : Array Expr) : List Expr → MetaM Expr
       | [] => minor_type.withApp fun minor_type_fn minor_type_args => do
-          let b ← mkNProdMk rlvl prods
+          let b ← PProdN.mk rlvl prods
           let .some ⟨idx, _⟩ := motives.indexOf? minor_type_fn
             | throwError m!"Did not find {minor_type} in {motives}"
           mkPProdMk (mkAppN fs[idx]! (minor_type_args.push b)) b
@@ -256,14 +207,8 @@ private def buildBRecOnMinorPremise (rlvl : Level) (motives : Array Expr)
               let type' ← mkForallFVars arg_args
                 (← mkPProd arg_type (mkAppN belows[idx]! arg_type_args) )
               withLocalDeclD name type' fun arg' => do
-                if arg_args.isEmpty then
-                  mkLambdaFVars #[arg'] (← go (prods.push arg') args)
-                else
-                  let r := mkAppN arg' arg_args
-                  let r₁ ← mkLambdaFVars arg_args (← mkPProdFst r)
-                  let r₂ ← mkLambdaFVars arg_args (← mkPProdSnd r)
-                  let r ← mkPProdMk r₁ r₂
-                  mkLambdaFVars #[arg'] (← go (prods.push r) args)
+                let r ← etaPProd arg_args arg'
+                mkLambdaFVars #[arg'] (← go (prods.push r) args)
             else
               mkLambdaFVars #[arg] (← go prods args)
     go #[] minor_args.toList
diff --git a/src/Lean/Meta/PProdN.lean b/src/Lean/Meta/PProdN.lean
new file mode 100644
index 0000000000..fcde4d4a46
--- /dev/null
+++ b/src/Lean/Meta/PProdN.lean
@@ -0,0 +1,145 @@
+/-
+Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joachim Breitner
+-/
+
+prelude
+import Lean.Meta.InferType
+
+/-!
+This module provides functios to pack and unpack values using nested `PProd` or `And`,
+as used in the `.below` construction, in the `.brecOn` construction for mutual recursion and
+and the `mutual_induct` construction.
+
+It uses `And` (equivalent to `PProd.{0}` when possible).
+
+The nesting is `t₁ ×' (t₂ ×' t₃)`, not `t₁ ×' (t₂ ×' (t₃ ×' PUnit))`. This is more readable,
+slightly shorter, and means that the packing is the identity if `n=1`, which we rely on in some
+places. It comes at the expense that hat projection needs to know `n`.
+
+Packing an empty list uses `True` or `PUnit` depending on the given `lvl`.
+
+Also see `Lean.Meta.ArgsPacker` for a similar module for `PSigma` and `PSum`, used by well-founded recursion.
+-/
+
+
+namespace Lean.Meta
+
+/-- Given types `t₁` and `t₂`, produces `t₁ ×' t₂` (or `t₁ ∧ t₂` if the universes allow) -/
+def mkPProd (e1 e2 : Expr) : MetaM Expr := do
+  let lvl1 ← getLevel e1
+  let lvl2 ← getLevel e2
+  if lvl1 matches .zero && lvl2 matches .zero then
+    return mkApp2 (.const `And []) e1 e2
+  else
+    return mkApp2 (.const ``PProd [lvl1, lvl2]) e1 e2
+
+/-- Given values of typs `t₁` and `t₂`, produces value of type `t₁ ×' t₂` (or `t₁ ∧ t₂` if the universes allow) -/
+def mkPProdMk (e1 e2 : Expr) : MetaM Expr := do
+  let t1 ← inferType e1
+  let t2 ← inferType e2
+  let lvl1 ← getLevel t1
+  let lvl2 ← getLevel t2
+  if lvl1 matches .zero && lvl2 matches .zero then
+    return mkApp4 (.const ``And.intro []) t1 t2 e1 e2
+  else
+    return mkApp4 (.const ``PProd.mk [lvl1, lvl2]) t1 t2 e1 e2
+
+/-- `PProd.fst` or `And.left` (using `.proj`) -/
+def mkPProdFst (e : Expr) : MetaM Expr := do
+  let t ← whnf (← inferType e)
+  match_expr t with
+  | PProd _ _ => return .proj ``PProd 0 e
+  | And _ _ => return .proj ``And 0 e
+  | _ => panic! "mkPProdFst: cannot handle{indentExpr e}\nof type{indentExpr t}"
+
+/-- `PProd.snd` or `And.right` (using `.proj`) -/
+def mkPProdSnd (e : Expr) : MetaM Expr := do
+  let t ← whnf (← inferType e)
+  match_expr t with
+  | PProd _ _ => return .proj ``PProd 1 e
+  | And _ _ => return .proj ``And 1 e
+  | _ => panic! "mkPProdSnd: cannot handle{indentExpr e}\nof type{indentExpr t}"
+
+
+
+namespace PProdN
+
+/-- Given types `tᵢ`, produces `t₁ ×' t₂ ×' t₃` -/
+def pack (lvl : Level) (xs : Array Expr) : MetaM Expr := do
+  if xs.size = 0 then
+    if lvl matches .zero then return .const ``True []
+                         else return .const ``PUnit [lvl]
+  let xBack := xs.back
+  xs.pop.foldrM mkPProd xBack
+
+/-- Given values `xᵢ` of type `tᵢ`, produces value of type `t₁ ×' t₂ ×' t₃` -/
+def mk (lvl : Level) (xs : Array Expr) : MetaM Expr := do
+  if xs.size = 0 then
+    if lvl matches .zero then return .const ``True.intro []
+                         else return .const ``PUnit.unit [lvl]
+  let xBack := xs.back
+  xs.pop.foldrM mkPProdMk xBack
+
+/-- Given a value of type `t₁ ×' … ×' tᵢ ×' … ×' tₙ`, return a value of type `tᵢ` -/
+def proj (n i : Nat) (e : Expr) : MetaM Expr := do
+  let mut value := e
+  for _ in [:i] do
+      value ← mkPProdSnd value
+  if i+1 < n then
+    mkPProdFst value
+  else
+    pure value
+
+
+
+/--
+Packs multiple type-forming lambda expressions taking the same parameters using `PProd`.
+
+The parameter `type` is the common type of the these expressions
+
+For example
+```
+packLambdas (Nat → Sort u) #[(fun (n : Nat) => Nat), (fun (n : Nat) => Fin n -> Fin n )]
+```
+will return
+```
+fun (n : Nat) => (Nat ×' (Fin n → Fin n))
+```
+
+It is the identity if `es.size = 1`.
+
+It returns a dummy motive `(xs : ) → PUnit` or `(xs : … ) → True` if no expressions are given.
+(this is the reason we need the expected type in the `type` parameter).
+
+-/
+def packLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do
+  if es.size = 1 then
+    return es[0]!
+  forallTelescope type fun xs sort => do
+    assert! sort.isSort
+    -- NB: Use beta, not instantiateLambda; when constructing the belowDict below
+    -- we pass `C`, a plain FVar, here
+    let es' := es.map (·.beta xs)
+    let packed ← PProdN.pack sort.sortLevel! es'
+    mkLambdaFVars xs packed
+
+/--
+The value analogue to `PProdN.packLambdas`.
+
+It is the identity if `es.size = 1`.
+-/
+def mkLambdas (type : Expr) (es : Array Expr) : MetaM Expr := do
+  if es.size = 1 then
+    return es[0]!
+  forallTelescope type fun xs body => do
+    let lvl ← getLevel body
+    let es' := es.map (·.beta xs)
+    let packed ← PProdN.mk lvl es'
+    mkLambdaFVars xs packed
+
+
+end PProdN
+
+end Lean.Meta
diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean
index e6eb1f96f5..d5f1ce3d66 100644
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -12,6 +12,7 @@ import Lean.Meta.Tactic.Cleanup
 import Lean.Meta.Tactic.Subst
 import Lean.Meta.Injective -- for elimOptParam
 import Lean.Meta.ArgsPacker
+import Lean.Meta.PProdN
 import Lean.Elab.PreDefinition.WF.Eqns
 import Lean.Elab.PreDefinition.Structural.Eqns
 import Lean.Elab.Command
@@ -188,21 +189,6 @@ def removeLamda {n} [MonadLiftT MetaM n] [MonadError n] [MonadNameGenerator n] [
   let b := b.instantiate1 (.fvar x)
   k x b
 
-/-- `PProd.fst` or `And.left` -/
-def mkFst (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd t₁ t₂ => return mkApp3 (.const ``PProd.fst t.getAppFn.constLevels!) t₁ t₂ e
-  | And t₁ t₂ => return mkApp3 (.const ``And.left []) t₁ t₂ e
-  | _ => throwError "Cannot project out of{indentExpr e}\nof type{indentExpr t}"
-
-/-- `PProd.snd` or `And.right` -/
-def mkSnd (e : Expr) : MetaM Expr := do
-  let t ← whnf (← inferType e)
-  match_expr t with
-  | PProd t₁ t₂ => return mkApp3 (.const ``PProd.snd t.getAppFn.constLevels!) t₁ t₂ e
-  | And t₁ t₂ => return mkApp3 (.const ``And.right []) t₁ t₂ e
-  | _ => throwError "Cannot project out of{indentExpr e}\nof type{indentExpr t}"
 
 /--
 A monad to help collecting inductive hypothesis.
@@ -310,7 +296,7 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
               forallBoundedTelescope altType (some 1) fun newIH' _goal' => do
                 let #[newIH'] := newIH' | unreachable!
                 let altIHs ← M.exec <| foldAndCollect oldIH' newIH'.fvarId! isRecCall alt
-                let altIH ← mkAndIntroN altIHs
+                let altIH ← PProdN.mk 0 altIHs
                 mkLambdaFVars #[newIH'] altIH)
           (onRemaining := fun _ => pure #[mkFVar newIH])
         let ihMatcherApp'' ← ihMatcherApp'.inferMatchType
@@ -328,11 +314,6 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
           (onRemaining := fun _ => pure #[])
         return matcherApp'.toExpr
 
-    -- These projections can be type changing, so re-infer their type arguments
-    match_expr e with
-    | PProd.fst _ _ e => mkFst (← foldAndCollect oldIH newIH isRecCall e)
-    | PProd.snd _ _ e => mkSnd (← foldAndCollect oldIH newIH isRecCall e)
-    | _ =>
 
     if e.getAppArgs.any (·.isFVarOf oldIH) then
       -- Sometimes Fix.lean abstracts over oldIH in a proof definition.
@@ -371,6 +352,10 @@ partial def foldAndCollect (oldIH newIH : FVarId) (isRecCall : Expr → Option E
     | .mdata m b =>
       pure <| .mdata m (← foldAndCollect oldIH newIH isRecCall b)
 
+    -- These projections can be type changing (to And), so re-infer their type arguments
+    | .proj ``PProd 0 e => mkPProdFst (← foldAndCollect oldIH newIH isRecCall e)
+    | .proj ``PProd 1 e => mkPProdSnd (← foldAndCollect oldIH newIH isRecCall e)
+
     | .proj t i e =>
       pure <| .proj t i (← foldAndCollect oldIH newIH isRecCall e)
 
@@ -690,7 +675,6 @@ def deriveUnaryInduction (name : Name) : MetaM Name := do
     { name := inductName, levelParams := us, type := eTyp, value := e' }
   return inductName
 
-
 /--
 In the type of `value`, reduces
 * Beta-redexes
@@ -806,7 +790,7 @@ def deriveUnpackedInduction (eqnInfo : WF.EqnInfo) (unaryInductName : Name): Met
       let value ← forallTelescope ci.type fun xs _body => do
         let value := .const ci.name (levelParams.map mkLevelParam)
         let value := mkAppN value xs
-        let value := mkProjAndN eqnInfo.declNames.size idx value
+        let value ← PProdN.proj eqnInfo.declNames.size idx value
         mkLambdaFVars xs value
       let type ← inferType value
       addDecl <| Declaration.thmDecl { name := inductName, levelParams, type, value }
diff --git a/tests/lean/run/letrecInProofs.lean b/tests/lean/run/letrecInProofs.lean
index 853b9f821a..8f8c0aa92e 100644
--- a/tests/lean/run/letrecInProofs.lean
+++ b/tests/lean/run/letrecInProofs.lean
@@ -19,7 +19,7 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
       have ihl : x ≮ l → node s x ≠ l ∧ node s x ≮ l := right x s l
       have ihr : x ≮ r → node s x ≠ r ∧ node s x ≮ r := right x s r
       have hl : x ≠ l ∧ x ≮ l := h.1
-      have hr : x ≠ r ∧ x ≮ r := h.2.1
+      have hr : x ≠ r ∧ x ≮ r := h.2
       have ihl : node s x ≠ l ∧ node s x ≮ l := ihl hl.2
       have ihr : node s x ≠ r ∧ node s x ≮ r := ihr hr.2
       apply And.intro
@@ -31,7 +31,6 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
       focus
         apply And.intro
         apply ihl
-        apply And.intro _ trivial
         apply ihr
   let rec left (x t : Tree) (b : Tree) (h : x ≮ b) : node x t ≠ b ∧ node x t ≮ b := by
     match b, h with
@@ -42,7 +41,7 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
       have ihl : x ≮ l → node x t ≠ l ∧ node x t ≮ l := left x t l
       have ihr : x ≮ r → node x t ≠ r ∧ node x t ≮ r := left x t r
       have hl : x ≠ l ∧ x ≮ l := h.1
-      have hr : x ≠ r ∧ x ≮ r := h.2.1
+      have hr : x ≠ r ∧ x ≮ r := h.2
       have ihl : node x t ≠ l ∧ node x t ≮ l := ihl hl.2
       have ihr : node x t ≠ r ∧ node x t ≮ r := ihr hr.2
       apply And.intro
@@ -54,19 +53,17 @@ theorem Tree.acyclic (x t : Tree) : x = t → x ≮ t := by
       focus
         apply And.intro
         apply ihl
-        apply And.intro _ trivial
         apply ihr
   let rec aux : (x : Tree) → x ≮ x
     | leaf     => trivial
     | node l r => by
         have ih₁ : l ≮ l := aux l
         have ih₂ : r ≮ r := aux r
-        show (node l r ≠ l ∧ node l r ≮ l) ∧ (node l r ≠ r ∧ node l r ≮ r) ∧ True
+        show (node l r ≠ l ∧ node l r ≮ l) ∧ (node l r ≠ r ∧ node l r ≮ r)
         apply And.intro
         focus
           apply left
           assumption
-        apply And.intro _ trivial
         focus
           apply right
           assumption
@@ -78,7 +75,7 @@ open Tree
 
 theorem ex1 (x : Tree) : x ≠ node leaf (node x leaf) := by
   intro h
-  exact absurd rfl $ Tree.acyclic _ _ h |>.2.1.2.1.1
+  exact absurd rfl $ Tree.acyclic _ _ h |>.2.2.1.1
 
 theorem ex2 (x : Tree) : x ≠ node x leaf := by
   intro h
@@ -86,4 +83,4 @@ theorem ex2 (x : Tree) : x ≠ node x leaf := by
 
 theorem ex3 (x y : Tree) : x ≠ node y x := by
   intro h
-  exact absurd rfl $ Tree.acyclic _ _ h |>.2.1.1
+  exact absurd rfl $ Tree.acyclic _ _ h |>.2.1
diff --git a/tests/lean/run/nestedInductiveConstructions.lean b/tests/lean/run/nestedInductiveConstructions.lean
index 6b51c1067e..e1d1ab8c41 100644
--- a/tests/lean/run/nestedInductiveConstructions.lean
+++ b/tests/lean/run/nestedInductiveConstructions.lean
@@ -12,11 +12,10 @@ inductive Tree where | node  : List Tree → Tree
 info: @[reducible] protected def Ex1.Tree.below.{u} : {motive_1 : Tree → Sort u} →
   {motive_2 : List.{0} Tree → Sort u} → Tree → Sort (max 1 u) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec.{(max 1 u) + 1}
-    (fun a a_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}) PUnit.{max 1 u}
+  Tree.rec.{(max 1 u) + 1} (fun a a_ih => PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -26,11 +25,10 @@ fun {motive_1} {motive_2} t =>
 info: @[reducible] protected def Ex1.Tree.below_1.{u} : {motive_1 : Tree → Sort u} →
   {motive_2 : List.{0} Tree → Sort u} → List.{0} Tree → Sort (max 1 u) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec_1.{(max 1 u) + 1}
-    (fun a a_ih => PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}) PUnit.{max 1 u}
+  Tree.rec_1.{(max 1 u) + 1} (fun a a_ih => PProd.{u, max 1 u} (motive_2 a) a_ih) PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -40,8 +38,8 @@ fun {motive_1} {motive_2} t =>
 info: @[reducible] protected def Ex1.Tree.ibelow_1 : {motive_1 : Tree → Prop} →
   {motive_2 : List.{0} Tree → Prop} → List.{0} Tree → Prop :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec_1.{1} (fun a a_ih => And (And (motive_2 a) a_ih) True) True
-    (fun head tail head_ih tail_ih => And (And (motive_1 head) head_ih) (And (And (motive_2 tail) tail_ih) True)) t
+  Tree.rec_1.{1} (fun a a_ih => And (motive_2 a) a_ih) True
+    (fun head tail head_ih tail_ih => And (And (motive_1 head) head_ih) (And (motive_2 tail) tail_ih)) t
 -/
 #guard_msgs in
 #print Tree.ibelow_1
@@ -82,16 +80,15 @@ info: @[reducible] protected def Ex2.Tree.below.{u} : {motive_1 : Tree → Sort
 fun {motive_1} {motive_2} {motive_3} t =>
   Tree.rec.{(max 1 u) + 1}
     (fun a a_1 a_ih a_ih_1 =>
-      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u}))
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1))
     PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
     PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_3 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -104,16 +101,15 @@ info: @[reducible] protected def Ex2.Tree.below_1.{u} : {motive_1 : Tree → Sor
 fun {motive_1} {motive_2} {motive_3} t =>
   Tree.rec_1.{(max 1 u) + 1}
     (fun a a_1 a_ih a_ih_1 =>
-      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u}))
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1))
     PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
     PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_3 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -126,16 +122,15 @@ info: @[reducible] protected def Ex2.Tree.below_2.{u} : {motive_1 : Tree → Sor
 fun {motive_1} {motive_2} {motive_3} t =>
   Tree.rec_2.{(max 1 u) + 1}
     (fun a a_1 a_ih a_ih_1 =>
-      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1) PUnit.{max 1 u}))
+      PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 a) a_ih) (PProd.{u, max 1 u} (motive_3 a_1) a_ih_1))
     PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_2 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_2 tail) tail_ih))
     PUnit.{max 1 u}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_1 head) head_ih)
-        (PProd.{max 1 u, max 1 u} (PProd.{u, max 1 u} (motive_3 tail) tail_ih) PUnit.{max 1 u}))
+        (PProd.{u, max 1 u} (motive_3 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -169,12 +164,10 @@ inductive Tree : Type u where | node : List Tree → Tree
 info: @[reducible] protected def Ex3.Tree.below.{u_1, u} : {motive_1 : Tree.{u} → Sort u_1} →
   {motive_2 : List.{u} Tree.{u} → Sort u_1} → Tree.{u} → Sort (max 1 u_1) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec.{(max 1 u_1) + 1, u}
-    (fun a a_ih => PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1})
-    PUnit.{max 1 u_1}
+  Tree.rec.{(max 1 u_1) + 1, u} (fun a a_ih => PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_1 head) head_ih)
-        (PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih) PUnit.{max 1 u_1}))
+        (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih))
     t
 -/
 #guard_msgs in
@@ -184,12 +177,10 @@ fun {motive_1} {motive_2} t =>
 info: @[reducible] protected def Ex3.Tree.below_1.{u_1, u} : {motive_1 : Tree.{u} → Sort u_1} →
   {motive_2 : List.{u} Tree.{u} → Sort u_1} → List.{u} Tree.{u} → Sort (max 1 u_1) :=
 fun {motive_1} {motive_2} t =>
-  Tree.rec_1.{(max 1 u_1) + 1, u}
-    (fun a a_ih => PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1})
-    PUnit.{max 1 u_1}
+  Tree.rec_1.{(max 1 u_1) + 1, u} (fun a a_ih => PProd.{u_1, max 1 u_1} (motive_2 a) a_ih) PUnit.{max 1 u_1}
     (fun head tail head_ih tail_ih =>
       PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_1 head) head_ih)
-        (PProd.{max 1 u_1, max 1 u_1} (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih) PUnit.{max 1 u_1}))
+        (PProd.{u_1, max 1 u_1} (motive_2 tail) tail_ih))
     t
 -/
 #guard_msgs in
diff --git a/tests/lean/unusedLet.lean.expected.out b/tests/lean/unusedLet.lean.expected.out
index c33c68f746..7408d3dcc9 100644
--- a/tests/lean/unusedLet.lean.expected.out
+++ b/tests/lean/unusedLet.lean.expected.out
@@ -8,5 +8,5 @@ fun x =>
       | 0 => fun x => 1
       | n.succ => fun x =>
         let y := 42;
-        2 * x.fst.fst)
+        2 * x.1.1)
       f