Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Mario Carneiro, Heather Macbeth, Yaël Dillies
-/
import Std.Lean.Parser
import Mathlib.Data.Int.Order.Basic
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Tactic.Positivity.Core
import Mathlib.Algebra.GroupPower.Order
import Mathlib.Algebra.Order.Field.Basic
import Qq

/-!
## `positivity` core extensions

This file sets up the basic `positivity` extensions tagged with the `@[positivity]` attribute.
-/

namespace Mathlib.Meta.Positivity
open Lean Meta Qq Function

section LinearOrder
variable [LinearOrder: Type ?u.21 → Type ?u.21LinearOrder R: ?m.4R] {a: Ra b: Rb c: Rc : R: ?m.4R}

private lemma le_min_of_lt_of_le: a < b → a ≤ c → a ≤ min b cle_min_of_lt_of_le  (ha: a < bha : a: Ra < b: Rb) (hb: a ≤ chb : a: Ra ≤ c: Rc) : a: Ra ≤ min: {α : Type ?u.657} → [self : Min α] → α → α → αmin b: Rb c: Rc := le_min: ∀ {α : Type ?u.740} [inst : LinearOrder α] {a b c : α}, c ≤ a → c ≤ b → c ≤ min a ble_min ha: a < bha.le: ∀ {α : Type ?u.790} [inst : Preorder α] {a b : α}, a < b → a ≤ ble hb: a ≤ chb
private lemma le_min_of_le_of_lt: ∀ {R : Type u_1} [inst : LinearOrder R] {a b c : R}, a ≤ b → a < c → a ≤ min b cle_min_of_le_of_lt (ha: a ≤ bha : a: Ra ≤ b: Rb) (hb: a < chb : a: Ra < c: Rc) : a: Ra ≤ min: {α : Type ?u.1798} → [self : Min α] → α → α → αmin b: Rb c: Rc := le_min: ∀ {α : Type ?u.1881} [inst : LinearOrder α] {a b c : α}, c ≤ a → c ≤ b → c ≤ min a ble_min ha: a ≤ bha hb: a < chb.le: ∀ {α : Type ?u.1935} [inst : Preorder α] {a b : α}, a < b → a ≤ ble
private lemma min_ne: ∀ {R : Type u_1} [inst : LinearOrder R] {a b c : R}, a ≠ c → b ≠ c → min a b ≠ cmin_ne (ha: a ≠ cha : a: Ra ≠ c: Rc) (hb: b ≠ chb : b: Rb ≠ c: Rc) : min: {α : Type ?u.2322} → [self : Min α] → α → α → αmin a: Ra b: Rb ≠ c: Rc :=
byGoals accomplished! 🐙 R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ cmin a b ≠ crw [R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ cmin a b ≠ cmin_def: ∀ {α : Type ?u.2435} [inst : LinearOrder α] (a b : α), min a b = if a ≤ b then a else bmin_defR: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ c(if a ≤ b then a else b) ≠ c]R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ c(if a ≤ b then a else b) ≠ c;R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ c(if a ≤ b then a else b) ≠ c R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ cmin a b ≠ csplit_ifsR: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ ch✝: a ≤ binla ≠ cR: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ ch✝: ¬a ≤ binrb ≠ c R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ c(if a ≤ b then a else b) ≠ c<;>R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ ch✝: a ≤ binla ≠ cR: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ ch✝: ¬a ≤ binrb ≠ c R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ c(if a ≤ b then a else b) ≠ cassumptionGoals accomplished! 🐙

private lemma min_ne_of_ne_of_lt: a ≠ c → c < b → min a b ≠ cmin_ne_of_ne_of_lt (ha: a ≠ cha : a: Ra ≠ c: Rc) (hb: c < bhb : c: Rc < b: Rb) : min: {α : Type ?u.3242} → [self : Min α] → α → α → αmin a: Ra b: Rb ≠ c: Rc := min_ne: ∀ {R : Type ?u.3335} [inst : LinearOrder R] {a b c : R}, a ≠ c → b ≠ c → min a b ≠ cmin_ne ha: a ≠ cha hb: c < bhb.ne': ∀ {α : Type ?u.3380} [inst : Preorder α] {x y : α}, x < y → y ≠ xne'
private lemma min_ne_of_lt_of_ne: ∀ {R : Type u_1} [inst : LinearOrder R] {a b c : R}, c < a → b ≠ c → min a b ≠ cmin_ne_of_lt_of_ne (ha: c < aha : c: Rc < a: Ra) (hb: b ≠ chb : b: Rb ≠ c: Rc) : min: {α : Type ?u.4119} → [self : Min α] → α → α → αmin a: Ra b: Rb ≠ c: Rc := min_ne: ∀ {R : Type ?u.4212} [inst : LinearOrder R] {a b c : R}, a ≠ c → b ≠ c → min a b ≠ cmin_ne ha: c < aha.ne': ∀ {α : Type ?u.4256} [inst : Preorder α] {x y : α}, x < y → y ≠ xne' hb: b ≠ chb

private lemma max_ne: ∀ {R : Type u_1} [inst : LinearOrder R] {a b c : R}, a ≠ c → b ≠ c → max a b ≠ cmax_ne (ha: a ≠ cha : a: Ra ≠ c: Rc) (hb: b ≠ chb : b: Rb ≠ c: Rc) : max: {α : Type ?u.4647} → [self : Max α] → α → α → αmax a: Ra b: Rb ≠ c: Rc :=
byGoals accomplished! 🐙 R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ cmax a b ≠ crw [R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ cmax a b ≠ cmax_def: ∀ {α : Type ?u.4760} [inst : LinearOrder α] (a b : α), max a b = if a ≤ b then b else amax_defR: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ c(if a ≤ b then b else a) ≠ c]R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ c(if a ≤ b then b else a) ≠ c;R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ c(if a ≤ b then b else a) ≠ c R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ cmax a b ≠ csplit_ifsR: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ ch✝: a ≤ binlb ≠ cR: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ ch✝: ¬a ≤ binra ≠ c R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ c(if a ≤ b then b else a) ≠ c<;>R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ ch✝: a ≤ binlb ≠ cR: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ ch✝: ¬a ≤ binra ≠ c R: Type u_1inst✝: LinearOrder Ra, b, c: Rha: a ≠ chb: b ≠ c(if a ≤ b then b else a) ≠ cassumptionGoals accomplished! 🐙

end LinearOrder

/-- The `positivity` extension which identifies expressions of the form `min a b`,
such that `positivity` successfully recognises both `a` and `b`. -/
@[positivity min: {α : Type ?u.15863} → [self : Min α] → α → α → αmin _: ?m.15864_ _: ?m.15864_] def evalMin: PositivityExtevalMin : PositivityExt: TypePositivityExt where eval {u: ?m.5135u α: ?m.5138α} zα: ?m.5141zα pα: ?m.5144pα e: ?m.5147e := do
let .app: Expr → Expr → Expr.app (.app: Expr → Expr → Expr.app (f: Q(«\$α» → «\$α» → «\$α»)f : Q(\$α → \$α → \$α)) (a: Q(«\$α»)a : Q(\$α))) (b: Q(«\$α»)b : Q(\$α)) ← withReducible: {n : Type → Type ?u.5210} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithReducible (whnf: Expr → MetaM Exprwhnf e: ?m.5147e)
| throwError "not min": ?m.8674 ?m.8675throwErrorthrowError "not min": ?m.8674 ?m.8675 "not min"
let _e_eq: «\$e» =Q «\$f» «\$a» «\$b»_e_eq : \$e: «\$α»e =Q \$f: «\$α» → «\$α» → «\$α»f \$a: «\$α»a \$b: «\$α»b := ⟨⟩: «\$e» =Q «\$f» «\$a» «\$b»⟨⟩
let _a: ?m.5462_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(LinearOrder: Type ?u.5448 → Type ?u.5448LinearOrderLinearOrder \$α: ?m.5135 \$α: Type uα) : Q(Type u: ?m.5135Type u))
assumeInstancesCommute
let ⟨_f_eq: «\$f» =Q min_f_eq⟩ ← withDefault: {n : Type → Type ?u.7073} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithDefault <| withNewMCtxDepth: {n : Type → Type ?u.7119} →
[inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → optParam Bool false → n αwithNewMCtxDepth <| assertDefEqQ: {u : Level} →
{α :
let u := u;
Q(Sort u)} →
(a b : Q(«\$α»)) → MetaM (PLift («\$a» =Q «\$b»))assertDefEqQ (u := u: ?m.5135u.succ: Level → Levelsucc) f: Q(«\$α» → «\$α» → «\$α»)f q(min: ?m.5135min)
match ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.5141zα pα: ?m.5144pα a: Q(«\$α»)a, ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.5141zα pα: ?m.5144pα b: Q(«\$α»)b with
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa, .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb => pure: {f : Type ?u.7440 → Type ?u.7439} → [self : Pure f] → {α : Type ?u.7440} → α → f αpure (.positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive q(lt_min: ∀ {α : Type ?u.7471} [inst : LinearOrder α] {a b c : α}, a < b → a < c → a < min b clt_minlt_min \$pa \$pb: ?m.5135 \$pa: 0 < «\$a»palt_min \$pa \$pb: ?m.5135 \$pb: 0 < «\$b»pb))
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa, .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pb: Q(0 ≤ «\$b»)pb => pure: {f : Type ?u.7579 → Type ?u.7578} → [self : Pure f] → {α : Type ?u.7579} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative q(le_min_of_lt_of_le: ∀ {R : Type ?u.7610} [inst : LinearOrder R] {a b c : R}, a < b → a ≤ c → a ≤ min b cle_min_of_lt_of_lele_min_of_lt_of_le \$pa \$pb: ?m.5135 \$pa: 0 < «\$a»pale_min_of_lt_of_le \$pa \$pb: ?m.5135 \$pb: 0 ≤ «\$b»pb))
| .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pa: Q(0 ≤ «\$a»)pa, .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb => pure: {f : Type ?u.7686 → Type ?u.7685} → [self : Pure f] → {α : Type ?u.7686} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative q(le_min_of_le_of_lt: ∀ {R : Type ?u.7717} [inst : LinearOrder R] {a b c : R}, a ≤ b → a < c → a ≤ min b cle_min_of_le_of_ltle_min_of_le_of_lt \$pa \$pb: ?m.5135 \$pa: 0 ≤ «\$a»pale_min_of_le_of_lt \$pa \$pb: ?m.5135 \$pb: 0 < «\$b»pb))
| .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pa: Q(0 ≤ «\$a»)pa, .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pb: Q(0 ≤ «\$b»)pb => pure: {f : Type ?u.7783 → Type ?u.7782} → [self : Pure f] → {α : Type ?u.7783} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative q(le_min: ∀ {α : Type ?u.7814} [inst : LinearOrder α] {a b c : α}, c ≤ a → c ≤ b → c ≤ min a ble_minle_min \$pa \$pb: ?m.5135 \$pa: 0 ≤ «\$a»pale_min \$pa \$pb: ?m.5135 \$pb: 0 ≤ «\$b»pb))
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa, .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pb: Q(«\$b» ≠ 0)pb => pure: {f : Type ?u.7882 → Type ?u.7881} → [self : Pure f] → {α : Type ?u.7882} → α → f αpure (.nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero q(min_ne_of_lt_of_ne: ∀ {R : Type ?u.7913} [inst : LinearOrder R] {a b c : R}, c < a → b ≠ c → min a b ≠ cmin_ne_of_lt_of_nemin_ne_of_lt_of_ne \$pa \$pb: ?m.5135 \$pa: 0 < «\$a»pamin_ne_of_lt_of_ne \$pa \$pb: ?m.5135 \$pb: «\$b» ≠ 0pb))
| .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pa: Q(«\$a» ≠ 0)pa, .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb => pure: {f : Type ?u.7979 → Type ?u.7978} → [self : Pure f] → {α : Type ?u.7979} → α → f αpure (.nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero q(min_ne_of_ne_of_lt: ∀ {R : Type ?u.8010} [inst : LinearOrder R] {a b c : R}, a ≠ c → c < b → min a b ≠ cmin_ne_of_ne_of_ltmin_ne_of_ne_of_lt \$pa \$pb: ?m.5135 \$pa: «\$a» ≠ 0pamin_ne_of_ne_of_lt \$pa \$pb: ?m.5135 \$pb: 0 < «\$b»pb))
| .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pa: Q(«\$a» ≠ 0)pa, .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pb: Q(«\$b» ≠ 0)pb => pure: {f : Type ?u.8073 → Type ?u.8072} → [self : Pure f] → {α : Type ?u.8073} → α → f αpure (.nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero q(min_ne: ∀ {R : Type ?u.8104} [inst : LinearOrder R] {a b c : R}, a ≠ c → b ≠ c → min a b ≠ cmin_nemin_ne \$pa \$pb: ?m.5135 \$pa: «\$a» ≠ 0pamin_ne \$pa \$pb: ?m.5135 \$pb: «\$b» ≠ 0pb))
| _, _ => pure: {f : Type ?u.8154 → Type ?u.8153} → [self : Pure f] → {α : Type ?u.8154} → α → f αpure .none: {u : Level} → {α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Strictness zα pα e.none

/-- Extension for the `max` operator. The `max` of two numbers is nonnegative if at least one
is nonnegative, strictly positive if at least one is positive, and nonzero if both are nonzero. -/
@[positivity max: {α : Type ?u.25669} → [self : Max α] → α → α → αmax _: ?m.25670_ _: ?m.25670_] def evalMax: PositivityExtevalMax : PositivityExt: TypePositivityExt where eval {u: ?m.15887u α: ?m.15890α} zα: ?m.15893zα pα: ?m.15896pα e: ?m.15899e := do
let .app: Expr → Expr → Expr.app (.app: Expr → Expr → Expr.app (f: Q(«\$α» → «\$α» → «\$α»)f : Q(\$α → \$α → \$α)) (a: Q(«\$α»)a : Q(\$α))) (b: Q(«\$α»)b : Q(\$α)) ← withReducible: {n : Type → Type ?u.15962} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithReducible (whnf: Expr → MetaM Exprwhnf e: ?m.15899e)
| throwError "not max": ?m.19545 ?m.19546throwErrorthrowError "not max": ?m.19545 ?m.19546 "not max"
let _e_eq: «\$e» =Q «\$f» «\$a» «\$b»_e_eq : \$e: «\$α»e =Q \$f: «\$α» → «\$α» → «\$α»f \$a: «\$α»a \$b: «\$α»b := ⟨⟩: «\$e» =Q «\$f» «\$a» «\$b»⟨⟩
let _a: ?m.16214_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(LinearOrder: Type ?u.16200 → Type ?u.16200LinearOrderLinearOrder \$α: ?m.15887 \$α: Type uα) : Q(Type u: Type (u+1)Type u))
assumeInstancesCommute
let ⟨_f_eq: «\$f» =Q max_f_eq⟩ ← withDefault: {n : Type → Type ?u.17825} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithDefault <| withNewMCtxDepth: {n : Type → Type ?u.17871} →
[inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → optParam Bool false → n αwithNewMCtxDepth <| assertDefEqQ: {u : Level} →
{α :
let u := u;
Q(Sort u)} →
(a b : Q(«\$α»)) → MetaM (PLift («\$a» =Q «\$b»))assertDefEqQ (u := u: ?m.15887u.succ: Level → Levelsucc) f: Q(«\$α» → «\$α» → «\$α»)f q(max: ?m.15887max)
let result: Strictness zα pα eresult : Strictness: {u : Level} → {α : Q(Type u)} → Q(Zero «\$α») → Q(PartialOrder «\$α») → Q(«\$α») → TypeStrictness zα: ?m.15893zα pα: ?m.15896pα e: ?m.15899e ← catchNone: {u : Level} →
{α : Q(Type u)} →
{zα : Q(Zero «\$α»)} →
{pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → MetaM (Strictness zα pα e) → MetaM (Strictness zα pα e)catchNone do
let ra: ?m.18167ra ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.15893zα pα: ?m.15896pα a: Q(«\$α»)a
match ra: ?m.18167ra with
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa => pure: {f : Type ?u.18184 → Type ?u.18183} → [self : Pure f] → {α : Type ?u.18184} → α → f αpure (.positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive q(lt_max_of_lt_left: ∀ {α : Type ?u.18215} [inst : LinearOrder α] {a b c : α}, a < b → a < max b clt_max_of_lt_leftlt_max_of_lt_left \$pa: ?m.15887 \$pa: 0 < «\$a»pa))
| .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pa: Q(0 ≤ «\$a»)pa => pure: {f : Type ?u.18309 → Type ?u.18308} → [self : Pure f] → {α : Type ?u.18309} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative q(le_max_of_le_left: ∀ {α : Type ?u.18340} [inst : LinearOrder α] {a b c : α}, a ≤ b → a ≤ max b cle_max_of_le_leftle_max_of_le_left \$pa: ?m.15887 \$pa: 0 ≤ «\$a»pa))
-- If `a ≠ 0`, we might prove `max a b ≠ 0` if `b ≠ 0` but we don't want to evaluate
-- `b` before having ruled out `0 < a`, for performance. So we do that in the second branch
-- of the `orElse'`.
| _ => pure: {f : Type ?u.18393 → Type ?u.18392} → [self : Pure f] → {α : Type ?u.18393} → α → f αpure .none: {u : Level} → {α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Strictness zα pα e.none
orElse: {u : Level} →
{α : Q(Type u)} →
{zα : Q(Zero «\$α»)} →
{pα : Q(PartialOrder «\$α»)} →
{e : Q(«\$α»)} → Strictness zα pα e → MetaM (Strictness zα pα e) → MetaM (Strictness zα pα e)orElse result: Strictness zα pα eresult do
let rb: ?m.18649rb ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.15893zα pα: ?m.15896pα b: Q(«\$α»)b
match rb: ?m.18649rb with
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb => pure: {f : Type ?u.18666 → Type ?u.18665} → [self : Pure f] → {α : Type ?u.18666} → α → f αpure (.positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive q(lt_max_of_lt_right: ∀ {α : Type ?u.18699} [inst : LinearOrder α] {a b c : α}, a < c → a < max b clt_max_of_lt_rightlt_max_of_lt_right \$pb: ?m.15887 \$pb: 0 < «\$b»pb))
| .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pb: Q(0 ≤ «\$b»)pb => pure: {f : Type ?u.18810 → Type ?u.18809} → [self : Pure f] → {α : Type ?u.18810} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative q(le_max_of_le_right: ∀ {α : Type ?u.18841} [inst : LinearOrder α] {a b c : α}, a ≤ c → a ≤ max b cle_max_of_le_rightle_max_of_le_right \$pb: ?m.15887 \$pb: 0 ≤ «\$b»pb))
| .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pb: Q(«\$b» ≠ 0)pb => do
match ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.15893zα pα: ?m.15896pα a: Q(«\$α»)a with
| .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pa: Q(«\$a» ≠ 0)pa => pure: {f : Type ?u.18967 → Type ?u.18966} → [self : Pure f] → {α : Type ?u.18967} → α → f αpure (.nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero q(max_ne: ∀ {R : Type ?u.18998} [inst : LinearOrder R] {a b c : R}, a ≠ c → b ≠ c → max a b ≠ cmax_nemax_ne \$pa \$pb: ?m.15887 \$pa: «\$a» ≠ 0pamax_ne \$pa \$pb: ?m.15887 \$pb: «\$b» ≠ 0pb))
| _ => pure: {f : Type ?u.19044 → Type ?u.19043} → [self : Pure f] → {α : Type ?u.19044} → α → f αpure .none: {u : Level} → {α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Strictness zα pα e.none
| _ => pure: {f : Type ?u.19210 → Type ?u.19209} → [self : Pure f] → {α : Type ?u.19210} → α → f αpure .none: {u : Level} → {α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Strictness zα pα e.none

/-- The `positivity` extension which identifies expressions of the form `a + b`,
such that `positivity` successfully recognises both `a` and `b`. -/
@[positivity _: ?m.37274_ + _: ?m.37277_, Add.add: {α : Type ?u.37295} → [self : Add α] → α → α → αAdd.add _: ?m.37296_ _: ?m.37296_] def evalAdd: PositivityExtevalAdd : PositivityExt: TypePositivityExt where eval {u: ?m.25693u α: ?m.25696α} zα: ?m.25699zα pα: ?m.25702pα e: ?m.25705e := do
let .app: Expr → Expr → Expr.app (.app: Expr → Expr → Expr.app (f: Q(«\$α» → «\$α» → «\$α»)f : Q(\$α → \$α → \$α)) (a: Q(«\$α»)a : Q(\$α))) (b: Q(«\$α»)b : Q(\$α)) ← withReducible: {n : Type → Type ?u.25768} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithReducible (whnf: Expr → MetaM Exprwhnf e: ?m.25705e)
| throwError "not +": ?m.30239 ?m.30240throwErrorthrowError "not +": ?m.30239 ?m.30240 "not +"
let _e_eq: «\$e» =Q «\$f» «\$a» «\$b»_e_eq : \$e: «\$α»e =Q \$f: «\$α» → «\$α» → «\$α»f \$a: «\$α»a \$b: «\$α»b := ⟨⟩: «\$e» =Q «\$f» «\$a» «\$b»⟨⟩
let _a: ?m.26020_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(AddZeroClass: Type ?u.26006 → Type ?u.26006AddZeroClassAddZeroClass \$α: ?m.25693 \$α: Type uα) : Q(Type u: ?m.25693Type u))
assumeInstancesCommute
let ⟨_f_eq: «\$f» =Q HAdd.hAdd_f_eq⟩ ← withDefault: {n : Type → Type ?u.27404} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithDefault <| withNewMCtxDepth: {n : Type → Type ?u.27450} →
[inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → optParam Bool false → n αwithNewMCtxDepth <| assertDefEqQ: {u : Level} →
{α :
let u := u;
Q(Sort u)} →
(a b : Q(«\$α»)) → MetaM (PLift («\$a» =Q «\$b»))assertDefEqQ (u := u: ?m.25693u.succ: Level → Levelsucc) f: Q(«\$α» → «\$α» → «\$α»)f q(HAdd.hAdd: ?m.25693HAdd.hAdd)
let ra: ?m.27825ra ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.25699zα pα: ?m.25702pα a: Q(«\$α»)a; let rb: ?m.27877rb ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.25699zα pα: ?m.25702pα b: Q(«\$α»)b
match ra: ?m.27825ra, rb: ?m.27877rb with
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa, .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb =>
let _a: ?m.28237_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(CovariantClass: (M : Type ?u.27962) → (N : Type ?u.27961) → (M → N → N) → (N → N → Prop) → PropCovariantClassCovariantClass \$α \$α (·+·) (·<·): ?m.25693 \$α: Type uαCovariantClass \$α \$α (·+·) (·<·): ?m.25693 \$α: Type uαCovariantClass \$α \$α (·+·) (·<·): ?m.25693 (·+·): «\$α» → «\$α» → «\$α»(·+·)CovariantClass \$α \$α (·+·) (·<·): ?m.25693 (·<·): «\$α» → «\$α» → Prop(·<·)) : Q(Prop: TypeProp))
pure: {f : Type ?u.28240 → Type ?u.28239} → [self : Pure f] → {α : Type ?u.28240} → α → f αpure (.positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive q(add_pos: ∀ {α : Type ?u.28271} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b : α}, 0 < a → 0 < b → 0 < a + badd_posadd_pos \$pa \$pb: ?m.25693 \$pa: 0 < «\$a»paadd_pos \$pa \$pb: ?m.25693 \$pb: 0 < «\$b»pb))
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa, .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pb: Q(0 ≤ «\$b»)pb =>
let _a: ?m.28755_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(CovariantClass: (M : Type ?u.28483) → (N : Type ?u.28482) → (M → N → N) → (N → N → Prop) → PropCovariantClassCovariantClass \$α \$α (swap (·+·)) (·<·): ?m.25693 \$α: Type uαCovariantClass \$α \$α (swap (·+·)) (·<·): ?m.25693 \$α: Type uαCovariantClass \$α \$α (swap (·+·)) (·<·): ?m.25693 (swap: {α : Sort ?u.28486} →
{β : Sort ?u.28485} → {φ : α → β → Sort ?u.28484} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x yswapCovariantClass \$α \$α (swap (·+·)) (·<·): ?m.25693 (·+·): «\$α» → «\$α» → «\$α»(·+·)CovariantClass \$α \$α (swap (·+·)) (·<·): ?m.25693) (·<·): «\$α» → «\$α» → Prop(·<·)) : Q(Prop: TypeProp))
pure: {f : Type ?u.28758 → Type ?u.28757} → [self : Pure f] → {α : Type ?u.28758} → α → f αpure (.positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive q(lt_add_of_pos_of_le: ∀ {α : Type ?u.28789} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, 0 < a → b ≤ c → b < a + clt_add_of_pos_of_lelt_add_of_pos_of_le \$pa \$pb: ?m.25693 \$pa: 0 < «\$a»palt_add_of_pos_of_le \$pa \$pb: ?m.25693 \$pb: 0 ≤ «\$b»pb))
| .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pa: Q(0 ≤ «\$a»)pa, .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb =>
let _a: ?m.29212_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(CovariantClass: (M : Type ?u.28962) → (N : Type ?u.28961) → (M → N → N) → (N → N → Prop) → PropCovariantClassCovariantClass \$α \$α (·+·) (·<·): ?m.25693 \$α: Type uαCovariantClass \$α \$α (·+·) (·<·): ?m.25693 \$α: Type uαCovariantClass \$α \$α (·+·) (·<·): ?m.25693 (·+·): «\$α» → «\$α» → «\$α»(·+·)CovariantClass \$α \$α (·+·) (·<·): ?m.25693 (·<·): «\$α» → «\$α» → Prop(·<·)) : Q(Prop: TypeProp))
pure: {f : Type ?u.29215 → Type ?u.29214} → [self : Pure f] → {α : Type ?u.29215} → α → f αpure (.positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive q(lt_add_of_le_of_pos: ∀ {α : Type ?u.29246} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1] {a b c : α}, b ≤ c → 0 < a → b < c + alt_add_of_le_of_poslt_add_of_le_of_pos \$pa \$pb: ?m.25693 \$pa: 0 ≤ «\$a»palt_add_of_le_of_pos \$pa \$pb: ?m.25693 \$pb: 0 < «\$b»pb))
| .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pa: Q(0 ≤ «\$a»)pa, .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pb: Q(0 ≤ «\$b»)pb =>
let _a: ?m.29682_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(CovariantClass: (M : Type ?u.29410) → (N : Type ?u.29409) → (M → N → N) → (N → N → Prop) → PropCovariantClassCovariantClass \$α \$α (·+·) (·≤·): ?m.25693 \$α: Type uαCovariantClass \$α \$α (·+·) (·≤·): ?m.25693 \$α: Type uαCovariantClass \$α \$α (·+·) (·≤·): ?m.25693 (·+·): «\$α» → «\$α» → «\$α»(·+·)CovariantClass \$α \$α (·+·) (·≤·): ?m.25693 (·≤·): «\$α» → «\$α» → Prop(·≤·)) : Q(Prop: TypeProp))
pure: {f : Type ?u.29685 → Type ?u.29684} → [self : Pure f] → {α : Type ?u.29685} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative q(add_nonneg: ∀ {α : Type ?u.29716} [inst : AddZeroClass α] [inst_1 : Preorder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {a b : α}, 0 ≤ a → 0 ≤ b → 0 ≤ a + badd_nonnegadd_nonneg \$pa \$pb: ?m.25693 \$pa: 0 ≤ «\$a»paadd_nonneg \$pa \$pb: ?m.25693 \$pb: 0 ≤ «\$b»pb))
| _, _ => failure: {f : Type ?u.29824 → Type ?u.29823} → [self : Alternative f] → {α : Type ?u.29824} → f αfailure

private theorem mul_nonneg_of_pos_of_nonneg: ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b : α}, 0 < a → 0 ≤ b → 0 ≤ a * bmul_nonneg_of_pos_of_nonneg [OrderedSemiring: Type ?u.37331 → Type ?u.37331OrderedSemiring α: ?m.37328α] {a: αa b: αb : α: ?m.37328α}
(ha: 0 < aha : 0: ?m.373400 < a: αa) (hb: 0 ≤ bhb : 0: ?m.376840 ≤ b: αb) : 0: ?m.377970 ≤ a: αa * b: αb :=
mul_nonneg: ∀ {α : Type ?u.38180} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulMono α],
0 ≤ a → 0 ≤ b → 0 ≤ a * bmul_nonneg ha: 0 < aha.le: ∀ {α : Type ?u.38534} [inst : Preorder α] {a b : α}, a < b → a ≤ ble hb: 0 ≤ bhb

private theorem mul_nonneg_of_nonneg_of_pos: ∀ {α : Type u_1} [inst : OrderedSemiring α] {a b : α}, 0 ≤ a → 0 < b → 0 ≤ a * bmul_nonneg_of_nonneg_of_pos [OrderedSemiring: Type ?u.38662 → Type ?u.38662OrderedSemiring α: ?m.38659α] {a: αa b: αb : α: ?m.38659α}
(ha: 0 ≤ aha : 0: ?m.386710 ≤ a: αa) (hb: 0 < bhb : 0: ?m.390150 < b: αb) : 0: ?m.391280 ≤ a: αa * b: αb :=
mul_nonneg: ∀ {α : Type ?u.39511} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulMono α],
0 ≤ a → 0 ≤ b → 0 ≤ a * bmul_nonneg ha: 0 ≤ aha hb: 0 < bhb.le: ∀ {α : Type ?u.39867} [inst : Preorder α] {a b : α}, a < b → a ≤ ble

private theorem mul_ne_zero_of_ne_zero_of_pos: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : NoZeroDivisors α] {a b : α}, a ≠ 0 → 0 < b → a * b ≠ 0mul_ne_zero_of_ne_zero_of_pos [OrderedSemiring: Type ?u.39992 → Type ?u.39992OrderedSemiring α: ?m.39989α] [NoZeroDivisors: (M₀ : Type ?u.39995) → [inst : Mul M₀] → [inst : Zero M₀] → PropNoZeroDivisors α: ?m.39989α]
{a: αa b: αb : α: ?m.39989α} (ha: a ≠ 0ha : a: αa ≠ 0: ?m.403930) (hb: 0 < bhb : 0: ?m.405740 < b: αb) : a: αa * b: αb ≠ 0: ?m.410240 :=
mul_ne_zero: ∀ {M₀ : Type ?u.41041} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : NoZeroDivisors M₀] {a b : M₀},
a ≠ 0 → b ≠ 0 → a * b ≠ 0mul_ne_zero ha: a ≠ 0ha (ne_of_gt: ∀ {α : Type ?u.41139} [inst : Preorder α] {a b : α}, b < a → a ≠ bne_of_gt hb: 0 < bhb)

private theorem mul_ne_zero_of_pos_of_ne_zero: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : NoZeroDivisors α] {a b : α}, 0 < a → b ≠ 0 → a * b ≠ 0mul_ne_zero_of_pos_of_ne_zero [OrderedSemiring: Type ?u.41662 → Type ?u.41662OrderedSemiring α: ?m.41659α] [NoZeroDivisors: (M₀ : Type ?u.41665) → [inst : Mul M₀] → [inst : Zero M₀] → PropNoZeroDivisors α: ?m.41659α]
{a: αa b: αb : α: ?m.41659α} (ha: 0 < aha : 0: ?m.420620 < a: αa) (hb: b ≠ 0hb : b: αb ≠ 0: ?m.423550) : a: αa * b: αb ≠ 0: ?m.426940 :=
mul_ne_zero: ∀ {M₀ : Type ?u.42711} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : NoZeroDivisors M₀] {a b : M₀},
a ≠ 0 → b ≠ 0 → a * b ≠ 0mul_ne_zero (ne_of_gt: ∀ {α : Type ?u.42808} [inst : Preorder α] {a b : α}, b < a → a ≠ bne_of_gt ha: 0 < aha) hb: b ≠ 0hb

/-- The `positivity` extension which identifies expressions of the form `a * b`,
such that `positivity` successfully recognises both `a` and `b`. -/
@[positivity _: ?m.53628_ * _: ?m.53631_, Mul.mul: {α : Type ?u.53651} → [self : Mul α] → α → α → αMul.mul _: ?m.53652_ _: ?m.53652_] def evalMul: PositivityExtevalMul : PositivityExt: TypePositivityExt where eval {u: ?m.43329u α: ?m.43332α} zα: ?m.43335zα pα: ?m.43338pα e: ?m.43341e := do
let .app: Expr → Expr → Expr.app (.app: Expr → Expr → Expr.app (f: Q(«\$α» → «\$α» → «\$α»)f : Q(\$α → \$α → \$α)) (a: Q(«\$α»)a : Q(\$α))) (b: Q(«\$α»)b : Q(\$α)) ← withReducible: {n : Type → Type ?u.43404} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithReducible (whnf: Expr → MetaM Exprwhnf e: ?m.43341e)
| throwError "not *": ?m.46614 ?m.46615throwErrorthrowError "not *": ?m.46614 ?m.46615 "not *"
let _e_eq: «\$e» =Q «\$f» «\$a» «\$b»_e_eq : \$e: «\$α»e =Q \$f: «\$α» → «\$α» → «\$α»f \$a: «\$α»a \$b: «\$α»b := ⟨⟩: «\$e» =Q «\$f» «\$a» «\$b»⟨⟩
let _a: ?m.43656_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(StrictOrderedSemiring: Type ?u.43642 → Type ?u.43642StrictOrderedSemiringStrictOrderedSemiring \$α: ?m.43329 \$α: Type uα) : Q(Type u: Type (u+1)Type u))
assumeInstancesCommute
let ⟨_f_eq: «\$f» =Q HMul.hMul_f_eq⟩ ← withDefault: {n : Type → Type ?u.43993} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithDefault <| withNewMCtxDepth: {n : Type → Type ?u.44039} →
[inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → optParam Bool false → n αwithNewMCtxDepth <| assertDefEqQ: {u : Level} →
{α :
let u := u;
Q(Sort u)} →
(a b : Q(«\$α»)) → MetaM (PLift («\$a» =Q «\$b»))assertDefEqQ (u := u: ?m.43329u.succ: Level → Levelsucc) f: Q(«\$α» → «\$α» → «\$α»)f q(HMul.hMul: {α : Type ?u.44091} → {β : Type ?u.44090} → {γ : outParam (Type ?u.44089)} → [self : HMul α β γ] → α → β → γHMul.hMul)
let ra: ?m.44348ra ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.43335zα pα: ?m.43338pα a: Q(«\$α»)a; let rb: ?m.44400rb ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.43335zα pα: ?m.43338pα b: Q(«\$α»)b
match ra: ?m.44348ra, rb: ?m.44400rb with
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa, .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb => pure: {f : Type ?u.44436 → Type ?u.44435} → [self : Pure f] → {α : Type ?u.44436} → α → f αpure (.positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive q(mul_pos: ∀ {α : Type ?u.44467} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulStrictMono α],
0 < a → 0 < b → 0 < a * bmul_posmul_pos \$pa \$pb: ?m.43329 \$pa: 0 < «\$a»pamul_pos \$pa \$pb: ?m.43329 \$pb: 0 < «\$b»pb))
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa, .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pb: Q(0 ≤ «\$b»)pb => pure: {f : Type ?u.44841 → Type ?u.44840} → [self : Pure f] → {α : Type ?u.44841} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative q(mul_nonneg_of_pos_of_nonneg: ∀ {α : Type ?u.44872} [inst : OrderedSemiring α] {a b : α}, 0 < a → 0 ≤ b → 0 ≤ a * bmul_nonneg_of_pos_of_nonnegmul_nonneg_of_pos_of_nonneg \$pa \$pb: ?m.43329 \$pa: 0 < «\$a»pamul_nonneg_of_pos_of_nonneg \$pa \$pb: ?m.43329 \$pb: 0 ≤ «\$b»pb))
| .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pa: Q(0 ≤ «\$a»)pa, .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb => pure: {f : Type ?u.44983 → Type ?u.44982} → [self : Pure f] → {α : Type ?u.44983} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative q(mul_nonneg_of_nonneg_of_pos: ∀ {α : Type ?u.45014} [inst : OrderedSemiring α] {a b : α}, 0 ≤ a → 0 < b → 0 ≤ a * bmul_nonneg_of_nonneg_of_posmul_nonneg_of_nonneg_of_pos \$pa \$pb: ?m.43329 \$pa: 0 ≤ «\$a»pamul_nonneg_of_nonneg_of_pos \$pa \$pb: ?m.43329 \$pb: 0 < «\$b»pb))
| .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pa: Q(0 ≤ «\$a»)pa, .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pb: Q(0 ≤ «\$b»)pb => pure: {f : Type ?u.45064 → Type ?u.45063} → [self : Pure f] → {α : Type ?u.45064} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative q(mul_nonneg: ∀ {α : Type ?u.45095} {a b : α} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulMono α],
0 ≤ a → 0 ≤ b → 0 ≤ a * bmul_nonnegmul_nonneg \$pa \$pb: ?m.43329 \$pa: 0 ≤ «\$a»pamul_nonneg \$pa \$pb: ?m.43329 \$pb: 0 ≤ «\$b»pb))
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa, .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pb: Q(«\$b» ≠ 0)pb =>
let _a: ?m.45437_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(NoZeroDivisors: (M₀ : Type ?u.45292) → [inst : Mul M₀] → [inst : Zero M₀] → PropNoZeroDivisorsNoZeroDivisors \$α: ?m.43329 \$α: Type uα) : Q(Prop: TypeProp))
pure: {f : Type ?u.45440 → Type ?u.45439} → [self : Pure f] → {α : Type ?u.45440} → α → f αpure (.nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero q(mul_ne_zero_of_pos_of_ne_zero: ∀ {α : Type ?u.45471} [inst : OrderedSemiring α] [inst_1 : NoZeroDivisors α] {a b : α}, 0 < a → b ≠ 0 → a * b ≠ 0mul_ne_zero_of_pos_of_ne_zeromul_ne_zero_of_pos_of_ne_zero \$pa \$pb: ?m.43329 \$pa: 0 < «\$a»pamul_ne_zero_of_pos_of_ne_zero \$pa \$pb: ?m.43329 \$pb: «\$b» ≠ 0pb))
| .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pa: Q(«\$a» ≠ 0)pa, .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb =>
let _a: ?m.45668_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(NoZeroDivisors: (M₀ : Type ?u.45659) → [inst : Mul M₀] → [inst : Zero M₀] → PropNoZeroDivisorsNoZeroDivisors \$α: ?m.43329 \$α: Type uα) : Q(Prop: TypeProp))
pure: {f : Type ?u.45671 → Type ?u.45670} → [self : Pure f] → {α : Type ?u.45671} → α → f αpure (.nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero q(mul_ne_zero_of_ne_zero_of_pos: ∀ {α : Type ?u.45702} [inst : OrderedSemiring α] [inst_1 : NoZeroDivisors α] {a b : α}, a ≠ 0 → 0 < b → a * b ≠ 0mul_ne_zero_of_ne_zero_of_posmul_ne_zero_of_ne_zero_of_pos \$pa \$pb: ?m.43329 \$pa: «\$a» ≠ 0pamul_ne_zero_of_ne_zero_of_pos \$pa \$pb: ?m.43329 \$pb: 0 < «\$b»pb))
| .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pa: Q(«\$a» ≠ 0)pa, .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pb: Q(«\$b» ≠ 0)pb =>
let _a: ?m.45878_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(NoZeroDivisors: (M₀ : Type ?u.45869) → [inst : Mul M₀] → [inst : Zero M₀] → PropNoZeroDivisorsNoZeroDivisors \$α: ?m.43329 \$α: Type uα) : Q(Prop: TypeProp))
pure: {f : Type ?u.45881 → Type ?u.45880} → [self : Pure f] → {α : Type ?u.45881} → α → f αpure (.nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero (q(mul_ne_zero: ∀ {M₀ : Type ?u.45912} [inst : Mul M₀] [inst_1 : Zero M₀] [inst_2 : NoZeroDivisors M₀] {a b : M₀},
a ≠ 0 → b ≠ 0 → a * b ≠ 0mul_ne_zeromul_ne_zero \$pa \$pb: ?m.43329 \$pa: «\$a» ≠ 0pamul_ne_zero \$pa \$pb: ?m.43329 \$pb: «\$b» ≠ 0pb)))
| _, _ => pure: {f : Type ?u.46160 → Type ?u.46159} → [self : Pure f] → {α : Type ?u.46160} → α → f αpure .none: {u : Level} → {α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Strictness zα pα e.none

private lemma int_div_self_pos: ∀ {a : ℤ}, 0 < a → 0 < a / aint_div_self_pos {a: ℤa : ℤ: Typeℤ} (ha: 0 < aha : 0: ?m.536880 < a: ℤa) : 0: ?m.537250 < a: ℤa / a: ℤa :=
byGoals accomplished! 🐙 a: ℤha: 0 < a0 < a / a{a: ℤha: 0 < a0 < a / a a: ℤha: 0 < a0 < a / arw [a: ℤha: 0 < a0 < a / aInt.ediv_self: ∀ {a : ℤ}, a ≠ 0 → a / a = 1Int.ediv_self ha: 0 < aha.ne': ∀ {α : Type ?u.53809} [inst : Preorder α] {x y : α}, x < y → y ≠ xne'a: ℤha: 0 < a0 < 1]a: ℤha: 0 < a0 < 1;a: ℤha: 0 < a0 < 1 a: ℤha: 0 < a0 < a / aexact zero_lt_one: ∀ {α : Type ?u.53877} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
[inst_4 : NeZero 1], 0 < 1zero_lt_oneGoals accomplished! 🐙 }Goals accomplished! 🐙

private lemma int_div_nonneg_of_pos_of_nonneg: ∀ {a b : ℤ}, 0 < a → 0 ≤ b → 0 ≤ a / bint_div_nonneg_of_pos_of_nonneg {a: ℤa b: ℤb : ℤ: Typeℤ} (ha: 0 < aha : 0: ?m.545690 < a: ℤa) (hb: 0 ≤ bhb : 0: ?m.546060 ≤ b: ℤb) : 0: ?m.546350 ≤ a: ℤa / b: ℤb :=
Int.ediv_nonneg: ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ a / bInt.ediv_nonneg ha: 0 < aha.le: ∀ {α : Type ?u.54732} [inst : Preorder α] {a b : α}, a < b → a ≤ ble hb: 0 ≤ bhb

private lemma int_div_nonneg_of_nonneg_of_pos: ∀ {a b : ℤ}, 0 ≤ a → 0 < b → 0 ≤ a / bint_div_nonneg_of_nonneg_of_pos {a: ℤa b: ℤb : ℤ: Typeℤ} (ha: 0 ≤ aha : 0: ?m.547990 ≤ a: ℤa) (hb: 0 < bhb : 0: ?m.548360 < b: ℤb) : 0: ?m.548650 ≤ a: ℤa / b: ℤb :=
Int.ediv_nonneg: ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ a / bInt.ediv_nonneg ha: 0 ≤ aha hb: 0 < bhb.le: ∀ {α : Type ?u.54962} [inst : Preorder α] {a b : α}, a < b → a ≤ ble

private lemma int_div_nonneg_of_pos_of_pos: ∀ {a b : ℤ}, 0 < a → 0 < b → 0 ≤ a / bint_div_nonneg_of_pos_of_pos {a: ℤa b: ℤb : ℤ: Typeℤ} (ha: 0 < aha : 0: ?m.550290 < a: ℤa) (hb: 0 < bhb : 0: ?m.550660 < b: ℤb) : 0: ?m.550920 ≤ a: ℤa / b: ℤb :=
Int.ediv_nonneg: ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ a / bInt.ediv_nonneg ha: 0 < aha.le: ∀ {α : Type ?u.55192} [inst : Preorder α] {a b : α}, a < b → a ≤ ble hb: 0 < bhb.le: ∀ {α : Type ?u.55248} [inst : Preorder α] {a b : α}, a < b → a ≤ ble

/-- The `positivity` extension which identifies expressions of the form `a / b`,
where `a` and `b` are integers. -/
@[positivity (_: ℤ_ : ℤ) / (_: ℤ_ : ℤ)] def evalIntDiv: PositivityExtevalIntDiv : PositivityExt: TypePositivityExt where eval {_u: ?m.55267_u _α: ?m.55270_α} zα: ?m.55273zα pα: ?m.55276pα e: ?m.55279e := do
let .app: Expr → Expr → Expr.app (.app: Expr → Expr → Expr.app f: Exprf (a: Q(ℤ)a : Q(ℤ))) (b: Q(ℤ)b : Q(ℤ)) ← withReducible: {n : Type → Type ?u.55342} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithReducible (whnf: Expr → MetaM Exprwhnf e: ?m.55279e) | throwError "not /": ?m.57039 ?m.57040throwErrorthrowError "not /": ?m.57039 ?m.57040 "not /"
let ra: ?m.55552ra ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.55273zα pα: ?m.55276pα a: Q(ℤ)a; let rb: ?m.55604rb ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.55273zα pα: ?m.55276pα b: Q(ℤ)b
guard: {f : Type → Type ?u.55848} → [inst : Alternative f] → (p : Prop) → [inst : Decidable p] → f Unitguard <|← withDefault: {n : Type → Type ?u.55648} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithDefault <| withNewMCtxDepth: {n : Type → Type ?u.55694} →
[inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → optParam Bool false → n αwithNewMCtxDepth <| isDefEq: Expr → Expr → MetaM BoolisDefEq f: Exprf q(HDiv.hDiv: {α : Type ?u.55754} → {β : Type ?u.55753} → {γ : outParam (Type ?u.55752)} → [self : HDiv α β γ] → α → β → γHDiv.hDiv (α := ℤ: Typeℤ) (β := ℤ: Typeℤ))
match ra: ?m.55552ra, rb: ?m.55604rb with
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa, .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb =>
have pa': Q(0 < «\$a»)pa' : Q(0: ?m.560090 < \$a: ℤa) := pa: Q(0 < «\$a»)pa
have pb': Q(0 < «\$b»)pb' : Q(0: ?m.560490 < \$b: ℤb) := pb: Q(0 < «\$b»)pb
if pa: Q(0 < «\$a»)pa == pb: Q(0 < «\$b»)pb then  -- Only attempts to prove `0 < a / a`, otherwise falls back to `0 ≤ a / b`
pure: {f : Type ?u.56149 → Type ?u.56148} → [self : Pure f] → {α : Type ?u.56149} → α → f αpure (.positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive (q(int_div_self_pos: ∀ {a : ℤ}, 0 < a → 0 < a / aint_div_self_pos \$pa': 0 < «\$a»pa') : Expr: TypeExpr))
else
pure: {f : Type ?u.56218 → Type ?u.56217} → [self : Pure f] → {α : Type ?u.56218} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative (q(int_div_nonneg_of_pos_of_pos: ∀ {a b : ℤ}, 0 < a → 0 < b → 0 ≤ a / bint_div_nonneg_of_pos_of_pos \$pa': 0 < «\$a»pa' \$pb': 0 < «\$b»pb') : Expr: TypeExpr))
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa, .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pb: Q(0 ≤ «\$b»)pb =>
have pa': Q(0 < «\$a»)pa' : Q(0: ?m.563030 < \$a: ℤa) := pa: Q(0 < «\$a»)pa
have pb': Q(0 ≤ «\$b»)pb' : Q(0: ?m.563320 ≤ \$b: ℤb) := pb: Q(0 ≤ «\$b»)pb
pure: {f : Type ?u.56359 → Type ?u.56358} → [self : Pure f] → {α : Type ?u.56359} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative (q(int_div_nonneg_of_pos_of_nonneg: ∀ {a b : ℤ}, 0 < a → 0 ≤ b → 0 ≤ a / bint_div_nonneg_of_pos_of_nonneg \$pa': 0 < «\$a»pa' \$pb': 0 ≤ «\$b»pb') : Expr: TypeExpr))
| .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pa: Q(0 ≤ «\$a»)pa, .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb =>
have pa': Q(0 ≤ «\$a»)pa' : Q(0: ?m.564430 ≤ \$a: ℤa) := pa: Q(0 ≤ «\$a»)pa
have pb': Q(0 < «\$b»)pb' : Q(0: ?m.564720 < \$b: ℤb) := pb: Q(0 < «\$b»)pb
pure: {f : Type ?u.56496 → Type ?u.56495} → [self : Pure f] → {α : Type ?u.56496} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative (q(int_div_nonneg_of_nonneg_of_pos: ∀ {a b : ℤ}, 0 ≤ a → 0 < b → 0 ≤ a / bint_div_nonneg_of_nonneg_of_pos \$pa': 0 ≤ «\$a»pa' \$pb': 0 < «\$b»pb') : Expr: TypeExpr))
| .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pa: Q(0 ≤ «\$a»)pa, .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pb: Q(0 ≤ «\$b»)pb =>
have pa': Q(0 ≤ «\$a»)pa' : Q(0: ?m.565760 ≤ \$a: ℤa) := pa: Q(0 ≤ «\$a»)pa
have pb': Q(0 ≤ «\$b»)pb' : Q(0: ?m.566050 ≤ \$b: ℤb) := pb: Q(0 ≤ «\$b»)pb
pure: {f : Type ?u.56629 → Type ?u.56628} → [self : Pure f] → {α : Type ?u.56629} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative (q(Int.ediv_nonneg: ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → 0 ≤ a / bInt.ediv_nonneg \$pa': 0 ≤ «\$a»pa' \$pb': 0 ≤ «\$b»pb') : Expr: TypeExpr))
| _, _ => pure: {f : Type ?u.56690 → Type ?u.56689} → [self : Pure f] → {α : Type ?u.56690} → α → f αpure .none: {u : Level} → {α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Strictness zα pα e.none

section LinearOrderedSemifield
variable [LinearOrderedSemifield: Type ?u.63074 → Type ?u.63074LinearOrderedSemifield R: ?m.63083R] {a: Ra b: Rb : R: ?m.63071R}

private lemma div_nonneg_of_pos_of_nonneg: ∀ {R : Type u_1} [inst : LinearOrderedSemifield R] {a b : R}, 0 < a → 0 ≤ b → 0 ≤ a / bdiv_nonneg_of_pos_of_nonneg (ha: 0 < aha : 0: ?m.630950 < a: Ra) (hb: 0 ≤ bhb : 0: ?m.632510 ≤ b: Rb) : 0: ?m.633320 ≤ a: Ra / b: Rb :=
div_nonneg: ∀ {α : Type ?u.63423} [inst : LinearOrderedSemifield α] {a b : α}, 0 ≤ a → 0 ≤ b → 0 ≤ a / bdiv_nonneg ha: 0 < aha.le: ∀ {α : Type ?u.63467} [inst : Preorder α] {a b : α}, a < b → a ≤ ble hb: 0 ≤ bhb

private lemma div_nonneg_of_nonneg_of_pos: ∀ {R : Type u_1} [inst : LinearOrderedSemifield R] {a b : R}, 0 ≤ a → 0 < b → 0 ≤ a / bdiv_nonneg_of_nonneg_of_pos (ha: 0 ≤ aha : 0: ?m.635730 ≤ a: Ra) (hb: 0 < bhb : 0: ?m.637290 < b: Rb) : 0: ?m.638100 ≤ a: Ra / b: Rb :=
div_nonneg: ∀ {α : Type ?u.63901} [inst : LinearOrderedSemifield α] {a b : α}, 0 ≤ a → 0 ≤ b → 0 ≤ a / bdiv_nonneg ha: 0 ≤ aha hb: 0 < bhb.le: ∀ {α : Type ?u.63945} [inst : Preorder α] {a b : α}, a < b → a ≤ ble

private lemma div_ne_zero_of_pos_of_ne_zero: 0 < a → b ≠ 0 → a / b ≠ 0div_ne_zero_of_pos_of_ne_zero (ha: 0 < aha : 0: ?m.640510 < a: Ra) (hb: b ≠ 0hb : b: Rb ≠ 0: ?m.642080) : a: Ra / b: Rb ≠ 0: ?m.642790 :=
div_ne_zero: ∀ {G₀ : Type ?u.64286} [inst : GroupWithZero G₀] {a b : G₀}, a ≠ 0 → b ≠ 0 → a / b ≠ 0div_ne_zero ha: 0 < aha.ne': ∀ {α : Type ?u.64336} [inst : Preorder α] {x y : α}, x < y → y ≠ xne' hb: b ≠ 0hb

private lemma div_ne_zero_of_ne_zero_of_pos: a ≠ 0 → 0 < b → a / b ≠ 0div_ne_zero_of_ne_zero_of_pos (ha: a ≠ 0ha : a: Ra ≠ 0: ?m.644490) (hb: 0 < bhb : 0: ?m.645120 < b: Rb) : a: Ra / b: Rb ≠ 0: ?m.646760 :=
div_ne_zero: ∀ {G₀ : Type ?u.64683} [inst : GroupWithZero G₀] {a b : G₀}, a ≠ 0 → b ≠ 0 → a / b ≠ 0div_ne_zero ha: a ≠ 0ha hb: 0 < bhb.ne': ∀ {α : Type ?u.64734} [inst : Preorder α] {x y : α}, x < y → y ≠ xne'

end LinearOrderedSemifield

/-- The `positivity` extension which identifies expressions of the form `a / b`,
such that `positivity` successfully recognises both `a` and `b`. -/
@[positivity _: ?m.72696_ / _: ?m.72699_] def evalDiv: PositivityExtevalDiv : PositivityExt: TypePositivityExt where eval {u: ?m.64833u α: ?m.64836α} zα: ?m.64839zα pα: ?m.64842pα e: ?m.64845e := do
let .app: Expr → Expr → Expr.app (.app: Expr → Expr → Expr.app (f: Q(«\$α» → «\$α» → «\$α»)f : Q(\$α → \$α → \$α)) (a: Q(«\$α»)a : Q(\$α))) (b: Q(«\$α»)b : Q(\$α)) ← withReducible: {n : Type → Type ?u.64908} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithReducible (whnf: Expr → MetaM Exprwhnf e: ?m.64845e)
| throwError "not /": ?m.66751 ?m.66752throwErrorthrowError "not /": ?m.66751 ?m.66752 "not /"
let _e_eq: «\$e» =Q «\$f» «\$a» «\$b»_e_eq : \$e: «\$α»e =Q \$f: «\$α» → «\$α» → «\$α»f \$a: «\$α»a \$b: «\$α»b := ⟨⟩: «\$e» =Q «\$f» «\$a» «\$b»⟨⟩
let _a: ?m.65160_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(LinearOrderedSemifield: Type ?u.65146 → Type ?u.65146LinearOrderedSemifieldLinearOrderedSemifield \$α: ?m.64833 \$α: Type uα) : Q(Type u: Type (u+1)Type u))
assumeInstancesCommute
let ⟨_f_eq: «\$f» =Q HDiv.hDiv_f_eq⟩ ← withDefault: {n : Type → Type ?u.65340} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithDefault <| withNewMCtxDepth: {n : Type → Type ?u.65386} →
[inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → optParam Bool false → n αwithNewMCtxDepth <| assertDefEqQ: {u : Level} →
{α :
let u := u;
Q(Sort u)} →
(a b : Q(«\$α»)) → MetaM (PLift («\$a» =Q «\$b»))assertDefEqQ (u := u: ?m.64833u.succ: Level → Levelsucc) f: Q(«\$α» → «\$α» → «\$α»)f q(HDiv.hDiv: ?m.64833HDiv.hDiv)
let ra: ?m.65571ra ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.64839zα pα: ?m.64842pα a: Q(«\$α»)a; let rb: ?m.65623rb ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.64839zα pα: ?m.64842pα b: Q(«\$α»)b
match ra: ?m.65571ra, rb: ?m.65623rb with
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa, .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb => pure: {f : Type ?u.65659 → Type ?u.65658} → [self : Pure f] → {α : Type ?u.65659} → α → f αpure (.positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive q(div_pos: ∀ {α : Type ?u.65690} [inst : LinearOrderedSemifield α] {a b : α}, 0 < a → 0 < b → 0 < a / bdiv_posdiv_pos \$pa \$pb: ?m.64833 \$pa: 0 < «\$a»padiv_pos \$pa \$pb: ?m.64833 \$pb: 0 < «\$b»pb))
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa, .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pb: Q(0 ≤ «\$b»)pb => pure: {f : Type ?u.65795 → Type ?u.65794} → [self : Pure f] → {α : Type ?u.65795} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative q(div_nonneg_of_pos_of_nonneg: ∀ {R : Type ?u.65826} [inst : LinearOrderedSemifield R] {a b : R}, 0 < a → 0 ≤ b → 0 ≤ a / bdiv_nonneg_of_pos_of_nonnegdiv_nonneg_of_pos_of_nonneg \$pa \$pb: ?m.64833 \$pa: 0 < «\$a»padiv_nonneg_of_pos_of_nonneg \$pa \$pb: ?m.64833 \$pb: 0 ≤ «\$b»pb))
| .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pa: Q(0 ≤ «\$a»)pa, .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb => pure: {f : Type ?u.65884 → Type ?u.65883} → [self : Pure f] → {α : Type ?u.65884} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative q(div_nonneg_of_nonneg_of_pos: ∀ {R : Type ?u.65915} [inst : LinearOrderedSemifield R] {a b : R}, 0 ≤ a → 0 < b → 0 ≤ a / bdiv_nonneg_of_nonneg_of_posdiv_nonneg_of_nonneg_of_pos \$pa \$pb: ?m.64833 \$pa: 0 ≤ «\$a»padiv_nonneg_of_nonneg_of_pos \$pa \$pb: ?m.64833 \$pb: 0 < «\$b»pb))
| .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pa: Q(0 ≤ «\$a»)pa, .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pb: Q(0 ≤ «\$b»)pb => pure: {f : Type ?u.65965 → Type ?u.65964} → [self : Pure f] → {α : Type ?u.65965} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative q(div_nonneg: ∀ {α : Type ?u.65996} [inst : LinearOrderedSemifield α] {a b : α}, 0 ≤ a → 0 ≤ b → 0 ≤ a / bdiv_nonnegdiv_nonneg \$pa \$pb: ?m.64833 \$pa: 0 ≤ «\$a»padiv_nonneg \$pa \$pb: ?m.64833 \$pb: 0 ≤ «\$b»pb))
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa, .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pb: Q(«\$b» ≠ 0)pb => pure: {f : Type ?u.66046 → Type ?u.66045} → [self : Pure f] → {α : Type ?u.66046} → α → f αpure (.nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero q(div_ne_zero_of_pos_of_ne_zero: ∀ {R : Type ?u.66077} [inst : LinearOrderedSemifield R] {a b : R}, 0 < a → b ≠ 0 → a / b ≠ 0div_ne_zero_of_pos_of_ne_zerodiv_ne_zero_of_pos_of_ne_zero \$pa \$pb: ?m.64833 \$pa: 0 < «\$a»padiv_ne_zero_of_pos_of_ne_zero \$pa \$pb: ?m.64833 \$pb: «\$b» ≠ 0pb))
| .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pa: Q(«\$a» ≠ 0)pa, .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pb: Q(0 < «\$b»)pb => pure: {f : Type ?u.66127 → Type ?u.66126} → [self : Pure f] → {α : Type ?u.66127} → α → f αpure (.nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero q(div_ne_zero_of_ne_zero_of_pos: ∀ {R : Type ?u.66158} [inst : LinearOrderedSemifield R] {a b : R}, a ≠ 0 → 0 < b → a / b ≠ 0div_ne_zero_of_ne_zero_of_posdiv_ne_zero_of_ne_zero_of_pos \$pa \$pb: ?m.64833 \$pa: «\$a» ≠ 0padiv_ne_zero_of_ne_zero_of_pos \$pa \$pb: ?m.64833 \$pb: 0 < «\$b»pb))
| .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pa: Q(«\$a» ≠ 0)pa, .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pb: Q(«\$b» ≠ 0)pb => pure: {f : Type ?u.66203 → Type ?u.66202} → [self : Pure f] → {α : Type ?u.66203} → α → f αpure (.nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero q(div_ne_zero: ∀ {G₀ : Type ?u.66234} [inst : GroupWithZero G₀] {a b : G₀}, a ≠ 0 → b ≠ 0 → a / b ≠ 0div_ne_zerodiv_ne_zero \$pa \$pb: ?m.64833 \$pa: «\$a» ≠ 0padiv_ne_zero \$pa \$pb: ?m.64833 \$pb: «\$b» ≠ 0pb))
| _, _ => pure: {f : Type ?u.66295 → Type ?u.66294} → [self : Pure f] → {α : Type ?u.66295} → α → f αpure .none: {u : Level} → {α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Strictness zα pα e.none

/-- The `positivity` extension which identifies expressions of the form `a⁻¹`,
such that `positivity` successfully recognises `a`. -/
@[positivity (_: α_ : α: ?m.77498α)⁻¹]
def evalInv: PositivityExtevalInv : PositivityExt: TypePositivityExt where eval {u: ?m.72720u α: ?m.72723α} zα: ?m.72726zα pα: ?m.72729pα e: ?m.72732e := do
let .app: Expr → Expr → Expr.app (f: Q(«\$α» → «\$α»)f : Q(\$α → \$α)) (a: Q(«\$α»)a : Q(\$α)) ← withReducible: {n : Type → Type ?u.72795} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithReducible (whnf: Expr → MetaM Exprwhnf e: ?m.72732e) | throwError "not ⁻¹": ?m.74031 ?m.74032throwErrorthrowError "not ⁻¹": ?m.74031 ?m.74032 "not ⁻¹"
let _e_eq: «\$e» =Q «\$f» «\$a»_e_eq : \$e: «\$α»e =Q \$f: «\$α» → «\$α»f \$a: «\$α»a := ⟨⟩: «\$e» =Q «\$f» «\$a»⟨⟩
let _a: ?m.73035_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(LinearOrderedSemifield: Type ?u.73021 → Type ?u.73021LinearOrderedSemifieldLinearOrderedSemifield \$α: ?m.72720 \$α: Type uα) : Q(Type u: ?m.72720Type u))
assumeInstancesCommute
let ⟨_f_eq: «\$f» =Q Inv.inv_f_eq⟩ ← withDefault: {n : Type → Type ?u.73215} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithDefault <| withNewMCtxDepth: {n : Type → Type ?u.73261} →
[inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → optParam Bool false → n αwithNewMCtxDepth <| assertDefEqQ: {u : Level} →
{α :
let u := u;
Q(Sort u)} →
(a b : Q(«\$α»)) → MetaM (PLift («\$a» =Q «\$b»))assertDefEqQ (u := u: ?m.72720u.succ: Level → Levelsucc) f: Q(«\$α» → «\$α»)f q(Inv.inv: ?m.72720Inv.inv)
let ra: ?m.73454ra ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.72726zα pα: ?m.72729pα a: Q(«\$α»)a
match ra: ?m.73454ra with
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa => pure: {f : Type ?u.73476 → Type ?u.73475} → [self : Pure f] → {α : Type ?u.73476} → α → f αpure (.positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive q(inv_pos_of_pos: ∀ {α : Type ?u.73507} [inst : LinearOrderedSemifield α] {a : α}, 0 < a → 0 < a⁻¹inv_pos_of_posinv_pos_of_pos \$pa: ?m.72720 \$pa: 0 < «\$a»pa))
| .nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative pa: Q(0 ≤ «\$a»)pa => pure: {f : Type ?u.73594 → Type ?u.73593} → [self : Pure f] → {α : Type ?u.73594} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative q(inv_nonneg_of_nonneg: ∀ {α : Type ?u.73625} [inst : LinearOrderedSemifield α] {a : α}, 0 ≤ a → 0 ≤ a⁻¹inv_nonneg_of_nonneginv_nonneg_of_nonneg \$pa: ?m.72720 \$pa: 0 ≤ «\$a»pa))
| .nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero pa: Q(«\$a» ≠ 0)pa => pure: {f : Type ?u.73668 → Type ?u.73667} → [self : Pure f] → {α : Type ?u.73668} → α → f αpure (.nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero q(inv_ne_zero: ∀ {G₀ : Type ?u.73699} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a⁻¹ ≠ 0inv_ne_zeroinv_ne_zero \$pa: ?m.72720 \$pa: «\$a» ≠ 0pa))
| .none: Strictness zα pα a.none => pure: {f : Type ?u.73754 → Type ?u.73753} → [self : Pure f] → {α : Type ?u.73754} → α → f αpure .none: {u : Level} → {α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Strictness zα pα e.none

private theorem pow_zero_pos: ∀ {α : Type u_1} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] (a : α), 0 < a ^ 0pow_zero_pos [OrderedSemiring: Type ?u.77668 → Type ?u.77668OrderedSemiring α: ?m.77665α] [Nontrivial: Type ?u.77671 → PropNontrivial α: ?m.77665α] (a: αa : α: ?m.77665α) : 0: ?m.776780 < a: αa ^ 0: ?m.776970 :=
zero_lt_one: ∀ {α : Type ?u.78303} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
[inst_4 : NeZero 1], 0 < 1zero_lt_one.trans_le: ∀ {α : Type ?u.78590} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < ctrans_le (pow_zero: ∀ {M : Type ?u.78794} [inst : Monoid M] (a : M), a ^ 0 = 1pow_zero a: αa).ge: ∀ {α : Type ?u.78903} [inst : Preorder α] {x y : α}, x = y → y ≤ xge

private lemma zpow_zero_pos: ∀ {R : Type u_1} [inst : LinearOrderedSemifield R] (a : R), 0 < a ^ 0zpow_zero_pos [LinearOrderedSemifield: Type ?u.79471 → Type ?u.79471LinearOrderedSemifield R: ?m.79468R] (a: Ra : R: ?m.79468R) : 0: ?m.794780 < a: Ra ^ (0: ?m.794980 : ℤ: Typeℤ) :=
zero_lt_one: ∀ {α : Type ?u.82408} [inst : Zero α] [inst_1 : One α] [inst_2 : PartialOrder α] [inst_3 : ZeroLEOneClass α]
[inst_4 : NeZero 1], 0 < 1zero_lt_one.trans_le: ∀ {α : Type ?u.82695} [inst : Preorder α] {a b c : α}, a < b → b ≤ c → a < ctrans_le (zpow_zero: ∀ {G : Type ?u.82859} [inst : DivInvMonoid G] (a : G), a ^ 0 = 1zpow_zero a: Ra).ge: ∀ {α : Type ?u.82903} [inst : Preorder α] {x y : α}, x = y → y ≤ xge

/-- The `positivity` extension which identifies expressions of the form `a ^ (0:ℕ)`.
This extension is run in addition to the general `a ^ b` extension (they are overlapping). -/
@[positivity (_: α_ : α: ?m.86414α) ^ (0: ?m.864230:ℕ), Pow.pow: {α : Type ?u.89497} → {β : Type ?u.89496} → [self : Pow α β] → α → β → αPow.pow _: ?m.89498_ (0: ?m.895040:ℕ)]
def evalPowZeroNat: PositivityExtevalPowZeroNat : PositivityExt: TypePositivityExt where eval {u: ?m.83360u α: ?m.83363α} _zα: ?m.83366_zα _pα: ?m.83369_pα e: ?m.83372e := do
let .app: Expr → Expr → Expr.app (.app: Expr → Expr → Expr.app _ (a: Q(«\$α»)a : Q(\$α))) _ ← withReducible: {n : Type → Type ?u.83435} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithReducible (whnf: Expr → MetaM Exprwhnf e: ?m.83372e) | throwError "not ^": ?m.83834 ?m.83835throwErrorthrowError "not ^": ?m.83834 ?m.83835 "not ^"
_: ?m.83646_ ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(OrderedSemiring: Type ?u.83632 → Type ?u.83632OrderedSemiringOrderedSemiring \$α: ?m.83360 \$α: Type uα) : Q(Type u: Type (u+1)Type u))
_: ?m.83710_ ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(Nontrivial: Type ?u.83698 → PropNontrivialNontrivial \$α: ?m.83360 \$α: Type uα) : Q(Prop: TypeProp))
pure: {f : Type ?u.83714 → Type ?u.83713} → [self : Pure f] → {α : Type ?u.83714} → α → f αpure (.positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive (q(pow_zero_pos: ∀ {α : Type ?u.83755} [inst : OrderedSemiring α] [inst_1 : Nontrivial α] (a : α), 0 < a ^ 0pow_zero_pospow_zero_pos \$a: ?m.83360 \$a: «\$α»a) : Expr: TypeExpr))

/-- The `positivity` extension which identifies expressions of the form `a ^ (0:ℤ)`. -/
@[positivity (_: α_ : α: ?m.92419α) ^ (0: ?m.924280:ℤ), Pow.pow: {α : Type ?u.95222} → {β : Type ?u.95221} → [self : Pow α β] → α → β → αPow.pow _: ?m.95223_ (0: ?m.952290:ℤ)]
def evalPowZeroInt: PositivityExtevalPowZeroInt : PositivityExt: TypePositivityExt where eval {u: ?m.89531u α: ?m.89534α} _zα: ?m.89537_zα _pα: ?m.89540_pα e: ?m.89543e := do
let .app: Expr → Expr → Expr.app (.app: Expr → Expr → Expr.app _ (a: Q(«\$α»)a : Q(\$α))) _ ← withReducible: {n : Type → Type ?u.89606} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithReducible (whnf: Expr → MetaM Exprwhnf e: ?m.89543e) | throwError "not ^": ?m.89915 ?m.89916throwErrorthrowError "not ^": ?m.89915 ?m.89916 "not ^"
_: ?m.89817_ ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(LinearOrderedSemifield: Type ?u.89803 → Type ?u.89803LinearOrderedSemifieldLinearOrderedSemifield \$α: ?m.89531 \$α: Type uα) : Q(Type u: Type (u+1)Type u))
pure: {f : Type ?u.89821 → Type ?u.89820} → [self : Pure f] → {α : Type ?u.89821} → α → f αpure (.positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive (q(zpow_zero_pos: ∀ {R : Type ?u.89862} [inst : LinearOrderedSemifield R] (a : R), 0 < a ^ 0zpow_zero_poszpow_zero_pos \$a: ?m.89531 \$a: «\$α»a) : Expr: TypeExpr))

/-- The `positivity` extension which identifies expressions of the form `a ^ (b : ℕ)`,
such that `positivity` successfully recognises both `a` and `b`. -/
@[positivity (_: α_ : α: ?m.107867α) ^ (_: ℕ_ : ℕ), Pow.pow: {α : Type ?u.110938} → {β : Type ?u.110937} → [self : Pow α β] → α → β → αPow.pow _: ?m.110939_ (_: ℕ_ : ℕ)]
def evalPow: PositivityExtevalPow : PositivityExt: TypePositivityExt where eval {u: ?m.95256u α: ?m.95259α} zα: ?m.95262zα pα: ?m.95265pα e: ?m.95268e := do
let .app: Expr → Expr → Expr.app (.app: Expr → Expr → Expr.app _ (a: Q(«\$α»)a : Q(\$α))) (b: Q(ℕ)b : Q(ℕ)) ← withReducible: {n : Type → Type ?u.95331} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n αwithReducible (whnf: Expr → MetaM Exprwhnf e: ?m.95268e) | throwError "not ^": ?m.100035 ?m.100036throwErrorthrowError "not ^": ?m.100035 ?m.100036 "not ^"
let result: ?m.96605result ← catchNone: {u : Level} →
{α : Q(Type u)} →
{zα : Q(Zero «\$α»)} →
{pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → MetaM (Strictness zα pα e) → MetaM (Strictness zα pα e)catchNone do
let .true: Bool.true := b: Q(ℕ)b.isAppOfArity: Expr → Name → ℕ → BoolisAppOfArity ``OfNat.ofNat: {α : Type u} → (x : ℕ) → [self : OfNat α x] → αOfNat.ofNat 3: ?m.955483 | throwError "not a ^ n where n is a literal": ?m.96299 ?m.96300throwErrorthrowError "not a ^ n where n is a literal": ?m.96299 ?m.96300 "not a ^ n where n is a literal"
let some: {α : Type ?u.95575} → α → Option αsome n: ℕn := (b: Q(ℕ)b.getRevArg!: Expr → ℕ → ExprgetRevArg! 1: ?m.955671).natLit?: Expr → Option ℕnatLit? | throwError "not a ^ n where n is a literal": ?m.95999 ?m.96000throwErrorthrowError "not a ^ n where n is a literal": ?m.95999 ?m.96000 "not a ^ n where n is a literal"
guard: {f : Type → Type ?u.95632} → [inst : Alternative f] → (p : Prop) → [inst : Decidable p] → f Unitguard (n: ℕn % 2: ?m.956522 = 0: ?m.956660)
let m: Q(ℕ)m : Q(ℕ: Typeℕ) := mkRawNatLit: ℕ → ExprmkRawNatLit (n: ℕn / 2: ?m.957622)
let _a: ?m.95885_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(LinearOrderedRing: Type ?u.95876 → Type ?u.95876LinearOrderedRingLinearOrderedRing \$α: ?m.95256 \$α: Type uα) : Q(Type u: Type (u+1)Type u))
pure: {f : Type ?u.95888 → Type ?u.95887} → [self : Pure f] → {α : Type ?u.95888} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative (q(pow_bit0_nonneg: ∀ {R : Type ?u.95934} [inst : LinearOrderedRing R] (a : R) (n : ℕ), 0 ≤ a ^ bit0 npow_bit0_nonnegpow_bit0_nonneg \$a \$m: ?m.95256 \$a: «\$α»apow_bit0_nonneg \$a \$m: ?m.95256 \$m: ℕm) : Expr: TypeExpr))
orElse: {u : Level} →
{α : Q(Type u)} →
{zα : Q(Zero «\$α»)} →
{pα : Q(PartialOrder «\$α»)} →
{e : Q(«\$α»)} → Strictness zα pα e → MetaM (Strictness zα pα e) → MetaM (Strictness zα pα e)orElse result: ?m.96605result do
let ra: ?m.96699ra ← core: {u : Level} →
{α : Q(Type u)} → (zα : Q(Zero «\$α»)) → (pα : Q(PartialOrder «\$α»)) → (e : Q(«\$α»)) → MetaM (Strictness zα pα e)core zα: ?m.95262zα pα: ?m.95265pα a: Q(«\$α»)a
let ofNonneg: Expr → Q(OrderedSemiring «\$α») → MetaM (Strictness zα pα e)ofNonneg pa: ?m.96702pa (oα: Q(OrderedSemiring «\$α»)oα : Q(OrderedSemiring: Type ?u.96710 → Type ?u.96710OrderedSemiringOrderedSemiring \$α: ?m.95256 \$α: Type uα)) : MetaM: Type → TypeMetaM (Strictness: {u : Level} → {α : Q(Type u)} → Q(Zero «\$α») → Q(PartialOrder «\$α») → Q(«\$α») → TypeStrictness zα: ?m.95262zα pα: ?m.95265pα e: ?m.95268e) := do
have pa': Q(0 ≤ «\$a»)pa' : Q(byGoals accomplished! 🐙 «\$α»: Type u«\$zα»: Zero «\$α»«\$pα»: PartialOrder «\$α»«\$e»: «\$α»\$fn✝: Expr«\$a»: «\$α»«\$b»: ℕ«\$oα»: OrderedSemiring «\$α»Sort ?u.96722clear! «\$zα»: Zero «\$α»«\$zα» «\$pα»: PartialOrder «\$α»«\$pα»«\$α»: Type u«\$e»: «\$α»\$fn✝: Expr«\$a»: «\$α»«\$b»: ℕ«\$oα»: OrderedSemiring «\$α»Sort ?u.96722;«\$α»: Type u«\$e»: «\$α»\$fn✝: Expr«\$a»: «\$α»«\$b»: ℕ«\$oα»: OrderedSemiring «\$α»Sort ?u.96722 «\$α»: Type u«\$zα»: Zero «\$α»«\$pα»: PartialOrder «\$α»«\$e»: «\$α»\$fn✝: Expr«\$a»: «\$α»«\$b»: ℕ«\$oα»: OrderedSemiring «\$α»Sort ?u.96722exact 0: ?m.967290 ≤ \$a: «\$α»aGoals accomplished! 🐙) := pa: ?m.96702pa
pure: {f : Type ?u.97071 → Type ?u.97070} → [self : Pure f] → {α : Type ?u.97071} → α → f αpure (.nonnegative: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 ≤ «\$e») → Strictness zα pα e.nonnegative (q(pow_nonneg: ∀ {α : Type ?u.97107} [inst : OrderedSemiring α] {a : α}, 0 ≤ a → ∀ (n : ℕ), 0 ≤ a ^ npow_nonnegpow_nonneg \$pa' \$b: ?m.95256 \$pa': 0 ≤ «\$a»pa'pow_nonneg \$pa' \$b: ?m.95256 \$b: ℕb) : Expr: TypeExpr))
let ofNonzero: Expr → Q(OrderedSemiring «\$α») → MetaM (Strictness zα pα e)ofNonzero pa: ?m.97185pa (oα: Q(OrderedSemiring «\$α»)oα : Q(OrderedSemiring: Type ?u.97194 → Type ?u.97194OrderedSemiringOrderedSemiring \$α: ?m.95256 \$α: Type uα)) : MetaM: Type → TypeMetaM (Strictness: {u : Level} → {α : Q(Type u)} → Q(Zero «\$α») → Q(PartialOrder «\$α») → Q(«\$α») → TypeStrictness zα: ?m.95262zα pα: ?m.95265pα e: ?m.95268e) := do
have pa': Q(«\$a» ≠ 0)pa' : Q(byGoals accomplished! 🐙 «\$α»: Type u«\$zα»: Zero «\$α»«\$pα»: PartialOrder «\$α»«\$e»: «\$α»\$fn✝: Expr«\$a»: «\$α»«\$b»: ℕ«\$oα»: OrderedSemiring «\$α»Sort ?u.97206clear! «\$zα»: Zero «\$α»«\$zα» «\$pα»: PartialOrder «\$α»«\$pα»«\$α»: Type u«\$e»: «\$α»\$fn✝: Expr«\$a»: «\$α»«\$b»: ℕ«\$oα»: OrderedSemiring «\$α»Sort ?u.97206;«\$α»: Type u«\$e»: «\$α»\$fn✝: Expr«\$a»: «\$α»«\$b»: ℕ«\$oα»: OrderedSemiring «\$α»Sort ?u.97206 «\$α»: Type u«\$zα»: Zero «\$α»«\$pα»: PartialOrder «\$α»«\$e»: «\$α»\$fn✝: Expr«\$a»: «\$α»«\$b»: ℕ«\$oα»: OrderedSemiring «\$α»Sort ?u.97206exact \$a: «\$α»a ≠ 0: ?m.972140Goals accomplished! 🐙) := pa: ?m.97185pa
let _a: ?m.97784_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(by: ?m.95256byGoals accomplished! 🐙 : ?m.95256 «\$α»: Type u«\$zα»: Zero «\$α»«\$pα»: PartialOrder «\$α»«\$e»: «\$α»\$fn✝: Expr«\$a»: «\$α»«\$b»: ℕ«\$oα»: OrderedSemiring «\$α»«\$pa'»: «\$a» ≠ 0Propclear! «\$zα»: Zero «\$α»«\$zα» «\$pα»: PartialOrder «\$α»«\$pα»«\$α»: Type u«\$e»: «\$α»\$fn✝: Expr«\$a»: «\$α»«\$b»: ℕ«\$oα»: OrderedSemiring «\$α»«\$pa'»: «\$a» ≠ 0Prop;: ?m.95256;«\$α»: Type u«\$e»: «\$α»\$fn✝: Expr«\$a»: «\$α»«\$b»: ℕ«\$oα»: OrderedSemiring «\$α»«\$pa'»: «\$a» ≠ 0Prop : ?m.95256 «\$α»: Type u«\$zα»: Zero «\$α»«\$pα»: PartialOrder «\$α»«\$e»: «\$α»\$fn✝: Expr«\$a»: «\$α»«\$b»: ℕ«\$oα»: OrderedSemiring «\$α»«\$pa'»: «\$a» ≠ 0Propexact NoZeroDivisors: (M₀ : Type ?u.97440) → [inst : Mul M₀] → [inst : Zero M₀] → PropNoZeroDivisors \$α: Type uαGoals accomplished! 🐙) : Q(Prop: TypeProp))
pure: {f : Type ?u.97787 → Type ?u.97786} → [self : Pure f] → {α : Type ?u.97787} → α → f αpure (.nonzero: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(«\$e» ≠ 0) → Strictness zα pα e.nonzero (q(pow_ne_zero: ∀ {M : Type ?u.97823} [inst : MonoidWithZero M] [inst_1 : NoZeroDivisors M] {a : M} (n : ℕ), a ≠ 0 → a ^ n ≠ 0pow_ne_zeropow_ne_zero \$b \$pa': ?m.95256 \$b: ℕbpow_ne_zero \$b \$pa': ?m.95256 \$pa': «\$a» ≠ 0pa') : Expr: TypeExpr))
match ra: ?m.96699ra with
| .positive: {u : Level} →
{α : Q(Type u)} → {zα : Q(Zero «\$α»)} → {pα : Q(PartialOrder «\$α»)} → {e : Q(«\$α»)} → Q(0 < «\$e») → Strictness zα pα e.positive pa: Q(0 < «\$a»)pa =>
try
let _a: ?m.98123_a ← synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)synthInstanceQ (q(StrictOrderedSemiring: Type ?u.98116 → Type ?u.98116StrictOrderedSemiringStrictOrderedSemiring \$α: ?m.95256 \$α: Type uα) : Q(Type u: ?m.95256Type u))
have pa': Q(0 < «\$a»)pa' : Q(by: ?m.95256byGoals accomplished! 🐙```