ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (cancel m₁ m₂)
⊢ denote_eq ctx (m₁, m₂)
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (cancel m₁ m₂)
⊢ denote_eq ctx (m₁, m₂)
simp at h
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (cancel m₁ m₂)
this : denote_eq ctx (List.reverse [] ++ m₁, List.reverse [] ++ m₂)
⊢ denote_eq ctx (m₁, m₂)
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (cancel m₁ m₂)
⊢ denote_eq ctx (m₁, m₂)
have := Poly.of_denote_eq_cancelAux (h := h)
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (cancel m₁ m₂)
this : denote_eq ctx (m₁, m₂)
⊢ denote_eq ctx (m₁, m₂)
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (cancel m₁ m₂)
this : denote_eq ctx (List.reverse [] ++ m₁, List.reverse [] ++ m₂)
⊢ denote_eq ctx (m₁, m₂)
simp at this
no goals
ctx : Context
m₁ m₂ : Poly
h : denote_eq ctx (cancel m₁ m₂)
this : denote_eq ctx (m₁, m₂)
⊢ denote_eq ctx (m₁, m₂)
assumption