-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf :
  IsInducing (X := (↑W : Type u)) (Y := (↑X : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑W : Type u)) → (↑X : Type u))
hg :
  IsInducing (X := (↑Y : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑Z : Type u))
eq_induced :
  Eq (α := TopologicalSpace (↑(W ⨯ Y) : Type u))
    (induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (W ⨯ Y) _ prod.fst) :
          (a : (↑(W ⨯ Y) : Type u)) → (↑W : Type u))
        W.str ⊓
      induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (W ⨯ Y) _ prod.snd) :
          (a : (↑(W ⨯ Y) : Type u)) → (↑Y : Type u))
        Y.str)
    (induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (W ⨯ Y) _ prod.fst) :
          (a : (↑(W ⨯ Y) : Type u)) → (↑W : Type u))
        W.str ⊓
      induced (Y := (↑Y : Type u))
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (W ⨯ Y) _ prod.snd) :
          (a : (↑(W ⨯ Y) : Type u)) → (↑Y : Type u))
        (induced
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
            (a : (↑Y : Type u)) → (↑Z : Type u))
          Z.str))
⊢ Eq (α := TopologicalSpace (↑(W ⨯ Y) : Type u))
    (induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (W ⨯ Y) _ prod.fst) :
          (a : (↑(W ⨯ Y) : Type u)) → (↑W : Type u))
        W.str ⊓
      induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (W ⨯ Y) _ prod.snd) :
          (a : (↑(W ⨯ Y) : Type u)) → (↑Y : Type u))
        Y.str)
    (induced (Y := (↑W : Type u))
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (W ⨯ Y) _ prod.fst) :
          (a : (↑(W ⨯ Y) : Type u)) → (↑W : Type u))
        (induced
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
            (a : (↑W : Type u)) → (↑X : Type u))
          X.str) ⊓
      induced (Y := (↑Y : Type u))
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (W ⨯ Y) _ prod.snd) :
          (a : (↑(W ⨯ Y) : Type u)) → (↑Y : Type u))
        (induced
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
            (a : (↑Y : Type u)) → (↑Z : Type u))
          Z.str))
have eq_induced₁ : Eq (α := TopologicalSpace (↑(W ⨯ Y) : Type u))
  (induced
      (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (W ⨯ Y) _ prod.fst) :
        (a : (↑(W ⨯ Y) : Type u)) → (↑W : Type u))
      W.str ⊓
    induced
      (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (W ⨯ Y) _ prod.snd) :
        (a : (↑(W ⨯ Y) : Type u)) → (↑Y : Type u))
      Y.str)
  (induced
      (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (W ⨯ Y) _ prod.fst) :
        (a : (↑(W ⨯ Y) : Type u)) → (↑W : Type u))
      W.str ⊓
    induced
      (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (W ⨯ Y) _ prod.snd) :
        (a : (↑(W ⨯ Y) : Type u)) → (↑Y : Type u))
      Y.str)
Tactic: rw [← hf.eq_induced, ← hg.eq_induced]