awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y Z : C
ι₁ : X ⟶ Z
ι₂ : Y ⟶ Z
inst_5 : PreservesColimit (parallelPair ι₂ 0) F
i : IsColimit (BinaryCofan.mk ι₁ ι₂)
bc : BinaryBicone.{v₁, u₁} X Y := BinaryBicone.ofColimitCocone i
⊢ PreservesColimit (parallelPair bc.inr 0) F

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X Y Z : C
ι₁ : X ⟶ Z
ι₂ : Y ⟶ Z
inst_5 : PreservesColimit (parallelPair ι₂ 0) F
i : IsColimit (BinaryCofan.mk ι₁ ι₂)
bc : BinaryBicone.{v₁, u₁} X Y := BinaryBicone.ofColimitCocone i
presf : PreservesColimit (parallelPair bc.inr 0) F := inst_5
hf : IsColimit bc.inrCokernelCofork := BinaryBicone.isColimitInrCokernelCofork i
⊢ IsColimit (F.mapCocone (BinaryCofan.mk ι₁ ι₂))

Tactic:
exact
    (isColimitMapCoconeBinaryCofanEquiv F ι₁ ι₂).invFun
      (BinaryBicone.isBilimitOfCokernelFst (F.mapBinaryBicone bc)
          (isColimitMapCoconeCoforkEquiv' F bc.inr_fst (isColimitOfPreserves F hf))).isColimit

Premises used: CategoryTheory.Functor.mapBinaryBicone, CategoryTheory.Limits.isColimitMapCoconeBinaryCofanEquiv, CategoryTheory.Limits.BinaryBicone.isBilimitOfCokernelFst, CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv', CategoryTheory.Limits.BinaryBicone.inr_fst, DFunLike.coe, Equiv.invFun, CategoryTheory.Limits.BinaryBicone.IsBilimit.isColimit, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this : PreservesBinaryBiproducts F := ⋯
⊢ F.Additive

Tactic:
haveI := additive_of_preservesBinaryBiproducts F
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
preserves : ∀ {c : Cocone (parallelPair f g)} (hc : IsColimit c), Nonempty (IsColimit (F.mapCocone c))
⊢ PreservesColimit (parallelPair f g) F

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (F := parallelPair (f - g) 0) (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (F := parallelPair (F.map (f - g)) 0) (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) :=
  isColimitCoforkMapOfIsColimit' F ⋯ c'
preserves : IsColimit (F.mapCocone c)
⊢ Nonempty (IsColimit (F.mapCocone c))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (F := parallelPair (f - g) 0) (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (F := parallelPair (F.map (f - g)) 0) (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) :=
  isColimitCoforkMapOfIsColimit' F ⋯ c'
_ : IsColimit ((Cocone.functoriality (parallelPair f g) F).obj (Cofork.ofπ (Cofork.π c) ⋯))
⊢ IsColimit (F.mapCocone c)

Tactic:
apply
    IsColimit.ofIsoColimit _ ((Cocone.functoriality _ F).mapIso (Cofork.isoCoforkOfπ c).symm)

Premises used: CategoryTheory.Limits.Cofork.isoCoforkOfπ, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Limits.Cocone.functoriality, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (F := parallelPair (f - g) 0) (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (F := parallelPair (F.map (f - g)) 0) (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) :=
  isColimitCoforkMapOfIsColimit' F ⋯ c'
apply : IsColimit (Cofork.ofπ (F.map (Cofork.π c)) ⋯)
⊢ IsColimit ((Cocone.functoriality (parallelPair f g) F).obj (Cofork.ofπ (Cofork.π c) ⋯))

Tactic:
apply (isColimitMapCoconeCoforkEquiv F (Cofork.condition c)).invFun

Premises used: CategoryTheory.Limits.Cofork.condition, Equiv.invFun, CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (F := parallelPair (f - g) 0) (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (F := parallelPair (F.map (f - g)) 0) (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) :=
  isColimitCoforkMapOfIsColimit' F ⋯ c'
⊢ (parallelPair (F.map (f - g)) 0).map WalkingParallelPairHom.left ≫
      Iso.hom (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair (F.map f - F.map g) 0).map WalkingParallelPairHom.left

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (F := parallelPair (f - g) 0) (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (F := parallelPair (F.map (f - g)) 0) (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) :=
  isColimitCoforkMapOfIsColimit' F ⋯ c'
⊢ (parallelPair (F.map (f - g)) 0).map WalkingParallelPairHom.right ≫
      Iso.hom (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one)) =
    Iso.hom (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero)) ≫
      (parallelPair (F.map f - F.map g) 0).map WalkingParallelPairHom.right

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (F := parallelPair (f - g) 0) (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (F := parallelPair (F.map (f - g)) 0) (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) :=
  isColimitCoforkMapOfIsColimit' F ⋯ c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
  parallelPair.ext (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero))
    (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ (coforkOfCokernelCofork ((Cocone.precompose p.symm.hom).obj (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯))).π ≫
      Iso.hom
        (Iso.refl
          (coforkOfCokernelCofork
              ((Cocone.precompose p.symm.hom).obj (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯))).pt) =
    (Cofork.ofπ (F.map (Cofork.π c)) ⋯).π

Tactic:
simp [p]
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cocone (parallelPair f g)
i : IsColimit c
c' : IsColimit (F := parallelPair (f - g) 0) (CokernelCofork.ofπ (Cofork.π c) ⋯) :=
  isColimitCokernelCoforkOfCofork (i.ofIsoColimit (Cofork.isoCoforkOfπ c))
iFc : IsColimit (F := parallelPair (F.map (f - g)) 0) (CokernelCofork.ofπ (F.map (Cofork.π c)) ⋯) :=
  isColimitCoforkMapOfIsColimit' F ⋯ c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
  parallelPair.ext (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.zero))
    (Iso.refl ((parallelPair (F.map (f - g)) 0).obj WalkingParallelPair.one)) ⋯ ⋯
⊢ IsColimit (Cofork.ofπ (F.map (Cofork.π c)) ⋯)

Tactic:
exact
    IsColimit.ofIsoColimit
      (isColimitCoforkOfCokernelCofork ((IsColimit.precomposeHomEquiv p.symm _).symm iFc))
      (Cofork.ext (Iso.refl _) (by simp [p]))

Premises used: CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Iso.refl, CategoryTheory.Iso.symm, CategoryTheory.Limits.Cofork.ext, Equiv.symm, DFunLike.coe, CategoryTheory.Limits.IsColimit.precomposeHomEquiv
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
K : Functor.{0, v₁, 0, u₁} WalkingParallelPair C
this : PreservesColimit (parallelPair (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)) F := ⋯
⊢ PreservesColimit K F

Tactic:
apply preservesColimit_of_iso_diagram F (diagramIsoParallelPair K).symm

Premises used: CategoryTheory.Limits.diagramIsoParallelPair, CategoryTheory.Limits.preservesColimit_of_iso_diagram, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : HasFiniteCoproducts.{v₁, u₁} C
inst_7 : HasCoequalizers.{v₁, u₁} C
inst_8 : HasZeroObject.{v₁, u₁} C
inst_9 : HasZeroObject.{v₂, u₂} D
inst_10 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this_1 : PreservesColimitsOfShape WalkingParallelPair F := ⋯
this_2 : PreservesColimit (empty C) F := ⋯
this_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F := ⋯
this : PreservesFiniteCoproducts F := ⋯
⊢ PreservesFiniteColimits F

Tactic:
preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts F

Premises used: CategoryTheory.Limits.preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts
-- Module: Mathlib.CategoryTheory.Preadditive.LeftExact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Preadditive.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
inst_5 : HasBinaryBiproducts.{v₁, u₁} C
inst_6 : HasFiniteCoproducts.{v₁, u₁} C
inst_7 : HasCoequalizers.{v₁, u₁} C
inst_8 : HasZeroObject.{v₁, u₁} C
inst_9 : HasZeroObject.{v₂, u₂} D
inst_10 : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
this_1 : PreservesColimitsOfShape WalkingParallelPair F := ⋯
this_2 : PreservesColimit (empty C) F := ⋯
this_3 : PreservesColimitsOfShape (Discrete PEmpty.{1}) F := ⋯
this : PreservesFiniteCoproducts F := ⋯
⊢ PreservesFiniteColimits F

Tactic:
exact preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts F

Premises used: CategoryTheory.Limits.preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteCoproducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasCoproduct.{w, v, u} f
S : Finset (Discrete α)
dsimp :
  Eq.{v + 1} (α := (sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as) ⟶ sigmaObj.{w, v, u} f)
    (Sigma.desc fun (s : ↥S) ↦ Sigma.ι f (↑s : Discrete α).as)
    (∑ a ∈ S.attach, Sigma.π (fun (a : ↥S) ↦ f (↑a : Discrete α).as) a ≫ Sigma.ι f (↑a : Discrete α).as)
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u} (liftToFinsetObj (Discrete.functor f)) S ⟶
      Functor.obj.{w, v, w, u}
        (Functor.obj (Functor.const (Finset (Discrete α)))
          (Cocone.pt.{w, v, w, u} (F := liftToFinsetObj (Discrete.functor f)) (finiteSubcoproductsCocone f)))
        S)
    (NatTrans.app (Cocone.ι (finiteSubcoproductsCocone f)) S)
    (∑ a ∈ S.attach, Sigma.π (fun (a : ↥S) ↦ f (↑a : Discrete α).as) a ≫ Sigma.ι f (↑a : Discrete α).as)

Tactic:
dsimp only [liftToFinsetObj_obj, Discrete.functor_obj_eq_as, finiteSubcoproductsCocone_pt,
    Functor.const_obj_obj, finiteSubcoproductsCocone_ι_app]

Premises used: CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_pt, CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetObj_obj, CategoryTheory.Discrete.functor_obj_eq_as, CategoryTheory.Limits.CoproductsFromFiniteFiltered.finiteSubcoproductsCocone_ι_app, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteCoproducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasCoproduct.{w, v, u} f
S : Finset (Discrete α)
h :
  ∀ (v : ↥S),
    Eq.{v + 1} (α := f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
          (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) v)
          (Sigma.desc fun (s : ↥S) ↦ Sigma.ι f (↑s : Discrete α).as) :
        f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
          (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) v)
          (∑ a ∈ S.attach, Sigma.π (fun (a : ↥S) ↦ f (↑a : Discrete α).as) a ≫ Sigma.ι f (↑a : Discrete α).as) :
        f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
⊢ Eq.{v + 1} (α := (sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as) ⟶ sigmaObj.{w, v, u} f)
    (Sigma.desc fun (s : ↥S) ↦ Sigma.ι f (↑s : Discrete α).as)
    (∑ a ∈ S.attach, Sigma.π (fun (a : ↥S) ↦ f (↑a : Discrete α).as) a ≫ Sigma.ι f (↑a : Discrete α).as)

Tactic:
ext v
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteCoproducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasCoproduct.{w, v, u} f
S : Finset (Discrete α)
v : ↥S
h :
  Eq.{v + 1} (α := f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f) (Sigma.ι f (↑v : Discrete α).as)
    (∑ j ∈ S.attach,
      CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
        (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) v)
        (Sigma.π (fun (a : ↥S) ↦ f (↑a : Discrete α).as) j ≫ Sigma.ι f (↑j : Discrete α).as))
⊢ Eq.{v + 1} (α := f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
        (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) v)
        (Sigma.desc fun (s : ↥S) ↦ Sigma.ι f (↑s : Discrete α).as) :
      f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
        (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) v)
        (∑ a ∈ S.attach, Sigma.π (fun (a : ↥S) ↦ f (↑a : Discrete α).as) a ≫ Sigma.ι f (↑a : Discrete α).as) :
      f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)

Tactic:
simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app, Preadditive.comp_sum]

Premises used: CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Preadditive.comp_sum, CategoryTheory.Limits.colimit.ι_desc
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteCoproducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasCoproduct.{w, v, u} f
S : Finset (Discrete α)
v : ↥S
h :
  Eq.{v + 1} (α := f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f) (Sigma.ι f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
      (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) v)
      (Sigma.π (fun (a : ↥S) ↦ f (↑a : Discrete α).as) v ≫ Sigma.ι f (↑v : Discrete α).as))
h₁ :
  ∀ b ∈ S.attach,
    b ≠ v →
      Eq.{v + 1} (α := f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
        (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
            (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) v)
            (Sigma.π (fun (a : ↥S) ↦ f (↑a : Discrete α).as) b ≫ Sigma.ι f (↑b : Discrete α).as) :
          f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
        (0 : f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
h₂ :
  v ∉ S.attach →
    Eq.{v + 1} (α := f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
          (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) v)
          (Sigma.π (fun (a : ↥S) ↦ f (↑a : Discrete α).as) v ≫ Sigma.ι f (↑v : Discrete α).as) :
        f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
      (0 : f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
⊢ Eq.{v + 1} (α := f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f) (Sigma.ι f (↑v : Discrete α).as)
    (∑ j ∈ S.attach,
      CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
        (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) v)
        (Sigma.π (fun (a : ↥S) ↦ f (↑a : Discrete α).as) j ≫ Sigma.ι f (↑j : Discrete α).as))

Tactic:
rw [Finset.sum_eq_single v]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteCoproducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasCoproduct.{w, v, u} f
S : Finset (Discrete α)
v : ↥S
⊢ Eq.{v + 1} (α := f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f) (Sigma.ι f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
      (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) v)
      (Sigma.π (fun (a : ↥S) ↦ f (↑a : Discrete α).as) v ≫ Sigma.ι f (↑v : Discrete α).as))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteCoproducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasCoproduct.{w, v, u} f
S : Finset (Discrete α)
v b : ↥S
hb : b ∈ S.attach
hb₁ : b ≠ v
h :
  Eq.{v + 1} (α := f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
    (CategoryStruct.comp (Y := f (↑b : Discrete α).as) 0 (Sigma.ι f (↑b : Discrete α).as)) 0
h₁ h₂ : Eq.{v + 1} (α := f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f) 0 0
⊢ Eq.{v + 1} (α := f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
        (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) v)
        (Sigma.π (fun (a : ↥S) ↦ f (↑a : Discrete α).as) b ≫ Sigma.ι f (↑b : Discrete α).as) :
      f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
    (0 : f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)

Tactic:
rw [Sigma.ι_π_of_ne_assoc _ (Ne.symm hb₁), zero_comp]

Premises used: Ne.symm, CategoryTheory.Limits.Sigma.ι_π_of_ne_assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.LiftToFinset
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteCoproducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasCoproduct.{w, v, u} f
S : Finset (Discrete α)
v : ↥S
⊢ v ∉ S.attach →
    Eq.{v + 1} (α := f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : ↥S) ↦ f (↑x : Discrete α).as)
          (Sigma.ι.{w, v, u} (C := C) (fun (x : ↥S) ↦ f (↑x : Discrete α).as) v)
          (Sigma.π (fun (a : ↥S) ↦ f (↑a : Discrete α).as) v ≫ Sigma.ι f (↑v : Discrete α).as) :
        f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)
      (0 : f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f)

Tactic:
simp