-- 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)
h :
  Membership.mem (γ := Set (↑(pullback g₁ g₂) : Type u))
      (Set.range (ι := (↑(pullback f₁ f₂) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback f₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
          (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u)))
      x →
    Membership.mem (γ := Set (↑(pullback g₁ g₂) : Type u))
      (Set.preimage (β := (↑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))
          (Set.range (ι := (↑W : 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))) ∩
        Set.preimage (β := (↑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))
          (Set.range (ι := (↑X : 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
⊢ Membership.mem (γ := Set (↑(pullback g₁ g₂) : Type u))
      (Set.range (ι := (↑(pullback f₁ f₂) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              pullback f₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
          (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u)))
      x ↔
    Membership.mem (γ := Set (↑(pullback g₁ g₂) : Type u))
      (Set.preimage (β := (↑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))
          (Set.range (ι := (↑W : 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))) ∩
        Set.preimage (β := (↑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))
          (Set.range (ι := (↑X : 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
have h₁ : Membership.mem (γ := Set (↑(pullback g₁ g₂) : Type u))
    (Set.preimage (β := (↑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))
        (Set.range (ι := (↑W : 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))) ∩
      Set.preimage (β := (↑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))
        (Set.range (ι := (↑X : 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 →
  Membership.mem (γ := Set (↑(pullback g₁ g₂) : Type u))
    (Set.range (ι := (↑(pullback f₁ f₂) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            pullback f₁ f₂) (Y := pullback g₁ g₂) (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ eq₁ eq₂)) :
        (a : (↑(pullback f₁ f₂) : Type u)) → (↑(pullback g₁ g₂) : Type u)))
    x
Tactic: constructor