awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LeftExact (goal)
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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
⊢ PreservesLimit (parallelPair f g) F
have preserves : ∀ {c : Cone (parallelPair f g)} (hc : IsLimit c), Nonempty (IsLimit (F.mapCone c))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LeftExact (goal)
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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (F := parallelPair (f - g) 0) (KernelFork.ofι (Fork.ι c) ⋯) :=
  isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (F := parallelPair (F.map (f - g)) 0) (KernelFork.ofι (F.map (Fork.ι c)) ⋯) :=
  isLimitForkMapOfIsLimit' F ⋯ c'
⊢ Nonempty (IsLimit (F.mapCone c))
have preserves : IsLimit (F.mapCone c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LeftExact (goal)
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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (F := parallelPair (f - g) 0) (KernelFork.ofι (Fork.ι c) ⋯) :=
  isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (F := parallelPair (F.map (f - g)) 0) (KernelFork.ofι (F.map (Fork.ι c)) ⋯) :=
  isLimitForkMapOfIsLimit' F ⋯ c'
⊢ IsLimit (F.mapCone c)
have apply : IsLimit ((Cone.functoriality (parallelPair f g) F).obj (Fork.ofι (Fork.ι c) sorry))
Tactic: apply IsLimit.ofIsoLimit _ ((Cone.functoriality _ F).mapIso (Fork.isoForkOfι c).symm)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LeftExact (goal)
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), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this_1 : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (F := parallelPair (f - g) 0) (KernelFork.ofι (Fork.ι c) ⋯) :=
  isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (F := parallelPair (F.map (f - g)) 0) (KernelFork.ofι (F.map (Fork.ι c)) ⋯) :=
  isLimitForkMapOfIsLimit' F ⋯ c'
⊢ IsLimit ((Cone.functoriality (parallelPair f g) F).obj (Fork.ofι (Fork.ι c) ⋯))
have apply : IsLimit (Fork.ofι (F.map (Fork.ι c)) sorry)
Tactic: apply (isLimitMapConeForkEquiv F (Fork.condition c)).invFun
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LeftExact (hypothesis)
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 := ⋯
⊢ PreservesColimit (parallelPair f g) F
have this₁ : F.Additive
Tactic: haveI := additive_of_preservesBinaryBiproducts F
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LeftExact (goal)
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
⊢ PreservesColimit (parallelPair f g) F
have preserves : ∀ {c : Cocone (parallelPair f g)} (hc : IsColimit c), Nonempty (IsColimit (F.mapCocone c))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LeftExact (goal)
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'
⊢ Nonempty (IsColimit (F.mapCocone c))
have preserves : IsColimit (F.mapCocone c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LeftExact (goal)
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 (F.mapCocone c)
have _ : IsColimit ((Cocone.functoriality (parallelPair f g) F).obj (Cofork.ofπ (Cofork.π c) sorry))
Tactic: apply
    IsColimit.ofIsoColimit _ ((Cocone.functoriality _ F).mapIso (Cofork.isoCoforkOfπ c).symm)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LeftExact (goal)
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) ⋯))
have apply : IsColimit (Cofork.ofπ (F.map (Cofork.π c)) sorry)
Tactic: apply (isColimitMapCoconeCoforkEquiv F (Cofork.condition c)).invFun
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
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 α)
⊢ 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)
have 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)
Tactic: dsimp only [liftToFinsetObj_obj, Discrete.functor_obj_eq_as, finiteSubcoproductsCocone_pt,
    Functor.const_obj_obj, finiteSubcoproductsCocone_ι_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
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 α)
⊢ 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)
have 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)
Tactic: ext v
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
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)
    (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)
have 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))
Tactic: simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app, Preadditive.comp_sum]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
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)
    (∑ 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))
have 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))
Tactic: rw [Finset.sum_eq_single v]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
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))
⊢ 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))
have 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)
Tactic: rw [Finset.sum_eq_single v]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
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)
⊢ 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))
have 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)
Tactic: rw [Finset.sum_eq_single v]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
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
⊢ 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)
have 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
Tactic: rw [Sigma.ι_π_of_ne_assoc _ (Ne.symm hb₁), zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
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
⊢ 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)
have h₁ : Eq.{v + 1} (α := f (↑v : Discrete α).as ⟶ sigmaObj.{w, v, u} f) 0 0
Tactic: rw [Sigma.ι_π_of_ne_assoc _ (Ne.symm hb₁), zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteProducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasProduct.{w, v, u} f
S : (Finset (Discrete α))ᵒᵖ
⊢ Eq.{v + 1} (α :=
    Functor.obj.{w, v, w, u}
        (Functor.obj (Functor.const (Finset (Discrete α))ᵒᵖ)
          (Cone.pt.{w, v, w, u} (F := liftToFinsetObj (Discrete.functor f)) (finiteSubproductsCone f)))
        S ⟶
      Functor.obj.{w, v, w, u} (liftToFinsetObj (Discrete.functor f)) S)
    (NatTrans.app (Cone.π (finiteSubproductsCone f)) S)
    (∑ a ∈ (Opposite.unop S).attach,
      CategoryStruct.comp (Y := f (↑a : Discrete α).as) (Pi.π f (↑a : Discrete α).as)
        (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) a))
have dsimp : Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
  (Pi.lift fun (s : ↥(Opposite.unop S)) ↦ Pi.π f (↑s : Discrete α).as)
  (∑ a ∈ (Opposite.unop S).attach,
    CategoryStruct.comp (Y := f (↑a : Discrete α).as) (Pi.π f (↑a : Discrete α).as)
      (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) a))
Tactic: dsimp only [finiteSubproductsCone_pt, Functor.const_obj_obj, liftToFinsetObj_obj,
    Discrete.functor_obj_eq_as, finiteSubproductsCone_π_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteProducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasProduct.{w, v, u} f
S : (Finset (Discrete α))ᵒᵖ
⊢ Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
    (Pi.lift fun (s : ↥(Opposite.unop S)) ↦ Pi.π f (↑s : Discrete α).as)
    (∑ a ∈ (Opposite.unop S).attach,
      CategoryStruct.comp (Y := f (↑a : Discrete α).as) (Pi.π f (↑a : Discrete α).as)
        (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) a))
have h : ∀ (v : ↥(Opposite.unop S)),
  Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
        (Pi.lift fun (s : ↥(Opposite.unop S)) ↦ Pi.π f (↑s : Discrete α).as)
        (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v) :
      piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
        (∑ a ∈ (Opposite.unop S).attach,
          CategoryStruct.comp (Y := f (↑a : Discrete α).as) (Pi.π f (↑a : Discrete α).as)
            (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) a))
        (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v) :
      piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
Tactic: ext v
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.LiftToFinset (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteProducts.{v, u} C
α : Type w
inst_3 : DecidableEq α
f : α → C
inst_4 : HasProduct.{w, v, u} f
S : (Finset (Discrete α))ᵒᵖ
v : ↥(Opposite.unop S)
⊢ Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
        (Pi.lift fun (s : ↥(Opposite.unop S)) ↦ Pi.π f (↑s : Discrete α).as)
        (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v) :
      piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
    (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
        (∑ a ∈ (Opposite.unop S).attach,
          CategoryStruct.comp (Y := f (↑a : Discrete α).as) (Pi.π f (↑a : Discrete α).as)
            (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) a))
        (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v) :
      piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as)
have h : Eq.{v + 1} (α := piObj.{w, v, u} f ⟶ f (↑v : Discrete α).as) (Pi.π f (↑v : Discrete α).as)
  (∑ x ∈ (Opposite.unop S).attach,
    CategoryStruct.comp (Y := f (↑x : Discrete α).as) (Pi.π f (↑x : Discrete α).as)
      (CategoryStruct.comp (Y := piObj.{w, v, u} fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as)
        (Pi.ι.{w, v, u} (C := C) (fun (a : ↥(Opposite.unop S)) ↦ f (↑a : Discrete α).as) x)
        (Pi.π (fun (x : ↥(Opposite.unop S)) ↦ f (↑x : Discrete α).as) v)))
Tactic: simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app, Preadditive.sum_comp, Category.assoc]