feat(Tactic/Simproc): support Prop-valued dependent quantifiers in existsAndEq

[vasnesterov]

Search for equality a = a' inside P : Prop in ∃ h : P, Q h. The latter proposition can be seen as a dependent conjunction (h : P) ∧ Q h so this is a direct generalization of what the simproc was already doing before.

It was requested in Zulip: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/potential.20simp_procs/near/617574483

---

• depends on: chore(Tactic/Simproc/ExistsAndEq): simplify proof building using subst #43162 [optional extra text]

[vasnesterov]

!bench

[leanprover-radar]

Benchmark results for 47b3ce2 against ffbfefa are in. No significant results found. @vasnesterov

• 🟥 build//instructions: +34.1G (+0.02%)

Small changes (1✅, 1🟥)

• 🟥 build/module/Mathlib.Algebra.Order.Hom.Lattice//instructions: +134.7M (+3.85%)
• ✅ build/module/Mathlib.Tactic.Simproc.ExistsAndEq//instructions: -561.0M (-5.87%)

[github-actions]

PR summary 2c721f5e81

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ Path.forResult
+ eqDetermines
+ existsAndEqCore
+ mkAfterToBefore
+ mkBeforeToAfter
+ withMVarsAsFVars
- assertUnreachable
- withExistsElimAlongPath
- withNestedExistsElim
- withNestedExistsIntro

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 2c721f5).

• +19 new declarations
• −10 removed declarations

+ExistsAndEq.GoTo.andLeft
+ExistsAndEq.GoTo.andLeft.elim
+ExistsAndEq.GoTo.andLeft.sizeOf_spec
+ExistsAndEq.GoTo.andRight
+ExistsAndEq.GoTo.andRight.elim
+ExistsAndEq.GoTo.andRight.sizeOf_spec
+ExistsAndEq.GoTo.existsBody
+ExistsAndEq.GoTo.existsBody.elim
+ExistsAndEq.GoTo.existsBody.sizeOf_spec
+ExistsAndEq.GoTo.existsType
+ExistsAndEq.GoTo.existsType.elim
+ExistsAndEq.GoTo.existsType.sizeOf_spec
-ExistsAndEq.GoTo.left
-ExistsAndEq.GoTo.left.elim
-ExistsAndEq.GoTo.left.sizeOf_spec
-ExistsAndEq.GoTo.right
-ExistsAndEq.GoTo.right.elim
-ExistsAndEq.GoTo.right.sizeOf_spec
+ExistsAndEq.Path.forResult
+ExistsAndEq.construct
+ExistsAndEq.destruct
+ExistsAndEq.eqDetermines
+ExistsAndEq.existsAndEqCore
+ExistsAndEq.proveFromHoisted
-ExistsAndEq.withExistsElimAlongPath
-ExistsAndEq.withExistsElimAlongPathImp
+ExistsAndEq.withMVarsAsFVars
-ExistsAndEq.withNestedExistsElim
-ExistsAndEq.withNestedExistsIntro

---

No changes to strong technical debt.
No changes to weak technical debt.

Current commit 2c721f5e81
Reference commit b9d865b99b

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[vasnesterov]

!bench

[leanprover-radar]

Benchmark results for f6c9e05 against d9f6d18 are in. No significant results found. @vasnesterov

• 🟥 build//instructions: +36.8G (+0.03%)

Small changes (2✅, 1🟥)

• ✅ build/module/Mathlib.Algebra.Order.Group.Abs//instructions: -95.5M (-0.78%)
• ✅ build/module/Mathlib.Combinatorics.Additive.Dissociation//instructions: -222.3M (-2.18%)
• 🟥 build/module/Mathlib.Tactic.Simproc.ExistsAndEq//instructions: +317.3M (+3.29%)

[vasnesterov]

!bench

[leanprover-radar]

Benchmark results for c881a3d against b9d865b are in. No significant results found. @vasnesterov

• ✅ build//instructions: -31.2G (-0.02%)

Small changes (3✅, 2🟥)

• ✅ build/module/Mathlib.Algebra.Order.Group.Abs//instructions: -93.6M (-0.77%)
• ✅ build/module/Mathlib.Combinatorics.Additive.Dissociation//instructions: -230.0M (-2.26%)
• 🟥 build/module/Mathlib.Combinatorics.SimpleGraph.Walks.Operations//instructions: +108.4M (+3.68%)
• ✅ build/module/Mathlib.RingTheory.Ideal.Quotient.Nilpotent//instructions: -282.8M (-3.20%)
• 🟥 build/module/Mathlib.Tactic.Simproc.ExistsAndEq//instructions: +282.0M (+2.93%)

[mathlib-dependent-issues]

This PR/issue depends on:

• chore(Tactic/Simproc/ExistsAndEq): simplify proof building using subst #43162
  By Dependent Issues (🤖). Happy coding!