awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
refine : D.glued.toLocallyRingedSpace ≅ D.toLocallyRingedSpaceGlueData.glued
⊢ D.glued.toSheafedSpace ≅ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.glued

Tactic:
refine LocallyRingedSpace.forgetToSheafedSpace.mapIso ?_ ≪≫
    LocallyRingedSpace.GlueData.isoSheafedSpace _

Premises used: AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace, AlgebraicGeometry.LocallyRingedSpace.GlueData.isoSheafedSpace, CategoryTheory.Functor.mapIso
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
⊢ D.glued.toLocallyRingedSpace ≅ D.toLocallyRingedSpaceGlueData.glued

Tactic:
exact Scheme.GlueData.isoLocallyRingedSpace _

Premises used: AlgebraicGeometry.Scheme.GlueData.isoLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i : D.J
rw :
  (InducedCategory.Hom.hom (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.ι i) ≫
        (Iso.inv D.toLocallyRingedSpaceGlueData.isoSheafedSpace ≫
            (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).hom).base =
    (D.ι i).base
⊢ CategoryStruct.comp (Y :=
      D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued)
      (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)
      (Iso.inv
        (Iso.trans (Y :=
          Functor.obj (PresheafedSpace.forget CommRingCat)
            D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.glued)
          (Functor.mapIso (PresheafedSpace.forget CommRingCat)
            (Iso.trans (Y :=
              Functor.obj SheafedSpace.forgetToPresheafedSpace
                D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.glued)
              (Functor.mapIso SheafedSpace.forgetToPresheafedSpace
                  (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace ≪≫
                    D.toLocallyRingedSpaceGlueData.isoSheafedSpace) :
                Functor.obj SheafedSpace.forgetToPresheafedSpace D.glued.toSheafedSpace ≅
                  Functor.obj SheafedSpace.forgetToPresheafedSpace
                    D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.glued)
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.isoPresheafedSpace :
                D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.glued.toPresheafedSpace ≅
                  D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.glued)))
          (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.gluedIso
            (PresheafedSpace.forget CommRingCat)))) =
    (D.ι i).base

Tactic:
rw [Iso.trans_inv, GlueData.ι_gluedIso_inv_assoc, Functor.mapIso_inv, Iso.trans_inv,
    Functor.mapIso_inv, Iso.trans_inv, SheafedSpace.forgetToPresheafedSpace_map,
    PresheafedSpace.forget_map,
    PresheafedSpace.forget_map, ← PresheafedSpace.comp_base, ← Category.assoc,
    D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.ι_isoPresheafedSpace_inv i]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData, AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData, CategoryTheory.GlueData.ι_gluedIso_inv_assoc, AlgebraicGeometry.PresheafedSpace.forget_map, AlgebraicGeometry.SheafedSpace.GlueData.ι_isoPresheafedSpace_inv, AlgebraicGeometry.PresheafedSpace.comp_base, CategoryTheory.Functor.mapIso_inv, AlgebraicGeometry.SheafedSpace.forgetToPresheafedSpace_map, CategoryTheory.Iso.trans_inv
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i : D.J
dsimp :
  Hom.base
        (InducedCategory.Hom.hom
          (((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData LocallyRingedSpace.forgetToSheafedSpace).ι i)) ≫
      Hom.base (InducedCategory.Hom.hom (Iso.inv D.toLocallyRingedSpaceGlueData.isoSheafedSpace)) ≫
        D.isoLocallyRingedSpace.inv.base =
    (D.ι i).base
⊢ (InducedCategory.Hom.hom (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.ι i) ≫
        (Iso.inv D.toLocallyRingedSpaceGlueData.isoSheafedSpace ≫
            (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).hom).base =
    (D.ι i).base

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i : D.J
rw :
  (InducedCategory.Hom.hom (LocallyRingedSpace.Hom.toShHom (D.toLocallyRingedSpaceGlueData.ι i)) ≫
        D.isoLocallyRingedSpace.inv.toHom).base =
    (D.ι i).base
⊢ Hom.base
        (InducedCategory.Hom.hom
          (((D.mapGlueData forgetToLocallyRingedSpace).mapGlueData LocallyRingedSpace.forgetToSheafedSpace).ι i)) ≫
      Hom.base (InducedCategory.Hom.hom (Iso.inv D.toLocallyRingedSpaceGlueData.isoSheafedSpace)) ≫
        D.isoLocallyRingedSpace.inv.base =
    (D.ι i).base

Tactic:
rw [← Category.assoc, ← PresheafedSpace.comp_base,
    ← InducedCategory.comp_hom, D.toLocallyRingedSpaceGlueData.ι_isoSheafedSpace_inv i,
    ← PresheafedSpace.comp_base]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData, AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv, CategoryTheory.InducedCategory.comp_hom, AlgebraicGeometry.PresheafedSpace.comp_base
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i : D.J
change : (D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv).base = (D.ι i).base
⊢ (InducedCategory.Hom.hom (LocallyRingedSpace.Hom.toShHom (D.toLocallyRingedSpaceGlueData.ι i)) ≫
        D.isoLocallyRingedSpace.inv.toHom).base =
    (D.ι i).base

Tactic:
change (_ ≫ D.isoLocallyRingedSpace.inv).base = _

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.GlueData.isoLocallyRingedSpace, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i : D.J
rw rw₁ : Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom (D.ι i))) = (D.ι i).base
⊢ (D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv).base = (D.ι i).base

Tactic:
rw [D.ι_isoLocallyRingedSpace_inv i]

Premises used: AlgebraicGeometry.Scheme.GlueData.ι_isoLocallyRingedSpace_inv
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ Eq (α := ↥D.glued) ((D.ι i) x : ↥D.glued) ((D.ι j) y : ↥D.glued) ↔
    D.Rel (Sigma.mk (β := fun (i : D.J) ↦ ↥(D.U i)) i x) (Sigma.mk (β := fun (i : D.J) ↦ ↥(D.U i)) j y)

Tactic:
Iff.trans ?_
    (TopCat.GlueData.ι_eq_iff_rel
      D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData
      i j x y)

Premises used: AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData, AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData, AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData, AlgebraicGeometry.SheafedSpace.GlueData.toPresheafedSpaceGlueData, Iff.trans, TopCat.GlueData.ι_eq_iff_rel
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
refine :
  Eq (α := ↥D.glued) ((D.ι i) x : ↥D.glued) ((D.ι j) y : ↥D.glued) ↔
    Eq (α :=
      (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (Y := D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued)
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i) :
            (a :
                (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U i) :
                  Type u)) →
              (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                Type u))
          x :
        (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (Y := D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued)
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι j) :
            (a :
                (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U j) :
                  Type u)) →
              (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                Type u))
          y :
        (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued : Type u))
⊢ Eq (α := ↥D.glued) ((D.ι i) x : ↥D.glued) ((D.ι j) y : ↥D.glued) ↔
    D.Rel (Sigma.mk (β := fun (i : D.J) ↦ ↥(D.U i)) i x) (Sigma.mk (β := fun (i : D.J) ↦ ↥(D.U i)) j y)

Tactic:
refine Iff.trans ?_
    (TopCat.GlueData.ι_eq_iff_rel
      D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData
      i j x y)

Premises used: AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData, AlgebraicGeometry.Scheme.GlueData.toLocallyRingedSpaceGlueData, AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData, AlgebraicGeometry.SheafedSpace.GlueData.toPresheafedSpaceGlueData, Iff.trans, TopCat.GlueData.ι_eq_iff_rel
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
i j : D.J
x : ↥(D.U i)
y : ↥(D.U j)
⊢ Mono D.isoCarrier.inv

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
U : Set ↥D.glued
rw :
  (∀ (i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J),
      IsOpen (X :=
        (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U i) : Type u))
        (Set.preimage (β :=
          (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
            Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) (Y :=
                D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued)
                (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) :
            (a :
                (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U i) :
                  Type u)) →
              (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                Type u))
          ((⇑(TopCat.homeoOfIso D.isoCarrier.symm) :
              (a :
                  (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                    Type u)) →
                ↥D.glued) ⁻¹'
            U))) ↔
    ∀ (i : D.J), IsOpen (X := ↥(D.U i)) (⇑(D.ι i) ⁻¹' U)
⊢ IsOpen U ↔ ∀ (i : D.J), IsOpen (X := ↥(D.U i)) (⇑(D.ι i) ⁻¹' U)

Tactic:
rw [← (TopCat.homeoOfIso D.isoCarrier.symm).isOpen_preimage, TopCat.GlueData.isOpen_iff]

Premises used: TopCat.GlueData.isOpen_iff, AlgebraicGeometry.Scheme.GlueData.isoCarrier, TopCat.homeoOfIso, CategoryTheory.Iso.symm, Homeomorph.isOpen_preimage
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
U : Set ↥D.glued
h :
  ∀ (a : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J),
    IsOpen (X :=
        (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U a) : Type u))
        (Set.preimage (β :=
          (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
            Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) (Y :=
                D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued)
                (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι a)) :
            (a :
                (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U a) :
                  Type u)) →
              (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                Type u))
          ((⇑(TopCat.homeoOfIso D.isoCarrier.symm) :
              (a :
                  (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                    Type u)) →
                ↥D.glued) ⁻¹'
            U)) ↔
      IsOpen (X := ↥(D.U a)) (⇑(D.ι a) ⁻¹' U)
⊢ (∀ (i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J),
      IsOpen (X :=
        (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U i) : Type u))
        (Set.preimage (β :=
          (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
            Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) (Y :=
                D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued)
                (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) :
            (a :
                (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U i) :
                  Type u)) →
              (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                Type u))
          ((⇑(TopCat.homeoOfIso D.isoCarrier.symm) :
              (a :
                  (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                    Type u)) →
                ↥D.glued) ⁻¹'
            U))) ↔
    ∀ (i : D.J), IsOpen (X := ↥(D.U i)) (⇑(D.ι i) ⁻¹' U)

Tactic:
apply forall_congr'

Premises used: forall_congr'
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
U : Set ↥D.glued
i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J
h :
  IsOpen (X :=
      (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U i) : Type u))
      (Function.comp (β :=
          (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
            Type u))
          (⇑(TopCat.homeoOfIso D.isoCarrier.symm) :
            (a :
                (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                  Type u)) →
              ↥D.glued)
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) (Y :=
                D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued)
                (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) :
            (a :
                (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U i) :
                  Type u)) →
              (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                Type u)) ⁻¹'
        U) ↔
    IsOpen (X := ↥(D.U i))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
                D.isoCarrier.inv)) :
          (a : ↥(D.U i)) → ↥D.glued) ⁻¹'
        U)
⊢ IsOpen (X :=
      (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U i) : Type u))
      (Set.preimage (β :=
        (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (Y := D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued)
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) :
          (a :
              (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U i) :
                Type u)) →
            (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
              Type u))
        ((⇑(TopCat.homeoOfIso D.isoCarrier.symm) :
            (a :
                (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                  Type u)) →
              ↥D.glued) ⁻¹'
          U)) ↔
    IsOpen (X := ↥(D.U i)) (⇑(D.ι i) ⁻¹' U)

Tactic:
rw [← Set.preimage_comp, ← ι_isoCarrier_inv]

Premises used: Set.preimage_comp, AlgebraicGeometry.Scheme.GlueData.ι_isoCarrier_inv
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D : GlueData
U : Set ↥D.glued
i : D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.J
⊢ IsOpen (X :=
      (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U i) : Type u))
      (Function.comp (β :=
          (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
            Type u))
          (⇑(TopCat.homeoOfIso D.isoCarrier.symm) :
            (a :
                (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                  Type u)) →
              ↥D.glued)
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) (Y :=
                D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued)
                (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i)) :
            (a :
                (↑(D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.U i) :
                  Type u)) →
              (↑D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued :
                Type u)) ⁻¹'
        U) ↔
    IsOpen (X := ↥(D.U i))
      ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.ι i ≫
                D.isoCarrier.inv)) :
          (a : ↥(D.U i)) → ↥D.glued) ⁻¹'
        U)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D_1 : GlueData
D : GlueData
rw :
  (∀ (x : ↥D.glued),
      ∃ (i : { I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.I₀),
        Membership.mem (γ := Set ↥D.glued)
          (Set.range (ι := ↥({ I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.X i))
            ⇑({ I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.f i))
          x) ∧
    ∀ (i : { I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.I₀),
      IsOpenImmersion ({ I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.f i)
⊢ Membership.mem (γ := Set (Presieve D.glued)) ((precoverage IsOpenImmersion).coverings D.glued)
    { I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.presieve₀

Tactic:
rw [presieve₀_mem_precoverage_iff]

Premises used: AlgebraicGeometry.Scheme.presieve₀_mem_precoverage_iff
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D_1 : GlueData
D : GlueData
⊢ (∀ (x : ↥D.glued),
      ∃ (i : { I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.I₀),
        Membership.mem (γ := Set ↥D.glued)
          (Set.range (ι := ↥({ I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.X i))
            ⇑({ I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.f i))
          x) ∧
    ∀ (i : { I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.I₀),
      IsOpenImmersion ({ I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.f i)

Tactic:
⟨D.ι_jointly_surjective, inferInstance⟩

Premises used: inferInstance, And.intro, AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
D_1 : GlueData
D : GlueData
⊢ (∀ (x : ↥D.glued),
      ∃ (i : { I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.I₀),
        Membership.mem (γ := Set ↥D.glued)
          (Set.range (ι := ↥({ I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.X i))
            ⇑({ I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.f i))
          x) ∧
    ∀ (i : { I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.I₀),
      IsOpenImmersion ({ I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.f i)

Tactic:
exact ⟨D.ι_jointly_surjective, inferInstance⟩
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
refine :
  pullback (X := pullback (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) ⟶
    pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
      (pullback.fst (𝒰.f y) (𝒰.f x))
⊢ pullback (X := pullback (𝒰.f x) (𝒰.f y)) (Y := pullback (𝒰.f x) (𝒰.f z)) (pullback.fst (𝒰.f x) (𝒰.f y))
      (pullback.fst (𝒰.f x) (𝒰.f z)) ⟶
    pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
      (pullback.fst (𝒰.f y) (𝒰.f x))

Tactic:
refine (pullbackRightPullbackFstIso _ _ _).hom ≫ ?_

Premises used: CategoryTheory.Limits.pullbackRightPullbackFstIso, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
refine :
  pullback (X := pullback (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) ⟶
    pullback (X := pullback (𝒰.f y) (𝒰.f x)) (Y := pullback (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))
      (pullback.fst (𝒰.f y) (𝒰.f z))
⊢ pullback (X := pullback (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) ⟶
    pullback (X := pullback (𝒰.f y) (𝒰.f z)) (Y := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f z))
      (pullback.fst (𝒰.f y) (𝒰.f x))

Tactic:
refine ?_ ≫ (pullbackSymmetry _ _).hom

Premises used: CategoryTheory.Limits.pullbackSymmetry, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
refine :
  pullback (X := pullback (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) ⟶
    pullback (X := pullback (𝒰.f y) (𝒰.f x)) (pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y) (𝒰.f z)
⊢ pullback (X := pullback (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) (𝒰.f z) ⟶
    pullback (X := pullback (𝒰.f y) (𝒰.f x)) (Y := pullback (𝒰.f y) (𝒰.f z)) (pullback.fst (𝒰.f y) (𝒰.f x))
      (pullback.fst (𝒰.f y) (𝒰.f z))

Tactic:
refine ?_ ≫ (pullbackRightPullbackFstIso _ _ _).inv

Premises used: CategoryTheory.Limits.pullbackRightPullbackFstIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ X) ((pullback.fst (𝒰.f x) (𝒰.f y) ≫ 𝒰.f x) ≫ 𝟙 X)
    (Iso.hom (pullbackSymmetry (𝒰.f x) (𝒰.f y)) ≫ pullback.fst (𝒰.f y) (𝒰.f x) ≫ 𝒰.f y)

Tactic:
simp [pullback.condition]

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ 𝒰.f z ≫ 𝟙 X = 𝟙 (𝒰.X z) ≫ 𝒰.f z

Tactic:
simp