-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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
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
have h : ∀
  (eq₂ :
    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.ι j) :
            (a : (↑(D.U j) : 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.ι i) :
            (a : (↑(D.U i) : Type u)) → (↑D.glued : Type u))
          x₁ :
        (↑D.glued : Type u))),
  Membership.mem (α := (↑D.glued : Type u)) (γ := 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)))
    ((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))
Tactic: substs eq₁
Cleared hypotheses: x, eq₁, eq₂