awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Products (goal)
Goal:
X Y : Type u
x : X ⟶ Y
x_1 : Type u
⊢ Eq (α := (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
    (NatTrans.app
      (binaryProductFunctor.map x ≫
        Iso.hom
          ((fun (X : Type u) ↦
              (NatIso.ofComponents
                  (fun (Y : Type u) ↦
                    Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                  ⋯ :
                binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
            Y))
      x_1)
    (NatTrans.app
      (Iso.hom
          ((fun (X : Type u) ↦
              (NatIso.ofComponents
                  (fun (Y : Type u) ↦
                    Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                  ⋯ :
                binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
            X) ≫
        Functor.map prod.functor x)
      x_1)
have refine_2 : Eq (α := (binaryProductFunctor.obj X).obj x_1 ⟶ Y)
  (CategoryStruct.comp (Y := Y ⨯ x_1)
    (NatTrans.app
        (binaryProductFunctor.map x ≫
          Iso.hom
            ((fun (X : Type u) ↦
                (NatIso.ofComponents
                    (fun (Y : Type u) ↦
                      Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                    sorry :
                  binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
              Y))
        x_1 :
      (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
    prod.fst)
  (CategoryStruct.comp (Y := Y ⨯ x_1)
    (NatTrans.app
        (Iso.hom
            ((fun (X : Type u) ↦
                (NatIso.ofComponents
                    (fun (Y : Type u) ↦
                      Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                    sorry :
                  binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
              X) ≫
          Functor.map prod.functor x)
        x_1 :
      (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
    prod.fst)
Tactic: apply Limits.prod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Products (goal)
Goal:
X Y : Type u
x : X ⟶ Y
x_1 : Type u
⊢ Eq (α := (binaryProductFunctor.obj X).obj x_1 ⟶ Y)
    (CategoryStruct.comp (Y := Y ⨯ x_1)
      (NatTrans.app
          (binaryProductFunctor.map x ≫
            Iso.hom
              ((fun (X : Type u) ↦
                  (NatIso.ofComponents
                      (fun (Y : Type u) ↦
                        Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                      ⋯ :
                    binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
                Y))
          x_1 :
        (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
      prod.fst)
    (CategoryStruct.comp (Y := Y ⨯ x_1)
      (NatTrans.app
          (Iso.hom
              ((fun (X : Type u) ↦
                  (NatIso.ofComponents
                      (fun (Y : Type u) ↦
                        Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                      ⋯ :
                    binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
                X) ≫
            Functor.map prod.functor x)
          x_1 :
        (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
      prod.fst)
have refine_2 : BinaryFan.IsLimit.lift (binaryProductLimit Y x_1) (↾_root_.Prod.fst ≫ x) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.fst =
  ↾_root_.Prod.fst ≫ x
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Products (goal)
Goal:
X Y : Type u
x : X ⟶ Y
x_1 : Type u
⊢ Eq (α := (binaryProductFunctor.obj X).obj x_1 ⟶ x_1)
    (CategoryStruct.comp (Y := Y ⨯ x_1)
      (NatTrans.app
          (binaryProductFunctor.map x ≫
            Iso.hom
              ((fun (X : Type u) ↦
                  (NatIso.ofComponents
                      (fun (Y : Type u) ↦
                        Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                      ⋯ :
                    binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
                Y))
          x_1 :
        (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
      prod.snd)
    (CategoryStruct.comp (Y := Y ⨯ x_1)
      (NatTrans.app
          (Iso.hom
              ((fun (X : Type u) ↦
                  (NatIso.ofComponents
                      (fun (Y : Type u) ↦
                        Iso.symm (IsLimit.conePointUniqueUpToIso (limit.isLimit (pair X Y)) (binaryProductLimit X Y)))
                      ⋯ :
                    binaryProductFunctor.obj X ≅ Functor.obj prod.functor X))
                X) ≫
            Functor.map prod.functor x)
          x_1 :
        (binaryProductFunctor.obj X).obj x_1 ⟶ Functor.obj (Functor.obj prod.functor Y) x_1)
      prod.snd)
have refine_2 : BinaryFan.IsLimit.lift (binaryProductLimit Y x_1) (↾_root_.Prod.fst ≫ x) (↾_root_.Prod.snd) ≫ ↾_root_.Prod.snd =
  ↾_root_.Prod.snd
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Products (goal)
Goal:
J : Type v
F : J → Type (max v u)
x : Cone (Discrete.functor F)
x_1 :
  x.pt ⟶
    Cone.pt (J := Discrete J) (F := Discrete.functor F)
      { pt := (j : J) → F j,
        π :=
          Discrete.natTrans fun (x : Discrete J) ↦
            match (motive :=
              (x : Discrete J) →
                Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j)) x ⟶
                  Functor.obj (Discrete.functor F) x)
              x with
            | { as := j } =>
              ↾fun
                  (f :
                    Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j)) { as := j : Discrete J }) ↦
                f j }
w :
  ∀ (j : Discrete J),
    x_1 ≫
        NatTrans.app
          (Cone.π
            { pt := (j : J) → F j,
              π :=
                Discrete.natTrans fun (x : Discrete J) ↦
                  match (motive :=
                    (x : Discrete J) →
                      Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j)) x ⟶
                        Functor.obj (Discrete.functor F) x)
                    x with
                  | { as := j } =>
                    ↾fun
                        (f :
                          Functor.obj (Functor.obj (Functor.const (Discrete J)) ((j : J) → F j))
                            { as := j : Discrete J }) ↦
                      f j })
          j =
      x.π.app j
⊢ x_1 =
    ↾fun (x_2 : x.pt) (j : J) ↦
      (ConcreteCategory.hom (FC := TypeCat.Fun) (x.π.app { as := j : Discrete J }) :
          (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete J)).obj x.pt).obj { as := j })) →
            (fun (X : Type (max u v)) ↦ X) ((Discrete.functor F).obj { as := j }))
        x_2
have h : ∀ (x_2 : x.pt) (j : J),
  (ConcreteCategory.hom (FC := TypeCat.Fun) x_1).toFun x_2 j =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (↾fun (x_3 : x.pt) (j : J) ↦
          (ConcreteCategory.hom (FC := TypeCat.Fun) (x.π.app { as := j : Discrete J }) :
              (a : (fun (X : Type (max u v)) ↦ X) (((Functor.const (Discrete J)).obj x.pt).obj { as := j })) →
                (fun (X : Type (max u v)) ↦ X) ((Discrete.functor F).obj { as := j }))
            x_3))
      x_2 j
Tactic: ext x j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
X Y Z : Type u
X' Y' Z' : Type v
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
⊢ Eq (α := PullbackObj f g ⟶ Z) ((↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).1) ≫ f)
    ((↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).2) ≫ g)
have h : ∀ (p : PullbackObj f g),
  TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) ((↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).1) ≫ f)) p =
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) ((↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).2) ≫ g)) p
Tactic: ext p
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : Types.PullbackObj f g
⊢ (hom (FC := TypeCat.Fun) c.fst : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) X)
      (((equivPullbackObj hc).symm : (a : Types.PullbackObj f g) → c.pt) x : c.pt) =
    (↑x : X × Y).1
have obtain : ∀ (x : c.pt),
  Eq (α := (fun (X : Type v) ↦ X) X)
    ((hom (FC := TypeCat.Fun) c.fst : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) X)
        (((equivPullbackObj hc).symm : (a : Types.PullbackObj f g) → c.pt)
            ((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x : Types.PullbackObj f g) :
          c.pt) :
      (fun (X : Type v) ↦ X) X)
    ((↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x) : X × Y).1 : X)
Tactic: obtain ⟨x, rfl⟩ := (equivPullbackObj hc).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x : Types.PullbackObj f g
⊢ (hom (FC := TypeCat.Fun) c.snd : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) Y)
      (((equivPullbackObj hc).symm : (a : Types.PullbackObj f g) → c.pt) x : c.pt) =
    (↑x : X × Y).2
have obtain : ∀ (x : c.pt),
  Eq (α := (fun (X : Type v) ↦ X) Y)
    ((hom (FC := TypeCat.Fun) c.snd : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) Y)
        (((equivPullbackObj hc).symm : (a : Types.PullbackObj f g) → c.pt)
            ((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x : Types.PullbackObj f g) :
          c.pt) :
      (fun (X : Type v) ↦ X) Y)
    ((↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x) : X × Y).2 : Y)
Tactic: obtain ⟨x, rfl⟩ := (equivPullbackObj hc).surjective x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x y : c.pt
h₁ :
  Eq (α := (fun (X : Type v) ↦ X) X)
    ((hom (FC := TypeCat.Fun) c.fst : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) X) x :
      (fun (X : Type v) ↦ X) X)
    ((hom (FC := TypeCat.Fun) c.fst : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) X) y :
      (fun (X : Type v) ↦ X) X)
h₂ :
  Eq (α := (fun (X : Type v) ↦ X) Y)
    ((hom (FC := TypeCat.Fun) c.snd : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) Y) x :
      (fun (X : Type v) ↦ X) Y)
    ((hom (FC := TypeCat.Fun) c.snd : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) Y) y :
      (fun (X : Type v) ↦ X) Y)
⊢ Eq (α := Types.PullbackObj f g) ((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x : Types.PullbackObj f g)
    ((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) y : Types.PullbackObj f g)
have a : Eq.{v + 1} (α := X) (↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x) : X × Y).1
  (↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) y) : X × Y).1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
X Y S : Type v
f : X ⟶ S
g : Y ⟶ S
c : PullbackCone f g
hc : IsLimit c
x y : c.pt
h₁ :
  Eq (α := (fun (X : Type v) ↦ X) X)
    ((hom (FC := TypeCat.Fun) c.fst : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) X) x :
      (fun (X : Type v) ↦ X) X)
    ((hom (FC := TypeCat.Fun) c.fst : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) X) y :
      (fun (X : Type v) ↦ X) X)
h₂ :
  Eq (α := (fun (X : Type v) ↦ X) Y)
    ((hom (FC := TypeCat.Fun) c.snd : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) Y) x :
      (fun (X : Type v) ↦ X) Y)
    ((hom (FC := TypeCat.Fun) c.snd : (a : (fun (X : Type v) ↦ X) c.pt) → (fun (X : Type v) ↦ X) Y) y :
      (fun (X : Type v) ↦ X) Y)
a :
  Eq.{v + 1} (α := X) (↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x) : X × Y).1
    (↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) y) : X × Y).1
⊢ Eq (α := Types.PullbackObj f g) ((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x : Types.PullbackObj f g)
    ((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) y : Types.PullbackObj f g)
have a₁ : Eq.{v + 1} (α := Y) (↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) x) : X × Y).2
  (↑((equivPullbackObj hc : (a : c.pt) → Types.PullbackObj f g) y) : X × Y).2
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoPullback f g).inv ≫ pullback.fst f g = ↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).1
have h : ∀ (x : PullbackObj f g),
  (hom (FC := TypeCat.Fun) ((pullbackIsoPullback f g).inv ≫ pullback.fst f g)).toFun x =
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).1)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
X Y Z : Type u
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoPullback f g).inv ≫ pullback.snd f g = ↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).2
have h : ∀ (x : PullbackObj f g),
  (hom (FC := TypeCat.Fun) ((pullbackIsoPullback f g).inv ≫ pullback.snd f g)).toFun x =
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (↾fun (p : PullbackObj f g) ↦ (↑p : X × Y).2)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
⊢ Eq (α := (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (⇑(hom (FC := TypeCat.Fun) fst) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
    (Function.comp (β := X × Y) _root_.Prod.fst
      (Function.comp (β :=
        { p : X × Y //
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
              (fun (X : Type u) ↦ X) Z) })
        (Subtype.val (p := fun (p : X × Y) ↦
          Eq (α := (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
              (fun (X : Type u) ↦ X) Z)
            ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
              (fun (X : Type u) ↦ X) Z)))
        (⇑(hom (FC := TypeCat.Fun) e.hom) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (PullbackObj f g))))
have h₁ : ∀ (p : (fun (X : Type u) ↦ X) P),
  Eq (α := (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
      (fun (X : Type u) ↦ X) X)
    (Function.comp (β := X × Y) _root_.Prod.fst
        (Function.comp (β :=
          { p : X × Y //
            Eq (α := (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
                (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
                (fun (X : Type u) ↦ X) Z) })
          (Subtype.val (p := fun (p : X × Y) ↦
            Eq (α := (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
                (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
                (fun (X : Type u) ↦ X) Z)))
          (⇑(hom (FC := TypeCat.Fun) e.hom) :
            (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (PullbackObj f g)))
        p :
      X)
Tactic: ext p
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun (X : Type u) ↦ X) P
⊢ Eq (α := (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
      (fun (X : Type u) ↦ X) X)
    (Function.comp (β := X × Y) _root_.Prod.fst
        (Function.comp (β :=
          { p : X × Y //
            Eq (α := (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
                (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
                (fun (X : Type u) ↦ X) Z) })
          (Subtype.val (p := fun (p : X × Y) ↦
            Eq (α := (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
                (fun (X : Type u) ↦ X) Z)
              ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
                (fun (X : Type u) ↦ X) Z)))
          (⇑(hom (FC := TypeCat.Fun) e.hom) :
            (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (PullbackObj f g)))
        p :
      X)
have h₁ : Eq (α := (fun (X : Type u) ↦ X) X)
  ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
    (fun (X : Type u) ↦ X) X)
  ((hom (FC := TypeCat.Fun) (pullback.fst f g) : (a : (fun (X : Type u) ↦ X) (pullback f g)) → (fun (X : Type u) ↦ X) X)
      ((hom (FC := TypeCat.Fun) (Iso.hom h.isoPullback) :
            (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (pullback f g))
          p :
        (fun (X : Type u) ↦ X) (pullback f g)) :
    (fun (X : Type u) ↦ X) X)
Tactic: suffices fst p = pullback.fst f g (h.isoPullback.hom p) by simpa
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun (X : Type u) ↦ X) P
⊢ Eq (α := (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
      (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) (pullback.fst f g) :
          (a : (fun (X : Type u) ↦ X) (pullback f g)) → (fun (X : Type u) ↦ X) X)
        ((hom (FC := TypeCat.Fun) (Iso.hom h.isoPullback) :
              (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (pullback f g))
            p :
          (fun (X : Type u) ↦ X) (pullback f g)) :
      (fun (X : Type u) ↦ X) X)
have h₁ : Eq (α := (fun (X : Type u) ↦ X) X)
  ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
    (fun (X : Type u) ↦ X) X)
  ((hom (FC := TypeCat.Fun) (CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.fst f g)) :
        (a : P) → X)
      p :
    X)
Tactic: rw [← comp_apply h.isoPullback.hom (pullback.fst f g), IsPullback.isoPullback_hom_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
p : (fun (X : Type u) ↦ X) P
h₁ :
  Eq (α := (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
      (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) (CategoryStruct.comp (Y := pullback f g) (Iso.hom h.isoPullback) (pullback.fst f g)) :
          (a : P) → X)
        p :
      X)
⊢ Eq (α := (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
      (fun (X : Type u) ↦ X) X)
    ((hom (FC := TypeCat.Fun) (pullback.fst f g) :
          (a : (fun (X : Type u) ↦ X) (pullback f g)) → (fun (X : Type u) ↦ X) X)
        ((hom (FC := TypeCat.Fun) (Iso.hom h.isoPullback) :
              (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (pullback f g))
            p :
          (fun (X : Type u) ↦ X) (pullback f g)) :
      (fun (X : Type u) ↦ X) X)
have h₂ : Eq (α := (fun (X : Type u) ↦ X) X)
  ((hom (FC := TypeCat.Fun) fst : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X) p :
    (fun (X : Type u) ↦ X) X)
  ((hom (FC := TypeCat.Fun) fst : (a : P) → X) p : X)
Tactic: rw [← comp_apply h.isoPullback.hom (pullback.fst f g), IsPullback.isoPullback_hom_fst]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (hypothesis)
Goal:
P X Y Z : Type u
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
e : P ≅ PullbackObj f g := h.isoPullback ≪≫ pullbackIsoPullback f g
⊢ Eq (α := Set ((fun (X : Type u) ↦ X) X))
    (Set.range (ι := (fun (X : Type u) ↦ X) P)
      (⇑(hom (FC := TypeCat.Fun) fst) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X))
    (Set.preimage (β := (fun (X : Type u) ↦ X) Z)
      (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z)
      (Set.range (ι := (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z)))
have this : Eq (α := (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
  (⇑(hom (FC := TypeCat.Fun) fst) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) X)
  (Function.comp (β := X × Y) _root_.Prod.fst
    (Function.comp (β :=
      { p : X × Y //
        Eq (α := (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
            (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
            (fun (X : Type u) ↦ X) Z) })
      (Subtype.val (p := fun (p : X × Y) ↦
        Eq (α := (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z) p.1 :
            (fun (X : Type u) ↦ X) Z)
          ((hom (FC := TypeCat.Fun) g : (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z) p.2 :
            (fun (X : Type u) ↦ X) Z)))
      (⇑(hom (FC := TypeCat.Fun) e.hom) : (a : (fun (X : Type u) ↦ X) P) → (fun (X : Type u) ↦ X) (PullbackObj f g))))
Tactic: have : fst = _root_.Prod.fst ∘ Subtype.val ∘ e.hom := by
    ext p
    suffices fst p = pullback.fst f g (h.isoPullback.hom p) by simpa
    rw [← comp_apply h.isoPullback.hom (pullback.fst f g), IsPullback.isoPullback_hom_fst]