awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ 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)
have simp : Set.image (α := ↥(↑(↑U : X.Opens) : Scheme)) (⇑(↑U : X.Opens).ι)
    ((fun (a : ↥(Spec Γ(X, (↑U : X.Opens)))) ↦ (IsAffineOpen.isoSpec sorry).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: simp only [Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, range_glueDataObjι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ 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)
have 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 sorry).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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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)
⊢ 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)
have 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 sorry).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)
Tactic: rw [← Set.image_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, IsAffineOpen.isoSpec_inv_ι,
    IsAffineOpen.fromSpec_image_zeroLocus]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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)
⊢ 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)
have rw₂ : Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑((IsAffineOpen.isoSpec sorry).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)
Tactic: rw [← Set.image_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, IsAffineOpen.isoSpec_inv_ι,
    IsAffineOpen.fromSpec_image_zeroLocus]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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)
⊢ 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)
have rw₃ : Set.image (α := ↥(Spec Γ(X, (↑U : X.Opens)))) (⇑(IsAffineOpen.fromSpec sorry))
    (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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)
⊢ 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)
have 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)
Tactic: rw [← Set.image_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, IsAffineOpen.isoSpec_inv_ι,
    IsAffineOpen.fromSpec_image_zeroLocus]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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)
have 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)
Tactic: subst hU
Cleared hypotheses: U, h, hU, this_1, this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
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 (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)
have this₁ : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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.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)
have 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)
Tactic: simp only [IsLocalization.Away, ← Submonoid.map_powers]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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)
have 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))
Tactic: refine IsLocalization.of_surjective _ _ _ Ideal.Quotient.mk_surjective _
    Ideal.Quotient.mk_surjective ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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))
⊢ 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)
have 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))))
Tactic: refine IsLocalization.of_surjective _ _ _ Ideal.Quotient.mk_surjective _
    Ideal.Quotient.mk_surjective ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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)
⊢ 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))
have 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)))
Tactic: simp [RingHom.algebraMap_toAlgebra, Ideal.quotientMap_comp_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
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)) ⋯)
⊢ IsOpenImmersion (I.glueDataObjMap ⋯)
have 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)))
Tactic: have := I.isLocalization_away (X.affineBasicOpen_le f) f rfl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
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
⊢ Hom.opensRange (I.glueDataObjMap ⋯) = I.glueDataObjι V ⁻¹ᵁ (↑V : X.Opens).ι ⁻¹ᵁ X.basicOpen f
have 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)))
Tactic: have := I.isLocalization_away (X.affineBasicOpen_le f) f rfl
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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 ⋯) = I.glueDataObjι V ⁻¹ᵁ (↑V : X.Opens).ι ⁻¹ᵁ X.basicOpen f
have h : (↑(Hom.opensRange (I.glueDataObjMap sorry)) : Set ↥(I.glueDataObj V)) =
  (↑(I.glueDataObjι V ⁻¹ᵁ (↑V : X.Opens).ι ⁻¹ᵁ X.basicOpen f) : Set ↥(I.glueDataObj V))
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
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))
have 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))
Tactic: refine (localization_away_comap_range _ f').trans ?_