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, Aurélien Saue, Tim Baanen
-/
import Lean.Elab.Tactic.Basic
import Mathlib.Algebra.GroupPower.Basic
import Mathlib.Algebra.Ring.Basic
import Mathlib.Tactic.NormNum
import Mathlib.Tactic.Clear!
import Mathlib.Util.AtomM

/-!
# `ring` tactic

A tactic for solving equations in commutative (semi)rings,
where the exponents can also contain variables.
Based on  .

More precisely, expressions of the following form are supported:
- constants (non-negative integers)
- variables
- coefficients (any rational number, embedded into the (semi)ring)
- multiplication of expressions (`a * b`)
- scalar multiplication of expressions (`n • a`; the multiplier must have type `ℕ`)
- exponentiation of expressions (the exponent must have type `ℕ`)
- subtraction and negation of expressions (if the base is a full ring)

The extension to exponents means that something like `2 * 2^n * b = b * 2^(n+1)` can be proved,
even though it is not strictly speaking an equation in the language of commutative rings.

## Implementation notes

The basic approach to prove equalities is to normalise both sides and check for equality.
The normalisation is guided by building a value in the type `ExSum` at the meta level,
together with a proof (at the base level) that the original value is equal to
the normalised version.

The outline of the file:
- Define a mutual inductive family of types `ExSum`, `ExProd`, `ExBase`,
which can represent expressions with `+`, `*`, `^` and rational numerals.
The mutual induction ensures that associativity and distributivity are applied,
by restricting which kinds of subexpressions appear as arguments to the various operators.
- Represent addition, multiplication and exponentiation in the `ExSum` type,
thus allowing us to map expressions to `ExSum` (the `eval` function drives this).
We apply associativity and distributivity of the operators here (helped by `Ex*` types)
and commutativity as well (by sorting the subterms; unfortunately not helped by anything).
Any expression not of the above formats is treated as an atom (the same as a variable).

There are some details we glossed over which make the plan more complicated:
- The order on atoms is not initially obvious.
We construct a list containing them in order of initial appearance in the expression,
then use the index into the list as a key to order on.
- For `pow`, the exponent must be a natural number, while the base can be any semiring `α`.
We swap out operations for the base ring `α` with those for the exponent ring `ℕ`
as soon as we deal with exponents.

## Caveats and future work

The normalized form of an expression is the one that is useful for the tactic,
but not as nice to read. To remedy this, the user-facing normalization calls `ringNFCore`.

Subtraction cancels out identical terms, but division does not.
That is: `a - a = 0 := by ring` solves the goal,
but `a / a := 1 by ring` doesn't.
Note that `0 / 0` is generally defined to be `0`,
so division cancelling out is not true in general.

Multiplication of powers can be simplified a little bit further:
`2 ^ n * 2 ^ n = 4 ^ n := by ring` could be implemented
in a similar way that `2 * a + 2 * a = 4 * a := by ring` already works.
This feature wasn't needed yet, so it's not implemented yet.

## Tags

ring, semiring, exponent, power
-/

namespace Mathlib.Tactic
namespace Ring
open Mathlib.Meta Qq NormNum Lean.Meta AtomM
open Lean (MetaM Expr mkRawNatLit)

/-- A shortcut instance for `CommSemiring ℕ` used by ring. -/
def instCommSemiringNat: CommSemiring ℕinstCommSemiringNat : CommSemiring: Type ?u.2 → Type ?u.2CommSemiring ℕ: Typeℕ := inferInstance: {α : Sort ?u.4} → [i : α] → αinferInstance

/--
A typed expression of type `CommSemiring ℕ` used when we are working on
ring subexpressions of type `ℕ`.
-/
def sℕ: Q(CommSemiring ℕ)sℕ : Q(CommSemiring: Type ?u.63 → Type ?u.63CommSemiring ℕ: Typeℕ) := q(instCommSemiringNat: CommSemiring ℕinstCommSemiringNat)

mutual

/-- The base `e` of a normalized exponent expression. -/
inductive ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExBase : ∀ {α: Q(Type u)α : Q(Type u: Type (u+1)Type u)}, Q(CommSemiring: Type ?u.112 → Type ?u.112CommSemiringCommSemiring \$α: ?m.99 \$α: Type uα) → (e: Q(«\$α»)e : Q(\$α: Type uα)) → Type: Type 1Type
/--
An atomic expression `e` with id `id`.

Atomic expressions are those which `ring` cannot parse any further.
For instance, `a + (a % b)` has `a` and `(a % b)` as atoms.
The `ring1` tactic does not normalize the subexpressions in atoms, but `ring_nf` does.

Atoms in fact represent equivalence classes of expressions, modulo definitional equality.
The field `index : ℕ` should be a unique number for each class,
while `value : expr` contains a representative of this class.
The function `resolve_atom` determines the appropriate atom for a given expression.
-/
| atom: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℕ → ExBase sα eatom (id: ℕid : ℕ: Typeℕ) : ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExBase sα: ?m.203sα e: ?m.214e
/-- A sum of monomials.  -/
| sum: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ExSum sα e → ExBase sα esum (_: ExSum sα e_ : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: ?m.232sα e: ?m.240e) : ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExBase sα: ?m.232sα e: ?m.240e

/--
A monomial, which is a product of powers of `ExBase` expressions,
terminated by a (nonzero) constant coefficient.
-/
inductive ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd : ∀ {α: Q(Type u)α : Q(Type u: ?m.126Type u)}, Q(CommSemiring: Type ?u.139 → Type ?u.139CommSemiringCommSemiring \$α: ?m.126 \$α: Type uα) → (e: Q(«\$α»)e : Q(\$α: Type uα)) → Type: Type 1Type
/-- A coefficient `value`, which must not be `0`. `e` is a raw rat cast.
If `value` is not an integer, then `hyp` should be a proof of `(value.den : α) ≠ 0`. -/
| const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα econst (value: ℚvalue : ℚ: Typeℚ) (hyp: optParam (Option Expr) nonehyp : Option: Type ?u.286 → Type ?u.286Option Expr: TypeExpr := none: {α : Type ?u.303} → Option αnone) : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: ?m.280sα e: ?m.296e
/-- A product `x ^ e * b` is a monomial if `b` is a monomial. Here `x` is a `ExBase`
and `e` is a `ExProd` representing a monomial expression in `ℕ` (it is a monomial instead of
a polynomial because we eagerly normalize `x ^ (a + b) = x ^ a * x ^ b`.) -/
| mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»)mul {α: Q(Type u)α : Q(Type u: ?m.335Type u)} {sα: Q(CommSemiring «\$α»)sα : Q(CommSemiring: Type ?u.346 → Type ?u.346CommSemiringCommSemiring \$α: ?m.335 \$α: Type uα)} {x: Q(«\$α»)x : Q(\$α: Type uα)} {e: Q(ℕ)e : Q(ℕ: Typeℕ)} {b: Q(«\$α»)b : Q(\$α: Type uα)} :
ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExBase sα: Q(CommSemiring «\$α»)sα x: Q(«\$α»)x → ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sℕ: Q(CommSemiring ℕ)sℕ e: Q(ℕ)e → ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα b: Q(«\$α»)b → ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα q(\$x: «\$α»xx ^ \$e * \$b: ?m.335 ^ \$e: ℕex ^ \$e * \$b: ?m.335 * \$b: «\$α»b)

/-- A polynomial expression, which is a sum of monomials. -/
inductive ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum : ∀ {α: Q(Type u)α : Q(Type u: ?m.153Type u)}, Q(CommSemiring: Type ?u.166 → Type ?u.166CommSemiringCommSemiring \$α: ?m.153 \$α: Type uα) → (e: Q(«\$α»)e : Q(\$α: Type uα)) → Type: Type 1Type
/-- Zero is a polynomial. `e` is the expression `0`. -/
| zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → ExSum sα q(0)zero {α: Q(Type u)α : Q(Type u: ?m.1162Type u)} {sα: Q(CommSemiring «\$α»)sα : Q(CommSemiring: Type ?u.1173 → Type ?u.1173CommSemiringCommSemiring \$α: ?m.1162 \$α: Type uα)} : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: Q(CommSemiring «\$α»)sα q(0: ?m.11820 : \$α: Type uα)
/-- A sum `a + b` is a polynomial if `a` is a monomial and `b` is another polynomial. -/
| add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»)add {α: Q(Type u)α : Q(Type u: Type (u+1)Type u)} {sα: Q(CommSemiring «\$α»)sα : Q(CommSemiring: Type ?u.1373 → Type ?u.1373CommSemiringCommSemiring \$α: ?m.1362 \$α: Type uα)} {a: Q(«\$α»)a b: Q(«\$α»)b : Q(\$α: Type uα)} :
ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα a: Q(«\$α»)a → ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: Q(CommSemiring «\$α»)sα b: Q(«\$α»)b → ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: Q(CommSemiring «\$α»)sα q(\$a: «\$α»aa + \$b: ?m.1362 + \$b: «\$α»b)
end

mutual -- partial only to speed up compilation

/-- Equality test for expressions. This is not a `BEq` instance because it is heterogeneous. -/
partial def ExBase.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExBase sα a_1 → ExBase sα b → BoolExBase.eq : ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExBase sα: ?m.4842sα a: ?m.4852a → ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExBase sα: ?m.4842sα b: ?m.4872b → Bool: TypeBool
| .atom: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℕ → ExBase sα e.atom i: ℕi, .atom: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℕ → ExBase sα e.atom j: ℕj => i: ℕi == j: ℕj
| .sum: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ExSum sα e → ExBase sα e.sum a: ExSum sα a✝a, .sum: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ExSum sα e → ExBase sα e.sum b: ExSum sα b✝b => a: ExSum sα a✝a.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExSum sα a_1 → ExSum sα b → Booleq b: ExSum sα b✝b
| _, _ => false: Boolfalse

@[inherit_doc ExBase.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExBase sα a_1 → ExBase sα b → BoolExBase.eq]
partial def ExProd.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExProd sα a_1 → ExProd sα b → BoolExProd.eq : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: ?m.4895sα a: ?m.4905a → ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: ?m.4895sα b: ?m.4925b → Bool: TypeBool
| .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const i: ℚi _, .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const j: ℚj _ => i: ℚi == j: ℚj
| .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul a₁: ExBase sα x✝¹a₁ a₂: ExProd sℕ e✝¹a₂ a₃: ExProd sα b✝¹a₃, .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul b₁: ExBase sα x✝b₁ b₂: ExProd sℕ e✝b₂ b₃: ExProd sα b✝b₃ => a₁: ExBase sα x✝¹a₁.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExBase sα a_1 → ExBase sα b → Booleq b₁: ExBase sα x✝b₁ && a₂: ExProd sℕ e✝¹a₂.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExProd sα a_1 → ExProd sα b → Booleq b₂: ExProd sℕ e✝b₂ && a₃: ExProd sα b✝¹a₃.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExProd sα a_1 → ExProd sα b → Booleq b₃: ExProd sα b✝b₃
| _, _ => false: Boolfalse

@[inherit_doc ExBase.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExBase sα a_1 → ExBase sα b → BoolExBase.eq]
partial def ExSum.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExSum sα a_1 → ExSum sα b → BoolExSum.eq : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: ?m.4948sα a: ?m.4958a → ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: ?m.4948sα b: ?m.4978b → Bool: TypeBool
| .zero: ExSum sα q(0).zero, .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → ExSum sα q(0).zero => true: Booltrue
| .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add a₁: ExProd sα a✝¹a₁ a₂: ExSum sα b✝¹a₂, .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add b₁: ExProd sα a✝b₁ b₂: ExSum sα b✝b₂ => a₁: ExProd sα a✝¹a₁.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExProd sα a_1 → ExProd sα b → Booleq b₁: ExProd sα a✝b₁ && a₂: ExSum sα b✝¹a₂.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExSum sα a_1 → ExSum sα b → Booleq b₂: ExSum sα b✝b₂
| _, _ => false: Boolfalse
end

mutual -- partial only to speed up compilation
/--
A total order on normalized expressions.
This is not an `Ord` instance because it is heterogeneous.
-/
partial def ExBase.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExBase sα a_1 → ExBase sα b → OrderingExBase.cmp : ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExBase sα: ?m.30955sα a: ?m.30965a → ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExBase sα: ?m.30955sα b: ?m.30985b → Ordering: TypeOrdering
| .atom: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℕ → ExBase sα e.atom i: ℕi, .atom: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℕ → ExBase sα e.atom j: ℕj => compare: {α : Type ?u.31163} → [self : Ord α] → α → α → Orderingcompare i: ℕi j: ℕj
| .sum: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ExSum sα e → ExBase sα e.sum a: ExSum sα a✝a, .sum: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ExSum sα e → ExBase sα e.sum b: ExSum sα b✝b => a: ExSum sα a✝a.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExSum sα a_1 → ExSum sα b → Orderingcmp b: ExSum sα b✝b
| .atom: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℕ → ExBase sα e.atom .., .sum: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ExSum sα e → ExBase sα e.sum .. => .lt: Ordering.lt
| .sum: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ExSum sα e → ExBase sα e.sum .., .atom: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℕ → ExBase sα e.atom .. => .gt: Ordering.gt

@[inherit_doc ExBase.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExBase sα a_1 → ExBase sα b → OrderingExBase.cmp]
partial def ExProd.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExProd sα a_1 → ExProd sα b → OrderingExProd.cmp : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: ?m.31008sα a: ?m.31018a → ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: ?m.31008sα b: ?m.31038b → Ordering: TypeOrdering
| .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const i: ℚi _, .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const j: ℚj _ => compare: {α : Type ?u.35624} → [self : Ord α] → α → α → Orderingcompare i: ℚi j: ℚj
| .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul a₁: ExBase sα x✝¹a₁ a₂: ExProd sℕ e✝¹a₂ a₃: ExProd sα b✝¹a₃, .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul b₁: ExBase sα x✝b₁ b₂: ExProd sℕ e✝b₂ b₃: ExProd sα b✝b₃ => (a₁: ExBase sα x✝¹a₁.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExBase sα a_1 → ExBase sα b → Orderingcmp b₁: ExBase sα x✝b₁).then: Ordering → Ordering → Orderingthen (a₂: ExProd sℕ e✝¹a₂.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExProd sα a_1 → ExProd sα b → Orderingcmp b₂: ExProd sℕ e✝b₂) |>.then: Ordering → Ordering → Orderingthen (a₃: ExProd sα b✝¹a₃.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExProd sα a_1 → ExProd sα b → Orderingcmp b₃: ExProd sα b✝b₃)
| .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const _ _, .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul .. => .lt: Ordering.lt
| .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul .., .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const _ _ => .gt: Ordering.gt

@[inherit_doc ExBase.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExBase sα a_1 → ExBase sα b → OrderingExBase.cmp]
partial def ExSum.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExSum sα a_1 → ExSum sα b → OrderingExSum.cmp : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: ?m.31061sα a: ?m.31071a → ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: ?m.31061sα b: ?m.31091b → Ordering: TypeOrdering
| .zero: ExSum sα q(0).zero, .zero: ExSum sα q(0).zero => .eq: Ordering.eq
| .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add a₁: ExProd sα a✝¹a₁ a₂: ExSum sα b✝¹a₂, .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add b₁: ExProd sα a✝b₁ b₂: ExSum sα b✝b₂ => (a₁: ExProd sα a✝¹a₁.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExProd sα a_1 → ExProd sα b → Orderingcmp b₁: ExProd sα a✝b₁).then: Ordering → Ordering → Orderingthen (a₂: ExSum sα b✝¹a₂.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExSum sα a_1 → ExSum sα b → Orderingcmp b₂: ExSum sα b✝b₂)
| .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → ExSum sα q(0).zero, .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add .. => .lt: Ordering.lt
| .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add .., .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → ExSum sα q(0).zero => .gt: Ordering.gt
end

instance: {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → Inhabited ((e : Q(«\$arg»)) × ExBase sα e)instance : Inhabited: Sort ?u.50694 → Sort (max1?u.50694)Inhabited (Σ e: ?m.50699e, (ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExBase sα: ?m.50691sα) e: ?m.50699e) := ⟨default: {α : Sort ?u.50736} → [self : Inhabited α] → αdefault, .atom: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℕ → ExBase sα e.atom 0: ?m.508980⟩
instance: {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → Inhabited ((e : Q(«\$arg»)) × ExSum sα e)instance : Inhabited: Sort ?u.51025 → Sort (max1?u.51025)Inhabited (Σ e: ?m.51030e, (ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: ?m.51022sα) e: ?m.51030e) := ⟨_: ?m.51060_, .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → ExSum sα q(0).zero⟩
instance: {a : Lean.Level} → {arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → Inhabited ((e : Q(«\$arg»)) × ExProd sα e)instance : Inhabited: Sort ?u.51200 → Sort (max1?u.51200)Inhabited (Σ e: ?m.51205e, (ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: ?m.51197sα) e: ?m.51205e) := ⟨default: {α : Sort ?u.51242} → [self : Inhabited α] → αdefault, .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const 0: ?m.514040 none: {α : Type ?u.51414} → Option αnone⟩

mutual

/-- Converts `ExBase sα` to `ExBase sβ`, assuming `sα` and `sβ` are defeq. -/
partial def ExBase.cast: {a : Lean.Level} →
{arg : Q(Type a)} →
{sα : Q(CommSemiring «\$arg»)} →
{a_1 : Q(«\$arg»)} →
{a_2 : Lean.Level} →
{arg_1 : Q(Type a_2)} → {sβ : Q(CommSemiring «\$arg_1»)} → ExBase sα a_1 → (a : Q(«\$arg_1»)) × ExBase sβ aExBase.cast : ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExBase sα: ?m.51560sα a: ?m.51570a → Σ a: ?m.51601a, ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExBase sβ: ?m.51588sβ a: ?m.51601a
| .atom: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℕ → ExBase sα e.atom i: ℕi => ⟨a: Q(\$arg✝¹)a, .atom: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℕ → ExBase sα e.atom i: ℕi⟩
| .sum: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ExSum sα e → ExBase sα e.sum a: ExSum sα a✝¹a => let ⟨_, vb: ExSum ?m.51850 fst✝vb⟩ := a: ExSum sα a✝¹a.cast: {a : Lean.Level} →
{arg : Q(Type a)} →
{sα : Q(CommSemiring «\$arg»)} →
{a_1 : Q(«\$arg»)} →
{a_2 : Lean.Level} →
{arg_1 : Q(Type a_2)} → {sβ : Q(CommSemiring «\$arg_1»)} → ExSum sα a_1 → (a : Q(«\$arg_1»)) × ExSum sβ acast; ⟨_: ?m.51890_, .sum: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ExSum sα e → ExBase sα e.sum vb: ExSum ?m.51850 fst✝vb⟩

/-- Converts `ExProd sα` to `ExProd sβ`, assuming `sα` and `sβ` are defeq. -/
partial def ExProd.cast: {a : Lean.Level} →
{arg : Q(Type a)} →
{sα : Q(CommSemiring «\$arg»)} →
{a_1 : Q(«\$arg»)} →
{a_2 : Lean.Level} →
{arg_1 : Q(Type a_2)} → {sβ : Q(CommSemiring «\$arg_1»)} → ExProd sα a_1 → (a : Q(«\$arg_1»)) × ExProd sβ aExProd.cast : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: ?m.51622sα a: ?m.51632a → Σ a: ?m.51663a, ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sβ: ?m.51650sβ a: ?m.51663a
| .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const i: ℚi h: Option Exprh => ⟨a: Q(\$arg✝¹)a, .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const i: ℚi h: Option Exprh⟩
| .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul a₁: ExBase sα x✝a₁ a₂: ExProd sℕ e✝a₂ a₃: ExProd sα b✝a₃ => ⟨_: ?m.54038_, .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul a₁: ExBase sα x✝a₁.cast: {a : Lean.Level} →
{arg : Q(Type a)} →
{sα : Q(CommSemiring «\$arg»)} →
{a_1 : Q(«\$arg»)} →
{a_2 : Lean.Level} →
{arg_1 : Q(Type a_2)} → {sβ : Q(CommSemiring «\$arg_1»)} → ExBase sα a_1 → (a : Q(«\$arg_1»)) × ExBase sβ acast.2: {α : Type ?u.54056} → {β : α → Type ?u.54055} → (self : Sigma β) → β self.fst2 a₂: ExProd sℕ e✝a₂ a₃: ExProd sα b✝a₃.cast: {a : Lean.Level} →
{arg : Q(Type a)} →
{sα : Q(CommSemiring «\$arg»)} →
{a_1 : Q(«\$arg»)} →
{a_2 : Lean.Level} →
{arg_1 : Q(Type a_2)} → {sβ : Q(CommSemiring «\$arg_1»)} → ExProd sα a_1 → (a : Q(«\$arg_1»)) × ExProd sβ acast.2: {α : Type ?u.54069} → {β : α → Type ?u.54068} → (self : Sigma β) → β self.fst2⟩

/-- Converts `ExSum sα` to `ExSum sβ`, assuming `sα` and `sβ` are defeq. -/
partial def ExSum.cast: {a : Lean.Level} →
{arg : Q(Type a)} →
{sα : Q(CommSemiring «\$arg»)} →
{a_1 : Q(«\$arg»)} →
{a_2 : Lean.Level} →
{arg_1 : Q(Type a_2)} → {sβ : Q(CommSemiring «\$arg_1»)} → ExSum sα a_1 → (a : Q(«\$arg_1»)) × ExSum sβ aExSum.cast : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: ?m.51684sα a: ?m.51694a → Σ a: ?m.51725a, ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sβ: ?m.51712sβ a: ?m.51725a
| .zero: ExSum sα q(0).zero => ⟨_: ?m.56074_, .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → ExSum sα q(0).zero⟩
| .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add a₁: ExProd sα a✝a₁ a₂: ExSum sα b✝a₂ => ⟨_: ?m.56142_, .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add a₁: ExProd sα a✝a₁.cast: {a : Lean.Level} →
{arg : Q(Type a)} →
{sα : Q(CommSemiring «\$arg»)} →
{a_1 : Q(«\$arg»)} →
{a_2 : Lean.Level} →
{arg_1 : Q(Type a_2)} → {sβ : Q(CommSemiring «\$arg_1»)} → ExProd sα a_1 → (a : Q(«\$arg_1»)) × ExProd sβ acast.2: {α : Type ?u.56159} → {β : α → Type ?u.56158} → (self : Sigma β) → β self.fst2 a₂: ExSum sα b✝a₂.cast: {a : Lean.Level} →
{arg : Q(Type a)} →
{sα : Q(CommSemiring «\$arg»)} →
{a_1 : Q(«\$arg»)} →
{a_2 : Lean.Level} →
{arg_1 : Q(Type a_2)} → {sβ : Q(CommSemiring «\$arg_1»)} → ExSum sα a_1 → (a : Q(«\$arg_1»)) × ExSum sβ acast.2: {α : Type ?u.56172} → {β : α → Type ?u.56171} → (self : Sigma β) → β self.fst2⟩

end

/--
The result of evaluating an (unnormalized) expression `e` into the type family `E`
(one of `ExSum`, `ExProd`, `ExBase`) is a (normalized) element `e'`
and a representation `E e'` for it, and a proof of `e = e'`.
-/
structure Result: {u : Lean.Level} → {α : Q(Type u)} → (Q(«\$α») → Type) → Q(«\$α») → TypeResult {α: Q(Type u)α : Q(Type u: ?m.59383Type u)} (E: Q(«\$α») → TypeE : Q(\$α: Type uα) → Type: Type 1Type) (e: Q(«\$α»)e : Q(\$α: Type uα)) where
/-- The normalized result. -/
expr: {u : Lean.Level} → {α : Q(Type u)} → {E : Q(«\$α») → Type} → {e : Q(«\$α»)} → Result E e → Q(«\$α»)expr : Q(\$α: Type uα)
/-- The data associated to the normalization. -/
val: {u : Lean.Level} → {α : Q(Type u)} → {E : Q(«\$α») → Type} → {e : Q(«\$α»)} → (self : Result E e) → E self.exprval : E: Q(«\$α») → TypeE expr: Q(«\$α»)expr
/-- A proof that the original expression is equal to the normalized result. -/
proof: {u : Lean.Level} → {α : Q(Type u)} → {E : Q(«\$α») → Type} → {e : Q(«\$α»)} → (self : Result E e) → Q(«\$e» = dummy)proof : Q(\$e: «\$α»ee = \$expr: ?m.59383 = \$expr: «\$α»expr)

instance: {a : Lean.Level} →
{α : Q(Type a)} →
{E : Q(«\$α») → Type} → {e : Q(«\$α»)} → [inst : Inhabited ((e : Q(«\$α»)) × E e)] → Inhabited (Result E e)instance [Inhabited: Sort ?u.60122 → Sort (max1?u.60122)Inhabited (Σ e: unknown metavariable '?_uniq.60103'e, E: ?m.60095E e: ?m.60127e)] : Inhabited: Sort ?u.60134 → Sort (max1?u.60134)Inhabited (Result: {u : Lean.Level} → {α : Q(Type u)} → (Q(«\$α») → Type) → Q(«\$α») → TypeResult E: ?m.60095E e: ?m.60119e) :=
let ⟨e': Q(\$α✝)e', v: E e'v⟩ : Σ e: ?m.60157e, E: Q(\$α✝) → TypeE e: ?m.60157e := default: {α : Sort ?u.60161} → [self : Inhabited α] → αdefault; ⟨e': Q(\$α✝)e', v: E e'v, default: {α : Sort ?u.60365} → [self : Inhabited α] → αdefault⟩

variable {α: Q(Type u)α : Q(Type u: Type (u+1)Type u)} (sα: Q(CommSemiring «\$α»)sα : Q(CommSemiring: Type ?u.242276 → Type ?u.242276CommSemiringCommSemiring \$α: ?m.242265 \$α: Type uα)) [CommSemiring: Type ?u.230043 → Type ?u.230043CommSemiring R: ?m.340925R]

/--
Constructs the expression corresponding to `.const n`.
(The `.const` constructor does not check that the expression is correct.)
-/
def ExProd.mkNat: {u : Lean.Level} → {α : Q(Type u)} → (sα : Q(CommSemiring «\$α»)) → ℕ → (e : Q(«\$α»)) × ExProd sα eExProd.mkNat (n: ℕn : ℕ: Typeℕ) : (e: Q(«\$α»)e : Q(\$α: Type uα)) × ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα e: Q(«\$α»)e :=
let lit: Q(ℕ)lit : Q(ℕ: Typeℕ) := mkRawNatLit: ℕ → ExprmkRawNatLit n: ℕn
⟨q((\$lit: ℕlit).rawCast: {α : Type ?u.60868} → [inst : AddMonoidWithOne α] → ℕ → αrawCast : \$α: Type uα), .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const n: ℕn none: {α : Type ?u.61160} → Option αnone⟩

/--
Constructs the expression corresponding to `.const (-n)`.
(The `.const` constructor does not check that the expression is correct.)
-/
def ExProd.mkNegNat: Q(Ring «\$α») → ℕ → (e : Q(«\$α»)) × ExProd sα eExProd.mkNegNat (_: Q(Ring «\$α»)_ : Q(Ring: Type ?u.61327 → Type ?u.61327RingRing \$α: ?m.61290 \$α: Type uα)) (n: ℕn : ℕ: Typeℕ) : (e: Q(«\$α»)e : Q(\$α: Type uα)) × ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα e: Q(«\$α»)e :=
let lit: Q(ℕ)lit : Q(ℕ: Typeℕ) := mkRawNatLit: ℕ → ExprmkRawNatLit n: ℕn
⟨q((Int.negOfNat: ℕ → ℤInt.negOfNat \$lit: ℕlit).rawCast: {α : Type ?u.61379} → [inst : Ring α] → ℤ → αrawCast : \$α: Type uα), .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const (-n: ℕn) none: {α : Type ?u.61512} → Option αnone⟩

/--
Constructs the expression corresponding to `.const (-n)`.
(The `.const` constructor does not check that the expression is correct.)
-/
def ExProd.mkRat: {u : Lean.Level} →
{α : Q(Type u)} →
(sα : Q(CommSemiring «\$α»)) → Q(DivisionRing «\$α») → ℚ → Q(ℤ) → Q(ℕ) → Expr → (e : Q(«\$α»)) × ExProd sα eExProd.mkRat (_: Q(DivisionRing «\$α»)_ : Q(DivisionRing: Type ?u.61662 → Type ?u.61662DivisionRingDivisionRing \$α: ?m.61625 \$α: Type uα)) (q: ℚq : ℚ: Typeℚ) (n: Q(ℤ)n : Q(ℤ: Typeℤ)) (d: Q(ℕ)d : Q(ℕ: Typeℕ)) (h: Exprh : Expr: TypeExpr) :
(e: Q(«\$α»)e : Q(\$α: Type uα)) × ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα e: Q(«\$α»)e :=
⟨q(Rat.rawCast: {α : Type ?u.61728} → [inst : DivisionRing α] → ℤ → ℕ → αRat.rawCast \$n: ℤn \$d: ℕd : \$α: Type uα), .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const q: ℚq h: Exprh⟩

section
variable {sα: ?m.61977sα}

/-- Embed an exponent (a `ExBase, ExProd` pair) as a `ExProd` by multiplying by 1. -/
def ExBase.toProd: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{a : Q(«\$α»)} → {b : Q(ℕ)} → ExBase sα a → ExProd sℕ b → ExProd sα q(«\$a» ^ «\$b» * Nat.rawCast 1)ExBase.toProd (va: ExBase sα ava : ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExBase sα: Q(CommSemiring «\$α»)sα a: ?m.62028a) (vb: ExProd sℕ bvb : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sℕ: Q(CommSemiring ℕ)sℕ b: ?m.62038b) :
ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα q(\$a: «\$α»aa ^ \$b * (nat_lit 1).rawCast: ?m.61984 ^ \$b: ℕba ^ \$b * (nat_lit 1).rawCast: ?m.61984 * (nat_lit 1: ℕnat_litnat_lit 1: ℕ 1a ^ \$b * (nat_lit 1).rawCast: ?m.61984).rawCast: {α : Type ?u.62062} → [inst : AddMonoidWithOne α] → ℕ → αrawCast) := .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul va: ExBase sα ava vb: ExProd sℕ bvb (.const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const 1: ?m.630371 none: {α : Type ?u.63047} → Option αnone)

/-- Embed `ExProd` in `ExSum` by adding 0. -/
def ExProd.toSum: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ExProd sα e → ExSum sα q(«\$e» + 0)ExProd.toSum (v: ExProd sα ev : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα e: ?m.63212e) : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: Q(CommSemiring «\$α»)sα q(\$e: «\$α»ee + 0: ?m.63168 + 0: ?m.632290) := .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add v: ExProd sα ev .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → ExSum sα q(0).zero

/-- Get the leading coefficient of a `ExProd`. -/
def ExProd.coeff: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ExProd sα e → ℚExProd.coeff : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα e: ?m.63982e → ℚ: Typeℚ
| .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const q: ℚq _ => q: ℚq
| .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul _ _ v: ExProd sα b✝v => v: ExProd sα b✝v.coeff: {e : Q(«\$α»)} → ExProd sα e → ℚcoeff
end

/--
Two monomials are said to "overlap" if they differ by a constant factor, in which case the
constants just add. When this happens, the constant may be either zero (if the monomials cancel)
or nonzero (if they add up); the zero case is handled specially.
-/
inductive Overlap: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeOverlap (e: Q(«\$α»)e : Q(\$α: Type uα)) where
/-- The expression `e` (the sum of monomials) is equal to `0`. -/
| zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → Q(IsNat «\$e» 0) → Overlap sα ezero (_: Q(IsNat «\$e» 0)_ : Q(IsNat: {α : Type ?u.68605} → [inst : AddMonoidWithOne α] → α → ℕ → PropIsNatIsNat \$e (nat_lit 0): ?m.68558 \$e: «\$α»eIsNat \$e (nat_lit 0): ?m.68558 (nat_lit 0: ℕnat_litnat_lit 0: ℕ 0IsNat \$e (nat_lit 0): ?m.68558)))
/-- The expression `e` (the sum of monomials) is equal to another monomial
| nonzero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → Result (ExProd sα) e → Overlap sα enonzero (_: Result (ExProd sα) e_ : Result: {u : Lean.Level} → {α : Q(Type u)} → (Q(«\$α») → Type) → Q(«\$α») → TypeResult (ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα) e: Q(«\$α»)e)

theorem add_overlap_pf: ∀ {a b c : R} (x : R) (e : ℕ), a + b = c → x ^ e * a + x ^ e * b = x ^ e * cadd_overlap_pf (x: Rx : R: ?m.69571R) (e: unknown metavariable '?_uniq.69616'e) (pq_pf: a + b = cpq_pf : a: ?m.69598a + b: ?m.69611b = c: ?m.69624c) :
x: Rx ^ e: ?m.69629e * a: ?m.69598a + x: Rx ^ e: ?m.69629e * b: ?m.69611b = x: Rx ^ e: ?m.69629e * c: ?m.69624c := byGoals accomplished! 🐙 u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b, c, x: Re: ℕpq_pf: a + b = cx ^ e * a + x ^ e * b = x ^ e * csubst_varsu: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b, x: Re: ℕx ^ e * a + x ^ e * b = x ^ e * (a + b);u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b, x: Re: ℕx ^ e * a + x ^ e * b = x ^ e * (a + b) u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b, c, x: Re: ℕpq_pf: a + b = cx ^ e * a + x ^ e * b = x ^ e * csimp [mul_add: ∀ {R : Type ?u.71547} [inst : Mul R] [inst_1 : Add R] [inst_2 : LeftDistribClass R] (a b c : R),
a * (b + c) = a * b + a * cmul_add]Goals accomplished! 🐙

theorem add_overlap_pf_zero: ∀ {a b : R} (x : R) (e : ℕ), IsNat (a + b) 0 → IsNat (x ^ e * a + x ^ e * b) 0add_overlap_pf_zero (x: Rx : R: ?m.72347R) (e: unknown metavariable '?_uniq.72394'e) :
IsNat: {α : Type ?u.72426} → [inst : AddMonoidWithOne α] → α → ℕ → PropIsNat (a: ?m.72389a + b: ?m.72417b) (nat_lit 0: ℕnat_litnat_lit 0: ℕ 0) → IsNat: {α : Type ?u.72479} → [inst : AddMonoidWithOne α] → α → ℕ → PropIsNat (x: Rx ^ e: ?m.72422e * a: ?m.72389a + x: Rx ^ e: ?m.72422e * b: ?m.72417b) (nat_lit 0: ℕnat_litnat_lit 0: ℕ 0)
| ⟨h: a + b = ↑0h⟩ => ⟨byGoals accomplished! 🐙 u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b, x: Re: ℕh: a + b = ↑0x ^ e * a + x ^ e * b = ↑0simp [h: a + b = ↑0h, ← mul_add: ∀ {R : Type ?u.74808} [inst : Mul R] [inst_1 : Add R] [inst_2 : LeftDistribClass R] (a b c : R),
a * (b + c) = a * b + a * cmul_add]Goals accomplished! 🐙⟩

/--
Given monomials `va, vb`, attempts to add them together to get another monomial.
If the monomials are not compatible, returns `none`.
For example, `xy + 2xy = 3xy` is a `.nonzero` overlap, while `xy + xz` returns `none`
and `xy + -xy = 0` is a `.zero` overlap.
-/
def evalAddOverlap: {a b : Q(«\$α»)} → ExProd sα a → ExProd sα b → Option (Overlap sα q(«\$a» + «\$b»))evalAddOverlap (va: ExProd sα ava : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα a: ?m.76183a) (vb: ExProd sα bvb : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα b: ?m.76193b) : Option: Type ?u.76204 → Type ?u.76204Option (Overlap: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeOverlap sα: Q(CommSemiring «\$α»)sα q(\$a: «\$α»aa + \$b: ?m.76139 + \$b: «\$α»b)) :=
match va: ExProd sα ava, vb: ExProd sα bvb with
| .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const za: ℚza ha: Option Exprha, .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const zb: ℚzb hb: Option Exprhb => do
let ra: ?m.82497ra := Result.ofRawRat: {u : Lean.Level} → {α : Q(Type u)} → ℚ → (e : Q(«\$α»)) → optParam (Option Expr) none → NormNum.Result eResult.ofRawRat za: ℚza a: Q(«\$α»)a ha: Option Exprha; let rb: ?m.82507rb := Result.ofRawRat: {u : Lean.Level} → {α : Q(Type u)} → ℚ → (e : Q(«\$α»)) → optParam (Option Expr) none → NormNum.Result eResult.ofRawRat zb: ℚzb b: Q(«\$α»)b hb: Option Exprhb
let res: ?m.82561res ← NormNum.evalAdd.core: {u : Lean.Level} →
{α : Q(Type u)} →
(e : Q(«\$α»)) →
Q(«\$α» → «\$α» → «\$α») → (a b : Q(«\$α»)) → NormNum.Result a → NormNum.Result b → Option (NormNum.Result e)NormNum.evalAdd.core q(\$a: «\$α»aa + \$b: ?m.76139 + \$b: «\$α»b) q(Add.add: ?m.76139Add.add) _: Q(«\$α»)_ _: Q(«\$α»)_ ra: ?m.82497ra rb: ?m.82507rb
match res: ?m.82561res with
| .isNat: {u : Lean.Level} →
{α : Q(Type u)} →
{x : Q(«\$α»)} →
(inst : autoParam Q(AddMonoidWithOne «\$α») _auto✝) → (lit : Q(ℕ)) → Q(IsNat «\$x» «\$lit») → NormNum.Result x.isNat _ (.lit: Lean.Literal → Expr.lit (.natVal: ℕ → Lean.Literal.natVal 0: ℕ0)) p: Q(IsNat («\$a» + «\$b») 0)p => pure: {f : Type ?u.82592 → Type ?u.82591} → [self : Pure f] → {α : Type ?u.82592} → α → f αpure <| .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → Q(IsNat «\$e» 0) → Overlap sα e.zero p: Q(IsNat («\$a» + «\$b») 0)p
| rc: NormNum.Result ?m.82555rc =>
let ⟨zc: ℚzc, hc: Option Exprhc⟩ ← rc: NormNum.Result ?m.82555rc.toRatNZ: {a : Lean.Level} → {α : Q(Type a)} → {e : Q(«\$α»)} → NormNum.Result e → Option (ℚ × Option Expr)toRatNZ
let ⟨c: Q(«\$α»)c, pc: Q(«\$a» + «\$b» = «\$c»)pc⟩ := rc: NormNum.Result ?m.82555rc.toRawEq: {u : Lean.Level} → {α : Q(Type u)} → {e : Q(«\$α»)} → NormNum.Result e → (e' : Q(«\$α»)) × Q(«\$e» = «\$e'»)toRawEq
pure: {f : Type ?u.82785 → Type ?u.82784} → [self : Pure f] → {α : Type ?u.82785} → α → f αpure <| .nonzero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → Result (ExProd sα) e → Overlap sα e.nonzero ⟨c: Q(«\$α»)c, .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const zc: ℚzc hc: Option Exprhc, pc: Q(«\$a» + «\$b» = «\$c»)pc⟩
| .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul (x := a₁: Q(«\$α»)a₁) (e := a₂: Q(ℕ)a₂) va₁: ExBase sα a₁va₁ va₂: ExProd sℕ a₂va₂ va₃: ExProd sα b✝¹va₃, .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul vb₁: ExBase sα x✝vb₁ vb₂: ExProd sℕ e✝vb₂ vb₃: ExProd sα b✝vb₃ => do
guard: {f : Type → Type ?u.84261} → [inst : Alternative f] → (p : Prop) → [inst : Decidable p] → f Unitguard (va₁: ExBase sα a₁va₁.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExBase sα a_1 → ExBase sα b → Booleq vb₁: ExBase sα x✝vb₁ && va₂: ExProd sℕ a₂va₂.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExProd sα a_1 → ExProd sα b → Booleq vb₂: ExProd sℕ e✝vb₂)
match ← evalAddOverlap: {a b : Q(«\$α»)} → ExProd sα a → ExProd sα b → Option (Overlap sα q(«\$a» + «\$b»))evalAddOverlap va₃: ExProd sα b✝¹va₃ vb₃: ExProd sα b✝vb₃ with
| .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → Q(IsNat «\$e» 0) → Overlap sα e.zero p: Q(IsNat (\$b✝¹ + \$b✝) 0)p => pure: {f : Type ?u.84464 → Type ?u.84463} → [self : Pure f] → {α : Type ?u.84464} → α → f αpure <| .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → Q(IsNat «\$e» 0) → Overlap sα e.zero (q(add_overlap_pf_zero: ∀ {R : Type ?u.84513} [inst : CommSemiring R] {a b : R} (x : R) (e : ℕ),
IsNat (a + b) 0 → IsNat (x ^ e * a + x ^ e * b) 0add_overlap_pf_zeroadd_overlap_pf_zero \$a₁ \$a₂ \$p: ?m.76139 \$a₁: «\$α»a₁add_overlap_pf_zero \$a₁ \$a₂ \$p: ?m.76139 \$a₂: ℕa₂add_overlap_pf_zero \$a₁ \$a₂ \$p: ?m.76139 \$p: IsNat (\$b✝¹ + \$b✝) 0p) : Expr: TypeExpr)
| .nonzero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → Result (ExProd sα) e → Overlap sα e.nonzero ⟨_, vc: ExProd sα expr✝vc, p: Q(\$b✝¹ + \$b✝ = \$expr✝)p⟩ =>
pure: {f : Type ?u.84604 → Type ?u.84603} → [self : Pure f] → {α : Type ?u.84604} → α → f αpure <| .nonzero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → Result (ExProd sα) e → Overlap sα e.nonzero ⟨_: Q(«\$α»)_, .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul va₁: ExBase sα a₁va₁ va₂: ExProd sℕ a₂va₂ vc: ExProd sα expr✝vc, (q(add_overlap_pf: ∀ {R : Type ?u.84659} [inst : CommSemiring R] {a b c : R} (x : R) (e : ℕ), a + b = c → x ^ e * a + x ^ e * b = x ^ e * cadd_overlap_pfadd_overlap_pf \$a₁ \$a₂ \$p: ?m.76139 \$a₁: «\$α»a₁add_overlap_pf \$a₁ \$a₂ \$p: ?m.76139 \$a₂: ℕa₂add_overlap_pf \$a₁ \$a₂ \$p: ?m.76139 \$p: \$b✝¹ + \$b✝ = \$expr✝p) : Expr: TypeExpr)⟩
| _, _ => none: {α : Type ?u.84840} → Option αnone

theorem add_pf_zero_add: ∀ (b : R), 0 + b = badd_pf_zero_add (b: Rb : R: ?m.98733R) : 0: ?m.987570 + b: Rb = b: Rb := byGoals accomplished! 🐙 u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Rb: R0 + b = bsimpGoals accomplished! 🐙

theorem add_pf_add_zero: ∀ {R : Type u_1} [inst : CommSemiring R] (a : R), a + 0 = aadd_pf_add_zero (a: Ra : R: ?m.99718R) : a: Ra + 0: ?m.997420 = a: Ra := byGoals accomplished! 🐙 u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra: Ra + 0 = asimpGoals accomplished! 🐙

theorem add_pf_add_overlap: ∀ {a₁ b₁ c₁ a₂ b₂ c₂ : R}, a₁ + b₁ = c₁ → a₂ + b₂ = c₂ → a₁ + a₂ + (b₁ + b₂) = c₁ + c₂add_pf_add_overlap
(_: a₁ + b₁ = c₁_ : a₁: ?m.100725a₁ + b₁: ?m.100733b₁ = c₁: ?m.100741c₁) (_: a₂ + b₂ = c₂_ : a₂: ?m.100773a₂ + b₂: ?m.100805b₂ = c₂: ?m.100837c₂) : (a₁: ?m.100725a₁ + a₂: ?m.100773a₂ : R: ?m.100703R) + (b₁: ?m.100733b₁ + b₂: ?m.100805b₂) = c₁: ?m.100741c₁ + c₂: ?m.100837c₂ := byGoals accomplished! 🐙
u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra₁, b₁, c₁, a₂, b₂, c₂: Rx✝¹: a₁ + b₁ = c₁x✝: a₂ + b₂ = c₂a₁ + a₂ + (b₁ + b₂) = c₁ + c₂subst_varsu: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra₁, b₁, a₂, b₂: Ra₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂);u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra₁, b₁, a₂, b₂: Ra₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂) u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra₁, b₁, c₁, a₂, b₂, c₂: Rx✝¹: a₁ + b₁ = c₁x✝: a₂ + b₂ = c₂a₁ + a₂ + (b₁ + b₂) = c₁ + c₂simp [add_assoc: ∀ {G : Type ?u.101908} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)add_assoc, add_left_comm: ∀ {G : Type ?u.101926} [inst : AddCommSemigroup G] (a b c : G), a + (b + c) = b + (a + c)add_left_comm]Goals accomplished! 🐙

theorem add_pf_add_overlap_zero: ∀ {a₁ b₁ a₂ b₂ c : R}, IsNat (a₁ + b₁) 0 → a₂ + b₂ = c → a₁ + a₂ + (b₁ + b₂) = cadd_pf_add_overlap_zero
(h: IsNat (a₁ + b₁) 0h : IsNat: {α : Type ?u.102948} → [inst : AddMonoidWithOne α] → α → ℕ → PropIsNat (a₁: ?m.102799a₁ + b₁: ?m.102821b₁) (nat_lit 0: ℕnat_litnat_lit 0: ℕ 0)) (h₄: a₂ + b₂ = ch₄ : a₂: ?m.102883a₂ + b₂: ?m.102945b₂ = c: ?m.103007c) : (a₁: ?m.102799a₁ + a₂: ?m.102883a₂ : R: ?m.102763R) + (b₁: ?m.102821b₁ + b₂: ?m.102945b₂) = c: ?m.103007c := byGoals accomplished! 🐙

theorem add_pf_add_lt: ∀ {a₂ b c : R} (a₁ : R), a₂ + b = c → a₁ + a₂ + b = a₁ + cadd_pf_add_lt (a₁: Ra₁ : R: ?m.104921R) (_: a₂ + b = c_ : a₂: ?m.104945a₂ + b: ?m.104955b = c: ?m.104965c) : (a₁: Ra₁ + a₂: ?m.104945a₂) + b: ?m.104955b = a₁: Ra₁ + c: ?m.104965c := byGoals accomplished! 🐙 u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra₂, b, c, a₁: Rx✝: a₂ + b = ca₁ + a₂ + b = a₁ + csimp [*, add_assoc: ∀ {G : Type ?u.105804} [inst : AddSemigroup G] (a b c : G), a + b + c = a + (b + c)add_assoc]Goals accomplished! 🐙

theorem add_pf_add_gt: ∀ {R : Type u_1} [inst : CommSemiring R] {a b₂ c : R} (b₁ : R), a + b₂ = c → a + (b₁ + b₂) = b₁ + cadd_pf_add_gt (b₁: Rb₁ : R: ?m.106195R) (_: a + b₂ = c_ : a: ?m.106219a + b₂: ?m.106229b₂ = c: ?m.106239c) : a: ?m.106219a + (b₁: Rb₁ + b₂: ?m.106229b₂) = b₁: Rb₁ + c: ?m.106239c := byGoals accomplished! 🐙
u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₂, c, b₁: Rx✝: a + b₂ = ca + (b₁ + b₂) = b₁ + csubst_varsu: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₂, b₁: Ra + (b₁ + b₂) = b₁ + (a + b₂);u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₂, b₁: Ra + (b₁ + b₂) = b₁ + (a + b₂) u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₂, c, b₁: Rx✝: a + b₂ = ca + (b₁ + b₂) = b₁ + csimp [add_left_comm: ∀ {G : Type ?u.107087} [inst : AddCommSemigroup G] (a b c : G), a + (b + c) = b + (a + c)add_left_comm]Goals accomplished! 🐙

/-- Adds two polynomials `va, vb` together to get a normalized result polynomial.

* `0 + b = 0`
* `a + 0 = 0`
* `a * x + a * y = a * (x + y)` (for `x`, `y` coefficients; uses `evalAddOverlap`)
* `(a₁ + a₂) + (b₁ + b₂) = a₁ + (a₂ + (b₁ + b₂))` (if `a₁.lt b₁`)
* `(a₁ + a₂) + (b₁ + b₂) = b₁ + ((a₁ + a₂) + b₂)` (if not `a₁.lt b₁`)
-/
partial def evalAdd: {a b : Q(«\$α»)} → ExSum sα a → ExSum sα b → Result (ExSum sα) q(«\$a» + «\$b»)evalAdd (va: ExSum sα ava : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: Q(CommSemiring «\$α»)sα a: ?m.107600a) (vb: ExSum sα bvb : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: Q(CommSemiring «\$α»)sα b: ?m.107610b) : Result: {u : Lean.Level} → {α : Q(Type u)} → (Q(«\$α») → Type) → Q(«\$α») → TypeResult (ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: Q(CommSemiring «\$α»)sα) q(\$a: «\$α»aa + \$b: ?m.107556 + \$b: «\$α»b) :=
match va: ExSum sα ava, vb: ExSum sα bvb with
| .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → ExSum sα q(0).zero, vb: ExSum sα bvb => ⟨b: Q(«\$α»)b, vb: ExSum sα bvb, q(add_pf_zero_add: ∀ {R : Type ?u.110724} [inst : CommSemiring R] (b : R), 0 + b = badd_pf_zero_addadd_pf_zero_add \$b: ?m.107556 \$b: «\$α»b)⟩
| va: ExSum sα ava, .zero: ExSum sα q(0).zero => ⟨a: Q(«\$α»)a, va: ExSum sα ava, q(add_pf_add_zero: ∀ {R : Type ?u.110771} [inst : CommSemiring R] (a : R), a + 0 = aadd_pf_add_zeroadd_pf_add_zero \$a: ?m.107556 \$a: «\$α»a)⟩
| .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add (a := a₁: Q(«\$α»)a₁) (b := _a₂: Q(«\$α»)_a₂) va₁: ExProd sα a₁va₁ va₂: ExSum sα _a₂va₂, .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add (a := b₁: Q(«\$α»)b₁) (b := _b₂: Q(«\$α»)_b₂) vb₁: ExProd sα b₁vb₁ vb₂: ExSum sα _b₂vb₂ =>
match evalAddOverlap: {u : Lean.Level} →
{α : Q(Type u)} →
(sα : Q(CommSemiring «\$α»)) → {a b : Q(«\$α»)} → ExProd sα a → ExProd sα b → Option (Overlap sα q(«\$a» + «\$b»))evalAddOverlap sα: Q(CommSemiring «\$α»)sα va₁: ExProd sα a₁va₁ vb₁: ExProd sα b₁vb₁ with
| some: {α : Type ?u.110859} → α → Option αsome (.nonzero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → Result (ExProd sα) e → Overlap sα e.nonzero ⟨_, vc₁: ExProd sα expr✝vc₁, pc₁: Q(«\$a₁» + «\$b₁» = \$expr✝)pc₁⟩) =>
let ⟨_, vc₂: ExSum sα expr✝vc₂, pc₂: Q(«\$_a₂» + «\$_b₂» = \$expr✝)pc₂⟩ := evalAdd: {a b : Q(«\$α»)} → ExSum sα a → ExSum sα b → Result (ExSum sα) q(«\$a» + «\$b»)evalAdd va₂: ExSum sα _a₂va₂ vb₂: ExSum sα _b₂vb₂
⟨_: Q(«\$α»)_, .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add vc₁: ExProd sα expr✝¹vc₁ vc₂: ExSum sα expr✝vc₂, q(add_pf_add_overlap: ∀ {R : Type ?u.110972} [inst : CommSemiring R] {a₁ b₁ c₁ a₂ b₂ c₂ : R},
a₁ + b₁ = c₁ → a₂ + b₂ = c₂ → a₁ + a₂ + (b₁ + b₂) = c₁ + c₂add_pf_add_overlapadd_pf_add_overlap \$pc₁ \$pc₂: ?m.107556 \$pc₁: «\$a₁» + «\$b₁» = \$expr✝¹pc₁add_pf_add_overlap \$pc₁ \$pc₂: ?m.107556 \$pc₂: «\$_a₂» + «\$_b₂» = \$expr✝pc₂)⟩
| some: {α : Type ?u.111094} → α → Option αsome (.zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → Q(IsNat «\$e» 0) → Overlap sα e.zero pc₁: Q(IsNat («\$a₁» + «\$b₁») 0)pc₁) =>
let ⟨c₂: Q(«\$α»)c₂, vc₂: ExSum sα c₂vc₂, pc₂: Q(«\$_a₂» + «\$_b₂» = «\$c₂»)pc₂⟩ := evalAdd: {a b : Q(«\$α»)} → ExSum sα a → ExSum sα b → Result (ExSum sα) q(«\$a» + «\$b»)evalAdd va₂: ExSum sα _a₂va₂ vb₂: ExSum sα _b₂vb₂
⟨c₂: Q(«\$α»)c₂, vc₂: ExSum sα c₂vc₂, q(add_pf_add_overlap_zero: ∀ {R : Type ?u.111188} [inst : CommSemiring R] {a₁ b₁ a₂ b₂ c : R},
IsNat (a₁ + b₁) 0 → a₂ + b₂ = c → a₁ + a₂ + (b₁ + b₂) = cadd_pf_add_overlap_zeroadd_pf_add_overlap_zero \$pc₁ \$pc₂: ?m.107556 \$pc₁: IsNat («\$a₁» + «\$b₁») 0pc₁add_pf_add_overlap_zero \$pc₁ \$pc₂: ?m.107556 \$pc₂: «\$_a₂» + «\$_b₂» = «\$c₂»pc₂)⟩
| none: {α : Type ?u.111303} → Option αnone =>
if let .lt: Ordering.lt := va₁: ExProd sα a₁va₁.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExProd sα a_1 → ExProd sα b → Orderingcmp vb₁: ExProd sα b₁vb₁ then
let ⟨_c: Q(«\$α»)_c, vc: ExSum sα _cvc, (pc: Q(«\$_a₂» + («\$b₁» + «\$_b₂») = «\$_c»)pc : Q(\$_a₂ + (\$b₁ + \$_b₂) = \$_c))⟩ := evalAdd: {a b : Q(«\$α»)} → ExSum sα a → ExSum sα b → Result (ExSum sα) q(«\$a» + «\$b»)evalAdd va₂: ExSum sα _a₂va₂ vb: ExSum sα bvb
⟨_: Q(«\$α»)_, .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add va₁: ExProd sα a₁va₁ vc: ExSum sα _cvc, q(add_pf_add_lt: ∀ {R : Type ?u.112010} [inst : CommSemiring R] {a₂ b c : R} (a₁ : R), a₂ + b = c → a₁ + a₂ + b = a₁ + cadd_pf_add_ltadd_pf_add_lt \$a₁ \$pc: ?m.107556 \$a₁: «\$α»a₁add_pf_add_lt \$a₁ \$pc: ?m.107556 \$pc: «\$_a₂» + («\$b₁» + «\$_b₂») = «\$_c»pc)⟩
else
let ⟨_c: Q(«\$α»)_c, vc: ExSum sα _cvc, (pc: Q(«\$a₁» + «\$_a₂» + «\$_b₂» = «\$_c»)pc : Q(\$a₁ + \$_a₂ + \$_b₂ = \$_c))⟩ := evalAdd: {a b : Q(«\$α»)} → ExSum sα a → ExSum sα b → Result (ExSum sα) q(«\$a» + «\$b»)evalAdd va: ExSum sα ava vb₂: ExSum sα _b₂vb₂
⟨_: Q(«\$α»)_, .add: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → ExSum sα q(«\$a» + «\$b»).add vb₁: ExProd sα b₁vb₁ vc: ExSum sα _cvc, q(add_pf_add_gt: ∀ {R : Type ?u.112818} [inst : CommSemiring R] {a b₂ c : R} (b₁ : R), a + b₂ = c → a + (b₁ + b₂) = b₁ + cadd_pf_add_gtadd_pf_add_gt \$b₁ \$pc: ?m.107556 \$b₁: «\$α»b₁add_pf_add_gt \$b₁ \$pc: ?m.107556 \$pc: «\$a₁» + «\$_a₂» + «\$_b₂» = «\$_c»pc)⟩

theorem one_mul: ∀ {R : Type u_1} [inst : CommSemiring R] (a : R), Nat.rawCast 1 * a = aone_mul (a: Ra : R: ?m.122733R) : (nat_lit 1: ℕnat_litnat_lit 1: ℕ 1).rawCast: {α : Type ?u.122756} → [inst : AddMonoidWithOne α] → ℕ → αrawCast * a: Ra = a: Ra := byGoals accomplished! 🐙 u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra: RNat.rawCast 1 * a = asimp [Nat.rawCast: {α : Type ?u.123398} → [inst : AddMonoidWithOne α] → ℕ → αNat.rawCast]Goals accomplished! 🐙

theorem mul_one: ∀ (a : R), a * Nat.rawCast 1 = amul_one (a: Ra : R: ?m.124033R) : a: Ra * (nat_lit 1: ℕnat_litnat_lit 1: ℕ 1).rawCast: {α : Type ?u.124056} → [inst : AddMonoidWithOne α] → ℕ → αrawCast = a: Ra := byGoals accomplished! 🐙 u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra: Ra * Nat.rawCast 1 = asimp [Nat.rawCast: {α : Type ?u.124698} → [inst : AddMonoidWithOne α] → ℕ → αNat.rawCast]Goals accomplished! 🐙

theorem mul_pf_left: ∀ {a₃ b c : R} (a₁ : R) (a₂ : ℕ), a₃ * b = c → a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * cmul_pf_left (a₁: Ra₁ : R: ?m.125329R) (a₂: unknown metavariable '?_uniq.125348'a₂) (_: a₃ * b = c_ : a₃: ?m.125356a₃ * b: ?m.125369b = c: ?m.125382c) : (a₁: Ra₁ ^ a₂: ?m.125387a₂ * a₃: ?m.125356a₃ : R: ?m.125329R) * b: ?m.125369b = a₁: Ra₁ ^ a₂: ?m.125387a₂ * c: ?m.125382c := byGoals accomplished! 🐙
u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra₃, b, c, a₁: Ra₂: ℕx✝: a₃ * b = ca₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * csubst_varsu: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra₃, b, a₁: Ra₂: ℕa₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b);u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra₃, b, a₁: Ra₂: ℕa₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b) u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra₃, b, c, a₁: Ra₂: ℕx✝: a₃ * b = ca₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * crw [u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra₃, b, a₁: Ra₂: ℕa₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b)mul_assoc: ∀ {G : Type ?u.126513} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assocu: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra₃, b, a₁: Ra₂: ℕa₁ ^ a₂ * (a₃ * b) = a₁ ^ a₂ * (a₃ * b)]Goals accomplished! 🐙

theorem mul_pf_right: ∀ {a b₃ c : R} (b₁ : R) (b₂ : ℕ), a * b₃ = c → a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * cmul_pf_right (b₁: Rb₁ : R: ?m.126674R) (b₂: ℕb₂) (_: a * b₃ = c_ : a: ?m.126701a * b₃: ?m.126714b₃ = c: ?m.126727c) : a: ?m.126701a * (b₁: Rb₁ ^ b₂: ?m.126732b₂ * b₃: ?m.126714b₃) = b₁: Rb₁ ^ b₂: ?m.126732b₂ * c: ?m.126727c := byGoals accomplished! 🐙
u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₃, c, b₁: Rb₂: ℕx✝: a * b₃ = ca * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * csubst_varsu: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₃, b₁: Rb₂: ℕa * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃);u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₃, b₁: Rb₂: ℕa * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃) u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₃, c, b₁: Rb₂: ℕx✝: a * b₃ = ca * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * crw [u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₃, b₁: Rb₂: ℕa * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃)mul_left_comm: ∀ {G : Type ?u.128023} [inst : CommSemigroup G] (a b c : G), a * (b * c) = b * (a * c)mul_left_commu: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₃, b₁: Rb₂: ℕb₁ ^ b₂ * (a * b₃) = b₁ ^ b₂ * (a * b₃)]Goals accomplished! 🐙

theorem mul_pp_pf_overlap: ∀ {ea eb e : ℕ} {a₂ b₂ c : R} (x : R), ea + eb = e → a₂ * b₂ = c → x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * cmul_pp_pf_overlap (x: Rx : R: ?m.128163R) (_: ea + eb = e_ : ea: ?m.128187ea + eb: ?m.128197eb = e: ?m.128207e) (_: a₂ * b₂ = c_ : a₂: ?m.128241a₂ * b₂: ?m.128275b₂ = c: ?m.128309c) :
(x: Rx ^ ea: ?m.128187ea * a₂: ?m.128241a₂ : R: ?m.128163R) * (x: Rx ^ eb: ?m.128197eb * b₂: ?m.128275b₂) = x: Rx ^ e: ?m.128207e * c: ?m.128309c := byGoals accomplished! 🐙
u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Rea, eb, e: ℕa₂, b₂, c, x: Rx✝¹: ea + eb = ex✝: a₂ * b₂ = cx ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * csubst_varsu: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Rea, eb: ℕa₂, b₂, x: Rx ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂);u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Rea, eb: ℕa₂, b₂, x: Rx ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂) u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Rea, eb, e: ℕa₂, b₂, c, x: Rx✝¹: ea + eb = ex✝: a₂ * b₂ = cx ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * csimp [pow_add: ∀ {M : Type ?u.130172} [inst : Monoid M] (a : M) (m n : ℕ), a ^ (m + n) = a ^ m * a ^ npow_add, mul_mul_mul_comm: ∀ {G : Type ?u.130196} [inst : CommSemigroup G] (a b c d : G), a * b * (c * d) = a * c * (b * d)mul_mul_mul_comm]Goals accomplished! 🐙

/-- Multiplies two monomials `va, vb` together to get a normalized result monomial.

* `x * y = (x * y)` (for `x`, `y` coefficients)
* `x * (b₁ * b₂) = b₁ * (b₂ * x)` (for `x` coefficient)
* `(a₁ * a₂) * y = a₁ * (a₂ * y)` (for `y` coefficient)
* `(x ^ ea * a₂) * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂)`
(if `ea` and `eb` are identical except coefficient)
* `(a₁ * a₂) * (b₁ * b₂) = a₁ * (a₂ * (b₁ * b₂))` (if `a₁.lt b₁`)
* `(a₁ * a₂) * (b₁ * b₂) = b₁ * ((a₁ * a₂) * b₂)` (if not `a₁.lt b₁`)
-/
partial def evalMulProd: {u : Lean.Level} →
{α : Q(Type u)} →
(sα : Q(CommSemiring «\$α»)) → {a b : Q(«\$α»)} → ExProd sα a → ExProd sα b → Result (ExProd sα) q(«\$a» * «\$b»)evalMulProd (va: ExProd sα ava : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα a: ?m.130715a) (vb: ExProd sα bvb : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα b: ?m.130725b) : Result: {u : Lean.Level} → {α : Q(Type u)} → (Q(«\$α») → Type) → Q(«\$α») → TypeResult (ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα) q(\$a: «\$α»aa * \$b: ?m.130671 * \$b: «\$α»b) :=
match va: ExProd sα ava, vb: ExProd sα bvb with
| .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const za: ℚza ha: Option Exprha, .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const zb: ℚzb hb: Option Exprhb =>
if za: ℚza = 1: ?m.1359621 then
⟨b: Q(«\$α»)b, .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const zb: ℚzb hb: Option Exprhb, (q(one_mul: ∀ {R : Type ?u.136048} [inst : CommSemiring R] (a : R), Nat.rawCast 1 * a = aone_mulone_mul \$b: ?m.130671 \$b: «\$α»b) : Expr: TypeExpr)⟩
else if zb: ℚzb = 1: ?m.1360651 then
⟨a: Q(«\$α»)a, .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const za: ℚza ha: Option Exprha, (q(mul_one: ∀ {R : Type ?u.136113} [inst : CommSemiring R] (a : R), a * Nat.rawCast 1 = amul_onemul_one \$a: ?m.130671 \$a: «\$α»a) : Expr: TypeExpr)⟩
else
let ra: ?m.136117ra := Result.ofRawRat: {u : Lean.Level} → {α : Q(Type u)} → ℚ → (e : Q(«\$α»)) → optParam (Option Expr) none → NormNum.Result eResult.ofRawRat za: ℚza a: Q(«\$α»)a ha: Option Exprha; let rb: ?m.136127rb := Result.ofRawRat: {u : Lean.Level} → {α : Q(Type u)} → ℚ → (e : Q(«\$α»)) → optParam (Option Expr) none → NormNum.Result eResult.ofRawRat zb: ℚzb b: Q(«\$α»)b hb: Option Exprhb
let rc: ?m.136132rc := (NormNum.evalMul.core: {u : Lean.Level} →
{α : Q(Type u)} →
(e : Q(«\$α»)) →
Q(«\$α» → «\$α» → «\$α») →
(a b : Q(«\$α»)) → Q(Semiring «\$α») → NormNum.Result a → NormNum.Result b → Option (NormNum.Result e)NormNum.evalMul.core q(\$a: «\$α»aa * \$b: ?m.130671 * \$b: «\$α»b) q(HMul.hMul: ?m.130671HMul.hMul) _: Q(«\$α»)_ _: Q(«\$α»)_
q(CommSemiring.toSemiring: ?m.130671CommSemiring.toSemiring) ra: ?m.136117ra rb: ?m.136127rb).get!: {α : Type ?u.136140} → [inst : Inhabited α] → Option α → αget!
let ⟨zc: ℚzc, hc: Option Exprhc⟩ := rc: ?m.136132rc.toRatNZ: {a : Lean.Level} → {α : Q(Type a)} → {e : Q(«\$α»)} → NormNum.Result e → Option (ℚ × Option Expr)toRatNZ.get!: {α : Type ?u.136163} → [inst : Inhabited α] → Option α → αget!
let ⟨c: Q(«\$α»)c, pc: Q(«\$a» * «\$b» = «\$c»)pc⟩ :=  rc: ?m.136132rc.toRawEq: {u : Lean.Level} → {α : Q(Type u)} → {e : Q(«\$α»)} → NormNum.Result e → (e' : Q(«\$α»)) × Q(«\$e» = «\$e'»)toRawEq
⟨c: Q(«\$α»)c, .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const zc: ℚzc hc: Option Exprhc, pc: Q(«\$a» * «\$b» = «\$c»)pc⟩
| .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul (x := a₁: Q(«\$α»)a₁) (e := a₂: Q(ℕ)a₂) va₁: ExBase sα a₁va₁ va₂: ExProd sℕ a₂va₂ va₃: ExProd sα b✝va₃, .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const _ _ =>
let ⟨_, vc: ExProd sα expr✝vc, pc: Q(\$b✝ * \$b✝¹ = \$expr✝)pc⟩ := evalMulProd: {a b : Q(«\$α»)} → ExProd sα a → ExProd sα b → Result (ExProd sα) q(«\$a» * «\$b»)evalMulProd va₃: ExProd sα b✝va₃ vb: ExProd sα b✝¹vb
⟨_: Q(«\$α»)_, .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul va₁: ExBase sα a₁va₁ va₂: ExProd sℕ a₂va₂ vc: ExProd sα expr✝vc, (q(mul_pf_left: ∀ {R : Type ?u.137086} [inst : CommSemiring R] {a₃ b c : R} (a₁ : R) (a₂ : ℕ),
a₃ * b = c → a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * cmul_pf_leftmul_pf_left \$a₁ \$a₂ \$pc: ?m.130671 \$a₁: «\$α»a₁mul_pf_left \$a₁ \$a₂ \$pc: ?m.130671 \$a₂: ℕa₂mul_pf_left \$a₁ \$a₂ \$pc: ?m.130671 \$pc: \$b✝ * \$b✝¹ = \$expr✝pc) : Expr: TypeExpr)⟩
| .const: {u : Lean.Level} →
{α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e.const _ _, .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul (x := b₁: Q(«\$α»)b₁) (e := b₂: Q(ℕ)b₂) vb₁: ExBase sα b₁vb₁ vb₂: ExProd sℕ b₂vb₂ vb₃: ExProd sα b✝vb₃ =>
let ⟨_, vc: ExProd sα expr✝vc, pc: Q(\$a✝ * \$b✝ = \$expr✝)pc⟩ := evalMulProd: {a b : Q(«\$α»)} → ExProd sα a → ExProd sα b → Result (ExProd sα) q(«\$a» * «\$b»)evalMulProd va: ExProd sα a✝va vb₃: ExProd sα b✝vb₃
⟨_: Q(«\$α»)_, .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul vb₁: ExBase sα b₁vb₁ vb₂: ExProd sℕ b₂vb₂ vc: ExProd sα expr✝vc, (q(mul_pf_right: ∀ {R : Type ?u.137395} [inst : CommSemiring R] {a b₃ c : R} (b₁ : R) (b₂ : ℕ),
a * b₃ = c → a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * cmul_pf_rightmul_pf_right \$b₁ \$b₂ \$pc: ?m.130671 \$b₁: «\$α»b₁mul_pf_right \$b₁ \$b₂ \$pc: ?m.130671 \$b₂: ℕb₂mul_pf_right \$b₁ \$b₂ \$pc: ?m.130671 \$pc: \$a✝ * \$b✝ = \$expr✝pc) : Expr: TypeExpr)⟩
| .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul (x := xa: Q(«\$α»)xa) (e := ea: Q(ℕ)ea) vxa: ExBase sα xavxa vea: ExProd sℕ eavea va₂: ExProd sα b✝¹va₂, .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul (x := xb: Q(«\$α»)xb) (e := eb: Q(ℕ)eb) vxb: ExBase sα xbvxb veb: ExProd sℕ ebveb vb₂: ExProd sα b✝vb₂ => Id.run: {α : Type ?u.137628} → Id α → αId.run do
if vxa: ExBase sα xavxa.eq: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExBase sα a_1 → ExBase sα b → Booleq vxb: ExBase sα xbvxb then
if let some: {α : Type ?u.137648} → α → Option αsome (.nonzero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → Result (ExProd sα) e → Overlap sα e.nonzero ⟨_, ve: ExProd sℕ expr✝ve, pe: Q(«\$ea» + «\$eb» = \$expr✝)pe⟩) := evalAddOverlap: {u : Lean.Level} →
{α : Q(Type u)} →
(sα : Q(CommSemiring «\$α»)) → {a b : Q(«\$α»)} → ExProd sα a → ExProd sα b → Option (Overlap sα q(«\$a» + «\$b»))evalAddOverlap sℕ: Q(CommSemiring ℕ)sℕ vea: ExProd sℕ eavea veb: ExProd sℕ ebveb then
let ⟨_, vc: ExProd sα expr✝vc, pc: Q(\$b✝¹ * \$b✝ = \$expr✝)pc⟩ := evalMulProd: {a b : Q(«\$α»)} → ExProd sα a → ExProd sα b → Result (ExProd sα) q(«\$a» * «\$b»)evalMulProd va₂: ExProd sα b✝¹va₂ vb₂: ExProd sα b✝vb₂
return ⟨_: Q(«\$α»)_, .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul vxa: ExBase sα xavxa ve: ExProd sℕ expr✝¹ve vc: ExProd sα expr✝vc, (q(mul_pp_pf_overlap: ∀ {R : Type ?u.137936} [inst : CommSemiring R] {ea eb e : ℕ} {a₂ b₂ c : R} (x : R),
ea + eb = e → a₂ * b₂ = c → x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * cmul_pp_pf_overlapmul_pp_pf_overlap \$xa \$pe \$pc: ?m.130671 \$xa: «\$α»xamul_pp_pf_overlap \$xa \$pe \$pc: ?m.130671 \$pe: «\$ea» + «\$eb» = \$expr✝¹pemul_pp_pf_overlap \$xa \$pe \$pc: ?m.130671 \$pc: \$b✝¹ * \$b✝ = \$expr✝pc) : Expr: TypeExpr)⟩
if let .lt: Ordering.lt := (vxa: ExBase sα xavxa.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExBase sα a_1 → ExBase sα b → Orderingcmp vxb: ExBase sα xbvxb).then: Ordering → Ordering → Orderingthen (vea: ExProd sℕ eavea.cmp: {a : Lean.Level} →
{arg : Q(Type a)} → {sα : Q(CommSemiring «\$arg»)} → {a_1 b : Q(«\$arg»)} → ExProd sα a_1 → ExProd sα b → Orderingcmp veb: ExProd sℕ ebveb) then
let ⟨_, vc: ExProd sα expr✝vc, pc: Q(\$b✝¹ * «\$b» = \$expr✝)pc⟩ := evalMulProd: {a b : Q(«\$α»)} → ExProd sα a → ExProd sα b → Result (ExProd sα) q(«\$a» * «\$b»)evalMulProd va₂: ExProd sα b✝¹va₂ vb: ExProd sα bvb
⟨_: Q(«\$α»)_, .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul vxa: ExBase sα xavxa vea: ExProd sℕ eavea vc: ExProd sα expr✝vc, (q(mul_pf_left: ∀ {R : Type ?u.138536} [inst : CommSemiring R] {a₃ b c : R} (a₁ : R) (a₂ : ℕ),
a₃ * b = c → a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * cmul_pf_leftmul_pf_left \$xa \$ea \$pc: ?m.130671 \$xa: «\$α»xamul_pf_left \$xa \$ea \$pc: ?m.130671 \$ea: ℕeamul_pf_left \$xa \$ea \$pc: ?m.130671 \$pc: \$b✝¹ * «\$b» = \$expr✝pc) : Expr: TypeExpr)⟩
else
let ⟨_, vc: ExProd sα expr✝vc, pc: Q(«\$a» * \$b✝ = \$expr✝)pc⟩ := evalMulProd: {a b : Q(«\$α»)} → ExProd sα a → ExProd sα b → Result (ExProd sα) q(«\$a» * «\$b»)evalMulProd va: ExProd sα ava vb₂: ExProd sα b✝vb₂
⟨_: Q(«\$α»)_, .mul: {u : Lean.Level} →
{α : Q(Type u)} →
{sα : Q(CommSemiring «\$α»)} →
{x : Q(«\$α»)} →
{e : Q(ℕ)} → {b : Q(«\$α»)} → ExBase sα x → ExProd sℕ e → ExProd sα b → ExProd sα q(«\$x» ^ «\$e» * «\$b»).mul vxb: ExBase sα xbvxb veb: ExProd sℕ ebveb vc: ExProd sα expr✝vc, (q(mul_pf_right: ∀ {R : Type ?u.138697} [inst : CommSemiring R] {a b₃ c : R} (b₁ : R) (b₂ : ℕ),
a * b₃ = c → a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * cmul_pf_rightmul_pf_right \$xb \$eb \$pc: ?m.130671 \$xb: «\$α»xbmul_pf_right \$xb \$eb \$pc: ?m.130671 \$eb: ℕebmul_pf_right \$xb \$eb \$pc: ?m.130671 \$pc: «\$a» * \$b✝ = \$expr✝pc) : Expr: TypeExpr)⟩

theorem mul_zero: ∀ (a : R), a * 0 = 0mul_zero (a: Ra : R: ?m.148391R) : a: Ra * 0: ?m.1484150 = 0: ?m.1484310 := byGoals accomplished! 🐙 u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra: Ra * 0 = 0simpGoals accomplished! 🐙

theorem mul_add: ∀ {a b₁ c₁ b₂ c₂ d : R}, a * b₁ = c₁ → a * b₂ = c₂ → c₁ + 0 + c₂ = d → a * (b₁ + b₂) = dmul_add (_: a * b₁ = c₁_ : (a: ?m.149410a : R: ?m.149387R) * b₁: ?m.149419b₁ = c₁: ?m.149428c₁) (_: a * b₂ = c₂_ : a: ?m.149410a * b₂: ?m.149873b₂ = c₂: ?m.150079c₂) (_: c₁ + 0 + c₂ = d_ : c₁: ?m.149428c₁ + 0: ?m.1509070 + c₂: ?m.150079c₂ = d: ?m.150501d) :
a: ?m.149410a * (b₁: ?m.149419b₁ + b₂: ?m.149873b₂) = d: ?m.150501d := byGoals accomplished! 🐙 u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₁, c₁, b₂, c₂, d: Rx✝²: a * b₁ = c₁x✝¹: a * b₂ = c₂x✝: c₁ + 0 + c₂ = da * (b₁ + b₂) = dsubst_varsu: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₁, b₂: Ra * (b₁ + b₂) = a * b₁ + 0 + a * b₂;u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₁, b₂: Ra * (b₁ + b₂) = a * b₁ + 0 + a * b₂ u: Lean.LevelR: Type u_1α: Q(Type u)sα: Q(CommSemiring «\$α»)inst✝: CommSemiring Ra, b₁, c₁, b₂, c₂, d: Rx✝²: a * b₁ = c₁x✝¹: a * b₂ = c₂x✝: c₁ + 0 + c₂ = da * (b₁ + b₂) = dsimp [_root_.mul_add: ∀ {R : Type ?u.152082} [inst : Mul R] [inst_1 : Add R] [inst_2 : LeftDistribClass R] (a b c : R),
a * (b + c) = a * b + a * c_root_.mul_add]Goals accomplished! 🐙

/-- Multiplies a monomial `va` to a polynomial `vb` to get a normalized result polynomial.

* `a * 0 = 0`
* `a * (b₁ + b₂) = (a * b₁) + (a * b₂)`
-/
def evalMul₁: {a b : Q(«\$α»)} → ExProd sα a → ExSum sα b → Result (ExSum sα) q(«\$a» * «\$b»)evalMul₁ (va: ExProd sα ava : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExProd sα: Q(CommSemiring «\$α»)sα a: ?m.153076a) (vb: ExSum sα bvb : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: Q(CommSemiring «\$α»)sα b: ?m.153086b) : Result: {u : Lean.Level} → {α : Q(Type u)} → (Q(«\$α») → Type) → Q(«\$α») → TypeResult (ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «\$α») → Q(«\$α») → TypeExSum sα: Q(CommSemiring «\$α»)sα) q(\$a: «\$α»aa * \$b: ?m.153032 * \$b: «\$α»b) :=
match vb: ExSum sα bvb with
| .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «\$α»)} → ExSum sα q(0).zero => ⟨_: Q(«\$α»)_, .zero: ```