From 8fa82e8a92971c0c5cd842af3d348a79938e427c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 9 Sep 2026 12:11:14 +0200
Subject: [PATCH 1/8] =?UTF-8?q?feat(Tactic/Positivity):=20cover=20`Finset.?=
 =?UTF-8?q?sum=5Fpos'`=20with=20the=20`Finset.sum`=20extension=20To=20prov?=
 =?UTF-8?q?e=20`0=20<=20=E2=88=91=20a=20=E2=88=88=20s,=20f=20a`,=20the=20`?=
 =?UTF-8?q?positivity`=20extension=20now=20also=20searches=20through=20ass?=
 =?UTF-8?q?umptions=20of=20the=20form=20`a=20=E2=88=88=20s`=20and=20for=20?=
 =?UTF-8?q?each=20of=20them=20tries=20to=20prove=20`0=20<=20f=20a`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Will be used in convexity theory.

Generated by Claude Opus

Assisted-by: Claude Opus 5
---
 Mathlib/Tactic/Positivity/Finset.lean | 55 ++++++++++++++++++++++-----
 1 file changed, 45 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Tactic/Positivity/Finset.lean b/Mathlib/Tactic/Positivity/Finset.lean
index 139070a33db6d9..10be963c5c5d56 100644
--- a/Mathlib/Tactic/Positivity/Finset.lean
+++ b/Mathlib/Tactic/Positivity/Finset.lean
@@ -61,8 +61,9 @@ meta def evalFinsetDens : PositivityExt where eval {u 𝕜} _ pα? e :=
   | _, _, _ => throwError "not Finset.dens"
 
 attribute [local instance] monadLiftOptionMetaM in
-/-- The `positivity` extension which proves that `∑ i ∈ s, f i` is nonnegative if `f` is, and
-positive if each `f i` is and `s` is nonempty.
+/-- The `positivity` extension which proves that `∑ a ∈ s, f a` is nonnegative if `f` is, and
+positive if either each `f i` is and `s` is nonempty, or some `f a` is where `a ∈ s` is an
+assumption.
 
 TODO: The following example does not work
 ```
@@ -88,17 +89,38 @@ meta def evalFinsetSum : PositivityExt where eval {u α} zα pα? e :=
       let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody
       pure <| some q(@sum_pos $ι $α $instα (@PartialOrder.toPreorder _ $pα) $pα' $f $s _
         (fun i _ ↦ $pr i) $ps)
-    -- Try to show that the sum is positive
+    -- Try to show that the sum is positive because all summands are
     if let some p_pos := p_pos then
       return .positive p_pos
+    let pbody ← rbody.toNonneg
+    let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody
+    -- Else try to show that the sum is positive because one summand is. We look for the witness
+    -- among the assumptions of the form `a ∈ s`, since we have no other way of getting hold of an
+    -- element of `s` at which `f` might be positive.
+    let p_pos' : Option Q(0 < $e) ← do
+      let .some pα' ← trySynthInstanceQ q(IsOrderedCancelAddMonoid $α) | pure none
+      let mut res : Option Q(0 < $e) := none
+      for ldecl in ← getLCtx do
+        if res.isSome then break
+        if ldecl.isImplementationDetail then continue
+        let_expr Membership.mem _ _ _ s' a := ldecl.type | continue
+        unless ← withNewMCtxDepth (isDefEq s' s) do continue
+        have a : Q($ι) := a
+        have hmem : Q($a ∈ $s) := ldecl.toExpr
+        have fa : Q($α) := .betaRev f #[a]
+        let .positive pa ← catchNone (core zα pα fa) | continue
+        have pa : Q(0 < $f $a) := pa
+        assertInstancesCommute
+        res := some q(@sum_pos' $ι $α $instα (@PartialOrder.toPreorder _ $pα) $pα' $f $s _
+          (fun i _ ↦ $pr i) ⟨$a, $hmem, $pa⟩)
+      pure res
+    if let some p_pos' := p_pos' then
+      return .positive p_pos'
     -- Fall back to showing that the sum is nonnegative
-    else
-      let pbody ← rbody.toNonneg
-      let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody
-      let pα' ← synthInstanceQ q(AddLeftMono $α)
-      assertInstancesCommute
-      return .nonnegative q(@sum_nonneg $ι $α $instα (@PartialOrder.toPreorder _ $pα) $f $s $pα'
-        fun i _ ↦ $pr i)
+    let pα' ← synthInstanceQ q(AddLeftMono $α)
+    assertInstancesCommute
+    return .nonnegative q(@sum_nonneg $ι $α $instα (@PartialOrder.toPreorder _ $pα) $f $s $pα'
+      fun i _ ↦ $pr i)
   | _ => throwError "not Finset.sum"
 
 variable {α : Type*} {s : Finset α}
@@ -117,6 +139,19 @@ example [Nonempty α] : 0 < Fintype.card α := by positivity
 example [Nonempty α] : 0 < dens (univ : Finset α) := by positivity
 example [Nonempty α] : dens (univ : Finset α) ≠ 0 := by positivity
 
+example {f : α → ℕ} : 0 ≤ ∑ a ∈ s, f a := by positivity
+example {f : α → ℕ} (hs : s.Nonempty) : 0 < ∑ i ∈ s, (f i + 1) := by positivity
+example {f : α → ℕ} {a : α} (ha : a ∈ s) (hfa : 0 < f a) : 0 < ∑ a ∈ s, f a := by positivity
+example {f : α → ℕ} {a : α} (ha : a ∈ s) (hfa : f a ≠ 0) : ∑ a ∈ s, f a ≠ 0 := by positivity
+-- `f` need not be positive at the witness `a`, in which case we only get nonnegativity
+example {f : α → ℕ} {a : α} (_ha : a ∈ s) : 0 ≤ ∑ a ∈ s, f a := by positivity
+
+-- Extra `_ ∈ s` assumptions do not throw off `positivity`
+example {f : α → ℕ} {a b : α} (_ha : a ∈ s) (hb : b ∈ s) (hb : 0 < f b) : 0 < ∑ a ∈ s, f a := by
+  positivity
+example {f : α → ℕ} {a b : α} (ha : a ∈ s) (_hb : b ∈ s) (hfa : 0 < f a) : 0 < ∑ a ∈ s, f a := by
+  positivity
+
 example {G : Type*} {A : Finset G} :
     let f := fun _ : G ↦ 1; (∀ s, f s ^ 2 = 1) → 0 ≤ #A := by
   intros

From fa3701416dae0899fdfebd044e45c46981145634 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 9 Sep 2026 16:07:59 +0200
Subject: [PATCH 2/8] returh

---
 Mathlib/Tactic/Positivity/Finset.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Tactic/Positivity/Finset.lean b/Mathlib/Tactic/Positivity/Finset.lean
index 10be963c5c5d56..c793d42edb3c2c 100644
--- a/Mathlib/Tactic/Positivity/Finset.lean
+++ b/Mathlib/Tactic/Positivity/Finset.lean
@@ -97,11 +97,9 @@ meta def evalFinsetSum : PositivityExt where eval {u α} zα pα? e :=
     -- Else try to show that the sum is positive because one summand is. We look for the witness
     -- among the assumptions of the form `a ∈ s`, since we have no other way of getting hold of an
     -- element of `s` at which `f` might be positive.
-    let p_pos' : Option Q(0 < $e) ← do
+    let p_pos' : Option Q(0 < $e) ← (do
       let .some pα' ← trySynthInstanceQ q(IsOrderedCancelAddMonoid $α) | pure none
-      let mut res : Option Q(0 < $e) := none
       for ldecl in ← getLCtx do
-        if res.isSome then break
         if ldecl.isImplementationDetail then continue
         let_expr Membership.mem _ _ _ s' a := ldecl.type | continue
         unless ← withNewMCtxDepth (isDefEq s' s) do continue
@@ -109,11 +107,10 @@ meta def evalFinsetSum : PositivityExt where eval {u α} zα pα? e :=
         have hmem : Q($a ∈ $s) := ldecl.toExpr
         have fa : Q($α) := .betaRev f #[a]
         let .positive pa ← catchNone (core zα pα fa) | continue
-        have pa : Q(0 < $f $a) := pa
         assertInstancesCommute
-        res := some q(@sum_pos' $ι $α $instα (@PartialOrder.toPreorder _ $pα) $pα' $f $s _
+        return some q(@sum_pos' $ι $α $instα (@PartialOrder.toPreorder _ $pα) $pα' $f $s _
           (fun i _ ↦ $pr i) ⟨$a, $hmem, $pa⟩)
-      pure res
+      return none)
     if let some p_pos' := p_pos' then
       return .positive p_pos'
     -- Fall back to showing that the sum is nonnegative

From a2ceaf3465005642c75cbc3b2f82b855713dc65d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 9 Sep 2026 16:10:38 +0200
Subject: [PATCH 3/8] fix

---
 Mathlib/Tactic/Positivity/Finset.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/Tactic/Positivity/Finset.lean b/Mathlib/Tactic/Positivity/Finset.lean
index c793d42edb3c2c..3d741d77d5cbe2 100644
--- a/Mathlib/Tactic/Positivity/Finset.lean
+++ b/Mathlib/Tactic/Positivity/Finset.lean
@@ -107,6 +107,7 @@ meta def evalFinsetSum : PositivityExt where eval {u α} zα pα? e :=
         have hmem : Q($a ∈ $s) := ldecl.toExpr
         have fa : Q($α) := .betaRev f #[a]
         let .positive pa ← catchNone (core zα pα fa) | continue
+        have pa : Q(0 < $f $a) := pa
         assertInstancesCommute
         return some q(@sum_pos' $ι $α $instα (@PartialOrder.toPreorder _ $pα) $pα' $f $s _
           (fun i _ ↦ $pr i) ⟨$a, $hmem, $pa⟩)

From eb7ea102158c1f01843d6b812671702572ea96f7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 9 Sep 2026 17:13:43 +0200
Subject: [PATCH 4/8] use Qq more

---
 Mathlib/Tactic/Positivity/Finset.lean | 20 ++++++++++++++------
 Mathlib/Util/Qq.lean                  |  7 +++++++
 2 files changed, 21 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Tactic/Positivity/Finset.lean b/Mathlib/Tactic/Positivity/Finset.lean
index 3d741d77d5cbe2..8551bc3a48cdad 100644
--- a/Mathlib/Tactic/Positivity/Finset.lean
+++ b/Mathlib/Tactic/Positivity/Finset.lean
@@ -60,6 +60,15 @@ meta def evalFinsetDens : PositivityExt where eval {u 𝕜} _ pα? e :=
     return .positive q(@Nonempty.dens_pos $α $instα $s $ps)
   | _, _, _ => throwError "not Finset.dens"
 
+private meta def findMemFinset {u : Level} {α : Q(Type u)} (s : Q(Finset $α)) (p : Q(Prop))
+    (e : Q($p)) :
+    MetaM <| Option <| (a : Q($α)) × Q($a ∈ $s) := withNewMCtxDepth do
+  let m ← mkFreshExprMVarQ q($α)
+  let .defEq _ ← isDefEqQ q($p) q($m ∈ $s) | return none
+  let ⟨m, _⟩ ← instantiateMVarsQ' q($m)
+  let ⟨e, _⟩ ← instantiateMVarsQ' q($e)
+  return some ⟨q($m), q($e)⟩
+
 attribute [local instance] monadLiftOptionMetaM in
 /-- The `positivity` extension which proves that `∑ a ∈ s, f a` is nonnegative if `f` is, and
 positive if either each `f i` is and `s` is nonempty, or some `f a` is where `a ∈ s` is an
@@ -101,16 +110,15 @@ meta def evalFinsetSum : PositivityExt where eval {u α} zα pα? e :=
       let .some pα' ← trySynthInstanceQ q(IsOrderedCancelAddMonoid $α) | pure none
       for ldecl in ← getLCtx do
         if ldecl.isImplementationDetail then continue
-        let_expr Membership.mem _ _ _ s' a := ldecl.type | continue
-        unless ← withNewMCtxDepth (isDefEq s' s) do continue
-        have a : Q($ι) := a
-        have hmem : Q($a ∈ $s) := ldecl.toExpr
+        unless ← Meta.isProp ldecl.type do continue
+        let .some ⟨a, ha⟩ ← findMemFinset q($s) ldecl.type ldecl.toExpr | continue
         have fa : Q($α) := .betaRev f #[a]
+        let fa ← instantiateMVarsQ q($fa)
+        let : $fa =Q $f $a := ⟨⟩
         let .positive pa ← catchNone (core zα pα fa) | continue
-        have pa : Q(0 < $f $a) := pa
         assertInstancesCommute
         return some q(@sum_pos' $ι $α $instα (@PartialOrder.toPreorder _ $pα) $pα' $f $s _
-          (fun i _ ↦ $pr i) ⟨$a, $hmem, $pa⟩)
+          (fun i _ ↦ $pr i) ⟨$a, $ha, $pa⟩)
       return none)
     if let some p_pos' := p_pos' then
       return .positive p_pos'
diff --git a/Mathlib/Util/Qq.lean b/Mathlib/Util/Qq.lean
index 1e5e45be9bc682..8b8d133feb5a36 100644
--- a/Mathlib/Util/Qq.lean
+++ b/Mathlib/Util/Qq.lean
@@ -87,4 +87,11 @@ def mkNatLitQ (n : Nat) : Q(Nat) := mkNatLit n
 This is a Qq version of `Lean.mkIntLit`. -/
 def mkIntLitQ (n : Int) : Q(Int) := mkIntLit n
 
+/-- Version of `instantiateMVarsQ` that returns the Qq-fact that the new expression is equal to the
+previous one. -/
+def instantiateMVarsQ' {u : Level} {α : Q(Sort u)} (e : Q($α)) :
+    MetaM <| (e' : Q($α)) ×' ($e' =Q $e) := do
+  let e' ← instantiateMVars e
+  return ⟨e', ⟨⟩⟩
+
 end Qq

From 6212407d8d9a763fa103637642a5f6d135c4cf09 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 9 Sep 2026 17:31:45 +0200
Subject: [PATCH 5/8] one fewer argument

---
 Mathlib/Tactic/Positivity/Finset.lean | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Tactic/Positivity/Finset.lean b/Mathlib/Tactic/Positivity/Finset.lean
index 8551bc3a48cdad..a65e6d28502cc6 100644
--- a/Mathlib/Tactic/Positivity/Finset.lean
+++ b/Mathlib/Tactic/Positivity/Finset.lean
@@ -60,14 +60,12 @@ meta def evalFinsetDens : PositivityExt where eval {u 𝕜} _ pα? e :=
     return .positive q(@Nonempty.dens_pos $α $instα $s $ps)
   | _, _, _ => throwError "not Finset.dens"
 
-private meta def findMemFinset {u : Level} {α : Q(Type u)} (s : Q(Finset $α)) (p : Q(Prop))
-    (e : Q($p)) :
-    MetaM <| Option <| (a : Q($α)) × Q($a ∈ $s) := withNewMCtxDepth do
+private meta def isMemFinset? {u : Level} {α : Q(Type u)} (s : Q(Finset $α)) (p : Q(Prop)) :
+    MetaM <| Option <| (a : Q($α)) ×' $p =Q ($a ∈ $s) := withNewMCtxDepth do
   let m ← mkFreshExprMVarQ q($α)
   let .defEq _ ← isDefEqQ q($p) q($m ∈ $s) | return none
   let ⟨m, _⟩ ← instantiateMVarsQ' q($m)
-  let ⟨e, _⟩ ← instantiateMVarsQ' q($e)
-  return some ⟨q($m), q($e)⟩
+  return some ⟨q($m), ⟨⟩⟩
 
 attribute [local instance] monadLiftOptionMetaM in
 /-- The `positivity` extension which proves that `∑ a ∈ s, f a` is nonnegative if `f` is, and
@@ -111,9 +109,10 @@ meta def evalFinsetSum : PositivityExt where eval {u α} zα pα? e :=
       for ldecl in ← getLCtx do
         if ldecl.isImplementationDetail then continue
         unless ← Meta.isProp ldecl.type do continue
-        let .some ⟨a, ha⟩ ← findMemFinset q($s) ldecl.type ldecl.toExpr | continue
+        have ty : Q(Prop) := ldecl.type
+        have ha : Q($ty) := ldecl.toExpr
+        let .some ⟨a, _⟩ ← isMemFinset? q($s) ty | continue
         have fa : Q($α) := .betaRev f #[a]
-        let fa ← instantiateMVarsQ q($fa)
         let : $fa =Q $f $a := ⟨⟩
         let .positive pa ← catchNone (core zα pα fa) | continue
         assertInstancesCommute

From 95454737fdf61bc513d1c8afa6ccc4837d3d9adc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 9 Sep 2026 17:34:42 +0200
Subject: [PATCH 6/8] not as many @

---
 Mathlib/Tactic/Positivity/Finset.lean | 15 ++++++---------
 1 file changed, 6 insertions(+), 9 deletions(-)

diff --git a/Mathlib/Tactic/Positivity/Finset.lean b/Mathlib/Tactic/Positivity/Finset.lean
index a65e6d28502cc6..34a9e7acd08a34 100644
--- a/Mathlib/Tactic/Positivity/Finset.lean
+++ b/Mathlib/Tactic/Positivity/Finset.lean
@@ -91,11 +91,10 @@ meta def evalFinsetSum : PositivityExt where eval {u α} zα pα? e :=
     let p_pos : Option Q(0 < $e) ← do
       let .positive pbody := rbody | pure none -- Fail if the body is not provably positive
       let some ps ← proveFinsetNonempty s | pure none
-      let .some pα' ← trySynthInstanceQ q(IsOrderedCancelAddMonoid $α) | pure none
+      let .some _pα' ← trySynthInstanceQ q(IsOrderedCancelAddMonoid $α) | pure none
       assertInstancesCommute
       let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody
-      pure <| some q(@sum_pos $ι $α $instα (@PartialOrder.toPreorder _ $pα) $pα' $f $s _
-        (fun i _ ↦ $pr i) $ps)
+      pure <| some q(sum_pos (fun i _ ↦ $pr i) $ps)
     -- Try to show that the sum is positive because all summands are
     if let some p_pos := p_pos then
       return .positive p_pos
@@ -105,7 +104,7 @@ meta def evalFinsetSum : PositivityExt where eval {u α} zα pα? e :=
     -- among the assumptions of the form `a ∈ s`, since we have no other way of getting hold of an
     -- element of `s` at which `f` might be positive.
     let p_pos' : Option Q(0 < $e) ← (do
-      let .some pα' ← trySynthInstanceQ q(IsOrderedCancelAddMonoid $α) | pure none
+      let .some _pα' ← trySynthInstanceQ q(IsOrderedCancelAddMonoid $α) | pure none
       for ldecl in ← getLCtx do
         if ldecl.isImplementationDetail then continue
         unless ← Meta.isProp ldecl.type do continue
@@ -116,16 +115,14 @@ meta def evalFinsetSum : PositivityExt where eval {u α} zα pα? e :=
         let : $fa =Q $f $a := ⟨⟩
         let .positive pa ← catchNone (core zα pα fa) | continue
         assertInstancesCommute
-        return some q(@sum_pos' $ι $α $instα (@PartialOrder.toPreorder _ $pα) $pα' $f $s _
-          (fun i _ ↦ $pr i) ⟨$a, $ha, $pa⟩)
+        return some q(sum_pos' (fun i _ ↦ $pr i) ⟨$a, $ha, $pa⟩)
       return none)
     if let some p_pos' := p_pos' then
       return .positive p_pos'
     -- Fall back to showing that the sum is nonnegative
-    let pα' ← synthInstanceQ q(AddLeftMono $α)
+    let _pα' ← synthInstanceQ q(AddLeftMono $α)
     assertInstancesCommute
-    return .nonnegative q(@sum_nonneg $ι $α $instα (@PartialOrder.toPreorder _ $pα) $f $s $pα'
-      fun i _ ↦ $pr i)
+    return .nonnegative q(sum_nonneg fun i _ ↦ $pr i)
   | _ => throwError "not Finset.sum"
 
 variable {α : Type*} {s : Finset α}

From b23e91212f51d9faf56bea52e695add33a20b16c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 9 Sep 2026 17:53:42 +0200
Subject: [PATCH 7/8] docstring

---
 Mathlib/Tactic/Positivity/Finset.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Mathlib/Tactic/Positivity/Finset.lean b/Mathlib/Tactic/Positivity/Finset.lean
index 34a9e7acd08a34..9554e53ded6bf5 100644
--- a/Mathlib/Tactic/Positivity/Finset.lean
+++ b/Mathlib/Tactic/Positivity/Finset.lean
@@ -60,6 +60,8 @@ meta def evalFinsetDens : PositivityExt where eval {u 𝕜} _ pα? e :=
     return .positive q(@Nonempty.dens_pos $α $instα $s $ps)
   | _, _, _ => throwError "not Finset.dens"
 
+/-- Return whether `p` is a proposition of the form `?a ∈ s`. If so, return `a` and a Qq-proof that
+`p` is `a ∈ s`. -/
 private meta def isMemFinset? {u : Level} {α : Q(Type u)} (s : Q(Finset $α)) (p : Q(Prop)) :
     MetaM <| Option <| (a : Q($α)) ×' $p =Q ($a ∈ $s) := withNewMCtxDepth do
   let m ← mkFreshExprMVarQ q($α)

From e4d0a9f376930d7597dbfb0b819c0e56bfa74c7e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Wed, 9 Sep 2026 17:36:31 +0100
Subject: [PATCH 8/8] withReducible

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
---
 Mathlib/Tactic/Positivity/Finset.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/Tactic/Positivity/Finset.lean b/Mathlib/Tactic/Positivity/Finset.lean
index 9554e53ded6bf5..726aabb8b1f102 100644
--- a/Mathlib/Tactic/Positivity/Finset.lean
+++ b/Mathlib/Tactic/Positivity/Finset.lean
@@ -65,7 +65,7 @@ meta def evalFinsetDens : PositivityExt where eval {u 𝕜} _ pα? e :=
 private meta def isMemFinset? {u : Level} {α : Q(Type u)} (s : Q(Finset $α)) (p : Q(Prop)) :
     MetaM <| Option <| (a : Q($α)) ×' $p =Q ($a ∈ $s) := withNewMCtxDepth do
   let m ← mkFreshExprMVarQ q($α)
-  let .defEq _ ← isDefEqQ q($p) q($m ∈ $s) | return none
+  let .defEq _ ← withReducible <| isDefEqQ q($p) q($m ∈ $s) | return none
   let ⟨m, _⟩ ← instantiateMVarsQ' q($m)
   return some ⟨q($m), ⟨⟩⟩