awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
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)) ((F.map fi) xi : ↥(F.obj k)) ((F.map fj) xj : ↥(F.obj k))
⊢ Eq (α := ↥(G.obj k)) ((s.app j ≫ G.map fj) xj : ↥(G.obj k)) ((G.map fj) ((s.app j) xj : ↥(G.obj j)) : ↥(G.obj k))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
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))
h :
  ∃ (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
⊢ ∃ (l : J) (fli : l ⟶ i) (flj : l ⟶ j) (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:
use l, fli, flj
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
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
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
⊢ ∃ (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

Premises used: Eq.symm, AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
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

Tactic:
⟨e.inv z, ?_, ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', And.intro, Exists.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
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
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
⊢ ∃ (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:
refine ⟨e.inv z, ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
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 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:
simp [← h1, ← Scheme.Hom.comp_apply, e]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
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 :
  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))
⊢ (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:
apply H fj
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
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
⊢ flj ≫ fj = fli ≫ fi

Tactic:
subsingleton
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
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 : Eq (α := ↥(F.obj k)) ((e.inv ≫ F.map (fli ≫ fi)) z : ↥(F.obj k)) ((F.map fj) xj : ↥(F.obj k))
⊢ 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:
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]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, AlgebraicGeometry.Scheme.forget_map, AlgebraicGeometry.Scheme.forget_obj, TypeCat.Fun.coe_mk, AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Functor.map_comp, CategoryTheory.ConcreteCategory.hom_ofHom, CategoryTheory.Functor.comp_map
-- Module: Mathlib.AlgebraicGeometry.RelativeGluing
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)) ((F.map fi) xi : ↥(F.obj k)) ((F.map fj) 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)) ((e.inv ≫ F.map (fli ≫ fi)) z : ↥(F.obj k)) ((F.map fj) xj : ↥(F.obj k))

Tactic:
simp [e, Functor.map_comp, ← heq, h1]

Premises used: CategoryTheory.Functor.map_comp
-- 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} 𝒰
i j : 𝒰.I₀
hij : i ⟶ j
apply :
  IsOpenImmersion (X := Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)
    (CategoryTheory.Functor.map (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) hij)
⊢ IsOpenImmersion (d.functor.map hij)

Tactic:
apply MorphismProperty.of_isPullback (d.equifibered hij).flip

Premises used: CategoryTheory.MorphismProperty.of_isPullback, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.equifibered, CategoryTheory.IsPullback.flip
-- 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} 𝒰
i j : 𝒰.I₀
hij : i ⟶ j
⊢ IsOpenImmersion (X := Functor.obj.{u_2, u, u_1, u + 1} (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) i)
    (CategoryTheory.Functor.map (functorOfLocallyDirected (P := IsOpenImmersion) 𝒰) hij)

Tactic:
infer_instance
-- 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 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
H :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
    Function.Injective (α := ↥(d.functor.obj i)) (β := ↥(d.functor.obj j)) ⇑(d.functor.map hij)
⊢ (d.functor ⋙ forget).IsLocallyDirected

Tactic:
apply isLocallyDirected_of_equifibered_of_injective d.natTrans d.equifibered

Premises used: AlgebraicGeometry.Scheme.Cover.RelativeGluingData.equifibered, AlgebraicGeometry.Scheme.isLocallyDirected_of_equifibered_of_injective, 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 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : 𝒰.I₀
hij : i ⟶ j
⊢ Function.Injective (α := ↥(d.functor.obj i)) (β := ↥(d.functor.obj j)) ⇑(d.functor.map hij)

Tactic:
(d.functor.map hij).injective

Premises used: CategoryTheory.Functor.map, AlgebraicGeometry.Scheme.Hom.injective, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor
-- 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 : Quiver.IsThin.{u_1, u_2} 𝒰.I₀
i j : 𝒰.I₀
hij : i ⟶ j
⊢ Function.Injective (α := ↥(d.functor.obj i)) (β := ↥(d.functor.obj j)) ⇑(d.functor.map hij)

Tactic:
exact (d.functor.map hij).injective

Premises used: CategoryTheory.Functor.map, AlgebraicGeometry.Scheme.Hom.injective, AlgebraicGeometry.Scheme.Cover.RelativeGluingData.functor
-- 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₀
⊢ CategoryStruct.comp (Y := colimit d.functor) (colimit.ι d.functor i : d.functor.obj i ⟶ colimit d.functor)
      (d.toBase : d.glued ⟶ S) =
    d.natTrans.app i ≫ 𝒰.f i

Tactic:
simp [toBase]

Premises used: AlgebraicGeometry.Scheme.Cover.RelativeGluingData.toBase