awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F G : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
s : F ⟶ G
inst_1 : Quiver.IsThin.{u_1, u_2} J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective (α := ↥(F.obj i)) (β := ↥(F.obj j)) ⇑(F.map hij)
inst_2 : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq :
  Eq (α := ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fi)) : (a : ↥(F.obj i)) → ↥(F.obj k)) xi : ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fj)) : (a : ↥(F.obj j)) → ↥(F.obj k)) xj : ↥(F.obj k))
l : J
fli : l ⟶ i
flj : l ⟶ j
x : (G ⋙ forget).obj l
hi :
  Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map fli) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
        x :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
    ((s.app i) xi : ↥(G.obj i))
hj :
  Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map flj) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
        x :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
    ((s.app j) xj : ↥(G.obj j))
e : F.obj l ≅ pullback (s.app i) (G.map fli) := ⋯.isoPullback
⊢ ∃ (x : (F ⋙ forget).obj l),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map fli) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
          x =
        xi ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
          x =
        xj
have h : ∀ (z : ↥(pullback (s.app i) (G.map fli))) (h1 : (pullback.fst (s.app i) (G.map fli)) z = xi)
  (h2 : (pullback.snd (s.app i) (G.map fli)) z = x),
  ∃ (x : (F ⋙ forget).obj l),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map fli) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
          x =
        xi ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
          x =
        xj
Tactic: obtain ⟨z, h1, h2⟩ := Scheme.Pullback.exists_preimage_pullback xi x hi.symm
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F G : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
s : F ⟶ G
inst_1 : Quiver.IsThin.{u_1, u_2} J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective (α := ↥(F.obj i)) (β := ↥(F.obj j)) ⇑(F.map hij)
inst_2 : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq :
  Eq (α := ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fi)) : (a : ↥(F.obj i)) → ↥(F.obj k)) xi : ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fj)) : (a : ↥(F.obj j)) → ↥(F.obj k)) xj : ↥(F.obj k))
l : J
fli : l ⟶ i
flj : l ⟶ j
x : (G ⋙ forget).obj l
hi :
  Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map fli) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
        x :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
    ((s.app i) xi : ↥(G.obj i))
hj :
  Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map flj) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
        x :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
    ((s.app j) xj : ↥(G.obj j))
e : F.obj l ≅ pullback (s.app i) (G.map fli) := ⋯.isoPullback
z : ↥(pullback (s.app i) (G.map fli))
h1 : (pullback.fst (s.app i) (G.map fli)) z = xi
h2 : (pullback.snd (s.app i) (G.map fli)) z = x
⊢ ∃ (x : (F ⋙ forget).obj l),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map fli) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
          x =
        xi ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
          x =
        xj
have h : (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map fli) :
      (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
    (e.inv z : ↥(F.obj l)) =
  xi
Tactic: refine ⟨e.inv z, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F G : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
s : F ⟶ G
inst_1 : Quiver.IsThin.{u_1, u_2} J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective (α := ↥(F.obj i)) (β := ↥(F.obj j)) ⇑(F.map hij)
inst_2 : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq :
  Eq (α := ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fi)) : (a : ↥(F.obj i)) → ↥(F.obj k)) xi : ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fj)) : (a : ↥(F.obj j)) → ↥(F.obj k)) xj : ↥(F.obj k))
l : J
fli : l ⟶ i
flj : l ⟶ j
x : (G ⋙ forget).obj l
hi :
  Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map fli) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
        x :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
    ((s.app i) xi : ↥(G.obj i))
hj :
  Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map flj) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
        x :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
    ((s.app j) xj : ↥(G.obj j))
e : F.obj l ≅ pullback (s.app i) (G.map fli) := ⋯.isoPullback
z : ↥(pullback (s.app i) (G.map fli))
h1 : (pullback.fst (s.app i) (G.map fli)) z = xi
h2 : (pullback.snd (s.app i) (G.map fli)) z = x
h :
  (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map fli) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
      (e.inv z : ↥(F.obj l)) =
    xi
⊢ ∃ (x : (F ⋙ forget).obj l),
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map fli) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj i))
          x =
        xi ∧
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
          x =
        xj
have h₁ : (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
      (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
    (e.inv z : ↥(F.obj l)) =
  xj
Tactic: refine ⟨e.inv z, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F G : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
s : F ⟶ G
inst_1 : Quiver.IsThin.{u_1, u_2} J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective (α := ↥(F.obj i)) (β := ↥(F.obj j)) ⇑(F.map hij)
inst_2 : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq :
  Eq (α := ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fi)) : (a : ↥(F.obj i)) → ↥(F.obj k)) xi : ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fj)) : (a : ↥(F.obj j)) → ↥(F.obj k)) xj : ↥(F.obj k))
l : J
fli : l ⟶ i
flj : l ⟶ j
x : (G ⋙ forget).obj l
hi :
  Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map fli) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
        x :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
    ((s.app i) xi : ↥(G.obj i))
hj :
  Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map flj) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
        x :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
    ((s.app j) xj : ↥(G.obj j))
e : F.obj l ≅ pullback (s.app i) (G.map fli) := ⋯.isoPullback
z : ↥(pullback (s.app i) (G.map fli))
h1 : (pullback.fst (s.app i) (G.map fli)) z = xi
h2 : (pullback.snd (s.app i) (G.map fli)) z = x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
        (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
      (e.inv z : ↥(F.obj l)) =
    xj
have h : Eq (α := ↥(F.obj k))
  ((F.map fj)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
          (e.inv z : ↥(F.obj l)) :
        (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j)) :
    ↥(F.obj k))
  ((F.map fj) xj : ↥(F.obj k))
Tactic: apply H fj
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
Goal:
J : Type u_1
inst : Category.{u_2, u_1} J
F G : CategoryTheory.Functor.{u_2, u, u_1, u + 1} J Scheme
s : F ⟶ G
inst_1 : Quiver.IsThin.{u_1, u_2} J
hs : NatTrans.Equifibered s
H : ∀ {i j : J} (hij : i ⟶ j), Function.Injective (α := ↥(F.obj i)) (β := ↥(F.obj j)) ⇑(F.map hij)
inst_2 : (G ⋙ forget).IsLocallyDirected
i j k : J
fi : i ⟶ k
fj : j ⟶ k
xi : (F ⋙ forget).obj i
xj : (F ⋙ forget).obj j
heq :
  Eq (α := ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fi)) : (a : ↥(F.obj i)) → ↥(F.obj k)) xi : ↥(F.obj k))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (↾⇑(F.map fj)) : (a : ↥(F.obj j)) → ↥(F.obj k)) xj : ↥(F.obj k))
l : J
fli : l ⟶ i
flj : l ⟶ j
x : (G ⋙ forget).obj l
hi :
  Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map fli) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
        x :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj i))
    ((s.app i) xi : ↥(G.obj i))
hj :
  Eq (α := (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((G ⋙ forget).map flj) :
          (a : (fun (X : Type u) ↦ X) ((G ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
        x :
      (fun (X : Type u) ↦ X) ((G ⋙ forget).obj j))
    ((s.app j) xj : ↥(G.obj j))
e : F.obj l ≅ pullback (s.app i) (G.map fli) := ⋯.isoPullback
z : ↥(pullback (s.app i) (G.map fli))
h1 : (pullback.fst (s.app i) (G.map fli)) z = xi
h2 : (pullback.snd (s.app i) (G.map fli)) z = x
⊢ Eq (α := ↥(F.obj k))
    ((F.map fj)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((F ⋙ forget).map flj) :
              (a : (fun (X : Type u) ↦ X) ((F ⋙ forget).obj l)) → (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j))
            (e.inv z : ↥(F.obj l)) :
          (fun (X : Type u) ↦ X) ((F ⋙ forget).obj j)) :
      ↥(F.obj k))
    ((F.map fj) xj : ↥(F.obj k))
have h : Eq (α := ↥(F.obj k)) ((e.inv ≫ F.map (fli ≫ fi)) z : ↥(F.obj k)) ((F.map fj) xj : ↥(F.obj k))
Tactic: simp only [Functor.comp_obj, forget_obj, Functor.comp_map, forget_map,
        ConcreteCategory.hom_ofHom, TypeCat.Fun.coe_mk, ← Scheme.Hom.comp_apply,
        Category.assoc, ← Functor.map_comp, show flj ≫ fj = fli ≫ fi by subsingleton]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
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} 𝒰
i j : 𝒰.I₀
hij : i ⟶ j
⊢ IsOpenImmersion (d.functor.map hij)
have apply : IsOpenImmersion (X := Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)
  (CategoryTheory.Functor.map (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) hij)
Tactic: apply MorphismProperty.of_isPullback (d.equifibered hij).flip
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
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 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
⊢ (d.functor ⋙ forget).IsLocallyDirected
have H : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
  Function.Injective (α := ↥(d.functor.obj i)) (β := ↥(d.functor.obj j)) ⇑(d.functor.map hij)
Tactic: apply isLocallyDirected_of_equifibered_of_injective d.natTrans d.equifibered
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
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)
    ((𝒰.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)
have 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)
Tactic: dsimp [functorOfLocallyDirected_obj, xi, xj]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
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)
    ((𝒰.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)
have 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)
Tactic: rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply, ← ι_toBase, pullback.condition_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
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 : 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
have 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) sorry) 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
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))
⊢ ∃ (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
have h : ∃ (y : ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) k)),
  (pullback.lift (d.functor.map fi) (d.functor.map fj) sorry) y = x
Tactic: use k, fi, fj
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.RelativeGluing (goal)
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 (α := ↥(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))
have 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)
Tactic: apply (𝒰.f j).injective