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

Proof state:
case a.h.e'_2.h.e'_5.h₁
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ ((↑e).comp (algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField))).comp C =
    (mapRingHom (algebraMap R x.asIdeal.ResidueField)).comp C

Tactic:
ext

Result:
case a.h.e'_2.h.e'_5.h₁.a.a
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
x✝ : R
n✝ : ℕ
⊢ ((((↑e).comp (algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField))).comp C) x✝).coeff n✝ =
    (((mapRingHom (algebraMap R x.asIdeal.ResidueField)).comp C) x✝).coeff n✝

Proof state:
case a.h.e'_2.h.e'_5.h₁.a.a
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
x✝ : R
n✝ : ℕ
⊢ ((((↑e).comp (algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField))).comp C) x✝).coeff n✝ =
    (((mapRingHom (algebraMap R x.asIdeal.ResidueField)).comp C) x✝).coeff n✝

Tactic:
simp [e]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R[X]
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_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ IsNilpotent ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) f) ↔ map (algebraMap R x.asIdeal.ResidueField) f = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ IsNilpotent ((algebraMap R[X] (R[X] ⊗[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_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ e ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) f) = 0 ↔ map (algebraMap R x.asIdeal.ResidueField) f = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ e ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) f) = 0 ↔ map (algebraMap R x.asIdeal.ResidueField) f = 0

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

Result:
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ ((↑e).comp (algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField))) f = 0 ↔
    (mapRingHom (algebraMap R x.asIdeal.ResidueField)) f = 0

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

Tactic:
simp [Polynomial.ext_iff]

Result:
no goals

Proof state:
case a.h.e'_2.h.e'_5.h₂
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ ((↑e).comp (algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField))) X =
    (mapRingHom (algebraMap R x.asIdeal.ResidueField)) X

Tactic:
simp [e, monomial_one_one_eq_X]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ ((↑e).comp (algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField))) f = 0 ↔
    (mapRingHom (algebraMap R x.asIdeal.ResidueField)) f = 0

Tactic:
congr!

Result:
case a.h.e'_2.h.e'_5
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ (↑e).comp (algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) = mapRingHom (algebraMap R x.asIdeal.ResidueField)

Proof state:
case a.h.e'_2.h.e'_5
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ (↑e).comp (algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) = mapRingHom (algebraMap R x.asIdeal.ResidueField)

Tactic:
ext1

Result:
case a.h.e'_2.h.e'_5.h₁
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ ((↑e).comp (algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField))).comp C =
    (mapRingHom (algebraMap R x.asIdeal.ResidueField)).comp C

case a.h.e'_2.h.e'_5.h₂
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ ((↑e).comp (algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField))) X =
    (mapRingHom (algebraMap R x.asIdeal.ResidueField)) X

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

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

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

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

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

Tactic:
let e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R _ _).trans (polyEquivTensor R x.asIdeal.ResidueField).symm

Result:
R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
e : R[X] ⊗[R] x.asIdeal.ResidueField ≃ₐ[R] x.asIdeal.ResidueField[X] :=
  (Algebra.TensorProduct.comm R R[X] x.asIdeal.ResidueField).trans (polyEquivTensor R x.asIdeal.ResidueField).symm
⊢ IsNilpotent ((algebraMap R[X] (R[X] ⊗[R] x.asIdeal.ResidueField)) f) ↔ map (algebraMap R x.asIdeal.ResidueField) f = 0