-- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
lemma mem_image_comap_C_basicOpen (f : MvPolynomial σ R) (x : PrimeSpectrum R) :
    x ∈ comap (C (σ := σ)) '' basicOpen f ↔ ∃ i, f.coeff i ∉ x.asIdeal

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ x ∈ ⇑(comap C) '' ↑(basicOpen f) ↔ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0

Tactic:
refine (mem_image_comap_basicOpen _ _).trans (not_iff_not.mpr ?_)

Result:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ IsNilpotent ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) f) ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0

Proof state:
case a.h.e'_2.h.e'_5.hX.a
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝ (((↑e).comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField))) (X i✝)) =
    coeff m✝ ((map (algebraMap R x.asIdeal.ResidueField)) (X i✝))

Tactic:
simp [e, monomial_one_one_eq_X, scalarRTensorAlgEquiv, coeff_map, coeff_X']

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ x ∈ ⇑(comap C) '' ↑(basicOpen f) ↔ ∃ i, coeff i f ∉ x.asIdeal

Tactic:
trans f.map (algebraMap R x.asIdeal.ResidueField) ≠ 0

Result:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ x ∈ ⇑(comap C) '' ↑(basicOpen f) ↔ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0

R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0 ↔ ∃ i, coeff i f ∉ x.asIdeal

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
⊢ e ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) f) = 0 ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0

Tactic:
show (e.toAlgHom.toRingHom).comp (algebraMap _ _) f = 0 ↔ MvPolynomial.map _ f = 0

Result:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
⊢ ((↑e).comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField))) f = 0 ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
⊢ IsNilpotent ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) f) ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0

Tactic:
rw [← IsNilpotent.map_iff e.injective, isNilpotent_iff_eq_zero]

Result:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
⊢ e ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) f) = 0 ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0 ↔ ∃ i, coeff i f ∉ x.asIdeal

Tactic:
simp [MvPolynomial.ext_iff, coeff_map]

Result:
no goals

Proof state:
case a.h.e'_2.h.e'_5.hC.a.a
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
x✝ : R
m✝ : σ →₀ ℕ
⊢ coeff m✝ ((((↑e).comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField))).comp C) x✝) =
    coeff m✝ (((map (algebraMap R x.asIdeal.ResidueField)).comp C) x✝)

Tactic:
simp [scalarRTensorAlgEquiv, e, coeff_map,
  Algebra.smul_def, apply_ite (f := algebraMap _ _)]

Result:
no goals

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
⊢ ((↑e).comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField))) f = 0 ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0

Tactic:
congr!

Result:
case a.h.e'_2.h.e'_5
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
⊢ (↑e).comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) =
    map (algebraMap R x.asIdeal.ResidueField)

Proof state:
case a.h.e'_2.h.e'_5
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
⊢ (↑e).comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) =
    map (algebraMap R x.asIdeal.ResidueField)

Tactic:
ext

Result:
case a.h.e'_2.h.e'_5.hC.a.a
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
x✝ : R
m✝ : σ →₀ ℕ
⊢ coeff m✝ ((((↑e).comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField))).comp C) x✝) =
    coeff m✝ (((map (algebraMap R x.asIdeal.ResidueField)).comp C) x✝)

case a.h.e'_2.h.e'_5.hX.a
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝ (((↑e).comp (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField))) (X i✝)) =
    coeff m✝ ((map (algebraMap R x.asIdeal.ResidueField)) (X i✝))

Proof state:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ IsNilpotent ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) f) ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0

Tactic:
let e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R]
    MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv

Result:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] MvPolynomial σ x.asIdeal.ResidueField := scalarRTensorAlgEquiv
⊢ IsNilpotent ((algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) f) ↔
    (map (algebraMap R x.asIdeal.ResidueField)) f = 0