-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
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))
rw :
  Eq (α := (↑(D.U (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) : 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.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))
        ((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.t (b.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))
                  (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) :
              (a_1 : (↑(D.V (b.fst, a.fst)) : Type u)) → (↑(D.V (a.fst, 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)) :
          (↑(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)) :
      (↑(D.U (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) : 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.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 :
      (↑(D.U (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) : 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.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))
      ((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.t (b.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))
                (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) :
            (a_1 : (↑(D.V (b.fst, a.fst)) : Type u)) → (↑(D.V (a.fst, 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)) :
        (↑(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)) =
    a.snd (β := fun (i : D.J) ↦ (↑(D.U i) : Type u))
have rw₁ : Eq (α := (↑(D.U (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) : 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.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 :
    (↑(D.U (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) : 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.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 :
    (↑(D.U (a.fst (β := fun (i : D.J) ↦ (↑(D.U i) : Type u)))) : Type u))
Tactic: rw [← e₁, D.t_inv_apply]