## Stream: new members

### Topic: rw duplicates an hypothesis

#### Riccardo Brasca (Nov 22 2020 at 15:37):

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 (Nov 22 2020 at 15:44):

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

#### Kevin Buzzard (Nov 22 2020 at 15:44):

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

#### Yakov Pechersky (Nov 22 2020 at 15:48):

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

#### Filippo A. E. Nuccio (Nov 22 2020 at 15:48):

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

#### Riccardo Brasca (Nov 22 2020 at 15:49):

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 (Nov 22 2020 at 15:51):

and how do you close the goal, finally?

#### Kevin Buzzard (Nov 22 2020 at 15:51):

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 (Nov 22 2020 at 15:52):

@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 (Nov 22 2020 at 15:52):

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 (Nov 22 2020 at 15:53):

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 (Nov 22 2020 at 15:55):

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

#### Riccardo Brasca (Nov 22 2020 at 15:56):

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 (Nov 22 2020 at 15:57):

Nothing wrong with having another h

#### Kevin Buzzard (Nov 22 2020 at 15:58):

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

#### Filippo A. E. Nuccio (Nov 22 2020 at 15:59):

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 (Nov 22 2020 at 15:59):

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

#### Kevin Buzzard (Nov 22 2020 at 15:59):

You should maybe rewrite at h |-

#### Yakov Pechersky (Nov 22 2020 at 16:00):

You'll also need to rw at hpos

#### Riccardo Brasca (Nov 22 2020 at 16:14):

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 (Nov 22 2020 at 16:16):

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

#### Riccardo Brasca (Nov 22 2020 at 16:19):

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 (Nov 22 2020 at 16:19):

Ah, I see now.

Last updated: May 16 2021 at 21:11 UTC