ctx : Context
k : Nat
v : Var
⊢ Expr.denote ctx (bif v == fixedVar then Expr.num k else bif k == 1 then Expr.var v else Expr.mulL k (Expr.var v)) =
    k * Var.denote ctx v
ctx : Context
k : Nat
v : Var
⊢ Expr.denote ctx (monomialToExpr k v) = k * Var.denote ctx v
simp [monomialToExpr]
case inl
ctx : Context
k : Nat
v : Var
h : (v == fixedVar) = true
⊢ k = k * Var.denote ctx v

case inr
ctx : Context
k : Nat
v : Var
h : ¬(v == fixedVar) = true
⊢ Expr.denote ctx (bif k == 1 then Expr.var v else Expr.mulL k (Expr.var v)) = k * Var.denote ctx v
ctx : Context
k : Nat
v : Var
⊢ Expr.denote ctx (bif v == fixedVar then Expr.num k else bif k == 1 then Expr.var v else Expr.mulL k (Expr.var v)) =
    k * Var.denote ctx v
by_cases h : v == fixedVar <;> simp [h, Expr.denote]
no goals
case inl
ctx : Context
k : Nat
v : Var
h : (v == fixedVar) = true
⊢ k = k * Var.denote ctx v
simp [eq_of_beq h, Var.denote]
case inr.inl
ctx : Context
k : Nat
v : Var
h✝ : ¬(v == fixedVar) = true
h : (k == 1) = true
⊢ Var.denote ctx v = k * Var.denote ctx v
case inr
ctx : Context
k : Nat
v : Var
h : ¬(v == fixedVar) = true
⊢ Expr.denote ctx (bif k == 1 then Expr.var v else Expr.mulL k (Expr.var v)) = k * Var.denote ctx v
by_cases h : k == 1 <;> simp [h, Expr.denote]
no goals
case inr.inl
ctx : Context
k : Nat
v : Var
h✝ : ¬(v == fixedVar) = true
h : (k == 1) = true
⊢ Var.denote ctx v = k * Var.denote ctx v
simp [eq_of_beq h]