awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{v_1, u, u_1, u + 1} C (Type u)
f : F ⟶ G
H : MonoFactorisation f
w :
  ∀ (x : C) (x_1 : (monoFactorisation f).I.obj x),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (NatTrans.app
            ({
                app := fun (X : C) ↦
                  ↾fun (x : (monoFactorisation f).I.obj X) ↦
                    match (motive := (monoFactorisation f).I.obj X → H.I.obj X) x with
                    | ⟨x, hx⟩ =>
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (H.e.app X) :
                          (a : (fun (X : Type u) ↦ X) (F.obj X)) → (fun (X : Type u) ↦ X) (H.I.obj X))
                        (Exists.choose (p := fun (y : F.obj X) ↦
                          (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                                (a : (fun (X : Type u) ↦ X) (F.obj X)) → (fun (X : Type u) ↦ X) (G.obj X))
                              y =
                            x)
                          hx),
                naturality := ⋯ : NatTrans (monoFactorisation f).I H.I } ≫
              H.m)
            x))
        x_1 =
      (ConcreteCategory.hom (FC := TypeCat.Fun) ((monoFactorisation f).m.app x)).toFun x_1
⊢ {
        app := fun (X : C) ↦
          ↾fun (x : (monoFactorisation f).I.obj X) ↦
            match (motive := (monoFactorisation f).I.obj X → H.I.obj X) x with
            | ⟨x, hx⟩ =>
              (ConcreteCategory.hom (FC := TypeCat.Fun) (H.e.app X) :
                  (a : (fun (X : Type u) ↦ X) (F.obj X)) → (fun (X : Type u) ↦ X) (H.I.obj X))
                (Exists.choose (p := fun (y : F.obj X) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                        (a : (fun (X : Type u) ↦ X) (F.obj X)) → (fun (X : Type u) ↦ X) (G.obj X))
                      y =
                    x)
                  hx),
        naturality := ⋯ } ≫
      H.m =
    (monoFactorisation f).m

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{v_1, u, u_1, u + 1} C (Type u)
f : F ⟶ G
H : MonoFactorisation f
x : C
x_1 : (monoFactorisation f).I.obj x
w :
  (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x) : (a : F.obj x) → G.obj x)
      (Exists.choose (p := fun (y : F.obj x) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x) : (a : F.obj x) → G.obj x) y = (↑x_1 : G.obj x)) ⋯) =
    (↑x_1 : G.obj x)
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (NatTrans.app
          ({
              app := fun (X : C) ↦
                ↾fun (x : (monoFactorisation f).I.obj X) ↦
                  match (motive := (monoFactorisation f).I.obj X → H.I.obj X) x with
                  | ⟨x, hx⟩ =>
                    (ConcreteCategory.hom (FC := TypeCat.Fun) (H.e.app X) :
                        (a : (fun (X : Type u) ↦ X) (F.obj X)) → (fun (X : Type u) ↦ X) (H.I.obj X))
                      (Exists.choose (p := fun (y : F.obj X) ↦
                        (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app X) :
                              (a : (fun (X : Type u) ↦ X) (F.obj X)) → (fun (X : Type u) ↦ X) (G.obj X))
                            y =
                          x)
                        hx),
              naturality := ⋯ : NatTrans (monoFactorisation f).I H.I } ≫
            H.m)
          x))
      x_1 =
    (ConcreteCategory.hom (FC := TypeCat.Fun) ((monoFactorisation f).m.app x)).toFun x_1

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
F G : Functor.{v_1, u, u_1, u + 1} C (Type u)
f : F ⟶ G
H : MonoFactorisation f
x : C
x_1 : (monoFactorisation f).I.obj x
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x) : (a : F.obj x) → G.obj x)
      (Exists.choose (p := fun (y : F.obj x) ↦
        (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x) : (a : F.obj x) → G.obj x) y = (↑x_1 : G.obj x)) ⋯) =
    (↑x_1 : G.obj x)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
α : Type w
inst_2 : HasLimitsOfShape.{w, w, v, u} (Discrete α) C
f : α → Functor.{v₁, v, u₁, u} D C
d : D
s : α
⊢ Eq (α := (∏ᶜ f).obj d ⟶ (f s).obj d)
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (s : α) ↦ (f s).obj d)
        (Iso.hom (piObjIso f d) : (∏ᶜ f).obj d ⟶ piObj.{w, v, u} fun (s : α) ↦ (f s).obj d)
        (Pi.π (fun (s : α) ↦ (f s).obj d) s : (piObj.{w, v, u} fun (s : α) ↦ (f s).obj d) ⟶ (f s).obj d) :
      (∏ᶜ f).obj d ⟶ (f s).obj d)
    (NatTrans.app (Pi.π f s) d : (∏ᶜ f).obj d ⟶ (f s).obj d)

Tactic:
simp [piObjIso]

Premises used: CategoryTheory.Limits.piObjIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
α : Type w
inst_2 : HasLimitsOfShape.{w, w, v, u} (Discrete α) C
f : α → Functor.{v₁, v, u₁, u} D C
d : D
s : α
⊢ Eq (α := (piObj.{w, v, u} fun (s : α) ↦ (f s).obj d) ⟶ (f s).obj d)
    (CategoryStruct.comp (Y := (∏ᶜ f).obj d)
        (Iso.inv (piObjIso f d) : (piObj.{w, v, u} fun (s : α) ↦ (f s).obj d) ⟶ (∏ᶜ f).obj d)
        (NatTrans.app (Pi.π f s) d : (∏ᶜ f).obj d ⟶ (f s).obj d) :
      (piObj.{w, v, u} fun (s : α) ↦ (f s).obj d) ⟶ (f s).obj d)
    (Pi.π (fun (s : α) ↦ (f s).obj d) s : (piObj.{w, v, u} fun (s : α) ↦ (f s).obj d) ⟶ (f s).obj d)

Tactic:
simp [piObjIso]

Premises used: CategoryTheory.Limits.piObjIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
α : Type w
inst_2 : HasColimitsOfShape.{w, w, v, u} (Discrete α) C
f : α → Functor.{v₁, v, u₁, u} D C
d : D
s : α
⊢ Eq (α := (f s).obj d ⟶ sigmaObj.{w, v, u} fun (s : α) ↦ (f s).obj d)
    (CategoryStruct.comp (Y := (∐ f).obj d) (NatTrans.app (Sigma.ι f s) d : (f s).obj d ⟶ (∐ f).obj d)
        (Iso.hom (sigmaObjIso f d) : (∐ f).obj d ⟶ sigmaObj.{w, v, u} fun (s : α) ↦ (f s).obj d) :
      (f s).obj d ⟶ sigmaObj.{w, v, u} fun (s : α) ↦ (f s).obj d)
    (Sigma.ι.{w, v, u} (C := C) (fun (s : α) ↦ (f s).obj d) s :
      (f s).obj d ⟶ sigmaObj.{w, v, u} fun (s : α) ↦ (f s).obj d)

Tactic:
simp [sigmaObjIso]

Premises used: CategoryTheory.Limits.sigmaObjIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
α : Type w
inst_2 : HasColimitsOfShape.{w, w, v, u} (Discrete α) C
f : α → Functor.{v₁, v, u₁, u} D C
d : D
s : α
⊢ Eq (α := (f s).obj d ⟶ (∐ f).obj d)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (s : α) ↦ (f s).obj d)
        (Sigma.ι.{w, v, u} (C := C) (fun (s : α) ↦ (f s).obj d) s :
          (f s).obj d ⟶ sigmaObj.{w, v, u} fun (s : α) ↦ (f s).obj d)
        (Iso.inv (sigmaObjIso f d) : (sigmaObj.{w, v, u} fun (s : α) ↦ (f s).obj d) ⟶ (∐ f).obj d) :
      (f s).obj d ⟶ (∐ f).obj d)
    (NatTrans.app (Sigma.ι f s) d : (f s).obj d ⟶ (∐ f).obj d)

Tactic:
simp [sigmaObjIso]

Premises used: CategoryTheory.Limits.sigmaObjIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x : D
⊢ Eq (α :=
    Cone.pt (F := cospan (f.app x) (g.app x))
        { pt := (c x).pt, π := (c x).π ≫ cospanHomMk (H.map (𝟙 x)) (F.map (𝟙 x)) (G.map (𝟙 x)) ⋯ ⋯ :
          Cone (cospan (f.app x) (g.app x)) } ⟶
      (cospan (f.app x) (g.app x)).obj none)
    ((hc x).lift
        { pt := (c x).pt, π := (c x).π ≫ cospanHomMk (H.map (𝟙 x)) (F.map (𝟙 x)) (G.map (𝟙 x)) ⋯ ⋯ :
          Cone (cospan (f.app x) (g.app x)) } ≫
      (c x).π.app none)
    (𝟙 (c x).pt ≫ (c x).π.app none)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x : D
⊢ Eq (α :=
    Cone.pt (F := cospan (f.app x) (g.app x))
        { pt := (c x).pt, π := (c x).π ≫ cospanHomMk (H.map (𝟙 x)) (F.map (𝟙 x)) (G.map (𝟙 x)) ⋯ ⋯ :
          Cone (cospan (f.app x) (g.app x)) } ⟶
      (cospan (f.app x) (g.app x)).obj (some WalkingPair.left))
    ((hc x).lift
        { pt := (c x).pt, π := (c x).π ≫ cospanHomMk (H.map (𝟙 x)) (F.map (𝟙 x)) (G.map (𝟙 x)) ⋯ ⋯ :
          Cone (cospan (f.app x) (g.app x)) } ≫
      (c x).π.app (some WalkingPair.left))
    (𝟙 (c x).pt ≫ (c x).π.app (some WalkingPair.left))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x : D
⊢ Eq (α :=
    Cone.pt (F := cospan (f.app x) (g.app x))
        { pt := (c x).pt, π := (c x).π ≫ cospanHomMk (H.map (𝟙 x)) (F.map (𝟙 x)) (G.map (𝟙 x)) ⋯ ⋯ :
          Cone (cospan (f.app x) (g.app x)) } ⟶
      (cospan (f.app x) (g.app x)).obj (some WalkingPair.right))
    ((hc x).lift
        { pt := (c x).pt, π := (c x).π ≫ cospanHomMk (H.map (𝟙 x)) (F.map (𝟙 x)) (G.map (𝟙 x)) ⋯ ⋯ :
          Cone (cospan (f.app x) (g.app x)) } ≫
      (c x).π.app (some WalkingPair.right))
    (𝟙 (c x).pt ≫ (c x).π.app (some WalkingPair.right))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X Y Z : D
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α :=
    Cone.pt (F := cospan (f.app Z) (g.app Z))
        { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map (x ≫ x_1)) (F.map (x ≫ x_1)) (G.map (x ≫ x_1)) ⋯ ⋯ :
          Cone (cospan (f.app Z) (g.app Z)) } ⟶
      (cospan (f.app Z) (g.app Z)).obj none)
    ((hc Z).lift
        { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map (x ≫ x_1)) (F.map (x ≫ x_1)) (G.map (x ≫ x_1)) ⋯ ⋯ :
          Cone (cospan (f.app Z) (g.app Z)) } ≫
      (c Z).π.app none)
    (CategoryStruct.comp (Y := (c Y).pt)
        ((hc Y).lift { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map x) (F.map x) (G.map x) ⋯ ⋯ } :
          Cone.pt (F := cospan (f.app Y) (g.app Y))
              { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map x) (F.map x) (G.map x) ⋯ ⋯ :
                Cone (cospan (f.app Y) (g.app Y)) } ⟶
            (c Y).pt)
        ((hc Z).lift { pt := (c Y).pt, π := (c Y).π ≫ cospanHomMk (H.map x_1) (F.map x_1) (G.map x_1) ⋯ ⋯ } :
          Cone.pt (F := cospan (f.app Z) (g.app Z))
              { pt := (c Y).pt, π := (c Y).π ≫ cospanHomMk (H.map x_1) (F.map x_1) (G.map x_1) ⋯ ⋯ :
                Cone (cospan (f.app Z) (g.app Z)) } ⟶
            (c Z).pt) ≫
      (c Z).π.app none)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X Y Z : D
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α :=
    Cone.pt (F := cospan (f.app Z) (g.app Z))
        { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map (x ≫ x_1)) (F.map (x ≫ x_1)) (G.map (x ≫ x_1)) ⋯ ⋯ :
          Cone (cospan (f.app Z) (g.app Z)) } ⟶
      (cospan (f.app Z) (g.app Z)).obj (some WalkingPair.left))
    ((hc Z).lift
        { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map (x ≫ x_1)) (F.map (x ≫ x_1)) (G.map (x ≫ x_1)) ⋯ ⋯ :
          Cone (cospan (f.app Z) (g.app Z)) } ≫
      (c Z).π.app (some WalkingPair.left))
    (CategoryStruct.comp (Y := (c Y).pt)
        ((hc Y).lift { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map x) (F.map x) (G.map x) ⋯ ⋯ } :
          Cone.pt (F := cospan (f.app Y) (g.app Y))
              { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map x) (F.map x) (G.map x) ⋯ ⋯ :
                Cone (cospan (f.app Y) (g.app Y)) } ⟶
            (c Y).pt)
        ((hc Z).lift { pt := (c Y).pt, π := (c Y).π ≫ cospanHomMk (H.map x_1) (F.map x_1) (G.map x_1) ⋯ ⋯ } :
          Cone.pt (F := cospan (f.app Z) (g.app Z))
              { pt := (c Y).pt, π := (c Y).π ≫ cospanHomMk (H.map x_1) (F.map x_1) (G.map x_1) ⋯ ⋯ :
                Cone (cospan (f.app Z) (g.app Z)) } ⟶
            (c Z).pt) ≫
      (c Z).π.app (some WalkingPair.left))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
X Y Z : D
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq (α :=
    Cone.pt (F := cospan (f.app Z) (g.app Z))
        { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map (x ≫ x_1)) (F.map (x ≫ x_1)) (G.map (x ≫ x_1)) ⋯ ⋯ :
          Cone (cospan (f.app Z) (g.app Z)) } ⟶
      (cospan (f.app Z) (g.app Z)).obj (some WalkingPair.right))
    ((hc Z).lift
        { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map (x ≫ x_1)) (F.map (x ≫ x_1)) (G.map (x ≫ x_1)) ⋯ ⋯ :
          Cone (cospan (f.app Z) (g.app Z)) } ≫
      (c Z).π.app (some WalkingPair.right))
    (CategoryStruct.comp (Y := (c Y).pt)
        ((hc Y).lift { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map x) (F.map x) (G.map x) ⋯ ⋯ } :
          Cone.pt (F := cospan (f.app Y) (g.app Y))
              { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map x) (F.map x) (G.map x) ⋯ ⋯ :
                Cone (cospan (f.app Y) (g.app Y)) } ⟶
            (c Y).pt)
        ((hc Z).lift { pt := (c Y).pt, π := (c Y).π ≫ cospanHomMk (H.map x_1) (F.map x_1) (G.map x_1) ⋯ ⋯ } :
          Cone.pt (F := cospan (f.app Z) (g.app Z))
              { pt := (c Y).pt, π := (c Y).π ≫ cospanHomMk (H.map x_1) (F.map x_1) (G.map x_1) ⋯ ⋯ :
                Cone (cospan (f.app Z) (g.app Z)) } ⟶
            (c Z).pt) ≫
      (c Z).π.app (some WalkingPair.right))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
w :
  ∀ (x : D),
    Eq (α :=
      Functor.obj.{v₂, v₁, u₂, u₁}
          { obj := fun (X : D) ↦ (c X).pt,
            map := fun {X Y : D} (h : X ⟶ Y) ↦
              (hc Y).lift { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯ },
            map_id := ⋯, map_comp := ⋯ }
          x ⟶
        H.obj x)
      (NatTrans.app
        ({ app := fun (X : D) ↦ (c X).fst, naturality := ⋯ :
            NatTrans
              { obj := fun (X : D) ↦ (c X).pt,
                map := fun {X Y : D} (h : X ⟶ Y) ↦
                  (hc Y).lift
                    { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯ :
                      Cone (cospan (f.app Y) (g.app Y)) },
                map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v₁, u₂, u₁} D C }
              F } ≫
          f)
        x)
      (NatTrans.app
        ({ app := fun (X : D) ↦ (c X).snd, naturality := ⋯ :
            NatTrans
              { obj := fun (X : D) ↦ (c X).pt,
                map := fun {X Y : D} (h : X ⟶ Y) ↦
                  (hc Y).lift
                    { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯ :
                      Cone (cospan (f.app Y) (g.app Y)) },
                map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v₁, u₂, u₁} D C }
              G } ≫
          g)
        x)
⊢ Eq (α :=
    { obj := fun (X : D) ↦ (c X).pt,
        map := fun {X Y : D} (h : X ⟶ Y) ↦
          (hc Y).lift { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯ },
        map_id := ⋯, map_comp := ⋯ } ⟶
      H)
    ({ app := fun (X : D) ↦ (c X).fst, naturality := ⋯ :
        NatTrans
          { obj := fun (X : D) ↦ (c X).pt,
            map := fun {X Y : D} (h : X ⟶ Y) ↦
              (hc Y).lift
                { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯ :
                  Cone (cospan (f.app Y) (g.app Y)) },
            map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v₁, u₂, u₁} D C }
          F } ≫
      f)
    ({ app := fun (X : D) ↦ (c X).snd, naturality := ⋯ :
        NatTrans
          { obj := fun (X : D) ↦ (c X).pt,
            map := fun {X Y : D} (h : X ⟶ Y) ↦
              (hc Y).lift
                { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯ :
                  Cone (cospan (f.app Y) (g.app Y)) },
            map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v₁, u₂, u₁} D C }
          G } ≫
      g)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
x : D
⊢ Eq (α :=
    Functor.obj.{v₂, v₁, u₂, u₁}
        { obj := fun (X : D) ↦ (c X).pt,
          map := fun {X Y : D} (h : X ⟶ Y) ↦
            (hc Y).lift { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯ },
          map_id := ⋯, map_comp := ⋯ }
        x ⟶
      H.obj x)
    (NatTrans.app
      ({ app := fun (X : D) ↦ (c X).fst, naturality := ⋯ :
          NatTrans
            { obj := fun (X : D) ↦ (c X).pt,
              map := fun {X Y : D} (h : X ⟶ Y) ↦
                (hc Y).lift
                  { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯ :
                    Cone (cospan (f.app Y) (g.app Y)) },
              map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v₁, u₂, u₁} D C }
            F } ≫
        f)
      x)
    (NatTrans.app
      ({ app := fun (X : D) ↦ (c X).snd, naturality := ⋯ :
          NatTrans
            { obj := fun (X : D) ↦ (c X).pt,
              map := fun {X Y : D} (h : X ⟶ Y) ↦
                (hc Y).lift
                  { pt := (c X).pt, π := (c X).π ≫ cospanHomMk (H.map h) (F.map h) (G.map h) ⋯ ⋯ :
                    Cone (cospan (f.app Y) (g.app Y)) },
              map_id := ⋯, map_comp := ⋯ : Functor.{v₂, v₁, u₂, u₁} D C }
            G } ≫
        g)
      x)

Tactic:
simp [(c _).condition]

Premises used: CategoryTheory.Limits.PullbackCone.condition
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
k : D
refine_1 : cospan (f.app k) (g.app k) ≅ cospan f g ⋙ Functor.obj (evaluation D C) k
refine_2 :
  (Cone.postcompose
          (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
              (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
              (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
      (c k) ≅
    Functor.mapCone (Functor.obj (evaluation D C) k) (combine f g c hc)
⊢ IsLimit (F := cospan f g ⋙ Functor.obj (evaluation D C) k)
    (Functor.mapCone (Functor.obj (evaluation D C) k) (combine f g c hc))

Tactic:
refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (hc k)

Premises used: DFunLike.coe, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
k : D
⊢ cospan (f.app k) (g.app k) ≅ cospan f g ⋙ Functor.obj (evaluation D C) k

Tactic:
exact cospanIsoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.cospanIsoMk
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
k : D
refine_2 :
  ∀ (j : WalkingCospan),
    NatTrans.app
        ((Cone.postcompose
                (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                    (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                    (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
            (c k)).π
        j =
      Iso.hom
          (Iso.refl
            ((Cone.postcompose
                    (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                        (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                        (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
                (c k)).pt) ≫
        NatTrans.app (Cone.π (Functor.mapCone (Functor.obj (evaluation D C) k) (combine f g c hc))) j
⊢ (Cone.postcompose
          (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
              (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
              (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
      (c k) ≅
    Functor.mapCone (Functor.obj (evaluation D C) k) (combine f g c hc)

Tactic:
refine Cone.ext (Iso.refl _) ?_

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : HasPullbacks.{v₁, u₁} C
f : F ⟶ H
g : G ⟶ H
d : D
⊢ Eq (α := (pullback f g).obj d ⟶ F.obj d)
    (CategoryStruct.comp (Y := pullback (f.app d) (g.app d))
        (Iso.hom (pullbackObjIso f g d) : (pullback f g).obj d ⟶ pullback (f.app d) (g.app d))
        (pullback.fst (f.app d) (g.app d) : pullback (f.app d) (g.app d) ⟶ F.obj d) :
      (pullback f g).obj d ⟶ F.obj d)
    (NatTrans.app (pullback.fst f g) d : (pullback f g).obj d ⟶ F.obj d)

Tactic:
simp [pullbackObjIso]

Premises used: CategoryTheory.Limits.pullbackObjIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : HasPullbacks.{v₁, u₁} C
f : F ⟶ H
g : G ⟶ H
d : D
⊢ Eq (α := (pullback f g).obj d ⟶ G.obj d)
    (CategoryStruct.comp (Y := pullback (f.app d) (g.app d))
        (Iso.hom (pullbackObjIso f g d) : (pullback f g).obj d ⟶ pullback (f.app d) (g.app d))
        (pullback.snd (f.app d) (g.app d) : pullback (f.app d) (g.app d) ⟶ G.obj d) :
      (pullback f g).obj d ⟶ G.obj d)
    (NatTrans.app (pullback.snd f g) d : (pullback f g).obj d ⟶ G.obj d)

Tactic:
simp [pullbackObjIso]

Premises used: CategoryTheory.Limits.pullbackObjIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G H : Functor.{v₂, v₁, u₂, u₁} D C
inst_2 : HasPullbacks.{v₁, u₁} C
f : F ⟶ H
g : G ⟶ H
d : D
⊢ Eq (α := pullback (f.app d) (g.app d) ⟶ F.obj d)
    (CategoryStruct.comp (Y := (pullback f g).obj d)
        (Iso.inv (pullbackObjIso f g d) : pullback (f.app d) (g.app d) ⟶ (pullback f g).obj d)
        (NatTrans.app (pullback.fst f g) d : (pullback f g).obj d ⟶ F.obj d) :
      pullback (f.app d) (g.app d) ⟶ F.obj d)
    (pullback.fst (f.app d) (g.app d) : pullback (f.app d) (g.app d) ⟶ F.obj d)

Tactic:
simp [pullbackObjIso]

Premises used: CategoryTheory.Limits.pullbackObjIso