-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma range_glueDataObjι (U : X.affineOpens) :
    Set.range (I.glueDataObjι U).base =
      U.2.isoSpec.inv.base '' PrimeSpectrum.zeroLocus (I.ideal U)

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) ''
      Set.range ⇑(ConcreteCategory.hom (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base) =
    (fun a => (ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
erw [range_comap_of_surjective]

Result:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) ''
      PrimeSpectrum.zeroLocus ↑(RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))) =
    (fun a => (ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

case hf
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))

Proof state:
case hf
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))

Tactic:
exact Ideal.Quotient.mk_surjective

Result:
no goals

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Set.range ⇑(ConcreteCategory.hom (I.glueDataObjι U).base) =
    ⇑(ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
simp only [glueDataObjι, Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp,
  SetLike.coe_sort_coe]

Result:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) ''
      Set.range ⇑(ConcreteCategory.hom (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base) =
    (fun a => (ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) ''
      PrimeSpectrum.zeroLocus ↑(RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))) =
    (fun a => (ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

case hf
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))

Tactic:
swap

Result:
case hf
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))

X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) ''
      PrimeSpectrum.zeroLocus ↑(RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))) =
    (fun a => (ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) ''
      PrimeSpectrum.zeroLocus ↑(RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))) =
    (fun a => (ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
simp only [Ideal.mk_ker, CommRingCat.hom_ofHom]

Result:
no goals