X = monomial 1 1 required rw explicitly?

Stream: new members

[Shanghe Chen]

Hi in the following code why is rw [eq1] necessary? The equation can be proved by rfl. But if it’s omitted, rw [monomial_mul_monomial] does not work.

import Mathlib
open Polynomial
variable (R : Type) [Ring R]
#check monomial 1 (1: R)

example:  monomial 1 (1: R) = X := by
  rfl

example:X*X=(X^2:R[X]) := by
  let eq1 : X = monomial 1 (1:R) := by rfl
  rw [eq1]
  rw [monomial_mul_monomial]
  -- let h:= monomial_mul_monomial 1 1 (1:R) (1:R)
  -- rw [h]
  simp

[Jireh Loreaux]

Because docs#Polynomial.X is defeq (at default transparency) to docs#Polynomial.monomial 1 (1 : R), but not at reducible transparency, which is the transparency at which rw operates.

[Jireh Loreaux]

You can see this because

example : monomial 1 (1 : R) = X := by
  with_reducible rfl -- fails

[Jireh Loreaux]

rw [monomial_mul_monomial] looks for monomial but doesn't see it, because it doesn't see through the definition of X.

[Jireh Loreaux]

However, you don't need to write eq1 itself, you can just use: docs#Polynomial.monomial_one_one_eq_X

[Shanghe Chen]

Oh thanks for pointing out the difference of transparencies and the theorem. I didn’t realize it exists in Mathlib!

[Shanghe Chen]

I find that Mario's answer in what-is-the-precise-meaning-of-reducible explains the difference in detail too