chore: bump toolchain to v4.32.0-rc1 (#40732)

Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Joscha <joscha@plugh.de>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Julia Markus Himmel <2065352+TwoFX@users.noreply.github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

Author: 8 people

Counterexamples/DirectSumIsInternal.lean

@@ -56,8 +56,10 @@ theorem withSign.isCompl : IsCompl ℤ≥0 ℤ≤0 := by
     · exact Submodule.mem_sup_left (mem_withSign_one.mpr hp)
     · exact Submodule.mem_sup_right (mem_withSign_neg_one.mpr hn)
 
-lemma withSign.independent : iSupIndep withSign := by
-  apply (iSupIndep_pair UnitsInt.one_ne_neg_one _).mpr withSign.isCompl.disjoint
+set_option linter.defProp false in
+def withSign.independent : iSupIndep withSign := by
+  apply
+    (iSupIndep_pair UnitsInt.one_ne_neg_one _).mpr withSign.isCompl.disjoint
   intro i
   fin_cases i <;> simp
 

Mathlib/Algebra/Category/Grp/Basic.lean

@@ -600,19 +600,24 @@ instance CommGrpCat.forget_reflects_isos : (forget CommGrpCat.{u}).ReflectsIsomo
 -- note: in the following definitions, there is a problem with `@[to_additive]`
 -- as the `Category` instance is not found on the additive variant
 -- this variant is then renamed with an `Aux` suffix
-
+set_option linter.checkUnivs false in
 /-- An alias for `GrpCat.{max u v}`, to deal around unification issues. -/
 @[to_additive (attr := nolint checkUnivs) GrpMaxAux
   /-- An alias for `AddGrpCat.{max u v}`, to deal around unification issues. -/]
 abbrev GrpMax.{u1, u2} := GrpCat.{max u1 u2}
+
+set_option linter.checkUnivs false in
 /-- An alias for `AddGrpCat.{max u v}`, to deal around unification issues. -/
 @[nolint checkUnivs]
 abbrev AddGrpMax.{u1, u2} := AddGrpCat.{max u1 u2}
 
+set_option linter.checkUnivs false in
 /-- An alias for `CommGrpCat.{max u v}`, to deal around unification issues. -/
 @[to_additive (attr := nolint checkUnivs) AddCommGrpMaxAux
   /-- An alias for `AddCommGrpCat.{max u v}`, to deal around unification issues. -/]
 abbrev CommGrpMax.{u1, u2} := CommGrpCat.{max u1 u2}
+
+set_option linter.checkUnivs false in
 /-- An alias for `AddCommGrpCat.{max u v}`, to deal around unification issues. -/
 @[nolint checkUnivs]
 abbrev AddCommGrpMax.{u1, u2} := AddCommGrpCat.{max u1 u2}

Mathlib/Algebra/Module/Presentation/Basic.lean

@@ -48,6 +48,7 @@ namespace Module
 
 variable (A : Type u) [Ring A]
 
+set_option linter.checkUnivs false in
 /-- Given a ring `A`, this structure involves a family of elements (indexed by a type `R`)
 in a free module `G →₀ A`. This allows to define an `A`-module by generators and relations,
 see `Relations.Quotient`. -/
@@ -488,6 +489,7 @@ end Relations
 
 variable (M : Type v) [AddCommGroup M] [Module A M]
 
+set_option linter.checkUnivs false in
 /-- Given an `A`-module `M`, a term in this type is a presentation by `M` by
 generators and relations. -/
 @[nolint checkUnivs]

Mathlib/Algebra/Order/AbsoluteValue/Basic.lean

@@ -416,8 +416,8 @@ open Lean Meta Mathlib Meta Positivity Qq in
 For performance reasons, we only attempt to apply this when `abv` is a variable.
 If it is an explicit function, e.g. `|_|` or `‖_‖`, another extension should apply. -/
 @[positivity _]
-meta def Mathlib.Meta.Positivity.evalAbv : PositivityExt where eval {_ _α} _zα pα? e := do
-  let some _ := pα? | pure .none
+meta def Mathlib.Meta.Positivity.evalAbv : PositivityExt where eval {_ _α} _zα pα? e :=
+  match pα? with | none => pure .none | some _ => do
   let (.app f a) ← whnfR e | throwError "not abv ·"
   if !f.getAppFn.isFVar then
     throwError "abv: function is not a variable"

Mathlib/Algebra/Order/Algebra.lean

@@ -95,14 +95,13 @@ open Lean Meta Qq Function
 
 /-- Extension for `algebraMap`. -/
 @[positivity algebraMap _ _ _]
-meta def evalAlgebraMap : PositivityExt where eval {u β} _zβ pβ? e := do
+meta def evalAlgebraMap : PositivityExt where eval {u β} _zβ pβ? e :=
+  match pβ? with | none => pure .none | some _ => do
   let ~q(@algebraMap $α _ $instα $instβ $instαβ $a) := e | throwError "not `algebraMap`"
-  let pα ← try? <| synthInstanceQ q(PartialOrder $α)
-  match ← core q(inferInstance) pα a with
+  let some pα ← try? <| synthInstanceQ q(PartialOrder $α) | pure .none
+  match ← core q(inferInstance) (some pα) a with
   | .positive pa =>
-    let some _ := pβ? | pure .none
     let _instαSemiring ← synthInstanceQ q(Semiring $α)
-    let _instαPartialOrder ← synthInstanceQ q(PartialOrder $α)
     try
       let _instβSemiring ← synthInstanceQ q(Semiring $β)
       let _instβPartialOrder ← synthInstanceQ q(PartialOrder $β)
@@ -118,9 +117,7 @@ meta def evalAlgebraMap : PositivityExt where eval {u β} _zβ pβ? e := do
       assertInstancesCommute
       return .nonnegative q(algebraMap_nonneg $β <| le_of_lt $pa)
   | .nonnegative pa =>
-    let some _ := pβ? | pure .none
     let _instαSemiring ← synthInstanceQ q(CommSemiring $α)
-    let _instαPartialOrder ← synthInstanceQ q(PartialOrder $α)
     let _instβSemiring ← synthInstanceQ q(Semiring $β)
     let _instβPartialOrder ← synthInstanceQ q(PartialOrder $β)
     let _instβIsOrderedRing ← synthInstanceQ q(IsOrderedRing $β)

Mathlib/Algebra/Order/BigOperators/Expect.lean

@@ -220,22 +220,22 @@ open scoped BigOperators
 attribute [local instance] monadLiftOptionMetaM in
 /-- Positivity extension for `Finset.expect`. -/
 @[positivity Finset.expect _ _]
-meta def evalFinsetExpect : PositivityExt where eval {u α} zα pα? e := do
-  let some pα := pα? | pure .none
+meta def evalFinsetExpect : PositivityExt where eval {u α} zα pα? e :=
+  match pα? with | none => pure .none | some pα => do
   match e with
   | ~q(@Finset.expect $ι _ $instα $instmod $s $f) =>
     let i : Q($ι) ← mkFreshExprMVarQ q($ι) .syntheticOpaque
     have body : Q($α) := .betaRev f #[i]
     let rbody ← core zα pα body
-    let p_pos : Option Q(0 < $e) ← (do
+    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 instαordsmul ← trySynthInstanceQ q(PosSMulStrictMono ℚ≥0 $α) | pure none
       assumeInstancesCommute
       let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody
-      return some
-        q(@expect_pos $ι $α $instα $pα $pα' $instmod $instαordsmul $s $f (fun i _ ↦ $pr i) $ps))
+      pure <| some
+        q(@expect_pos $ι $α $instα $pα $pα' $instmod $instαordsmul $s $f (fun i _ ↦ $pr i) $ps)
     -- Try to show that the sum is positive
     if let some p_pos := p_pos then
       return .positive p_pos

Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

@@ -225,16 +225,16 @@ example (s : Finset ℕ) (f : ℕ → ℤ) (hf : ∀ n, 0 ≤ f n) : 0 ≤ s.pro
 because `compareHyp` can't look for assumptions behind binders.
 -/
 @[positivity Finset.prod _ _]
-meta def evalFinsetProd : PositivityExt where eval {u α} zα pα? e := do
+meta def evalFinsetProd : PositivityExt where eval {u α} zα pα? e :=
+  match pα? with | none => pure .none | some pα => do
   match e with
   | ~q(@Finset.prod $ι _ $instα $s $f) =>
-    let some pα := pα? | pure .none
     let i : Q($ι) ← mkFreshExprMVarQ q($ι) .syntheticOpaque
     have body : Q($α) := Expr.betaRev f #[i]
     let rbody ← core zα pα body
     let _instαmon ← synthInstanceQ q(CommMonoidWithZero $α)
     -- Try to show that the product is positive
-    let p_pos : Option Q(0 < $e) := ← do
+    let p_pos : Option Q(0 < $e) ← do
       let .positive pbody := rbody | pure none -- Fail if the body is not provably positive
       -- TODO(https://github.com/leanprover-community/quote4/issues/38):
       -- We must name the following, else `assertInstancesCommute` loops.
@@ -243,19 +243,19 @@ meta def evalFinsetProd : PositivityExt where eval {u α} zα pα? e := do
       let .some _instαnontriv ← trySynthInstanceQ q(Nontrivial $α) | pure none
       assertInstancesCommute
       let pr : Q(∀ i, 0 < $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
-      return some q(prod_pos fun i _ ↦ $pr i)
+      pure <| some q(prod_pos fun i _ ↦ $pr i)
     if let some p_pos := p_pos then return .positive p_pos
     -- Try to show that the product is nonnegative
-    let p_nonneg : Option Q(0 ≤ $e) := ← do
+    let p_nonneg : Option Q(0 ≤ $e) ← do
       let some pbody := rbody.toNonneg
-        | return none -- Fail if the body is not provably nonnegative
+        | pure none -- Fail if the body is not provably nonnegative
       let pr : Q(∀ i, 0 ≤ $f i) ← mkLambdaFVars #[i] pbody (binderInfoForMVars := .default)
       -- TODO(https://github.com/leanprover-community/quote4/issues/38):
       -- We must name the following, else `assertInstancesCommute` loops.
       let .some _instαzeroone ← trySynthInstanceQ q(ZeroLEOneClass $α) | pure none
       let .some _instαposmul ← trySynthInstanceQ q(PosMulMono $α) | pure none
       assertInstancesCommute
-      return some q(prod_nonneg fun i _ ↦ $pr i)
+      pure <| some q(prod_nonneg fun i _ ↦ $pr i)
     if let some p_nonneg := p_nonneg then return .nonnegative p_nonneg
     -- Fall back to showing that the product is nonzero
     let pbody ← rbody.toNonzero

Mathlib/Algebra/Order/Field/Basic.lean

@@ -740,26 +740,28 @@ such that `positivity` successfully recognises both `a` and `b`. -/
   trace[Tactic.positivity.zeroness] "evalDiv: {a} divided by {b}"
   let _a ← synthInstanceQ q(Semifield $α)
   let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(HDiv.hDiv)
-  let some pα := pα? |
+  match (dependent := true) pα? with
+  | none =>
     match ← core zα pα? a, ← core zα pα? b with
     | .nonzero pa, .nonzero pb =>
       let _a ← synthInstanceQ q(GroupWithZero $α)
       assumeInstancesCommute
       pure (.nonzero q(div_ne_zero $pa $pb))
     | _, _ => pure .none
-  let _a ← synthInstanceQ q(GroupWithZero $α)
-  let _a ← synthInstanceQ q(PosMulReflectLT $α)
-  assumeInstancesCommute
-  let ra ← core zα pα a; let rb ← core zα pα b
-  match ra, rb with
-  | .positive pa, .positive pb => pure (.positive q(div_pos $pa $pb))
-  | .positive pa, .nonnegative pb => pure (.nonnegative q(div_nonneg_of_pos_of_nonneg $pa $pb))
-  | .nonnegative pa, .positive pb => pure (.nonnegative q(div_nonneg_of_nonneg_of_pos $pa $pb))
-  | .nonnegative pa, .nonnegative pb => pure (.nonnegative q(div_nonneg $pa $pb))
-  | .positive pa, .nonzero pb => pure (.nonzero q(div_ne_zero_of_pos_of_ne_zero $pa $pb))
-  | .nonzero pa, .positive pb => pure (.nonzero q(div_ne_zero_of_ne_zero_of_pos $pa $pb))
-  | .nonzero pa, .nonzero pb => pure (.nonzero q(div_ne_zero $pa $pb))
-  | _, _ => pure .none
+  | some pα =>
+    let _a ← synthInstanceQ q(GroupWithZero $α)
+    let _a ← synthInstanceQ q(PosMulReflectLT $α)
+    assumeInstancesCommute
+    let ra ← core zα pα a; let rb ← core zα pα b
+    match ra, rb with
+    | .positive pa, .positive pb => pure (.positive q(div_pos $pa $pb))
+    | .positive pa, .nonnegative pb => pure (.nonnegative q(div_nonneg_of_pos_of_nonneg $pa $pb))
+    | .nonnegative pa, .positive pb => pure (.nonnegative q(div_nonneg_of_nonneg_of_pos $pa $pb))
+    | .nonnegative pa, .nonnegative pb => pure (.nonnegative q(div_nonneg $pa $pb))
+    | .positive pa, .nonzero pb => pure (.nonzero q(div_ne_zero_of_pos_of_ne_zero $pa $pb))
+    | .nonzero pa, .positive pb => pure (.nonzero q(div_ne_zero_of_ne_zero_of_pos $pa $pb))
+    | .nonzero pa, .nonzero pb => pure (.nonzero q(div_ne_zero $pa $pb))
+    | _, _ => pure .none
 
 /-- The `positivity` extension which identifies expressions of the form `a⁻¹`,
 such that `positivity` successfully recognises `a`. -/
@@ -769,33 +771,35 @@ meta def evalInv : PositivityExt where eval {u α} zα pα? e := do
   let _e_eq : $e =Q $f $a := ⟨⟩
   let _a ← synthInstanceQ q(Semifield $α)
   let ⟨_f_eq⟩ ← withDefault <| withNewMCtxDepth <| assertDefEqQ q($f) q(Inv.inv)
-  let some _ := pα? |
+  match (dependent := true) pα? with
+  | none =>
     match ← core zα pα? a with
     | .nonzero pa =>
       let _a ← synthInstanceQ q(GroupWithZero $α)
       assumeInstancesCommute
       pure (.nonzero q(inv_ne_zero $pa))
     | _ => pure .none
-  let _a ← synthInstanceQ q(GroupWithZero $α)
-  let _a ← synthInstanceQ q(PartialOrder $α)
-  let _a ← synthInstanceQ q(PosMulReflectLT $α)
-  assumeInstancesCommute
-  let ra ← core zα pα? a
-  match ra with
-  | .positive pa =>
+  | some pα =>
+    let _a ← synthInstanceQ q(GroupWithZero $α)
+    let _a ← synthInstanceQ q(PartialOrder $α)
+    let _a ← synthInstanceQ q(PosMulReflectLT $α)
     assumeInstancesCommute
-    pure (.positive q(inv_pos_of_pos $pa))
-  | .nonnegative pa =>
-    assumeInstancesCommute
-    pure (.nonnegative q(inv_nonneg_of_nonneg $pa))
-  | .nonzero pa => pure (.nonzero q(inv_ne_zero $pa))
-  | .none => pure .none
+    let ra ← core zα (some pα) a
+    match ra with
+    | .positive pa =>
+      assumeInstancesCommute
+      pure (.positive q(inv_pos_of_pos $pa))
+    | .nonnegative pa =>
+      assumeInstancesCommute
+      pure (.nonnegative q(inv_nonneg_of_nonneg $pa))
+    | .nonzero pa => pure (.nonzero q(inv_ne_zero $pa))
+    | .none => pure .none
 
 /-- The `positivity` extension which identifies expressions of the form `a ^ (0:ℤ)`. -/
 @[positivity _ ^ (0 : ℤ), Pow.pow _ (0 : ℤ)]
-meta def evalPowZeroInt : PositivityExt where eval {u α} _zα pα? e := do
+meta def evalPowZeroInt : PositivityExt where eval {u α} _zα pα? e :=
+  match pα? with | none => pure .none | some _ => do
   let .app (.app _ (a : Q($α))) _ ← withReducible (whnf e) | throwError "not ^"
-  let some _ := pα? | pure .none
   let _a ← synthInstanceQ q(Semifield $α)
   let _a ← synthInstanceQ q(LinearOrder $α)
   let _a ← synthInstanceQ q(IsStrictOrderedRing $α)

Mathlib/Algebra/Order/Field/Power.lean

@@ -125,69 +125,71 @@ such that `positivity` successfully recognises both `a` and `b`. -/
 @[positivity _ ^ (_ : ℤ), Pow.pow _ (_ : ℤ)]
 meta def evalZPow : PositivityExt where eval {u α} zα pα? e := do
   let .app (.app _ (a : Q($α))) (b : Q(ℤ)) ← withReducible (whnf e) | throwError "not ^"
-  let some pα := pα? |
+  match (dependent := true) pα? with
+  | none =>
     match ← core zα pα? a with
     | .nonzero pa =>
       let _a ← synthInstanceQ q(GroupWithZero $α)
       assumeInstancesCommute
       haveI' : $e =Q $a ^ $b := ⟨⟩
       pure (.nonzero q(zpow_ne_zero $b $pa))
     | _ => pure .none
-  let result ← catchNone do
-    let _a ← synthInstanceQ q(Field $α)
-    let _a ← synthInstanceQ q(LinearOrder $α)
-    let _a ← synthInstanceQ q(IsStrictOrderedRing $α)
-    assumeInstancesCommute
-    match ← whnfR b with
-    | .app (.app (.app (.const `OfNat.ofNat _) _) (.lit (Literal.natVal n))) _ =>
-      guard (n % 2 = 0)
-      have m : Q(ℕ) := mkRawNatLit (n / 2)
-      haveI' : $b =Q $m + $m := ⟨⟩
-      haveI' : $e =Q $a ^ $b := ⟨⟩
-      pure (.nonnegative q(Even.zpow_nonneg (Even.add_self _) $a))
-    | .app (.app (.app (.const `Neg.neg _) _) _) b' =>
-      let b' ← whnfR b'
-      let .true := b'.isAppOfArity ``OfNat.ofNat 3 | throwError "not a ^ -n where n is a literal"
-      let some n := (b'.getRevArg! 1).rawNatLit? | throwError "not a ^ -n where n is a literal"
-      guard (n % 2 = 0)
-      have m : Q(ℕ) := mkRawNatLit (n / 2)
-      haveI' : $b =Q (-$m) + (-$m) := ⟨⟩
-      haveI' : $e =Q $a ^ $b := ⟨⟩
-      pure (.nonnegative q(Even.zpow_nonneg (Even.add_self _) $a))
-    | _ => throwError "not a ^ n where n is a literal or a negated literal"
-  orElse result do
-    let ra ← core zα pα a
-    let ofNonneg (pa : Q(0 ≤ $a))
-        (_oα : Q(Semifield $α)) (_oα : Q(LinearOrder $α)) (_oα : Q(IsStrictOrderedRing $α)) :
-        MetaM (Strictness zα e pα) := do
-      haveI' : $e =Q $a ^ $b := ⟨⟩
-      assumeInstancesCommute
-      pure (.nonnegative q(zpow_nonneg $pa $b))
-    let ofNonzero (pa : Q($a ≠ 0)) (_oα : Q(GroupWithZero $α)) : MetaM (Strictness zα e pα) := do
-      haveI' : $e =Q $a ^ $b := ⟨⟩
-      let _a ← synthInstanceQ q(GroupWithZero $α)
+  | some pα =>
+    let result ← catchNone do
+      let _a ← synthInstanceQ q(Field $α)
+      let _a ← synthInstanceQ q(LinearOrder $α)
+      let _a ← synthInstanceQ q(IsStrictOrderedRing $α)
       assumeInstancesCommute
-      pure (.nonzero q(zpow_ne_zero $b $pa))
-    match ra with
-    | .positive pa =>
-      try
-        let _a ← synthInstanceQ q(Semifield $α)
-        let _a ← synthInstanceQ q(LinearOrder $α)
-        let _a ← synthInstanceQ q(IsStrictOrderedRing $α)
+      match ← whnfR b with
+      | .app (.app (.app (.const `OfNat.ofNat _) _) (.lit (Literal.natVal n))) _ =>
+        guard (n % 2 = 0)
+        have m : Q(ℕ) := mkRawNatLit (n / 2)
+        haveI' : $b =Q $m + $m := ⟨⟩
+        haveI' : $e =Q $a ^ $b := ⟨⟩
+        pure (.nonnegative q(Even.zpow_nonneg (Even.add_self _) $a))
+      | .app (.app (.app (.const `Neg.neg _) _) _) b' =>
+        let b' ← whnfR b'
+        let .true := b'.isAppOfArity ``OfNat.ofNat 3 | throwError "not a ^ -n where n is a literal"
+        let some n := (b'.getRevArg! 1).rawNatLit? | throwError "not a ^ -n where n is a literal"
+        guard (n % 2 = 0)
+        have m : Q(ℕ) := mkRawNatLit (n / 2)
+        haveI' : $b =Q (-$m) + (-$m) := ⟨⟩
+        haveI' : $e =Q $a ^ $b := ⟨⟩
+        pure (.nonnegative q(Even.zpow_nonneg (Even.add_self _) $a))
+      | _ => throwError "not a ^ n where n is a literal or a negated literal"
+    orElse result do
+      let ra ← core zα pα a
+      let ofNonneg (pa : Q(0 ≤ $a))
+          (_oα : Q(Semifield $α)) (_oα : Q(LinearOrder $α)) (_oα : Q(IsStrictOrderedRing $α)) :
+          MetaM (Strictness zα e pα) := do
+        haveI' : $e =Q $a ^ $b := ⟨⟩
         assumeInstancesCommute
+        pure (.nonnegative q(zpow_nonneg $pa $b))
+      let ofNonzero (pa : Q($a ≠ 0)) (_oα : Q(GroupWithZero $α)) : MetaM (Strictness zα e pα) := do
         haveI' : $e =Q $a ^ $b := ⟨⟩
-        pure (.positive q(zpow_pos $pa $b))
-      catch e : Exception =>
-        trace[Tactic.positivity.failure] "{e.toMessageData}"
-        let sα ← synthInstanceQ q(Semifield $α)
-        let oα ← synthInstanceQ q(LinearOrder $α)
-        let iα ← synthInstanceQ q(IsStrictOrderedRing $α)
-        orElse (← catchNone (ofNonneg q(le_of_lt $pa) sα oα iα))
-          (ofNonzero q(ne_of_gt $pa) q(inferInstance))
-    | .nonnegative pa =>
-      ofNonneg pa (← synthInstanceQ (_ : Q(Type u)))
-                  (← synthInstanceQ (_ : Q(Type u))) (← synthInstanceQ (_ : Q(Prop)))
-    | .nonzero pa => ofNonzero pa (← synthInstanceQ (_ : Q(Type u)))
-    | .none => pure .none
+        let _a ← synthInstanceQ q(GroupWithZero $α)
+        assumeInstancesCommute
+        pure (.nonzero q(zpow_ne_zero $b $pa))
+      match ra with
+      | .positive pa =>
+        try
+          let _a ← synthInstanceQ q(Semifield $α)
+          let _a ← synthInstanceQ q(LinearOrder $α)
+          let _a ← synthInstanceQ q(IsStrictOrderedRing $α)
+          assumeInstancesCommute
+          haveI' : $e =Q $a ^ $b := ⟨⟩
+          pure (.positive q(zpow_pos $pa $b))
+        catch e : Exception =>
+          trace[Tactic.positivity.failure] "{e.toMessageData}"
+          let sα ← synthInstanceQ q(Semifield $α)
+          let oα ← synthInstanceQ q(LinearOrder $α)
+          let iα ← synthInstanceQ q(IsStrictOrderedRing $α)
+          orElse (← catchNone (ofNonneg q(le_of_lt $pa) sα oα iα))
+            (ofNonzero q(ne_of_gt $pa) q(inferInstance))
+      | .nonnegative pa =>
+        ofNonneg pa (← synthInstanceQ (_ : Q(Type u)))
+                    (← synthInstanceQ (_ : Q(Type u))) (← synthInstanceQ (_ : Q(Prop)))
+      | .nonzero pa => ofNonzero pa (← synthInstanceQ (_ : Q(Type u)))
+      | .none => pure .none
 
 end Mathlib.Meta.Positivity