awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 (α := (↑Γ(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
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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))
refine_1 :
  Eq (α := (↑Γ(pullback (I.glueDataObjι U) (X.homOfLE ⋯), ⊤) : Type u))
    ((CommRingCat.Hom.hom
            (Hom.app (↑U : X.Opens).ι (↑V : X.Opens) ≫
              Hom.appLE (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U)
                ((↑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))
⊢ 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))

Tactic:
simp_rw [F, ← pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯)
enter : I.glueDataObjι V
| Hom.liftQuotient (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) (I.ideal V) ⋯ ≫ I.glueDataObjι V

Tactic:
enter [2]
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯)
enter : Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ (IsAffineOpen.isoSpec ⋯).inv
| Hom.liftQuotient (F ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom) (I.ideal V) ⋯ ≫ I.glueDataObjι V

Tactic:
enter [2]; rw [glueDataObjι]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
⊢ (↑U : X.Opens) ⊓ (↑V : X.Opens) ≤ (↑V : X.Opens) ⊓ (↑U : X.Opens)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
⊢ I.glueDataT U V ≫ pullback.snd (I.glueDataObjι V) (X.homOfLE ⋯) =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
pullback.lift_snd _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_snd
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯

Tactic:
(pullback.lift_fst_assoc _ _ _ _).trans ?_

Premises used: CategoryTheory.Limits.pullback.lift_fst_assoc, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
refine :
  Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
        (I.ideal V) ⋯ ≫
      I.glueDataObjι V =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯
⊢ I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueDataObjι V =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
refine (pullback.lift_fst_assoc _ _ _ _).trans ?_

Premises used: CategoryTheory.Limits.pullback.lift_fst_assoc, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
enter : I.glueDataObjι V
| Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
      (I.ideal V) ⋯ ≫
    I.glueDataObjι V

Tactic:
enter [2]
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V : (↑X.affineOpens : Type u)
enter : Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ (IsAffineOpen.isoSpec ⋯).inv
| Hom.liftQuotient (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯ ≫ (IsAffineOpen.isoSpec ⋯).hom)
      (I.ideal V) ⋯ ≫
    I.glueDataObjι V

Tactic:
enter [2]; rw [glueDataObjι]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯)
rw₄ rw₅ :
  Eq (α := I.glueDataObjPullback U V ⟶ (↑(↑V : X.Opens) : Scheme))
    (pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯)
    (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 ⋯

Tactic:
rw [Scheme.Hom.liftQuotient_comp_assoc, Category.assoc, Category.assoc, Iso.hom_inv_id,
    Category.comp_id]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id, AlgebraicGeometry.Scheme.Hom.liftQuotient_comp_assoc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V W U₀ : (↑X.affineOpens : Type u)
hU₀ : (↑U : X.Opens) ⊓ (↑W : X.Opens) ≤ (↑U₀ : X.Opens)
simp :
  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)
⊢ 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)).ι)

Tactic:
simp only [Scheme.Opens.range_ι, TopologicalSpace.Opens.coe_inf, Set.subset_inter_iff]

Premises used: Set.subset_inter_iff, AlgebraicGeometry.Scheme.Opens.range_ι, TopologicalSpace.Opens.coe_inf
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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)
right :
  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)
⊢ 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)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯))))
      (Function.comp (β := ↥(↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) ⇑((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι
        ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
            pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯))) ⊆
    (↑(↑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)

Tactic:
rw [pullback.condition_assoc (f := I.glueDataObjι U), X.homOfLE_ι,
          ← Category.assoc, Scheme.Hom.comp_base, TopCat.coe_comp]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.homOfLE_ι, CategoryTheory.Limits.pullback.condition_assoc, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 (ι := ↥(↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) ⇑((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι ⊆
    (↑(↑V : X.Opens) : Set ↥X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯))))
      (Function.comp (β := ↥(↑((↑U : X.Opens) ⊓ (↑V : X.Opens)) : Scheme)) ⇑((↑U : X.Opens) ⊓ (↑V : X.Opens)).ι
        ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
            pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯))) ⊆
    (↑(↑V : X.Opens) : Set ↥X)

Tactic:
exact (Set.range_comp_subset_range _ _).trans (by simp)

Premises used: Set.range_comp_subset_range, HasSubset.Subset.trans
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V W U₀ : (↑X.affineOpens : Type u)
hU₀ : (↑U : X.Opens) ⊓ (↑W : X.Opens) ≤ (↑U₀ : X.Opens)
right :
  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 ⋯))))
      (Function.comp (β := ↥(↑((↑U : X.Opens) ⊓ (↑W : X.Opens)) : Scheme)) ⇑((↑U : X.Opens) ⊓ (↑W : X.Opens)).ι
        ⇑(pullback.snd (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
            pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯))) ⊆
    (↑(↑U₀ : 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)

Tactic:
rw [pullback.condition_assoc, pullback.condition_assoc, X.homOfLE_ι,
          ← Category.assoc, Scheme.Hom.comp_base, TopCat.coe_comp]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.homOfLE_ι, CategoryTheory.Limits.pullback.condition_assoc, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 (ι := ↥(↑((↑U : X.Opens) ⊓ (↑W : X.Opens)) : Scheme)) ⇑((↑U : X.Opens) ⊓ (↑W : X.Opens)).ι ⊆
    (↑(↑U₀ : X.Opens) : Set ↥X)

Tactic:
simpa using hU₀
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
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 ⋯))))
      (Function.comp (β := ↥(↑((↑U : X.Opens) ⊓ (↑W : X.Opens)) : Scheme)) ⇑((↑U : X.Opens) ⊓ (↑W : X.Opens)).ι
        ⇑(pullback.snd (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
            pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯))) ⊆
    (↑(↑U₀ : X.Opens) : Set ↥X)

Tactic:
exact (Set.range_comp_subset_range _ _).trans (by simpa using hU₀)

Premises used: Set.range_comp_subset_range, HasSubset.Subset.trans
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V W U₀ : (↑X.affineOpens : Type u)
hU₀ : (↑U : X.Opens) ⊓ (↑W : X.Opens) ≤ (↑U₀ : X.Opens)
rw :
  ((pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
          I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) ≫
        I.glueDataObjι V) ≫
      (↑V : X.Opens).ι =
    (IsOpenImmersion.lift ((↑V : X.Opens) ⊓ (↑U₀ : X.Opens)).ι
          (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).ι)
          ⋯ ≫
        X.homOfLE ⋯) ≫
      (↑V : X.Opens).ι
⊢ (pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
        I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) ≫
      I.glueDataObjι V =
    IsOpenImmersion.lift ((↑V : X.Opens) ⊓ (↑U₀ : X.Opens)).ι
        (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).ι)
        ⋯ ≫
      X.homOfLE ⋯

Tactic:
rw [← cancel_mono (Scheme.Opens.ι _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V W U₀ : (↑X.affineOpens : Type u)
hU₀ : (↑U : X.Opens) ⊓ (↑W : X.Opens) ≤ (↑U₀ : X.Opens)
⊢ ((pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
          I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) ≫
        I.glueDataObjι V) ≫
      (↑V : X.Opens).ι =
    (IsOpenImmersion.lift ((↑V : X.Opens) ⊓ (↑U₀ : X.Opens)).ι
          (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).ι)
          ⋯ ≫
        X.homOfLE ⋯) ≫
      (↑V : X.Opens).ι

Tactic:
simp [pullback.condition_assoc]

Premises used: CategoryTheory.Limits.pullback.condition_assoc
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V W U₀ : (↑X.affineOpens : Type u)
hU₀ : (↑U : X.Opens) ⊓ (↑W : X.Opens) ≤ (↑U₀ : X.Opens)
⊢ I.glueDataT'Aux U V W U₀ hU₀ ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) =
    pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)

Tactic:
pullback.lift_fst _ _ _

Premises used: CategoryTheory.Limits.pullback.lift_fst
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
U V W U₀ : (↑X.affineOpens : Type u)
hU₀ : (↑U : X.Opens) ⊓ (↑W : X.Opens) ≤ (↑U₀ : X.Opens)
⊢ I.glueDataT'Aux U V W U₀ hU₀ ≫ pullback.snd (I.glueDataObjι V) (X.homOfLE ⋯) ≫ ((↑V : X.Opens) ⊓ (↑U₀ : X.Opens)).ι =
    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).ι

Tactic:
(pullback.lift_snd_assoc _ _ _ _).trans (IsOpenImmersion.lift_fac _ _ _)

Premises used: CategoryTheory.Limits.pullback.lift_snd_assoc, AlgebraicGeometry.IsOpenImmersion.lift_fac, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
i : (↑X.affineOpens : Type u)
⊢ (↑i : X.Opens) ≤ (↑i : X.Opens) ⊓ (↑i : X.Opens)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
i : (↑X.affineOpens : Type u)
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 (↑((↑i : X.Opens) ⊓ (↑i : X.Opens)) : Scheme)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
i : (↑X.affineOpens : Type u)
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 (↑(↑i : X.Opens) : Scheme)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
i : (↑X.affineOpens : Type u)
h₀ :
  I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)
h₁ :
  I.glueDataT i i ≫ pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.snd (I.glueDataObjι i) (X.homOfLE ⋯)
⊢ I.glueDataT i i = 𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2)

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext
-- Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
Goal:
X : Scheme
I : X.IdealSheafData
i : (↑X.affineOpens : Type u)
h₀ :
  (I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫ I.glueDataObjι i =
    (𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫ I.glueDataObjι i
⊢ I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯) =
    𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)

Tactic:
rw [← cancel_mono (glueDataObjι _ _)]

Premises used: AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι, CategoryTheory.cancel_mono