awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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 (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right j)))
    (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j) (D.diagramOverOpenπ U j)
have rw : Eq (α :=
  limit (D.diagramOverOpen U) ⟶
    (componentwiseDiagram D.diagram.multispan
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                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)) sorry :
                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)))))
    (D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j :
      limit (D.diagramOverOpen U) ⟶ (D.diagramOverOpen U).obj (op (WalkingMultispan.right j)))
    ((componentwiseDiagram D.diagram.multispan
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                  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)) sorry :
                    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 j ≫
    (componentwiseDiagram D.diagram.multispan
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                  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)) sorry :
                    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 [← @cancel_mono
          (f := (componentwiseDiagram 𝖣.diagram.multispan _).map
            (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫ 𝟙 _) ..]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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)
⊢ 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))))
have 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 := sorry } })
          (op (WalkingMultispan.left (i, j))) ≫
        𝟙
          ((componentwiseDiagram D.diagram.multispan
                (Functor.obj
                    (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                      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)) sorry :
                  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]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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)
⊢ 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))))
have rw : Eq (α :=
  limit (D.diagramOverOpen U) ⟶
    (componentwiseDiagram D.diagram.multispan
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                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 := sorry } })
        (op (WalkingMultispan.left (i, j))))
  (limit.π (D.diagramOverOpen U) (op (WalkingMultispan.left (i, j))))
Tactic: rw [Category.comp_id, Category.comp_id]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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 :=
    (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)))))
have rw : Mono (X :=
  (componentwiseDiagram D.diagram.multispan
        (Functor.obj
            (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
              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)) sorry :
              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)) sorry :
              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))))
Tactic: rw [Category.comp_id]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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
        (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)))))
have 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)))))
Tactic: erw [D.ι_image_preimage_eq i j U]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (hypothesis)
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 :=
    (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))))))))
have this : IsIso (D.t i j).c
Tactic: have : IsIso (D.t i j).c := by apply c_isIso_of_iso
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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)
⊢ D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 (limit (D.diagramOverOpen U))
have 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
Tactic: ext j
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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))ᵒᵖ
⊢ (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
have 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))
Tactic: induction j with | op j => ?_
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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))
have 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))))
Tactic: rcases j with (⟨j, k⟩ | ⟨j⟩)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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))))
⊢ 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))
have 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)))
Tactic: rcases j with (⟨j, k⟩ | ⟨j⟩)
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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)))))
    (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)))))
have w : Eq (α :=
  limit (D.diagramOverOpen U) ⟶
    (componentwiseDiagram D.diagram.multispan
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                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)) sorry :
                  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)) sorry :
            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]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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 : (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)))
have w : 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)))
Tactic: simp_rw [Category.assoc]
-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
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 : (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)))
have w : 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) (op (WalkingMultispan.right j)))
Tactic: rw [Category.id_comp]