awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyReflectIsomorphisms (D := D) F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Epi ((F i).map f)
inst_2 : ∀ (i : I), PreservesColimit (span f f) (F i)
inst_3 : HasPushout f f
hc : IsColimit (PushoutCocone.mk (W := pushout f f) (pushout.inl f f) (pushout.inr f f) ⋯)
i : I
⊢ IsIso ((F i).map (PushoutCocone.mk (W := pushout f f) (pushout.inl f f) (pushout.inr f f) ⋯).inl)

Tactic:
(epi_iff_isIso_inl ((isColimitMapCoconePushoutCoconeEquiv (F i) pushout.condition).1
    (isColimitOfPreserves (F i) hc))).1 (hf i)

Premises used: CategoryTheory.Limits.pushout.condition, Equiv.toFun, CategoryTheory.Limits.colimit, Iff.mp, CategoryTheory.epi_iff_isIso_inl, CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyReflectIsomorphisms (D := D) F
X Y : C
f : X ⟶ Y
hf : ∀ (i : I), Epi ((F i).map f)
inst_2 : ∀ (i : I), PreservesColimit (span f f) (F i)
inst_3 : HasPushout f f
hc : IsColimit (PushoutCocone.mk (W := pushout f f) (pushout.inl f f) (pushout.inr f f) ⋯)
i : I
⊢ IsIso ((F i).map (PushoutCocone.mk (W := pushout f f) (pushout.inl f f) (pushout.inr f f) ⋯).inl)

Tactic:
exact (epi_iff_isIso_inl ((isColimitMapCoconePushoutCoconeEquiv (F i) pushout.condition).1
    (isColimitOfPreserves (F i) hc))).1 (hf i)

Premises used: CategoryTheory.Limits.pushout.condition, Equiv.toFun, Iff.mp, CategoryTheory.epi_iff_isIso_inl, CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyReflectIsomorphisms (D := D) F
inst_2 : ∀ (i : I), PreservesLimitsOfShape WalkingParallelPair (F i)
inst_3 : HasEqualizers.{u_4, u_1} C
⊢ JointlyFaithful (D := D) F

Tactic:
.of_jointly_reflects_isIso_of_mono (fun _ _ _ _ _ ↦ h.isIso _)

Premises used: CategoryTheory.JointlyFaithful.of_jointly_reflects_isIso_of_mono, CategoryTheory.JointlyReflectIsomorphisms.isIso
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyReflectMonomorphisms (D := D) F
inst_2 : ∀ (i : I), (F i).PreservesMonomorphisms
X Y : C
f : X ⟶ Y
⊢ Mono f ↔ ∀ (i : I), Mono ((F i).map f)

Tactic:
⟨fun _ _ ↦ inferInstance, fun _ ↦ h.mono f⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.JointlyReflectMonomorphisms.mono
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyReflectEpimorphisms (D := D) F
inst_2 : ∀ (i : I), (F i).PreservesEpimorphisms
X Y : C
f : X ⟶ Y
⊢ Epi f ↔ ∀ (i : I), Epi ((F i).map f)

Tactic:
⟨fun _ _ ↦ inferInstance, fun _ ↦ h.epi f⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.JointlyReflectEpimorphisms.epi
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyFaithful (D := D) F
X Y : C
f : X ⟶ Y
h_1 : ∀ (i : I), Mono ((F i).map f)
Z : C
g₁ g₂ : Z ⟶ X
hg : g₁ ≫ f = g₂ ≫ f
i : I
⊢ (F i).map g₁ = (F i).map g₂

Tactic:
simp only [← cancel_mono ((F i).map f), ← Functor.map_comp, hg]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
Goal:
C : Type u_1
inst : Category.{u_4, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_5, u_3} (D i)
F : (i : I) → Functor.{u_4, u_5, u_1, u_3} C (D i)
h : JointlyFaithful (D := D) F
X Y : C
f : X ⟶ Y
h_1 : ∀ (i : I), Epi ((F i).map f)
Z : C
g₁ g₂ : Y ⟶ Z
hg : f ≫ g₁ = f ≫ g₂
i : I
⊢ (F i).map g₁ = (F i).map g₂

Tactic:
simp only [← cancel_epi ((F i).map f), ← Functor.map_comp, hg]

Premises used: CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst_3 : HasLimit G
inst_4 : ∀ (i : I), PreservesLimit G (F i)
suffices : IsIso (Y := limit G) (limit.lift G c)
⊢ IsLimit c

Tactic:
suffices IsIso (limit.lift _ c) from
    IsLimit.ofIsoLimit (limit.isLimit _)
      (Cone.ext (asIso (limit.lift _ c) :)).symm
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst_3 : HasLimit G
inst_4 : ∀ (i : I), PreservesLimit G (F i)
rw : ∀ (i : I), IsIso (Y := (F i).obj (limit G)) ((F i).map (limit.lift G c))
⊢ IsIso (Y := limit G) (limit.lift G c)

Tactic:
rw [hF.isIso_iff]

Premises used: CategoryTheory.JointlyReflectIsomorphisms.isIso_iff
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst_3 : HasLimit G
inst_4 : ∀ (i : I), PreservesLimit G (F i)
i : I
H : IsLimit ((F i).mapCone (limit.cone G)) := isLimitOfPreserves (F i) (limit.isLimit G)
e : ((F i).mapCone c).pt ≅ ((F i).mapCone (limit.cone G)).pt := (hc i).conePointUniqueUpToIso H
j : J
⊢ e.hom ≫ ((F i).mapCone (limit.cone G)).π.app j = (F i).map (limit.lift G c) ≫ ((F i).mapCone (limit.cone G)).π.app j

Tactic:
simpa [← Functor.map_comp] using
        IsLimit.conePointUniqueUpToIso_hom_comp (hc i) H j

Premises used: CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst_3 : HasLimit G
inst_4 : ∀ (i : I), PreservesLimit G (F i)
i : I
H : IsLimit ((F i).mapCone (limit.cone G)) := isLimitOfPreserves (F i) (limit.isLimit G)
e : ((F i).mapCone c).pt ≅ ((F i).mapCone (limit.cone G)).pt := (hc i).conePointUniqueUpToIso H
⊢ e.hom = (F i).map (limit.lift G c)

Tactic:
have : e.hom = (F i).map (limit.lift G c) :=
    H.hom_ext (fun j ↦ by
      simpa [← Functor.map_comp] using
        IsLimit.conePointUniqueUpToIso_hom_comp (hc i) H j)
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst_3 : HasLimit G
inst_4 : ∀ (i : I), PreservesLimit G (F i)
i : I
H : IsLimit ((F i).mapCone (limit.cone G)) := isLimitOfPreserves (F i) (limit.isLimit G)
e : ((F i).mapCone c).pt ≅ ((F i).mapCone (limit.cone G)).pt := (hc i).conePointUniqueUpToIso H
this : e.hom = (F i).map (limit.lift G c)
rw : IsIso e.hom
⊢ IsIso (Y := (F i).obj (limit G)) ((F i).map (limit.lift G c))

Tactic:
rw [← this]
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cone G
hc : (i : I) → IsLimit ((F i).mapCone c)
inst_3 : HasLimit G
inst_4 : ∀ (i : I), PreservesLimit G (F i)
i : I
H : IsLimit ((F i).mapCone (limit.cone G)) := isLimitOfPreserves (F i) (limit.isLimit G)
e : ((F i).mapCone c).pt ≅ ((F i).mapCone (limit.cone G)).pt := (hc i).conePointUniqueUpToIso H
this : e.hom = (F i).map (limit.lift G c)
⊢ IsIso e.hom

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst_3 : HasColimit G
inst_4 : ∀ (i : I), PreservesColimit G (F i)
suffices : IsIso (X := colimit G) (colimit.desc G c)
⊢ IsColimit c

Tactic:
suffices IsIso (colimit.desc _ c) from
    IsColimit.ofIsoColimit (colimit.isColimit _)
      (Cocone.ext (asIso (colimit.desc _ c) :))
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst_3 : HasColimit G
inst_4 : ∀ (i : I), PreservesColimit G (F i)
rw : ∀ (i : I), IsIso (X := (F i).obj (colimit G)) ((F i).map (colimit.desc G c))
⊢ IsIso (X := colimit G) (colimit.desc G c)

Tactic:
rw [hF.isIso_iff]

Premises used: CategoryTheory.JointlyReflectIsomorphisms.isIso_iff
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst_3 : HasColimit G
inst_4 : ∀ (i : I), PreservesColimit G (F i)
i : I
H : IsColimit ((F i).mapCocone (colimit.cocone G)) := isColimitOfPreserves (F i) (colimit.isColimit G)
e : ((F i).mapCocone (colimit.cocone G)).pt ≅ ((F i).mapCocone c).pt := H.coconePointUniqueUpToIso (hc i)
j : J
⊢ ((F i).mapCocone (colimit.cocone G)).ι.app j ≫ e.hom =
    ((F i).mapCocone (colimit.cocone G)).ι.app j ≫ (F i).map (colimit.desc G c)

Tactic:
simpa [← Functor.map_comp] using
        IsColimit.comp_coconePointUniqueUpToIso_hom H (hc i) j

Premises used: CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst_3 : HasColimit G
inst_4 : ∀ (i : I), PreservesColimit G (F i)
i : I
H : IsColimit ((F i).mapCocone (colimit.cocone G)) := isColimitOfPreserves (F i) (colimit.isColimit G)
e : ((F i).mapCocone (colimit.cocone G)).pt ≅ ((F i).mapCocone c).pt := H.coconePointUniqueUpToIso (hc i)
⊢ e.hom = (F i).map (colimit.desc G c)

Tactic:
have : e.hom = (F i).map (colimit.desc G c) :=
    H.hom_ext (fun j ↦ by
      simpa [← Functor.map_comp] using
        IsColimit.comp_coconePointUniqueUpToIso_hom H (hc i) j)
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst_3 : HasColimit G
inst_4 : ∀ (i : I), PreservesColimit G (F i)
i : I
H : IsColimit ((F i).mapCocone (colimit.cocone G)) := isColimitOfPreserves (F i) (colimit.isColimit G)
e : ((F i).mapCocone (colimit.cocone G)).pt ≅ ((F i).mapCocone c).pt := H.coconePointUniqueUpToIso (hc i)
this : e.hom = (F i).map (colimit.desc G c)
rw : IsIso e.hom
⊢ IsIso (X := (F i).obj (colimit G)) ((F i).map (colimit.desc G c))

Tactic:
rw [← this]
-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
Goal:
C : Type u_1
inst : Category.{u_5, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{u_6, u_3} (D i)
F : (i : I) → Functor.{u_5, u_6, u_1, u_3} C (D i)
hF : JointlyReflectIsomorphisms (D := D) F
J : Type u_4
inst_2 : Category.{v_1, u_4} J
G : Functor.{v_1, u_5, u_4, u_1} J C
c : Cocone G
hc : (i : I) → IsColimit ((F i).mapCocone c)
inst_3 : HasColimit G
inst_4 : ∀ (i : I), PreservesColimit G (F i)
i : I
H : IsColimit ((F i).mapCocone (colimit.cocone G)) := isColimitOfPreserves (F i) (colimit.isColimit G)
e : ((F i).mapCocone (colimit.cocone G)).pt ≅ ((F i).mapCocone c).pt := H.coconePointUniqueUpToIso (hc i)
this : e.hom = (F i).map (colimit.desc G c)
⊢ IsIso e.hom

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} D
inst_2 : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst_3 : HasPushouts.{u_3, u_2} D
inst_4 : IsRegularEpiCategory.{u_3, u_2} D
F G : Functor.{u_4, u_3, u_1, u_2} C D
f : F ⟶ G
inst_5 : Epi f
k : C
⊢ IsRegularEpi (f.app k)

Tactic:
have := IsRegularEpiCategory.regularEpiOfEpi (f.app k)
-- Module: Mathlib.CategoryTheory.Functor.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} D
inst_2 : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst_3 : HasPushouts.{u_3, u_2} D
inst_4 : IsRegularEpiCategory.{u_3, u_2} D
F G : Functor.{u_4, u_3, u_1, u_2} C D
f : F ⟶ G
inst_5 : Epi f
k : C
this : IsRegularEpi (f.app k)
refine_1 :
  parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd ≅
    parallelPair
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).fst
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).snd ⋙
      obj (evaluation C D) k
refine_2 :
  Iso (C :=
    Cocone
      (parallelPair
          (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
              pullback.isLimit (f.app k) (f.app k)).fst
          (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
              pullback.isLimit (f.app k) (f.app k)).snd ⋙
        obj (evaluation C D) k))
    (obj
      (Cocone.precompose
        (Iso.inv
          (NatIso.ofComponents
            (fun (X : WalkingParallelPair) ↦
              WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
                (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj x ≅
                  (parallelPair
                          (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                              pullback.isLimit (f.app k) (f.app k)).fst
                          (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                              pullback.isLimit (f.app k) (f.app k)).snd ⋙
                        obj (evaluation C D) k).obj
                    x)
                X
                (Iso.refl
                  ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
                    WalkingParallelPair.zero))
                (Iso.refl
                  ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
                    WalkingParallelPair.one)))
            ⋯)))
      (Cofork.ofπ (f.app k) ⋯))
    (mapCocone (obj (evaluation C D) k) (Cofork.ofπ f ⋯))
⊢ IsColimit (F :=
    parallelPair
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).fst
        (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
            pullback.isLimit (f.app k) (f.app k)).snd ⋙
      obj (evaluation C D) k)
    (mapCocone (obj (evaluation C D) k) (Cofork.ofπ f ⋯))

Tactic:
refine .equivOfNatIsoOfIso ?_ _ _ ?_ (isColimitCoforkOfEffectiveEpi (f.app k)
        (pullback.cone (f.app k) (f.app k))
        (pullback.isLimit (f.app k) (f.app k)))
-- Module: Mathlib.CategoryTheory.Functor.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} D
inst_2 : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst_3 : HasPushouts.{u_3, u_2} D
inst_4 : IsRegularEpiCategory.{u_3, u_2} D
F G : Functor.{u_4, u_3, u_1, u_2} C D
f : F ⟶ G
inst_5 : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
      WalkingParallelPair.zero ≅
    (parallelPair
            (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                pullback.isLimit (f.app k) (f.app k)).fst
            (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                pullback.isLimit (f.app k) (f.app k)).snd ⋙
          obj (evaluation C D) k).obj
      WalkingParallelPair.zero

Tactic:
exacts [Iso.refl _, Iso.refl _]

Premises used: CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Functor.RegularEpi
Goal:
C : Type u_1
D : Type u_2
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_3, u_2} D
inst_2 : ∀ {F G : D} (f : F ⟶ G) [Epi f], HasPullback f f
inst_3 : HasPushouts.{u_3, u_2} D
inst_4 : IsRegularEpiCategory.{u_3, u_2} D
F G : Functor.{u_4, u_3, u_1, u_2} C D
f : F ⟶ G
inst_5 : Epi f
k : C
this : IsRegularEpi (f.app k)
⊢ Iso (C :=
    Cocone
      (parallelPair
          (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
              pullback.isLimit (f.app k) (f.app k)).fst
          (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
              pullback.isLimit (f.app k) (f.app k)).snd ⋙
        obj (evaluation C D) k))
    (obj
      (Cocone.precompose
        (Iso.inv
          (NatIso.ofComponents
            (fun (X : WalkingParallelPair) ↦
              WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
                (parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj x ≅
                  (parallelPair
                          (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                              pullback.isLimit (f.app k) (f.app k)).fst
                          (PullbackCone.combine f f (fun (k : C) ↦ pullback.cone (f.app k) (f.app k)) fun (k : C) ↦
                              pullback.isLimit (f.app k) (f.app k)).snd ⋙
                        obj (evaluation C D) k).obj
                    x)
                X
                (Iso.refl
                  ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
                    WalkingParallelPair.zero))
                (Iso.refl
                  ((parallelPair (pullback.cone (f.app k) (f.app k)).fst (pullback.cone (f.app k) (f.app k)).snd).obj
                    WalkingParallelPair.one)))
            ⋯)))
      (Cofork.ofπ (f.app k) ⋯))
    (mapCocone (obj (evaluation C D) k) (Cofork.ofπ f ⋯))

Tactic:
exact Cocone.ext (Iso.refl _) <| by rintro (_ | _ | _); all_goals cat_disch

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Functor.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ Y₁ : C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
ψ : X₂ ⟶ Y₂
w :
  ∀ (X₃ : C₃),
    ((bifunctorComp₁₂Obj F₁₂ G X₁).map ψ ≫
            { app := fun (X₃ : C₃) ↦ (G.map ((F₁₂.map φ).app Y₂)).app X₃, naturality := ⋯ :
              NatTrans ((bifunctorComp₁₂Obj F₁₂ G X₁).obj Y₂) ((bifunctorComp₁₂Obj F₁₂ G Y₁).obj Y₂) }).app
        X₃ =
      NatTrans.app
        ({ app := fun (X₃ : C₃) ↦ (G.map ((F₁₂.map φ).app X₂)).app X₃, naturality := ⋯ :
            NatTrans ((bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂) ((bifunctorComp₁₂Obj F₁₂ G Y₁).obj X₂) } ≫
          (bifunctorComp₁₂Obj F₁₂ G Y₁).map ψ)
        X₃
⊢ (bifunctorComp₁₂Obj F₁₂ G X₁).map ψ ≫
      { app := fun (X₃ : C₃) ↦ (G.map ((F₁₂.map φ).app Y₂)).app X₃, naturality := ⋯ :
        NatTrans ((bifunctorComp₁₂Obj F₁₂ G X₁).obj Y₂) ((bifunctorComp₁₂Obj F₁₂ G Y₁).obj Y₂) } =
    { app := fun (X₃ : C₃) ↦ (G.map ((F₁₂.map φ).app X₂)).app X₃, naturality := ⋯ :
        NatTrans ((bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂) ((bifunctorComp₁₂Obj F₁₂ G Y₁).obj X₂) } ≫
      (bifunctorComp₁₂Obj F₁₂ G Y₁).map ψ

Tactic:
ext X₃
-- Module: Mathlib.CategoryTheory.Functor.Trifunctor
Goal:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} C₃
inst_3 : Category.{v_4, u_4} C₄
inst_4 : Category.{v_5, u_5} C₁₂
inst_5 : Category.{v_6, u_6} C₂₃
F₁₂ : C₁ ⥤ Functor.{v_2, v_5, u_2, u_5} C₂ C₁₂
G : C₁₂ ⥤ Functor.{v_3, v_4, u_3, u_4} C₃ C₄
X₁ Y₁ : C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
ψ : X₂ ⟶ Y₂
X₃ : C₃
w :
  (G.map ((F₁₂.obj X₁).map ψ)).app X₃ ≫ (G.map ((F₁₂.map φ).app Y₂)).app X₃ =
    (G.map ((F₁₂.map φ).app X₂)).app X₃ ≫ (G.map ((F₁₂.obj Y₁).map ψ)).app X₃
⊢ ((bifunctorComp₁₂Obj F₁₂ G X₁).map ψ ≫
          { app := fun (X₃ : C₃) ↦ (G.map ((F₁₂.map φ).app Y₂)).app X₃, naturality := ⋯ :
            NatTrans ((bifunctorComp₁₂Obj F₁₂ G X₁).obj Y₂) ((bifunctorComp₁₂Obj F₁₂ G Y₁).obj Y₂) }).app
      X₃ =
    NatTrans.app
      ({ app := fun (X₃ : C₃) ↦ (G.map ((F₁₂.map φ).app X₂)).app X₃, naturality := ⋯ :
          NatTrans ((bifunctorComp₁₂Obj F₁₂ G X₁).obj X₂) ((bifunctorComp₁₂Obj F₁₂ G Y₁).obj X₂) } ≫
        (bifunctorComp₁₂Obj F₁₂ G Y₁).map ψ)
      X₃

Tactic:
dsimp