awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
inst_4 : HasLimitsOfShape.{v₁, u₁, v, u} J C
F G : K ⥤ Functor.{v₁, v, u₁, u} J C
η : F ⟶ G
k : K
⊢ Eq (α :=
    (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
      (obj (flipFunctor K J C ⋙ lim) G).obj k)
    (NatTrans.app
      (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
        Iso.hom
          ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip)) G))
      k)
    (NatTrans.app
      (Iso.hom
          ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip)) F) ≫
        map (flipFunctor K J C ⋙ lim) η)
      k)
have w : ∀ (j : J),
  Eq (α :=
    (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
      ((obj (flipFunctor K J C) G).obj j).obj k)
    (CategoryStruct.comp (Y := (limit (obj (flipFunctor K J C) G)).obj k)
      (NatTrans.app
        (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) η ≫
          Iso.hom
            ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip))
              G))
        k)
      (NatTrans.app (limit.π (obj (flipFunctor K J C) G) j) k))
    (CategoryStruct.comp (Y := (limit (obj (flipFunctor K J C) G)).obj k)
      (NatTrans.app
          (Iso.hom
              ((fun (x : K ⥤ Functor.{v₁, v, u₁, u} J C) ↦ (Iso.symm (limitFlipIsoCompLim x) : x ⋙ lim ≅ limit x.flip))
                F) ≫
            map (flipFunctor K J C ⋙ lim) η)
          k :
        (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) lim) F).obj k ⟶
          (obj (flipFunctor K J C ⋙ lim) G).obj k)
      (NatTrans.app (limit.π (obj (flipFunctor K J C) G) j) k))
Tactic: apply limit_obj_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F G : J ⥤ Functor.{v₂, v, u₂, u} K C
η : F ⟶ G
⊢ Eq (α := obj colim F ⟶ obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G)
    (map colim η ≫ Iso.hom (colimitIsoFlipCompColim G))
    (CategoryStruct.comp (Y := obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
      (Iso.hom (colimitIsoFlipCompColim F))
      (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))
have w : ∀ (k : K),
  Eq (α :=
    (obj colim F).obj k ⟶
      (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k)
    (NatTrans.app (map colim η ≫ Iso.hom (colimitIsoFlipCompColim G)) k)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
        (Iso.hom (colimitIsoFlipCompColim F))
        (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))
      k)
Tactic: ext k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F G : J ⥤ Functor.{v₂, v, u₂, u} K C
η : F ⟶ G
k : K
⊢ Eq (α :=
    (obj colim F).obj k ⟶
      (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k)
    (NatTrans.app (map colim η ≫ Iso.hom (colimitIsoFlipCompColim G)) k)
    (NatTrans.app
      (CategoryStruct.comp (Y :=
        obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
        (Iso.hom (colimitIsoFlipCompColim F))
        (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))
      k)
have w : ∀ (j : J),
  Eq (α :=
    (F.obj j).obj k ⟶ (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k)
    (CategoryStruct.comp (Y := (colimit F).obj k) (NatTrans.app (colimit.ι F j) k)
      (NatTrans.app (map colim η ≫ Iso.hom (colimitIsoFlipCompColim G)) k))
    (CategoryStruct.comp (Y := (colimit F).obj k) (NatTrans.app (colimit.ι F j) k : (F.obj j).obj k ⟶ (colimit F).obj k)
      (NatTrans.app
          (CategoryStruct.comp (Y :=
            obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
            (Iso.hom (colimitIsoFlipCompColim F))
            (map (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))
          k :
        (obj colim F).obj k ⟶
          (obj (flipFunctor J K C ⋙ obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k))
Tactic: apply colimit_obj_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F G : K ⥤ Functor.{v₁, v, u₁, u} J C
η : F ⟶ G
⊢ Eq (α := obj (flipFunctor K J C ⋙ colim) F ⟶ obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G)
    (map (flipFunctor K J C ⋙ colim) η ≫ Iso.hom (colimitFlipIsoCompColim G))
    (CategoryStruct.comp (Y := obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
      (Iso.hom (colimitFlipIsoCompColim F)) (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))
have w : ∀ (k : K),
  Eq (α :=
    (obj (flipFunctor K J C ⋙ colim) F).obj k ⟶
      (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k)
    (NatTrans.app (map (flipFunctor K J C ⋙ colim) η ≫ Iso.hom (colimitFlipIsoCompColim G)) k)
    (NatTrans.app
      (CategoryStruct.comp (Y := obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
        (Iso.hom (colimitFlipIsoCompColim F)) (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))
      k)
Tactic: ext k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
J : Type u₁
inst_2 : Category.{v₁, u₁} J
K : Type u₂
inst_3 : Category.{v₂, u₂} K
inst_4 : HasColimitsOfShape.{v₁, u₁, v, u} J C
F G : K ⥤ Functor.{v₁, v, u₁, u} J C
η : F ⟶ G
k : K
⊢ Eq (α :=
    (obj (flipFunctor K J C ⋙ colim) F).obj k ⟶
      (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k)
    (NatTrans.app (map (flipFunctor K J C ⋙ colim) η ≫ Iso.hom (colimitFlipIsoCompColim G)) k)
    (NatTrans.app
      (CategoryStruct.comp (Y := obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
        (Iso.hom (colimitFlipIsoCompColim F)) (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))
      k)
have w : ∀ (j : J),
  Eq (α :=
    ((obj (flipFunctor K J C) F).obj j).obj k ⟶
      (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k)
    (CategoryStruct.comp (Y := (colimit (obj (flipFunctor K J C) F)).obj k)
      (NatTrans.app (colimit.ι (obj (flipFunctor K J C) F) j) k)
      (NatTrans.app (map (flipFunctor K J C ⋙ colim) η ≫ Iso.hom (colimitFlipIsoCompColim G)) k))
    (CategoryStruct.comp (Y := (colimit (obj (flipFunctor K J C) F)).obj k)
      (NatTrans.app (colimit.ι (obj (flipFunctor K J C) F) j) k :
        ((obj (flipFunctor K J C) F).obj j).obj k ⟶ (colimit (obj (flipFunctor K J C) F)).obj k)
      (NatTrans.app
          (CategoryStruct.comp (Y := obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) F)
            (Iso.hom (colimitFlipIsoCompColim F))
            (map (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) η))
          k :
        (obj (flipFunctor K J C ⋙ colim) F).obj k ⟶
          (obj (obj (whiskeringRight K (Functor.{v₁, v, u₁, u} J C) C) colim) G).obj k))
Tactic: apply colimit_obj_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F G : Functor.{v_2, v_1, u_2, u_1} D C
d : D
⊢ IsLimit (F := pair F G ⋙ Functor.obj (evaluation D C) d)
    (Functor.mapCone (Functor.obj (evaluation D C) d) (BinaryBicone.toCone (pointwiseBinaryBicone F G)))
have refine_1 : pair (F.obj d) (G.obj d) ≅ pair F G ⋙ Functor.obj (evaluation D C) d
Tactic: refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (BinaryBiproduct.isLimit (F.obj d) (G.obj d))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F G : Functor.{v_2, v_1, u_2, u_1} D C
d : D
refine_1 : pair (F.obj d) (G.obj d) ≅ pair F G ⋙ Functor.obj (evaluation D C) d
⊢ IsLimit (F := pair F G ⋙ Functor.obj (evaluation D C) d)
    (Functor.mapCone (Functor.obj (evaluation D C) d) (BinaryBicone.toCone (pointwiseBinaryBicone F G)))
have refine_2 : (Cone.postcompose (pairComp F G (Functor.obj (evaluation D C) d)).symm.hom).obj
    (BinaryBicone.toCone (BinaryBiproduct.bicone (F.obj d) (G.obj d))) ≅
  Functor.mapCone (Functor.obj (evaluation D C) d) (BinaryBicone.toCone (pointwiseBinaryBicone F G))
Tactic: refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (BinaryBiproduct.isLimit (F.obj d) (G.obj d))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F G : Functor.{v_2, v_1, u_2, u_1} D C
d : D
⊢ IsColimit (F := pair F G ⋙ Functor.obj (evaluation D C) d)
    (Functor.mapCocone (Functor.obj (evaluation D C) d) (BinaryBicone.toCocone (pointwiseBinaryBicone F G)))
have refine_1 : pair (F.obj d) (G.obj d) ≅ pair F G ⋙ Functor.obj (evaluation D C) d
Tactic: refine IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_ (BinaryBiproduct.isColimit (F.obj d) (G.obj d))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasBinaryBiproducts.{v_1, u_1} C
D : Type u_2
inst_3 : Category.{v_2, u_2} D
F G : Functor.{v_2, v_1, u_2, u_1} D C
d : D
refine_1 : pair (F.obj d) (G.obj d) ≅ pair F G ⋙ Functor.obj (evaluation D C) d
⊢ IsColimit (F := pair F G ⋙ Functor.obj (evaluation D C) d)
    (Functor.mapCocone (Functor.obj (evaluation D C) d) (BinaryBicone.toCocone (pointwiseBinaryBicone F G)))
have refine_2 : (Cocone.precompose (pairComp F G (Functor.obj (evaluation D C) d)).symm.inv).obj
    (BinaryBicone.toCocone (BinaryBiproduct.bicone (F.obj d) (G.obj d))) ≅
  Functor.mapCocone (Functor.obj (evaluation D C) d) (BinaryBicone.toCocone (pointwiseBinaryBicone F G))
Tactic: refine IsColimit.equivOfNatIsoOfIso ?_ _ _ ?_ (BinaryBiproduct.isColimit (F.obj d) (G.obj d))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono (goal)
Goal:
K : Type u
inst : Category.{v, u} K
C : Type u'
inst_1 : Category.{v', u'} C
D : Type u''
inst_2 : Category.{v'', u''} D
F G : Functor.{v, v', u, u'} K C
f : F ⟶ G
inst_3 : HasPullbacks.{v', u'} C
inst_4 : Mono f
H : Functor.{v', v'', u', u''} C D
inst_5 : H.PreservesMonomorphisms
X : K
⊢ Mono ((whiskerRight f H).app X)
have dsimp : Mono (H.map (f.app X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono (hypothesis)
Goal:
K : Type u
inst : Category.{v, u} K
C : Type u'
inst_1 : Category.{v', u'} C
D : Type u''
inst_2 : Category.{v'', u''} D
F G : Functor.{v, v', u, u'} K C
f : F ⟶ G
inst_3 : HasPullbacks.{v', u'} C
inst_4 : Mono f
H : Functor.{v', v'', u', u''} C D
inst_5 : H.PreservesMonomorphisms
⊢ Mono (whiskerRight f H)
have this : ∀ (X : K), Mono ((whiskerRight f H).app X)
Tactic: have : ∀ X, Mono ((whiskerRight f H).app X) := by intros; dsimp; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono (goal)
Goal:
K : Type u
inst : Category.{v, u} K
C : Type u'
inst_1 : Category.{v', u'} C
D : Type u''
inst_2 : Category.{v'', u''} D
F G : Functor.{v, v', u, u'} K C
f : F ⟶ G
inst_3 : HasPushouts.{v', u'} C
inst_4 : Epi f
H : Functor.{v', v'', u', u''} C D
inst_5 : H.PreservesEpimorphisms
X : K
⊢ Epi ((whiskerRight f H).app X)
have dsimp : Epi (H.map (f.app X))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono (hypothesis)
Goal:
K : Type u
inst : Category.{v, u} K
C : Type u'
inst_1 : Category.{v', u'} C
D : Type u''
inst_2 : Category.{v'', u''} D
F G : Functor.{v, v', u, u'} K C
f : F ⟶ G
inst_3 : HasPushouts.{v', u'} C
inst_4 : Epi f
H : Functor.{v', v'', u', u''} C D
inst_5 : H.PreservesEpimorphisms
⊢ Epi (whiskerRight f H)
have this : ∀ (X : K), Epi ((whiskerRight f H).app X)
Tactic: have : ∀ X, Epi ((whiskerRight f H).app X) := by intros; dsimp; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images (goal)
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 Y : C
g : X ⟶ Y
⊢ ((monoFactorisation f).I.map g ≫
      ↾fun (x : (monoFactorisation f).I.obj Y) ↦
        match (motive := (monoFactorisation f).I.obj Y → H.I.obj Y) x with
        | ⟨x, hx⟩ =>
          (ConcreteCategory.hom (FC := TypeCat.Fun) (H.e.app Y) :
              (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (H.I.obj Y))
            (Exists.choose (p := fun (y : F.obj Y) ↦
              (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
                    (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (G.obj Y))
                  y =
                x)
              hx)) =
    (↾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)) ≫
      H.I.map g
have h : ∀ (x : (monoFactorisation f).I.obj X),
  TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((monoFactorisation f).I.map g ≫
          ↾fun (x : (monoFactorisation f).I.obj Y) ↦
            match (motive := (monoFactorisation f).I.obj Y → H.I.obj Y) x with
            | ⟨x, hx⟩ =>
              (ConcreteCategory.hom (FC := TypeCat.Fun) (H.e.app Y) :
                  (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (H.I.obj Y))
                (Exists.choose (p := fun (y : F.obj Y) ↦
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
                        (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (G.obj Y))
                      y =
                    x)
                  hx)))
      x =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        ((↾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)) ≫
          H.I.map g))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images (goal)
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 Y : C
g : X ⟶ Y
x : (monoFactorisation f).I.obj X
⊢ Eq (α := (fun (X : Type u) ↦ X) (G.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.m.app Y) :
          (a : (fun (X : Type u) ↦ X) (H.I.obj Y)) → (fun (X : Type u) ↦ X) (G.obj Y))
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((monoFactorisation f).I.map g ≫
              ↾fun (x : (monoFactorisation f).I.obj Y) ↦
                match (motive := (monoFactorisation f).I.obj Y → H.I.obj Y) x with
                | ⟨x, hx⟩ =>
                  (ConcreteCategory.hom (FC := TypeCat.Fun) (H.e.app Y) :
                      (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (H.I.obj Y))
                    (Exists.choose (p := fun (y : F.obj Y) ↦
                      (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) :
                            (a : (fun (X : Type u) ↦ X) (F.obj Y)) → (fun (X : Type u) ↦ X) (G.obj Y))
                          y =
                        x)
                      hx)))
          x) :
      (fun (X : Type u) ↦ X) (G.obj Y))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (H.m.app Y) :
          (a : (fun (X : Type u) ↦ X) (H.I.obj Y)) → (fun (X : Type u) ↦ X) (G.obj Y))
        (TypeCat.Fun.toFun
          (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((↾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)) ≫
              H.I.map g))
          x) :
      (fun (X : Type u) ↦ X) (G.obj Y))
have h : Eq (α := G.obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) : (a : F.obj Y) → G.obj Y)
      (Exists.choose (p := fun (y : F.obj Y) ↦
        Eq (α := G.obj Y) ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app Y) : (a : F.obj Y) → G.obj Y) y : G.obj Y)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map g) : (a : G.obj X) → G.obj Y) (↑x : G.obj X) : G.obj Y))
        sorry) :
    G.obj Y)
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (G.map g) : (a : G.obj X) → G.obj Y)
      ((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 : G.obj X)) sorry) :
        G.obj X) :
    G.obj Y)
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images (goal)
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
⊢ {
        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
have 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 := sorry : 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: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Images (goal)
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
⊢ 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
have 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)) sorry) =
  (↑x_1 : G.obj x)
Tactic: simp