-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem Expr.denote_toPoly_go (ctx : Context) (e : Expr) :
  (toPoly.go k e p).denote ctx = k * e.denote ctx + p.denote ctx

Proof state:
case neg
ctx : Context
k k' : Nat
p : Poly
h : ¬(k' == 0) = true
⊢ Poly.denote ctx ((bif k' == 0 then id else fun x => (k * k', fixedVar) :: x) p) =
    k * denote ctx (num k') + Poly.denote ctx p

Tactic:
simp [h, Var.denote]

Result:
no goals

Proof state:
case neg
ctx : Context
k : Nat
a : Expr
k' : Nat
ih : ∀ {p : Poly}, Poly.denote ctx (toPoly.go (k * k') a p) = k * k' * denote ctx a + Poly.denote ctx p
p : Poly
h : ¬(k' == 0) = true
⊢ Poly.denote ctx ((bif k' == 0 then id else toPoly.go (k * k') a) p) = k * (denote ctx a * k') + Poly.denote ctx p

Tactic:
simp [h, cond_false, ih, Nat.mul_assoc]

Result:
no goals

Proof state:
case case5
ctx : Context
k : Nat
a : Expr
k' : Nat
ih : ∀ {p : Poly}, Poly.denote ctx (toPoly.go (k * k') a p) = k * k' * denote ctx a + Poly.denote ctx p
p : Poly
⊢ Poly.denote ctx (toPoly.go k (a.mulR k') p) = k * denote ctx (a.mulR k') + Poly.denote ctx p

Tactic:
simp only [toPoly.go, denote, mul_eq]

Result:
case case5
ctx : Context
k : Nat
a : Expr
k' : Nat
ih : ∀ {p : Poly}, Poly.denote ctx (toPoly.go (k * k') a p) = k * k' * denote ctx a + Poly.denote ctx p
p : Poly
⊢ Poly.denote ctx ((bif k' == 0 then id else toPoly.go (k * k') a) p) = k * (denote ctx a * k') + Poly.denote ctx p

Proof state:
case case1
ctx : Context
k k' : Nat
p : Poly
⊢ Poly.denote ctx ((bif k' == 0 then id else fun x => (k * k', fixedVar) :: x) p) =
    k * denote ctx (num k') + Poly.denote ctx p

Tactic:
by_cases h : k' == 0

Result:
case pos
ctx : Context
k k' : Nat
p : Poly
h : (k' == 0) = true
⊢ Poly.denote ctx ((bif k' == 0 then id else fun x => (k * k', fixedVar) :: x) p) =
    k * denote ctx (num k') + Poly.denote ctx p

case neg
ctx : Context
k k' : Nat
p : Poly
h : ¬(k' == 0) = true
⊢ Poly.denote ctx ((bif k' == 0 then id else fun x => (k * k', fixedVar) :: x) p) =
    k * denote ctx (num k') + Poly.denote ctx p

Proof state:
case case3
ctx : Context
k : Nat
a b : Expr
iha : ∀ {p : Poly}, Poly.denote ctx (toPoly.go k a p) = k * denote ctx a + Poly.denote ctx p
ihb : ∀ {p : Poly}, Poly.denote ctx (toPoly.go k b p) = k * denote ctx b + Poly.denote ctx p
p : Poly
⊢ Poly.denote ctx (toPoly.go k (a.add b) p) = k * denote ctx (a.add b) + Poly.denote ctx p

Tactic:
simp [toPoly.go, iha, ihb]

Result:
no goals

Proof state:
case case5
ctx : Context
k : Nat
a : Expr
k' : Nat
ih : ∀ {p : Poly}, Poly.denote ctx (toPoly.go (k * k') a p) = k * k' * denote ctx a + Poly.denote ctx p
p : Poly
⊢ Poly.denote ctx ((bif k' == 0 then id else toPoly.go (k * k') a) p) = k * (denote ctx a * k') + Poly.denote ctx p

Tactic:
by_cases h : k' == 0

Result:
case pos
ctx : Context
k : Nat
a : Expr
k' : Nat
ih : ∀ {p : Poly}, Poly.denote ctx (toPoly.go (k * k') a p) = k * k' * denote ctx a + Poly.denote ctx p
p : Poly
h : (k' == 0) = true
⊢ Poly.denote ctx ((bif k' == 0 then id else toPoly.go (k * k') a) p) = k * (denote ctx a * k') + Poly.denote ctx p

case neg
ctx : Context
k : Nat
a : Expr
k' : Nat
ih : ∀ {p : Poly}, Poly.denote ctx (toPoly.go (k * k') a p) = k * k' * denote ctx a + Poly.denote ctx p
p : Poly
h : ¬(k' == 0) = true
⊢ Poly.denote ctx ((bif k' == 0 then id else toPoly.go (k * k') a) p) = k * (denote ctx a * k') + Poly.denote ctx p

Proof state:
case case1
ctx : Context
k k' : Nat
p : Poly
⊢ Poly.denote ctx (toPoly.go k (num k') p) = k * denote ctx (num k') + Poly.denote ctx p

Tactic:
simp only [toPoly.go]

Result:
case case1
ctx : Context
k k' : Nat
p : Poly
⊢ Poly.denote ctx ((bif k' == 0 then id else fun x => (k * k', fixedVar) :: x) p) =
    k * denote ctx (num k') + Poly.denote ctx p

Proof state:
case case2
ctx : Context
k : Nat
i : Var
p : Poly
⊢ Poly.denote ctx (toPoly.go k (var i) p) = k * denote ctx (var i) + Poly.denote ctx p

Tactic:
simp [toPoly.go]

Result:
no goals

Proof state:
case pos
ctx : Context
k : Nat
a : Expr
k' : Nat
ih : ∀ {p : Poly}, Poly.denote ctx (toPoly.go (k * k') a p) = k * k' * denote ctx a + Poly.denote ctx p
p : Poly
h : (k' == 0) = true
⊢ Poly.denote ctx ((bif k' == 0 then id else toPoly.go (k * k') a) p) = k * (denote ctx a * k') + Poly.denote ctx p

Tactic:
simp [h, eq_of_beq h]

Result:
no goals

Proof state:
case pos
ctx : Context
k k' : Nat
p : Poly
h : (k' == 0) = true
⊢ Poly.denote ctx ((bif k' == 0 then id else fun x => (k * k', fixedVar) :: x) p) =
    k * denote ctx (num k') + Poly.denote ctx p

Tactic:
simp [h, eq_of_beq h]

Result:
no goals