awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : Eq (α := ↥X) ((𝒰.f i) x : ↥X) ((𝒰.f j) y : ↥X)
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt ≅
  (PullbackCone.mk (W := forgetToTop.obj (pullback (𝒰.f i) (𝒰.f j))) (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j)))
      (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j))) ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.f i) (𝒰.f j))
⊢ Eq (α :=
    ↥((gluedCover 𝒰).U
        (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
          (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x))))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).π.app WalkingCospan.left) :
          (a : (↑(TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt : Type u)) →
            ↥((gluedCover 𝒰).U ⟨i, x⟩.fst))
        (Subtype.mk (p := fun (p : (↑(forgetToTop.obj (𝒰.X i)) : Type u) × (↑(forgetToTop.obj (𝒰.X j)) : Type u)) ↦
          Eq (α := (↑(forgetToTop.obj X) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) (forgetToTop.map (𝒰.f i)) :
                  (a : (↑(forgetToTop.obj (𝒰.X i)) : Type u)) → (↑(forgetToTop.obj X) : Type u))
                p.1 :
              (↑(forgetToTop.obj X) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) (forgetToTop.map (𝒰.f j)) :
                  (a : (↑(forgetToTop.obj (𝒰.X j)) : Type u)) → (↑(forgetToTop.obj X) : Type u))
                p.2 :
              (↑(forgetToTop.obj X) : Type u)))
          (x, y) h) :
      ↥((gluedCover 𝒰).U
          (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
            (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x))))
    (Sigma.snd (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
        (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x) :
      ↥((gluedCover 𝒰).U
          (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
            (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) i x))))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
j : (gluedCover 𝒰).J
y : ↥((gluedCover 𝒰).U j)
h : Eq (α := ↥X) ((𝒰.f i) x : ↥X) ((𝒰.f j) y : ↥X)
e : (TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt ≅
  (PullbackCone.mk (W := forgetToTop.obj (pullback (𝒰.f i) (𝒰.f j))) (forgetToTop.map (pullback.fst (𝒰.f i) (𝒰.f j)))
      (forgetToTop.map (pullback.snd (𝒰.f i) (𝒰.f j))) ⋯).pt :=
  (TopCat.pullbackConeIsLimit (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).conePointUniqueUpToIso
    (isLimitOfHasPullbackOfPreservesLimit forgetToTop (𝒰.f i) (𝒰.f j))
⊢ Eq (α :=
    ↥((gluedCover 𝒰).U
        (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
          (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y))))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).π.app WalkingCospan.right) :
          (a : (↑(TopCat.pullbackCone (forgetToTop.map (𝒰.f i)) (forgetToTop.map (𝒰.f j))).pt : Type u)) →
            ↥((gluedCover 𝒰).U ⟨j, y⟩.fst))
        (Subtype.mk (p := fun (p : (↑(forgetToTop.obj (𝒰.X i)) : Type u) × (↑(forgetToTop.obj (𝒰.X j)) : Type u)) ↦
          Eq (α := (↑(forgetToTop.obj X) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) (forgetToTop.map (𝒰.f i)) :
                  (a : (↑(forgetToTop.obj (𝒰.X i)) : Type u)) → (↑(forgetToTop.obj X) : Type u))
                p.1 :
              (↑(forgetToTop.obj X) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) (forgetToTop.map (𝒰.f j)) :
                  (a : (↑(forgetToTop.obj (𝒰.X j)) : Type u)) → (↑(forgetToTop.obj X) : Type u))
                p.2 :
              (↑(forgetToTop.obj X) : Type u)))
          (x, y) h) :
      ↥((gluedCover 𝒰).U
          (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
            (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y))))
    (Sigma.snd (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
        (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y) :
      ↥((gluedCover 𝒰).U
          (Sigma.fst (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i))
            (Sigma.mk (β := fun (i : (gluedCover 𝒰).J) ↦ ↥((gluedCover 𝒰).U i)) j y))))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x : ↥(gluedCover 𝒰).glued
obtain :
  ∀ (i : (gluedCover 𝒰).J) (x : ↥((gluedCover 𝒰).U i)),
    IsIso (X := X.presheaf.stalk ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)))
      (Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x))
⊢ IsIso (Hom.stalkMap (fromGlued 𝒰) x)

Tactic:
obtain ⟨i, x, rfl⟩ := 𝒰.gluedCover.ι_jointly_surjective x

Premises used: AlgebraicGeometry.Scheme.Cover.gluedCover, AlgebraicGeometry.Scheme.GlueData.ι_jointly_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
⊢ Hom.stalkMap ((gluedCover 𝒰).ι i ≫ fromGlued 𝒰) x = Iso.hom (X.presheaf.stalkCongr ⋯) ≫ Hom.stalkMap (𝒰.f i) x

Tactic:
have := Hom.stalkMap_congr_hom _ _ (𝒰.ι_fromGlued i) x
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
this : Hom.stalkMap ((gluedCover 𝒰).ι i ≫ fromGlued 𝒰) x = Iso.hom (X.presheaf.stalkCongr ⋯) ≫ Hom.stalkMap (𝒰.f i) x
⊢ Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) =
    (Iso.hom (X.presheaf.stalkCongr ⋯) ≫ Hom.stalkMap (𝒰.f i) x) ≫ inv (Hom.stalkMap ((gluedCover 𝒰).ι i) x)

Tactic:
rw [Hom.stalkMap_comp, ← IsIso.eq_comp_inv] at this

Premises used: CategoryTheory.IsIso.eq_comp_inv, AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
this :
  Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) =
    (Iso.hom (X.presheaf.stalkCongr ⋯) ≫ Hom.stalkMap (𝒰.f i) x) ≫ inv (Hom.stalkMap ((gluedCover 𝒰).ι i) x)
rw :
  IsIso (X := X.presheaf.stalk ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)))
    ((Iso.hom (X.presheaf.stalkCongr ⋯) ≫ Hom.stalkMap (𝒰.f i) x) ≫ inv (Hom.stalkMap ((gluedCover 𝒰).ι i) x))
⊢ IsIso (X := X.presheaf.stalk ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)))
    (Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x))

Tactic:
rw [this]
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
i : (gluedCover 𝒰).J
x : ↥((gluedCover 𝒰).U i)
this :
  Hom.stalkMap (fromGlued 𝒰) (((gluedCover 𝒰).ι i) x) =
    (Iso.hom (X.presheaf.stalkCongr ⋯) ≫ Hom.stalkMap (𝒰.f i) x) ≫ inv (Hom.stalkMap ((gluedCover 𝒰).ι i) x)
⊢ IsIso (X := X.presheaf.stalk ((fromGlued 𝒰) (((gluedCover 𝒰).ι i) x : ↥(gluedCover 𝒰).glued)))
    ((Iso.hom (X.presheaf.stalkCongr ⋯) ≫ Hom.stalkMap (𝒰.f i) x) ≫ inv (Hom.stalkMap ((gluedCover 𝒰).ι i) x))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : IsOpen U
rw : ∀ (x : ↥X), Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x → ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t
⊢ IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U)

Tactic:
rw [isOpen_iff_forall_mem_open]

Premises used: isOpen_iff_forall_mem_open
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : IsOpen U
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
rw :
  ∀ (hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)) (x : ↥X)
    (hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x), ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t
⊢ ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t

Tactic:
rw [𝒰.gluedCover.isOpen_iff] at hU

Premises used: AlgebraicGeometry.Scheme.GlueData.isOpen_iff, AlgebraicGeometry.Scheme.Cover.gluedCover
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
h :
  Subset (α := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x)))
      (⇑(fromGlued 𝒰) '' U) ∧
    IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) ∧
      Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) x
⊢ ∃ t ⊆ ⇑(fromGlued 𝒰) '' U, IsOpen t ∧ x ∈ t

Tactic:
use 𝒰.fromGlued '' U ∩ Set.range (𝒰.f (𝒰.idx x))

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Cover.fromGlued, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, Set.range, AlgebraicGeometry.Scheme.Cover.idx, DFunLike.coe, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
right :
  IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) ∧
    Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) x
⊢ Subset (α := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x)))
      (⇑(fromGlued 𝒰) '' U) ∧
    IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) ∧
      Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) x

Tactic:
use Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
right : IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x)))
right₁ : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) x
⊢ IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) ∧
    Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) x

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
right :
  IsOpen (X := ↥X)
    (Set.image (α := ↥(𝒰.X (idx 𝒰 x))) (⇑(𝒰.f (idx 𝒰 x)))
      (Set.preimage (β := ↥X) (⇑(𝒰.f (idx 𝒰 x))) (⇑(fromGlued 𝒰) '' U)))
⊢ IsOpen (X := ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x)))

Tactic:
rw [← Set.image_preimage_eq_inter_range]

Premises used: Set.image_preimage_eq_inter_range
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
right : IsOpen (X := ↥(𝒰.X (idx 𝒰 x))) (Set.preimage (β := ↥X) (⇑(𝒰.f (idx 𝒰 x))) (⇑(fromGlued 𝒰) '' U))
⊢ IsOpen (X := ↥X)
    (Set.image (α := ↥(𝒰.X (idx 𝒰 x))) (⇑(𝒰.f (idx 𝒰 x)))
      (Set.preimage (β := ↥X) (⇑(𝒰.f (idx 𝒰 x))) (⇑(fromGlued 𝒰) '' U)))

Tactic:
apply (𝒰.f (𝒰.idx x)).isOpenEmbedding.isOpenMap

Premises used: CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.isOpenMap, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.Scheme.Cover.idx, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
⊢ IsOpen (X := ↥((gluedCover 𝒰).U (idx 𝒰 x))) (⇑((gluedCover 𝒰).ι (idx 𝒰 x)) ⁻¹' U)

Tactic:
hU (𝒰.idx x)

Premises used: AlgebraicGeometry.Scheme.Cover.idx
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
h :
  ↥(𝒰.X (idx 𝒰 x)) = ↥((gluedCover 𝒰).U (idx 𝒰 x)) →
    Eq (α := Set ↥(𝒰.X (idx 𝒰 x))) (Set.preimage (β := ↥X) (⇑(𝒰.f (idx 𝒰 x))) (⇑(fromGlued 𝒰) '' U))
      (⇑((gluedCover 𝒰).ι (idx 𝒰 x)) ⁻¹' U)
⊢ IsOpen (X := ↥(𝒰.X (idx 𝒰 x))) (Set.preimage (β := ↥X) (⇑(𝒰.f (idx 𝒰 x))) (⇑(fromGlued 𝒰) '' U))

Tactic:
convert! hU (𝒰.idx x) using 1

Premises used: AlgebraicGeometry.Scheme.Cover.idx
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
e_1 : ↥(𝒰.X (idx 𝒰 x)) = ↥((gluedCover 𝒰).U (idx 𝒰 x))
h :
  Eq (α := Set ↥(𝒰.X (idx 𝒰 x)))
    (Set.preimage (β := ↥(gluedCover 𝒰).glued)
      (⇑(TopCat.Hom.hom (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((gluedCover 𝒰).ι (idx 𝒰 x))))) :
            C(↥(𝒰.X (idx 𝒰 x)), ↥(gluedCover 𝒰).glued)) :
        (a : ↥(𝒰.X (idx 𝒰 x))) → ↥(gluedCover 𝒰).glued)
      (Set.preimage (β := ↥X) (⇑(TopCat.Hom.hom (fromGlued 𝒰).base) : (a : ↥(gluedCover 𝒰).glued) → ↥X)
        ((fun (a : ↥(gluedCover 𝒰).glued) ↦ (fromGlued 𝒰) a) '' U)))
    (⇑((gluedCover 𝒰).ι (idx 𝒰 x)) ⁻¹' U)
⊢ Eq (α := Set ↥(𝒰.X (idx 𝒰 x))) (Set.preimage (β := ↥X) (⇑(𝒰.f (idx 𝒰 x))) (⇑(fromGlued 𝒰) '' U))
    (⇑((gluedCover 𝒰).ι (idx 𝒰 x)) ⁻¹' U)

Tactic:
simp only [← ι_fromGlued, gluedCover_U, Hom.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp,
      Set.preimage_comp]

Premises used: AlgebraicGeometry.Scheme.Cover.gluedCover_U, ContinuousMap.coe_comp, Set.preimage_comp, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.hom_comp, AlgebraicGeometry.Scheme.Cover.ι_fromGlued
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
e_1 : ↥(𝒰.X (idx 𝒰 x)) = ↥((gluedCover 𝒰).U (idx 𝒰 x))
h :
  Set.preimage (β := ↥X) (⇑(TopCat.Hom.hom (fromGlued 𝒰).base) : (a : ↥(gluedCover 𝒰).glued) → ↥X)
      ((fun (a : ↥(gluedCover 𝒰).glued) ↦ (fromGlued 𝒰) a) '' U) =
    U
⊢ Eq (α := Set ↥(𝒰.X (idx 𝒰 x)))
    (Set.preimage (β := ↥(gluedCover 𝒰).glued)
      (⇑(TopCat.Hom.hom (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((gluedCover 𝒰).ι (idx 𝒰 x))))) :
            C(↥(𝒰.X (idx 𝒰 x)), ↥(gluedCover 𝒰).glued)) :
        (a : ↥(𝒰.X (idx 𝒰 x))) → ↥(gluedCover 𝒰).glued)
      (Set.preimage (β := ↥X) (⇑(TopCat.Hom.hom (fromGlued 𝒰).base) : (a : ↥(gluedCover 𝒰).glued) → ↥X)
        ((fun (a : ↥(gluedCover 𝒰).glued) ↦ (fromGlued 𝒰) a) '' U)))
    (⇑((gluedCover 𝒰).ι (idx 𝒰 x)) ⁻¹' U)

Tactic:
congr! 1
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
e_1 : ↥(𝒰.X (idx 𝒰 x)) = ↥((gluedCover 𝒰).U (idx 𝒰 x))
⊢ Set.preimage (β := ↥X) (⇑(TopCat.Hom.hom (fromGlued 𝒰).base) : (a : ↥(gluedCover 𝒰).glued) → ↥X)
      ((fun (a : ↥(gluedCover 𝒰).glued) ↦ (fromGlued 𝒰) a) '' U) =
    U

Tactic:
Set.preimage_image_eq _ 𝒰.fromGlued_injective

Premises used: Set.preimage_image_eq, AlgebraicGeometry.Scheme.Cover.fromGlued_injective
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
e_1 : ↥(𝒰.X (idx 𝒰 x)) = ↥((gluedCover 𝒰).U (idx 𝒰 x))
⊢ Set.preimage (β := ↥X) (⇑(TopCat.Hom.hom (fromGlued 𝒰).base) : (a : ↥(gluedCover 𝒰).glued) → ↥X)
      ((fun (a : ↥(gluedCover 𝒰).glued) ↦ (fromGlued 𝒰) a) '' U) =
    U

Tactic:
exact Set.preimage_image_eq _ 𝒰.fromGlued_injective

Premises used: Set.preimage_image_eq, AlgebraicGeometry.Scheme.Cover.fromGlued_injective
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
⊢ Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) x

Tactic:
⟨hx, 𝒰.covers x⟩

Premises used: Set.Mem, setOf, AlgebraicGeometry.Scheme.Cover.covers, Set.inter, And.intro
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
U : Set ↥(gluedCover 𝒰).glued
hU : ∀ (i : (gluedCover 𝒰).J), IsOpen (X := ↥((gluedCover 𝒰).U i)) (⇑((gluedCover 𝒰).ι i) ⁻¹' U)
x : ↥X
hx : Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U) x
⊢ Membership.mem (γ := Set ↥X) (⇑(fromGlued 𝒰) '' U ∩ Set.range (ι := ↥(𝒰.X (idx 𝒰 x))) ⇑(𝒰.f (idx 𝒰 x))) x

Tactic:
exact ⟨hx, 𝒰.covers x⟩
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
⊢ Continuous (X := ↥(gluedCover 𝒰).glued) (Y := ↥X) ⇑(fromGlued 𝒰)

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
rw : Function.Surjective (α := ↥(gluedCover 𝒰).glued) (β := ↥X) ⇑(fromGlued 𝒰)
⊢ Epi (fromGlued 𝒰).base

Tactic:
rw [TopCat.epi_iff_surjective]

Premises used: TopCat.epi_iff_surjective
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x : ↥X
obtain : ∀ (y : ↥(𝒰.X (idx 𝒰 x))) (h : (𝒰.f (idx 𝒰 x)) y = x), ∃ (a : ↥(gluedCover 𝒰).glued), (fromGlued 𝒰) a = x
⊢ ∃ (a : ↥(gluedCover 𝒰).glued), (fromGlued 𝒰) a = x

Tactic:
obtain ⟨y, h⟩ := 𝒰.covers x

Premises used: AlgebraicGeometry.Scheme.Cover.covers
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : (𝒰.f (idx 𝒰 x)) y = x
h₁ : (fromGlued 𝒰) (((gluedCover 𝒰).ι (idx 𝒰 x)) y : ↥(gluedCover 𝒰).glued) = x
⊢ ∃ (a : ↥(gluedCover 𝒰).glued), (fromGlued 𝒰) a = x

Tactic:
use 𝒰.gluedCover.ι (𝒰.idx x) y

Premises used: AlgebraicGeometry.Scheme.GlueData.ι, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Cover.gluedCover, AlgebraicGeometry.Scheme.Cover.idx, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : (𝒰.f (idx 𝒰 x)) y = x
h₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
          (↑((gluedCover 𝒰).U (idx 𝒰 x)).toPresheafedSpace : TopCat))
          (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((gluedCover 𝒰).ι (idx 𝒰 x)))) ≫ (fromGlued 𝒰).base) :
        (a : ↥((gluedCover 𝒰).U (idx 𝒰 x))) → ↥X)
      y =
    x
⊢ (fromGlued 𝒰) (((gluedCover 𝒰).ι (idx 𝒰 x)) y : ↥(gluedCover 𝒰).glued) = x

Tactic:
rw [← ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : (𝒰.f (idx 𝒰 x)) y = x
⊢ ((gluedCover 𝒰).ι (idx 𝒰 x) ≫ fromGlued 𝒰) y = x

Tactic:
rw [← 𝒰.ι_fromGlued (𝒰.idx x)] at h

Premises used: AlgebraicGeometry.Scheme.Cover.idx, AlgebraicGeometry.Scheme.Cover.ι_fromGlued
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : ((gluedCover 𝒰).ι (idx 𝒰 x) ≫ fromGlued 𝒰) y = x
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
          (↑((gluedCover 𝒰).U (idx 𝒰 x)).toPresheafedSpace : TopCat))
          (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((gluedCover 𝒰).ι (idx 𝒰 x)))) ≫ (fromGlued 𝒰).base) :
        (a : ↥((gluedCover 𝒰).U (idx 𝒰 x))) → ↥X)
      y =
    x

Tactic:
h
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
x : ↥X
y : ↥(𝒰.X (idx 𝒰 x))
h : ((gluedCover 𝒰).ι (idx 𝒰 x) ≫ fromGlued 𝒰) y = x
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) (X :=
          (↑((gluedCover 𝒰).U (idx 𝒰 x)).toPresheafedSpace : TopCat))
          (Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' ((gluedCover 𝒰).ι (idx 𝒰 x)))) ≫ (fromGlued 𝒰).base) :
        (a : ↥((gluedCover 𝒰).U (idx 𝒰 x))) → ↥X)
      y =
    x

Tactic:
exact h
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
⊢ IsOpenImmersion (fromGlued 𝒰)

Tactic:
IsOpenImmersion.of_isIso_stalkMap _ 𝒰.isOpenEmbedding_fromGlued

Premises used: AlgebraicGeometry.Scheme.Cover.isOpenEmbedding_fromGlued, AlgebraicGeometry.IsOpenImmersion.of_isIso_stalkMap
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
F : Scheme ⥤ PresheafedSpace CommRingCat :=
  forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace
change : IsIso (fromGlued 𝒰).toPshHom
⊢ IsIso (F.map (fromGlued 𝒰))

Tactic:
change IsIso 𝒰.fromGlued.toPshHom

Premises used: CategoryTheory.IsIso, AlgebraicGeometry.PresheafedSpace.Hom.toPshHom, AlgebraicGeometry.Scheme.Cover.fromGlued, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom'
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰 : X.OpenCover
F : Scheme ⥤ PresheafedSpace CommRingCat :=
  forgetToLocallyRingedSpace ⋙ LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace
⊢ IsIso (fromGlued 𝒰).toPshHom

Tactic:
apply PresheafedSpace.IsOpenImmersion.to_iso

Premises used: AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.to_iso
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
X : Scheme
𝒰_1 : X.OpenCover
𝒰 : OpenCover.{v, u} X
Y : Scheme
f : (x : 𝒰.I₀) → 𝒰.X x ⟶ Y
hf :
  ∀ (x y : 𝒰.I₀),
    Eq (α := pullback (𝒰.f x) (𝒰.f y) ⟶ Y) (pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x) (pullback.snd (𝒰.f x) (𝒰.f y) ≫ f y)
refine : (ulift (P := IsOpenImmersion) 𝒰).gluedCover.glued ⟶ Y
⊢ X ⟶ Y

Tactic:
refine inv 𝒰.ulift.fromGlued ≫ ?_

Premises used: AlgebraicGeometry.Scheme.Cover.fromGlued, CategoryTheory.inv, AlgebraicGeometry.Scheme.Cover.ulift