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)
right :
  Eq (α := S.pt ⟶ Y)
    (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 : (↑S.pt : Type u)) → (↑X : Type u))
                  s,
                (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (BinaryFan.snd S) :
                    (a : (↑S.pt : Type u)) → (↑Y : Type u))
                  s),
            continuous_toFun := ⋯ : C((↑S.1 : Type u), (↑X : Type u) × (↑Y : Type u)) } ≫
        (X.prodBinaryFan Y).π.app { as := WalkingPair.right } :
      S.pt ⟶ Y)
    (S.π.app { as := WalkingPair.right } :
      Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) S.pt)
          { as := WalkingPair.right : Discrete WalkingPair } ⟶
        Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
⊢ Eq (α := S.pt ⟶ Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (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)) } ≫
      (X.prodBinaryFan Y).π.app { as := WalkingPair.right })
    (S.π.app { as := WalkingPair.right })

Tactic:
dsimp
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
right :
  ∀ (x : (↑S.pt : Type u)),
    Eq (α := (↑Y : Type u))
      (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y := Y)
                (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 : (↑S.pt : Type u)) → (↑X : Type u))
                              s,
                            (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                  (CC := carrier) (BinaryFan.snd S) :
                                (a : (↑S.pt : Type u)) → (↑Y : Type u))
                              s),
                        continuous_toFun := ⋯ : C((↑S.1 : Type u), (↑X : Type u) × (↑Y : Type u)) } ≫
                    (X.prodBinaryFan Y).π.app { as := WalkingPair.right } :
                  S.pt ⟶ Y) :
              C((↑S.pt : Type u), (↑Y : Type u))) :
            (a : (↑S.pt : 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 :=
                S.pt) (Y := Y)
                (S.π.app { as := WalkingPair.right } :
                  Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) S.pt)
                      { as := WalkingPair.right : Discrete WalkingPair } ⟶
                    Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) :
              C((↑S.pt : Type u), (↑Y : Type u))) :
            (a : (↑S.pt : Type u)) → (↑Y : Type u))
          x :
        (↑Y : Type u))
⊢ Eq (α := S.pt ⟶ Y)
    (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 : (↑S.pt : Type u)) → (↑X : Type u))
                  s,
                (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                      (BinaryFan.snd S) :
                    (a : (↑S.pt : Type u)) → (↑Y : Type u))
                  s),
            continuous_toFun := ⋯ : C((↑S.1 : Type u), (↑X : Type u) × (↑Y : Type u)) } ≫
        (X.prodBinaryFan Y).π.app { as := WalkingPair.right } :
      S.pt ⟶ Y)
    (S.π.app { as := WalkingPair.right } :
      Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) S.pt)
          { as := WalkingPair.right : Discrete WalkingPair } ⟶
        Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })

Tactic:
ext
-- Module: Mathlib.Topology.Category.TopCat.Limits.Products
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
S : Cone (pair X Y)
x : (↑S.pt : Type u)
⊢ Eq (α := (↑Y : Type u))
    (((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y := Y)
              (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 : (↑S.pt : Type u)) → (↑X : Type u))
                            s,
                          (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                                carrier) (BinaryFan.snd S) :
                              (a : (↑S.pt : Type u)) → (↑Y : Type u))
                            s),
                      continuous_toFun := ⋯ : C((↑S.1 : Type u), (↑X : Type u) × (↑Y : Type u)) } ≫
                  (X.prodBinaryFan Y).π.app { as := WalkingPair.right } :
                S.pt ⟶ Y) :
            C((↑S.pt : Type u), (↑Y : Type u))) :
          (a : (↑S.pt : 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 := S.pt)
              (Y := Y)
              (S.π.app { as := WalkingPair.right } :
                Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) S.pt)
                    { as := WalkingPair.right : Discrete WalkingPair } ⟶
                  Functor.obj (pair X Y) { as := WalkingPair.right : Discrete WalkingPair }) :
            C((↑S.pt : Type u), (↑Y : Type u))) :
          (a : (↑S.pt : Type u)) → (↑Y : Type u))
        x :
      (↑Y : Type u))

Tactic:
rfl
-- 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
h : ∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j
w :
  ∀ (x : (↑S.pt : Type u)),
    Eq (α := (↑(X.prodBinaryFan Y).pt : 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 :
        (↑(X.prodBinaryFan Y).pt : Type u))
      ((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 :
        (↑(X.prodBinaryFan Y).pt : Type u))
⊢ m =
    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 := ⋯ }

Tactic:
ext x
-- 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
h : ∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j
x : (↑S.pt : Type u)
⊢ Eq (α := (↑(X.prodBinaryFan Y).pt : 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 :
      (↑(X.prodBinaryFan Y).pt : Type u))
    ((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 :
      (↑(X.prodBinaryFan Y).pt : Type u))

Tactic:
Prod.ext ?_ ?_

Premises used: Prod.ext
-- 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
h : ∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j
x : (↑S.pt : Type u)
⊢ 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 })

Tactic:
specialize h ⟨WalkingPair.left⟩

Premises used: CategoryTheory.Discrete.mk, CategoryTheory.Limits.WalkingPair.left
-- 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 (α := 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 (α := (↑(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
-- 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.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))
⊢ 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

Tactic:
h
-- 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.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))
⊢ 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

Tactic:
exact h
-- 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
h : ∀ (j : Discrete WalkingPair), m ≫ (X.prodBinaryFan Y).π.app j = S.π.app j
x : (↑S.pt : Type u)
⊢ 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⟩

Premises used: CategoryTheory.Limits.WalkingPair.right, CategoryTheory.Discrete.mk
-- 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 (α := 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 (α := (↑(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
-- 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:
h