no goals
case zero
ctx : Context
p₁✝ p₂✝ p₁ p₂ : Poly
⊢ denote ctx (add.go zero p₁ p₂) = denote ctx p₁ + denote ctx p₂
simp! [append_denote]
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₂
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 (succ n✝) p₁ p₂) = denote ctx p₁ + denote ctx p₂
simp!
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₂✝)
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₂
split <;> simp!
case inr
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₂))
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₂)
by_cases hlt : m₁ < m₂ <;> simp! [hlt, Nat.add_assoc, ih]
case inr.inr
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₂))
case inr
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₂))
by_cases hgt : m₂ < m₁ <;> simp! [hgt, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, ih]
case inr.inr
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₂))
case inr.inr
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₂))
have : m₁ = m₂ := List.le_antisymm hgt hlt
case inr.inr
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₂))
case inr.inr
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₂))
subst m₂
case inr.inr.inl
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 inr.inr.inr
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₂))
case inr.inr
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₂))
by_cases heq : k₁ + k₂ == 0 <;> simp! [heq, ih]
no goals
case inr.inr.inl
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₂))
simp [← Nat.add_assoc, ← Nat.right_distrib, eq_of_beq heq]
no goals
case inr.inr.inr
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₂))
simp [Nat.right_distrib, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]