/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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)
- addition of expressions
- 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.2
CommSemiring ℕ: 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.63
CommSemiring ℕ: 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(«$α») → Type
ExBase : ∀ {α: Q(Type u)
α : Q(Type u: Type (u+1)
Type u)}, Q(CommSemiring: Type ?u.112 → Type ?u.112
CommSemiringCommSemiring $α: ?m.99
 $α: Type u
α) → (e: Q(«$α»)
e : Q($α: Type u
α)) → Type: Type 1
Type
  /--
  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α e
atom (id: ℕ
id : ℕ: Type
ℕ) : ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExBase sα: ?m.203
sα e: ?m.214
e
  /-- A sum of monomials.  -/
  | sum: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → ExSum sα e → ExBase sα e
sum (_: ExSum sα e
_ : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: ?m.232
sα e: ?m.240
e) : ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExBase sα: ?m.232
sα e: ?m.240
e

/--
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(«$α») → Type
ExProd : ∀ {α: Q(Type u)
α : Q(Type u: ?m.126
Type u)}, Q(CommSemiring: Type ?u.139 → Type ?u.139
CommSemiringCommSemiring $α: ?m.126
 $α: Type u
α) → (e: Q(«$α»)
e : Q($α: Type u
α)) → Type: Type 1
Type
  /-- 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α e
const (value: ℚ
value : ℚ: Type
ℚ) (hyp: optParam (Option Expr) none
hyp : Option: Type ?u.286 → Type ?u.286
Option Expr: Type
Expr := none: {α : Type ?u.303} → Option α
none) : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: ?m.280
sα e: ?m.296
e
  /-- 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.335
Type u)} {sα: Q(CommSemiring «$α»)
sα : Q(CommSemiring: Type ?u.346 → Type ?u.346
CommSemiringCommSemiring $α: ?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(«$α») → Type
ExBase sα: Q(CommSemiring «$α»)
sα x: Q(«$α»)
x → ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sℕ: Q(CommSemiring ℕ)
sℕ e: Q(ℕ)
e → ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: Q(CommSemiring «$α»)
sα b: Q(«$α»)
b → ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd 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(«$α») → Type
ExSum : ∀ {α: Q(Type u)
α : Q(Type u: ?m.153
Type u)}, Q(CommSemiring: Type ?u.166 → Type ?u.166
CommSemiringCommSemiring $α: ?m.153
 $α: Type u
α) → (e: Q(«$α»)
e : Q($α: Type u
α)) → Type: Type 1
Type
  /-- 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.1162
Type u)} {sα: Q(CommSemiring «$α»)
sα : Q(CommSemiring: Type ?u.1173 → Type ?u.1173
CommSemiringCommSemiring $α: ?m.1162
 $α: Type u
α)} : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: Q(CommSemiring «$α»)
sα q(0: ?m.1182
0 : $α: 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.1373
CommSemiringCommSemiring $α: ?m.1362
 $α: Type u
α)} {a: Q(«$α»)
a b: Q(«$α»)
b : Q($α: Type u
α)} :
    ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: Q(CommSemiring «$α»)
sα a: Q(«$α»)
a → ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: Q(CommSemiring «$α»)
sα b: Q(«$α»)
b → ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum 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 → Bool
ExBase.eq : ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExBase sα: ?m.4842
sα a: ?m.4852
a → ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExBase sα: ?m.4842
sα b: ?m.4872
b → Bool: Type
Bool
  | .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 → Bool
eq b: ExSum sα b✝
b
  | _, _ => false: Bool
false

@[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 → Bool
ExBase.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 → Bool
ExProd.eq : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: ?m.4895
sα a: ?m.4905
a → ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: ?m.4895
sα b: ?m.4925
b → Bool: Type
Bool
  | .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 → Bool
eq 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 → Bool
eq 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 → Bool
eq b₃: ExProd sα b✝
b₃
  | _, _ => false: Bool
false

@[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 → Bool
ExBase.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 → Bool
ExSum.eq : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: ?m.4948
sα a: ?m.4958
a → ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: ?m.4948
sα b: ?m.4978
b → Bool: Type
Bool
  | .zero: ExSum sα q(0)
.zero, .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → ExSum sα q(0)
.zero => true: Bool
true
  | .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 → Bool
eq 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 → Bool
eq b₂: ExSum sα b✝
b₂
  | _, _ => false: Bool
false
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 → Ordering
ExBase.cmp : ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExBase sα: ?m.30955
sα a: ?m.30965
a → ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExBase sα: ?m.30955
sα b: ?m.30985
b → Ordering: Type
Ordering
  | .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 α] → α → α → Ordering
compare 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 → Ordering
cmp 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 → Ordering
ExBase.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 → Ordering
ExProd.cmp : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: ?m.31008
sα a: ?m.31018
a → ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: ?m.31008
sα b: ?m.31038
b → Ordering: Type
Ordering
  | .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 α] → α → α → Ordering
compare 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 → Ordering
cmp b₁: ExBase sα x✝
b₁).then: Ordering → Ordering → Ordering
then (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 → Ordering
cmp b₂: ExProd sℕ e✝
b₂) |>.then: Ordering → Ordering → Ordering
then (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 → Ordering
cmp 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 → Ordering
ExBase.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 → Ordering
ExSum.cmp : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: ?m.31061
sα a: ?m.31071
a → ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: ?m.31061
sα b: ?m.31091
b → Ordering: Type
Ordering
  | .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 → Ordering
cmp b₁: ExProd sα a✝
b₁).then: Ordering → Ordering → Ordering
then (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 → Ordering
cmp 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.50699
e, (ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExBase sα: ?m.50691
sα) e: ?m.50699
e) := ⟨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.50898
0⟩
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.51030
e, (ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: ?m.51022
sα) e: ?m.51030
e) := ⟨_: ?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.51205
e, (ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: ?m.51197
sα) e: ?m.51205
e) := ⟨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.51404
0 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β a
ExBase.cast : ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExBase sα: ?m.51560
sα a: ?m.51570
a → Σ a: ?m.51601
a, ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExBase sβ: ?m.51588
sβ a: ?m.51601
a
  | .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β a
cast; ⟨_: ?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β a
ExProd.cast : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: ?m.51622
sα a: ?m.51632
a → Σ a: ?m.51663
a, ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sβ: ?m.51650
sβ a: ?m.51663
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 Expr
h => ⟨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 Expr
h⟩
  | .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β a
cast.2: {α : Type ?u.54056} → {β : α → Type ?u.54055} → (self : Sigma β) → β self.fst
2 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β a
cast.2: {α : Type ?u.54069} → {β : α → Type ?u.54068} → (self : Sigma β) → β self.fst
2⟩

/-- 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β a
ExSum.cast : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: ?m.51684
sα a: ?m.51694
a → Σ a: ?m.51725
a, ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sβ: ?m.51712
sβ a: ?m.51725
a
  | .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β a
cast.2: {α : Type ?u.56159} → {β : α → Type ?u.56158} → (self : Sigma β) → β self.fst
2 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β a
cast.2: {α : Type ?u.56172} → {β : α → Type ?u.56171} → (self : Sigma β) → β self.fst
2⟩

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(«$α») → Type
Result {α: Q(Type u)
α : Q(Type u: ?m.59383
Type u)} (E: Q(«$α») → Type
E : Q($α: Type u
α) → Type: Type 1
Type) (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.expr
val : E: Q(«$α») → Type
E 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.60095
E e: ?m.60127
e)] : Inhabited: Sort ?u.60134 → Sort (max1?u.60134)
Inhabited (Result: {u : Lean.Level} → {α : Q(Type u)} → (Q(«$α») → Type) → Q(«$α») → Type
Result E: ?m.60095
E e: ?m.60119
e) :=
  let ⟨e': Q($α✝)
e', v: E e'
v⟩ : Σ e: ?m.60157
e, E: Q($α✝) → Type
E e: ?m.60157
e := 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.242276
CommSemiringCommSemiring $α: ?m.242265
 $α: Type u
α)) [CommSemiring: Type ?u.230043 → Type ?u.230043
CommSemiring R: ?m.340925
R]

/--
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α e
ExProd.mkNat (n: ℕ
n : ℕ: Type
ℕ) : (e: Q(«$α»)
e : Q($α: Type u
α)) × ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: Q(CommSemiring «$α»)
sα e: Q(«$α»)
e :=
  let lit: Q(ℕ)
lit : Q(ℕ: Type
ℕ) := mkRawNatLit: ℕ → Expr
mkRawNatLit 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α e
ExProd.mkNegNat (_: Q(Ring «$α»)
_ : Q(Ring: Type ?u.61327 → Type ?u.61327
RingRing $α: ?m.61290
 $α: Type u
α)) (n: ℕ
n : ℕ: Type
ℕ) : (e: Q(«$α»)
e : Q($α: Type u
α)) × ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: Q(CommSemiring «$α»)
sα e: Q(«$α»)
e :=
  let lit: Q(ℕ)
lit : Q(ℕ: Type
ℕ) := mkRawNatLit: ℕ → Expr
mkRawNatLit 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α e
ExProd.mkRat (_: Q(DivisionRing «$α»)
_ : Q(DivisionRing: Type ?u.61662 → Type ?u.61662
DivisionRingDivisionRing $α: ?m.61625
 $α: Type u
α)) (q: ℚ
q : ℚ: Type
ℚ) (n: Q(ℤ)
n : Q(ℤ: Type
ℤ)) (d: Q(ℕ)
d : Q(ℕ: Type
ℕ)) (h: Expr
h : Expr: Type
Expr) :
    (e: Q(«$α»)
e : Q($α: Type u
α)) × ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd 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: Expr
h⟩

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

/-- 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α a
va : ExBase: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExBase sα: Q(CommSemiring «$α»)
sα a: ?m.62028
a) (vb: ExProd sℕ b
vb : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sℕ: Q(CommSemiring ℕ)
sℕ b: ?m.62038
b) :
  ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd 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α a
va vb: ExProd sℕ b
vb (.const: {u : Lean.Level} →
  {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e
.const 1: ?m.63037
1 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α e
v : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: Q(CommSemiring «$α»)
sα e: ?m.63212
e) : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: Q(CommSemiring «$α»)
sα q($e: «$α»
ee + 0: ?m.63168
 + 0: ?m.63229
0) := .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α e
v .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(«$α») → Type
ExProd sα: Q(CommSemiring «$α»)
sα e: ?m.63982
e → ℚ: 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(«$α») → Type
Overlap (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α e
zero (_: Q(IsNat «$e» 0)
_ : Q(IsNat: {α : Type ?u.68605} → [inst : AddMonoidWithOne α] → α → ℕ → Prop
IsNatIsNat $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
  (with nonzero leading coefficient). -/
  | nonzero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → Result (ExProd sα) e → Overlap sα e
nonzero (_: Result (ExProd sα) e
_ : Result: {u : Lean.Level} → {α : Q(Type u)} → (Q(«$α») → Type) → Q(«$α») → Type
Result (ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd 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 * c
add_overlap_pf (x: R
x : R: ?m.69571
R) (e: unknown metavariable '?_uniq.69616'
e) (pq_pf: a + b = c
pq_pf : a: ?m.69598
a + b: ?m.69611
b = c: ?m.69624
c) :
    x: R
x ^ e: ?m.69629
e * a: ?m.69598
a + x: R
x ^ e: ?m.69629
e * b: ?m.69611
b = x: R
x ^ e: ?m.69629
e * c: ?m.69624
c := by
Goals accomplished! 🐙 u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b, c, x: R

e: ℕ

pq_pf: a + b = c

x ^ e * a + x ^ e * b = x ^ e * csubst_varsu: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b, x: R

e: ℕ

x ^ e * a + x ^ e * b = x ^ e * (a + b);u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b, x: R

e: ℕ

x ^ e * a + x ^ e * b = x ^ e * (a + b) u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b, c, x: R

e: ℕ

pq_pf: a + b = c

x ^ 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 * c
mul_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) 0
add_overlap_pf_zero (x: R
x : R: ?m.72347
R) (e: unknown metavariable '?_uniq.72394'
e) :
    IsNat: {α : Type ?u.72426} → [inst : AddMonoidWithOne α] → α → ℕ → Prop
IsNat (a: ?m.72389
a + b: ?m.72417
b) (nat_lit 0: ℕ
nat_litnat_lit 0: ℕ
 0) → IsNat: {α : Type ?u.72479} → [inst : AddMonoidWithOne α] → α → ℕ → Prop
IsNat (x: R
x ^ e: ?m.72422
e * a: ?m.72389
a + x: R
x ^ e: ?m.72422
e * b: ?m.72417
b) (nat_lit 0: ℕ
nat_litnat_lit 0: ℕ
 0)
  | ⟨h: a + b = ↑0
h⟩ => ⟨by
Goals accomplished! 🐙 u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b, x: R

e: ℕ

h: a + b = ↑0

x ^ e * a + x ^ e * b = ↑0simp [h: a + b = ↑0
h, ← 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 * c
mul_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α a
va : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: Q(CommSemiring «$α»)
sα a: ?m.76183
a) (vb: ExProd sα b
vb : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: Q(CommSemiring «$α»)
sα b: ?m.76193
b) : Option: Type ?u.76204 → Type ?u.76204
Option (Overlap: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
Overlap sα: Q(CommSemiring «$α»)
sα q($a: «$α»
aa + $b: ?m.76139
 + $b: «$α»
b)) :=
  match va: ExProd sα a
va, vb: ExProd sα b
vb 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 Expr
ha, .const: {u : Lean.Level} →
  {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e
.const zb: ℚ
zb hb: Option Expr
hb => do
    let ra: ?m.82497
ra := Result.ofRawRat: {u : Lean.Level} → {α : Q(Type u)} → ℚ → (e : Q(«$α»)) → optParam (Option Expr) none → NormNum.Result e
Result.ofRawRat za: ℚ
za a: Q(«$α»)
a ha: Option Expr
ha; let rb: ?m.82507
rb := Result.ofRawRat: {u : Lean.Level} → {α : Q(Type u)} → ℚ → (e : Q(«$α»)) → optParam (Option Expr) none → NormNum.Result e
Result.ofRawRat zb: ℚ
zb b: Q(«$α»)
b hb: Option Expr
hb
    let res: ?m.82561
res ← 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.76139
Add.add) _: Q(«$α»)
_ _: Q(«$α»)
_ ra: ?m.82497
ra rb: ?m.82507
rb
    match res: ?m.82561
res 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.82555
rc =>
      let ⟨zc: ℚ
zc, hc: Option Expr
hc⟩ ← rc: NormNum.Result ?m.82555
rc.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.82555
rc.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 Expr
hc, 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 Unit
guard (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 → Bool
eq 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 → Bool
eq 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) 0
add_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✝) 0
p) : Expr: Type
Expr)
    | .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 * c
add_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: Type
Expr)⟩
  | _, _ => none: {α : Type ?u.84840} → Option α
none

theorem add_pf_zero_add: ∀ (b : R), 0 + b = b
add_pf_zero_add (b: R
b : R: ?m.98733
R) : 0: ?m.98757
0 + b: R
b = b: R
b := by
Goals accomplished! 🐙 u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

b: R

0 + b = bsimp
Goals accomplished! 🐙

theorem add_pf_add_zero: ∀ {R : Type u_1} [inst : CommSemiring R] (a : R), a + 0 = a
add_pf_add_zero (a: R
a : R: ?m.99718
R) : a: R
a + 0: ?m.99742
0 = a: R
a := by
Goals accomplished! 🐙 u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a: R

a + 0 = asimp
Goals 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.100725
a₁ + b₁: ?m.100733
b₁ = c₁: ?m.100741
c₁) (_: a₂ + b₂ = c₂
_ : a₂: ?m.100773
a₂ + b₂: ?m.100805
b₂ = c₂: ?m.100837
c₂) : (a₁: ?m.100725
a₁ + a₂: ?m.100773
a₂ : R: ?m.100703
R) + (b₁: ?m.100733
b₁ + b₂: ?m.100805
b₂) = c₁: ?m.100741
c₁ + c₂: ?m.100837
c₂ := by
Goals accomplished! 🐙
  u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, c₁, a₂, b₂, c₂: R

x✝¹: a₁ + b₁ = c₁

x✝: a₂ + b₂ = c₂

a₁ + a₂ + (b₁ + b₂) = c₁ + c₂subst_varsu: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂: R

a₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂);u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂: R

a₁ + a₂ + (b₁ + b₂) = a₁ + b₁ + (a₂ + b₂) u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, c₁, a₂, b₂, c₂: R

x✝¹: 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₂) = c
add_pf_add_overlap_zero
    (h: IsNat (a₁ + b₁) 0
h : IsNat: {α : Type ?u.102948} → [inst : AddMonoidWithOne α] → α → ℕ → Prop
IsNat (a₁: ?m.102799
a₁ + b₁: ?m.102821
b₁) (nat_lit 0: ℕ
nat_litnat_lit 0: ℕ
 0)) (h₄: a₂ + b₂ = c
h₄ : a₂: ?m.102883
a₂ + b₂: ?m.102945
b₂ = c: ?m.103007
c) : (a₁: ?m.102799
a₁ + a₂: ?m.102883
a₂ : R: ?m.102763
R) + (b₁: ?m.102821
b₁ + b₂: ?m.102945
b₂) = c: ?m.103007
c := by
Goals accomplished! 🐙
  u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂, c: R

h: IsNat (a₁ + b₁) 0

h₄: a₂ + b₂ = c

a₁ + a₂ + (b₁ + b₂) = csubst_varsu: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂: R

h: IsNat (a₁ + b₁) 0

a₁ + a₂ + (b₁ + b₂) = a₂ + b₂;u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂: R

h: IsNat (a₁ + b₁) 0

a₁ + a₂ + (b₁ + b₂) = a₂ + b₂ u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂, c: R

h: IsNat (a₁ + b₁) 0

h₄: a₂ + b₂ = c

a₁ + a₂ + (b₁ + b₂) = crw [u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂: R

h: IsNat (a₁ + b₁) 0

a₁ + a₂ + (b₁ + b₂) = a₂ + b₂add_add_add_comm: ∀ {G : Type ?u.104256} [inst : AddCommSemigroup G] (a b c d : G), a + b + (c + d) = a + c + (b + d)
add_add_add_comm,u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂: R

h: IsNat (a₁ + b₁) 0

a₁ + b₁ + (a₂ + b₂) = a₂ + b₂ u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂: R

h: IsNat (a₁ + b₁) 0

a₁ + a₂ + (b₁ + b₂) = a₂ + b₂h: IsNat (a₁ + b₁) 0
h.1: ∀ {α : Type ?u.104610} [inst : AddMonoidWithOne α] {a : α} {n : ℕ}, IsNat a n → a = ↑n
1,u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂: R

h: IsNat (a₁ + b₁) 0

↑0 + (a₂ + b₂) = a₂ + b₂ u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂: R

h: IsNat (a₁ + b₁) 0

a₁ + a₂ + (b₁ + b₂) = a₂ + b₂Nat.cast_zero: ∀ {R : Type ?u.104790} [inst : AddMonoidWithOne R], ↑0 = 0
Nat.cast_zero,u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂: R

h: IsNat (a₁ + b₁) 0

0 + (a₂ + b₂) = a₂ + b₂ u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂: R

h: IsNat (a₁ + b₁) 0

a₁ + a₂ + (b₁ + b₂) = a₂ + b₂add_pf_zero_add: ∀ {R : Type ?u.104822} [inst : CommSemiring R] (b : R), 0 + b = b
add_pf_zero_addu: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₁, b₁, a₂, b₂: R

h: IsNat (a₁ + b₁) 0

a₂ + b₂ = a₂ + b₂]
Goals accomplished! 🐙

theorem add_pf_add_lt: ∀ {a₂ b c : R} (a₁ : R), a₂ + b = c → a₁ + a₂ + b = a₁ + c
add_pf_add_lt (a₁: R
a₁ : R: ?m.104921
R) (_: a₂ + b = c
_ : a₂: ?m.104945
a₂ + b: ?m.104955
b = c: ?m.104965
c) : (a₁: R
a₁ + a₂: ?m.104945
a₂) + b: ?m.104955
b = a₁: R
a₁ + c: ?m.104965
c := by
Goals accomplished! 🐙 u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₂, b, c, a₁: R

x✝: a₂ + b = c

a₁ + 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₁ + c
add_pf_add_gt (b₁: R
b₁ : R: ?m.106195
R) (_: a + b₂ = c
_ : a: ?m.106219
a + b₂: ?m.106229
b₂ = c: ?m.106239
c) : a: ?m.106219
a + (b₁: R
b₁ + b₂: ?m.106229
b₂) = b₁: R
b₁ + c: ?m.106239
c := by
Goals accomplished! 🐙
  u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₂, c, b₁: R

x✝: a + b₂ = c

a + (b₁ + b₂) = b₁ + csubst_varsu: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₂, b₁: R

a + (b₁ + b₂) = b₁ + (a + b₂);u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₂, b₁: R

a + (b₁ + b₂) = b₁ + (a + b₂) u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₂, c, b₁: R

x✝: a + b₂ = c

a + (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α a
va : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: Q(CommSemiring «$α»)
sα a: ?m.107600
a) (vb: ExSum sα b
vb : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: Q(CommSemiring «$α»)
sα b: ?m.107610
b) : Result: {u : Lean.Level} → {α : Q(Type u)} → (Q(«$α») → Type) → Q(«$α») → Type
Result (ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: Q(CommSemiring «$α»)
sα) q($a: «$α»
aa + $b: ?m.107556
 + $b: «$α»
b) :=
  match va: ExSum sα a
va, vb: ExSum sα b
vb with
  | .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → ExSum sα q(0)
.zero, vb: ExSum sα b
vb => ⟨b: Q(«$α»)
b, vb: ExSum sα b
vb, q(add_pf_zero_add: ∀ {R : Type ?u.110724} [inst : CommSemiring R] (b : R), 0 + b = b
add_pf_zero_addadd_pf_zero_add $b: ?m.107556
 $b: «$α»
b)⟩
  | va: ExSum sα a
va, .zero: ExSum sα q(0)
.zero => ⟨a: Q(«$α»)
a, va: ExSum sα a
va, q(add_pf_add_zero: ∀ {R : Type ?u.110771} [inst : CommSemiring R] (a : R), a + 0 = a
add_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₂) = c
add_pf_add_overlap_zeroadd_pf_add_overlap_zero $pc₁ $pc₂: ?m.107556
 $pc₁: IsNat («$a₁» + «$b₁») 0
pc₁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 → Ordering
cmp vb₁: ExProd sα b₁
vb₁ then
        let ⟨_c: Q(«$α»)
_c, vc: ExSum sα _c
vc, (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α 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 va₁: ExProd sα a₁
va₁ vc: ExSum sα _c
vc, 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₁ + c
add_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α _c
vc, (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α 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 vb₁: ExProd sα b₁
vb₁ vc: ExSum sα _c
vc, 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₁ + c
add_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 = a
one_mul (a: R
a : R: ?m.122733
R) : (nat_lit 1: ℕ
nat_litnat_lit 1: ℕ
 1).rawCast: {α : Type ?u.122756} → [inst : AddMonoidWithOne α] → ℕ → α
rawCast * a: R
a = a: R
a := by
Goals accomplished! 🐙 u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a: R

Nat.rawCast 1 * a = asimp [Nat.rawCast: {α : Type ?u.123398} → [inst : AddMonoidWithOne α] → ℕ → α
Nat.rawCast]
Goals accomplished! 🐙

theorem mul_one: ∀ (a : R), a * Nat.rawCast 1 = a
mul_one (a: R
a : R: ?m.124033
R) : a: R
a * (nat_lit 1: ℕ
nat_litnat_lit 1: ℕ
 1).rawCast: {α : Type ?u.124056} → [inst : AddMonoidWithOne α] → ℕ → α
rawCast = a: R
a := by
Goals accomplished! 🐙 u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a: R

a * 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₂ * c
mul_pf_left (a₁: R
a₁ : R: ?m.125329
R) (a₂: unknown metavariable '?_uniq.125348'
a₂) (_: a₃ * b = c
_ : a₃: ?m.125356
a₃ * b: ?m.125369
b = c: ?m.125382
c) : (a₁: R
a₁ ^ a₂: ?m.125387
a₂ * a₃: ?m.125356
a₃ : R: ?m.125329
R) * b: ?m.125369
b = a₁: R
a₁ ^ a₂: ?m.125387
a₂ * c: ?m.125382
c := by
Goals accomplished! 🐙
  u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₃, b, c, a₁: R

a₂: ℕ

x✝: a₃ * b = c

a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * csubst_varsu: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₃, b, a₁: R

a₂: ℕ

a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b);u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₃, b, a₁: R

a₂: ℕ

a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * (a₃ * b) u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₃, b, c, a₁: R

a₂: ℕ

x✝: a₃ * b = c

a₁ ^ a₂ * a₃ * b = a₁ ^ a₂ * crw [u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₃, b, a₁: R

a₂: ℕ

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.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a₃, b, a₁: R

a₂: ℕ

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₂ * c
mul_pf_right (b₁: R
b₁ : R: ?m.126674
R) (b₂: ℕ
b₂) (_: a * b₃ = c
_ : a: ?m.126701
a * b₃: ?m.126714
b₃ = c: ?m.126727
c) : a: ?m.126701
a * (b₁: R
b₁ ^ b₂: ?m.126732
b₂ * b₃: ?m.126714
b₃) = b₁: R
b₁ ^ b₂: ?m.126732
b₂ * c: ?m.126727
c := by
Goals accomplished! 🐙
  u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₃, c, b₁: R

b₂: ℕ

x✝: a * b₃ = c

a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * csubst_varsu: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₃, b₁: R

b₂: ℕ

a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃);u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₃, b₁: R

b₂: ℕ

a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * (a * b₃) u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₃, c, b₁: R

b₂: ℕ

x✝: a * b₃ = c

a * (b₁ ^ b₂ * b₃) = b₁ ^ b₂ * crw [u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₃, b₁: R

b₂: ℕ

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.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₃, b₁: R

b₂: ℕ

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 * c
mul_pp_pf_overlap (x: R
x : R: ?m.128163
R) (_: ea + eb = e
_ : ea: ?m.128187
ea + eb: ?m.128197
eb = e: ?m.128207
e) (_: a₂ * b₂ = c
_ : a₂: ?m.128241
a₂ * b₂: ?m.128275
b₂ = c: ?m.128309
c) :
    (x: R
x ^ ea: ?m.128187
ea * a₂: ?m.128241
a₂ : R: ?m.128163
R) * (x: R
x ^ eb: ?m.128197
eb * b₂: ?m.128275
b₂) = x: R
x ^ e: ?m.128207
e * c: ?m.128309
c := by
Goals accomplished! 🐙
  u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

ea, eb, e: ℕ

a₂, b₂, c, x: R

x✝¹: ea + eb = e

x✝: a₂ * b₂ = c

x ^ ea * a₂ * (x ^ eb * b₂) = x ^ e * csubst_varsu: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

ea, eb: ℕ

a₂, b₂, x: R

x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂);u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

ea, eb: ℕ

a₂, b₂, x: R

x ^ ea * a₂ * (x ^ eb * b₂) = x ^ (ea + eb) * (a₂ * b₂) u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

ea, eb, e: ℕ

a₂, b₂, c, x: R

x✝¹: ea + eb = e

x✝: a₂ * b₂ = c

x ^ 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 ^ n
pow_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α a
va : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: Q(CommSemiring «$α»)
sα a: ?m.130715
a) (vb: ExProd sα b
vb : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: Q(CommSemiring «$α»)
sα b: ?m.130725
b) : Result: {u : Lean.Level} → {α : Q(Type u)} → (Q(«$α») → Type) → Q(«$α») → Type
Result (ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: Q(CommSemiring «$α»)
sα) q($a: «$α»
aa * $b: ?m.130671
 * $b: «$α»
b) :=
  match va: ExProd sα a
va, vb: ExProd sα b
vb 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 Expr
ha, .const: {u : Lean.Level} →
  {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → {e : Q(«$α»)} → ℚ → optParam (Option Expr) none → ExProd sα e
.const zb: ℚ
zb hb: Option Expr
hb =>
    if za: ℚ
za = 1: ?m.135962
1 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 Expr
hb, (q(one_mul: ∀ {R : Type ?u.136048} [inst : CommSemiring R] (a : R), Nat.rawCast 1 * a = a
one_mulone_mul $b: ?m.130671
 $b: «$α»
b) : Expr: Type
Expr)⟩
    else if zb: ℚ
zb = 1: ?m.136065
1 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 Expr
ha, (q(mul_one: ∀ {R : Type ?u.136113} [inst : CommSemiring R] (a : R), a * Nat.rawCast 1 = a
mul_onemul_one $a: ?m.130671
 $a: «$α»
a) : Expr: Type
Expr)⟩
    else
      let ra: ?m.136117
ra := Result.ofRawRat: {u : Lean.Level} → {α : Q(Type u)} → ℚ → (e : Q(«$α»)) → optParam (Option Expr) none → NormNum.Result e
Result.ofRawRat za: ℚ
za a: Q(«$α»)
a ha: Option Expr
ha; let rb: ?m.136127
rb := Result.ofRawRat: {u : Lean.Level} → {α : Q(Type u)} → ℚ → (e : Q(«$α»)) → optParam (Option Expr) none → NormNum.Result e
Result.ofRawRat zb: ℚ
zb b: Q(«$α»)
b hb: Option Expr
hb
      let rc: ?m.136132
rc := (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.130671
HMul.hMul) _: Q(«$α»)
_ _: Q(«$α»)
_
        q(CommSemiring.toSemiring: ?m.130671
CommSemiring.toSemiring) ra: ?m.136117
ra rb: ?m.136127
rb).get!: {α : Type ?u.136140} → [inst : Inhabited α] → Option α → α
get!
      let ⟨zc: ℚ
zc, hc: Option Expr
hc⟩ := rc: ?m.136132
rc.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.136132
rc.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 Expr
hc, 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₂ * c
mul_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: Type
Expr)⟩
  | .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₂ * c
mul_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: Type
Expr)⟩
  | .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α xa
vxa vea: ExProd sℕ ea
vea 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α xb
vxb veb: ExProd sℕ eb
veb vb₂: ExProd sα b✝
vb₂ => Id.run: {α : Type ?u.137628} → Id α → α
Id.run do
    if vxa: ExBase sα xa
vxa.eq: {a : Lean.Level} →
  {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → ExBase sα a_1 → ExBase sα b → Bool
eq vxb: ExBase sα xb
vxb 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ℕ ea
vea veb: ExProd sℕ eb
veb 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α xa
vxa 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 * c
mul_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: Type
Expr)⟩
    if let .lt: Ordering
.lt := (vxa: ExBase sα xa
vxa.cmp: {a : Lean.Level} →
  {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → ExBase sα a_1 → ExBase sα b → Ordering
cmp vxb: ExBase sα xb
vxb).then: Ordering → Ordering → Ordering
then (vea: ExProd sℕ ea
vea.cmp: {a : Lean.Level} →
  {arg : Q(Type a)} → {sα : Q(CommSemiring «$arg»)} → {a_1 b : Q(«$arg»)} → ExProd sα a_1 → ExProd sα b → Ordering
cmp veb: ExProd sℕ eb
veb) 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
      ⟨_: 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α xa
vxa vea: ExProd sℕ ea
vea 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₂ * c
mul_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: Type
Expr)⟩
    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α 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 vxb: ExBase sα xb
vxb veb: ExProd sℕ eb
veb 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₂ * c
mul_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: Type
Expr)⟩

theorem mul_zero: ∀ (a : R), a * 0 = 0
mul_zero (a: R
a : R: ?m.148391
R) : a: R
a * 0: ?m.148415
0 = 0: ?m.148431
0 := by
Goals accomplished! 🐙 u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a: R

a * 0 = 0simp
Goals accomplished! 🐙

theorem mul_add: ∀ {a b₁ c₁ b₂ c₂ d : R}, a * b₁ = c₁ → a * b₂ = c₂ → c₁ + 0 + c₂ = d → a * (b₁ + b₂) = d
mul_add (_: a * b₁ = c₁
_ : (a: ?m.149410
a : R: ?m.149387
R) * b₁: ?m.149419
b₁ = c₁: ?m.149428
c₁) (_: a * b₂ = c₂
_ : a: ?m.149410
a * b₂: ?m.149873
b₂ = c₂: ?m.150079
c₂) (_: c₁ + 0 + c₂ = d
_ : c₁: ?m.149428
c₁ + 0: ?m.150907
0 + c₂: ?m.150079
c₂ = d: ?m.150501
d) :
    a: ?m.149410
a * (b₁: ?m.149419
b₁ + b₂: ?m.149873
b₂) = d: ?m.150501
d := by
Goals accomplished! 🐙 u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₁, c₁, b₂, c₂, d: R

x✝²: a * b₁ = c₁

x✝¹: a * b₂ = c₂

x✝: c₁ + 0 + c₂ = d

a * (b₁ + b₂) = dsubst_varsu: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₁, b₂: R

a * (b₁ + b₂) = a * b₁ + 0 + a * b₂;u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₁, b₂: R

a * (b₁ + b₂) = a * b₁ + 0 + a * b₂ u: Lean.Level

R: Type u_1

α: Q(Type u)

sα: Q(CommSemiring «$α»)

inst✝: CommSemiring R

a, b₁, c₁, b₂, c₂, d: R

x✝²: a * b₁ = c₁

x✝¹: a * b₂ = c₂

x✝: c₁ + 0 + c₂ = d

a * (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α a
va : ExProd: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExProd sα: Q(CommSemiring «$α»)
sα a: ?m.153076
a) (vb: ExSum sα b
vb : ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: Q(CommSemiring «$α»)
sα b: ?m.153086
b) : Result: {u : Lean.Level} → {α : Q(Type u)} → (Q(«$α») → Type) → Q(«$α») → Type
Result (ExSum: {u : Lean.Level} → {α : Q(Type u)} → Q(CommSemiring «$α») → Q(«$α») → Type
ExSum sα: Q(CommSemiring «$α»)
sα) q($a: «$α»
aa * $b: ?m.153032
 * $b: «$α»
b) :=
  match vb: ExSum sα b
vb with
  | .zero: {u : Lean.Level} → {α : Q(Type u)} → {sα : Q(CommSemiring «$α»)} → ExSum sα q(0)
.zero => ⟨_: Q(«$α»)
_, .zero: