awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ Epi (D.f i i).base

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
erw :
  D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        NatTrans.app
            (Cone.π
              { pt := (D.U i).presheaf.obj (op U),
                π :=
                  { app := fun (j : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ) ↦ D.ιInvAppπApp U (unop j),
                    naturality := ⋯ } })
            (op (WalkingMultispan.left (i, j))) ≫
          𝟙
            ((componentwiseDiagram D.diagram.multispan
                  (Functor.obj
                      (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                        Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                      U :
                    Opens (↑(↑D.glued : TopCat) : Type v))).obj
              (op (WalkingMultispan.left (i, j)))) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
      𝟙
        ((componentwiseDiagram D.diagram.multispan
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v))).obj
          (op (WalkingMultispan.left (i, j))))
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        D.ιInvApp U ≫
          limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
            𝟙
              ((componentwiseDiagram D.diagram.multispan
                    (Functor.obj
                        (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                          Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                        U :
                      Opens (↑(↑D.glued : TopCat) : Type v))).obj
                (op (WalkingMultispan.left (i, j)))) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
      𝟙
        ((componentwiseDiagram D.diagram.multispan
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v))).obj
          (op (WalkingMultispan.left (i, j))))

Tactic:
erw [limit.lift_π_assoc]

Premises used: CategoryTheory.Limits.limit.lift_π_assoc
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
rw :
  Eq (α :=
    limit (D.diagramOverOpen U) ⟶
      (componentwiseDiagram D.diagram.multispan
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U :
              Opens (↑(↑D.glued : TopCat) : Type v))).obj
        (op (WalkingMultispan.left (i, j))))
    (D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        NatTrans.app
          (Cone.π
            { pt := (D.U i).presheaf.obj (op U),
              π :=
                { app := fun (j : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ) ↦ D.ιInvAppπApp U (unop j),
                  naturality := ⋯ } })
          (op (WalkingMultispan.left (i, j))))
    (limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))))
⊢ D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        NatTrans.app
            (Cone.π
              { pt := (D.U i).presheaf.obj (op U),
                π :=
                  { app := fun (j : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ) ↦ D.ιInvAppπApp U (unop j),
                    naturality := ⋯ } })
            (op (WalkingMultispan.left (i, j))) ≫
          𝟙
            ((componentwiseDiagram D.diagram.multispan
                  (Functor.obj
                      (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                        Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                      U :
                    Opens (↑(↑D.glued : TopCat) : Type v))).obj
              (op (WalkingMultispan.left (i, j)))) =
    limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))) ≫
      𝟙
        ((componentwiseDiagram D.diagram.multispan
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v))).obj
          (op (WalkingMultispan.left (i, j))))

Tactic:
rw [Category.comp_id, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ Eq (α :=
    limit
        (componentwiseDiagram D.diagram.multispan
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U :
            Opens (↑(↑D.glued : TopCat) : Type v))) ⟶
      (componentwiseDiagram D.diagram.multispan
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U :
              Opens (↑(↑D.glued : TopCat) : Type v))).obj
        (op (WalkingMultispan.left (i, j))))
    (CategoryStruct.comp (Y :=
      (componentwiseDiagram D.diagram.multispan
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U :
              Opens (↑(↑D.glued : TopCat) : Type v))).obj
        (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (i, j)))))
      (limit.π
        (componentwiseDiagram D.diagram.multispan
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U :
            Opens (↑(↑D.glued : TopCat) : Type v)))
        (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (i, j)))))
      ((componentwiseDiagram D.diagram.multispan
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U :
              Opens (↑(↑D.glued : TopCat) : Type v))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (i, j)))))
    (limit.π
      (componentwiseDiagram D.diagram.multispan
        (Functor.obj
            (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
              Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
            U :
          Opens (↑(↑D.glued : TopCat) : Type v)))
      (op (WalkingMultispan.left (i, j))))

Tactic:
limit.w (componentwiseDiagram 𝖣.diagram.multispan _)
        (Quiver.Hom.op (WalkingMultispan.Hom.fst (i, j)))

Premises used: CategoryTheory.GlueData.diagram, Quiver.Hom.op, AlgebraicGeometry.PresheafedSpace.componentwiseDiagram, CategoryTheory.Limits.WalkingMultispan.Hom.fst, CategoryTheory.Limits.MultispanIndex.multispan, CategoryTheory.Limits.limit.w, AlgebraicGeometry.PresheafedSpace.GlueData.toGlueData
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
rw :
  Mono (X :=
    (componentwiseDiagram D.diagram.multispan
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U :
            Opens (↑(↑D.glued : TopCat) : Type v))).obj
      (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))
    (Y :=
    (componentwiseDiagram D.diagram.multispan
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U :
            Opens (↑(↑D.glued : TopCat) : Type v))).obj
      (op (WalkingMultispan.left (i, j))))
    ((componentwiseDiagram D.diagram.multispan
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U :
            Opens (↑(↑D.glued : TopCat) : Type v))).map
      (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))))
⊢ Mono (X :=
    (componentwiseDiagram D.diagram.multispan
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U :
            Opens (↑(↑D.glued : TopCat) : Type v))).obj
      (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))
    ((componentwiseDiagram D.diagram.multispan
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U :
              Opens (↑(↑D.glued : TopCat) : Type v))).map
        (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫
      𝟙
        ((componentwiseDiagram D.diagram.multispan
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v))).obj
          (op (WalkingMultispan.left (i, j)))))

Tactic:
rw [Category.comp_id]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst_1 : Category.{v, u} C
D : GlueData.{v, u} C
inst_2 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
inst :
  Mono (X :=
    (D.U j).presheaf.obj
      (op ((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U)))))
    ((D.f j i).c.app
      (op ((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U)))))
⊢ Mono (X :=
    (D.U j).presheaf.obj
      (op
        (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
          (Opens.map
              (Hom.base
                (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j))))))) :
            Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
              Opens
                (↑(↑(D.diagram.multispan.obj
                          (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))) :
                      TopCat) :
                  Type v))
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U :
            Opens (↑(↑D.glued : TopCat) : Type v)))))
    ((D.f j i).c.app
      (op
        (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
          (Opens.map
              (Hom.base
                (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j))))))) :
            Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
              Opens
                (↑(↑(D.diagram.multispan.obj
                          (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))) :
                      TopCat) :
                  Type v))
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U :
            Opens (↑(↑D.glued : TopCat) : Type v)))))

Tactic:
erw [D.ι_image_preimage_eq i j U]

Premises used: AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ Mono (X :=
    (D.U j).presheaf.obj
      (op ((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U)))))
    ((D.f j i).c.app
      (op ((opensFunctor (D.f j i)).obj ((Opens.map (D.t j i).base).obj ((Opens.map (D.f i j).base).obj U)))))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ IsIso (D.t i j).c

Tactic:
apply c_isIso_of_iso

Premises used: AlgebraicGeometry.PresheafedSpace.c_isIso_of_iso
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ IsIso (D.t i j).c

Tactic:
have : IsIso (D.t i j).c := by apply c_isIso_of_iso
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
this : IsIso (D.t i j).c
⊢ Mono (X :=
    (Functor.obj (TopCat.Presheaf.pushforward C (D.f j i).base) (D.V (j, i)).presheaf).obj
      (op
        (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
          (Opens.map
              (Hom.base
                (colimit.ι D.diagram.multispan
                  (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j))))))) :
            Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
              Opens
                (↑(↑(D.diagram.multispan.obj
                          (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))) :
                      TopCat) :
                  Type v))
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U :
            Opens (↑(↑D.glued : TopCat) : Type v)))))
    ((D.t i j).c.app
      (op
        ((Opens.map (D.f j i).base).obj
          (unop
            (op
              (Functor.obj (C := Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v))
                (Opens.map
                    (Hom.base
                      (colimit.ι D.diagram.multispan
                        (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j))))))) :
                  Opens (↑(↑(Limits.colimit D.diagram.multispan) : TopCat) : Type v) ⥤
                    Opens
                      (↑(↑(D.diagram.multispan.obj
                                (unop (op (WalkingMultispan.right ((MultispanShape.prod D.J).snd (i, j)))))) :
                            TopCat) :
                        Type v))
                (Functor.obj
                    (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                      Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                    U :
                  Opens (↑(↑D.glued : TopCat) : Type v))))))))

Tactic:
infer_instance
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
w :
  ∀ (j : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ),
    (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ limit.π (D.diagramOverOpen U) j =
      𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) j
⊢ D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U))

Tactic:
ext j
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
j : WalkingMultispan (MultispanShape.prod D.J)
⊢ Eq (α := limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op j))
    ((D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ limit.π (D.diagramOverOpen U) (op j))
    (𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op j))

Tactic:
?_
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
j : (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ
w :
  ∀ (j : WalkingMultispan (MultispanShape.prod D.J)),
    Eq (α := limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op j))
      ((D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ limit.π (D.diagramOverOpen U) (op j))
      (𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op j))
⊢ (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ limit.π (D.diagramOverOpen U) j =
    𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) j

Tactic:
induction j with | op j => ?_

Premises used: Opposite.op
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
j : WalkingMultispan (MultispanShape.prod D.J)
w :
  ∀ (j k : D.J),
    Eq (α := limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.left (j, k))))
      ((D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
        limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (j, k))))
      (𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (j, k))))
w₁ :
  ∀ (j : (MultispanShape.prod D.J).R),
    Eq (α := limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right j)))
      ((D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫
        limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)))
      (𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j)))
⊢ Eq (α := limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op j))
    ((D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U) ≫ limit.π (D.diagramOverOpen U) (op j))
    (𝟙 (limit (D.diagramOverOpen U)) ≫ limit.π (D.diagramOverOpen U) (op j))

Tactic:
rcases j with (⟨j, k⟩ | ⟨j⟩)
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
j k : D.J
w :
  Eq (α :=
    limit (D.diagramOverOpen U) ⟶
      (componentwiseDiagram D.diagram.multispan
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U :
              Opens (↑(↑D.glued : TopCat) : Type v))).obj
        (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))))
    (D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        CategoryStruct.comp (Y := limit (D.diagramOverOpen U)) (D.ιInvApp U)
          (limit.π
            (componentwiseDiagram D.diagram.multispan
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v)))
            (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))))
    (limit.π
      (componentwiseDiagram D.diagram.multispan
        (Functor.obj
            (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
              Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
            U :
          Opens (↑(↑D.glued : TopCat) : Type v)))
      (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))))
⊢ Eq (α :=
    limit (D.diagramOverOpen U) ⟶
      (componentwiseDiagram D.diagram.multispan
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U :
              Opens (↑(↑D.glued : TopCat) : Type v))).obj
        (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))))
    (CategoryStruct.comp (Y := limit (D.diagramOverOpen U)) (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U)
      (limit.π
        (componentwiseDiagram D.diagram.multispan
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U :
            Opens (↑(↑D.glued : TopCat) : Type v)))
        (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))))
    (limit.π
      (componentwiseDiagram D.diagram.multispan
        (Functor.obj
            (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
              Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
            U :
          Opens (↑(↑D.glued : TopCat) : Type v)))
      (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))))

Tactic:
simp_rw [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
j k : D.J
⊢ Eq (α :=
    limit (D.diagramOverOpen U) ⟶
      (componentwiseDiagram D.diagram.multispan
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U :
              Opens (↑(↑D.glued : TopCat) : Type v))).obj
        (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))))
    (D.diagramOverOpenπ U i ≫
      D.ιInvAppπEqMap U ≫
        CategoryStruct.comp (Y := limit (D.diagramOverOpen U)) (D.ιInvApp U)
          (limit.π
            (componentwiseDiagram D.diagram.multispan
              (Functor.obj
                  (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                    Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                  U :
                Opens (↑(↑D.glued : TopCat) : Type v)))
            (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k))))))
    (limit.π
      (componentwiseDiagram D.diagram.multispan
        (Functor.obj
            (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
              Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
            U :
          Opens (↑(↑D.glued : TopCat) : Type v)))
      (op (WalkingMultispan.right ((MultispanShape.prod D.J).fst (j, k)))))

Tactic:
apply π_ιInvApp_π

Premises used: AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π