# Zulip Chat Archive

## 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