-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Pullbacks (goal)
Goal:
W X Y Z S T : TopCat
f₁ : W ⟶ S
f₂ : X ⟶ S
g₁ : Y ⟶ T
g₂ : Z ⟶ T
i₁ : W ⟶ Y
i₂ : X ⟶ Z
i₃ : S ⟶ T
H₃ : Mono i₃
eq₁ : f₁ ≫ i₃ = i₁ ≫ g₁
eq₂ : f₂ ≫ i₃ = i₂ ≫ g₂
x : (↑(pullback g₁ g₂) : Type u)
x₁ : (↑W : Type u)
hx₁ :
  Eq (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₁ :
          (a : (↑W : Type u)) → (↑Y : Type u))
        x₁ :
      (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback g₁ g₂) (pullback.fst g₁ g₂) :
          (a : (↑(pullback g₁ g₂) : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))
x₂ : (↑X : Type u)
hx₂ :
  Eq (α := (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₂ :
          (a : (↑X : Type u)) → (↑Z : Type u))
        x₂ :
      (↑Z : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback g₁ g₂) (pullback.snd g₁ g₂) :
          (a : (↑(pullback g₁ g₂) : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
a :
  Eq (α := (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (f₁ ≫ i₃) :
          (a : (↑W : Type u)) → (↑T : Type u))
        x₁ :
      (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₃ :
          (a : (↑S : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₂ :
              (a : (↑X : Type u)) → (↑S : Type u))
            x₂ :
          (↑S : Type u)) :
      (↑T : Type u))
a₁ :
  Eq (α := (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (i₁ ≫ g₁) :
          (a : (↑W : Type u)) → (↑T : Type u))
        x₁ :
      (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₃ :
          (a : (↑S : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₂ :
              (a : (↑X : Type u)) → (↑S : Type u))
            x₂ :
          (↑S : Type u)) :
      (↑T : Type u))
a₂ :
  Eq (α := (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (i₁ ≫ g₁) :
          (a : (↑W : Type u)) → (↑T : Type u))
        x₁ :
      (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (f₂ ≫ i₃) :
          (a : (↑X : Type u)) → (↑T : Type u))
        x₂ :
      (↑T : Type u))
a₃ :
  Eq (α := (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (i₁ ≫ g₁) :
          (a : (↑W : Type u)) → (↑T : Type u))
        x₁ :
      (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (i₂ ≫ g₂) :
          (a : (↑X : Type u)) → (↑T : Type u))
        x₂ :
      (↑T : Type u))
a₄ :
  Eq (α := (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g₁ :
          (a : (↑Y : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₁ :
              (a : (↑W : Type u)) → (↑Y : Type u))
            x₁ :
          (↑Y : Type u)) :
      (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (i₂ ≫ g₂) :
          (a : (↑X : Type u)) → (↑T : Type u))
        x₂ :
      (↑T : Type u))
a₅ :
  Eq (α := (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g₁ :
          (a : (↑Y : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₁ :
              (a : (↑W : Type u)) → (↑Y : Type u))
            x₁ :
          (↑Y : Type u)) :
      (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g₂ :
          (a : (↑Z : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₂ :
              (a : (↑X : Type u)) → (↑Z : Type u))
            x₂ :
          (↑Z : Type u)) :
      (↑T : Type u))
a₆ :
  Eq (α := (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g₁ :
          (a : (↑Y : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback g₁ g₂) (pullback.fst g₁ g₂) :
              (a : (↑(pullback g₁ g₂) : Type u)) → (↑Y : Type u))
            x :
          (↑Y : Type u)) :
      (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g₂ :
          (a : (↑Z : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₂ :
              (a : (↑X : Type u)) → (↑Z : Type u))
            x₂ :
          (↑Z : Type u)) :
      (↑T : Type u))
a₇ :
  Eq (α := (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g₁ :
          (a : (↑Y : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback g₁ g₂) (pullback.fst g₁ g₂) :
              (a : (↑(pullback g₁ g₂) : Type u)) → (↑Y : Type u))
            x :
          (↑Y : Type u)) :
      (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g₂ :
          (a : (↑Z : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback g₁ g₂) (pullback.snd g₁ g₂) :
              (a : (↑(pullback g₁ g₂) : Type u)) → (↑Z : Type u))
            x :
          (↑Z : Type u)) :
      (↑T : Type u))
a₈ :
  Eq (α := (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback g₁ g₂) (pullback.fst g₁ g₂ ≫ g₁) :
          (a : (↑(pullback g₁ g₂) : Type u)) → (↑T : Type u))
        x :
      (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g₂ :
          (a : (↑Z : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                pullback g₁ g₂) (pullback.snd g₁ g₂) :
              (a : (↑(pullback g₁ g₂) : Type u)) → (↑Z : Type u))
            x :
          (↑Z : Type u)) :
      (↑T : Type u))
⊢ Eq (α := (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₃ :
          (a : (↑S : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₁ :
              (a : (↑W : Type u)) → (↑S : Type u))
            x₁ :
          (↑S : Type u)) :
      (↑T : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) i₃ :
          (a : (↑S : Type u)) → (↑T : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f₂ :
              (a : (↑X : Type u)) → (↑S : Type u))
            x₂ :
          (↑S : Type u)) :
      (↑T : Type u))
have a₉ : Eq (α := (↑T : Type u))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          pullback g₁ g₂) (pullback.snd g₁ g₂ ≫ g₂) :
        (a : (↑(pullback g₁ g₂) : Type u)) → (↑T : Type u))
      x :
    (↑T : Type u))
  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g₂ :
        (a : (↑Z : Type u)) → (↑T : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback g₁ g₂) (pullback.snd g₁ g₂) :
            (a : (↑(pullback g₁ g₂) : Type u)) → (↑Z : Type u))
          x :
        (↑Z : Type u)) :
    (↑T : Type u))
Tactic: rw [← ConcreteCategory.comp_apply, eq₁, ← ConcreteCategory.comp_apply, eq₂,
      ConcreteCategory.comp_apply, ConcreteCategory.comp_apply, hx₁, hx₂,
      ← ConcreteCategory.comp_apply, pullback.condition, ConcreteCategory.comp_apply]