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
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 :
  Eq (α := ↥(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))
        ((pullback.lift (d.functor.map fi) (d.functor.map fj) ⋯) xk :
          ↥(pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
              (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))) :
      ↥(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 :
      ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
⊢ (pullback.lift (d.functor.map fi) (d.functor.map fj) ⋯) xk = x

Tactic:
apply (pullback.snd (d.cover.f i) _).injective

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover, CategoryTheory.Limits.pullback.snd, 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_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
⊢ Eq (α := ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
    ((CategoryStruct.comp (Y :=
          pullback (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
            (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))
          (pullback.lift (d.functor.map fi) (d.functor.map fj) ⋯)
          (pullback.snd (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) i)
            (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j)))
        xk :
      ↥(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 :
      ↥(PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover d.cover) j))

Tactic:
simp [h1, xj]
-- 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 : 𝒰.I₀
h :
  ∀ (x : ↥d.glued),
    Membership.mem (γ := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) x ↔
      Membership.mem (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i)) x
⊢ Eq (α := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))

Tactic:
ext x
-- 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 : 𝒰.I₀
x : ↥d.glued
⊢ Membership.mem (γ := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) x ↔
    Membership.mem (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i)) x

Tactic:
⟨fun ⟨ui, h⟩ ↦ ?_, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, Membership.mem, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Iff.intro, _private.0.AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι.match_1, AlgebraicGeometry.PresheafedSpace.Hom.base, Set.range, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor, DFunLike.coe, CategoryTheory.Limits.colimit.ι
-- 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 : 𝒰.I₀
x : ↥d.glued
h :
  Membership.mem (γ := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) x →
    ∀ (ui : ↥(𝒰.X i)) (h : Eq (α := ↥S) ((𝒰.f i) ui : ↥S) (d.toBase x : ↥S)),
      Membership.mem (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i)) x
h₁ :
  Membership.mem (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i)) x →
    Membership.mem (γ := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) x
⊢ Membership.mem (γ := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) x ↔
    Membership.mem (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i)) x

Tactic:
refine ⟨fun ⟨ui, h⟩ ↦ ?_, ?_⟩
-- 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 : 𝒰.I₀
x : ↥d.glued
h_1 : Membership.mem (γ := Set ↥d.glued) (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i))) x
ui : ↥(𝒰.X i)
h : Eq (α := ↥S) ((𝒰.f i) ui : ↥S) (d.toBase x : ↥S)
h₁ :
  ∀ (j : 𝒰.I₀) (xj : ↥(d.functor.obj j)),
    Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
        (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
        ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) →
      ∀ (h : Eq (α := ↥S) ((𝒰.f i) ui : ↥S) (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)),
        Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
          (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
          ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
⊢ Membership.mem (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i)) x

Tactic:
obtain ⟨j, xj, rfl⟩ := IsLocallyDirected.ι_jointly_surjective _ x

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.ι_jointly_surjective, rfl
-- 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 : 𝒰.I₀
ui : ↥(𝒰.X i)
j : 𝒰.I₀
xj : ↥(d.functor.obj j)
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
h : Eq (α := ↥S) ((𝒰.f i) ui : ↥S) (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)
⊢ Eq (α := ↥S) ((𝒰.f i) ui : ↥S)
    ((𝒰.f j)
        ((d.natTrans.app j) xj :
          ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)) :
      ↥S)

Tactic:
simp only [h, functorOfLocallyDirected_obj, ← Scheme.Hom.comp_apply, ι_toBase]

Premises used: AlgebraicGeometry.Scheme.Cover.functorOfLocallyDirected_obj, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase, 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 : 𝒰.I₀
ui : ↥(𝒰.X i)
j : 𝒰.I₀
xj : ↥(d.functor.obj j)
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
h : Eq (α := ↥S) ((𝒰.f i) ui : ↥S) (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)
h₁ :
  ∀ (k : 𝒰.I₀) (fi : k ⟶ i) (fj : k ⟶ j) (uk : ↥(𝒰.X k))
    (h :
      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 :
      Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
        (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)),
    Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
      ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
⊢ Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))

Tactic:
obtain ⟨k, fi, fj, uk, rfl, h⟩ := 𝒰.exists_of_f_eq_f ui (d.natTrans.app j xj) <| by
      simp only [h, functorOfLocallyDirected_obj, ← Scheme.Hom.comp_apply, ι_toBase]

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, rfl, 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 : 𝒰.I₀
xj : ↥(d.functor.obj j)
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h_2 :
  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 :
  Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
    (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)
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 : 𝒰.I₀
xj : ↥(d.functor.obj j)
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h_2 :
  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 :
  Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
    (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)
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:
simp 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 : 𝒰.I₀
xj : ↥(d.functor.obj j)
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h_2 :
  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 :
  Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
    (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)
a :
  Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥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, ← ι_toBase, Scheme.Hom.comp_apply, ← h]

Premises used: AlgebraicGeometry.Scheme.Cover.RelativeGluingData.ι_toBase, 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 : 𝒰.I₀
xj : ↥(d.functor.obj j)
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h_2 :
  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 :
  Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
    (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)
⊢ Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
    ((𝒰.f j) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j)) : ↥S)

Tactic:
simp [← 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 : 𝒰.I₀
xj : ↥(d.functor.obj j)
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))
k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
h_2 :
  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 :
  Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
    (d.toBase ((colimit.ι d.functor j) xj : ↥(colimit d.functor)) : ↥S)
h₁ :
  ∀ (xk : ↥(d.functor.obj k)) (h2 : (d.natTrans.app k) xk = uk),
    Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
        (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
        ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor)) →
      ∀
        (h :
          Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
            ((d.natTrans.app j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) :
              ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j)))
        (h :
          Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
            (d.toBase ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor)) :
              ↥S)),
        Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
          (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
          ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor))
⊢ Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
    ((colimit.ι d.functor j) xj : ↥(colimit d.functor))

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

Premises used: AlgebraicGeometry.Scheme.Cover.RelativeGluingData.equifibered, rfl, 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 k : 𝒰.I₀
fi : k ⟶ i
fj : k ⟶ j
uk : ↥(𝒰.X k)
xk : ↥(d.functor.obj k)
h2 : (d.natTrans.app k) xk = uk
h_1 :
  Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued)
    (Set.preimage (β := ↥S) (⇑d.toBase) (Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)))
    ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor))
h_2 :
  Eq (α := ↥(𝒰.X j)) ((trans (P := IsOpenImmersion) 𝒰 fj) uk : ↥(𝒰.X j))
    ((d.natTrans.app j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) :
      ↥(Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) j))
h :
  Eq (α := ↥S) ((𝒰.f i) ((trans (P := IsOpenImmersion) 𝒰 fi) uk : ↥(𝒰.X i)) : ↥S)
    (d.toBase ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor)) : ↥S)
h₁ :
  Eq (α := ↥(colimit d.functor))
    ((colimit.ι d.functor i) ((d.functor.map fi) xk : ↥(d.functor.obj i)) : ↥(colimit d.functor))
    ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor))
⊢ Membership.mem (α := ↥d.glued) (γ := Set ↥d.glued) (Set.range (ι := ↥(d.functor.obj i)) ⇑(colimit.ι d.functor i))
    ((colimit.ι d.functor j) ((d.functor.map fj) xk : ↥(d.functor.obj j)) : ↥(colimit d.functor))

Tactic:
use d.functor.map fi xk

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', CategoryTheory.Functor.map, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor, DFunLike.coe