awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
hU : U = X.affineBasicOpen f
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V) ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  RingHom.toAlgebra (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯)
this : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
subst :
  ∀ (h : X.affineBasicOpen f ≤ V),
    let this := (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra;
    IsLocalization.Away f (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)
⊢ IsLocalization.Away f (↑Γ(X, (↑U : X.Opens)) : Type u)

Tactic:
subst hU
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
h : X.affineBasicOpen f ≤ V
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
  (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
    Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f))) :=
  RingHom.toAlgebra
    (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯)
this : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
⊢ IsLocalization.Away f (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)

Tactic:
V.2.isLocalization_of_eq_basicOpen _ _ rfl

Premises used: AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen, rfl, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
h : X.affineBasicOpen f ≤ V
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
  (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
    Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f))) :=
  RingHom.toAlgebra
    (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯)
this : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
⊢ IsLocalization.Away f (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)

Tactic:
exact V.2.isLocalization_of_eq_basicOpen _ _ rfl

Premises used: AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen, rfl, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
hU : U = X.affineBasicOpen f
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V) ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  RingHom.toAlgebra (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯)
this : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
⊢ IsLocalization.Away f (↑Γ(X, (↑U : X.Opens)) : Type u)

Tactic:
have : IsLocalization.Away f Γ(X, U) := by
    subst hU; exact V.2.isLocalization_of_eq_basicOpen _ _ rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
hU : U = X.affineBasicOpen f
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V) ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  RingHom.toAlgebra (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯)
this_2 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
this : IsLocalization.Away f (↑Γ(X, (↑U : X.Opens)) : Type u)
simp :
  IsLocalization
    (Submonoid.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
      (Ideal.Quotient.mk (I.ideal V)) (Submonoid.powers f))
    ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)
⊢ IsLocalization.Away (R := (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    ((Ideal.Quotient.mk (I.ideal V) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
        f :
      (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)

Tactic:
simp only [IsLocalization.Away, ← Submonoid.map_powers]

Premises used: IsLocalization.Away, Submonoid.map_powers
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
hU : U = X.affineBasicOpen f
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V) ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  RingHom.toAlgebra (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯)
this_2 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
this : IsLocalization.Away f (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ IsLocalization
    (Submonoid.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
      (Ideal.Quotient.mk (I.ideal V)) (Submonoid.powers f))
    ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)

Tactic:
IsLocalization.of_surjective _ _ _ Ideal.Quotient.mk_surjective _
    Ideal.Quotient.mk_surjective ?_ ?_

Premises used: IsLocalization.of_surjective, Ideal.Quotient.mk_surjective
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
hU : U = X.affineBasicOpen f
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V) ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  RingHom.toAlgebra (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯)
this_2 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
this : IsLocalization.Away f (↑Γ(X, (↑U : X.Opens)) : Type u)
refine_1 :
  RingHom.comp (Ideal.Quotient.mk (I.ideal U))
      (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u)) =
    RingHom.comp
      (algebraMap ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V) ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))
      (Ideal.Quotient.mk (I.ideal V))
refine_2 :
  LE.le (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
    (RingHom.ker (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)
      (Ideal.Quotient.mk (I.ideal U)))
    (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
      (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
      (RingHom.ker (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
        (Ideal.Quotient.mk (I.ideal V))))
⊢ IsLocalization
    (Submonoid.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
      (Ideal.Quotient.mk (I.ideal V)) (Submonoid.powers f))
    ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)

Tactic:
refine IsLocalization.of_surjective _ _ _ Ideal.Quotient.mk_surjective _
    Ideal.Quotient.mk_surjective ?_ ?_

Premises used: IsLocalization.of_surjective, Ideal.Quotient.mk_surjective
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
hU : U = X.affineBasicOpen f
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V) ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  RingHom.toAlgebra (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯)
this_2 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
this : IsLocalization.Away f (↑Γ(X, (↑U : X.Opens)) : Type u)
refine_1 :
  Eq (α := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)
    (RingHom.comp (Ideal.Quotient.mk (I.ideal U)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)))
    (RingHom.comp (Ideal.Quotient.mk (I.ideal U)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)))
⊢ RingHom.comp (Ideal.Quotient.mk (I.ideal U))
      (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u)) =
    RingHom.comp
      (algebraMap ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V) ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U))
      (Ideal.Quotient.mk (I.ideal V))

Tactic:
simp [RingHom.algebraMap_toAlgebra, Ideal.quotientMap_comp_mk]

Premises used: Ideal.quotientMap_comp_mk, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
hU : U = X.affineBasicOpen f
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V) ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  RingHom.toAlgebra (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯)
this_2 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
this : IsLocalization.Away f (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ Eq (α := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)
    (RingHom.comp (Ideal.Quotient.mk (I.ideal U)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)))
    (RingHom.comp (Ideal.Quotient.mk (I.ideal U)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
h : U ≤ V
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
hU : U = X.affineBasicOpen f
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V) ((↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U) :=
  RingHom.toAlgebra (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯)
this_2 : Algebra (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
this : IsLocalization.Away f (↑Γ(X, (↑U : X.Opens)) : Type u)
⊢ LE.le (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u))
    (RingHom.ker (F := (↑Γ(X, (↑U : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u) ⧸ I.ideal U)
      (Ideal.Quotient.mk (I.ideal U)))
    (Ideal.map (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑U : X.Opens)) : Type u))
      (algebraMap (↑Γ(X, (↑V : X.Opens)) : Type u) (↑Γ(X, (↑U : X.Opens)) : Type u))
      (RingHom.ker (F := (↑Γ(X, (↑V : X.Opens)) : Type u) →+* (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
        (Ideal.Quotient.mk (I.ideal V))))

Tactic:
simp only [Ideal.mk_ker, RingHom.algebraMap_toAlgebra, I.map_ideal', le_refl]

Premises used: le_refl, AlgebraicGeometry.Scheme.IdealSheafData.map_ideal', RingHom.algebraMap_toAlgebra, Ideal.mk_ker
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
this : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
  (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
    Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f))) :=
  RingHom.toAlgebra
    (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯)
⊢ IsLocalization.Away (R := (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    ((Ideal.Quotient.mk (I.ideal V) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
        f :
      (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
      Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f)))

Tactic:
have := I.isLocalization_away (X.affineBasicOpen_le f) f rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
  (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
    Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f))) :=
  RingHom.toAlgebra
    (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯)
this :
  IsLocalization.Away (R := (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    ((Ideal.Quotient.mk (I.ideal V) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
        f :
      (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
      Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f)))
⊢ IsOpenImmersion (I.glueDataObjMap ⋯)

Tactic:
IsOpenImmersion.of_isLocalization (Ideal.Quotient.mk _ f)

Premises used: Ideal.Quotient.mk, AlgebraicGeometry.IsOpenImmersion.of_isLocalization, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
  (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
    Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f))) :=
  RingHom.toAlgebra
    (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯)
this :
  IsLocalization.Away (R := (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    ((Ideal.Quotient.mk (I.ideal V) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
        f :
      (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
      Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f)))
⊢ IsOpenImmersion (I.glueDataObjMap ⋯)

Tactic:
exact IsOpenImmersion.of_isLocalization (Ideal.Quotient.mk _ f)

Premises used: Ideal.Quotient.mk, AlgebraicGeometry.IsOpenImmersion.of_isLocalization, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
this : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
  (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
    Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f))) :=
  RingHom.toAlgebra
    (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯)
f' : (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V :=
  (Ideal.Quotient.mk (I.ideal V) :
      (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    f
⊢ IsLocalization.Away (R := (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    ((Ideal.Quotient.mk (I.ideal V) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
        f :
      (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
      Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f)))

Tactic:
have := I.isLocalization_away (X.affineBasicOpen_le f) f rfl
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
  (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
    Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f))) :=
  RingHom.toAlgebra
    (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯)
f' : (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V :=
  (Ideal.Quotient.mk (I.ideal V) :
      (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    f
this :
  IsLocalization.Away (R := (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    ((Ideal.Quotient.mk (I.ideal V) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
        f :
      (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
      Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f)))
h :
  (↑(Hom.opensRange (I.glueDataObjMap ⋯)) : Set ↥(I.glueDataObj V)) =
    (↑(I.glueDataObjι V ⁻¹ᵁ (↑V : X.Opens).ι ⁻¹ᵁ X.basicOpen f) : Set ↥(I.glueDataObj V))
⊢ Hom.opensRange (I.glueDataObjMap ⋯) = I.glueDataObjι V ⁻¹ᵁ (↑V : X.Opens).ι ⁻¹ᵁ X.basicOpen f

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
  (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
    Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f))) :=
  RingHom.toAlgebra
    (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯)
f' : (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V :=
  (Ideal.Quotient.mk (I.ideal V) :
      (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    f
this :
  IsLocalization.Away (R := (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    ((Ideal.Quotient.mk (I.ideal V) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
        f :
      (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
      Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f)))
⊢ (↑(Hom.opensRange (I.glueDataObjMap ⋯)) : Set ↥(I.glueDataObj V)) =
    (↑(I.glueDataObjι V ⁻¹ᵁ (↑V : X.Opens).ι ⁻¹ᵁ X.basicOpen f) : Set ↥(I.glueDataObj V))

Tactic:
(localization_away_comap_range _ f').trans ?_

Premises used: setOf, Ideal.quotientMap, Ideal.Quotient.lift, Set.range, PrimeSpectrum.comap, PrimeSpectrum.localization_away_comap_range, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
  (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
    Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f))) :=
  RingHom.toAlgebra
    (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯)
f' : (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V :=
  (Ideal.Quotient.mk (I.ideal V) :
      (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    f
this :
  IsLocalization.Away (R := (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    ((Ideal.Quotient.mk (I.ideal V) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
        f :
      (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
      Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f)))
h :
  (↑(PrimeSpectrum.basicOpen f') : Set (PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V))) =
    (↑(I.glueDataObjι V ⁻¹ᵁ (↑V : X.Opens).ι ⁻¹ᵁ X.basicOpen f) : Set ↥(I.glueDataObj V))
⊢ (↑(Hom.opensRange (I.glueDataObjMap ⋯)) : Set ↥(I.glueDataObj V)) =
    (↑(I.glueDataObjι V ⁻¹ᵁ (↑V : X.Opens).ι ⁻¹ᵁ X.basicOpen f) : Set ↥(I.glueDataObj V))

Tactic:
refine (localization_away_comap_range _ f').trans ?_

Premises used: PrimeSpectrum.localization_away_comap_range, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
V : (↑X.affineOpens : Type u)
f : (↑Γ(X, (↑V : X.Opens)) : Type u)
this_1 : Algebra ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
  (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
    Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f))) :=
  RingHom.toAlgebra
    (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) ⋯)
f' : (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V :=
  (Ideal.Quotient.mk (I.ideal V) :
      (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    f
this :
  IsLocalization.Away (R := (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    ((Ideal.Quotient.mk (I.ideal V) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
        f :
      (↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)
    (HasQuotient.Quotient (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u) (B :=
      Ideal (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u)) (I.ideal (X.affineBasicOpen f)))
h :
  (↑((Opens.comap
                { toFun := comap (Ideal.Quotient.mk (I.ideal V)), continuous_toFun := ⋯ :
                  C(PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V),
                    PrimeSpectrum (↑Γ(X, (↑V : X.Opens)) : Type u)) } :
              (a : TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, (↑V : X.Opens)) : Type u))) →
                TopologicalSpace.Opens (PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V)))
            (IsAffineOpen.fromSpec ⋯ ⁻¹ᵁ X.basicOpen f) :
          TopologicalSpace.Opens (PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V))) :
      Set (PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V))) =
    (↑((Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ X.basicOpen f) :
      Set ↥(I.glueDataObj V))
⊢ (↑(PrimeSpectrum.basicOpen f') : Set (PrimeSpectrum ((↑Γ(X, (↑V : X.Opens)) : Type u) ⧸ I.ideal V))) =
    (↑(I.glueDataObjι V ⁻¹ᵁ (↑V : X.Opens).ι ⁻¹ᵁ X.basicOpen f) : Set ↥(I.glueDataObj V))

Tactic:
rw [← comap_basicOpen, ← V.2.fromSpec_preimage_basicOpen,
    ← Scheme.Hom.comp_preimage, glueDataObjι_ι]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_preimage, AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_basicOpen, PrimeSpectrum.comap_basicOpen, AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι_ι, Subtype.property