awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
⊢ IsPullback (X'.binaryCofan Y').inl αX f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))

Tactic:
⟨⟨hαX.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩

Premises used: CategoryTheory.Limits.PullbackCone.isLimitAux', CategoryTheory.IsPullback.mk, CategoryTheory.CommSq.mk, Nonempty.intro, Eq.symm
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
h₁ :
  (s :
      PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
        (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))) →
    { l : s.pt ⟶ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).pt //
      l ≫ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).fst = s.fst ∧
        l ≫ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).snd = s.snd ∧
          ∀ {m : s.pt ⟶ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).pt},
            m ≫ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).fst = s.fst →
              m ≫ (PullbackCone.mk (X'.binaryCofan Y').inl αX ⋯).snd = s.snd → m = l }
⊢ IsPullback (X'.binaryCofan Y').inl αX f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))

Tactic:
refine ⟨⟨hαX.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
x : (↑s.pt : Type u)
val : (↑X' : Type u)
h :
  Eq (α :=
    (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
          { as := WalkingPair.left : Discrete WalkingPair }) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            s.fst :
          (a : (↑s.pt : Type u)) →
            (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj { as := WalkingPair.left }) :
              Type u))
        x :
      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
            { as := WalkingPair.left : Discrete WalkingPair }) :
        Type u))
    (Sum.inl val : (↑X' : Type u) ⊕ (↑Y' : Type u))
⊢ ∃! y : (↑X' : Type u),
    Eq (α :=
      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
            { as := WalkingPair.left : Discrete WalkingPair }) :
        Type u))
      (Sum.inl val) (Sum.inl y)

Tactic:
⟨val, rfl, fun y h => Sum.inl_injective h.symm⟩

Premises used: Sum.inl_injective, ExistsUnique, And.intro, Exists.intro, Eq.symm, rfl
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
x : (↑s.pt : Type u)
val : (↑X' : Type u)
h :
  Eq (α :=
    (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
          { as := WalkingPair.left : Discrete WalkingPair }) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            s.fst :
          (a : (↑s.pt : Type u)) →
            (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj { as := WalkingPair.left }) :
              Type u))
        x :
      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
            { as := WalkingPair.left : Discrete WalkingPair }) :
        Type u))
    (Sum.inl val : (↑X' : Type u) ⊕ (↑Y' : Type u))
⊢ ∃! y : (↑X' : Type u),
    Eq (α :=
      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
            { as := WalkingPair.left : Discrete WalkingPair }) :
        Type u))
      (Sum.inl val) (Sum.inl y)

Tactic:
exact ⟨val, rfl, fun y h => Sum.inl_injective h.symm⟩
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
x : (↑s.pt : Type u)
val : (↑Y' : Type u)
h :
  Eq (α :=
    (↑(Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
          ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f :
          (a : (↑(X'.binaryCofan Y').pt : Type u)) →
            (↑((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                s.fst :
              (a : (↑s.pt : Type u)) →
                (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj { as := WalkingPair.left }) :
                  Type u))
            x :
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                { as := WalkingPair.left : Discrete WalkingPair }) :
            Type u)) :
      (↑(Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
            ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))) :
        Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier) f :
          (a : (↑(X'.binaryCofan Y').pt : Type u)) →
            (↑((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})).pt : Type u))
        (Sum.inr val) :
      (↑(Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
            ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))) :
        Type u))
⊢ ∃! y : (↑X' : Type u), Sum.inr val = Sum.inl y

Tactic:
cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαY val :).symm

Premises used: CategoryTheory.Limits.PullbackCone.condition, CategoryTheory.ConcreteCategory.congr_hom, Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
⊢ ∀ (x : (↑s.pt : Type u)),
    ∃! y : (↑X' : Type u),
      Eq (α :=
        (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
              { as := WalkingPair.left : Discrete WalkingPair }) :
          Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                s.fst :
              (a : (↑s.pt : Type u)) →
                (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj { as := WalkingPair.left }) :
                  Type u))
            x :
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                { as := WalkingPair.left : Discrete WalkingPair }) :
            Type u))
        (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u))

Tactic:
have : ∀ x, ∃! y, s.fst x = Sum.inl y := by
        intro x
        rcases h : s.fst x with val | val
        · exact ⟨val, rfl, fun y h => Sum.inl_injective h.symm⟩
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαY val :).symm
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
l : (x : (↑s.pt : Type u)) → (↑X' : Type u)
hl :
  ∀ (x : (↑s.pt : Type u)),
    (fun (y : (↑X' : Type u)) ↦
        Eq (α :=
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                { as := WalkingPair.left : Discrete WalkingPair }) :
            Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  s.fst :
                (a : (↑s.pt : Type u)) →
                  (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                        { as := WalkingPair.left }) :
                    Type u))
              x :
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u))
          (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
      (l x)
hl' :
  ∀ (x : (↑s.pt : Type u)) (y : (↑X' : Type u)),
    (fun (y : (↑X' : Type u)) ↦
          Eq (α :=
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) s.fst :
                  (a : (↑s.pt : Type u)) →
                    (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                          { as := WalkingPair.left }) :
                      Type u))
                x :
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))
            (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
        y →
      y = l x
h₁ : Continuous (Y := (↑X' : Type u) ⊕ (↑Y' : Type u)) (Sum.inl ∘ l)
⊢ Continuous l

Tactic:
apply (IsEmbedding.inl (X := X') (Y := Y')).isInducing.continuous_iff.mpr

Premises used: Iff.mpr, Topology.IsEmbedding.inl, Topology.IsInducing.continuous_iff, Topology.IsEmbedding.isInducing
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
l : (x : (↑s.pt : Type u)) → (↑X' : Type u)
hl :
  ∀ (x : (↑s.pt : Type u)),
    (fun (y : (↑X' : Type u)) ↦
        Eq (α :=
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                { as := WalkingPair.left : Discrete WalkingPair }) :
            Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  s.fst :
                (a : (↑s.pt : Type u)) →
                  (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                        { as := WalkingPair.left }) :
                    Type u))
              x :
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u))
          (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
      (l x)
hl' :
  ∀ (x : (↑s.pt : Type u)) (y : (↑X' : Type u)),
    (fun (y : (↑X' : Type u)) ↦
          Eq (α :=
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) s.fst :
                  (a : (↑s.pt : Type u)) →
                    (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                          { as := WalkingPair.left }) :
                      Type u))
                x :
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))
            (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
        y →
      y = l x
⊢ Continuous (TopCat.Hom.hom s.fst).toFun

Tactic:
s.fst.hom.2

Premises used: CategoryTheory.Limits.PullbackCone.fst, ContinuousMap.continuous_toFun, TopCat.Hom.hom
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
l : (x : (↑s.pt : Type u)) → (↑X' : Type u)
hl :
  ∀ (x : (↑s.pt : Type u)),
    (fun (y : (↑X' : Type u)) ↦
        Eq (α :=
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                { as := WalkingPair.left : Discrete WalkingPair }) :
            Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  s.fst :
                (a : (↑s.pt : Type u)) →
                  (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                        { as := WalkingPair.left }) :
                    Type u))
              x :
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u))
          (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
      (l x)
hl' :
  ∀ (x : (↑s.pt : Type u)) (y : (↑X' : Type u)),
    (fun (y : (↑X' : Type u)) ↦
          Eq (α :=
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) s.fst :
                  (a : (↑s.pt : Type u)) →
                    (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                          { as := WalkingPair.left }) :
                      Type u))
                x :
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))
            (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
        y →
      y = l x
e_2 :
  ((↑X' : Type u) ⊕ (↑Y' : Type u)) =
    (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
          { as := WalkingPair.left : Discrete WalkingPair }) :
      Type u)
⊢ Sum.inl ∘ l = (TopCat.Hom.hom s.fst).toFun

Tactic:
(funext hl).symm

Premises used: funext, Eq.symm
-- Module: Mathlib.CategoryTheory.Extensive
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
l : (x : (↑s.pt : Type u)) → (↑X' : Type u)
hl :
  ∀ (x : (↑s.pt : Type u)),
    (fun (y : (↑X' : Type u)) ↦
        Eq (α :=
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                { as := WalkingPair.left : Discrete WalkingPair }) :
            Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  s.fst :
                (a : (↑s.pt : Type u)) →
                  (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                        { as := WalkingPair.left }) :
                    Type u))
              x :
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u))
          (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
      (l x)
hl' :
  ∀ (x : (↑s.pt : Type u)) (y : (↑X' : Type u)),
    (fun (y : (↑X' : Type u)) ↦
          Eq (α :=
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) s.fst :
                  (a : (↑s.pt : Type u)) →
                    (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                          { as := WalkingPair.left }) :
                      Type u))
                x :
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))
            (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
        y →
      y = l x
e_2 :
  ((↑X' : Type u) ⊕ (↑Y' : Type u)) =
    (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
          { as := WalkingPair.left : Discrete WalkingPair }) :
      Type u)
⊢ Sum.inl ∘ l = (TopCat.Hom.hom s.fst).toFun

Tactic:
exact (funext hl).symm

Premises used: funext, Eq.symm