-- Module: Mathlib.CategoryTheory.Limits.Types.Pullbacks
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
this :
  Eq (α := (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (⇑(hom (FC := TypeCat.Fun) fst) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (Function.comp (β := X × Y) _root_.Prod.fst
      (Function.comp (β :=
        { p : X × Y //
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
              (fun (X : Type u) ↦ X) Z) })
        (Subtype.val (p := fun (p : X × Y) ↦
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
              (fun (X : Type u) ↦ X) Z)))
        (⇑(hom (FC := TypeCat.Fun) e.hom) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (PullbackObj f g))))
rw :
  Eq (α := Set ((fun (X : Type u) ↦ X) X))
    (Set.image (α := X × Y) _root_.Prod.fst
      (Set.image (α :=
        { p : X × Y //
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
              (fun (X : Type u) ↦ X) Z) })
        (Subtype.val (p := fun (p : X × Y) ↦
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
              (fun (X : Type u) ↦ X) Z)))
        Set.univ))
    (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
      (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)
      (Set.range (ι := (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)))
⊢ Eq (α := Set ((fun (X : Type u) ↦ X) X))
    (Set.range (ι := (fun (X : Type u) ↦ X) P)
      (⇑(hom (FC := TypeCat.Fun) fst) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X))
    (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
      (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)
      (Set.range (ι := (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)))

Tactic:
rw [this, Set.range_comp, Set.range_comp, Set.range_eq_univ.mpr (surjective_of_epi e.hom)]

Premises used: Iff.mpr, Set.range_eq_univ, Set.range_comp, CategoryTheory.surjective_of_epi, CategoryTheory.Iso.hom