awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
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))
⊢ 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:
apply colimit_obj_ext

Premises used: CategoryTheory.Limits.colimit_obj_ext
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
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
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:
simp [comp_evaluation, ← NatTrans.comp_app_assoc _ (colimMap _)]

Premises used: CategoryTheory.comp_evaluation, CategoryTheory.NatTrans.comp_app_assoc, CategoryTheory.Limits.colimMap
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
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
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))
⊢ IsLimit (F := pair F G ⋙ Functor.obj (evaluation D C) 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))

Premises used: CategoryTheory.Limits.BinaryBiproduct.isLimit, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
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
⊢ pair (F.obj d) (G.obj d) ≅ pair F G ⋙ Functor.obj (evaluation D C) d

Tactic:
exact (pairComp F G ((evaluation D C).obj d)).symm

Premises used: CategoryTheory.Limits.pairComp, CategoryTheory.Iso.symm, CategoryTheory.evaluation, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
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
⊢ (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:
exact Cone.ext (Iso.refl _) <| by rintro (_ | _ | _) <;> cat_disch

Premises used: CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.ext
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
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
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))
⊢ IsColimit (F := pair F G ⋙ Functor.obj (evaluation D C) 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))

Premises used: CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso, CategoryTheory.Limits.BinaryBiproduct.isColimit, DFunLike.coe, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
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
⊢ (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:
exact Cocone.ext (Iso.refl _) <| by rintro (_ | _ | _) <;> cat_disch

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
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
k : K
⊢ Mono (f.app k)

Tactic:
inferInstanceAs (Mono (((evaluation K C).obj k).map f))

Premises used: _private.0.CategoryTheory.instMonoAppOfFunctor._proof_1
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
Goal:
K : Type u
inst : Category.{v, u} K
C : Type u'
inst_1 : Category.{v', u'} C
F G : Functor.{v, v', u, u'} K C
f : F ⟶ G
inst_2 : HasPullbacks.{v', u'} C
⊢ Mono f ↔ ∀ (k : K), Mono (f.app k)

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ mono_of_mono_app _⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.NatTrans.mono_of_mono_app
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
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
dsimp : Mono (H.map (f.app X))
⊢ Mono ((whiskerRight f H).app X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
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 (H.map (f.app X))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
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)

Tactic:
have : ∀ X, Mono ((whiskerRight f H).app X) := by intros; dsimp; infer_instance
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
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
this : ∀ (X : K), Mono ((whiskerRight f H).app X)
⊢ Mono (whiskerRight f H)

Tactic:
apply NatTrans.mono_of_mono_app

Premises used: CategoryTheory.NatTrans.mono_of_mono_app
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
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_1 G : Functor.{v, v', u, u'} K C
f_1 : F_1 ⟶ G
inst_3 : HasPullbacks.{v', u'} C
F : Functor.{v', v'', u', u''} C D
inst_4 : F.PreservesMonomorphisms
X Y : Functor.{v, v', u, u'} K C
f : X ⟶ Y
h : Mono f
⊢ Mono (whiskerRight f F)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
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
k : K
⊢ Epi (f.app k)

Tactic:
inferInstanceAs (Epi (((evaluation K C).obj k).map f))

Premises used: _private.0.CategoryTheory.instEpiAppOfFunctor._proof_1
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
Goal:
K : Type u
inst : Category.{v, u} K
C : Type u'
inst_1 : Category.{v', u'} C
F G : Functor.{v, v', u, u'} K C
f : F ⟶ G
inst_2 : HasPushouts.{v', u'} C
⊢ Epi f ↔ ∀ (k : K), Epi (f.app k)

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ epi_of_epi_app _⟩

Premises used: CategoryTheory.NatTrans.epi_of_epi_app, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
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
dsimp : Epi (H.map (f.app X))
⊢ Epi ((whiskerRight f H).app X)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
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 (H.map (f.app X))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
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)

Tactic:
have : ∀ X, Epi ((whiskerRight f H).app X) := by intros; dsimp; infer_instance
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
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
this : ∀ (X : K), Epi ((whiskerRight f H).app X)
⊢ Epi (whiskerRight f H)

Tactic:
apply NatTrans.epi_of_epi_app

Premises used: CategoryTheory.NatTrans.epi_of_epi_app
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Filtered
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
K : Type u₂
inst_1 : Category.{v₂, u₂} K
inst_2 : HasFilteredColimitsOfSize.{w', w, v₁, u₁} C
⊢ HasFilteredColimitsOfSize.{w', w, max u₂ v₁, max (max (max u₁ u₂) v₁) v₂} (Functor.{v₂, v₁, u₂, u₁} K C)

Tactic:
⟨fun _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFilteredColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Filtered
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
K : Type u₂
inst_1 : Category.{v₂, u₂} K
inst_2 : HasCofilteredLimitsOfSize.{w', w, v₁, u₁} C
⊢ HasCofilteredLimitsOfSize.{w', w, max u₂ v₁, max (max (max u₁ u₂) v₁) v₂} (Functor.{v₂, v₁, u₂, u₁} K C)

Tactic:
⟨fun _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasCofilteredLimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Finite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Type u_2
inst_1 : Category.{v_2, u_2} K
inst_2 : HasFiniteLimits.{v_1, u_1} C
⊢ HasFiniteLimits (Functor.{v_2, v_1, u_2, u_1} K C)

Tactic:
⟨fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteLimits.mk
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Finite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Type u_2
inst_1 : Category.{v_2, u_2} K
inst_2 : HasFiniteProducts.{v_1, u_1} C
⊢ HasFiniteProducts (Functor.{v_2, v_1, u_2, u_1} K C)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteProducts.mk
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Finite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Type u_2
inst_1 : Category.{v_2, u_2} K
inst_2 : HasFiniteColimits.{v_1, u_1} C
⊢ HasFiniteColimits (Functor.{v_2, v_1, u_2, u_1} K C)

Tactic:
⟨fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteColimits.mk
-- Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Finite
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
K : Type u_2
inst_1 : Category.{v_2, u_2} K
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
⊢ HasFiniteCoproducts (Functor.{v_2, v_1, u_2, u_1} K C)

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteCoproducts.mk
-- 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 Y : C
g : X ⟶ Y
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
⊢ ((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

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 Y : C
g : X ⟶ Y
x : (monoFactorisation f).I.obj X
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))
          ⋯) :
      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)) ⋯) :
          G.obj X) :
      G.obj Y)
⊢ 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))

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 Y : C
g : X ⟶ Y
x : (monoFactorisation f).I.obj X
⊢ 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))
          ⋯) :
      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)) ⋯) :
          G.obj X) :
      G.obj Y)

Tactic:
grind