awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D : GlueData
⊢ Scheme
have apply : ∀ (x : (↑D.toLocallyRingedSpaceGlueData.glued.toTopCat : Type u)),
  ∃ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ D.toLocallyRingedSpaceGlueData.glued),
    Membership.mem (γ := Set (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u))
        (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) f.base) :
            (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u)))
        x ∧
      LocallyRingedSpace.IsOpenImmersion f
Tactic: apply LocallyRingedSpace.IsOpenImmersion.scheme
    D.toLocallyRingedSpaceGlueData.toGlueData.glued
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D : GlueData
x : (↑D.toLocallyRingedSpaceGlueData.glued.toTopCat : Type u)
⊢ ∃ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ D.toLocallyRingedSpaceGlueData.glued),
    Membership.mem (γ := Set (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u))
        (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) f.base) :
            (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u)))
        x ∧
      LocallyRingedSpace.IsOpenImmersion f
have obtain : ∀ (i : D.toLocallyRingedSpaceGlueData.J) (y : (↑(D.toLocallyRingedSpaceGlueData.U i).toTopCat : Type u)),
  ∃ (R : CommRingCat.{u}) (f : Spec.toLocallyRingedSpace.obj (op R) ⟶ D.toLocallyRingedSpaceGlueData.glued),
    Membership.mem (α := (↑D.toLocallyRingedSpaceGlueData.glued.toTopCat : Type u)) (γ :=
        Set (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u))
        (Set.range (ι := (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                TopCat.carrier) f.base) :
            (a : (↑(↑(Spec.toLocallyRingedSpace.obj (op R)).toPresheafedSpace : TopCat) : Type u)) →
              (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u)))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (Y := (↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat))
                (Hom.base (LocallyRingedSpace.Hom.toHom (D.toLocallyRingedSpaceGlueData.ι i))) :
              (a : (↑(↑(D.toLocallyRingedSpaceGlueData.U i).toPresheafedSpace : TopCat) : Type u)) →
                (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u))
            y :
          (↑(↑D.toLocallyRingedSpaceGlueData.glued.toPresheafedSpace : TopCat) : Type u)) ∧
      LocallyRingedSpace.IsOpenImmersion f
Tactic: obtain ⟨i, y, rfl⟩ := D.toLocallyRingedSpaceGlueData.ι_jointly_surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D : GlueData
i : D.J
⊢ IsOpenImmersion (Y := D.glued) (D.ι i)
have rw : LocallyRingedSpace.IsOpenImmersion (D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv)
Tactic: rw [IsOpenImmersion, ← D.ι_isoLocallyRingedSpace_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D : GlueData
⊢ (↑D.glued.toPresheafedSpace : TopCat) ≅
    D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData.glued
have refine : D.glued.toPresheafedSpace ≅ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.glued
Tactic: refine (PresheafedSpace.forget _).mapIso ?_ ≪≫
    GlueData.gluedIso _ (PresheafedSpace.forget.{_, _, u} _)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D : GlueData
⊢ D.glued.toPresheafedSpace ≅ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.glued
have refine : D.glued.toSheafedSpace ≅ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.glued
Tactic: refine SheafedSpace.forgetToPresheafedSpace.mapIso ?_ ≪≫
    SheafedSpace.GlueData.isoPresheafedSpace _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D : GlueData
⊢ D.glued.toSheafedSpace ≅ D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.glued
have refine : D.glued.toLocallyRingedSpace ≅ D.toLocallyRingedSpaceGlueData.glued
Tactic: refine LocallyRingedSpace.forgetToSheafedSpace.mapIso ?_ ≪≫
    LocallyRingedSpace.GlueData.isoSheafedSpace _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D : GlueData
i : D.J
⊢ 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
have rw : (InducedCategory.Hom.hom (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.ι i) ≫
      (Iso.inv D.toLocallyRingedSpaceGlueData.isoSheafedSpace ≫
          (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).hom).base =
  (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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D : GlueData
i : D.J
⊢ (InducedCategory.Hom.hom (D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.ι i) ≫
        (Iso.inv D.toLocallyRingedSpaceGlueData.isoSheafedSpace ≫
            (LocallyRingedSpace.forgetToSheafedSpace.mapIso D.isoLocallyRingedSpace).inv).hom).base =
    (D.ι i).base
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D : GlueData
i : D.J
⊢ 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
have rw : (InducedCategory.Hom.hom (LocallyRingedSpace.Hom.toShHom (D.toLocallyRingedSpaceGlueData.ι i)) ≫
      D.isoLocallyRingedSpace.inv.toHom).base =
  (D.ι i).base
Tactic: rw [← Category.assoc, ← PresheafedSpace.comp_base,
    ← InducedCategory.comp_hom, D.toLocallyRingedSpaceGlueData.ι_isoSheafedSpace_inv i,
    ← PresheafedSpace.comp_base]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D : GlueData
i : D.J
⊢ (InducedCategory.Hom.hom (LocallyRingedSpace.Hom.toShHom (D.toLocallyRingedSpaceGlueData.ι i)) ≫
        D.isoLocallyRingedSpace.inv.toHom).base =
    (D.ι i).base
have change : (D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv).base = (D.ι i).base
Tactic: change (_ ≫ D.isoLocallyRingedSpace.inv).base = _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D : GlueData
i : D.J
⊢ (D.toLocallyRingedSpaceGlueData.ι i ≫ D.isoLocallyRingedSpace.inv).base = (D.ι i).base
have rw : Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom (D.ι i))) = (D.ι i).base
Tactic: rw [D.ι_isoLocallyRingedSpace_inv i]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
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)
have 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))
Tactic: refine Iff.trans ?_
    (TopCat.GlueData.ι_eq_iff_rel
      D.toLocallyRingedSpaceGlueData.toSheafedSpaceGlueData.toPresheafedSpaceGlueData.toTopGlueData
      i j x y)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D : GlueData
U : Set ↥D.glued
⊢ IsOpen U ↔ ∀ (i : D.J), IsOpen (X := ↥(D.U i)) (⇑(D.ι i) ⁻¹' U)
have 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)
Tactic: rw [← (TopCat.homeoOfIso D.isoCarrier.symm).isOpen_preimage, TopCat.GlueData.isOpen_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
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))
        (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)
have 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)
Tactic: apply forall_congr'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
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))
      (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)
have 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)
Tactic: rw [← Set.preimage_comp, ← ι_isoCarrier_inv]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
D_1 : GlueData
D : GlueData
⊢ Membership.mem (γ := Set (Presieve D.glued)) ((precoverage IsOpenImmersion).coverings D.glued)
    { I₀ := D.J, X := D.U, f := D.ι : PreZeroHypercover D.glued }.presieve₀
have 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)
Tactic: rw [presieve₀_mem_precoverage_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ 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))
have 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))
Tactic: refine (pullbackRightPullbackFstIso _ _ _).hom ≫ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ 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))
have 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))
Tactic: refine ?_ ≫ (pullbackSymmetry _ _).hom
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ 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))
have 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)
Tactic: refine ?_ ≫ (pullbackRightPullbackFstIso _ _ _).inv
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
have h₀ : (gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
    pullback.fst (𝒰.f x) (𝒰.f y) =
  pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f y)
Tactic: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Gluing (goal)
Goal:
X : Scheme
𝒰 : X.OpenCover
x y z : 𝒰.I₀
h₀ :
  (gluedCoverT' 𝒰 x y z ≫
        gluedCoverT' 𝒰 y z x ≫
          gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
      pullback.fst (𝒰.f x) (𝒰.f y) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.fst (𝒰.f x) (𝒰.f y)
⊢ gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) =
    pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))
have h₁ : (gluedCoverT' 𝒰 x y z ≫
      gluedCoverT' 𝒰 y z x ≫
        gluedCoverT' 𝒰 z x y ≫ pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z))) ≫
    pullback.snd (𝒰.f x) (𝒰.f y) =
  pullback.fst (pullback.fst (𝒰.f x) (𝒰.f y)) (pullback.fst (𝒰.f x) (𝒰.f z)) ≫ pullback.snd (𝒰.f x) (𝒰.f y)
Tactic: apply pullback.hom_ext