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

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

Tactic:
simp [denote_le] at ih ⊢

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

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

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

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

Tactic:
have ih := ih (h := h)

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

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

Tactic:
simp [denote_le] at ih ⊢

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

Tactic:
have := Nat.le_add_of_sub_le ih

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