-- Module: Mathlib.Topology.Gluing
Goal:
D : GlueData
i j : D.J
x : (↑D.glued : Type u)
x₁ : (↑(D.U i) : Type u)
eq₁ :
  (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₁ =
    x
x₂ : (↑(D.U j) : Type u)
eq₂ :
  (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))
      x₂ =
    x
h :
  ∀
    (y :
      (↑(D.V
            (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x₁),
              Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j x₂))) :
        Type u))
    (e₁ :
      Eq (α :=
        (↑(D.U
              (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x₁))) :
          Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                D.V
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x₁),
                    Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                      (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j x₂)))
                (D.f
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x₁))
                  (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                    (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) j x₂))) :
              (a : (↑(D.V (⟨i, x₁⟩.fst, ⟨j, x₂⟩.fst)) : Type u)) → (↑(D.U ⟨i, x₁⟩.fst) : Type u))
            y :
          (↑(D.U
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x₁))) :
            Type u))
        (Sigma.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
            (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x₁) :
          (↑(D.U
                (Sigma.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
                  (Sigma.mk (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)) i x₁))) :
            Type u))),
    Membership.mem (γ := Set (↑D.glued : Type u))
      (Set.range (ι := (↑(D.V (i, j)) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
              D.glued) (D.f i j ≫ D.ι i)) :
          (a : (↑(D.V (i, j)) : Type u)) → (↑D.glued : Type u)))
      x
⊢ Membership.mem (γ := Set (↑D.glued : Type u))
    (Set.range (ι := (↑(D.V (i, j)) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            D.glued) (D.f i j ≫ D.ι i)) :
        (a : (↑(D.V (i, j)) : Type u)) → (↑D.glued : Type u)))
    x

Tactic:
obtain ⟨y, e₁, -⟩ := (D.ι_eq_iff_rel _ _ _ _).mp (eq₁.trans eq₂.symm)

Premises used: Iff.mp, TopCat.GlueData.ι_eq_iff_rel, Eq.symm, Eq.trans