Lean4
/-- Given two terms `l₁`, `l₂` of type `qNF M`, i.e. lists of `(ℤ × Q($M)) × ℕ`s (an integer, an
`Expr` and a natural number), recursively construct a proof that in the field `$M`, the product of
the "multiplicative linear combinations" represented by `l₁` and `l₂` is the multiplicative linear
combination represented by `FieldSimp.qNF.mul l₁ l₁`. -/
def mkMulProof (iM : Q(CommGroupWithZero $M)) (l₁ l₂ : qNF M) :
Q((NF.eval $(l₁.toNF)) * NF.eval $(l₂.toNF) = NF.eval $((qNF.mul l₁ l₂).toNF)) :=
match l₁, l₂ with
| [], l => (q(one_mul (NF.eval $(l.toNF))) :)
| l, [] => (q(mul_one (NF.eval $(l.toNF))) :)
| ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
if k₁ > k₂ then
let pf := mkMulProof iM t₁ (((a₂, x₂), k₂) :: t₂)
(q(NF.mul_eq_eval₁ ($a₁, $x₁) $pf) :)
else
if k₁ = k₂ then
let pf := mkMulProof iM t₁ t₂
(q(NF.mul_eq_eval₂ $a₁ $a₂ $x₁ $pf) :)
else
let pf := mkMulProof iM (((a₁, x₁), k₁) :: t₁) t₂
(q(NF.mul_eq_eval₃ ($a₂, $x₂) $pf) :)
