awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
⊢ IsClosedImmersion (X := X.irreducibleComponent Z hZ) (X.irreducibleComponentι Z hZ)

Tactic:
inferInstanceAs (IsClosedImmersion (X.irreducibleComponentIdeal Z hZ).subschemeι)

Premises used: _private.0.AlgebraicGeometry.Scheme.instIsClosedImmersionIrreducibleComponentι._proof_1
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
⊢ IrreducibleSpace.{u} ↥(X.irreducibleComponent Z hZ)

Tactic:
Subtype.irreducibleSpace hZ.1

Premises used: Subtype.irreducibleSpace, And.left
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
⊢ Z = Set.univ

Tactic:
rw [irreducibleComponents_eq_singleton, Set.mem_singleton_iff] at hZ

Premises used: irreducibleComponents_eq_singleton, Set.mem_singleton_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
hZ₁ : Z = Set.univ
⊢ IsNoetherian X

Tactic:
rw [irreducibleComponents_eq_singleton, Set.mem_singleton_iff] at hZ

Premises used: irreducibleComponents_eq_singleton, Set.mem_singleton_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst_1 : IsNoetherian X
inst_2 : IrreducibleSpace.{u} ↥X
hZ₁ : Z = Set.univ
inst : IsNoetherian X
⊢ IrreducibleSpace.{u} ↥X

Tactic:
rw [irreducibleComponents_eq_singleton, Set.mem_singleton_iff] at hZ

Premises used: irreducibleComponents_eq_singleton, Set.mem_singleton_iff
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Z = Set.univ
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
⊢ X.irreducibleComponentOpen Z = ⊤

Tactic:
simp [irreducibleComponentOpen, irreducibleComponents_eq_singleton, hZ]

Premises used: irreducibleComponents_eq_singleton, AlgebraicGeometry.Scheme.irreducibleComponentOpen
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
rw : CategoryTheory.IsIso.{u, u + 1} (X := (↑⊤ : Scheme)) (Opens.ι ⊤)
⊢ CategoryTheory.IsIso (X.irreducibleComponentOpen Z).ι

Tactic:
rw [irreducibleComponentOpen_eq_top X Z hZ]

Premises used: AlgebraicGeometry.Scheme.irreducibleComponentOpen_eq_top
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
⊢ CategoryTheory.IsIso.{u, u + 1} (X := (↑⊤ : Scheme)) (Opens.ι ⊤)

Tactic:
X.topIso.isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, AlgebraicGeometry.Scheme.ofRestrict, AlgebraicGeometry.Scheme.topIso, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
⊢ CategoryTheory.IsIso.{u, u + 1} (X := (↑⊤ : Scheme)) (Opens.ι ⊤)

Tactic:
exact X.topIso.isIso_hom

Premises used: CategoryTheory.Iso.isIso_hom, AlgebraicGeometry.Scheme.topIso
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
⊢ CategoryTheory.IsIso (X.irreducibleComponentOpen Z).ι

Tactic:
have : CategoryTheory.IsIso (irreducibleComponentOpen X Z).ι := by
    rw [irreducibleComponentOpen_eq_top X Z hZ]
    exact X.topIso.isIso_hom
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
this : CategoryTheory.IsIso (X.irreducibleComponentOpen Z).ι
rw : Eq.{u + 1} (α := X.IdealSheafData) (Hom.ker (X := (↑⊤ : Scheme)) (Opens.ι ⊤)) ⊥
⊢ CategoryTheory.IsIso (X := X.irreducibleComponent Z hZ) (X.irreducibleComponentι Z hZ)

Tactic:
rw [irreducibleComponentι, isIso_subschemeι_iff_eq_bot, irreducibleComponentIdeal_def,
    irreducibleComponentOpen_eq_top X Z hZ]

Premises used: AlgebraicGeometry.Scheme.irreducibleComponentOpen_eq_top, AlgebraicGeometry.Scheme.irreducibleComponentIdeal_def, AlgebraicGeometry.Scheme.isIso_subschemeι_iff_eq_bot, AlgebraicGeometry.Scheme.irreducibleComponentι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
this : CategoryTheory.IsIso (X.irreducibleComponentOpen Z).ι
⊢ Eq.{u + 1} (α := X.IdealSheafData) (Hom.ker (X := (↑⊤ : Scheme)) (Opens.ι ⊤)) ⊥

Tactic:
X.topIso.hom.ker_eq_bot_of_isIso

Premises used: AlgebraicGeometry.Scheme.Hom.ker_eq_bot_of_isIso, AlgebraicGeometry.Scheme.ofRestrict, AlgebraicGeometry.Scheme.topIso, AlgebraicGeometry.Scheme.Opens.ι, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
Goal:
X : Scheme
Z : Set ↥X
hZ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X) Z
inst : IsNoetherian X
inst_1 : IrreducibleSpace.{u} ↥X
this : CategoryTheory.IsIso (X.irreducibleComponentOpen Z).ι
⊢ Eq.{u + 1} (α := X.IdealSheafData) (Hom.ker (X := (↑⊤ : Scheme)) (Opens.ι ⊤)) ⊥

Tactic:
exact X.topIso.hom.ker_eq_bot_of_isIso

Premises used: AlgebraicGeometry.Scheme.Hom.ker_eq_bot_of_isIso, AlgebraicGeometry.Scheme.topIso, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ IsPreimmersion (I.glueDataObjι U)

Tactic:
have : IsPreimmersion (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))) :=
    .mk_SpecMap
      (isClosedEmbedding_comap_of_surjective _ _ Ideal.Quotient.mk_surjective).isEmbedding
      (RingHom.surjectiveOnStalks_of_surjective Ideal.Quotient.mk_surjective)
  .comp _ _

Premises used: AlgebraicGeometry.IsPreimmersion.mk_SpecMap, AlgebraicGeometry.IsAffineOpen.isoSpec, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, CommRingCat.carrier, Ideal.Quotient.mk, RingHom.surjectiveOnStalks_of_surjective, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, Topology.IsClosedEmbedding.isEmbedding, Ideal.Quotient.mk_surjective, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, HasQuotient.Quotient, Opposite.op, CommRingCat.of, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, AlgebraicGeometry.IsPreimmersion.comp, PrimeSpectrum.isClosedEmbedding_comap_of_surjective, CategoryTheory.Iso.inv, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace, AlgebraicGeometry.Scheme.IdealSheafData.ideal, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι._proof_2
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
rw :
  Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv ≫ (↑U : X.Opens).ι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
⊢ I.glueDataObjι U ≫ (↑U : X.Opens).ι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯

Tactic:
rw [glueDataObjι, Category.assoc]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv ≫ (↑U : X.Opens).ι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
φ : Γ(X, (↑U : X.Opens)) ⟶ CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
rw :
  Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
    (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))))
    (Ideal.comap (CommRingCat.Hom.hom (↑U : X.Opens).topIso.hom)
      (RingHom.ker (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)
        (Ideal.Quotient.mk (I.ideal U))))
⊢ Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
    (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))))
    (Ideal.comap (CommRingCat.Hom.hom (↑U : X.Opens).topIso.hom) (I.ideal U))

Tactic:
rw [← Ideal.mk_ker (I := I.ideal _)]

Premises used: Ideal.mk_ker
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
φ : Γ(X, (↑U : X.Opens)) ⟶ CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
change :
  Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
    (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv))))
    (Ideal.comap (CommRingCat.Hom.hom (↑U : X.Opens).topIso.hom) (RingHom.ker (CommRingCat.Hom.hom φ)))
⊢ Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
    (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))))
    (Ideal.comap (CommRingCat.Hom.hom (↑U : X.Opens).topIso.hom)
      (RingHom.ker (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)
        (Ideal.Quotient.mk (I.ideal U))))

Tactic:
change RingHom.ker (Spec.map φ ≫ _).appTop.hom = (RingHom.ker φ.hom).comap _

Premises used: CommRingCat.Hom.hom, AlgebraicGeometry.Spec.map, AlgebraicGeometry.Scheme.Hom.appTop, Ideal.comap, CategoryTheory.CategoryStruct.comp, RingHom.ker
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
φ : Γ(X, (↑U : X.Opens)) ⟶ CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
rw :
  Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
    (RingHom.ker
      (CommRingCat.Hom.hom
        (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫
          Iso.hom (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))))))
    (RingHom.ker (CommRingCat.Hom.hom ((↑U : X.Opens).topIso.hom ≫ φ)))
⊢ Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
    (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv))))
    (Ideal.comap (CommRingCat.Hom.hom (↑U : X.Opens).topIso.hom) (RingHom.ker (CommRingCat.Hom.hom φ)))

Tactic:
rw [← RingHom.ker_equiv_comp _ (Scheme.ΓSpecIso _).commRingCatIsoToRingEquiv, RingHom.comap_ker,
    RingEquiv.toRingHom_eq_coe, Iso.commRingCatIsoToRingEquiv_toRingHom, ← CommRingCat.hom_comp,
    ← CommRingCat.hom_comp]

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, RingHom.comap_ker, AlgebraicGeometry.Scheme.ΓSpecIso, CommRingCat.hom_comp, RingEquiv.toRingHom_eq_coe, CategoryTheory.Iso.commRingCatIsoToRingEquiv_toRingHom, RingHom.ker_equiv_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
φ : Γ(X, (↑U : X.Opens)) ⟶ CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
e_f :
  Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫
      Iso.hom (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))) =
    (↑U : X.Opens).topIso.hom ≫ φ
⊢ Eq (α := Ideal (↑Γ((↑(↑U : X.Opens) : Scheme), ⊤) : Type u))
    (RingHom.ker
      (CommRingCat.Hom.hom
        (Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫
          Iso.hom (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))))))
    (RingHom.ker (CommRingCat.Hom.hom ((↑U : X.Opens).topIso.hom ≫ φ)))

Tactic:
congr 2
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
φ : Γ(X, (↑U : X.Opens)) ⟶ CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
e_f :
  Hom.app (IsAffineOpen.isoSpec ⋯).inv ⊤ ≫ Iso.hom (ΓSpecIso Γ(X, (↑U : X.Opens))) ≫ φ =
    X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ φ
⊢ Hom.appTop (Spec.map φ ≫ (IsAffineOpen.isoSpec ⋯).inv) ≫
      Iso.hom (ΓSpecIso (CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))) =
    (↑U : X.Opens).topIso.hom ≫ φ

Tactic:
simp only [Scheme.Hom.comp_app, TopologicalSpace.Opens.map_top, Category.assoc,
    Scheme.ΓSpecIso_naturality, Scheme.Opens.topIso_hom]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.comp_app, AlgebraicGeometry.Scheme.ΓSpecIso_naturality, TopologicalSpace.Opens.map_top, AlgebraicGeometry.Scheme.Opens.topIso_hom
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
φ : Γ(X, (↑U : X.Opens)) ⟶ CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
e_f : (↑U : X.Opens).topIso.hom ≫ φ = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ φ
⊢ Hom.app (IsAffineOpen.isoSpec ⋯).inv ⊤ ≫ Iso.hom (ΓSpecIso Γ(X, (↑U : X.Opens))) ≫ φ =
    X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ φ

Tactic:
rw [← Scheme.Hom.appTop, U.2.isoSpec_inv_appTop, Category.assoc, Iso.inv_hom_id_assoc]

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec_inv_appTop, CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.Hom.appTop, CategoryTheory.Iso.inv_hom_id_assoc, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
φ : Γ(X, (↑U : X.Opens)) ⟶ CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))
⊢ (↑U : X.Opens).topIso.hom ≫ φ = X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) ≫ φ

Tactic:
simp only [Scheme.Opens.topIso_hom]

Premises used: AlgebraicGeometry.Scheme.Opens.topIso_hom
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
simp :
  Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme))
    (Set.image (α := ↥(Spec (CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)))) (⇑(IsAffineOpen.isoSpec ⋯).inv)
      (Set.range (ι := ↥(I.glueDataObj U)) ⇑(Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))))
    ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec ⋯).inv a) ''
      PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
⊢ Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme)) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueDataObjι U))
    (Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.isoSpec ⋯).inv)
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))))

Tactic:
simp only [glueDataObjι, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
erw :
  Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme))
    (Set.image (α := ↥(Spec (CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)))) (⇑(IsAffineOpen.isoSpec ⋯).inv)
      (PrimeSpectrum.zeroLocus
        (↑(RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))) :
          Set (↑(CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u))))
    ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec ⋯).inv a) ''
      PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
hf :
  Function.Surjective (α := (↑(CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)) (β :=
    (↑(CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)) : Type u))
    (⇑(CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))) :
      (a : (↑(CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)) →
        (↑(CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)) : Type u))
⊢ Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme))
    (Set.image (α := ↥(Spec (CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)))) (⇑(IsAffineOpen.isoSpec ⋯).inv)
      (Set.range (ι := ↥(I.glueDataObj U)) ⇑(Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))))
    ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec ⋯).inv a) ''
      PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))

Tactic:
erw [range_comap_of_surjective]

Premises used: range_comap_of_surjective
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Function.Surjective (α := (↑(CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)) (β :=
    (↑(CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)) : Type u))
    (⇑(CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))) :
      (a : (↑(CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)) →
        (↑(CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)) : Type u))

Tactic:
Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Function.Surjective (α := (↑(CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)) (β :=
    (↑(CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)) : Type u))
    (⇑(CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))) :
      (a : (↑(CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u)) →
        (↑(CommRingCat.of ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)) : Type u))

Tactic:
exact Ideal.Quotient.mk_surjective

Premises used: Ideal.Quotient.mk_surjective
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
simp :
  Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme))
    (Set.image (α := ↥(Spec (CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)))) (⇑(IsAffineOpen.isoSpec ⋯).inv)
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))))
    ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec ⋯).inv a) ''
      PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))
⊢ Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme))
    (Set.image (α := ↥(Spec (CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)))) (⇑(IsAffineOpen.isoSpec ⋯).inv)
      (PrimeSpectrum.zeroLocus
        (↑(RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))) :
          Set (↑(CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)) : Type u))))
    ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec ⋯).inv a) ''
      PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Eq (α := Set ↥(↑(↑U : X.Opens) : Scheme))
    (Set.image (α := ↥(Spec (CommRingCat.of (↑Γ(X, (↑U : X.Opens)) : Type u)))) (⇑(IsAffineOpen.isoSpec ⋯).inv)
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))))
    ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec ⋯).inv a) ''
      PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
simp :
  Set.image (α := ↥(↑(↑U : X.Opens) : Scheme)) (⇑(↑U : X.Opens).ι)
      ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec ⋯).inv a) ''
        PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) =
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
⊢ Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueDataObjι U ≫ (↑U : X.Opens).ι) =
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, range_glueDataObjι]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
rw :
  Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens))))
      (Function.comp (β := ↥(↑(↑U : X.Opens) : Scheme)) ⇑(↑U : X.Opens).ι fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦
        (IsAffineOpen.isoSpec ⋯).inv a)
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) =
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
rw₁ :
  Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens))))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((IsAffineOpen.isoSpec ⋯).inv.base ≫ (↑U : X.Opens).ι.base)) :
        (a : ↥(Spec Γ(X, (↑U : X.Opens)))) → ↥X)
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) =
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
rw₂ :
  Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑((IsAffineOpen.isoSpec ⋯).inv ≫ (↑U : X.Opens).ι))
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) =
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
rw₃ :
  Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec ⋯))
      (PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) =
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
rw₄ rw₅ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)
⊢ Set.image (α := ↥(↑(↑U : X.Opens) : Scheme)) (⇑(↑U : X.Opens).ι)
      ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec ⋯).inv a) ''
        PrimeSpectrum.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u))) =
    X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
rw [← Set.image_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, IsAffineOpen.isoSpec_inv_ι,
    IsAffineOpen.fromSpec_image_zeroLocus]

Premises used: Set.image_comp, AlgebraicGeometry.IsAffineOpen.fromSpec_image_zeroLocus, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι