-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_eq_cancelAux (ctx : Context) (fuel : Nat) (m₁ m₂ r₁ r₂ : Poly)
    (h : denote_eq ctx (r₁.reverse ++ m₁, r₂.reverse ++ m₂)) : denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)

Proof state:
case neg
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)
r₁ r₂ m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
m₁ : List (Nat × Var)
k₂ : Nat
m₂ : List (Nat × Var)
h : denote_eq ctx (List.reverse r₁ ++ (k₁, v₁) :: m₁, List.reverse r₂ ++ (k₂, v₁) :: m₂)
hltv hgtv : ¬blt v₁ v₁ = true
hltk : ¬k₁.blt k₂ = true
hgtk : ¬k₂.blt k₁ = true
⊢ denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)

Tactic:
have heqk : k₁ = k₂ := eq_of_not_blt_eq_true hltk hgtk

Result:
case neg
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)
r₁ r₂ m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
m₁ : List (Nat × Var)
k₂ : Nat
m₂ : List (Nat × Var)
h : denote_eq ctx (List.reverse r₁ ++ (k₁, v₁) :: m₁, List.reverse r₂ ++ (k₂, v₁) :: m₂)
hltv hgtv : ¬blt v₁ v₁ = true
hltk : ¬k₁.blt k₂ = true
hgtk : ¬k₂.blt k₁ = true
heqk : k₁ = k₂
⊢ denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)

Proof state:
case pos.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)
r₁ r₂ m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
m₁ : List (Nat × Var)
k₂ : Nat
m₂ : List (Nat × Var)
hltv hgtv : ¬blt v₁ v₁ = true
hltk : ¬k₁.blt k₂ = true
hgtk : k₂.blt k₁ = true
h : denote ctx r₁ + (denote ctx m₁ + k₁ * Var.denote ctx v₁) = denote ctx r₂ + (denote ctx m₂ + k₂ * Var.denote ctx v₁)
haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁
⊢ denote ctx r₁ + (denote ctx m₁ + (k₁ - k₂) * Var.denote ctx v₁) = denote ctx r₂ + denote ctx m₂

Tactic:
rw [Nat.mul_sub_right_distrib, ← Nat.add_assoc, ← Nat.add_sub_assoc haux]

Result:
case pos.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)
r₁ r₂ m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
m₁ : List (Nat × Var)
k₂ : Nat
m₂ : List (Nat × Var)
hltv hgtv : ¬blt v₁ v₁ = true
hltk : ¬k₁.blt k₂ = true
hgtk : k₂.blt k₁ = true
h : denote ctx r₁ + (denote ctx m₁ + k₁ * Var.denote ctx v₁) = denote ctx r₂ + (denote ctx m₂ + k₂ * Var.denote ctx v₁)
haux : k₂ * Var.denote ctx v₁ ≤ k₁ * Var.denote ctx v₁
⊢ denote ctx r₁ + denote ctx m₁ + k₁ * Var.denote ctx v₁ - k₂ * Var.denote ctx v₁ = denote ctx r₂ + denote ctx m₂

Proof state:
case neg.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)
r₁ r₂ m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
m₁ m₂ : List (Nat × Var)
hltv hgtv : ¬blt v₁ v₁ = true
h : denote_eq ctx (List.reverse r₁ ++ (k₁, v₁) :: m₁, List.reverse r₂ ++ (k₁, v₁) :: m₂)
hltk hgtk : ¬k₁.blt k₁ = true
⊢ denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)

Tactic:
simp [denote_eq] at h |-

Result:
case neg.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)
r₁ r₂ m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
m₁ m₂ : List (Nat × Var)
hltv hgtv : ¬blt v₁ v₁ = true
hltk hgtk : ¬k₁.blt k₁ = true
h : denote ctx r₁ + (denote ctx m₁ + k₁ * Var.denote ctx v₁) = denote ctx r₂ + (denote ctx m₂ + k₁ * Var.denote ctx v₁)
⊢ denote ctx r₁ + denote ctx m₁ = denote ctx r₂ + denote ctx m₂

Proof state:
case pos.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)
r₁ r₂ m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
m₁ : List (Nat × Var)
k₂ : Nat
m₂ : List (Nat × Var)
h : denote_eq ctx (List.reverse r₁ ++ (k₁, v₁) :: m₁, List.reverse r₂ ++ (k₂, v₁) :: m₂)
hltv hgtv : ¬blt v₁ v₁ = true
hltk : ¬k₁.blt k₂ = true
hgtk : k₂.blt k₁ = true
⊢ denote_eq ctx (((k₁ - k₂, v₁) :: r₁).reverse ++ m₁, List.reverse r₂ ++ m₂)

Tactic:
simp [denote_eq] at h |-

Result:
case pos.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)
r₁ r₂ m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
m₁ : List (Nat × Var)
k₂ : Nat
m₂ : List (Nat × Var)
hltv hgtv : ¬blt v₁ v₁ = true
hltk : ¬k₁.blt k₂ = true
hgtk : k₂.blt k₁ = true
h : denote ctx r₁ + (denote ctx m₁ + k₁ * Var.denote ctx v₁) = denote ctx r₂ + (denote ctx m₂ + k₂ * Var.denote ctx v₁)
⊢ denote ctx r₁ + (denote ctx m₁ + (k₁ - k₂) * Var.denote ctx v₁) = denote ctx r₂ + denote ctx m₂

Proof state:
case pos.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)
r₁ r₂ m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
m₁ : List (Nat × Var)
k₂ : Nat
m₂ : List (Nat × Var)
hltv hgtv : ¬blt v₁ v₁ = true
hltk : k₁.blt k₂ = true
h : denote ctx r₁ + (denote ctx m₁ + k₁ * Var.denote ctx v₁) = denote ctx r₂ + (denote ctx m₂ + k₂ * Var.denote ctx v₁)
⊢ denote ctx r₁ + denote ctx m₁ = denote ctx r₂ + (denote ctx m₂ + (k₂ - k₁) * Var.denote ctx v₁)

Tactic:
have haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁ := Nat.mul_le_mul_right _ (Nat.le_of_lt (Nat.blt_eq.mp hltk))

Result:
case pos.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_eq ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_eq ctx (cancelAux fuel m₁ m₂ r₁ r₂)
r₁ r₂ m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
m₁ : List (Nat × Var)
k₂ : Nat
m₂ : List (Nat × Var)
hltv hgtv : ¬blt v₁ v₁ = true
hltk : k₁.blt k₂ = true
h : denote ctx r₁ + (denote ctx m₁ + k₁ * Var.denote ctx v₁) = denote ctx r₂ + (denote ctx m₂ + k₂ * Var.denote ctx v₁)
haux : k₁ * Var.denote ctx v₁ ≤ k₂ * Var.denote ctx v₁
⊢ denote ctx r₁ + denote ctx m₁ = denote ctx r₂ + (denote ctx m₂ + (k₂ - k₁) * Var.denote ctx v₁)