awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k_1 i j k : ι
⊢ CategoryStruct.comp (Y := Limits.pullback (⋯.fst' (f k)) (⋯.fst' (f i)))
        (⋯.lift₃ (f k) (f i) (pullback₃.p₂ ⋯ (f j) (f k)) (pullback₃.p₃ ⋯ (f j) (f k)) (pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯)
        (pullback.snd (⋯.fst' (f k)) (⋯.fst' (f i))) ≫
      ⋯.snd (f i) =
    (pullback.fst (⋯.fst' (f j)) (⋯.fst' (f k)) ≫ ⋯.symmetry ⋯) ≫ ⋯.snd (f i)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k_1 i j k : ι
⊢ CategoryStruct.comp (Y := ⋯.pullback₃ (f j) (f k))
      (⋯.lift₃ (f k) (f i) (pullback₃.p₂ ⋯ (f j) (f k)) (pullback₃.p₃ ⋯ (f j) (f k)) (pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯ ≫
        ⋯.lift₃ (f i) (f j) (pullback₃.p₂ ⋯ (f k) (f i)) (pullback₃.p₃ ⋯ (f k) (f i)) (pullback₃.p₁ ⋯ (f k) (f i)) ⋯ ⋯ ≫
          ⋯.lift₃ (f j) (f k) (pullback₃.p₂ ⋯ (f i) (f j)) (pullback₃.p₃ ⋯ (f i) (f j)) (pullback₃.p₁ ⋯ (f i) (f j)) ⋯
            ⋯)
      (pullback₃.p₁ ⋯ (f j) (f k)) =
    𝟙 (Limits.pullback (⋯.fst' (f j)) (⋯.fst' (f k))) ≫ pullback₃.p₁ ⋯ (f j) (f k)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k_1 i j k : ι
⊢ CategoryStruct.comp (Y := ⋯.pullback₃ (f j) (f k))
      (⋯.lift₃ (f k) (f i) (pullback₃.p₂ ⋯ (f j) (f k)) (pullback₃.p₃ ⋯ (f j) (f k)) (pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯ ≫
        ⋯.lift₃ (f i) (f j) (pullback₃.p₂ ⋯ (f k) (f i)) (pullback₃.p₃ ⋯ (f k) (f i)) (pullback₃.p₁ ⋯ (f k) (f i)) ⋯ ⋯ ≫
          ⋯.lift₃ (f j) (f k) (pullback₃.p₂ ⋯ (f i) (f j)) (pullback₃.p₃ ⋯ (f i) (f j)) (pullback₃.p₁ ⋯ (f i) (f j)) ⋯
            ⋯)
      (pullback₃.p₂ ⋯ (f j) (f k)) =
    𝟙 (Limits.pullback (⋯.fst' (f j)) (⋯.fst' (f k))) ≫ pullback₃.p₂ ⋯ (f j) (f k)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i_1 j_1 k_1 i j k : ι
⊢ CategoryStruct.comp (Y := ⋯.pullback₃ (f j) (f k))
      (⋯.lift₃ (f k) (f i) (pullback₃.p₂ ⋯ (f j) (f k)) (pullback₃.p₃ ⋯ (f j) (f k)) (pullback₃.p₁ ⋯ (f j) (f k)) ⋯ ⋯ ≫
        ⋯.lift₃ (f i) (f j) (pullback₃.p₂ ⋯ (f k) (f i)) (pullback₃.p₃ ⋯ (f k) (f i)) (pullback₃.p₁ ⋯ (f k) (f i)) ⋯ ⋯ ≫
          ⋯.lift₃ (f j) (f k) (pullback₃.p₂ ⋯ (f i) (f j)) (pullback₃.p₃ ⋯ (f i) (f j)) (pullback₃.p₁ ⋯ (f i) (f j)) ⋯
            ⋯)
      (pullback₃.p₃ ⋯ (f j) (f k)) =
    𝟙 (Limits.pullback (⋯.fst' (f j)) (⋯.fst' (f k))) ≫ pullback₃.p₃ ⋯ (f j) (f k)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
⊢ IsOpenImmersion (toGlued hf i)

Tactic:
inferInstanceAs (IsOpenImmersion ((glueData hf).ι i))

Premises used: _private.0.AlgebraicGeometry.Scheme.LocalRepresentability.instIsOpenImmersionToGlued._proof_1
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
a :
  Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((yonedaEquiv : (a : yoneda.obj (X i) ⟶ F.obj) → F.obj.obj (op (X i)))
        (CategoryTheory.Functor.map yoneda (toGlued hf i) ≫ (yonedaGluedToSheaf hf).hom) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((yonedaEquiv : (a : yoneda.obj (X i) ⟶ F.obj) → F.obj.obj (op (X i))) (f i) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
⊢ CategoryTheory.Functor.map yoneda (toGlued hf i) ≫ (yonedaGluedToSheaf hf).hom = f i

Tactic:
apply yonedaEquiv.injective

Premises used: Equiv.injective, CategoryTheory.yonedaEquiv
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
a :
  Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (InducedCategory.Hom.hom
                {
                  hom :=
                    (Equiv.symm yonedaEquiv :
                        (a : F.obj.obj (op (glueData hf).glued)) → yoneda.obj (glueData hf).glued ⟶ F.obj)
                      ((glueData hf).sheafValGluedMk
                        (fun (i : (glueData hf).J) ↦
                          (yonedaEquiv :
                              (a : yoneda.obj ((glueData hf).U i) ⟶ F.obj) → F.obj.obj (op ((glueData hf).U i)))
                            (f i))
                        ⋯) :
                  InducedCategory.Hom (D := Schemeᵒᵖ ⥤ Type u) (F :=
                    ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf zariskiTopology))
                    (zariskiTopology.yoneda.obj (glueData hf).glued) F })
              (op (X i))) :
          (a : (yoneda.obj (glueData hf).glued).obj (op (X i))) → F.obj.obj (op (X i)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾fun
                    (g :
                      Functor.obj
                        { obj := fun (Y : Schemeᵒᵖ) ↦ unop Y ⟶ X i,
                          map := fun {X_1 Y : Schemeᵒᵖ} (f : X_1 ⟶ Y) ↦ ↾fun (g : unop X_1 ⟶ X i) ↦ f.unop ≫ g,
                          map_id := ⋯, map_comp := ⋯ : Schemeᵒᵖ ⥤ Type u }
                        (op (X i))) ↦
                  g ≫ toGlued hf i) :
              (a : (yoneda.obj (X i)).obj (op (X i))) → (yoneda.obj (glueData hf).glued).obj (op (X i)))
            (𝟙 (X i)) :
          Functor.obj (Functor.obj yoneda (glueData hf).glued) (op (X i))) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((f i).app (op (X i))) :
          (a : (fun (X : Type u) ↦ X) ((yoneda.obj (X i)).obj (op (X i)))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op (X i))))
        (𝟙 (X i)) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i))))
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((yonedaEquiv : (a : yoneda.obj (X i) ⟶ F.obj) → F.obj.obj (op (X i)))
        (CategoryTheory.Functor.map yoneda (toGlued hf i) ≫ (yonedaGluedToSheaf hf).hom) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((yonedaEquiv : (a : yoneda.obj (X i) ⟶ F.obj) → F.obj.obj (op (X i))) (f i) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))

Tactic:
rw [yonedaGluedToSheaf, yonedaEquiv_apply, yonedaEquiv_apply,
    NatTrans.comp_app_apply, yoneda_map_app]

Premises used: CategoryTheory.yoneda_map_app, CategoryTheory.yonedaEquiv_apply, CategoryTheory.NatTrans.comp_app_apply, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (NatTrans.app
              (InducedCategory.Hom.hom
                {
                  hom :=
                    (Equiv.symm yonedaEquiv :
                        (a : F.obj.obj (op (glueData hf).glued)) → yoneda.obj (glueData hf).glued ⟶ F.obj)
                      ((glueData hf).sheafValGluedMk
                        (fun (i : (glueData hf).J) ↦
                          (yonedaEquiv :
                              (a : yoneda.obj ((glueData hf).U i) ⟶ F.obj) → F.obj.obj (op ((glueData hf).U i)))
                            (f i))
                        ⋯) :
                  InducedCategory.Hom (D := Schemeᵒᵖ ⥤ Type u) (F :=
                    ObjectProperty.FullSubcategory.obj (P := Presheaf.IsSheaf zariskiTopology))
                    (zariskiTopology.yoneda.obj (glueData hf).glued) F })
              (op (X i))) :
          (a : (yoneda.obj (glueData hf).glued).obj (op (X i))) → F.obj.obj (op (X i)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (↾fun
                    (g :
                      Functor.obj
                        { obj := fun (Y : Schemeᵒᵖ) ↦ unop Y ⟶ X i,
                          map := fun {X_1 Y : Schemeᵒᵖ} (f : X_1 ⟶ Y) ↦ ↾fun (g : unop X_1 ⟶ X i) ↦ f.unop ≫ g,
                          map_id := ⋯, map_comp := ⋯ : Schemeᵒᵖ ⥤ Type u }
                        (op (X i))) ↦
                  g ≫ toGlued hf i) :
              (a : (yoneda.obj (X i)).obj (op (X i))) → (yoneda.obj (glueData hf).glued).obj (op (X i)))
            (𝟙 (X i)) :
          Functor.obj (Functor.obj yoneda (glueData hf).glued) (op (X i))) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((f i).app (op (X i))) :
          (a : (fun (X : Type u) ↦ X) ((yoneda.obj (X i)).obj (op (X i)))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op (X i))))
        (𝟙 (X i)) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i))))

Tactic:
simpa using GlueData.sheafValGluedMk_val _ _ _ _

Premises used: AlgebraicGeometry.Scheme.GlueData.sheafValGluedMk_val
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
rw :
  Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op (X i))) :
          (a : X i ⟶ (glueData hf).glued) → F.obj.obj (op (X i)))
        (toGlued hf i) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op (X i))) :
          (a : (fun (X : Type u) ↦ X) ((yoneda.obj (glueData hf).glued).obj (op (X i)))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op (X i))))
        (toGlued hf i) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i))))
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op (X i))) :
          (a : X i ⟶ (glueData hf).glued) → F.obj.obj (op (X i)))
        (toGlued hf i) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((yonedaEquiv : (a : yoneda.obj (X i) ⟶ F.obj) → F.obj.obj (op (X i))) (f i) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))

Tactic:
rw [← yoneda_toGlued_yonedaGluedToSheaf hf i, yonedaEquiv_comp,
    yonedaEquiv_yoneda_map]

Premises used: CategoryTheory.yonedaEquiv_yoneda_map, AlgebraicGeometry.Scheme.LocalRepresentability.yoneda_toGlued_yonedaGluedToSheaf, CategoryTheory.yonedaEquiv_comp
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i : ι
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op (X i))) :
          (a : X i ⟶ (glueData hf).glued) → F.obj.obj (op (X i)))
        (toGlued hf i) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op (X i))) :
          (a : (fun (X : Type u) ↦ X) ((yoneda.obj (glueData hf).glued).obj (op (X i)))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op (X i))))
        (toGlued hf i) :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op (X i))))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
V U : Scheme
γ : V ⟶ U
α : U ⟶ (glueData hf).glued
⊢ Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op V)) :
          (a : V ⟶ (glueData hf).glued) → F.obj.obj (op V))
        (γ ≫ α) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.obj (P := Presheaf.IsSheaf zariskiTopology).map γ.op) :
          (a : F.obj.obj (op U)) → F.obj.obj (op V))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
              (a : U ⟶ (glueData hf).glued) → F.obj.obj (op U))
            α :
          F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)) :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op V))

Tactic:
ConcreteCategory.congr_hom ((yonedaGluedToSheaf hf).hom.naturality γ.op) α

Premises used: Quiver.Hom.op, CategoryTheory.NatTrans.naturality, AlgebraicGeometry.Scheme.LocalRepresentability.yonedaGluedToSheaf, CategoryTheory.ConcreteCategory.congr_hom, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : CategoryTheory.Functor.map yoneda a ≫ f i = CategoryTheory.Functor.map yoneda b ≫ f j
rw : ⋯.lift' a b h ≫ ⋯.fst' (f j) ≫ toGlued hf i = b ≫ toGlued hf j
⊢ a ≫ toGlued hf i = b ≫ toGlued hf j

Tactic:
rw [← (hf i).rep.lift'_fst a b h, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.relativelyRepresentable.lift'_fst, CategoryTheory.MorphismProperty.relative.rep
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : CategoryTheory.Functor.map yoneda a ≫ f i = CategoryTheory.Functor.map yoneda b ≫ f j
rw : ⋯.lift' a b h ≫ ⋯.snd (f j) ≫ toGlued hf j
| b ≫ toGlued hf j

Tactic:
rw [← (hf i).rep.lift'_snd a b h, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MorphismProperty.relative.rep, CategoryTheory.Functor.relativelyRepresentable.lift'_snd
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : CategoryTheory.Functor.map yoneda a ≫ f i = CategoryTheory.Functor.map yoneda b ≫ f j
conv_rhs : ⋯.lift' a b h ≫ ⋯.fst' (f j) ≫ toGlued hf i = ⋯.lift' a b h ≫ ⋯.snd (f j) ≫ toGlued hf j
⊢ ⋯.lift' a b h ≫ ⋯.fst' (f j) ≫ toGlued hf i = b ≫ toGlued hf j

Tactic:
conv_rhs => rw [← (hf i).rep.lift'_snd a b h, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MorphismProperty.relative.rep, CategoryTheory.Functor.relativelyRepresentable.lift'_snd
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : CategoryTheory.Functor.map yoneda a ≫ f i = CategoryTheory.Functor.map yoneda b ≫ f j
e_a : ⋯.fst' (f j) ≫ toGlued hf i = ⋯.snd (f j) ≫ toGlued hf j
⊢ ⋯.lift' a b h ≫ ⋯.fst' (f j) ≫ toGlued hf i = ⋯.lift' a b h ≫ ⋯.snd (f j) ≫ toGlued hf j

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : CategoryTheory.Functor.map yoneda a ≫ f i = CategoryTheory.Functor.map yoneda b ≫ f j
⊢ (glueData hf).t i j ≫ (glueData hf).f j i ≫ (glueData hf).ι j = ⋯.snd (f j) ≫ toGlued hf j

Tactic:
simp [toGlued]

Premises used: AlgebraicGeometry.Scheme.LocalRepresentability.toGlued
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
U : Scheme
i j : ι
a : U ⟶ X i
b : U ⟶ X j
h : CategoryTheory.Functor.map yoneda a ≫ f i = CategoryTheory.Functor.map yoneda b ≫ f j
⊢ ⋯.fst' (f j) ≫ toGlued hf i = ⋯.snd (f j) ≫ toGlued hf j

Tactic:
exact ((glueData hf).glue_condition i j).symm.trans (by simp [toGlued])

Premises used: AlgebraicGeometry.Scheme.GlueData.glue_condition, AlgebraicGeometry.Scheme.LocalRepresentability.glueData, Eq.symm, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
j : ι
⊢ PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover) j = toGlued hf j

Tactic:
rfl

Premises used: CategoryTheory.GlueData.ι, AlgebraicGeometry.Scheme.LocalRepresentability.toGlued, rfl, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  Eq (α := F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U)) → F.obj.obj (op U))
        α :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U)) → F.obj.obj (op U))
        β :
      F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U))
⊢ Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        α :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        β :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))

Tactic:
replace h : (yonedaGluedToSheaf hf).hom.app _ α = (yonedaGluedToSheaf hf).hom.app _ β := h
-- Module: Mathlib.AlgebraicGeometry.Sites.Representability
Goal:
F : Sheaf zariskiTopology (Type u)
ι : Type u
X : ι → Scheme
f : (i : ι) → Functor.obj yoneda (X i) ⟶ F.obj (P := Presheaf.IsSheaf zariskiTopology)
hf : ∀ (i : ι), IsOpenImmersion.presheaf (f i)
i j k : ι
U : Scheme
α β : U ⟶ (glueData hf).glued
h :
  Eq (α := (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        α :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) ((yonedaGluedToSheaf hf).hom.app (op U)) :
          (a : (fun (X : Type u) ↦ X) ((zariskiTopology.yoneda.obj (glueData hf).glued).obj.obj (op U))) →
            (fun (X : Type u) ↦ X) (F.obj.obj (op U)))
        β :
      (fun (X : Type u) ↦ X) (F.obj (P := Presheaf.IsSheaf zariskiTopology).obj (op U)))
⊢ Membership.mem (γ := Set (Sieve (glueData hf).glued))
    ((grothendieckTopology IsOpenImmersion : (a : Scheme) → Set (Sieve a)) (glueData hf).glued)
    (Sieve.ofArrows (I :=
      PreZeroHypercover.I₀ (S := (glueData hf).glued)
        (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.X (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover))
      (PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover (glueData hf).openCover)))

Tactic:
have mem := (glueData hf).openCover.mem_grothendieckTopology