-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Poly.denote_insert (ctx : Context) (k : Nat) (v : Var) (p : Poly) :
    (p.insert k v).denote ctx = p.denote ctx + k * v.denote ctx

Proof state:
case neg
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
h₁ : ¬blt v v' = true
h₂ : ¬beq v v' = true
⊢ denote ctx ((k', v') :: insert k v p) = denote ctx ((k', v') :: p) + k * Var.denote ctx v

Tactic:
simp [denote_insert]

Result:
no goals

Proof state:
case neg
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
h₁ : ¬blt v v' = true
h₂ : ¬beq v v' = true
⊢ denote ctx (insert k v ((k', v') :: p)) = denote ctx ((k', v') :: p) + k * Var.denote ctx v

Tactic:
simp only [insert, h₁, h₂, cond_false, cond_true]

Result:
case neg
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
h₁ : ¬blt v v' = true
h₂ : ¬beq v v' = true
⊢ denote ctx ((k', v') :: insert k v p) = denote ctx ((k', v') :: p) + k * Var.denote ctx v

Proof state:
case pos
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
h₁ : blt v v' = true
⊢ denote ctx (insert k v ((k', v') :: p)) = denote ctx ((k', v') :: p) + k * Var.denote ctx v

Tactic:
simp [h₁]

Result:
no goals

Proof state:
ctx : Context
k : Nat
v : Var
p : Poly
⊢ denote ctx (insert k v []) = denote ctx [] + k * Var.denote ctx v

Tactic:
simp

Result:
no goals

Proof state:
case neg
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
h₁ : ¬blt v v' = true
⊢ denote ctx (insert k v ((k', v') :: p)) = denote ctx ((k', v') :: p) + k * Var.denote ctx v

Tactic:
by_cases h₂ : Nat.beq v v'

Result:
case pos
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
h₁ : ¬blt v v' = true
h₂ : beq v v' = true
⊢ denote ctx (insert k v ((k', v') :: p)) = denote ctx ((k', v') :: p) + k * Var.denote ctx v

case neg
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
h₁ : ¬blt v v' = true
h₂ : ¬beq v v' = true
⊢ denote ctx (insert k v ((k', v') :: p)) = denote ctx ((k', v') :: p) + k * Var.denote ctx v

Proof state:
case pos
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
h₁ : ¬blt v v' = true
h₂ : beq v v' = true
⊢ denote ctx ((k + k', v') :: p) = denote ctx ((k', v') :: p) + k * Var.denote ctx v

Tactic:
simp [Nat.eq_of_beq_eq_true h₂]

Result:
no goals

Proof state:
case pos
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
h₁ : ¬blt v v' = true
h₂ : beq v v' = true
⊢ denote ctx (insert k v ((k', v') :: p)) = denote ctx ((k', v') :: p) + k * Var.denote ctx v

Tactic:
simp only [insert, h₁, h₂, cond_false, cond_true]

Result:
case pos
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
h₁ : ¬blt v v' = true
h₂ : beq v v' = true
⊢ denote ctx ((k + k', v') :: p) = denote ctx ((k', v') :: p) + k * Var.denote ctx v

Proof state:
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
⊢ denote ctx (insert k v ((k', v') :: p)) = denote ctx ((k', v') :: p) + k * Var.denote ctx v

Tactic:
by_cases h₁ : Nat.blt v v'

Result:
case pos
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
h₁ : blt v v' = true
⊢ denote ctx (insert k v ((k', v') :: p)) = denote ctx ((k', v') :: p) + k * Var.denote ctx v

case neg
ctx : Context
k : Nat
v : Var
p✝ : Poly
k' : Nat
v' : Var
p : List (Nat × Var)
h₁ : ¬blt v v' = true
⊢ denote ctx (insert k v ((k', v') :: p)) = denote ctx ((k', v') :: p) + k * Var.denote ctx v