awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Germ
Goal:
α : Type u_4
l : Filter α
R : Type u_5
inst : CommMonoid R
ι : Type u_6
f : ι → α → R
s : Finset ι
⊢ Eq (α := l.Germ R) (↑(∏ i ∈ s, f i) : l.Germ R) (∏ i ∈ s, (↑(f i) : l.Germ R))

Tactic:
map_prod (Germ.coeMulHom l : (α → R) →* Germ l R) f s

Premises used: Filter.Germ.ofFun, map_prod, Quotient.mk', Filter.Germ.coeMulHom
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
⊢ Function.Surjective (α := (↑D.sigmaOpens : Type u)) (β := (↑D.glued : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            D.sigmaOpens) (Y := D.glued) (D.π : D.sigmaOpens ⟶ D.glued) :
          C((↑D.sigmaOpens : Type u), (↑D.glued : Type u))) :
      (a : (↑D.sigmaOpens : Type u)) → (↑D.glued : Type u))

Tactic:
(TopCat.epi_iff_surjective 𝖣.π).mp inferInstance

Premises used: TopCat.GlueData.toGlueData, inferInstance, Iff.mp, TopCat.epi_iff_surjective, CategoryTheory.GlueData.π
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
U : Set (↑D.glued : Type u)
simp_rw :
  IsOpen U ↔
    ∀ (i : D.J),
      IsOpen (X := (↑(D.U i) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                D.glued)
                (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                  (Multicoequalizer.sigmaπ D.diagram))) :
            (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ⁻¹'
          U)
⊢ IsOpen U ↔
    ∀ (i : D.J),
      IsOpen (X := (↑(D.U i) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                D.glued) (Multicoequalizer.π D.diagram i)) :
            (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ⁻¹'
          U)

Tactic:
simp_rw [← Multicoequalizer.ι_sigmaπ 𝖣.diagram]
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
U : Set (↑D.glued : Type u)
rw :
  IsOpen (X :=
      (↑(coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap) :
        Type u))
      ((⇑(homeoOfIso (Iso.symm (Multicoequalizer.isoCoequalizer D.diagram))) :
          (a : (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u)) →
            (↑(multicoequalizer D.diagram) : Type u)) ⁻¹'
        U) ↔
    ∀ (i : D.J),
      IsOpen (X := (↑(D.U i) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                D.glued)
                (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                  (Multicoequalizer.sigmaπ D.diagram))) :
            (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ⁻¹'
          U)
⊢ IsOpen U ↔
    ∀ (i : D.J),
      IsOpen (X := (↑(D.U i) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                D.glued)
                (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                  (Multicoequalizer.sigmaπ D.diagram))) :
            (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ⁻¹'
          U)

Tactic:
rw [← (homeoOfIso (Multicoequalizer.isoCoequalizer 𝖣.diagram).symm).isOpen_preimage]
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
U : Set (↑D.glued : Type u)
rw :
  (∀ (j : Discrete (MultispanShape.prod D.J).R),
      IsOpen (X := (↑(Functor.obj (Discrete.functor D.diagram.right) j) : Type u))
        (Set.preimage (β := (↑(colimit (Discrete.functor D.diagram.right)) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                Functor.obj (Discrete.functor D.diagram.right) j) (Y := colimit (Discrete.functor D.diagram.right))
                (colimit.ι (Discrete.functor D.diagram.right) j)) :
            (a : (↑((Discrete.functor D.diagram.right).obj j) : Type u)) →
              (↑(colimit (Discrete.functor D.diagram.right)) : Type u))
          (Set.preimage (β :=
            (↑(coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                  D.diagram.sndSigmaMap) :
              Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  (X := ∐ D.diagram.right) (Y :=
                  coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap
                    D.diagram.sndSigmaMap)
                  (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) :
              (a : (↑(∐ D.diagram.right) : Type u)) →
                (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u))
            ((⇑(homeoOfIso (Iso.symm (Multicoequalizer.isoCoequalizer D.diagram))) :
                (a : (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u)) →
                  (↑(multicoequalizer D.diagram) : Type u)) ⁻¹'
              U)))) ↔
    ∀ (i : D.J),
      IsOpen (X := (↑(D.U i) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                D.glued)
                (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                  (Multicoequalizer.sigmaπ D.diagram))) :
            (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ⁻¹'
          U)
⊢ IsOpen (X :=
      (↑(coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap) :
        Type u))
      ((⇑(homeoOfIso (Iso.symm (Multicoequalizer.isoCoequalizer D.diagram))) :
          (a : (↑(coequalizer D.diagram.fstSigmaMap D.diagram.sndSigmaMap) : Type u)) →
            (↑(multicoequalizer D.diagram) : Type u)) ⁻¹'
        U) ↔
    ∀ (i : D.J),
      IsOpen (X := (↑(D.U i) : Type u))
        ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
                D.glued)
                (CategoryStruct.comp (Y := ∐ D.diagram.right) (Sigma.ι D.diagram.right i)
                  (Multicoequalizer.sigmaπ D.diagram))) :
            (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u)) ⁻¹'
          U)

Tactic:
rw [coequalizer_isOpen_iff, colimit_isOpen_iff.{u}]

Premises used: TopCat.coequalizer_isOpen_iff
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
x : (↑D.glued : Type u)
⊢ ∃ (i : D.J) (y : (↑(D.U i) : Type u)),
    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued) (D.ι i) :
          (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
        y =
      x

Tactic:
𝖣.ι_jointly_surjective (forget TopCat) x

Premises used: TopCat.GlueData.toGlueData, CategoryTheory.forget, TopCat, CategoryTheory.GlueData.ι_jointly_surjective
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
x : (i : D.J) × (↑(D.U i) : Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          D.V (x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)), x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))))
          (D.f (x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))) (x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) :
        (a : (↑(D.V (x.fst, x.fst)) : Type u)) → (↑(D.U x.fst) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              D.V (x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)), x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))))
              (D.t (x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))
                (x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) :
            (a : (↑(D.V (x.fst, x.fst)) : Type u)) → (↑(D.V (x.fst, x.fst)) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  D.U (x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) (Y :=
                  D.V
                    (x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)),
                      x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))))
                  (inv
                    (D.f (x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))
                      (x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))))) :
                (a : (↑(D.U x.fst) : Type u)) → (↑(D.V (x.fst, x.fst)) : Type u))
              (x.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))) :
            (↑(D.V
                  (x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)),
                    x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) :
              Type u)) :
        (↑(D.V (x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)), x.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) :
          Type u)) =
    x.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))

Tactic:
simp [IsIso.inv_hom_id_apply (D.f x.fst x.fst)]

Premises used: TopCat.GlueData.toGlueData, CategoryTheory.GlueData.f, Sigma.fst, CategoryTheory.IsIso.inv_hom_id_apply
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
a b : (i : D.J) × (↑(D.U i) : Type u)
x :
  (↑(D.V (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)), b.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) : Type u)
e₁ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          D.V (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)), b.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))))
          (D.f (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))) (b.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) :
        (a_1 : (↑(D.V (a.fst, b.fst)) : Type u)) → (↑(D.U a.fst) : Type u))
      x =
    a.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
e₂ :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          D.V (b.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)), a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))))
          (D.f (b.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))) (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) :
        (a : (↑(D.V (b.fst, a.fst)) : Type u)) → (↑(D.U b.fst) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              D.V (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)), b.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))))
              (D.t (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))
                (b.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) :
            (a_1 : (↑(D.V (a.fst, b.fst)) : Type u)) → (↑(D.V (b.fst, a.fst)) : Type u))
          x :
        (↑(D.V (b.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)), a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) :
          Type u)) =
    b.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
⊢ D.Rel b a

Tactic:
exact ⟨D.t _ _ x, e₂, by rw [← e₁, D.t_inv_apply]⟩
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j k : D.J
z : (↑(pullback (D.f j i) (D.f j k)) : Type u)
e₂ :
  Eq (α := (↑(D.U j) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j i) :
          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.t i j) :
              (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (D.t j i) :
                  (a : (↑(D.V (j, i)) : Type u)) → (↑(D.V (i, j)) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (X := pullback (D.f j i) (D.f j k)) (pullback.fst (D.f j i) (D.f j k)) :
                      (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, i)) : Type u))
                    z :
                  (↑(D.V (j, i)) : Type u)) :
              (↑(D.V (i, j)) : Type u)) :
          (↑(D.V (j, i)) : Type u)) :
      (↑(D.U j) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j k) :
          (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback (D.f j i) (D.f j k)) (pullback.snd (D.f j i) (D.f j k)) :
              (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, k)) : Type u))
            z :
          (↑(D.V (j, k)) : Type u)) :
      (↑(D.U j) : Type u))
rw : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = D.t' j i k ≫ pullback.snd (D.f i k) (D.f i j) ≫ D.f i j
⊢ D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j

Tactic:
rw [← 𝖣.t_fac_assoc]
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j k : D.J
z : (↑(pullback (D.f j i) (D.f j k)) : Type u)
e₂ :
  Eq (α := (↑(D.U j) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j i) :
          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.t i j) :
              (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (D.t j i) :
                  (a : (↑(D.V (j, i)) : Type u)) → (↑(D.V (i, j)) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (X := pullback (D.f j i) (D.f j k)) (pullback.fst (D.f j i) (D.f j k)) :
                      (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, i)) : Type u))
                    z :
                  (↑(D.V (j, i)) : Type u)) :
              (↑(D.V (i, j)) : Type u)) :
          (↑(D.V (j, i)) : Type u)) :
      (↑(D.U j) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j k) :
          (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback (D.f j i) (D.f j k)) (pullback.snd (D.f j i) (D.f j k)) :
              (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, k)) : Type u))
            z :
          (↑(D.V (j, k)) : Type u)) :
      (↑(D.U j) : Type u))
e_a :
  Eq (α := pullback (D.f i k) (D.f i j) ⟶ D.U i) (pullback.fst (D.f i k) (D.f i j) ≫ D.f i k)
    (pullback.snd (D.f i k) (D.f i j) ≫ D.f i j)
⊢ D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = D.t' j i k ≫ pullback.snd (D.f i k) (D.f i j) ≫ D.f i j

Tactic:
congr 1
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j k : D.J
z : (↑(pullback (D.f j i) (D.f j k)) : Type u)
e₂ :
  Eq (α := (↑(D.U j) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j i) :
          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.t i j) :
              (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (D.t j i) :
                  (a : (↑(D.V (j, i)) : Type u)) → (↑(D.V (i, j)) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (X := pullback (D.f j i) (D.f j k)) (pullback.fst (D.f j i) (D.f j k)) :
                      (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, i)) : Type u))
                    z :
                  (↑(D.V (j, i)) : Type u)) :
              (↑(D.V (i, j)) : Type u)) :
          (↑(D.V (j, i)) : Type u)) :
      (↑(D.U j) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j k) :
          (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback (D.f j i) (D.f j k)) (pullback.snd (D.f j i) (D.f j k)) :
              (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, k)) : Type u))
            z :
          (↑(D.V (j, k)) : Type u)) :
      (↑(D.U j) : Type u))
⊢ Eq (α := pullback (D.f i k) (D.f i j) ⟶ D.U i) (pullback.fst (D.f i k) (D.f i j) ≫ D.f i k)
    (pullback.snd (D.f i k) (D.f i j) ≫ D.f i j)

Tactic:
pullback.condition

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j k : D.J
z : (↑(pullback (D.f j i) (D.f j k)) : Type u)
e₂ :
  Eq (α := (↑(D.U j) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j i) :
          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.t i j) :
              (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (D.t j i) :
                  (a : (↑(D.V (j, i)) : Type u)) → (↑(D.V (i, j)) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (X := pullback (D.f j i) (D.f j k)) (pullback.fst (D.f j i) (D.f j k)) :
                      (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, i)) : Type u))
                    z :
                  (↑(D.V (j, i)) : Type u)) :
              (↑(D.V (i, j)) : Type u)) :
          (↑(D.V (j, i)) : Type u)) :
      (↑(D.U j) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j k) :
          (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback (D.f j i) (D.f j k)) (pullback.snd (D.f j i) (D.f j k)) :
              (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, k)) : Type u))
            z :
          (↑(D.V (j, k)) : Type u)) :
      (↑(D.U j) : Type u))
⊢ Eq (α := pullback (D.f i k) (D.f i j) ⟶ D.U i) (pullback.fst (D.f i k) (D.f i j) ≫ D.f i k)
    (pullback.snd (D.f i k) (D.f i j) ≫ D.f i j)

Tactic:
exact pullback.condition

Premises used: CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j k : D.J
z : (↑(pullback (D.f j i) (D.f j k)) : Type u)
e₂ :
  Eq (α := (↑(D.U j) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j i) :
          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.t i j) :
              (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (D.t j i) :
                  (a : (↑(D.V (j, i)) : Type u)) → (↑(D.V (i, j)) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (X := pullback (D.f j i) (D.f j k)) (pullback.fst (D.f j i) (D.f j k)) :
                      (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, i)) : Type u))
                    z :
                  (↑(D.V (j, i)) : Type u)) :
              (↑(D.V (i, j)) : Type u)) :
          (↑(D.V (j, i)) : Type u)) :
      (↑(D.U j) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j k) :
          (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback (D.f j i) (D.f j k)) (pullback.snd (D.f j i) (D.f j k)) :
              (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, k)) : Type u))
            z :
          (↑(D.V (j, k)) : Type u)) :
      (↑(D.U j) : Type u))
⊢ D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j

Tactic:
have h₁ : D.t' j i k ≫ pullback.fst _ _ ≫ D.f i k = pullback.fst _ _ ≫ D.t j i ≫ D.f i j := by
      rw [← 𝖣.t_fac_assoc]; congr 1; exact pullback.condition
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j k : D.J
z : (↑(pullback (D.f j i) (D.f j k)) : Type u)
e₂ :
  Eq (α := (↑(D.U j) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j i) :
          (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                (D.t i j) :
              (a : (↑(D.V (i, j)) : Type u)) → (↑(D.V (j, i)) : Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    (D.t j i) :
                  (a : (↑(D.V (j, i)) : Type u)) → (↑(D.V (i, j)) : Type u))
                ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                        (X := pullback (D.f j i) (D.f j k)) (pullback.fst (D.f j i) (D.f j k)) :
                      (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, i)) : Type u))
                    z :
                  (↑(D.V (j, i)) : Type u)) :
              (↑(D.V (i, j)) : Type u)) :
          (↑(D.V (j, i)) : Type u)) :
      (↑(D.U j) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (D.f j k) :
          (a : (↑(D.V (j, k)) : Type u)) → (↑(D.U j) : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback (D.f j i) (D.f j k)) (pullback.snd (D.f j i) (D.f j k)) :
              (a : (↑(pullback (D.f j i) (D.f j k)) : Type u)) → (↑(D.V (j, k)) : Type u))
            z :
          (↑(D.V (j, k)) : Type u)) :
      (↑(D.U j) : Type u))
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
rw :
  D.t' j i k ≫ D.t' i k j ≫ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i =
    pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j
⊢ D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.t i k ≫ D.f k i =
    pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j

Tactic:
rw [← 𝖣.t_fac_assoc]