-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/SOM.lean
theorem Poly.add_denote (ctx : Context) (p₁ p₂ : Poly) : (p₁.add p₂).denote ctx = p₁.denote ctx + p₂.denote ctx :=
  go hugeFuel p₁ p₂
where
  go (fuel : Nat) (p₁ p₂ : Poly) : (Poly.add.go fuel p₁ p₂).denote ctx = p₁.denote ctx + p₂.denote ctx

Proof state:
case neg
ctx : Context
p₁✝¹ p₂✝¹ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝ p₂✝ : Poly
k₁ : Nat
m₁ : Mon
p₁ : List (Nat × Mon)
k₂ : Nat
m₂ : Mon
p₂ : List (Nat × Mon)
hlt : ¬m₁ < m₂
hgt : ¬m₂ < m₁
this : m₁ = m₂
⊢ denote ctx (bif k₁ + k₂ == 0 then add.go n✝ p₁ p₂ else (k₁ + k₂, m₁) :: add.go n✝ p₁ p₂) =
    k₁ * Mon.denote ctx m₁ + (k₂ * Mon.denote ctx m₂ + (denote ctx p₁ + denote ctx p₂))

Tactic:
subst m₂

Result:
case neg
ctx : Context
p₁✝¹ p₂✝¹ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝ p₂✝ : Poly
k₁ : Nat
m₁ : Mon
p₁ : List (Nat × Mon)
k₂ : Nat
p₂ : List (Nat × Mon)
hlt hgt : ¬m₁ < m₁
⊢ denote ctx (bif k₁ + k₂ == 0 then add.go n✝ p₁ p₂ else (k₁ + k₂, m₁) :: add.go n✝ p₁ p₂) =
    k₁ * Mon.denote ctx m₁ + (k₂ * Mon.denote ctx m₁ + (denote ctx p₁ + denote ctx p₂))

Proof state:
case succ
ctx : Context
p₁✝ p₂✝ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁ p₂ : Poly
⊢ denote ctx
      (match p₁, p₂ with
      | p₁, [] => p₁
      | [], p₁ => p₁
      | (k₁, m₁) :: p₁, (k₂, m₂) :: p₂ =>
        bif decide (m₁ < m₂) then (k₁, m₁) :: add.go n✝ p₁ ((k₂, m₂) :: p₂)
        else
          bif decide (m₂ < m₁) then (k₂, m₂) :: add.go n✝ ((k₁, m₁) :: p₁) p₂
          else bif k₁ + k₂ == 0 then add.go n✝ p₁ p₂ else (k₁ + k₂, m₁) :: add.go n✝ p₁ p₂) =
    denote ctx p₁ + denote ctx p₂

Tactic:
split <;> simp!

Result:
case succ.h_3
ctx : Context
p₁ p₂ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝¹ p₂✝¹ : Poly
k₁✝ : Nat
m₁✝ : Mon
p₁✝ : List (Nat × Mon)
k₂✝ : Nat
m₂✝ : Mon
p₂✝ : List (Nat × Mon)
⊢ denote ctx
      (bif decide (m₁✝ < m₂✝) then (k₁✝, m₁✝) :: add.go n✝ p₁✝ ((k₂✝, m₂✝) :: p₂✝)
      else
        bif decide (m₂✝ < m₁✝) then (k₂✝, m₂✝) :: add.go n✝ ((k₁✝, m₁✝) :: p₁✝) p₂✝
        else bif k₁✝ + k₂✝ == 0 then add.go n✝ p₁✝ p₂✝ else (k₁✝ + k₂✝, m₁✝) :: add.go n✝ p₁✝ p₂✝) =
    k₁✝ * Mon.denote ctx m₁✝ + denote ctx p₁✝ + (k₂✝ * Mon.denote ctx m₂✝ + denote ctx p₂✝)

Proof state:
case succ
ctx : Context
p₁✝ p₂✝ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁ p₂ : Poly
⊢ denote ctx (add.go (n✝ + 1) p₁ p₂) = denote ctx p₁ + denote ctx p₂

Tactic:
simp!

Result:
case succ
ctx : Context
p₁✝ p₂✝ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁ p₂ : Poly
⊢ denote ctx
      (match p₁, p₂ with
      | p₁, [] => p₁
      | [], p₁ => p₁
      | (k₁, m₁) :: p₁, (k₂, m₂) :: p₂ =>
        bif decide (m₁ < m₂) then (k₁, m₁) :: add.go n✝ p₁ ((k₂, m₂) :: p₂)
        else
          bif decide (m₂ < m₁) then (k₂, m₂) :: add.go n✝ ((k₁, m₁) :: p₁) p₂
          else bif k₁ + k₂ == 0 then add.go n✝ p₁ p₂ else (k₁ + k₂, m₁) :: add.go n✝ p₁ p₂) =
    denote ctx p₁ + denote ctx p₂

Proof state:
case pos
ctx : Context
p₁✝¹ p₂✝¹ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝ p₂✝ : Poly
k₁ : Nat
m₁ : Mon
p₁ : List (Nat × Mon)
k₂ : Nat
p₂ : List (Nat × Mon)
hlt hgt : ¬m₁ < m₁
heq : (k₁ + k₂ == 0) = true
⊢ denote ctx p₁ + denote ctx p₂ = k₁ * Mon.denote ctx m₁ + (k₂ * Mon.denote ctx m₁ + (denote ctx p₁ + denote ctx p₂))

Tactic:
simp [← Nat.add_assoc, ← Nat.right_distrib, eq_of_beq heq]

Result:
no goals

Proof state:
case neg
ctx : Context
p₁✝¹ p₂✝¹ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝ p₂✝ : Poly
k₁ : Nat
m₁ : Mon
p₁ : List (Nat × Mon)
k₂ : Nat
p₂ : List (Nat × Mon)
hlt hgt : ¬m₁ < m₁
⊢ denote ctx (bif k₁ + k₂ == 0 then add.go n✝ p₁ p₂ else (k₁ + k₂, m₁) :: add.go n✝ p₁ p₂) =
    k₁ * Mon.denote ctx m₁ + (k₂ * Mon.denote ctx m₁ + (denote ctx p₁ + denote ctx p₂))

Tactic:
by_cases heq : k₁ + k₂ == 0 <;> simp! [heq, ih]

Result:
case pos
ctx : Context
p₁✝¹ p₂✝¹ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝ p₂✝ : Poly
k₁ : Nat
m₁ : Mon
p₁ : List (Nat × Mon)
k₂ : Nat
p₂ : List (Nat × Mon)
hlt hgt : ¬m₁ < m₁
heq : (k₁ + k₂ == 0) = true
⊢ denote ctx p₁ + denote ctx p₂ = k₁ * Mon.denote ctx m₁ + (k₂ * Mon.denote ctx m₁ + (denote ctx p₁ + denote ctx p₂))

case neg
ctx : Context
p₁✝¹ p₂✝¹ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝ p₂✝ : Poly
k₁ : Nat
m₁ : Mon
p₁ : List (Nat × Mon)
k₂ : Nat
p₂ : List (Nat × Mon)
hlt hgt : ¬m₁ < m₁
heq : ¬(k₁ + k₂ == 0) = true
⊢ (k₁ + k₂) * Mon.denote ctx m₁ + (denote ctx p₁ + denote ctx p₂) =
    k₁ * Mon.denote ctx m₁ + (k₂ * Mon.denote ctx m₁ + (denote ctx p₁ + denote ctx p₂))

Proof state:
case neg
ctx : Context
p₁✝¹ p₂✝¹ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝ p₂✝ : Poly
k₁ : Nat
m₁ : Mon
p₁ : List (Nat × Mon)
k₂ : Nat
p₂ : List (Nat × Mon)
hlt hgt : ¬m₁ < m₁
heq : ¬(k₁ + k₂ == 0) = true
⊢ (k₁ + k₂) * Mon.denote ctx m₁ + (denote ctx p₁ + denote ctx p₂) =
    k₁ * Mon.denote ctx m₁ + (k₂ * Mon.denote ctx m₁ + (denote ctx p₁ + denote ctx p₂))

Tactic:
simp [Nat.right_distrib, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]

Result:
no goals

Proof state:
case neg
ctx : Context
p₁✝¹ p₂✝¹ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝ p₂✝ : Poly
k₁ : Nat
m₁ : Mon
p₁ : List (Nat × Mon)
k₂ : Nat
m₂ : Mon
p₂ : List (Nat × Mon)
hlt : ¬m₁ < m₂
hgt : ¬m₂ < m₁
⊢ denote ctx (bif k₁ + k₂ == 0 then add.go n✝ p₁ p₂ else (k₁ + k₂, m₁) :: add.go n✝ p₁ p₂) =
    k₁ * Mon.denote ctx m₁ + (k₂ * Mon.denote ctx m₂ + (denote ctx p₁ + denote ctx p₂))

Tactic:
have : m₁ = m₂ := List.le_antisymm hgt hlt

Result:
case neg
ctx : Context
p₁✝¹ p₂✝¹ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝ p₂✝ : Poly
k₁ : Nat
m₁ : Mon
p₁ : List (Nat × Mon)
k₂ : Nat
m₂ : Mon
p₂ : List (Nat × Mon)
hlt : ¬m₁ < m₂
hgt : ¬m₂ < m₁
this : m₁ = m₂
⊢ denote ctx (bif k₁ + k₂ == 0 then add.go n✝ p₁ p₂ else (k₁ + k₂, m₁) :: add.go n✝ p₁ p₂) =
    k₁ * Mon.denote ctx m₁ + (k₂ * Mon.denote ctx m₂ + (denote ctx p₁ + denote ctx p₂))

Proof state:
case zero
ctx : Context
p₁✝ p₂✝ p₁ p₂ : Poly
⊢ denote ctx (add.go 0 p₁ p₂) = denote ctx p₁ + denote ctx p₂

Tactic:
simp! [append_denote]

Result:
no goals

Proof state:
ctx : Context
p₁✝¹ p₂✝¹ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝ p₂✝ : Poly
k₁ : Nat
m₁ : Mon
p₁ : List (Nat × Mon)
k₂ : Nat
m₂ : Mon
p₂ : List (Nat × Mon)
⊢ denote ctx
      (bif decide (m₁ < m₂) then (k₁, m₁) :: add.go n✝ p₁ ((k₂, m₂) :: p₂)
      else
        bif decide (m₂ < m₁) then (k₂, m₂) :: add.go n✝ ((k₁, m₁) :: p₁) p₂
        else bif k₁ + k₂ == 0 then add.go n✝ p₁ p₂ else (k₁ + k₂, m₁) :: add.go n✝ p₁ p₂) =
    k₁ * Mon.denote ctx m₁ + denote ctx p₁ + (k₂ * Mon.denote ctx m₂ + denote ctx p₂)

Tactic:
by_cases hlt : m₁ < m₂ <;> simp! [hlt, Nat.add_assoc, ih]

Result:
case neg
ctx : Context
p₁✝¹ p₂✝¹ : Poly
n✝ : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (add.go n✝ p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁✝ p₂✝ : Poly
k₁ : Nat
m₁ : Mon
p₁ : List (Nat × Mon)
k₂ : Nat
m₂ : Mon
p₂ : List (Nat × Mon)
hlt : ¬m₁ < m₂
⊢ denote ctx
      (bif decide (m₂ < m₁) then (k₂, m₂) :: add.go n✝ ((k₁, m₁) :: p₁) p₂
      else bif k₁ + k₂ == 0 then add.go n✝ p₁ p₂ else (k₁ + k₂, m₁) :: add.go n✝ p₁ p₂) =
    k₁ * Mon.denote ctx m₁ + (denote ctx p₁ + (k₂ * Mon.denote ctx m₂ + denote ctx p₂))