awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥X
hx : x ∈ (↑I.support : Set ↥X)
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
⊢ Membership.mem (γ := Set ↥X) (Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo) x
have refine_2 : ∀ (y : ↥(I.glueDataObj (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU)))
  (hx :
    Membership.mem (α := ↥X) (↑I.support : Set ↥X)
      ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
            (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
          y :
        ↥X))
  (hxU :
    Membership.mem (α := ↥X) (↑U : Set ↥X)
      ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
            (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
          y :
        ↥X)),
  Membership.mem (α := ↥X) (γ := Set ↥X) (Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo)
    ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
        y :
      ↥X)
Tactic: obtain ⟨y, rfl⟩ := (I.range_glueDataObjι_ι_eq_support_inter ⟨U, hU⟩).ge ⟨hx, hxU⟩
Cleared hypotheses: x, hx, hxU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
y : ↥(I.glueDataObj (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU))
hx :
  Membership.mem (α := ↥X) (↑I.support : Set ↥X)
    ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
        y :
      ↥X)
hxU :
  Membership.mem (α := ↥X) (↑U : Set ↥X)
    ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
        y :
      ↥X)
⊢ Membership.mem (α := ↥X) (γ := Set ↥X) (Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo)
    ((I.glueDataObjι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) : X.Opens).ι)
        y :
      ↥X)
have refine_2 : Membership.mem (α := ↥X) (γ := Set ↥X) (Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo)
  ((I.glueData.ι (Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U hU) ≫ I.gluedTo) y : ↥X)
Tactic: rw [← ι_gluedTo]
-- 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.glueData.ι U) = (↑(I.gluedTo ⁻¹ᵁ (↑U : X.Opens)) : Set ↥I.glueData.glued)
have simp : Eq (α := Set ↥I.glueData.glued) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U))
  (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X))
Tactic: simp only [TopologicalSpace.Opens.map_coe]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Eq (α := Set ↥I.glueData.glued) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U))
    (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X))
have a : Eq (α := Set ↥X)
  (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U)))
  (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
Tactic: apply I.gluedTo_injective.image_injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Eq (α := Set ↥X)
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
have a : Eq (α := Set ↥X)
  (Set.range (ι := ↥(I.glueDataObj U)) (Function.comp (β := ↥I.glueData.glued) ⇑I.gluedTo ⇑(I.glueData.ι U)))
  (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
Tactic: rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ι_gluedTo,
    range_glueDataObjι_ι, Set.image_preimage_eq_inter_range, range_gluedTo,
    ← coe_support_inter, Set.inter_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
a :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U)) (Function.comp (β := ↥I.glueData.glued) ⇑I.gluedTo ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
⊢ Eq (α := Set ↥X)
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
have a₁ : Eq (α := Set ↥X)
  (Set.range (ι := ↥(I.glueDataObj U))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          (X := (↑(I.glueDataObj U).toPresheafedSpace : TopCat))
          (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (I.glueData.ι U))) ≫ I.gluedTo.base)) :
      (a : ↥(I.glueDataObj U)) → ↥X))
  (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
Tactic: rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ι_gluedTo,
    range_glueDataObjι_ι, Set.image_preimage_eq_inter_range, range_gluedTo,
    ← coe_support_inter, Set.inter_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
a :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U)) (Function.comp (β := ↥I.glueData.glued) ⇑I.gluedTo ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₁ :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(I.glueDataObj U).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (I.glueData.ι U))) ≫
              I.gluedTo.base)) :
        (a : ↥(I.glueDataObj U)) → ↥X))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
⊢ Eq (α := Set ↥X)
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
have a₂ : Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U ≫ I.gluedTo))
  (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
Tactic: rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ι_gluedTo,
    range_glueDataObjι_ι, Set.image_preimage_eq_inter_range, range_gluedTo,
    ← coe_support_inter, Set.inter_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
a :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U)) (Function.comp (β := ↥I.glueData.glued) ⇑I.gluedTo ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₁ :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(I.glueDataObj U).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (I.glueData.ι U))) ≫
              I.gluedTo.base)) :
        (a : ↥(I.glueDataObj U)) → ↥X))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₂ :
  Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U ≫ I.gluedTo))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
⊢ Eq (α := Set ↥X)
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
have a₃ : Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueDataObjι U ≫ (↑U : X.Opens).ι))
  (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
Tactic: rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ι_gluedTo,
    range_glueDataObjι_ι, Set.image_preimage_eq_inter_range, range_gluedTo,
    ← coe_support_inter, Set.inter_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
a :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U)) (Function.comp (β := ↥I.glueData.glued) ⇑I.gluedTo ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₁ :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(I.glueDataObj U).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (I.glueData.ι U))) ≫
              I.gluedTo.base)) :
        (a : ↥(I.glueDataObj U)) → ↥X))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₂ :
  Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U ≫ I.gluedTo))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₃ :
  Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueDataObjι U ≫ (↑U : X.Opens).ι))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
⊢ Eq (α := Set ↥X)
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
have a₄ : X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
  Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X))
Tactic: rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ι_gluedTo,
    range_glueDataObjι_ι, Set.image_preimage_eq_inter_range, range_gluedTo,
    ← coe_support_inter, Set.inter_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
a :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U)) (Function.comp (β := ↥I.glueData.glued) ⇑I.gluedTo ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₁ :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(I.glueDataObj U).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (I.glueData.ι U))) ≫
              I.gluedTo.base)) :
        (a : ↥(I.glueDataObj U)) → ↥X))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₂ :
  Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U ≫ I.gluedTo))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₃ :
  Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueDataObjι U ≫ (↑U : X.Opens).ι))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₄ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X))
⊢ Eq (α := Set ↥X)
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
have a₅ : X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
  (↑(↑U : X.Opens) : Set ↥X) ∩ Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo
Tactic: rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ι_gluedTo,
    range_glueDataObjι_ι, Set.image_preimage_eq_inter_range, range_gluedTo,
    ← coe_support_inter, Set.inter_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
a :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U)) (Function.comp (β := ↥I.glueData.glued) ⇑I.gluedTo ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₁ :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(I.glueDataObj U).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (I.glueData.ι U))) ≫
              I.gluedTo.base)) :
        (a : ↥(I.glueDataObj U)) → ↥X))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₂ :
  Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U ≫ I.gluedTo))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₃ :
  Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueDataObjι U ≫ (↑U : X.Opens).ι))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₄ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X))
a₅ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    (↑(↑U : X.Opens) : Set ↥X) ∩ Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo
⊢ Eq (α := Set ↥X)
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
have a₆ : X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
  (↑(↑U : X.Opens) : Set ↥X) ∩ (↑I.support : Set ↥X)
Tactic: rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ι_gluedTo,
    range_glueDataObjι_ι, Set.image_preimage_eq_inter_range, range_gluedTo,
    ← coe_support_inter, Set.inter_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
a :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U)) (Function.comp (β := ↥I.glueData.glued) ⇑I.gluedTo ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₁ :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(I.glueDataObj U).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (I.glueData.ι U))) ≫
              I.gluedTo.base)) :
        (a : ↥(I.glueDataObj U)) → ↥X))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₂ :
  Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U ≫ I.gluedTo))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₃ :
  Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueDataObjι U ≫ (↑U : X.Opens).ι))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₄ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X))
a₅ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    (↑(↑U : X.Opens) : Set ↥X) ∩ Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo
a₆ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    (↑(↑U : X.Opens) : Set ↥X) ∩ (↑I.support : Set ↥X)
⊢ Eq (α := Set ↥X)
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
have a₇ : (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) = (↑(↑U : X.Opens) : Set ↥X) ∩ (↑I.support : Set ↥X)
Tactic: rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ι_gluedTo,
    range_glueDataObjι_ι, Set.image_preimage_eq_inter_range, range_gluedTo,
    ← coe_support_inter, Set.inter_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
a :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U)) (Function.comp (β := ↥I.glueData.glued) ⇑I.gluedTo ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₁ :
  Eq (α := Set ↥X)
    (Set.range (ι := ↥(I.glueDataObj U))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (X := (↑(I.glueDataObj U).toPresheafedSpace : TopCat))
            (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (I.glueData.ι U))) ≫
              I.gluedTo.base)) :
        (a : ↥(I.glueDataObj U)) → ↥X))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₂ :
  Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U ≫ I.gluedTo))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₃ :
  Eq (α := Set ↥X) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueDataObjι U ≫ (↑U : X.Opens).ι))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
a₄ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X))
a₅ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    (↑(↑U : X.Opens) : Set ↥X) ∩ Set.range (ι := ↥I.glueData.glued) ⇑I.gluedTo
a₆ :
  X.zeroLocus (↑(I.ideal U) : Set (↑Γ(X, (↑U : X.Opens)) : Type u)) ∩ (↑(↑U : X.Opens) : Set ↥X) =
    (↑(↑U : X.Opens) : Set ↥X) ∩ (↑I.support : Set ↥X)
a₇ : (↑I.support : Set ↥X) ∩ (↑(↑U : X.Opens) : Set ↥X) = (↑(↑U : X.Opens) : Set ↥X) ∩ (↑I.support : Set ↥X)
⊢ Eq (α := Set ↥X)
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (Set.range (ι := ↥(I.glueDataObj U)) ⇑(I.glueData.ι U)))
    (Set.image (α := ↥I.glueData.glued) (⇑I.gluedTo) (⇑I.gluedTo ⁻¹' (↑(↑U : X.Opens) : Set ↥X)))
have a₈ : (↑(↑U : X.Opens) : Set ↥X) ∩ (↑I.support : Set ↥X) = (↑(↑U : X.Opens) : Set ↥X) ∩ (↑I.support : Set ↥X)
Tactic: rw [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, ι_gluedTo,
    range_glueDataObjι_ι, Set.image_preimage_eq_inter_range, range_gluedTo,
    ← coe_support_inter, Set.inter_comm]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ IsPreimmersion I.gluedTo
have rw : ∀ (i : (↑X.affineOpens : Type u)),
  IsPreimmersion (X := (↑(I.gluedTo ⁻¹ᵁ (↑i : X.Opens)) : Scheme)) (I.gluedTo ∣_ (↑i : X.Opens))
Tactic: rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top (P := @IsPreimmersion)
    _ (iSup_affineOpens_eq_top X)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ IsPreimmersion (X := (↑(I.gluedTo ⁻¹ᵁ (↑U : X.Opens)) : Scheme)) (I.gluedTo ∣_ (↑U : X.Opens))
have rw : IsPreimmersion (I.glueDataObjι U)
Tactic: rw [← MorphismProperty.cancel_left_of_respectsIso @IsPreimmersion (I.glueDataObjIso U).hom,
    glueDataObjIso_hom_restrict]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ Eq (α := (a : ↥I.subscheme) → ↥X) (⇑(I.subschemeIso.hom ≫ I.gluedTo))
    (Subtype.val (p := fun (x : ↥X) ↦ x ∈ I.support))
have h : ∀ (x : ↥I.subscheme), (I.subschemeIso.hom ≫ I.gluedTo) x = (↑x : ↥X)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥I.subscheme
⊢ (↑((I.gluedHomeo : (a : ↥I.glueData.glued) → ↥I.support)
          ((I.gluedHomeo.symm : (a : ↥I.support) → ↥I.glueData.glued) x)) :
      ↥X) =
    (↑x : ↥X)
have h : (↑x : ↥X) = (↑x : ↥X)
Tactic: rw [I.gluedHomeo.apply_symm_apply]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ IsPreimmersion I.subschemeι
have rw : IsPreimmersion (I.subschemeIso.hom ≫ I.gluedTo)
Tactic: rw [subschemeι_def]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
⊢ QuasiCompact I.subschemeι
have rw : QuasiCompact (I.subschemeIso.hom ≫ I.gluedTo)
Tactic: rw [subschemeι_def]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U : (↑X.affineOpens : Type u)
⊢ Hom.opensRange (X := I.glueData.U U) (I.glueData.ι U ≫ I.subschemeIso.inv) = I.subschemeι ⁻¹ᵁ (↑U : X.Opens)
have h : (↑(Hom.opensRange (X := I.glueData.U U) (I.glueData.ι U ≫ I.subschemeIso.inv)) : Set ↥I.subscheme) =
  (↑(I.subschemeι ⁻¹ᵁ (↑U : X.Opens)) : Set ↥I.subscheme)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
x : ↥I.subscheme
U : (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯).I₀ :=
  Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯) (↑x : ↥X)
⊢ Membership.mem (γ := Set ↥I.subscheme)
    (Set.range (ι :=
      ↥(Spec
          (CommRingCat.of
            (HasQuotient.Quotient
              (↑Γ(X,
                    (↑(Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)
                          (↑x : ↥X)) :
                      X.Opens)) :
                Type u)
              (B :=
              Ideal
                (↑Γ(X,
                      (↑(Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)
                            (↑x : ↥X)) :
                        X.Opens)) :
                  Type u))
              (I.ideal
                (Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯)
                  (↑x : ↥X)))))))
      ⇑(I.glueData.ι
            (Cover.idx (X.openCoverOfIsOpenCover (fun (i : (↑X.affineOpens : Type u)) ↦ (↑i : X.Opens)) ⋯) (↑x : ↥X)) ≫
          I.subschemeIso.inv))
    x
have hy : (↑x : ↥X) ∈ (↑U : X.Opens)
Tactic: obtain ⟨⟨y, hy : y ∈ U.1⟩, rfl : y = x.1⟩ :=
      (X.openCoverOfIsOpenCover _ (iSup_affineOpens_eq_top X)).covers x.1