awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a :
  D.t' k j i ≫ D.t' j i k ≫ D.t' i k j ≫ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i =
    D.t' k j i ≫ pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j
⊢ 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

Tactic:
apply @Epi.left_cancellation _ _ _ _ (D.t' k j i)

Premises used: CategoryTheory.Epi.left_cancellation
-- 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
a :
  Eq (α := pullback (D.f k j) (D.f k i) ⟶ D.U k) (pullback.snd (D.f k j) (D.f k i) ≫ D.f k i)
    (pullback.fst (D.f k j) (D.f k i) ≫ D.f k j)
⊢ D.t' k j i ≫ D.t' j i k ≫ D.t' i k j ≫ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i =
    D.t' k j i ≫ pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j

Tactic:
rw [𝖣.cocycle_assoc, 𝖣.t_fac_assoc, 𝖣.t_inv_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))
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
⊢ Eq (α := pullback (D.f k j) (D.f k i) ⟶ D.U k) (pullback.snd (D.f k j) (D.f k i) ≫ D.f k i)
    (pullback.fst (D.f k j) (D.f k i) ≫ D.f k j)

Tactic:
pullback.condition.symm

Premises used: CategoryTheory.Limits.pullback.condition, Eq.symm
-- 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
⊢ Eq (α := pullback (D.f k j) (D.f k i) ⟶ D.U k) (pullback.snd (D.f k j) (D.f k i) ≫ D.f k i)
    (pullback.fst (D.f k j) (D.f k i) ≫ D.f k j)

Tactic:
exact pullback.condition.symm

Premises used: CategoryTheory.Limits.pullback.condition, Eq.symm
-- 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
⊢ 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:
have h₂ : D.t' j i k ≫ pullback.fst _ _ ≫ D.t i k ≫ D.f k i =
        pullback.snd _ _ ≫ D.t j k ≫ D.f k j := by
      rw [← 𝖣.t_fac_assoc]
      apply @Epi.left_cancellation _ _ _ _ (D.t' k j i)
      rw [𝖣.cocycle_assoc, 𝖣.t_fac_assoc, 𝖣.t_inv_assoc]
      exact pullback.condition.symm
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
x y : (↑(∐ D.U) : Type u)
h :
  Eq (α := (↑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)
            (CategoryStruct.comp (Y :=
              coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap)
              (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)
              (Iso.inv (Multicoequalizer.isoCoequalizer D.diagram))) :
          (a : (↑D.sigmaOpens : Type u)) → (↑D.glued : Type u))
        x :
      (↑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)
            (CategoryStruct.comp (Y :=
              coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap)
              (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)
              (Iso.inv (Multicoequalizer.isoCoequalizer D.diagram))) :
          (a : (↑D.sigmaOpens : Type u)) → (↑D.glued : Type u))
        y :
      (↑D.glued : Type u))
⊢ Eq (α :=
    (↑(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))
        x :
      (↑(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))
        y :
      (↑(coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap) :
        Type u))

Tactic:
replace h : coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap x =
      coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap y :=
    (TopCat.mono_iff_injective (Multicoequalizer.isoCoequalizer 𝖣.diagram).inv).mp
    inferInstance h
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
x y : (↑(∐ D.U) : Type u)
h :
  Eq (α :=
    (↑(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))
        x :
      (↑(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))
        y :
      (↑(coequalizer (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap) :
        Type u))
diagram : WalkingParallelPair ⥤ Type u :=
  parallelPair (X := ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap D.diagram.sndSigmaMap ⋙
    forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
⊢ Eq (α := (fun (X : Type u) ↦ X) (colimit diagram))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι diagram one) :
          (a : (fun (X : Type u) ↦ X) (diagram.obj one)) → (fun (X : Type u) ↦ X) (colimit diagram))
        x :
      (fun (X : Type u) ↦ X) (colimit diagram))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (colimit.ι diagram one) :
          (a : (fun (X : Type u) ↦ X) (diagram.obj one)) → (fun (X : Type u) ↦ X) (colimit diagram))
        y :
      (fun (X : Type u) ↦ X) (colimit diagram))

Tactic:
have : colimit.ι diagram one x = colimit.ι diagram one y := by
    dsimp only [coequalizer.π] at h
    rw [← ι_preservesColimitIso_hom, ConcreteCategory.forget_map_eq_ofHom, types_comp_apply]
    simp_all
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
x : (↑(D.U i) : Type u)
y : (↑(D.U j) : Type u)
mp :
  Eq (α := (↑D.glued : 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))
          x :
        (↑D.glued : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              D.glued) (D.ι j) :
            (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
          y :
        (↑D.glued : Type u)) →
    D.Rel (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x)
      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y)
mpr :
  D.Rel (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x)
      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y) →
    Eq (α := (↑D.glued : 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))
          x :
        (↑D.glued : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              D.glued) (D.ι j) :
            (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
          y :
        (↑D.glued : Type u))
⊢ Eq (α := (↑D.glued : 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))
          x :
        (↑D.glued : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              D.glued) (D.ι j) :
            (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
          y :
        (↑D.glued : Type u)) ↔
    D.Rel (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x)
      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y)

Tactic:
constructor
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
x : (↑(D.U i) : Type u)
y : (↑(D.U j) : Type u)
mp :
  Eq (α := (↑D.glued : 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))
          x :
        (↑D.glued : 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 j) :
            (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
          y :
        (↑D.glued : Type u)) →
    D.Rel (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x)
      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y)
⊢ Eq (α := (↑D.glued : 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))
          x :
        (↑D.glued : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              D.glued) (D.ι j) :
            (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
          y :
        (↑D.glued : Type u)) →
    D.Rel (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x)
      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y)

Tactic:
delta GlueData.ι

Premises used: CategoryTheory.GlueData.ι
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
x : (↑(D.U i) : Type u)
y : (↑(D.U j) : Type u)
mp :
  Eq (α := (↑D.glued : 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))
          x :
        (↑D.glued : 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 j)
                (Multicoequalizer.sigmaπ D.diagram)) :
            (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
          y :
        (↑D.glued : Type u)) →
    D.Rel (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x)
      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y)
⊢ Eq (α := (↑D.glued : 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))
          x :
        (↑D.glued : 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 j) :
            (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
          y :
        (↑D.glued : Type u)) →
    D.Rel (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x)
      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y)

Tactic:
simp_rw [← Multicoequalizer.ι_sigmaπ]

Premises used: CategoryTheory.Limits.Multicoequalizer.ι_sigmaπ
-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
x : (↑(D.U i) : Type u)
y : (↑(D.U j) : Type u)
h :
  Eq (α := (↑D.glued : 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))
        x :
      (↑D.glued : 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 j)
              (Multicoequalizer.sigmaπ D.diagram)) :
          (a : (↑(D.U j) : Type u)) → (↑D.glued : Type u))
        y :
      (↑D.glued : Type u))
mp :
  D.Rel
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
          ((sigmaIsoSigma D.U).inv ≫ (sigmaIsoSigma D.U).hom) :
        (a : (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u)) → (↑(of ((i : D.J) × (↑(D.U i) : Type u))) : Type u))
      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x))
    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y)
⊢ D.Rel (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x)
    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j y)

Tactic:
rw [←
      show _ = Sigma.mk i x from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]