awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (hypothesis)
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 (α := S.pt ⟶ Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ (X.prodBinaryFan Y).π.app { as := WalkingPair.left }) (S.π.app { as := WalkingPair.left })
⊢ Eq.{u + 1} (α := (↑X : 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).1
    ((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).1
have h₁ : Eq (α := (↑(Functor.obj (pair X Y) { as := WalkingPair.left : 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.left : Discrete WalkingPair })
          (m ≫ (X.prodBinaryFan Y).π.app { as := WalkingPair.left }) :
        (a : (↑S.pt : Type u)) → (↑((pair X Y).obj { as := WalkingPair.left }) : Type u))
      x :
    (↑(Functor.obj (pair X Y) { 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 := S.pt)
          (Y := Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
          (S.π.app { as := WalkingPair.left }) :
        (a : (↑S.pt : Type u)) → (↑((pair X Y).obj { as := WalkingPair.left }) : Type u))
      x :
    (↑(Functor.obj (pair X Y) { as := WalkingPair.left : Discrete WalkingPair }) : Type u))
Tactic: apply_fun fun e => e x at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (hypothesis)
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
m : S.pt ⟶ (X.prodBinaryFan Y).pt
h : ∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j
x : (↑S.pt : 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
have h₁ : Eq (α := S.pt ⟶ Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
  (m ≫ (X.prodBinaryFan Y).π.app { as := WalkingPair.right }) (S.π.app { as := WalkingPair.right })
Tactic: specialize h ⟨WalkingPair.right⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (hypothesis)
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 (α := S.pt ⟶ Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (m ≫ (X.prodBinaryFan Y).π.app { as := WalkingPair.right }) (S.π.app { as := WalkingPair.right })
⊢ 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
have 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))
Tactic: apply_fun fun e => e x at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
X Y : TopCat
⊢ (X.prodIsoProd Y).hom ≫ prodFst = prod.fst
have simp : Eq.{u + 1} (α := of ((↑X : Type u) × (↑Y : Type u)) ⟶ X) prodFst ((X.prodBinaryFan Y).π.app { as := WalkingPair.left })
Tactic: simp [← Iso.eq_inv_comp, prodIsoProd]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
X Y : TopCat
⊢ (X.prodIsoProd Y).hom ≫ prodSnd = prod.snd
have simp : Eq.{u + 1} (α := of ((↑X : Type u) × (↑Y : Type u)) ⟶ Y) prodSnd ((X.prodBinaryFan Y).π.app { as := WalkingPair.right })
Tactic: simp [← Iso.eq_inv_comp, prodIsoProd]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
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)
have 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)
Tactic: refine homeo.isInducing.eq_induced.trans ?_
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
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 (⇑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)
have 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)
Tactic: simp [induced_compose]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
⊢ 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))))
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
W X Y Z : TopCat
f : W ⟶ Y
g : X ⟶ Z
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
have h : 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
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))
⊢ 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
have 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
Tactic: use (prodIsoProd W X).inv (x₁, x₂)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
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))
⊢ (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
have 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))
Tactic: apply Concrete.limit_ext
-- 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))
⊢ IsInducing (X := (↑(W ⨯ Y) : Type u)) (Y := (↑(X ⨯ Z) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          W ⨯ Y) (Y := X ⨯ Z) (prod.map f g)) :
      (a : (↑(W ⨯ Y) : Type u)) → (↑(X ⨯ Z) : Type u))
have eq_induced : Eq (α := TopologicalSpace (↑(W ⨯ Y) : Type u)) (W ⨯ Y).str
  (induced (Y := (↑(X ⨯ Z) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          W ⨯ Y) (Y := X ⨯ Z) (prod.map f g)) :
      (a : (↑(W ⨯ Y) : Type u)) → (↑(X ⨯ Z) : Type u))
    (X ⨯ Z).str)
Tactic: constructor