ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
this : Poly.denote_eq ctx (Poly.cancel (toNormPoly a) (toNormPoly b)) = Poly.denote_eq ctx (toNormPoly a, toNormPoly b)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)
ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)
have := Poly.denote_eq_cancel_eq ctx a.toNormPoly b.toNormPoly
ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
this : Poly.denote_eq ctx (toPoly c, toPoly d) = Poly.denote_eq ctx (toNormPoly a, toNormPoly b)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)
ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
this : Poly.denote_eq ctx (Poly.cancel (toNormPoly a) (toNormPoly b)) = Poly.denote_eq ctx (toNormPoly a, toNormPoly b)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)
rw [h] at this
ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
this : (denote ctx c = denote ctx d) = (denote ctx a = denote ctx b)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)
ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
this : Poly.denote_eq ctx (toPoly c, toPoly d) = Poly.denote_eq ctx (toNormPoly a, toNormPoly b)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)
simp [toNormPoly, Poly.norm, Poly.denote_eq] at this
no goals
ctx : Context
a b c d : Expr
h : Poly.cancel (toNormPoly a) (toNormPoly b) = (toPoly c, toPoly d)
this : (denote ctx c = denote ctx d) = (denote ctx a = denote ctx b)
⊢ (denote ctx a = denote ctx b) = (denote ctx c = denote ctx d)
exact this.symm