case mk
ctx : Context
eq✝ : Bool
lhs✝ rhs✝ : Expr
⊢ PolyCnstr.denote ctx (toNormPoly { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }) =
    denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }
ctx : Context
c : ExprCnstr
⊢ PolyCnstr.denote ctx (toNormPoly c) = denote ctx c
cases c
case mk
ctx : Context
eq : Bool
lhs rhs : Expr
⊢ PolyCnstr.denote ctx (toNormPoly { eq := eq, lhs := lhs, rhs := rhs }) =
    denote ctx { eq := eq, lhs := lhs, rhs := rhs }
case mk
ctx : Context
eq✝ : Bool
lhs✝ rhs✝ : Expr
⊢ PolyCnstr.denote ctx (toNormPoly { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }) =
    denote ctx { eq := eq✝, lhs := lhs✝, rhs := rhs✝ }
rename_i eq lhs rhs
case mk
ctx : Context
eq : Bool
lhs rhs : Expr
⊢ (bif eq then
      Poly.denote_eq ctx
        ((Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).fst,
          (Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).snd)
    else
      Poly.denote_le ctx
        ((Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).fst,
          (Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).snd)) =
    bif eq then Expr.denote ctx lhs = Expr.denote ctx rhs else Expr.denote ctx lhs ≤ Expr.denote ctx rhs
case mk
ctx : Context
eq : Bool
lhs rhs : Expr
⊢ PolyCnstr.denote ctx (toNormPoly { eq := eq, lhs := lhs, rhs := rhs }) =
    denote ctx { eq := eq, lhs := lhs, rhs := rhs }
simp [ExprCnstr.denote, PolyCnstr.denote, ExprCnstr.toNormPoly]
case mk.inl
ctx : Context
eq : Bool
lhs rhs : Expr
h : eq = true
⊢ Poly.denote_eq ctx
      ((Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).fst,
        (Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).snd) =
    (Expr.denote ctx lhs = Expr.denote ctx rhs)

case mk.inr
ctx : Context
eq : Bool
lhs rhs : Expr
h : ¬eq = true
⊢ Poly.denote_le ctx
      ((Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).fst,
        (Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).snd) =
    (Expr.denote ctx lhs ≤ Expr.denote ctx rhs)
case mk
ctx : Context
eq : Bool
lhs rhs : Expr
⊢ (bif eq then
      Poly.denote_eq ctx
        ((Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).fst,
          (Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).snd)
    else
      Poly.denote_le ctx
        ((Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).fst,
          (Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).snd)) =
    bif eq then Expr.denote ctx lhs = Expr.denote ctx rhs else Expr.denote ctx lhs ≤ Expr.denote ctx rhs
by_cases h : eq = true <;> simp [h]
case mk.inl
ctx : Context
eq : Bool
lhs rhs : Expr
h : eq = true
⊢ Poly.denote_eq ctx (Expr.toNormPoly lhs, Expr.toNormPoly rhs) = (Expr.denote ctx lhs = Expr.denote ctx rhs)
case mk.inl
ctx : Context
eq : Bool
lhs rhs : Expr
h : eq = true
⊢ Poly.denote_eq ctx
      ((Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).fst,
        (Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).snd) =
    (Expr.denote ctx lhs = Expr.denote ctx rhs)
rw [Poly.denote_eq_cancel_eq]
no goals
case mk.inl
ctx : Context
eq : Bool
lhs rhs : Expr
h : eq = true
⊢ Poly.denote_eq ctx (Expr.toNormPoly lhs, Expr.toNormPoly rhs) = (Expr.denote ctx lhs = Expr.denote ctx rhs)
simp [Poly.denote_eq, Expr.toNormPoly, Poly.norm]
case mk.inr
ctx : Context
eq : Bool
lhs rhs : Expr
h : ¬eq = true
⊢ Poly.denote_le ctx (Expr.toNormPoly lhs, Expr.toNormPoly rhs) = (Expr.denote ctx lhs ≤ Expr.denote ctx rhs)
case mk.inr
ctx : Context
eq : Bool
lhs rhs : Expr
h : ¬eq = true
⊢ Poly.denote_le ctx
      ((Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).fst,
        (Poly.cancel (Expr.toNormPoly lhs) (Expr.toNormPoly rhs)).snd) =
    (Expr.denote ctx lhs ≤ Expr.denote ctx rhs)
rw [Poly.denote_le_cancel_eq]
no goals
case mk.inr
ctx : Context
eq : Bool
lhs rhs : Expr
h : ¬eq = true
⊢ Poly.denote_le ctx (Expr.toNormPoly lhs, Expr.toNormPoly rhs) = (Expr.denote ctx lhs ≤ Expr.denote ctx rhs)
simp [Poly.denote_le, Expr.toNormPoly, Poly.norm]