awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K_1 : Functor.{w', v₁, w, u₁} J_1 C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cone K
t : IsLimit (F.mapCone c)
s : Cone K
m : s ⟶ c
rw : (Cone.functoriality K F).map m = t.liftConeMorphism ((Cone.functoriality K F).obj s)
⊢ (Cone.functoriality K F).map m =
    (Cone.functoriality K F).map
      ((Cone.functoriality K F).preimage (t.liftConeMorphism ((Cone.functoriality K F).obj s)))

Tactic:
rw [Functor.map_preimage]

Premises used: CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K_1 : Functor.{w', v₁, w, u₁} J_1 C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cone K
t : IsLimit (F.mapCone c)
s : Cone K
m : s ⟶ c
⊢ (Cone.functoriality K F).map m = t.liftConeMorphism ((Cone.functoriality K F).obj s)

Tactic:
apply t.uniq_cone_morphism

Premises used: CategoryTheory.Limits.IsLimit.uniq_cone_morphism
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K_1 : Functor.{w', v₁, w, u₁} J_1 C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cocone K
t : IsColimit (F.mapCocone c)
apply :
  ∀ (s : Cocone K) (m : c ⟶ s),
    (Cocone.functoriality K F).map m =
      (Cocone.functoriality K F).map
        ((Cocone.functoriality K F).preimage (t.descCoconeMorphism ((Cocone.functoriality K F).obj s)))
⊢ ∀ (s : Cocone K) (m : c ⟶ s),
    m = (Cocone.functoriality K F).preimage (t.descCoconeMorphism ((Cocone.functoriality K F).obj s))

Tactic:
apply fun s m => (Cocone.functoriality K F).map_injective _

Premises used: CategoryTheory.Limits.Cocone.functoriality, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K_1 : Functor.{w', v₁, w, u₁} J_1 C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cocone K
t : IsColimit (F.mapCocone c)
s : Cocone K
m : c ⟶ s
rw : (Cocone.functoriality K F).map m = t.descCoconeMorphism ((Cocone.functoriality K F).obj s)
⊢ (Cocone.functoriality K F).map m =
    (Cocone.functoriality K F).map
      ((Cocone.functoriality K F).preimage (t.descCoconeMorphism ((Cocone.functoriality K F).obj s)))

Tactic:
rw [Functor.map_preimage]

Premises used: CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K_1 : Functor.{w', v₁, w, u₁} J_1 C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cocone K
t : IsColimit (F.mapCocone c)
s : Cocone K
m : c ⟶ s
⊢ (Cocone.functoriality K F).map m = t.descCoconeMorphism ((Cocone.functoriality K F).obj s)

Tactic:
apply t.uniq_cocone_morphism

Premises used: CategoryTheory.Limits.IsColimit.uniq_cocone_morphism
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
c₁ : Cocone K₁
c₂ : Cocone K₂
j₁ : J₁
j₂ : J₂
k₁ : J₁
k₂ : J₂
f₁ : (j₁, j₂).1 ⟶ (k₁, k₂).1
f₂ : (j₁, j₂).2 ⟶ (k₁, k₂).2
dsimp :
  ((G.map (K₁.map f₁)).app (K₂.obj j₂) ≫ (G.obj (K₁.obj k₁)).map (K₂.map f₂)) ≫
      (G.map (c₁.ι.app k₁)).app (K₂.obj k₂) ≫ (G.obj c₁.pt).map (c₂.ι.app k₂) =
    ((G.map (c₁.ι.app j₁)).app (K₂.obj j₂) ≫ (G.obj c₁.pt).map (c₂.ι.app j₂)) ≫ 𝟙 ((G.obj c₁.pt).obj c₂.pt)
⊢ Eq (α :=
    (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj (j₁, j₂) ⟶
      obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) (k₁, k₂))
    ((obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).map (f₁, f₂) ≫
      match (motive :=
        (x : J₁ × J₂) →
          (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj x ⟶
            obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) x)
        (k₁, k₂) with
      | (j₁, j₂) =>
        (G.map (c₁.ι.app j₁)).app (K₂.obj (j₁, j₂).2) ≫
          (G.obj (obj.{v_1, v_3, u_1, u_3} (obj (const J₁) c₁.pt) j₁)).map (c₂.ι.app j₂))
    (CategoryStruct.comp (Y := obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) (j₁, j₂))
      (match (motive :=
        (x : J₁ × J₂) →
          (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj x ⟶
            obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) x)
        (j₁, j₂) with
      | (j₁, j₂) =>
        (G.map (c₁.ι.app j₁)).app (K₂.obj (j₁, j₂).2) ≫
          (G.obj (obj.{v_1, v_3, u_1, u_3} (obj (const J₁) c₁.pt) j₁)).map (c₂.ι.app j₂))
      (map (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) (f₁, f₂)))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
c₁ : Cocone K₁
c₂ : Cocone K₂
j₁ : J₁
j₂ : J₂
k₁ : J₁
k₂ : J₂
f₁ : (j₁, j₂).1 ⟶ (k₁, k₂).1
f₂ : (j₁, j₂).2 ⟶ (k₁, k₂).2
⊢ ((G.map (K₁.map f₁)).app (K₂.obj j₂) ≫ (G.obj (K₁.obj k₁)).map (K₂.map f₂)) ≫
      (G.map (c₁.ι.app k₁)).app (K₂.obj k₂) ≫ (G.obj c₁.pt).map (c₂.ι.app k₂) =
    ((G.map (c₁.ι.app j₁)).app (K₂.obj j₂) ≫ (G.obj c₁.pt).map (c₂.ι.app j₂)) ≫ 𝟙 ((G.obj c₁.pt).obj c₂.pt)

Tactic:
simp only [assoc, comp_id, NatTrans.naturality_assoc,
          ← Functor.map_comp, NatTrans.naturality, const_obj_map, const_obj_obj,
          ← NatTrans.comp_app_assoc, c₁.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.comp_app_assoc, CategoryTheory.Category.comp_id, CategoryTheory.Limits.Cocone.w, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.const_obj_obj, CategoryTheory.Functor.const_obj_map, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
c₁ : Cone K₁
c₂ : Cone K₂
j₁ : J₁
j₂ : J₂
k₁ : J₁
k₂ : J₂
f₁ : (j₁, j₂).1 ⟶ (k₁, k₂).1
f₂ : (j₁, j₂).2 ⟶ (k₁, k₂).2
dsimp :
  𝟙 ((G.obj c₁.pt).obj c₂.pt) ≫ (G.map (c₁.π.app k₁)).app c₂.pt ≫ (G.obj (K₁.obj k₁)).map (c₂.π.app k₂) =
    ((G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)) ≫
      (G.map (K₁.map f₁)).app (K₂.obj j₂) ≫ (G.obj (K₁.obj k₁)).map (K₂.map f₂)
⊢ Eq.{v_5 + 1} (α :=
    obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) (j₁, j₂) ⟶
      (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj (k₁, k₂))
    (CategoryStruct.comp (Y := obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) (k₁, k₂))
      (map (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) (f₁, f₂))
      (match (motive :=
        (x : J₁ × J₂) →
          obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) x ⟶
            (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj x)
        (k₁, k₂) with
      | (j₁, j₂) => (G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)))
    ((match (motive :=
        (x : J₁ × J₂) →
          obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) x ⟶
            (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj x)
        (j₁, j₂) with
      | (j₁, j₂) => (G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)) ≫
      (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).map (f₁, f₂))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
c₁ : Cone K₁
c₂ : Cone K₂
j₁ : J₁
j₂ : J₂
k₁ : J₁
k₂ : J₂
f₁ : (j₁, j₂).1 ⟶ (k₁, k₂).1
f₂ : (j₁, j₂).2 ⟶ (k₁, k₂).2
⊢ 𝟙 ((G.obj c₁.pt).obj c₂.pt) ≫ (G.map (c₁.π.app k₁)).app c₂.pt ≫ (G.obj (K₁.obj k₁)).map (c₂.π.app k₂) =
    ((G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)) ≫
      (G.map (K₁.map f₁)).app (K₂.obj j₂) ≫ (G.obj (K₁.obj k₁)).map (K₂.map f₂)

Tactic:
simp only [assoc, id_comp, NatTrans.naturality_assoc,
          ← Functor.map_comp,
          ← NatTrans.comp_app_assoc, c₁.w, c₂.w]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.NatTrans.comp_app_assoc, CategoryTheory.Limits.Cone.w, CategoryTheory.Functor.map_comp, CategoryTheory.NatTrans.naturality_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
c₃ : Cocone (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G))
hc₃ : IsColimit c₃
j : J₁ × J₂
dsimp :
  c₃.ι.app j ≫ ((isColimitOfPreserves₂ G hc₁ hc₂).coconePointUniqueUpToIso hc₃).inv =
    NatTrans.app (G.map (c₁.ι.app j.1)) (K₂.obj j.2) ≫ (G.obj c₁.pt).map (c₂.ι.app j.2)
⊢ c₃.ι.app j ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).inv =
    NatTrans.app (G.map (c₁.ι.app j.1)) (K₂.obj j.2) ≫ (G.obj c₁.pt).map (c₂.ι.app j.2)

Tactic:
dsimp [isoObjCoconePointsOfIsColimit, Functor.mapCocone₂]

Premises used: CategoryTheory.Limits.PreservesColimit₂.isoObjCoconePointsOfIsColimit, CategoryTheory.Functor.mapCocone₂
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
c₃ : Cocone (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G))
hc₃ : IsColimit c₃
j : J₁ × J₂
rw :
  NatTrans.app (G.map (c₁.ι.app j.1)) (K₂.obj j.2) ≫ (G.obj c₁.pt).map (c₂.ι.app j.2) =
    c₃.ι.app j ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).inv
⊢ NatTrans.app (G.map (c₁.ι.app j.1)) (K₂.obj j.2) ≫
      (G.obj c₁.pt).map (c₂.ι.app j.2) ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).hom =
    c₃.ι.app j

Tactic:
rw [← Category.assoc, ← Iso.eq_comp_inv]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
c₃ : Cocone (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G))
hc₃ : IsColimit c₃
j : J₁ × J₂
⊢ NatTrans.app (G.map (c₁.ι.app j.1)) (K₂.obj j.2) ≫ (G.obj c₁.pt).map (c₂.ι.app j.2) =
    c₃.ι.app j ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).inv

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
inst_6 : HasColimit K₁
inst_7 : HasColimit K₂
j : J₁ × J₂
⊢ Eq (α := (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj j ⟶ (G.obj (colimit K₁)).obj (colimit K₂))
    (CategoryStruct.comp (Y := colimit (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)))
      (colimit.ι (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)) j :
        (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj j ⟶
          colimit (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)))
      (Iso.hom (isoColimitUncurryWhiskeringLeft₂ K₁ K₂ G) :
        colimit (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)) ⟶ (G.obj (colimit K₁)).obj (colimit K₂)))
    (NatTrans.app (G.map (colimit.ι K₁ j.1)) (K₂.obj j.2) ≫ (G.obj (colimit K₁)).map (colimit.ι K₂ j.2))

Tactic:
ι_comp_isoObjConePointsOfIsColimit_inv G
    (colimit.isColimit _) (colimit.isColimit _) (colimit.isColimit _) j

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.Limits.PreservesColimit₂.ι_comp_isoObjConePointsOfIsColimit_inv, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
inst_6 : HasColimit K₁
inst_7 : HasColimit K₂
j : J₁ × J₂
⊢ Eq (α := (G.obj (K₁.obj j.1)).obj (K₂.obj j.2) ⟶ colimit (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)))
    (NatTrans.app (G.map (colimit.ι K₁ j.1)) (K₂.obj j.2) ≫
        CategoryStruct.comp (Y := (G.obj (colimit K₁)).obj (colimit K₂)) ((G.obj (colimit K₁)).map (colimit.ι K₂ j.2))
          (Iso.inv (isoColimitUncurryWhiskeringLeft₂ K₁ K₂ G)) :
      (G.obj (K₁.obj j.1)).obj (K₂.obj j.2) ⟶ colimit (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)))
    (colimit.ι (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)) j :
      (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj j ⟶
        colimit (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)))

Tactic:
map_ι_comp_isoObjConePointsOfIsColimit_hom G
    (colimit.isColimit _) (colimit.isColimit _) (colimit.isColimit _) j

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.PreservesColimit₂.map_ι_comp_isoObjConePointsOfIsColimit_hom, CategoryTheory.Limits.colimit, CategoryTheory.Limits.colimit.ι
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
inst_6 : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst_7 : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G) :=
  { obj := fun (j₁ : J₁) ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j' : J₁} (f : j ⟶ j') ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun (j : J₁) ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun (x : J₁) ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
dsimp :
  CategoryStruct.comp (Y := (G.obj c₁.pt).obj c₂.pt)
      (𝟙 ((G.obj (K₁.obj j₁)).obj c₂.pt) ≫
          (P j₁).desc
            { pt := (G.obj c₁.pt).obj c₂.pt,
              ι :=
                { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
                  naturality := ⋯ } } :
        (G.obj (K₁.obj j₁)).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt)
      (𝟙 ((G.obj c₁.pt).obj c₂.pt) : (G.obj c₁.pt).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt) =
    (G.map (c₁.ι.app j₁)).app c₂.pt
⊢ ((Cocone.precompose E₀.hom).obj (coconeOfCoconeUncurry P (G.mapCocone₂ c₁ c₂))).ι.app j₁ ≫
      Iso.hom (Iso.refl ((Cocone.precompose E₀.hom).obj (coconeOfCoconeUncurry P (G.mapCocone₂ c₁ c₂))).pt) =
    ((G.flip.obj c₂.pt).mapCocone c₁).ι.app j₁

Tactic:
dsimp [E₀, Q₀]
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
inst_6 : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst_7 : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G) :=
  { obj := fun (j₁ : J₁) ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j' : J₁} (f : j ⟶ j') ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun (j : J₁) ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun (x : J₁) ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
simp :
  Eq (α := (G.obj (K₁.obj j₁)).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt)
    ((P j₁).desc
        { pt := (G.obj c₁.pt).obj c₂.pt,
          ι :=
            { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
              naturality := ⋯ } } :
      ((G.obj (K₁.obj j₁)).mapCocone c₂).pt ⟶
        Cocone.pt.{v_2, v_5, u_2, u_5} (J := J₂) (F := (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G).obj j₁)
          { pt := (G.obj c₁.pt).obj c₂.pt,
            ι :=
              { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
                naturality := ⋯ } })
    ((G.map (c₁.ι.app j₁)).app c₂.pt)
⊢ CategoryStruct.comp (Y := (G.obj c₁.pt).obj c₂.pt)
      (𝟙 ((G.obj (K₁.obj j₁)).obj c₂.pt) ≫
          (P j₁).desc
            { pt := (G.obj c₁.pt).obj c₂.pt,
              ι :=
                { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
                  naturality := ⋯ } } :
        (G.obj (K₁.obj j₁)).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt)
      (𝟙 ((G.obj c₁.pt).obj c₂.pt) : (G.obj c₁.pt).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt) =
    (G.map (c₁.ι.app j₁)).app c₂.pt

Tactic:
simp only [id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
inst_6 : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst_7 : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G) :=
  { obj := fun (j₁ : J₁) ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j' : J₁} (f : j ⟶ j') ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun (j : J₁) ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun (x : J₁) ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
refine_2 :
  Eq (α := (G.obj (K₁.obj j₁)).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt)
    ((P j₁).desc
        { pt := (G.obj c₁.pt).obj c₂.pt,
          ι :=
            { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
              naturality := ⋯ } } :
      ((G.obj (K₁.obj j₁)).mapCocone c₂).pt ⟶
        Cocone.pt.{v_2, v_5, u_2, u_5} (J := J₂) (F := (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G).obj j₁)
          { pt := (G.obj c₁.pt).obj c₂.pt,
            ι :=
              { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
                naturality := ⋯ } })
    ((G.map (c₁.ι.app j₁)).app c₂.pt)
refine_1 : Cocone ((obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G).obj j₁)
⊢ Eq (α := (G.obj (K₁.obj j₁)).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt)
    ((P j₁).desc
        { pt := (G.obj c₁.pt).obj c₂.pt,
          ι :=
            { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
              naturality := ⋯ } } :
      ((G.obj (K₁.obj j₁)).mapCocone c₂).pt ⟶
        Cocone.pt.{v_2, v_5, u_2, u_5} (J := J₂) (F := (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G).obj j₁)
          { pt := (G.obj c₁.pt).obj c₂.pt,
            ι :=
              { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
                naturality := ⋯ } })
    ((G.map (c₁.ι.app j₁)).app c₂.pt)

Tactic:
let s : Cocone (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G |>.obj j₁) := ?_