Constructing a proof for Polynomial.IsRoot

Stream: mathlib4

[Ryan Ziegler]

I'd like to prove the following simple theorem:

theorem T : (∃ x : ℝ, (Polynomial.IsRoot (X^2 - 1) x)) :=

I cannot find how to even approach this, anywhere! It should be so simple! I've figured out that I need to do as a proof something along the lines of

Exists.intro 1 (a proof that 1 is a root)

But I can't figure out what to do to make the proof. I've tried:

have h : Polynomial.IsRoot (X^2 - 1) 1 := Polynomial.eval (X^2 - 1) 1 = 0

and using h as the proof but this doesn't work. How do I construct a proof for Polynomial.IsRoot? Thanks!

[Jireh Loreaux]

Does by simp work to prove h?

[Kyle Miller]

Polynomial.eval (X^2 - 1) 1 = 0 is a proposition, not a proof, which is why that doesn't work.

Does this work?

have h : Polynomial.IsRoot (X^2 - 1) 1 := by simp

[Kevin Buzzard]

import Mathlib.Tactic

open Polynomial

theorem T : (∃ x : ℝ, (Polynomial.IsRoot (X^2 - 1) x)) := by
  use 1
  simp

[Jireh Loreaux]

:racecar:

[Ryan Ziegler]

simp does not work in h:

unsolved goals
X: Polynomial ℝ
⊢ Polynomial.eval 1 X ^ 2 - 1 = 0

but use 1, simp works, thank you!!

[Ryan Ziegler]

Out of curiosity, is there a way to do this with Exists.intro?

[Kevin Buzzard]

theorem T : (∃ x : ℝ, (Polynomial.IsRoot (X^2 - 1) x)) := by
  apply Exists.intro 1
  simp

[Kyle Miller]

(note that use 1 is equivalent to apply Exists.intro 1. the use tactic is a convenient way to apply a constructor without needing to know its name while also passing in some arguments)

[Ryan Ziegler]

Turns out my editor width wasn't wide enough and I missed an underline on by, use 1, simp and the apply both don't work, and still have the same unsolved goal I pasted above

[Kyle Miller]

Are you pasting in the exact code that Kevin gave, or are you switching it to use possibly incorrect syntax? I notice you have a , in what you just said, which isn't correct in Lean 4

[Ryan Ziegler]

I copy-pasted exactly.

[Ryan Ziegler]

Although I notice I don't have the import Mathlib.Tactic import if that would make a difference... My imports are rebuilding now

[Kyle Miller]

Was the error you were getting "unknown tactic" by chance? There's a chance also that somehow one of the tactics is importing necessary simp lemmas.

[Jireh Loreaux]

Note also, the reason that by simp didn't work for h was not because the proof was invalid, but because the claim didn't elaborate. This works once you specify the kind of polynomial you want with ℝ[X]:

import Mathlib.Tactic

open Polynomial

example : (∃ x : ℝ, (Polynomial.IsRoot (X ^ 2 - 1) x)) := by
  have h : Polynomial.IsRoot (X ^ 2 - 1 : ℝ[X]) 1 := by simp
  use 1

[Kyle Miller]

Oh, that's a good gotcha. You can also write have h : Polynomial.IsRoot (X ^ 2 - 1) (1 : ℝ) := by simp

[Ryan Ziegler]

Ah it appears just adding import Mathlib.Tactic adds enough to simp that the first things people sent work too

[Ryan Ziegler]

Thanks for the help!