-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Linear.lean
theorem ExprCnstr.denote_toNormPoly (ctx : Context) (c : ExprCnstr) : c.toNormPoly.denote ctx = c.denote ctx

Proof state:
case mk
ctx : Context
eq : Bool
lhs rhs : Expr
⊢ (bif eq then
      Poly.denote_eq ctx ((lhs.toNormPoly.cancel rhs.toNormPoly).fst, (lhs.toNormPoly.cancel rhs.toNormPoly).snd)
    else Poly.denote_le ctx ((lhs.toNormPoly.cancel rhs.toNormPoly).fst, (lhs.toNormPoly.cancel rhs.toNormPoly).snd)) ↔
    bif eq then Expr.denote ctx lhs = Expr.denote ctx rhs else Expr.denote ctx lhs ≤ Expr.denote ctx rhs

Tactic:
by_cases h : eq = true <;> simp [h]

Result:
case pos
ctx : Context
eq : Bool
lhs rhs : Expr
h : eq = true
⊢ Poly.denote_eq ctx ((lhs.toNormPoly.cancel rhs.toNormPoly).fst, (lhs.toNormPoly.cancel rhs.toNormPoly).snd) ↔
    Expr.denote ctx lhs = Expr.denote ctx rhs

case neg
ctx : Context
eq : Bool
lhs rhs : Expr
h : ¬eq = true
⊢ Poly.denote_le ctx ((lhs.toNormPoly.cancel rhs.toNormPoly).fst, (lhs.toNormPoly.cancel rhs.toNormPoly).snd) ↔
    Expr.denote ctx lhs ≤ Expr.denote ctx rhs

Proof state:
case mk
ctx : Context
eq✝ : Bool
lhs✝ rhs✝ : Expr
⊢ PolyCnstr.denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }.toNormPoly =
    denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }

Tactic:
rename_i eq lhs rhs

Result:
case mk
ctx : Context
eq : Bool
lhs rhs : Expr
⊢ PolyCnstr.denote ctx { eq := eq, lhs := lhs, rhs := rhs }.toNormPoly = denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Proof state:
case neg
ctx : Context
eq : Bool
lhs rhs : Expr
h : ¬eq = true
⊢ Poly.denote_le ctx ((lhs.toNormPoly.cancel rhs.toNormPoly).fst, (lhs.toNormPoly.cancel rhs.toNormPoly).snd) ↔
    Expr.denote ctx lhs ≤ Expr.denote ctx rhs

Tactic:
rw [Poly.denote_le_cancel_eq]

Result:
case neg
ctx : Context
eq : Bool
lhs rhs : Expr
h : ¬eq = true
⊢ Poly.denote_le ctx (lhs.toNormPoly, rhs.toNormPoly) ↔ Expr.denote ctx lhs ≤ Expr.denote ctx rhs

Proof state:
case pos
ctx : Context
eq : Bool
lhs rhs : Expr
h : eq = true
⊢ Poly.denote_eq ctx ((lhs.toNormPoly.cancel rhs.toNormPoly).fst, (lhs.toNormPoly.cancel rhs.toNormPoly).snd) ↔
    Expr.denote ctx lhs = Expr.denote ctx rhs

Tactic:
rw [Poly.denote_eq_cancel_eq]

Result:
case pos
ctx : Context
eq : Bool
lhs rhs : Expr
h : eq = true
⊢ Poly.denote_eq ctx (lhs.toNormPoly, rhs.toNormPoly) ↔ Expr.denote ctx lhs = Expr.denote ctx rhs

Proof state:
case mk
ctx : Context
eq : Bool
lhs rhs : Expr
⊢ PolyCnstr.denote ctx { eq := eq, lhs := lhs, rhs := rhs }.toNormPoly = denote ctx { eq := eq, lhs := lhs, rhs := rhs }

Tactic:
simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toNormPoly]

Result:
case mk
ctx : Context
eq : Bool
lhs rhs : Expr
⊢ (bif eq then
      Poly.denote_eq ctx ((lhs.toNormPoly.cancel rhs.toNormPoly).fst, (lhs.toNormPoly.cancel rhs.toNormPoly).snd)
    else Poly.denote_le ctx ((lhs.toNormPoly.cancel rhs.toNormPoly).fst, (lhs.toNormPoly.cancel rhs.toNormPoly).snd)) ↔
    bif eq then Expr.denote ctx lhs = Expr.denote ctx rhs else Expr.denote ctx lhs ≤ Expr.denote ctx rhs

Proof state:
case neg
ctx : Context
eq : Bool
lhs rhs : Expr
h : ¬eq = true
⊢ Poly.denote_le ctx (lhs.toNormPoly, rhs.toNormPoly) ↔ Expr.denote ctx lhs ≤ Expr.denote ctx rhs

Tactic:
simp [Poly.denote_le, Expr.toNormPoly, Poly.norm]

Result:
no goals

Proof state:
case pos
ctx : Context
eq : Bool
lhs rhs : Expr
h : eq = true
⊢ Poly.denote_eq ctx (lhs.toNormPoly, rhs.toNormPoly) ↔ Expr.denote ctx lhs = Expr.denote ctx rhs

Tactic:
simp [Poly.denote_eq, Expr.toNormPoly, Poly.norm]

Result:
no goals

Proof state:
ctx : Context
c : ExprCnstr
⊢ PolyCnstr.denote ctx c.toNormPoly = denote ctx c

Tactic:
cases c

Result:
case mk
ctx : Context
eq✝ : Bool
lhs✝ rhs✝ : Expr
⊢ PolyCnstr.denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }.toNormPoly =
    denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }