rw duplicates an hypothesis

Stream: new members

[Riccardo Brasca]

In the following example

import ring_theory.roots_of_unity
import field_theory.minimal_polynomial

variables {K : Type*} [field K] {n : ℕ} {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n)

open polynomial

include n μ h hpos

lemma primitive_root_is_integral : is_integral ℤ μ := sorry

lemma test (hn : n = 1) : minimal_polynomial (primitive_root_is_integral h hpos) = X - 1 :=
begin
  rw hn at h, --it creates another h
  simp at h, --now the second h is μ = 1
  sorry,
end

when I use rw hn at h, it creates a new hypothesis h, keeping also the old one. I think because h is hidden in the goal, that is displayed as minimal_polynomial _ = X - 1. In any case I don't know how to use this, rw h doesn't work. I also created a new hypothesis muone : μ = 1 to be sure that I am using the correct one, but rw muone says

rewrite tactic failed, motive is not type correct
  λ (_a : K), minimal_polynomial _ = X - 1 = (minimal_polynomial _ = X - 1)

How can I use that μ = 1? Thank you!

Note that I know how to prove that the minimal polynomial of 1 : K is X - 1, that's not the problem.

[Kevin Buzzard]

subst hn might work, as might simp [hn] at *. But they might not (I'm not at a computer right now)

[Kevin Buzzard]

You're right that lean demands that h is preserved because it's in the goal

[Yakov Pechersky]

when you get that motive error, simplest work around is to use simp_rw

[Filippo A. E. Nuccio]

So what you want to prove is that the minimal polynomial of the $1$-st root of unity is X-1 right?

[Riccardo Brasca]

subst does exactly what I want, thank you @Kevin Buzzard ! I have to understand what is the difference between rw and subs...

[Filippo A. E. Nuccio]

and how do you close the goal, finally?

[Kevin Buzzard]

subst hn says "completely rip out n from the entire local context all in one go and replace all occurrences with 1". rw hn at h rewrites only at h, and then tries to clear the old h but the clear fails because h is still being used somewhere.

[Riccardo Brasca]

@Filippo A. E. Nuccio The point is that I need to prove it stated like that (it is indeed one step in a more interesting lemma, and morally the easy step, I was surprised to get stuck on it).

[Filippo A. E. Nuccio]

Riccardo Brasca said:

Filippo A. E. Nuccio The point is that I need to prove it stated like that (it is indeed one step in a more interesting lemma, and morally the easy step, I was surprised to get stuck on it).

Yes, yes, I got that: I was trying to understand the statement. But I got that your point was about rw versus subst. At any rate, how do you finish with @Kevin Buzzard 's suggestion?

[Kevin Buzzard]

Yakov's suggestion works in situations where the subst trick doesn't, because the subst trick only works if the hypothesis is <variable> = ... or ... = <variable>

[Riccardo Brasca]

simp_rw hn at h has the same effect as rw hn at h, it creates another h.

[Riccardo Brasca]

simp_rw muone indeed does not give any error, and the goal becomes minimal_polynomial _ = X - 1. If I go on the underscore VS Code says λ {x : K}, is_integral ℤ x, that confuses me...

[Yakov Pechersky]

Nothing wrong with having another h

[Kevin Buzzard]

The simplified h will be after the unsimplified one, so it will be the one lean uses in rewrites etc

[Filippo A. E. Nuccio]

Riccardo Brasca said:

simp_rw muone indeed does not give any error, and the goal becomes minimal_polynomial _ = X - 1. If I go on the underscore VS Code says λ {x : K}, is_integral ℤ x, that confuses me...

This happened also with your code, no? Well, at least the first part

[Yakov Pechersky]

You can also make a new hypothesis with "have newh : is_primitive_root mu 1 := by..."

[Kevin Buzzard]

You should maybe rewrite at h |-

[Yakov Pechersky]

You'll also need to rw at hpos

[Riccardo Brasca]

Maybe I am confused, but it seems that subst is the only way I found to make μ disappears (replaced by 1) from the goal.

import ring_theory.roots_of_unity
import field_theory.minimal_polynomial

variables {K : Type*} [field K] {n : ℕ} {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n)

open polynomial

include n μ h hpos

lemma primitive_root_is_integral : is_integral ℤ μ := sorry

lemma test (hn : n = 1) : minimal_polynomial (primitive_root_is_integral h hpos) = X - 1 :=
begin
  have muone : μ = 1 := sorry,
--  simp_rw muone, --goal says λ {x : K}, is_integral ℤ x
--  subst muone, --goal says is_integral ℤ 1
end

[Filippo A. E. Nuccio]

But how do you intend to prove the result? I still haven't understood the problem with two h

[Riccardo Brasca]

The two h was not a real problem, just something looked weird to me. Once the goal becomes to prove that the minimal polynomial of 1 is X - 1 it's OK, see #5062. The problem was that I wasn't able to modify the goal, even knowing μ = 1, the goal was still about the minimal polynomial of μ.

[Filippo A. E. Nuccio]

Ah, I see now.