awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
x : (↑S.pt : Type u)
h :
  Eq (α := (↑(Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y :=
            Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
            (m ≫ (X.prodBinaryFan Y).π.app { as := WalkingPair.right }) :
          (a : (↑S.pt : Type u)) → (↑((pair X Y).obj { as := WalkingPair.right }) : Type u))
        x :
      (↑(Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X := S.pt)
            (Y := Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
            (S.π.app { as := WalkingPair.right }) :
          (a : (↑S.pt : Type u)) → (↑((pair X Y).obj { as := WalkingPair.right }) : Type u))
        x :
      (↑(Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) : Type u))
⊢ Eq.{u + 1} (α := (↑Y : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) m :
          (a : (↑S.pt : Type u)) → (↑(X.prodBinaryFan Y).pt : Type u))
        x).2
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (ofHom
              {
                toFun := fun (s : (↑S.1 : Type u)) ↦
                  ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) (BinaryFan.fst S) :
                        (a :
                            (↑(((Functor.const (Discrete WalkingPair)).obj S.pt).obj { as := WalkingPair.left }) :
                              Type u)) →
                          (↑((pair X Y).obj { as := WalkingPair.left }) : Type u))
                      s,
                    (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) (BinaryFan.snd S) :
                        (a :
                            (↑(((Functor.const (Discrete WalkingPair)).obj S.pt).obj { as := WalkingPair.right }) :
                              Type u)) →
                          (↑((pair X Y).obj { as := WalkingPair.right }) : Type u))
                      s),
                continuous_toFun := ⋯ : C((↑S.1 : Type u), (↑X : Type u) × (↑Y : Type u)) }) :
          (a : (↑S.pt : Type u)) → (↑(X.prodBinaryFan Y).pt : Type u))
        x).2

Tactic:
exact h
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
simp :
  Eq.{u + 1} (α := of ((↑X : Type u) × (↑Y : Type u)) ⟶ X) prodFst
    ((X.prodBinaryFan Y).π.app { as := WalkingPair.left })
⊢ (X.prodIsoProd Y).hom ≫ prodFst = prod.fst

Tactic:
simp [← Iso.eq_inv_comp, prodIsoProd]

Premises used: TopCat.prodIsoProd, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
⊢ Eq.{u + 1} (α := of ((↑X : Type u) × (↑Y : Type u)) ⟶ X) prodFst
    ((X.prodBinaryFan Y).π.app { as := WalkingPair.left })

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
simp :
  Eq.{u + 1} (α := of ((↑X : Type u) × (↑Y : Type u)) ⟶ Y) prodSnd
    ((X.prodBinaryFan Y).π.app { as := WalkingPair.right })
⊢ (X.prodIsoProd Y).hom ≫ prodSnd = prod.snd

Tactic:
simp [← Iso.eq_inv_comp, prodIsoProd]

Premises used: TopCat.prodIsoProd, CategoryTheory.Iso.eq_inv_comp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
⊢ Eq.{u + 1} (α := of ((↑X : Type u) × (↑Y : Type u)) ⟶ Y) prodSnd
    ((X.prodBinaryFan Y).π.app { as := WalkingPair.right })

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
x : (↑(X ⨯ Y) : Type u)
⊢ Eq (α := (↑(of ((↑X : Type u) × (↑Y : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (X.prodIsoProd Y).hom :
          (a : (↑(X ⨯ Y) : Type u)) → (↑(of ((↑X : Type u) × (↑Y : Type u))) : Type u))
        x :
      (↑(of ((↑X : Type u) × (↑Y : Type u))) : Type u))
    (((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.fst :
            (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u))
          x,
        (@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.snd :
            (a : (↑(X ⨯ Y) : Type u)) → (↑Y : Type u))
          x) :
      (↑X : Type u) × (↑Y : Type u))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
⊢ (X.prodIsoProd Y).inv ≫ prod.fst = prodFst

Tactic:
simp [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
⊢ (X.prodIsoProd Y).inv ≫ prod.snd = prodSnd

Tactic:
simp [Iso.inv_comp_eq]

Premises used: CategoryTheory.Iso.inv_comp_eq
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
homeo : (↑(X ⨯ Y) : Type u) ≃ₜ (↑(of ((↑X : Type u) × (↑Y : Type u))) : Type u) := homeoOfIso (X.prodIsoProd Y)
⊢ Eq (α := TopologicalSpace (↑(X ⨯ Y) : Type u)) (X ⨯ Y).str
    (induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.fst) :
          (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u))
        X.str ⊓
      induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.snd) :
          (a : (↑(X ⨯ Y) : Type u)) → (↑Y : Type u))
        Y.str)

Tactic:
homeo.isInducing.eq_induced.trans ?_

Premises used: Homeomorph.isInducing, Topology.IsInducing.eq_induced, Eq.trans
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
homeo : (↑(X ⨯ Y) : Type u) ≃ₜ (↑(of ((↑X : Type u) × (↑Y : Type u))) : Type u) := homeoOfIso (X.prodIsoProd Y)
refine :
  Eq (α := TopologicalSpace (↑(X ⨯ Y) : Type u))
    (induced (Y := (↑(of ((↑X : Type u) × (↑Y : Type u))) : Type u))
      (⇑homeo : (a : (↑(X ⨯ Y) : Type u)) → (↑(of ((↑X : Type u) × (↑Y : Type u))) : Type u))
      (of ((↑X : Type u) × (↑Y : Type u))).str)
    (induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.fst) :
          (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u))
        X.str ⊓
      induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.snd) :
          (a : (↑(X ⨯ Y) : Type u)) → (↑Y : Type u))
        Y.str)
⊢ Eq (α := TopologicalSpace (↑(X ⨯ Y) : Type u)) (X ⨯ Y).str
    (induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.fst) :
          (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u))
        X.str ⊓
      induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.snd) :
          (a : (↑(X ⨯ Y) : Type u)) → (↑Y : Type u))
        Y.str)

Tactic:
refine homeo.isInducing.eq_induced.trans ?_

Premises used: Homeomorph.isInducing, Topology.IsInducing.eq_induced, Eq.trans
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
homeo : (↑(X ⨯ Y) : Type u) ≃ₜ (↑(of ((↑X : Type u) × (↑Y : Type u))) : Type u) := homeoOfIso (X.prodIsoProd Y)
simp :
  Eq (α := TopologicalSpace (↑(X ⨯ Y) : Type u))
    (induced
        (Function.comp (β := (↑X : Type u) × (↑Y : Type u)) Prod.fst
          (⇑homeo : (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u) × (↑Y : Type u)))
        X.str ⊓
      induced
        (Function.comp (β := (↑X : Type u) × (↑Y : Type u)) Prod.snd
          (⇑homeo : (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u) × (↑Y : Type u)))
        Y.str)
    (induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.fst) :
          (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u))
        X.str ⊓
      induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.snd) :
          (a : (↑(X ⨯ Y) : Type u)) → (↑Y : Type u))
        Y.str)
⊢ Eq (α := TopologicalSpace (↑(X ⨯ Y) : Type u))
    (induced (⇑homeo : (a : (↑(X ⨯ Y) : Type u)) → (↑(of ((↑X : Type u) × (↑Y : Type u))) : Type u))
      (induced Prod.fst X.str ⊓ induced Prod.snd Y.str))
    (induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.fst) :
          (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u))
        X.str ⊓
      induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.snd) :
          (a : (↑(X ⨯ Y) : Type u)) → (↑Y : Type u))
        Y.str)

Tactic:
simp [induced_compose]

Premises used: induced_compose
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
X Y : TopCat
homeo : (↑(X ⨯ Y) : Type u) ≃ₜ (↑(of ((↑X : Type u) × (↑Y : Type u))) : Type u) := homeoOfIso (X.prodIsoProd Y)
⊢ Eq (α := TopologicalSpace (↑(X ⨯ Y) : Type u))
    (induced
        (Function.comp (β := (↑X : Type u) × (↑Y : Type u)) Prod.fst
          (⇑homeo : (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u) × (↑Y : Type u)))
        X.str ⊓
      induced
        (Function.comp (β := (↑X : Type u) × (↑Y : Type u)) Prod.snd
          (⇑homeo : (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u) × (↑Y : Type u)))
        Y.str)
    (induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.fst) :
          (a : (↑(X ⨯ Y) : Type u)) → (↑X : Type u))
        X.str ⊓
      induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (X ⨯ Y) _ prod.snd) :
          (a : (↑(X ⨯ Y) : Type u)) → (↑Y : Type u))
        Y.str)

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
h :
  ∀ (x : (↑(Y ⨯ Z) : Type u)),
    Membership.mem (γ := Set (↑(Y ⨯ Z) : Type u))
        (range (ι := (↑(W ⨯ X) : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                W ⨯ X) (Y := Y ⨯ Z) (prod.map f g)) :
            (a : (↑(W ⨯ X) : Type u)) → (↑(Y ⨯ Z) : Type u)))
        x ↔
      Membership.mem (γ := Set (↑(Y ⨯ Z) : Type u))
        (preimage (β := (↑Y : Type u))
            (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _
                  _ (Y ⨯ Z) _ prod.fst) :
              (a : (↑(Y ⨯ Z) : Type u)) → (↑Y : Type u))
            (range (ι := (↑W : Type u))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    f) :
                (a : (↑W : Type u)) → (↑Y : Type u))) ∩
          preimage (β := (↑Z : Type u))
            (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _
                  _ (Y ⨯ Z) _ prod.snd) :
              (a : (↑(Y ⨯ Z) : Type u)) → (↑Z : Type u))
            (range (ι := (↑X : Type u))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    g) :
                (a : (↑X : Type u)) → (↑Z : Type u))))
        x
⊢ Eq (α := Set (↑(Y ⨯ Z) : Type u))
    (range (ι := (↑(W ⨯ X) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            W ⨯ X) (Y := Y ⨯ Z) (prod.map f g)) :
        (a : (↑(W ⨯ X) : Type u)) → (↑(Y ⨯ Z) : Type u)))
    (preimage (β := (↑Y : Type u))
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (Y ⨯ Z) _ prod.fst) :
          (a : (↑(Y ⨯ Z) : Type u)) → (↑Y : Type u))
        (range (ι := (↑W : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
            (a : (↑W : Type u)) → (↑Y : Type u))) ∩
      preimage (β := (↑Z : Type u))
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (Y ⨯ Z) _ prod.snd) :
          (a : (↑(Y ⨯ Z) : Type u)) → (↑Z : Type u))
        (range (ι := (↑X : Type u))
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
            (a : (↑X : Type u)) → (↑Z : Type u))))

Tactic:
ext x
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (↑(Y ⨯ Z) : 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) f :
          (a : (↑W : Type u)) → (↑Y : Type u))
        x₁ :
      (↑Y : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (Y ⨯ Z) _ prod.fst :
          (a : (↑(Y ⨯ Z) : 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) g :
          (a : (↑X : Type u)) → (↑Z : Type u))
        x₂ :
      (↑Z : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (Y ⨯ Z) _ prod.snd :
          (a : (↑(Y ⨯ Z) : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
h :
  (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X := W ⨯ X)
          (Y := Y ⨯ Z) (prod.map f g) :
        (a : (↑(W ⨯ X) : Type u)) → (↑(Y ⨯ Z) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (W.prodIsoProd X).inv :
            (a : (↑(of ((↑W : Type u) × (↑X : Type u))) : Type u)) → (↑(W ⨯ X) : Type u))
          (x₁, x₂) :
        (↑(W ⨯ X) : Type u)) =
    x
⊢ Membership.mem (γ := Set (↑(Y ⨯ Z) : Type u))
    (range (ι := (↑(W ⨯ X) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            W ⨯ X) (Y := Y ⨯ Z) (prod.map f g)) :
        (a : (↑(W ⨯ X) : Type u)) → (↑(Y ⨯ Z) : Type u)))
    x

Tactic:
use (prodIsoProd W X).inv (x₁, x₂)

Premises used: CategoryTheory.ConcreteCategory.hom, TopCat.prodIsoProd, Prod.mk, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (↑(Y ⨯ Z) : 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) f :
          (a : (↑W : Type u)) → (↑Y : Type u))
        x₁ :
      (↑Y : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (Y ⨯ Z) _ prod.fst :
          (a : (↑(Y ⨯ Z) : 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) g :
          (a : (↑X : Type u)) → (↑Z : Type u))
        x₂ :
      (↑Z : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (Y ⨯ Z) _ prod.snd :
          (a : (↑(Y ⨯ Z) : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
h :
  ∀ (j : Discrete WalkingPair),
    Eq (α := (↑(Functor.obj (pair Y Z) j) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              limit (pair Y Z)) (limit.π (pair Y Z) j) :
            (a : (↑(limit (pair Y Z)) : Type u)) → (↑((pair Y Z).obj j) : Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
                  W ⨯ X) (Y := Y ⨯ Z) (prod.map f g) :
                (a : (↑(W ⨯ X) : Type u)) → (↑(Y ⨯ Z) : Type u))
              ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (W.prodIsoProd X).inv :
                    (a : (↑(of ((↑W : Type u) × (↑X : Type u))) : Type u)) → (↑(W ⨯ X) : Type u))
                  (x₁, x₂) :
                (↑(W ⨯ X) : Type u)) :
            (↑(Y ⨯ Z) : Type u)) :
        (↑(Functor.obj (pair Y Z) j) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              limit (pair Y Z)) (limit.π (pair Y Z) j) :
            (a : (↑(limit (pair Y Z)) : Type u)) → (↑((pair Y Z).obj j) : Type u))
          x :
        (↑(Functor.obj (pair Y Z) j) : Type u))
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X := W ⨯ X)
          (Y := Y ⨯ Z) (prod.map f g) :
        (a : (↑(W ⨯ X) : Type u)) → (↑(Y ⨯ Z) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              (W.prodIsoProd X).inv :
            (a : (↑(of ((↑W : Type u) × (↑X : Type u))) : Type u)) → (↑(W ⨯ X) : Type u))
          (x₁, x₂) :
        (↑(W ⨯ X) : Type u)) =
    x

Tactic:
apply Concrete.limit_ext

Premises used: CategoryTheory.Limits.Concrete.limit_ext
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (↑(Y ⨯ Z) : 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) f :
          (a : (↑W : Type u)) → (↑Y : Type u))
        x₁ :
      (↑Y : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (Y ⨯ Z) _ prod.fst :
          (a : (↑(Y ⨯ Z) : 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) g :
          (a : (↑X : Type u)) → (↑Z : Type u))
        x₂ :
      (↑Z : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (Y ⨯ Z) _ prod.snd :
          (a : (↑(Y ⨯ Z) : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
⊢ Eq (α := (↑(Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑W : Type u)) → (↑((pair Y Z).obj { as := WalkingPair.left }) : Type u))
        (x₁, x₂).1 :
      (↑(Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            limit (pair Y Z)) (Y := Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair })
            (limit.π (pair Y Z) { as := WalkingPair.left }) :
          (a : (↑(limit (pair Y Z)) : Type u)) → (↑((pair Y Z).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))

Tactic:
hx₁
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
x : (↑(Y ⨯ Z) : 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) f :
          (a : (↑W : Type u)) → (↑Y : Type u))
        x₁ :
      (↑Y : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (Y ⨯ Z) _ prod.fst :
          (a : (↑(Y ⨯ Z) : 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) g :
          (a : (↑X : Type u)) → (↑Z : Type u))
        x₂ :
      (↑Z : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (Y ⨯ Z) _ prod.snd :
          (a : (↑(Y ⨯ Z) : Type u)) → (↑Z : Type u))
        x :
      (↑Z : Type u))
⊢ Eq (α := (↑(Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f :
          (a : (↑W : Type u)) → (↑((pair Y Z).obj { as := WalkingPair.left }) : Type u))
        (x₁, x₂).1 :
      (↑(Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            limit (pair Y Z)) (Y := Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair })
            (limit.π (pair Y Z) { as := WalkingPair.left }) :
          (a : (↑(limit (pair Y Z)) : Type u)) → (↑((pair Y Z).obj { as := WalkingPair.left }) : Type u))
        x :
      (↑(Functor.obj (pair Y Z) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))

Tactic:
exact hx₁