How to pass cleanly through an equiv

Stream: general

[Bolton Bailey]

My state has a polynomial p: MvPolynomial (Fin (Nat.succ n)) F in it. I would like to be able to do

import Mathlib.Data.MvPolynomial.Equiv

lemma schwartz_zippel (F : Type) [CommRing F] (n : ℕ)
    (p : MvPolynomial (Fin (n + 1)) F) (hp : p ≠ 0) : p = 0 := by
  have p_eq : p = (MvPolynomial.finSuccEquiv F n).symm (MvPolynomial.finSuccEquiv F n p) := by
      rw [AlgEquiv.symm_apply_apply]
  rw [p_eq] at hp ⊢
  -- Call this polynomial p'
  set p' : Polynomial (MvPolynomial (Fin n) F) := MvPolynomial.finSuccEquiv F n p
  clear p_eq p

But at the end I get

tactic 'clear' failed, variable 'p'' depends on 'p'

Is there a way I can pass through the equiv and then clear p?

[Eric Wieser]

Can you make a #mwe?

[Bolton Bailey]

Sure, one sec

[Bolton Bailey]

Ok, it is a #mwe now

[Bolton Bailey]

Basically, I don't care that p' is defined based off of p since for the rest of the proof I only deal with p', so I would like to forget p, replace every reference to it with a reference to p' and then remove the clutter from the state.

[Alex J. Best]

Is this what you want?

import Mathlib.Data.MvPolynomial.Equiv

lemma schwartz_zippel (F : Type) [CommRing F] (n : ℕ)
    (p : MvPolynomial (Fin (n + 1)) F) (hp : p ≠ 0) : p = 0 := by
  have p_eq : p = (MvPolynomial.finSuccEquiv F n).symm (MvPolynomial.finSuccEquiv F n p) := by
      rw [AlgEquiv.symm_apply_apply]
  rw [p_eq] at hp ⊢
  -- Call this polynomial p'
  set p' : Polynomial (MvPolynomial (Fin n) F) := MvPolynomial.finSuccEquiv F n p
  clear_value p'
  clear p_eq p
  simp at *

[Bolton Bailey]

Yes! Thanks

[Eric Wieser]

Does this do what you want?

lemma schwartz_zippel (F : Type) [CommRing F] (n : ℕ)
    (p : MvPolynomial (Fin (n + 1)) F) (hp : p ≠ 0) : p = 0 := by
  revert p
  rw [(MvPolynomial.finSuccEquiv F n).symm.surjective.forall]
  intro p' hp'
  simp only [AddEquivClass.map_eq_zero_iff, AddEquivClass.map_ne_zero_iff] at hp' ⊢

[Eric Rodriguez]

docs#Function.Surjective.forall