fix: remove irrelevant hypotheses in auto-generated equation theorems

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -70,13 +70,24 @@ private def keepGoing (mvarId : MVarId) : ReaderT Context (StateRefT (Array Expr
   let ctx ← read
   return Option.isSome <| rhs.find? fun e => ctx.declNames.any e.isAppOf && e.hasLooseBVars
 
+private def lhsDependsOn (type : Expr) (fvarId : FVarId) : MetaM Bool :=
+  forallTelescope type fun _ type => do
+    if let some (_, lhs, _) ← matchEq? type then
+      dependsOn lhs fvarId
+    else
+      dependsOn type fvarId
+
+/--
+  Eliminate `namedPatterns` from equation, and trivial hypotheses.
+-/
 def simpEqnType (eqnType : Expr) : MetaM Expr := do
   forallTelescopeReducing (← instantiateMVars eqnType) fun ys type => do
     let proofVars := collect type
-    trace[Meta.debug] "proofVars: {proofVars.toList.map mkFVar}"
+    trace[Meta.debug] "simpEqnType: {type}"
     let mut type ← Match.unfoldNamedPattern type
     let mut eliminated : FVarIdSet := {}
     for y in ys.reverse do
+      trace[Meta.debug] ">> simpEqnType: {← inferType y}, {type}"
       if proofVars.contains y.fvarId! then
         let some (_, Expr.fvar fvarId _, rhs) ← matchEq? (← inferType y) | throwError "unexpected hypothesis in altenative{indentExpr eqnType}"
         eliminated := eliminated.insert fvarId
@@ -85,6 +96,14 @@ def simpEqnType (eqnType : Expr) : MetaM Expr := do
         if (← dependsOn type y.fvarId!) then
           type ← mkForallFVars #[y] type
       else
+        if let some (_, lhs, rhs) ← matchEq? (← inferType y) then
+          if (← isDefEq lhs rhs) then
+            if !(← dependsOn type y.fvarId!) then
+              continue
+            else if !(← lhsDependsOn type y.fvarId!) then
+              -- Since the `lhs` of the `type` does not depend on `y`, we replace it with `Eq.refl` in the `rhs`
+              type := type.replaceFVar y (← mkEqRefl lhs)
+              continue
         type ← mkForallFVars #[y] type
     return type
 where

tests/lean/986.lean

@@ -0,0 +1,4 @@
+attribute [simp] Array.insertionSort.swapLoop
+
+#check @Array.insertionSort.swapLoop._eq_1
+#check @Array.insertionSort.swapLoop._eq_2

tests/lean/986.lean.expected.out

@@ -0,0 +1,11 @@
+@Array.insertionSort.swapLoop._eq_1 : ∀ {α : Type u_1} (lt : α → α → Bool) (a : Array α) (h : 0 < Array.size a),
+  Array.insertionSort.swapLoop lt a 0 h = a
+@Array.insertionSort.swapLoop._eq_2 : ∀ {α : 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 =
+    (fun h' =>
+        if lt (Array.get a { val := Nat.succ j', isLt := h }) (Array.get a { val := j', isLt := h' }) = true then
+          Array.insertionSort.swapLoop lt (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }) j'
+            (_ : j' < Array.size (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }))
+        else a)
+      (_ : j' < Array.size a)