awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
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' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
val : Y'
h :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
        { as := WalkingPair.left : Discrete WalkingPair }))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
          (a : (fun (X : Type u) ↦ X) s.pt) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                { as := WalkingPair.left }))
        x :
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
          { as := WalkingPair.left : Discrete WalkingPair }))
    (Sum.inr val : X' ⊕ Y')
⊢ ∃! y : X', Sum.inr val = Sum.inl y
have h₁ : Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
        (a : (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone X' Y').pt) →
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
            (a : (fun (X : Type u) ↦ X) s.pt) →
              (fun (X : Type u) ↦ X)
                (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                  { as := WalkingPair.left }))
          x :
        (fun (X : Type u) ↦ X)
          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
            { as := WalkingPair.left : Discrete WalkingPair })) :
    (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
        (a : (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone X' Y').pt) →
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inr val) :
    (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
Tactic: apply_fun f at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
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' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
⊢ { l : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).pt //
    l ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).pt},
          m ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).snd = s.snd → m = l }
have this : ∀ (x : (fun (X : Type u) ↦ X) s.pt),
  ∃! y : X',
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
          { as := WalkingPair.left : Discrete WalkingPair }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
            (a : (fun (X : Type u) ↦ X) s.pt) →
              (fun (X : Type u) ↦ X)
                (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                  { as := WalkingPair.left }))
          x :
        (fun (X : Type u) ↦ X)
          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
            { as := WalkingPair.left : Discrete WalkingPair }))
      (Sum.inl y : X' ⊕ Y')
Tactic: have : ∀ x, ∃! y, s.fst x = Sum.inl y := by
        intro x
        rcases h : s.fst x with val | val
        · simp
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαY val :).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
l : (x : s.pt) → X'
hl :
  ∀ (x : s.pt),
    (fun (y : X') ↦
        Eq (α :=
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
              { as := WalkingPair.left : Discrete WalkingPair }))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
                (a : (fun (X : Type u) ↦ X) s.pt) →
                  (fun (X : Type u) ↦ X)
                    (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                      { as := WalkingPair.left }))
              x :
            (fun (X : Type u) ↦ X)
              (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                { as := WalkingPair.left : Discrete WalkingPair }))
          (Sum.inl y : X' ⊕ Y'))
      (l x)
hl' :
  ∀ (x : s.pt) (y : X'),
    (fun (y : X') ↦
          Eq (α :=
            (fun (X : Type u) ↦ X)
              (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                { as := WalkingPair.left : Discrete WalkingPair }))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
                  (a : (fun (X : Type u) ↦ X) s.pt) →
                    (fun (X : Type u) ↦ X)
                      (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                        { as := WalkingPair.left }))
                x :
              (fun (X : Type u) ↦ X)
                (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }))
            (Sum.inl y : X' ⊕ Y'))
        y →
      y = l x
⊢ ↾l ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).fst = s.fst
have h₁ : ∀ (x : s.pt),
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾l ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX sorry).fst)).toFun
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) s.fst).toFun x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
s : PullbackCone f (BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
l : (x : s.pt) → X'
hl :
  ∀ (x : s.pt),
    (fun (y : X') ↦
        Eq (α :=
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
              { as := WalkingPair.left : Discrete WalkingPair }))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
                (a : (fun (X : Type u) ↦ X) s.pt) →
                  (fun (X : Type u) ↦ X)
                    (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                      { as := WalkingPair.left }))
              x :
            (fun (X : Type u) ↦ X)
              (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                { as := WalkingPair.left : Discrete WalkingPair }))
          (Sum.inl y : X' ⊕ Y'))
      (l x)
hl' :
  ∀ (x : s.pt) (y : X'),
    (fun (y : X') ↦
          Eq (α :=
            (fun (X : Type u) ↦ X)
              (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                { as := WalkingPair.left : Discrete WalkingPair }))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
                  (a : (fun (X : Type u) ↦ X) s.pt) →
                    (fun (X : Type u) ↦ X)
                      (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                        { as := WalkingPair.left }))
                x :
              (fun (X : Type u) ↦ X)
                (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }))
            (Sum.inl y : X' ⊕ Y'))
        y →
      y = l x
l' : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).pt
h₁ : l' ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).fst = s.fst
h : l' ≫ (PullbackCone.mk (BinaryCofan.inl (Types.binaryCoproductCocone X' Y')) αX ⋯).snd = s.snd
⊢ l' = ↾l
have h₂ : ∀ (x : s.pt),
  (ConcreteCategory.hom (FC := TypeCat.Fun) l').toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) (↾l)).toFun x
Tactic: ext x
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
⊢ IsPullback (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY f
    (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
have h₁ : (s : PullbackCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))) →
  { l : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY sorry).pt //
    l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY sorry).fst = s.fst ∧
      l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY sorry).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY sorry).pt},
          m ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY sorry).fst = s.fst →
            m ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY sorry).snd = s.snd → m = l }
Tactic: refine ⟨⟨hαY.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
s : PullbackCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
⊢ ∃! y : Y',
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
          { as := WalkingPair.right : Discrete WalkingPair }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
            (a : (fun (X : Type u) ↦ X) s.pt) →
              (fun (X : Type u) ↦ X)
                (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                  { as := WalkingPair.right }))
          x :
        (fun (X : Type u) ↦ X)
          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
            { as := WalkingPair.right : Discrete WalkingPair }))
      (Sum.inr y : X' ⊕ Y')
have inl : ∀ (val : X')
  (h :
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
          { as := WalkingPair.right : Discrete WalkingPair }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
            (a : (fun (X : Type u) ↦ X) s.pt) →
              (fun (X : Type u) ↦ X)
                (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                  { as := WalkingPair.right }))
          x :
        (fun (X : Type u) ↦ X)
          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
            { as := WalkingPair.right : Discrete WalkingPair }))
      (Sum.inl val : X' ⊕ Y')),
  ∃! y : Y', Sum.inl val = Sum.inr y
Tactic: rcases h : s.fst x with val | val
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
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' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
s : PullbackCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
x : s.pt
val : X'
h :
  Eq (α :=
    (fun (X : Type u) ↦ X)
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
        { as := WalkingPair.right : Discrete WalkingPair }))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
          (a : (fun (X : Type u) ↦ X) s.pt) →
            (fun (X : Type u) ↦ X)
              (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                { as := WalkingPair.right }))
        x :
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
          { as := WalkingPair.right : Discrete WalkingPair }))
    (Sum.inl val : X' ⊕ Y')
⊢ ∃! y : Y', Sum.inl val = Sum.inr y
have h₁ : Eq (α := (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
        (a : (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone X' Y').pt) →
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
            (a : (fun (X : Type u) ↦ X) s.pt) →
              (fun (X : Type u) ↦ X)
                (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                  { as := WalkingPair.right }))
          x :
        (fun (X : Type u) ↦ X)
          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
            { as := WalkingPair.right : Discrete WalkingPair })) :
    (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) f :
        (a : (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone X' Y').pt) →
          (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
      (Sum.inl val) :
    (fun (X : Type u) ↦ X) (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt)
Tactic: apply_fun f at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
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' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
s : PullbackCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
⊢ { l : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).pt //
    l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).pt},
          m ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).snd = s.snd → m = l }
have this : ∀ (x : (fun (X : Type u) ↦ X) s.pt),
  ∃! y : Y',
    Eq (α :=
      (fun (X : Type u) ↦ X)
        (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
          { as := WalkingPair.right : Discrete WalkingPair }))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
            (a : (fun (X : Type u) ↦ X) s.pt) →
              (fun (X : Type u) ↦ X)
                (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                  { as := WalkingPair.right }))
          x :
        (fun (X : Type u) ↦ X)
          (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
            { as := WalkingPair.right : Discrete WalkingPair }))
      (Sum.inr y : X' ⊕ Y')
Tactic: have : ∀ x, ∃! y, s.fst x = Sum.inr y := by
        intro x
        rcases h : s.fst x with val | val
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm
        · simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
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' : Type u
αX : X' ⟶ PUnit.{u + 1}
αY : Y' ⟶ PUnit.{u + 1}
f : (Types.binaryCoproductCocone X' Y').pt ⟶ (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}).pt
hαX :
  αX ≫ BinaryCofan.inl (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inl (Types.binaryCoproductCocone X' Y') ≫ f
hαY :
  αY ≫ BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}) =
    BinaryCofan.inr (Types.binaryCoproductCocone X' Y') ≫ f
s : PullbackCone f (BinaryCofan.inr (Types.binaryCoproductCocone PUnit.{u + 1} PUnit.{u + 1}))
l : (x : s.pt) → Y'
hl :
  ∀ (x : s.pt),
    (fun (y : Y') ↦
        Eq (α :=
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
              { as := WalkingPair.right : Discrete WalkingPair }))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
                (a : (fun (X : Type u) ↦ X) s.pt) →
                  (fun (X : Type u) ↦ X)
                    (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                      { as := WalkingPair.right }))
              x :
            (fun (X : Type u) ↦ X)
              (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                { as := WalkingPair.right : Discrete WalkingPair }))
          (Sum.inr y : X' ⊕ Y'))
      (l x)
hl' :
  ∀ (x : s.pt) (y : Y'),
    (fun (y : Y') ↦
          Eq (α :=
            (fun (X : Type u) ↦ X)
              (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                { as := WalkingPair.right : Discrete WalkingPair }))
            ((ConcreteCategory.hom (FC := TypeCat.Fun) s.fst :
                  (a : (fun (X : Type u) ↦ X) s.pt) →
                    (fun (X : Type u) ↦ X)
                      (((Functor.const (Discrete WalkingPair)).obj (Types.binaryCoproductCocone X' Y').pt).obj
                        { as := WalkingPair.right }))
                x :
              (fun (X : Type u) ↦ X)
                (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (Types.binaryCoproductCocone X' Y').pt)
                  { as := WalkingPair.right : Discrete WalkingPair }))
            (Sum.inr y : X' ⊕ Y'))
        y →
      y = l x
⊢ ↾l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY ⋯).fst = s.fst
have h₁ : ∀ (x : s.pt),
  (ConcreteCategory.hom (FC := TypeCat.Fun)
          (↾l ≫ (PullbackCone.mk (BinaryCofan.inr (Types.binaryCoproductCocone X' Y')) αY sorry).fst)).toFun
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) s.fst).toFun x
Tactic: ext x