-- Lean 4 proof step from Mathlib.Topology.Gluing (goal)
Goal:
D : GlueData
i j : D.J
U : Set (↑(D.U i) : Type u)
this :
  Eq (α := Set (↑(D.V (j, i)) : Type u))
    (Set.preimage (β := (↑(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))
      (Set.preimage (β := (↑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))
        ((⇑(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)) ''
          U)))
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (D.t j i ≫ D.f i j)) :
        (a : (↑(D.V (j, i)) : Type u)) → (↑(D.U i) : Type u)) ⁻¹'
      U)
⊢ Eq (α := Set (↑(D.U j) : Type u))
    (Set.preimage (β := (↑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))
      ((⇑(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)) ''
        U))
    (Set.preimage (β := (↑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))
        ((⇑(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)) ''
          U) ∩
      Set.range (ι := (↑(D.V (j, i)) : 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)))
have symm : Eq (α := Set (↑(D.U j) : Type u))
  (Set.preimage (β := (↑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))
      ((⇑(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)) ''
        U) ∩
    Set.range (ι := (↑(D.V (j, i)) : 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)))
  (Set.preimage (β := (↑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))
    ((⇑(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)) ''
      U))
Tactic: symm