awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
i j : Shrink.{u, w} J
f : Quiver.Hom.{v, w} (V := J) (↓i : J) (↓j : J)
this_1 : IsIso (X := (↑(V F (↓i) ↓j) : Scheme)) (Opens.ι (V F (↓i) ↓j))
this :
  Eq (α := (↑(V F (↓i) ↓j) : Scheme) ⟶ (glueData F).glued) (tAux F (↓i) ↓j ≫ (glueData F).ι j)
    (Opens.ι (V F (↓i) ↓j) ≫ (glueData F).ι i)
h :
  (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)), Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
        Scheme) =
      (↑(V F (↓i) ↓j) : Scheme) →
    CategoryStruct.comp (Y :=
        (↑(Hom.opensRange (X :=
              F.obj
                (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j))
                  (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)) (↓i) (𝟙 ↓i, f))))
              (F.map
                (Sigma.snd.{w, v} (α := J) (β := fun (k : J) ↦ Prod.{v, v} (k ⟶ ↓i) (k ⟶ ↓j))
                    (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)) (↓i) (𝟙 ↓i, f) :
                      (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j))).1)) :
          Scheme))
        (Opens.ι (V F (↓i) ↓j) ≫ Iso.hom (Hom.isoOpensRange (F.map (𝟙 ↓i)))) ((F.obj ↓i).homOfLE ⋯) =
      𝟙 (↑(V F (↓i) ↓j) : Scheme)
⊢ Eq (α := (↑(V F (↓i) ↓j) : Scheme) ⟶ (glueData F).glued)
    (CategoryStruct.comp (Y :=
      (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
            Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
        Scheme))
      (CategoryStruct.comp (Y :=
          (↑(Hom.opensRange (X :=
                F.obj
                  (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j))
                    (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)) (↓i) (𝟙 ↓i, f))))
                (F.map
                  (Sigma.snd.{w, v} (α := J) (β := fun (k : J) ↦ Prod.{v, v} (k ⟶ ↓i) (k ⟶ ↓j))
                      (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)) (↓i) (𝟙 ↓i, f) :
                        (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j))).1)) :
            Scheme))
          (Opens.ι (V F (↓i) ↓j) ≫ Iso.hom (Hom.isoOpensRange (F.map (𝟙 ↓i)))) ((F.obj ↓i).homOfLE ⋯) :
        (↑(V F (↓i) ↓j) : Scheme) ⟶
          (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
            Scheme))
      (tAux F (↓i) ↓j ≫ (glueData F).ι j :
        (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
            Scheme) ⟶
          (glueData F).glued))
    (tAux F (↓i) ↓j ≫ (glueData F).ι j)

Tactic:
convert! Category.id_comp _

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
i j : Shrink.{u, w} J
f : Quiver.Hom.{v, w} (V := J) (↓i : J) (↓j : J)
this_1 : IsIso (X := (↑(V F (↓i) ↓j) : Scheme)) (Opens.ι (V F (↓i) ↓j))
this :
  Eq (α := (↑(V F (↓i) ↓j) : Scheme) ⟶ (glueData F).glued) (tAux F (↓i) ↓j ≫ (glueData F).ι j)
    (Opens.ι (V F (↓i) ↓j) ≫ (glueData F).ι i)
e_4 :
  (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)), Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
      Scheme) =
    (↑(V F (↓i) ↓j) : Scheme)
⊢ CategoryStruct.comp (Y :=
      (↑(Hom.opensRange (X :=
            F.obj
              (Sigma.fst (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j))
                (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)) (↓i) (𝟙 ↓i, f))))
            (F.map
              (Sigma.snd.{w, v} (α := J) (β := fun (k : J) ↦ Prod.{v, v} (k ⟶ ↓i) (k ⟶ ↓j))
                  (Sigma.mk (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)) (↓i) (𝟙 ↓i, f) :
                    (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j))).1)) :
        Scheme))
      (Opens.ι (V F (↓i) ↓j) ≫ Iso.hom (Hom.isoOpensRange (F.map (𝟙 ↓i)))) ((F.obj ↓i).homOfLE ⋯) =
    𝟙 (↑(V F (↓i) ↓j) : Scheme)

Tactic:
simp [← cancel_mono (Opens.ι _), V]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.IsLocallyDirected.V, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
j : J
⊢ j = ↓((equivShrink J : (a : J) → Shrink.{u, w} J) j : Shrink.{u, w} J)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
i j : J
f : i ⟶ j
⊢ Eq (α := F.obj i ⟶ Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (glueData F).glued) j)
    (F.map f ≫
      CategoryStruct.comp (Y := F.obj ↓((equivShrink J : (a : J) → Shrink.{u, w} J) j : Shrink.{u, w} J))
        (F.map (eqToHom ⋯)) ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j)))
    (CategoryStruct.comp (Y := F.obj ↓((equivShrink J : (a : J) → Shrink.{u, w} J) i : Shrink.{u, w} J))
        (F.map (eqToHom ⋯)) ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) i)) ≫
      CategoryTheory.Functor.map (Functor.obj (Functor.const J) (glueData F).glued) f)

Tactic:
simp only [← IsIso.inv_comp_eq, ← Functor.map_inv, ← Functor.map_comp_assoc,
      glueDataι_naturality, Functor.const_obj_obj, Functor.const_obj_map, Category.comp_id]

Premises used: CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.Functor.map_inv, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_comp_assoc, AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
i j : (glueData F).J
dsimp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ Eq (α := (glueData F).diagram.left (i, j) ⟶ s.pt)
    ((glueData F).diagram.fst (i, j) ≫
      (fun (i : (MultispanShape.prod (glueData F).J).R) ↦
          (s.ι.app ↓i : F.obj ↓i ⟶ Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) s.pt) ↓i))
        ((MultispanShape.prod (glueData F).J).fst (i, j)))
    ((glueData F).diagram.snd (i, j) ≫
      (fun (i : (MultispanShape.prod (glueData F).J).R) ↦
          (s.ι.app ↓i : F.obj ↓i ⟶ Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) s.pt) ↓i))
        ((MultispanShape.prod (glueData F).J).snd (i, j)))

Tactic:
dsimp [glueData, GlueData.diagram]

Premises used: CategoryTheory.GlueData.diagram, AlgebraicGeometry.Scheme.IsLocallyDirected.glueData
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
i j : (glueData F).J
simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp only [t, IsOpenImmersion.lift_fac]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.t, AlgebraicGeometry.IsOpenImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
i j : (glueData F).J
apply :
  ∀
    (k :
      PreZeroHypercover.I₀ (S :=
        (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
          Scheme))
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))),
    PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))
          k ≫
        Opens.ι (V F (↓i) ↓j) ≫ s.ι.app ↓i =
      PreZeroHypercover.f
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
              Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))
          k ≫
        tAux F (↓i) ↓j ≫ s.ι.app ↓j
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
apply (Scheme.Opens.iSupOpenCover _).hom_ext _ _ fun k ↦ ?_

Premises used: AlgebraicGeometry.Scheme.Cover.hom_ext, AlgebraicGeometry.Scheme.Opens.iSupOpenCover
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
i j : (glueData F).J
k :
  PreZeroHypercover.I₀ (S :=
    (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
      Scheme))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))
simp :
  (Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)).ι ≫ s.ι.app ↓i =
    CategoryStruct.comp (Y :=
      (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
        Scheme))
      ((F.obj ↓i).homOfLE ⋯ :
        (↑(Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme) ⟶
          (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
            Scheme))
      (tAux F (↓i) ↓j ≫ s.ι.app ↓j :
        (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
            Scheme) ⟶
          s.pt)
⊢ PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))
        k ≫
      Opens.ι (V F (↓i) ↓j) ≫ s.ι.app ↓i =
    PreZeroHypercover.f
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))
        k ≫
      tAux F (↓i) ↓j ≫ s.ι.app ↓j

Tactic:
simp only [Opens.iSupOpenCover, V, Scheme.homOfLE_ι_assoc]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.V, AlgebraicGeometry.Scheme.homOfLE_ι_assoc, AlgebraicGeometry.Scheme.Opens.iSupOpenCover
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
i j : (glueData F).J
k :
  PreZeroHypercover.I₀ (S :=
    (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
      Scheme))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))
rw :
  Iso.hom (Hom.isoOpensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) ≫
      (Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)).ι ≫ s.ι.app ↓i =
    F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).2 ≫ s.ι.app ↓j
⊢ (Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)).ι ≫ s.ι.app ↓i =
    CategoryStruct.comp (Y :=
      (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
            Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
        Scheme))
      ((F.obj ↓i).homOfLE ⋯ :
        (↑(Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) : Scheme) ⟶
          (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
            Scheme))
      (tAux F (↓i) ↓j ≫ s.ι.app ↓j :
        (↑(⨆ (k : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
                Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
            Scheme) ⟶
          s.pt)

Tactic:
rw [homOfLE_tAux_assoc F ↓i ↓j k.2.1 k.2.2, Iso.eq_inv_comp]

Premises used: Prod.fst, Equiv.symm, CategoryTheory.Iso.eq_inv_comp, equivShrink, Sigma.snd, AlgebraicGeometry.Scheme.IsLocallyDirected.homOfLE_tAux_assoc, Prod.snd, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
i j : (glueData F).J
k :
  PreZeroHypercover.I₀ (S :=
    (↑(⨆ (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)),
          Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) :
      Scheme))
    (Precoverage.ZeroHypercover.toPreZeroHypercover
      (Opens.iSupOpenCover fun (i_1 : (k : J) × (k ⟶ ↓i) × (k ⟶ ↓j)) ↦
        Hom.opensRange (F.map i_1.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)))
⊢ Iso.hom (Hom.isoOpensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)) ≫
      (Hom.opensRange (F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).1)).ι ≫ s.ι.app ↓i =
    F.map k.snd (β := fun (k : J) ↦ (k ⟶ ↓i) × (k ⟶ ↓j)).2 ≫ s.ι.app ↓j

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
j : J
⊢ (cocone F).ι.app j ≫
      Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
        ⋯ =
    s.ι.app j

Tactic:
(Category.assoc _ _ _).trans ?_

Premises used: CategoryTheory.Category.assoc, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
j : J
refine :
  F.map (eqToHom ⋯) ≫
      CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
        ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
        (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
          ⋯) =
    s.ι.app j
⊢ (cocone F).ι.app j ≫
      Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
        ⋯ =
    s.ι.app j

Tactic:
refine (Category.assoc _ _ _).trans ?_

Premises used: CategoryTheory.Category.assoc, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
j : J
enter :
  CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
    ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
    (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i) ⋯)
| (F.map (eqToHom ⋯) ≫
      CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
        ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
        (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
          ⋯) :
    F.obj j ⟶ s.pt)

Tactic:
enter [2]
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
j : J
⊢ Eq (α := F.obj ↓((equivShrink J : (a : J) → Shrink.{u, w} J) j : Shrink.{u, w} J) ⟶ s.pt)
    (CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
      ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
      (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
        ⋯))
    (s.ι.app ↓((equivShrink J : (a : J) → Shrink.{u, w} J) j : Shrink.{u, w} J))

Tactic:
Multicoequalizer.π_desc _ _ _ _ _

Premises used: CategoryTheory.Limits.Multicoequalizer.π_desc
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
j : J
⊢ Eq (α := F.obj ↓((equivShrink J : (a : J) → Shrink.{u, w} J) j : Shrink.{u, w} J) ⟶ s.pt)
    (CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
      ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
      (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
        ⋯))
    (s.ι.app ↓((equivShrink J : (a : J) → Shrink.{u, w} J) j : Shrink.{u, w} J))

Tactic:
exact Multicoequalizer.π_desc _ _ _ _ _

Premises used: CategoryTheory.Limits.Multicoequalizer.π_desc
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
j : J
enter enter₁ :
  CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
    ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
    (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i) ⋯)
| (F.map (eqToHom ⋯) ≫
      CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
        ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
        (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
          ⋯) :
    F.obj j ⟶ s.pt)

Tactic:
enter [2]; tactic => exact Multicoequalizer.π_desc _ _ _ _ _

Premises used: CategoryTheory.Limits.Multicoequalizer.π_desc
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
j : J
conv_lhs :
  CategoryStruct.comp (Y := F.obj ↓((equivShrink J : (a : J) → Shrink.{u, w} J) j : Shrink.{u, w} J))
      (F.map (eqToHom ⋯)) (s.ι.app ↓((equivShrink J : (a : J) → Shrink.{u, w} J) j : Shrink.{u, w} J)) =
    s.ι.app j
⊢ F.map (eqToHom ⋯) ≫
      CategoryStruct.comp (Y := Functor.obj.{v, u, w, u + 1} (Functor.obj (Functor.const J) (cocone F).pt) j)
        ((glueData F).ι ((equivShrink J : (a : J) → Shrink.{u, w} J) j))
        (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
          ⋯) =
    s.ι.app j

Tactic:
conv_lhs => enter [2]; tactic => exact Multicoequalizer.π_desc _ _ _ _ _

Premises used: CategoryTheory.Limits.Multicoequalizer.π_desc
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
j : J
⊢ CategoryStruct.comp (Y := F.obj ↓((equivShrink J : (a : J) → Shrink.{u, w} J) j : Shrink.{u, w} J))
      (F.map (eqToHom ⋯)) (s.ι.app ↓((equivShrink J : (a : J) → Shrink.{u, w} J) j : Shrink.{u, w} J)) =
    s.ι.app j

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
m : (cocone F).pt ⟶ s.pt
hm : ∀ (j : J), (cocone F).ι.app j ≫ m = s.ι.app j
i : (MultispanShape.prod (glueData F).J).R
simp : Multicoequalizer.π (glueData F).diagram i ≫ m = (glueData F).ι i ≫ m
⊢ Multicoequalizer.π (glueData F).diagram i ≫ m =
    CategoryStruct.comp (Y := multicoequalizer (glueData F).diagram) (Multicoequalizer.π (glueData F).diagram i)
      (Multicoequalizer.desc (glueData F).diagram s.pt (fun (i : (MultispanShape.prod (glueData F).J).R) ↦ s.ι.app ↓i)
        ⋯)

Tactic:
simp [← hm ↓i, cocone, reassoc_of% glueDataι_naturality]

Premises used: AlgebraicGeometry.Scheme.IsLocallyDirected.cocone, AlgebraicGeometry.Scheme.IsLocallyDirected.glueDataι_naturality, Equiv.symm, equivShrink, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Gluing
Goal:
J : Type w
inst : Category.{v, w} J
F : CategoryTheory.Functor.{v, u, w, u + 1} J Scheme
inst_1 : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst_2 : (F ⋙ forget).IsLocallyDirected
inst_3 : Quiver.IsThin.{w, v} J
inst_4 : Small.{u, w} J
s : Cocone F
m : (cocone F).pt ⟶ s.pt
hm : ∀ (j : J), (cocone F).ι.app j ≫ m = s.ι.app j
i : (MultispanShape.prod (glueData F).J).R
⊢ Multicoequalizer.π (glueData F).diagram i ≫ m = (glueData F).ι i ≫ m

Tactic:
rfl