awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
dsimp :
  Eq (α := ↥S)
    ((𝒰.f i)
        ((d.natTrans.app i) ((pullback.fst (colimit.ι d.functor i) (colimit.ι d.functor j)) x : ↥(d.functor.obj i)) :
          ↥(𝒰.X i)) :
      ↥S)
    ((𝒰.f j)
        ((d.natTrans.app j) ((pullback.snd (colimit.ι d.functor i) (colimit.ι d.functor j)) x : ↥(d.functor.obj j)) :
          ↥(𝒰.X j)) :
      ↥S)
⊢ Eq (α := ↥S)
    ((𝒰.f i)
        ((d.natTrans.app i) xi :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)) :
      ↥S)
    ((𝒰.f j)
        ((d.natTrans.app j) xj :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)) :
      ↥S)

Tactic:
dsimp [functorOfLocallyDirected_obj, xi, xj]

Premises used: AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_obj
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
rw :
  Eq (α := ↥S)
    ((pullback.snd (colimit.ι d.functor i) (colimit.ι d.functor j) ≫
          CategoryStruct.comp (Y := d.glued) (colimit.ι d.functor j : d.functor.obj j ⟶ colimit d.functor)
            (d.toBase : d.glued ⟶ S))
        x :
      ↥S)
    ((𝒰.f j)
        ((d.natTrans.app j) ((pullback.snd (colimit.ι d.functor i) (colimit.ι d.functor j)) x : ↥(d.functor.obj j)) :
          ↥(𝒰.X j)) :
      ↥S)
⊢ Eq (α := ↥S)
    ((𝒰.f i)
        ((d.natTrans.app i) ((pullback.fst (colimit.ι d.functor i) (colimit.ι d.functor j)) x : ↥(d.functor.obj i)) :
          ↥(𝒰.X i)) :
      ↥S)
    ((𝒰.f j)
        ((d.natTrans.app j) ((pullback.snd (colimit.ι d.functor i) (colimit.ι d.functor j)) x : ↥(d.functor.obj j)) :
          ↥(𝒰.X j)) :
      ↥S)

Tactic:
rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, ← ι_toBase, pullback.condition_assoc]

Premises used: AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase, CategoryTheory.Limits.pullback.condition_assoc, AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
⊢ Eq (α := ↥S)
    ((pullback.snd (colimit.ι d.functor i) (colimit.ι d.functor j) ≫
          CategoryStruct.comp (Y := d.glued) (colimit.ι d.functor j : d.functor.obj j ⟶ colimit d.functor)
            (d.toBase : d.glued ⟶ S))
        x :
      ↥S)
    ((𝒰.f j)
        ((d.natTrans.app j) ((pullback.snd (colimit.ι d.functor i) (colimit.ι d.functor j)) x : ↥(d.functor.obj j)) :
          ↥(𝒰.X j)) :
      ↥S)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
obtain :
  ∀ (k : 𝒰.I₀) (fi : k ⟶ i) (fj : k ⟶ j) (uk : ↥(𝒰.X k))
    (h1 :
      Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
        ((d.natTrans.app i) xi :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)))
    (h2 :
      Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
        ((d.natTrans.app j) xj :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))),
    ∃ (k : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)) (hki : k ⟶ i)
      (hkj : k ⟶ j) (y : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) k)),
      (pullback.lift (d.functor.map hki) (d.functor.map hkj) ⋯) y = x
⊢ ∃ (k : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)) (hki : k ⟶ i)
    (hkj : k ⟶ j) (y : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) k)),
    (pullback.lift (d.functor.map hki) (d.functor.map hkj) ⋯) y = x

Tactic:
obtain ⟨k, fi, fj, uk, h1, h2⟩ :=
        𝒰.exists_of_f_eq_f (d.natTrans.app i xi) (d.natTrans.app j xj) <| by
      dsimp [functorOfLocallyDirected_obj, xi, xj]
      rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, ← ι_toBase, pullback.condition_assoc]
      simp

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.Cover.exists_of_f_eq_f, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, CategoryTheory.NatTrans.app, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.natTrans
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 :
  Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
    ((d.natTrans.app i) xi : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i))
h2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
h :
  ∃ (y : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) k)),
    (pullback.lift (d.functor.map fi) (d.functor.map fj) ⋯) y = x
⊢ ∃ (k : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)) (hki : k ⟶ i)
    (hkj : k ⟶ j) (y : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) k)),
    (pullback.lift (d.functor.map hki) (d.functor.map hkj) ⋯) y = x

Tactic:
use k, fi, fj
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 :
  Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
    ((d.natTrans.app i) xi : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i))
h2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
a :
  Eq (α := ↥S)
    ((𝒰.f j)
        ((d.natTrans.app j) xj :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)) :
      ↥S)
    ((𝒰.f j)
        ((CategoryTheory.Functor.map (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) fj) uk :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)) :
      ↥S)
⊢ Eq (α := ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
    ((CategoryTheory.Functor.map (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) fj) uk :
      ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))

Tactic:
apply (𝒰.f j).injective

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.injective, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 :
  Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
    ((d.natTrans.app i) xi : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i))
h2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
a :
  Eq (α := ↥S) ((𝒰.f j) ((d.natTrans.app j) xj : ↥(𝒰.X j)) : ↥S)
    ((𝒰.f j) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j)) : ↥S)
⊢ Eq (α := ↥S)
    ((𝒰.f j)
        ((d.natTrans.app j) xj :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)) :
      ↥S)
    ((𝒰.f j)
        ((CategoryTheory.Functor.map (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) fj) uk :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)) :
      ↥S)

Tactic:
dsimp only [functorOfLocallyDirected_obj, functorOfLocallyDirected_map]

Premises used: AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_obj, AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_map
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 :
  Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
    ((d.natTrans.app i) xi : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i))
h2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
a : Eq (α := ↥S) ((d.natTrans.app j ≫ 𝒰.f j) xj : ↥S) ((𝒰.f j) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j)) : ↥S)
⊢ Eq (α := ↥S) ((𝒰.f j) ((d.natTrans.app j) xj : ↥(𝒰.X j)) : ↥S)
    ((𝒰.f j) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j)) : ↥S)

Tactic:
rw [← Scheme.Hom.comp_apply]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 :
  Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
    ((d.natTrans.app i) xi : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i))
h2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
⊢ Eq (α := ↥S) ((d.natTrans.app j ≫ 𝒰.f j) xj : ↥S) ((𝒰.f j) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j)) : ↥S)

Tactic:
simp [xj, h2]
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1 :
  Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
    ((d.natTrans.app i) xi : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i))
h2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
h :
  ∀ (xk : ↥(d.functor.obj k)) (h1 : (d.functor.map fj) xk = xj) (h2 : (d.natTrans.app k) xk = uk),
    ∃ (y : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) k)),
      (pullback.lift (d.functor.map fi) (d.functor.map fj) ⋯) y = x
⊢ ∃ (y : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) k)),
    (pullback.lift (d.functor.map fi) (d.functor.map fj) ⋯) y = x

Tactic:
obtain ⟨xk, h1, h2⟩ := exists_preimage_of_isPullback (d.equifibered fj) xj uk <| by
      apply (𝒰.f j).injective
      dsimp only [functorOfLocallyDirected_obj, functorOfLocallyDirected_map]
      rw [← Scheme.Hom.comp_apply]
      simp [xj, h2]

Premises used: AlgebraicGeometry.Scheme.Cover.RelativeGluingData.equifibered, AlgebraicGeometry.Scheme.exists_preimage_of_isPullback
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
Goal:
S : Scheme
𝒰 : OpenCover.{u_1, u} S
inst : Category.{u_2, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{u_2, u, u_1} (P := IsOpenImmersion) 𝒰
d : RelativeGluingData.{u, u_1, u_2} 𝒰
inst_2 : Small.{u, u_1} 𝒰.I₀
inst_3 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : PreZeroHypercover.I₀ (S := d.glued) (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover)
x :
  ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
xi : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i) :=
  (pullback.fst (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
xj : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j) :=
  (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    x
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h1_1 :
  Eq (α := ↥(𝒰.X i)) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i))
    ((d.natTrans.app i) xi : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i))
h2_1 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) xj : ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
xk : ↥(d.functor.obj k)
h1 : (d.functor.map fj) xk = xj
h2 : (d.natTrans.app k) xk = uk
h : (pullback.lift (d.functor.map fi) (d.functor.map fj) ⋯) xk = x
⊢ ∃ (y : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) k)),
    (pullback.lift (d.functor.map fi) (d.functor.map fj) ⋯) y = x

Tactic:
use xk