-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk
    {R : Type*} [CommRing R] (c : R) :
    letI := (mapRingHom (algebraMap R (Away c))).toAlgebra
    (range (comap (algebraMap R[X] (Away c)[X])))ᶜ
      = range (comap (mapRingHom (Ideal.Quotient.mk (.span {c}))))

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.powers (C c)) (Away c)[X]
surj : Function.Surjective ⇑(mapRingHom (Ideal.Quotient.mk (Ideal.span {c})))
⊢ (↑(basicOpen (C c)))ᶜ = zeroLocus ↑(RingHom.ker (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Tactic:
simp [Polynomial.ker_mapRingHom, Ideal.map_span]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
this : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
⊢ (range ⇑(comap (algebraMap R[X] (Away c)[X])))ᶜ = range ⇑(comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Tactic:
have := Polynomial.isLocalization (.powers c) (Away c)

Result:
R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.map C (Submonoid.powers c)) (Away c)[X]
⊢ (range ⇑(comap (algebraMap R[X] (Away c)[X])))ᶜ = range ⇑(comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.powers (C c)) (Away c)[X]
⊢ (range ⇑(comap (algebraMap R[X] (Away c)[X])))ᶜ = range ⇑(comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Tactic:
have surj : Function.Surjective (mapRingHom (Ideal.Quotient.mk (.span {c}))) :=
  Polynomial.map_surjective _ Ideal.Quotient.mk_surjective

Result:
R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.powers (C c)) (Away c)[X]
surj : Function.Surjective ⇑(mapRingHom (Ideal.Quotient.mk (Ideal.span {c})))
⊢ (range ⇑(comap (algebraMap R[X] (Away c)[X])))ᶜ = range ⇑(comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.powers (C c)) (Away c)[X]
surj : Function.Surjective ⇑(mapRingHom (Ideal.Quotient.mk (Ideal.span {c})))
⊢ (range ⇑(comap (algebraMap R[X] (Away c)[X])))ᶜ = range ⇑(comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Tactic:
rw [range_comap_of_surjective _ _ surj, localization_away_comap_range _ (C c)]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.powers (C c)) (Away c)[X]
surj : Function.Surjective ⇑(mapRingHom (Ideal.Quotient.mk (Ideal.span {c})))
⊢ (↑(basicOpen (C c)))ᶜ = zeroLocus ↑(RingHom.ker (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.map C (Submonoid.powers c)) (Away c)[X]
⊢ (range ⇑(comap (algebraMap R[X] (Away c)[X])))ᶜ = range ⇑(comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Tactic:
rw [Submonoid.map_powers] at this

Result:
R : Type u_1
inst✝ : CommRing R
c : R
this✝ : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
this : IsLocalization (Submonoid.powers (C c)) (Away c)[X]
⊢ (range ⇑(comap (algebraMap R[X] (Away c)[X])))ᶜ = range ⇑(comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
⊢ (range ⇑(comap (algebraMap R[X] (Away c)[X])))ᶜ = range ⇑(comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))

Tactic:
letI := (mapRingHom (algebraMap R (Away c))).toAlgebra

Result:
R : Type u_1
inst✝ : CommRing R
c : R
this : Algebra R[X] (Away c)[X] := (mapRingHom (algebraMap R (Away c))).toAlgebra
⊢ (range ⇑(comap (algebraMap R[X] (Away c)[X])))ᶜ = range ⇑(comap (mapRingHom (Ideal.Quotient.mk (Ideal.span {c}))))