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

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

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

Result:
case neg
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_le ctx (cancelAux fuel m₁ m₂ r₁ r₂)
r₁ r₂ m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
m₁ : List (Nat × Var)
k₂ : Nat
v₂ : Var
m₂ : List (Nat × Var)
h : denote_le ctx (List.reverse r₁ ++ (k₁, v₁) :: m₁, List.reverse r₂ ++ (k₂, v₂) :: m₂)
hltv : ¬blt v₁ v₂ = true
hgtv : ¬blt v₂ v₁ = true
heqv : v₁ = v₂
⊢ denote_le ctx
    (bif k₁.blt k₂ then cancelAux fuel m₁ m₂ r₁ ((k₂ - k₁, v₁) :: r₂)
    else bif k₂.blt k₁ then cancelAux fuel m₁ m₂ ((k₁ - k₂, v₁) :: r₁) r₂ else cancelAux fuel m₁ m₂ r₁ r₂)

Proof state:
case pos.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_le 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₂ * Var.denote ctx v₁ - k₁ * Var.denote ctx v₁

Tactic:
apply Nat.le_sub_of_add_le

Result:
case pos.h.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_le 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₁ + k₁ * Var.denote ctx v₁ ≤ denote ctx r₂ + denote ctx m₂ + k₂ * Var.denote ctx v₁

Proof state:
case pos.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_le ctx (cancelAux fuel m₁ m₂ r₁ r₂)
r₁ r₂ m₁✝ m₂✝ : Poly
k₁ : Nat
v₁ : Var
m₁ : List (Nat × Var)
k₂ : Nat
v₂ : Var
m₂ : List (Nat × Var)
hltv : blt v₁ v₂ = 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₁ * Var.denote ctx v₁) ≤ denote ctx r₂ + (denote ctx m₂ + k₂ * Var.denote ctx v₂)

Tactic:
assumption

Result:
no goals

Proof state:
case neg.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_le 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_le ctx (List.reverse r₁ ++ (k₁, v₁) :: m₁, List.reverse r₂ ++ (k₁, v₁) :: m₂)
hltk hgtk : ¬k₁.blt k₁ = true
⊢ denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)

Tactic:
simp [denote_le] at h |-

Result:
case neg.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_le 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_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_le 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_le ctx (List.reverse r₁ ++ (k₁, v₁) :: m₁, List.reverse r₂ ++ (k₂, v₁) :: m₂)
hltv hgtv : ¬blt v₁ v₁ = true
hltk : k₁.blt k₂ = true
⊢ denote_le ctx (List.reverse r₁ ++ m₁, ((k₂ - k₁, v₁) :: r₂).reverse ++ m₂)

Tactic:
simp [denote_le] at h |-

Result:
case pos.h
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_le 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₁)

Proof state:
case succ
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_le ctx (cancelAux fuel m₁ m₂ r₁ r₂)
m₁ m₂ r₁ r₂ : Poly
h : denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂)
⊢ denote_le ctx
    (match m₁, m₂ with
    | m₁, [] => (List.reverse r₁ ++ m₁, List.reverse r₂)
    | [], m₂ => (List.reverse r₁, List.reverse r₂ ++ m₂)
    | (k₁, v₁) :: m₁, (k₂, v₂) :: m₂ =>
      bif blt v₁ v₂ then cancelAux fuel m₁ ((k₂, v₂) :: m₂) ((k₁, v₁) :: r₁) r₂
      else
        bif blt v₂ v₁ then cancelAux fuel ((k₁, v₁) :: m₁) m₂ r₁ ((k₂, v₂) :: r₂)
        else
          bif k₁.blt k₂ then cancelAux fuel m₁ m₂ r₁ ((k₂ - k₁, v₁) :: r₂)
          else bif k₂.blt k₁ then cancelAux fuel m₁ m₂ ((k₁ - k₂, v₁) :: r₁) r₂ else cancelAux fuel m₁ m₂ r₁ r₂)

Tactic:
split <;> try (simp at h; assumption)

Result:
case succ.h_3
ctx : Context
fuel : Nat
ih :
  ∀ (m₁ m₂ r₁ r₂ : Poly),
    denote_le ctx (List.reverse r₁ ++ m₁, List.reverse r₂ ++ m₂) → denote_le ctx (cancelAux fuel m₁ m₂ r₁ r₂)
r₁ r₂ m₁✝¹ m₂✝¹ : Poly
k₁✝ : Nat
v₁✝ : Var
m₁✝ : List (Nat × Var)
k₂✝ : Nat
v₂✝ : Var
m₂✝ : List (Nat × Var)
h : denote_le ctx (List.reverse r₁ ++ (k₁✝, v₁✝) :: m₁✝, List.reverse r₂ ++ (k₂✝, v₂✝) :: m₂✝)
⊢ denote_le ctx
    (bif blt v₁✝ v₂✝ then cancelAux fuel m₁✝ ((k₂✝, v₂✝) :: m₂✝) ((k₁✝, v₁✝) :: r₁) r₂
    else
      bif blt v₂✝ v₁✝ then cancelAux fuel ((k₁✝, v₁✝) :: m₁✝) m₂✝ r₁ ((k₂✝, v₂✝) :: r₂)
      else
        bif k₁✝.blt k₂✝ then cancelAux fuel m₁✝ m₂✝ r₁ ((k₂✝ - k₁✝, v₁✝) :: r₂)
        else bif k₂✝.blt k₁✝ then cancelAux fuel m₁✝ m₂✝ ((k₁✝ - k₂✝, v₁✝) :: r₁) r₂ else cancelAux fuel m₁✝ m₂✝ r₁ r₂)