awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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
have 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
Tactic: rw [← 𝖣.t_fac_assoc]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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 = D.t' j i k ≫ pullback.snd (D.f i k) (D.f i j) ≫ D.f i j
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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
have 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
Tactic: rw [← 𝖣.t_fac_assoc]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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 ≫ 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
have 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
Tactic: apply @Epi.left_cancellation _ _ _ _ (D.t' k j i)
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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' 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
have 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)
Tactic: rw [𝖣.cocycle_assoc, 𝖣.t_fac_assoc, 𝖣.t_inv_assoc]
-- Lean 4 proof step from Mathlib.Topology.Gluing (hypothesis)
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)
⊢ Relation.EqvGen
    (Function.Coequalizer.Rel (α := (↑(∐ D.diagram.left) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.fstSigmaMap) :
        (a : (↑(∐ D.diagram.left) : Type u)) → (↑(∐ D.diagram.right) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            ∐ D.diagram.left) (Y := ∐ D.diagram.right) D.diagram.sndSigmaMap) :
        (a : (↑(∐ D.diagram.left) : Type u)) → (↑(∐ D.diagram.right) : Type u)))
    x y
have this : 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
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
x : (↑(D.U i) : Type u)
y : (↑(D.U j) : 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)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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)
⊢ 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)
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
x : (↑(D.U i) : Type u)
y : (↑(D.U j) : 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)
have 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)
Tactic: delta GlueData.ι
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
x : (↑(D.U i) : Type u)
y : (↑(D.U j) : 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) (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)
have 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)
Tactic: simp_rw [← Multicoequalizer.ι_sigmaπ]
-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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))
⊢ 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)
have 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)
Tactic: rw [←
      show _ = Sigma.mk i x from ConcreteCategory.congr_hom (sigmaIsoSigma.{_, u} D.U).inv_hom_id _]