-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_combineAux (ctx : Context) (fuel : Nat) (p₁ p₂ : Poly) : (p₁.combineAux fuel p₂).denote ctx = p₁.denote ctx + p₂.denote ctx

Proof state:
case neg
ctx : Context
fuel : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (combineAux fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂
m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
p₁ : List (Nat × Var)
k₂ : Nat
v₂ : Var
p₂ : List (Nat × Var)
hltv : ¬blt v₁ v₂ = true
hgtv : ¬blt v₂ v₁ = true
⊢ denote ctx p₁ + (denote ctx p₂ + (k₁ * Var.denote ctx v₁ + k₂ * Var.denote ctx v₁)) =
    denote ctx p₁ + (denote ctx p₂ + (k₁ * Var.denote ctx v₁ + k₂ * Var.denote ctx v₂))

Tactic:
have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv

Result:
case neg
ctx : Context
fuel : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (combineAux fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂
m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
p₁ : List (Nat × Var)
k₂ : Nat
v₂ : Var
p₂ : List (Nat × Var)
hltv : ¬blt v₁ v₂ = true
hgtv : ¬blt v₂ v₁ = true
heqv : v₁ = v₂
⊢ denote ctx p₁ + (denote ctx p₂ + (k₁ * Var.denote ctx v₁ + k₂ * Var.denote ctx v₁)) =
    denote ctx p₁ + (denote ctx p₂ + (k₁ * Var.denote ctx v₁ + k₂ * Var.denote ctx v₂))

Proof state:
case succ.h_3
ctx : Context
fuel : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (combineAux fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂
m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
p₁ : List (Nat × Var)
k₂ : Nat
v₂ : Var
p₂ : List (Nat × Var)
⊢ denote ctx
      (bif blt v₁ v₂ then (k₁, v₁) :: combineAux fuel p₁ ((k₂, v₂) :: p₂)
      else
        bif blt v₂ v₁ then (k₂, v₂) :: combineAux fuel ((k₁, v₁) :: p₁) p₂
        else (k₁ + k₂, v₁) :: combineAux fuel p₁ p₂) =
    denote ctx p₁ + (denote ctx p₂ + (k₁ * Var.denote ctx v₁ + k₂ * Var.denote ctx v₂))

Tactic:
by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv, ih]

Result:
case neg
ctx : Context
fuel : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (combineAux fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂
m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
p₁ : List (Nat × Var)
k₂ : Nat
v₂ : Var
p₂ : List (Nat × Var)
hltv : ¬blt v₁ v₂ = true
⊢ denote ctx
      (bif blt v₂ v₁ then (k₂, v₂) :: combineAux fuel ((k₁, v₁) :: p₁) p₂ else (k₁ + k₂, v₁) :: combineAux fuel p₁ p₂) =
    denote ctx p₁ + (denote ctx p₂ + (k₁ * Var.denote ctx v₁ + k₂ * Var.denote ctx v₂))

Proof state:
case neg
ctx : Context
fuel : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (combineAux fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂
m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
p₁ : List (Nat × Var)
k₂ : Nat
v₂ : Var
p₂ : List (Nat × Var)
hltv : ¬blt v₁ v₂ = true
hgtv : ¬blt v₂ v₁ = true
heqv : v₁ = v₂
⊢ denote ctx p₁ + (denote ctx p₂ + (k₁ * Var.denote ctx v₁ + k₂ * Var.denote ctx v₁)) =
    denote ctx p₁ + (denote ctx p₂ + (k₁ * Var.denote ctx v₁ + k₂ * Var.denote ctx v₂))

Tactic:
simp [heqv]

Result:
no goals

Proof state:
ctx : Context
fuel : Nat
p₁ p₂ : Poly
⊢ denote ctx (combineAux fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂

Tactic:
induction fuel generalizing p₁ p₂ with simp [combineAux]
| succ fuel ih =>
  split <;> simp
  rename_i k₁ v₁ p₁ k₂ v₂ p₂
  by_cases hltv : Nat.blt v₁ v₂ <;> simp [hltv, ih]
  by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv, ih]
  have heqv : v₁ = v₂ := eq_of_not_blt_eq_true hltv hgtv
  simp [heqv]

Result:
no goals

Proof state:
case succ
ctx : Context
fuel : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (combineAux fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂
p₁ p₂ : Poly
⊢ denote ctx
      (match p₁, p₂ with
      | p₁, [] => p₁
      | [], p₁ => p₁
      | (k₁, v₁) :: p₁, (k₂, v₂) :: p₂ =>
        bif blt v₁ v₂ then (k₁, v₁) :: combineAux fuel p₁ ((k₂, v₂) :: p₂)
        else
          bif blt v₂ v₁ then (k₂, v₂) :: combineAux fuel ((k₁, v₁) :: p₁) p₂
          else (k₁ + k₂, v₁) :: combineAux fuel p₁ p₂) =
    denote ctx p₁ + denote ctx p₂

Tactic:
split <;> simp

Result:
case succ.h_3
ctx : Context
fuel : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (combineAux fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂
m₁✝¹ m₂✝¹ : Poly
k₁✝ : Nat
v₁✝ : Var
m₁✝ : List (Nat × Var)
k₂✝ : Nat
v₂✝ : Var
m₂✝ : List (Nat × Var)
⊢ denote ctx
      (bif blt v₁✝ v₂✝ then (k₁✝, v₁✝) :: combineAux fuel m₁✝ ((k₂✝, v₂✝) :: m₂✝)
      else
        bif blt v₂✝ v₁✝ then (k₂✝, v₂✝) :: combineAux fuel ((k₁✝, v₁✝) :: m₁✝) m₂✝
        else (k₁✝ + k₂✝, v₁✝) :: combineAux fuel m₁✝ m₂✝) =
    denote ctx m₁✝ + (denote ctx m₂✝ + (k₁✝ * Var.denote ctx v₁✝ + k₂✝ * Var.denote ctx v₂✝))

Proof state:
case succ.h_3
ctx : Context
fuel : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (combineAux fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂
m₁✝¹ m₂✝¹ : Poly
k₁✝ : Nat
v₁✝ : Var
m₁✝ : List (Nat × Var)
k₂✝ : Nat
v₂✝ : Var
m₂✝ : List (Nat × Var)
⊢ denote ctx
      (bif blt v₁✝ v₂✝ then (k₁✝, v₁✝) :: combineAux fuel m₁✝ ((k₂✝, v₂✝) :: m₂✝)
      else
        bif blt v₂✝ v₁✝ then (k₂✝, v₂✝) :: combineAux fuel ((k₁✝, v₁✝) :: m₁✝) m₂✝
        else (k₁✝ + k₂✝, v₁✝) :: combineAux fuel m₁✝ m₂✝) =
    denote ctx m₁✝ + (denote ctx m₂✝ + (k₁✝ * Var.denote ctx v₁✝ + k₂✝ * Var.denote ctx v₂✝))

Tactic:
rename_i k₁ v₁ p₁ k₂ v₂ p₂

Result:
case succ.h_3
ctx : Context
fuel : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (combineAux fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂
m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
p₁ : List (Nat × Var)
k₂ : Nat
v₂ : Var
p₂ : List (Nat × Var)
⊢ denote ctx
      (bif blt v₁ v₂ then (k₁, v₁) :: combineAux fuel p₁ ((k₂, v₂) :: p₂)
      else
        bif blt v₂ v₁ then (k₂, v₂) :: combineAux fuel ((k₁, v₁) :: p₁) p₂
        else (k₁ + k₂, v₁) :: combineAux fuel p₁ p₂) =
    denote ctx p₁ + (denote ctx p₂ + (k₁ * Var.denote ctx v₁ + k₂ * Var.denote ctx v₂))

Proof state:
case neg
ctx : Context
fuel : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (combineAux fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂
m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
p₁ : List (Nat × Var)
k₂ : Nat
v₂ : Var
p₂ : List (Nat × Var)
hltv : ¬blt v₁ v₂ = true
⊢ denote ctx
      (bif blt v₂ v₁ then (k₂, v₂) :: combineAux fuel ((k₁, v₁) :: p₁) p₂ else (k₁ + k₂, v₁) :: combineAux fuel p₁ p₂) =
    denote ctx p₁ + (denote ctx p₂ + (k₁ * Var.denote ctx v₁ + k₂ * Var.denote ctx v₂))

Tactic:
by_cases hgtv : Nat.blt v₂ v₁ <;> simp [hgtv, ih]

Result:
case neg
ctx : Context
fuel : Nat
ih : ∀ (p₁ p₂ : Poly), denote ctx (combineAux fuel p₁ p₂) = denote ctx p₁ + denote ctx p₂
m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
p₁ : List (Nat × Var)
k₂ : Nat
v₂ : Var
p₂ : List (Nat × Var)
hltv : ¬blt v₁ v₂ = true
hgtv : ¬blt v₂ v₁ = true
⊢ denote ctx p₁ + (denote ctx p₂ + (k₁ * Var.denote ctx v₁ + k₂ * Var.denote ctx v₁)) =
    denote ctx p₁ + (denote ctx p₂ + (k₁ * Var.denote ctx v₁ + k₂ * Var.denote ctx v₂))