unable to rw

Stream: new members

[Damiano Testa]

Dear All,

I am trying to prove the lemma below, but I cannot get rw, simp_rw and conv to do what I would expect them to. What am I doing wrong?

Thank you very much!

import data.polynomial.degree.basic

open polynomial

lemma fac {R : Type*} [integral_domain R] {n : ℕ} {f g : polynomial R} {h : X^n = f*g} : (X ^ n).coeff (f.nat_degree+g.nat_degree) ≠ 0 :=
begin
--  simp_rw h, --simplify tactic failed to simplify
  conv_lhs {congr,rw h,}, --rewrite tactic failed, did not find instance of the pattern in the target expression
--  X ^ n
end

[Kevin Buzzard]

If you just click on the X^n's in the infoview you'll see that one is in R[X] and the other is in N[X] so they don't unify

[Damiano Testa]

Aaaahh!!! Thanks!!

[Kevin Buzzard]

even better, you can click on the X's

[Damiano Testa]

Indeed! I had clicked on X^n and failed to spot the difference... Thank you very much!

[Damiano Testa]

For the record, below is the statement that has a chance of being true!

lemma fac {R : Type*} [integral_domain R] {n : ℕ} {f g : polynomial R} {h : X^n = f*g} : ((X:polynomial R) ^ n).coeff (f.nat_degree+g.nat_degree) ≠ 0 :=
begin
  rw h,
  sorry,
end