awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
calc_1 calc_1₁ : Eq (α := G.obj X ⟶ G.obj Y) (G.map 0) (G.map 0)
⊢ Eq (α := G.obj X ⟶ G.obj Y) (G.map 0) (adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0)

Tactic:
rw [Adjunction.right_triangle_components_assoc]

Premises used: CategoryTheory.Adjunction.right_triangle_components_assoc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ Eq (α := obj.{v₂, v₂, u₂, u₂} (𝟭 D) (G.obj X) ⟶ G.obj Y) (adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0)
    (adj.unit.app (G.obj X) ≫
      CategoryStruct.comp (Y := G.obj (G.leftAdjoint.obj (G.obj X))) (G.map (G.leftAdjoint.map 0)) (G.map 0))

Tactic:
simp only [← G.map_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : G.IsRightAdjoint
X Y : C
adj : G.leftAdjoint ⊣ G := Adjunction.ofIsRightAdjoint G
⊢ Eq (α := obj.{v₂, v₂, u₂, u₂} (𝟭 D) (G.obj X) ⟶ G.obj Y)
    (adj.unit.app (G.obj X) ≫
      CategoryStruct.comp (Y := G.obj (G.leftAdjoint.obj (G.obj X))) (G.map (G.leftAdjoint.map 0)) (G.map 0))
    0

Tactic:
simp only [id_obj, comp_obj, Adjunction.unit_naturality_assoc, zero_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Functor.id_obj, CategoryTheory.Limits.zero_comp, CategoryTheory.Adjunction.unit_naturality_assoc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Full
X Y : C
rw rw₁ : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0)
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map (CategoryStruct.comp (Y := Y) 0 (F.preimage 0)))

Tactic:
rw [zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.Full
X Y : C
rw : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj Y) (F.map 0) (F.map (F.preimage 0))) 0
rw₁ : Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj Y) (F.map 0) 0) 0
rw₂ rw₃ : Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj Y) 0 0
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map (CategoryStruct.comp (Y := Y) 0 (F.preimage 0))) 0

Tactic:
rw [F.map_comp, F.map_preimage, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_comp, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : HasZeroMorphisms.{v₁, u₁} C
inst_4 : HasZeroMorphisms.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_6 : F.PreservesZeroMorphisms
inst_7 : G.PreservesZeroMorphisms
⊢ ∀ (X Y : C), Eq (α := (F ⋙ G).obj X ⟶ (F ⋙ G).obj Y) ((F ⋙ G).map 0) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F₁ F₂ : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F₁.PreservesZeroMorphisms
e : F₁ ≅ F₂
X Y : C
⊢ Eq (α := F₂.obj X ⟶ F₂.obj Y) (F₂.map 0) 0

Tactic:
simp only [← cancel_epi (e.hom.app X), ← e.hom.naturality,
    F₁.map_zero, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, CategoryTheory.NatTrans.naturality, CategoryTheory.Limits.zero_comp, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.NatTrans.app
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
hF : F.FullyFaithful
⊢ F.PreservesZeroMorphisms

Tactic:
letI : HasZeroMorphisms C := hF.hasZeroMorphisms
  ⟨fun _ _ ↦ hF.map_preimage _⟩

Premises used: CategoryTheory.Functor.PreservesZeroMorphisms.mk, CategoryTheory.Functor.FullyFaithful.map_preimage, OfNat.ofNat
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : HasZeroObject.{v₁, u₁} C
inst_4 : HasZeroObject.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₁, u₁} C
inst_6 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.PreservesZeroMorphisms
rw : Eq (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (F.map (𝟙 0))
rw₁ : Eq (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (F.map 0)
rw₂ : Eq.{v₂ + 1} (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) 0
rw₃ rw₄ : Eq.{v₂ + 1} (α := F.obj 0 ⟶ F.obj 0) 0 0
⊢ Eq.{v₂ + 1} (α := F.obj 0 ⟶ F.obj 0) (CategoryStruct.comp (Y := 0) 0 0) (𝟙 (F.obj 0))

Tactic:
rw [← F.map_id, id_zero, F.map_zero, zero_comp]

Premises used: CategoryTheory.Functor.map_zero, CategoryTheory.Limits.id_zero, CategoryTheory.Functor.map_id, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : HasZeroObject.{v₁, u₁} C
inst_4 : HasZeroObject.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₁, u₁} C
inst_6 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : F.PreservesZeroMorphisms
rw : Eq.{v₂ + 1} (α := Quiver.Hom.{v₂, u₂} (V := D) 0 0) (CategoryStruct.comp (Y := F.obj 0) 0 0) 0
rw₁ rw₂ : Eq.{v₂ + 1} (α := Quiver.Hom.{v₂, u₂} (V := D) 0 0) 0 0
⊢ Eq.{v₂ + 1} (α := Quiver.Hom.{v₂, u₂} (V := D) 0 0) (CategoryStruct.comp (Y := F.obj 0) 0 0) (𝟙 0)

Tactic:
rw [id_zero, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.id_zero
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₁, u₁} C
inst_3 : HasZeroObject.{v₂, u₂} D
inst_4 : HasZeroMorphisms.{v₁, u₁} C
inst_5 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
i : F.obj 0 ≅ 0
X Y : C
rw : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map (CategoryStruct.comp (Y := 0) 0 0))
rw₁ rw₂ : Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (F.map 0)
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map 0))

Tactic:
rw [← Functor.map_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₁, u₁} C
inst_3 : HasZeroObject.{v₂, u₂} D
inst_4 : HasZeroMorphisms.{v₁, u₁} C
inst_5 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
i : F.obj 0 ≅ 0
X Y : C
rw :
  Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map 0)) (F.map 0 ≫ 𝟙 (F.obj 0) ≫ F.map 0)
rw₁ rw₂ :
  Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map 0))
    (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map 0))
⊢ Eq (α := F.obj X ⟶ F.obj Y) (CategoryStruct.comp (Y := F.obj 0) (F.map 0) (F.map 0))
    (F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0)

Tactic:
rw [Iso.hom_inv_id, Category.id_comp]

Premises used: CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₁, u₁} C
inst_3 : HasZeroObject.{v₂, u₂} D
inst_4 : HasZeroMorphisms.{v₁, u₁} C
inst_5 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
i : F.obj 0 ≅ 0
X Y : C
⊢ Eq (α := F.obj X ⟶ F.obj Y) (F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0) 0

Tactic:
simp only [zero_of_to_zero i.hom, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_of_to_zero, CategoryTheory.Limits.zero_comp, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : HasZeroObject.{v₁, u₁} C
inst_4 : HasZeroObject.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₁, u₁} C
inst_6 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : PreservesColimit (empty C) F
⊢ F.PreservesZeroMorphisms

Tactic:
preservesZeroMorphisms_of_map_zero_object <|
    F.mapIso HasZeroObject.zeroIsoInitial ≪≫
      PreservesInitial.iso F ≪≫ HasZeroObject.zeroIsoInitial.symm

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsoInitial, CategoryTheory.Functor.preservesZeroMorphisms_of_map_zero_object, CategoryTheory.Limits.PreservesInitial.iso, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
inst_3 : HasZeroObject.{v₁, u₁} C
inst_4 : HasZeroObject.{v₂, u₂} D
inst_5 : HasZeroMorphisms.{v₁, u₁} C
inst_6 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_7 : PreservesLimit (empty C) F
⊢ F.PreservesZeroMorphisms

Tactic:
preservesZeroMorphisms_of_map_zero_object <|
    F.mapIso HasZeroObject.zeroIsoTerminal ≪≫
      PreservesTerminal.iso F ≪≫ HasZeroObject.zeroIsoTerminal.symm

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal, CategoryTheory.Functor.preservesZeroMorphisms_of_map_zero_object, CategoryTheory.Limits.PreservesTerminal.iso, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₁, u₁} C
inst_3 : HasZeroObject.{v₂, u₂} D
inst_4 : HasZeroMorphisms.{v₁, u₁} C
inst_5 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.PreservesZeroMorphisms
⊢ PreservesLimit (empty C) F

Tactic:
preservesTerminal_of_iso F <|
    F.mapIso HasZeroObject.zeroIsoTerminal.symm ≪≫ mapZeroObject F ≪≫ HasZeroObject.zeroIsoTerminal

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsoTerminal, CategoryTheory.Limits.preservesTerminal_of_iso, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapZeroObject, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₁, u₁} C
inst_3 : HasZeroObject.{v₂, u₂} D
inst_4 : HasZeroMorphisms.{v₁, u₁} C
inst_5 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.PreservesZeroMorphisms
⊢ PreservesColimit (empty C) F

Tactic:
preservesInitial_of_iso F <|
    HasZeroObject.zeroIsoInitial.symm ≪≫
      (mapZeroObject F).symm ≪≫ (F.mapIso HasZeroObject.zeroIsoInitial.symm).symm

Premises used: CategoryTheory.Limits.HasZeroObject.zeroIsoInitial, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapZeroObject, CategoryTheory.Limits.preservesInitial_of_iso, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : IsZero G
J : Type u_1
inst_4 : Category.{v_1, u_1} J
K : Functor.{v_1, v₁, u_1, u₁} J C
c : Cone K
x : IsLimit c
rw :
  (hG : ∀ (X : C), IsZero.{v₂, u₂} (G.obj X)) →
    (J : Type u_1) →
      [inst_5 : Category.{v_1, u_1} J] →
        {K : Functor.{v_1, v₁, u_1, u₁} J C} → {c : Cone K} → IsLimit c → IsLimit (G.mapCone c)
⊢ IsLimit (G.mapCone c)

Tactic:
rw [Functor.isZero_iff] at hG

Premises used: CategoryTheory.Functor.isZero_iff
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : ∀ (X : C), IsZero.{v₂, u₂} (G.obj X)
J : Type u_1
inst_4 : Category.{v_1, u_1} J
K : Functor.{v_1, v₁, u_1, u₁} J C
c : Cone K
x : IsLimit c
⊢ IsLimit (G.mapCone c)

Tactic:
exact IsLimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)

Premises used: CategoryTheory.Functor.isZero, CategoryTheory.Functor.comp, CategoryTheory.Limits.IsLimit.ofIsZero, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : IsZero G
J : Type u_1
inst_4 : Category.{v_1, u_1} J
K : Functor.{v_1, v₁, u_1, u₁} J C
c : Cocone K
x : IsColimit c
rw :
  (hG : ∀ (X : C), IsZero.{v₂, u₂} (G.obj X)) →
    (J : Type u_1) →
      [inst_5 : Category.{v_1, u_1} J] →
        {K : Functor.{v_1, v₁, u_1, u₁} J C} → {c : Cocone K} → IsColimit c → IsColimit (G.mapCocone c)
⊢ IsColimit (G.mapCocone c)

Tactic:
rw [Functor.isZero_iff] at hG

Premises used: CategoryTheory.Functor.isZero_iff
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroObject.{v₂, u₂} D
inst_3 : HasZeroMorphisms.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
hG : ∀ (X : C), IsZero.{v₂, u₂} (G.obj X)
J : Type u_1
inst_4 : Category.{v_1, u_1} J
K : Functor.{v_1, v₁, u_1, u₁} J C
c : Cocone K
x : IsColimit c
⊢ IsColimit (G.mapCocone c)

Tactic:
exact IsColimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)

Premises used: CategoryTheory.Functor.isZero, CategoryTheory.Functor.comp, CategoryTheory.Limits.IsColimit.ofIsZero, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc : IsColimit c
⊢ Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)

Tactic:
replace hc := (Types.isColimit_iff_coconeTypesIsColimit ..).1 ⟨hc⟩
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc :
  Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)
j j' : J
g : j ⟶ j'
h :
  ∀ (x_1 : (fun (X : Type w) ↦ X) (K.obj j)),
    ((fun (k : K.obj j') ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j') ↦ R) k ≫ s.ι.app j') ∘
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (K.map g)) :
            (a : (fun (X : Type w) ↦ X) (K.obj j)) → (fun (X : Type w) ↦ X) (K.obj j')))
        x_1 =
      Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) x_1 ≫ s.ι.app j
⊢ Eq (α := K.obj j → (R ⟶ s.pt))
    ((fun (k : K.obj j') ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j') ↦ R) k ≫ s.ι.app j') ∘
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (K.map g)) :
        (a : (fun (X : Type w) ↦ X) (K.obj j)) → (fun (X : Type w) ↦ X) (K.obj j')))
    fun (k : K.obj j) ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc :
  Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)
j j' : J
g : j ⟶ j'
x_1 : (fun (X : Type w) ↦ X) (K.obj j)
⊢ ((fun (k : K.obj j') ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j') ↦ R) k ≫ s.ι.app j') ∘
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (K.map g)) :
          (a : (fun (X : Type w) ↦ X) (K.obj j)) → (fun (X : Type w) ↦ X) (K.obj j')))
      x_1 =
    Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) x_1 ≫ s.ι.app j

Tactic:
simp [← s.w g]

Premises used: CategoryTheory.Limits.Cocone.w
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc :
  Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
coconeTypes : (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) → Functor.CoconeTypes.{v, w, v', u'} K :=
  fun (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) ↦
    { pt := R ⟶ s.pt, ι := fun (j : J) (k : K.obj j) ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j,
      ι_naturality := ⋯ }
s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)
j : J
dsimp :
  CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : c.pt) ↦ R)
      (Sigma.map' (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : K.obj j) → c.pt) fun (x : K.obj j) ↦
        𝟙 R)
      (Sigma.desc (hc.desc (coconeTypes s))) =
    s.ι.app j
⊢ CategoryStruct.comp (Y :=
      Functor.obj.{v', v, u', u}
        (Functor.obj (Functor.const J)
          (Cocone.pt.{v', v, u', u} (F := K ⋙ Functor.obj sigmaConst R)
            (Functor.mapCocone (Functor.obj sigmaConst R) c)))
        j)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj sigmaConst R) c)) j)
      (Sigma.desc (hc.desc (coconeTypes s))) =
    s.ι.app j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc :
  Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
coconeTypes : (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) → Functor.CoconeTypes.{v, w, v', u'} K :=
  fun (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) ↦
    { pt := R ⟶ s.pt, ι := fun (j : J) (k : K.obj j) ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j,
      ι_naturality := ⋯ }
s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)
j : J
h :
  ∀ (k : K.obj j),
    CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : K.obj j) ↦ R)
        (Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k)
        (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : c.pt) ↦ R)
          (Sigma.map' (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : K.obj j) → c.pt)
            fun (x : K.obj j) ↦ 𝟙 R)
          (Sigma.desc (hc.desc (coconeTypes s)))) =
      Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j
⊢ CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : c.pt) ↦ R)
      (Sigma.map' (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : K.obj j) → c.pt) fun (x : K.obj j) ↦
        𝟙 R)
      (Sigma.desc (hc.desc (coconeTypes s))) =
    s.ι.app j

Tactic:
ext k
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc :
  Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
coconeTypes : (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) → Functor.CoconeTypes.{v, w, v', u'} K :=
  fun (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) ↦
    { pt := R ⟶ s.pt, ι := fun (j : J) (k : K.obj j) ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j,
      ι_naturality := ⋯ }
s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)
j : J
k : K.obj j
⊢ CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : K.obj j) ↦ R)
      (Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k)
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : c.pt) ↦ R)
        (Sigma.map' (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (c.ι.app j)) : (a : K.obj j) → c.pt) fun (x : K.obj j) ↦
          𝟙 R)
        (Sigma.desc (hc.desc (coconeTypes s)))) =
    Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j

Tactic:
simp [dsimp% hc.fac_apply, dsimp% Sigma.ι_desc (hc.desc (coconeTypes s)), coconeTypes]

Premises used: CategoryTheory.Limits.Sigma.ι_desc, CategoryTheory.Functor.CoconeTypes.IsColimit.fac_apply, CategoryTheory.Functor.CoconeTypes.IsColimit.desc
-- Module: Mathlib.CategoryTheory.Limits.Preserves.SigmaConst
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
R : C
J : Type u'
x : Category.{v', u'} J
K : Functor.{v', w, u', w + 1} J (Type w)
c : Cocone K
hc :
  Functor.CoconeTypes.IsColimit.{w, w, v', u'} (J := J) (F := K)
    ((K.coconeTypesEquiv.symm : (a : Cocone K) → K.CoconeTypes) c)
coconeTypes : (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) → Functor.CoconeTypes.{v, w, v', u'} K :=
  fun (s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)) ↦
    { pt := R ⟶ s.pt, ι := fun (j : J) (k : K.obj j) ↦ Sigma.ι.{w, v, u} (C := C) (fun (x : K.obj j) ↦ R) k ≫ s.ι.app j,
      ι_naturality := ⋯ }
s : Cocone.{v', v, u', u} (K ⋙ Functor.obj sigmaConst R)
m : Cocone.pt.{v', v, u', u} (F := K ⋙ Functor.obj sigmaConst R) (Functor.mapCocone (Functor.obj sigmaConst R) c) ⟶ s.pt
hm : ∀ (j : J), NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj sigmaConst R) c)) j ≫ m = s.ι.app j
dsimp : m = Sigma.desc (hc.desc (coconeTypes s))
⊢ m = Sigma.desc (hc.desc (coconeTypes s))

Tactic:
dsimp