awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
H :
  LE.le (α := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme).Opens) ⊤
    (X.homOfLE ⋯ ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))
⊢ Eq (α := Γ(X, (↑V : X.Opens)).Hom Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (Iso.inv (ΓSpecIso Γ(X, (↑V : X.Opens))) ≫
        Hom.app (IsAffineOpen.isoSpec ⋯).hom ⊤ ≫
          CategoryStruct.comp (Y := Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) :
              Γ(X, (↑V : X.Opens).ι ''ᵁ ⊤) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
            (Hom.app F ⊤ :
              Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶
                Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), F ⁻¹ᵁ ⊤)) :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
    (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫
        X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫
          (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme).presheaf.map (homOfLE H).op ≫ Hom.appLE F ⊤ ⊤ ⋯ :
      Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤))
have h : Eq (α := Γ(X, (↑V : X.Opens)).Hom Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤))
  (CategoryStruct.comp (Y := Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
      (X.presheaf.map (eqToHom sorry ≫ Quiver.Hom.op (homOfLE sorry)) :
        Γ(X, (↑V : X.Opens)) ⟶ Γ(X, ((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ''ᵁ ⊤))
      (Hom.appLE F ⊤ (F ⁻¹ᵁ ⊤) sorry :
        Γ((↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme), ⊤) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), F ⁻¹ᵁ ⊤)) :
    Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤))
  (X.presheaf.map (Quiver.Hom.op (homOfLE sorry) ≫ Quiver.Hom.op (homOfLE sorry) ≫ Quiver.Hom.op (homOfLE sorry)) ≫
      Hom.appLE F ⊤ ⊤ sorry :
    Γ(X, (↑V : X.Opens)) ⟶ Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤))
Tactic: simp only [homOfLE_leOfHom, Opens.toScheme_presheaf_map, Quiver.Hom.unop_op,
        Hom.opensFunctor_map_homOfLE, ← Functor.map_comp_assoc, IsAffineOpen.isoSpec_hom_appTop,
        Opens.topIso_inv, eqToHom_op, homOfLE_leOfHom, Category.assoc,
        Iso.inv_hom_id_assoc, F.app_eq_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (hypothesis)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
⊢ Eq (α := (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    ((CommRingCat.Hom.hom
            (Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫
              Hom.appLE (F ≫ X.homOfLE ⋯) ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ ⋯) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
        x :
      (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    (0 : (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
have this : Eq (α := (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
  ((CommRingCat.Hom.hom
          (Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫ Hom.app (I.glueDataObjι U) ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))) :
        (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) →
          (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
      x :
    (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
  (0 : (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
Tactic: have : (U.1.ι.app V.1 ≫ (I.glueDataObjι U).app (U.1.ι ⁻¹ᵁ V.1)).hom x = 0 :=
        I.ideal_le_ker_glueDataObjι U V hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : (↑Γ(X, (↑V : X.Opens)) : Type u)
hx : x ∈ I.ideal V
this :
  Eq (α := (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
    ((CommRingCat.Hom.hom
            (Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫
              Hom.app (I.glueDataObjι U) ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens))) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) →
            (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
        x :
      (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
    (0 : (↑Γ(I.glueDataObj U, I.glueDataObjι U ⁻¹ᵁ (↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) : Type u))
⊢ Eq (α := (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    ((CommRingCat.Hom.hom
            (Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫
              Hom.appLE (F ≫ X.homOfLE ⋯) ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ ⋯) :
          (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
        x :
      (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    (0 : (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
have refine_1 : Eq (α := (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
  ((CommRingCat.Hom.hom
          (Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫
            Hom.appLE (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry) ≫ I.glueDataObjι U)
              ((↑U : X.Opens).ι ⁻¹ᵁ (↑V : X.Opens)) ⊤ sorry) :
        (a : (↑Γ(X, (↑V : X.Opens)) : Type u)) → (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
      x :
    (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
  (0 : (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE sorry), ⊤) : Type u))
Tactic: simp_rw [F, ← pullback.condition]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
| Hom.liftQuotient (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) (I.ideal V) ⋯ ≫ I.glueDataObjι V
have enter : I.glueDataObjι V
Tactic: enter [2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
F : pullback (Y := (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) (I.glueDataObjι U) (X.homOfLE ⋯) ⟶
  (↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme) :=
  pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
| Hom.liftQuotient (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) (I.ideal V) ⋯ ≫ I.glueDataObjι V
have enter : Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ (IsAffineOpen.isoSpec sorry).inv
Tactic: enter [2]; rw [glueDataObjι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
⊢ I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueDataObjι V =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯
have refine : Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE sorry) ≫ X.homOfLE sorry ≫ (IsAffineOpen.isoSpec sorry).hom)
      (I.ideal V) sorry ≫
    I.glueDataObjι V =
  pullback.snd (I.glueDataObjι U) (X.homOfLE sorry) ≫ X.homOfLE sorry
Tactic: refine (pullback.lift_fst_assoc _ _ _ _).trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
| Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
      (I.ideal V) ⋯ ≫
    I.glueDataObjι V
have enter : I.glueDataObjι V
Tactic: enter [2]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
| Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
      (I.ideal V) ⋯ ≫
    I.glueDataObjι V
have enter : Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ (IsAffineOpen.isoSpec sorry).inv
Tactic: enter [2]; rw [glueDataObjι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
⊢ Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
        (I.ideal V) ⋯ ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯
have rw : Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
  ((pullback.snd (I.glueDataObjι U) (X.homOfLE sorry) ≫ X.homOfLE sorry ≫ (IsAffineOpen.isoSpec sorry).hom) ≫
    (IsAffineOpen.isoSpec sorry).inv)
  (pullback.snd (I.glueDataObjι U) (X.homOfLE sorry) ≫ X.homOfLE sorry)
Tactic: rw [Scheme.Hom.liftQuotient_comp_assoc, Category.assoc, Category.assoc, Iso.hom_inv_id,
    Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
rw :
  Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
    ((pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫
      (IsAffineOpen.isoSpec ⋯).inv)
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯)
⊢ Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
        (I.ideal V) ⋯ ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯
have rw₁ : Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
  (pullback.snd (I.glueDataObjι U) (X.homOfLE sorry) ≫
    (X.homOfLE sorry ≫ (IsAffineOpen.isoSpec sorry).hom) ≫ (IsAffineOpen.isoSpec sorry).inv)
  (pullback.snd (I.glueDataObjι U) (X.homOfLE sorry) ≫ X.homOfLE sorry)
Tactic: rw [Scheme.Hom.liftQuotient_comp_assoc, Category.assoc, Category.assoc, Iso.hom_inv_id,
    Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
rw :
  Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
    ((pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫
      (IsAffineOpen.isoSpec ⋯).inv)
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯)
rw₁ :
  Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫
      (X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫ (IsAffineOpen.isoSpec ⋯).inv)
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯)
⊢ Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
        (I.ideal V) ⋯ ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯
have rw₂ : Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
  (pullback.snd (I.glueDataObjι U) (X.homOfLE sorry) ≫
    X.homOfLE sorry ≫ (IsAffineOpen.isoSpec sorry).hom ≫ (IsAffineOpen.isoSpec sorry).inv)
  (pullback.snd (I.glueDataObjι U) (X.homOfLE sorry) ≫ X.homOfLE sorry)
Tactic: rw [Scheme.Hom.liftQuotient_comp_assoc, Category.assoc, Category.assoc, Iso.hom_inv_id,
    Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
rw :
  Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
    ((pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫
      (IsAffineOpen.isoSpec ⋯).inv)
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯)
rw₁ :
  Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫
      (X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫ (IsAffineOpen.isoSpec ⋯).inv)
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯)
rw₂ :
  Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫
      X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom ≫ (IsAffineOpen.isoSpec ⋯).inv)
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯)
⊢ Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
        (I.ideal V) ⋯ ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯
have rw₃ : Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
  (pullback.snd (I.glueDataObjι U) (X.homOfLE sorry) ≫ X.homOfLE sorry ≫ 𝟙 (↑(↑V : X.Opens) : Scheme))
  (pullback.snd (I.glueDataObjι U) (X.homOfLE sorry) ≫ X.homOfLE sorry)
Tactic: rw [Scheme.Hom.liftQuotient_comp_assoc, Category.assoc, Category.assoc, Iso.hom_inv_id,
    Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
rw :
  Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
    ((pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫
      (IsAffineOpen.isoSpec ⋯).inv)
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯)
rw₁ :
  Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫
      (X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) ≫ (IsAffineOpen.isoSpec ⋯).inv)
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯)
rw₂ :
  Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫
      X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom ≫ (IsAffineOpen.isoSpec ⋯).inv)
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯)
rw₃ :
  Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ 𝟙 (↑(↑V : X.Opens) : Scheme))
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯)
⊢ Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
        (I.ideal V) ⋯ ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯
have rw₄ : Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
  (pullback.snd (I.glueDataObjι U) (X.homOfLE sorry) ≫ X.homOfLE sorry)
  (pullback.snd (I.glueDataObjι U) (X.homOfLE sorry) ≫ X.homOfLE sorry)
Tactic: rw [Scheme.Hom.liftQuotient_comp_assoc, Category.assoc, Category.assoc, Iso.hom_inv_id,
    Category.comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V W U₀ : (↑X.affineOpens : Type u)
hU₀ : (↑U : X.Opens) ⊓ (↑W : X.Opens) ≤ (↑U₀ : X.Opens)
⊢ Subset (α := Set ↥X)
    (Set.range (ι :=
      ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE ⋯)) (Y := pullback (I.glueDataObjι U) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))))
      ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
          pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι))
    (Set.range (ι := ↥(↑((↑V : X.Opens) ⊓ (↑U₀ : X.Opens)) : Scheme)) ⇑((↑V : X.Opens) ⊓ (↑U₀ : X.Opens)).ι)
have simp : Set.range (ι :=
      ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE sorry)) (Y := pullback (I.glueDataObjι U) (X.homOfLE sorry))
          (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry))))
      ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) ≫
          pullback.fst (I.glueDataObjι U) (X.homOfLE sorry) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι) ⊆
    (↑(↑V : X.Opens) : Set ↥X) ∧
  Set.range (ι :=
      ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE sorry)) (Y := pullback (I.glueDataObjι U) (X.homOfLE sorry))
          (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry))))
      ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) ≫
          pullback.fst (I.glueDataObjι U) (X.homOfLE sorry) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι) ⊆
    (↑(↑U₀ : X.Opens) : Set ↥X)
Tactic: simp only [Scheme.Opens.range_ι, TopologicalSpace.Opens.coe_inf, Set.subset_inter_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V W U₀ : (↑X.affineOpens : Type u)
hU₀ : (↑U : X.Opens) ⊓ (↑W : X.Opens) ≤ (↑U₀ : X.Opens)
⊢ Set.range (ι :=
        ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE ⋯)) (Y := pullback (I.glueDataObjι U) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))))
        ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
            pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι) ⊆
      (↑(↑V : X.Opens) : Set ↥X) ∧
    Set.range (ι :=
        ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE ⋯)) (Y := pullback (I.glueDataObjι U) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))))
        ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
            pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι) ⊆
      (↑(↑U₀ : X.Opens) : Set ↥X)
have left : Set.range (ι :=
    ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE sorry)) (Y := pullback (I.glueDataObjι U) (X.homOfLE sorry))
        (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry))))
    ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) ≫
        pullback.fst (I.glueDataObjι U) (X.homOfLE sorry) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι) ⊆
  (↑(↑V : X.Opens) : Set ↥X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V W U₀ : (↑X.affineOpens : Type u)
hU₀ : (↑U : X.Opens) ⊓ (↑W : X.Opens) ≤ (↑U₀ : X.Opens)
left :
  Set.range (ι :=
      ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE ⋯)) (Y := pullback (I.glueDataObjι U) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))))
      ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
          pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι) ⊆
    (↑(↑V : X.Opens) : Set ↥X)
⊢ Set.range (ι :=
        ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE ⋯)) (Y := pullback (I.glueDataObjι U) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))))
        ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
            pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι) ⊆
      (↑(↑V : X.Opens) : Set ↥X) ∧
    Set.range (ι :=
        ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE ⋯)) (Y := pullback (I.glueDataObjι U) (X.homOfLE ⋯))
            (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))))
        ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
            pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι) ⊆
      (↑(↑U₀ : X.Opens) : Set ↥X)
have right : Set.range (ι :=
    ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE sorry)) (Y := pullback (I.glueDataObjι U) (X.homOfLE sorry))
        (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry))))
    ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) ≫
        pullback.fst (I.glueDataObjι U) (X.homOfLE sorry) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι) ⊆
  (↑(↑U₀ : X.Opens) : Set ↥X)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme (goal)
Goal:
X : Scheme
I : X.IdealSheafData
U V W U₀ : (↑X.affineOpens : Type u)
hU₀ : (↑U : X.Opens) ⊓ (↑W : X.Opens) ≤ (↑U₀ : X.Opens)
⊢ Set.range (ι :=
      ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE ⋯)) (Y := pullback (I.glueDataObjι U) (X.homOfLE ⋯))
          (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))))
      ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
          pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U ≫ (↑U : X.Opens).ι) ⊆
    (↑(↑V : X.Opens) : Set ↥X)
have left : Set.range (ι :=
    ↥(pullback (X := pullback (I.glueDataObjι U) (X.homOfLE sorry)) (Y := pullback (I.glueDataObjι U) (X.homOfLE sorry))
        (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry))))
    (Function.comp (β := ↥(↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) ⇑((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι
      ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) (pullback.fst (I.glueDataObjι U) (X.homOfLE sorry)) ≫
          pullback.snd (I.glueDataObjι U) (X.homOfLE sorry))) ⊆
  (↑(↑V : X.Opens) : Set ↥X)
Tactic: rw [pullback.condition_assoc (f := I.glueDataObjι U), X.homOfLE_ι,
          ← Category.assoc, Scheme.Hom.comp_base, TopCat.coe_comp]