awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlj : l ⟶ k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
y : (F ⋙ forget).obj l
hy₁ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hli) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₁.fst))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
          Iso.inv (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
        x :
      ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
hy₂ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlj) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
          Iso.inv (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
        x :
      ↥(F.obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ Iso.hom (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
    (F.map hlj ≫ Iso.hom (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) ⋯
this_1 : IsOpenImmersion α
this : α y = x
⊢ ∃ (U_1 : (pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂)).Opens),
    x ∈ U_1 ∧
      U_1.ι ≫
          pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            Iso.inv (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) ≫
              F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2 =
        U_1.ι ≫
          pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
            Iso.inv (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) ≫
              F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2

Tactic:
⟨α.opensRange, ⟨y, this⟩, ?_⟩

Premises used: AlgebraicGeometry.Scheme.Hom.opensRange, And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
i j : J
k₁ k₂ : (k : J) × (k ⟶ i) × (k ⟶ j)
U : (F.obj i).Opens
h₁ : Hom.opensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) ≤ U
h₂ : Hom.opensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1) ≤ U
x : ↥(pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂))
l : J
hli : l ⟶ k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
hlj : l ⟶ k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
y : (F ⋙ forget).obj l
hy₁ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hli) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₁.fst))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
          Iso.inv (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
        x :
      ↥(F.obj (k₁.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
hy₂ :
  Eq (α := (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map hlj) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj k₂.fst))
        y :
      (fun (X : Type u) ↦ X) ((F ⋙ forget).obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
    ((pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
          Iso.inv (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
        x :
      ↥(F.obj (k₂.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)))))
α : F.obj l ⟶ pullback ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) :=
  pullback.lift (F.map hli ≫ Iso.hom (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
    (F.map hlj ≫ Iso.hom (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))) ⋯
this_1 : IsOpenImmersion α
this : α y = x
⊢ Iso.hom (Hom.isoOpensRange α) ≫
      (Hom.opensRange α).ι ≫
        pullback.fst ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
          Iso.inv (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) ≫
            F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2 =
    Iso.hom (Hom.isoOpensRange α) ≫
      (Hom.opensRange α).ι ≫
        pullback.snd ((F.obj i).homOfLE h₁) ((F.obj i).homOfLE h₂) ≫
          Iso.inv (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) ≫
            F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2

Tactic:
simp [α, ← Functor.map_comp, Subsingleton.elim (hli ≫ k₁.2.2) (hlj ≫ k₂.2.2)]

Premises used: CategoryTheory.CategoryStruct.comp, CategoryTheory.Functor.map_comp, Subsingleton.elim, Sigma.snd, Prod.snd
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
i j : J
k₁ k₂ :
  PreZeroHypercover.I₀ (S :=
    (↑(⨆ (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)), Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) :
      Scheme))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Opens.iSupOpenCover fun (k : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦
        Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
⊢ Eq.{u + 1} (α :=
    pullback (X := (↑(Hom.opensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) : Scheme)) (Y :=
        (↑(Hom.opensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) : Scheme)) (Z :=
        (↑(⨆ (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)),
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) :
          Scheme))
        ((F.obj i).homOfLE ⋯) ((F.obj i).homOfLE ⋯) ⟶
      F.obj j)
    (pullback.fst ((F.obj i).homOfLE ⋯) ((F.obj i).homOfLE ⋯) ≫
      Iso.inv (Hom.isoOpensRange (F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) ≫
        F.map k₁.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2)
    (pullback.snd ((F.obj i).homOfLE ⋯) ((F.obj i).homOfLE ⋯) ≫
      Iso.inv (Hom.isoOpensRange (F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) ≫
        F.map k₂.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2)

Tactic:
apply fst_inv_eq_snd_inv F

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.fst_inv_eq_snd_inv
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
i j k : J
fi : k ⟶ i
fj : k ⟶ j
⊢ Eq (α :=
    (↑(Hom.opensRange (X :=
            F.obj
              (Sigma.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
                (Sigma.mk (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)) k (fi, fj))))
            (F.map
              (Sigma.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
                  (Sigma.mk (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)) k (fi, fj))).1)) :
        Scheme) ⟶
      F.obj j)
    (CategoryStruct.comp (Y :=
        (↑(⨆ (k : (k : J) × (k ⟶ i) × (k ⟶ j)), Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) :
          Scheme))
        ((F.obj i).homOfLE ⋯ :
          (↑(Hom.opensRange (X :=
                  F.obj
                    (Sigma.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
                      (Sigma.mk (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)) k (fi, fj))))
                  (F.map
                    (Sigma.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
                        (Sigma.mk (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)) k (fi, fj))).1)) :
              Scheme) ⟶
            (↑(⨆ (k : (k : J) × (k ⟶ i) × (k ⟶ j)),
                  Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) :
              Scheme))
        (tAux F i j : (↑(V F i j) : Scheme) ⟶ F.obj j) :
      (↑(Hom.opensRange (X :=
              F.obj
                (Sigma.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
                  (Sigma.mk (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)) k (fi, fj))))
              (F.map
                (Sigma.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))
                    (Sigma.mk (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)) k (fi, fj))).1)) :
          Scheme) ⟶
        F.obj j)
    (Iso.inv (Hom.isoOpensRange (F.map fi)) ≫ F.map fj : (↑(Hom.opensRange (F.map fi)) : Scheme) ⟶ F.obj j)

Tactic:
(Scheme.Opens.iSupOpenCover (J := Σ k, (k ⟶ i) × (k ⟶ j)) _).ι_glueMorphisms _ _ ⟨k, fi, fj⟩

Premises used: Set.Mem, Prod.mk, AlgebraicGeometry.Scheme.restrict, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms, Sigma.mk, AlgebraicGeometry.Scheme.Opens.iSupOpenCover, AlgebraicGeometry.Scheme.Opens.toScheme
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
i j : J
x : ↥(↑(V F i j) : Scheme)
obtain :
  ∀
    (l :
      PreZeroHypercover.I₀ (S :=
        (↑(⨆ (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)),
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) :
          Scheme))
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1))))
    (x :
      ↥(PreZeroHypercover.X
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
          l)),
    Membership.mem (α := ↥(F.obj j)) (γ := Set ↥(F.obj j)) (Set.range (ι := ↥(↑(V F j i) : Scheme)) ⇑(V F j i).ι)
      ((tAux F i j)
          ((PreZeroHypercover.f
                (Precoverage.ZeroHypercover.toPreZeroHypercover
                  (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
                l)
              x :
            ↥(↑(⨆ (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)),
                    Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) :
                Scheme)) :
        ↥(F.obj j))
⊢ Membership.mem (α := ↥(F.obj j)) (γ := Set ↥(F.obj j)) (Set.range (ι := ↥(↑(V F j i) : Scheme)) ⇑(V F j i).ι)
    ((tAux F i j) x : ↥(F.obj j))

Tactic:
obtain ⟨l, x, rfl⟩ := (Scheme.Opens.iSupOpenCover _).exists_eq x

Premises used: AlgebraicGeometry.Scheme.Cover.exists_eq, AlgebraicGeometry.Scheme.Opens.iSupOpenCover, rfl
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
i j : J
l :
  PreZeroHypercover.I₀ (S :=
    (↑(⨆ (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)), Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) :
      Scheme))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦
        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
x :
  ↥(PreZeroHypercover.X
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦
          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
      l)
simp :
  Membership.mem (α := ↥(F.obj j)) (γ := Set ↥(F.obj j))
    (Set.range (ι :=
      ↥(↑(⨆ (k : (k : J) × (k ⟶ j) × (k ⟶ i)), Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ j) × (k ⟶ i)).1)) :
          Scheme))
      ⇑(Opens.ι
          (⨆ (k : (k : J) × (k ⟶ j) × (k ⟶ i)), Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ j) × (k ⟶ i)).1))))
    ((Iso.inv (Hom.isoOpensRange (F.map l.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) ≫
          F.map l.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2)
        x :
      ↥(F.obj j))
⊢ Membership.mem (α := ↥(F.obj j)) (γ := Set ↥(F.obj j)) (Set.range (ι := ↥(↑(V F j i) : Scheme)) ⇑(V F j i).ι)
    ((tAux F i j)
        ((PreZeroHypercover.f
              (Precoverage.ZeroHypercover.toPreZeroHypercover
                (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦
                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
              l)
            x :
          ↥(↑(⨆ (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)),
                  Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) :
              Scheme)) :
      ↥(F.obj j))

Tactic:
simp only [V, tAux, ← Scheme.Hom.comp_apply, Cover.ι_glueMorphisms]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.tAux, AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.Scheme.Cover.ι_glueMorphisms, AlgebraicGeometry.Scheme.IsLocallyDirected.V
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
i j : J
l :
  PreZeroHypercover.I₀ (S :=
    (↑(⨆ (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)), Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) :
      Scheme))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦
        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
x :
  ↥(PreZeroHypercover.X
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦
          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
      l)
simp :
  Membership.mem (α := ↥(F.obj j)) (γ := Set ↥(F.obj j))
    (⋃ (i_1 : (k : J) × (k ⟶ j) × (k ⟶ i)),
      Set.range (ι := ↥(F.obj (i_1.fst (β := fun (k : J) ↦ (k ⟶ j) × (k ⟶ i)))))
        ⇑(F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ j) × (k ⟶ i)).1))
    ((TopCat.Hom.hom (F.map l.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2).base : (a : ↥(F.obj l.fst)) → ↥(F.obj j))
        ((TopCat.Hom.hom
                (Hom.base
                  (LocallyRingedSpace.Hom.toHom
                    (Hom.toLRSHom'
                      (Iso.inv (Hom.isoOpensRange (F.map l.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))))) :
              (a :
                  ↥((Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦ Hom.opensRange (F.map i_1.snd.1)).X
                      l)) →
                ↥(F.obj l.fst))
            x :
          ↥(F.obj (l.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      ↥(F.obj j))
⊢ Membership.mem (α := ↥(F.obj j)) (γ := Set ↥(F.obj j))
    (Set.range (ι :=
      ↥(↑(⨆ (k : (k : J) × (k ⟶ j) × (k ⟶ i)), Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ j) × (k ⟶ i)).1)) :
          Scheme))
      ⇑(Opens.ι
          (⨆ (k : (k : J) × (k ⟶ j) × (k ⟶ i)), Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ j) × (k ⟶ i)).1))))
    ((Iso.inv (Hom.isoOpensRange (F.map l.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) ≫
          F.map l.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2)
        x :
      ↥(F.obj j))

Tactic:
simp only [Opens.range_ι, iSup_mk, carrier_eq_coe, Hom.coe_opensRange, coe_mk, Hom.comp_base,
      TopCat.hom_comp, ContinuousMap.comp_apply]

Premises used: TopologicalSpace.Opens.iSup_mk, ContinuousMap.comp_apply, TopologicalSpace.Opens.coe_mk, TopologicalSpace.Opens.carrier_eq_coe, AlgebraicGeometry.Scheme.Opens.range_ι, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.hom_comp, AlgebraicGeometry.Scheme.Hom.coe_opensRange
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
i j : J
l :
  PreZeroHypercover.I₀ (S :=
    (↑(⨆ (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)), Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) :
      Scheme))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦
        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
x :
  ↥(PreZeroHypercover.X
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦
          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
      l)
⊢ Membership.mem (α := ↥(F.obj j)) (γ := Set ↥(F.obj j))
    (⋃ (i_1 : (k : J) × (k ⟶ j) × (k ⟶ i)),
      Set.range (ι := ↥(F.obj (i_1.fst (β := fun (k : J) ↦ (k ⟶ j) × (k ⟶ i)))))
        ⇑(F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ j) × (k ⟶ i)).1))
    ((TopCat.Hom.hom (F.map l.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2).base : (a : ↥(F.obj l.fst)) → ↥(F.obj j))
        ((TopCat.Hom.hom
                (Hom.base
                  (LocallyRingedSpace.Hom.toHom
                    (Hom.toLRSHom'
                      (Iso.inv (Hom.isoOpensRange (F.map l.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))))) :
              (a :
                  ↥((Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦ Hom.opensRange (F.map i_1.snd.1)).X
                      l)) →
                ↥(F.obj l.fst))
            x :
          ↥(F.obj (l.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      ↥(F.obj j))

Tactic:
Set.mem_iUnion.mpr ⟨⟨l.1, l.2.2, l.2.1⟩, ⟨_, rfl⟩⟩

Premises used: Iff.mpr, Set.mem_iUnion, Prod.mk, Sigma.fst, Prod.fst, Exists.intro, Sigma.mk, Sigma.snd, Prod.snd, rfl
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
i j : J
l :
  PreZeroHypercover.I₀ (S :=
    (↑(⨆ (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)), Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)) :
      Scheme))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦
        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
x :
  ↥(PreZeroHypercover.X
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦
          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))
      l)
⊢ Membership.mem (α := ↥(F.obj j)) (γ := Set ↥(F.obj j))
    (⋃ (i_1 : (k : J) × (k ⟶ j) × (k ⟶ i)),
      Set.range (ι := ↥(F.obj (i_1.fst (β := fun (k : J) ↦ (k ⟶ j) × (k ⟶ i)))))
        ⇑(F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ j) × (k ⟶ i)).1))
    ((TopCat.Hom.hom (F.map l.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).2).base : (a : ↥(F.obj l.fst)) → ↥(F.obj j))
        ((TopCat.Hom.hom
                (Hom.base
                  (LocallyRingedSpace.Hom.toHom
                    (Hom.toLRSHom'
                      (Iso.inv (Hom.isoOpensRange (F.map l.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j)).1)))))) :
              (a :
                  ↥((Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ j)) ↦ Hom.opensRange (F.map i_1.snd.1)).X
                      l)) →
                ↥(F.obj l.fst))
            x :
          ↥(F.obj (l.fst (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ j))))) :
      ↥(F.obj j))

Tactic:
exact Set.mem_iUnion.mpr ⟨⟨l.1, l.2.2, l.2.1⟩, ⟨_, rfl⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
i : J
⊢ t F i i = 𝟙 (↑(V F i i) : Scheme)

Tactic:
(Scheme.Opens.iSupOpenCover _).hom_ext _ _ fun k ↦ ?_

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.V, AlgebraicGeometry.Scheme.Cover.hom_ext, AlgebraicGeometry.Scheme.Opens.iSupOpenCover
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
i : J
refine :
  ∀
    (k :
      PreZeroHypercover.I₀ (S :=
        (↑(⨆ (i_1 : (k : J) × (k ⟶ i) × (k ⟶ i)),
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)) :
          Scheme))
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ i)) ↦
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)))),
    PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ i)) ↦
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)))
          k ≫
        t F i i =
      PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ i) × (k ⟶ i)) ↦
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ i) × (k ⟶ i)).1)))
          k ≫
        𝟙 (↑(V F i i) : Scheme)
⊢ t F i i = 𝟙 (↑(V F i i) : Scheme)

Tactic:
refine (Scheme.Opens.iSupOpenCover _).hom_ext _ _ fun k ↦ ?_

Premises used: AlgebraicGeometry.Scheme.Cover.hom_ext, AlgebraicGeometry.Scheme.Opens.iSupOpenCover