awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
i : IsLimit c
s : Fork f g
⊢ (isLimitForkOfKernelFork i).lift s = i.lift (kernelForkOfFork s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
s : Fork (f - g) 0
m : s.pt ⟶ Cone.pt (F := parallelPair (f - g) 0) (kernelForkOfFork c)
h : m ≫ Fork.ι (kernelForkOfFork c) = s.ι
apply : m ≫ c.ι = i.lift (forkOfKernelFork s) ≫ c.ι
⊢ m = i.lift (forkOfKernelFork s)

Tactic:
apply Fork.IsLimit.hom_ext i

Premises used: CategoryTheory.Limits.Fork.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : HasKernel (f - g)
⊢ HasEqualizer f g

Tactic:
HasLimit.mk
    { cone := forkOfKernelFork _
      isLimit := isLimitForkOfKernelFork (equalizerIsEqualizer (f - g) 0) }

Premises used: CategoryTheory.Preadditive.isLimitForkOfKernelFork, CategoryTheory.Limits.Fork.ofι, CategoryTheory.Limits.equalizer.condition, HSub.hSub, CategoryTheory.Limits.equalizer.ι, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.equalizerIsEqualizer, CategoryTheory.Limits.LimitCone.mk, OfNat.ofNat, CategoryTheory.Preadditive.forkOfKernelFork
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : HasEqualizer f g
⊢ HasKernel (f - g)

Tactic:
HasLimit.mk
    { cone := kernelForkOfFork (equalizer.fork f g)
      isLimit := isLimitKernelForkOfFork (limit.isLimit (parallelPair f g)) }

Premises used: CategoryTheory.Preadditive.isLimitKernelForkOfFork, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.equalizer.fork, CategoryTheory.Preadditive.kernelForkOfFork, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Limits.parallelPair
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
rw : f ≫ Cofork.π c - g ≫ Cofork.π c = 0
rw₁ : (f - g) ≫ Cofork.π c = 0
rw₂ rw₃ : Eq.{v + 1} (α := X ⟶ c.pt) 0 0
⊢ f ≫ Cofork.π c = g ≫ Cofork.π c

Tactic:
rw [← sub_eq_zero, ← sub_comp, c.condition]

Premises used: sub_eq_zero, CategoryTheory.Limits.CokernelCofork.condition, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
⊢ (coforkOfCokernelCofork c).π = Cofork.π c

Tactic:
rfl

Premises used: CategoryTheory.Preadditive.coforkOfCokernelCofork, CategoryTheory.Limits.Cofork.ofπ, CategoryTheory.Limits.parallelPair, rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
rw : f ≫ c.π - g ≫ c.π = 0 ≫ c.π
rw₁ : f ≫ c.π - g ≫ c.π = 0
rw₂ : f ≫ c.π = g ≫ c.π
rw₃ rw₄ : g ≫ c.π = g ≫ c.π
⊢ (f - g) ≫ c.π = 0 ≫ c.π

Tactic:
rw [sub_comp, zero_comp, sub_eq_zero, c.condition]

Premises used: sub_eq_zero, CategoryTheory.Limits.Cofork.condition, CategoryTheory.Limits.zero_comp, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ Cofork.π (cokernelCoforkOfCofork c) = c.π

Tactic:
rfl

Premises used: CategoryTheory.Preadditive.cokernelCoforkOfCofork, CategoryTheory.Limits.Cofork.ofπ, CategoryTheory.Limits.parallelPair, rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ (f - g) ≫ π = 0

Tactic:
simp [w]
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
P : C
π : Y ⟶ P
w : f ≫ π = g ≫ π
⊢ Eq (α := CokernelCofork (f - g)) (cokernelCoforkOfCofork (Cofork.ofπ π w)) (CokernelCofork.ofπ π ⋯)

Tactic:
rfl

Premises used: CategoryTheory.Preadditive.cokernelCoforkOfCofork, rfl, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
i : IsColimit c
s : Cofork f g
m : (coforkOfCokernelCofork c).pt ⟶ s.pt
h : (coforkOfCokernelCofork c).π ≫ m = s.π
apply : Cofork.π c ≫ m = Cofork.π c ≫ i.desc (cokernelCoforkOfCofork s)
⊢ m = i.desc (cokernelCoforkOfCofork s)

Tactic:
apply Cofork.IsColimit.hom_ext i

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : CokernelCofork (f - g)
i : IsColimit c
s : Cofork f g
⊢ (isColimitCoforkOfCokernelCofork i).desc s = i.desc (cokernelCoforkOfCofork s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
s : Cofork (f - g) 0
m : Cocone.pt (F := parallelPair (f - g) 0) (cokernelCoforkOfCofork c) ⟶ s.pt
h : Cofork.π (cokernelCoforkOfCofork c) ≫ m = s.π
apply : c.π ≫ m = c.π ≫ i.desc (coforkOfCokernelCofork s)
⊢ m = i.desc (coforkOfCokernelCofork s)

Tactic:
apply Cofork.IsColimit.hom_ext i

Premises used: CategoryTheory.Limits.Cofork.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : HasCokernel (f - g)
⊢ HasCoequalizer f g

Tactic:
HasColimit.mk
    { cocone := coforkOfCokernelCofork _
      isColimit := isColimitCoforkOfCokernelCofork (coequalizerIsCoequalizer (f - g) 0) }

Premises used: CategoryTheory.Preadditive.isColimitCoforkOfCokernelCofork, CategoryTheory.Limits.coequalizer.condition, HSub.hSub, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Preadditive.coforkOfCokernelCofork, CategoryTheory.Limits.Cofork.ofπ, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.coequalizerIsCoequalizer, OfNat.ofNat, CategoryTheory.Limits.coequalizer.π
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
inst_2 : HasCoequalizer f g
⊢ HasCokernel (f - g)

Tactic:
HasColimit.mk
    { cocone := cokernelCoforkOfCofork (coequalizer.cofork f g)
      isColimit := isColimitCokernelCoforkOfCofork (colimit.isColimit (parallelPair f g)) }

Premises used: CategoryTheory.Limits.coequalizer.cofork, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Preadditive.cokernelCoforkOfCofork, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.parallelPair, CategoryTheory.Preadditive.isColimitCokernelCoforkOfCofork
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasKernels.{v, u} C
⊢ HasEqualizers.{v, u} C

Tactic:
@hasEqualizers_of_hasLimit_parallelPair _ _ fun {_} {_} f g => hasEqualizer_of_hasKernel f g

Premises used: CategoryTheory.Limits.hasEqualizers_of_hasLimit_parallelPair
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasCokernels.{v, u} C
⊢ HasCoequalizers.{v, u} C

Tactic:
@hasCoequalizers_of_hasColimit_parallelPair _ _ fun {_} {_} f g =>
    hasCoequalizer_of_hasCokernel f g

Premises used: CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : C
a : ℤˣ
e : X ≅ Y
⊢ ((↑a : ℤ) • e.hom) ≫ ((↑a⁻¹ : ℤ) • e.inv) = 𝟙 X

Tactic:
simp only [comp_zsmul, zsmul_comp, smul_smul, Units.inv_mul, one_smul, e.hom_inv_id]

Premises used: Units.inv_mul, smul_smul, CategoryTheory.Iso.hom_inv_id, one_smul, CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.Preadditive.zsmul_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : C
a : ℤˣ
e : X ≅ Y
⊢ ((↑a⁻¹ : ℤ) • e.inv) ≫ ((↑a : ℤ) • e.hom) = 𝟙 Y

Tactic:
simp only [comp_zsmul, zsmul_comp, smul_smul, Units.mul_inv, one_smul, e.inv_hom_id]

Premises used: CategoryTheory.Iso.inv_hom_id, smul_smul, Units.mul_inv, one_smul, CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.Preadditive.zsmul_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : C
a : ℤˣ
e : X ≅ Y
⊢ (a • e).hom = a • e.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : C
a : ℤˣ
e : X ≅ Y
⊢ (a • e).inv = a⁻¹ • e.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : C
e : X ≅ Y
⊢ (-e).hom = -e.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : C
e : X ≅ Y
⊢ (-e).inv = -e.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cone.{u_1, v, u_1, u} (Discrete.functor f)
j : Discrete J
mk :
  ∀ (as : J),
    Eq (α := s.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
      ((∑ j : J, s.π.app { as := j } ≫ b.ι j) ≫ b.toCone.π.app { as := as : Discrete J }) (s.π.app { as := as })
⊢ (∑ j : J, s.π.app { as := j } ≫ b.ι j) ≫ b.toCone.π.app j = s.π.app j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cone.{u_1, v, u_1, u} (Discrete.functor f)
as : J
mk :
  Eq (α := s.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
    (∑ x : J,
      if h : x = as then s.π.app { as := x } ≫ eqToHom ⋯
      else
        CategoryStruct.comp (Y := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := x : Discrete J })
          (s.π.app { as := x }) 0)
    (s.π.app { as := as })
⊢ Eq (α := s.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
    ((∑ j : J, s.π.app { as := j } ≫ b.ι j) ≫ b.toCone.π.app { as := as : Discrete J }) (s.π.app { as := as })

Tactic:
simp only [sum_comp, Category.assoc, Bicone.toCone_π_app, b.ι_π, comp_dite]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Preadditive.sum_comp, CategoryTheory.Limits.Bicone.ι_π, CategoryTheory.Limits.Bicone.toCone_π_app, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cone.{u_1, v, u_1, u} (Discrete.functor f)
as : J
⊢ Eq (α := s.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
    (∑ x : J,
      if h : x = as then s.π.app { as := x } ≫ eqToHom ⋯
      else
        CategoryStruct.comp (Y := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := x : Discrete J })
          (s.π.app { as := x }) 0)
    (s.π.app { as := as })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cone.{u_1, v, u_1, u} (Discrete.functor f)
j : Discrete J
mk :
  ∀ (as : J),
    Eq (α := s.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
      ((∑ j : J, s.π.app { as := j } ≫ b.ι j) ≫ b.toCone.π.app { as := as : Discrete J }) (s.π.app { as := as })
mk₁ :
  ∀ (as : J),
    Eq (α := s.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
      (∑ x : J,
        if h : x = as then s.π.app { as := x } ≫ eqToHom ⋯
        else
          CategoryStruct.comp (Y := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := x : Discrete J })
            (s.π.app { as := x }) 0)
      (s.π.app { as := as })
⊢ (∑ j : J, s.π.app { as := j } ≫ b.ι j) ≫ b.toCone.π.app j = s.π.app j

Tactic:
classical
        cases j
        simp only [sum_comp, Category.assoc, Bicone.toCone_π_app, b.ι_π, comp_dite]
        simp

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Preadditive.sum_comp, CategoryTheory.Limits.Bicone.ι_π, CategoryTheory.Limits.Bicone.toCone_π_app, CategoryTheory.comp_dite
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cone.{u_1, v, u_1, u} (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
rw : m ≫ 𝟙 b.toCone.pt = ∑ j : J, s.π.app { as := j } ≫ b.ι j
⊢ m = ∑ j : J, s.π.app { as := j } ≫ b.ι j

Tactic:
rw [← Category.comp_id m]

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cone.{u_1, v, u_1, u} (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
dsimp : m ≫ 𝟙 b.pt = ∑ j : J, s.π.app { as := j } ≫ b.ι j
⊢ m ≫ 𝟙 b.toCone.pt = ∑ j : J, s.π.app { as := j } ≫ b.ι j

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cone.{u_1, v, u_1, u} (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
rw : Eq.{v + 1} (α := s.pt ⟶ b.pt) (∑ j : J, m ≫ b.π j ≫ b.ι j) (∑ j : J, s.π.app { as := j } ≫ b.ι j)
⊢ m ≫ 𝟙 b.pt = ∑ j : J, s.π.app { as := j } ≫ b.ι j

Tactic:
rw [← total, comp_sum]

Premises used: CategoryTheory.Preadditive.comp_sum
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cone.{u_1, v, u_1, u} (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
apply : ∀ (x : J), Membership.mem (γ := Finset J) Finset.univ x → m ≫ b.π x ≫ b.ι x = s.π.app { as := x } ≫ b.ι x
⊢ Eq.{v + 1} (α := s.pt ⟶ b.pt) (∑ j : J, m ≫ b.π j ≫ b.ι j) (∑ j : J, s.π.app { as := j } ≫ b.ι j)

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cone.{u_1, v, u_1, u} (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
j : J
_ : Membership.mem (γ := Finset J) Finset.univ j → m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j
⊢ Membership.mem (γ := Finset J) Finset.univ j → m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j

Tactic:
_
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cone.{u_1, v, u_1, u} (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
j : J
h_1 : Membership.mem (γ := Finset J) Finset.univ j
⊢ m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j

Tactic:
simpa using eq_whisker (h ⟨j⟩) _

Premises used: CategoryTheory.eq_whisker, CategoryTheory.Discrete.mk
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cone.{u_1, v, u_1, u} (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
j : J
h_1 : Membership.mem (γ := Finset J) Finset.univ j
⊢ m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j

Tactic:
have reassoced : m ≫ Bicone.π b j ≫ Bicone.ι b j = s.π.app ⟨j⟩ ≫ Bicone.ι b j := by
          simpa using eq_whisker (h ⟨j⟩) _
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cone.{u_1, v, u_1, u} (Discrete.functor f)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete J), m ≫ b.toCone.π.app j = s.π.app j
j : J
h_1 : Membership.mem (γ := Finset J) Finset.univ j
reassoced : m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j
rw rw₁ : s.π.app { as := j : Discrete J } ≫ b.ι j = s.π.app { as := j } ≫ b.ι j
⊢ m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j

Tactic:
rw [reassoced]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cocone.{u_1, v, u_1, u} (Discrete.functor f)
j : Discrete J
mk :
  ∀ (as : J),
    Eq (α := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J } ⟶ s.pt)
      (b.toCocone.ι.app { as := as : Discrete J } ≫ ∑ j : J, b.π j ≫ s.ι.app { as := j }) (s.ι.app { as := as })
⊢ b.toCocone.ι.app j ≫ ∑ j : J, b.π j ≫ s.ι.app { as := j } = s.ι.app j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cocone.{u_1, v, u_1, u} (Discrete.functor f)
as : J
mk :
  Eq (α := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J } ⟶ s.pt)
    (∑ x : J,
      if h : as = x then eqToHom ⋯ ≫ s.ι.app { as := x } else CategoryStruct.comp (Y := f x) 0 (s.ι.app { as := x }))
    (s.ι.app { as := as })
⊢ Eq (α := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J } ⟶ s.pt)
    (b.toCocone.ι.app { as := as : Discrete J } ≫ ∑ j : J, b.π j ≫ s.ι.app { as := j }) (s.ι.app { as := as })

Tactic:
simp only [comp_sum, ← Category.assoc, Bicone.toCocone_ι_app, b.ι_π, dite_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum, CategoryTheory.Limits.Bicone.toCocone_ι_app, CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cocone.{u_1, v, u_1, u} (Discrete.functor f)
as : J
⊢ Eq (α := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J } ⟶ s.pt)
    (∑ x : J,
      if h : as = x then eqToHom ⋯ ≫ s.ι.app { as := x } else CategoryStruct.comp (Y := f x) 0 (s.ι.app { as := x }))
    (s.ι.app { as := as })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cocone.{u_1, v, u_1, u} (Discrete.functor f)
j : Discrete J
mk :
  ∀ (as : J),
    Eq (α := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J } ⟶ s.pt)
      (b.toCocone.ι.app { as := as : Discrete J } ≫ ∑ j : J, b.π j ≫ s.ι.app { as := j }) (s.ι.app { as := as })
mk₁ :
  ∀ (as : J),
    Eq (α := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J } ⟶ s.pt)
      (∑ x : J,
        if h : as = x then eqToHom ⋯ ≫ s.ι.app { as := x } else CategoryStruct.comp (Y := f x) 0 (s.ι.app { as := x }))
      (s.ι.app { as := as })
⊢ b.toCocone.ι.app j ≫ ∑ j : J, b.π j ≫ s.ι.app { as := j } = s.ι.app j

Tactic:
classical
        cases j
        simp only [comp_sum, ← Category.assoc, Bicone.toCocone_ι_app, b.ι_π, dite_comp]
        simp

Premises used: CategoryTheory.Category.assoc, CategoryTheory.dite_comp, CategoryTheory.Preadditive.comp_sum, CategoryTheory.Limits.Bicone.toCocone_ι_app, CategoryTheory.Limits.Bicone.ι_π
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cocone.{u_1, v, u_1, u} (Discrete.functor f)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
rw : 𝟙 b.toCocone.pt ≫ m = ∑ j : J, b.π j ≫ s.ι.app { as := j }
⊢ m = ∑ j : J, b.π j ≫ s.ι.app { as := j }

Tactic:
rw [← Category.id_comp m]

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cocone.{u_1, v, u_1, u} (Discrete.functor f)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
dsimp : 𝟙 b.pt ≫ m = ∑ j : J, b.π j ≫ s.ι.app { as := j }
⊢ 𝟙 b.toCocone.pt ≫ m = ∑ j : J, b.π j ≫ s.ι.app { as := j }

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cocone.{u_1, v, u_1, u} (Discrete.functor f)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
rw : Eq.{v + 1} (α := b.pt ⟶ s.pt) (∑ j : J, (b.π j ≫ b.ι j) ≫ m) (∑ j : J, b.π j ≫ s.ι.app { as := j })
⊢ 𝟙 b.pt ≫ m = ∑ j : J, b.π j ≫ s.ι.app { as := j }

Tactic:
rw [← total, sum_comp]

Premises used: CategoryTheory.Preadditive.sum_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Fintype J
f : J → C
b : Bicone.{u_1, v, u} f
total : Eq.{v + 1} (α := b.pt ⟶ b.pt) (∑ j : J, b.π j ≫ b.ι j) (𝟙 b.pt)
s : Cocone.{u_1, v, u_1, u} (Discrete.functor f)
m : b.toCocone.pt ⟶ s.pt
h : ∀ (j : Discrete J), b.toCocone.ι.app j ≫ m = s.ι.app j
apply : ∀ (x : J), Membership.mem (γ := Finset J) Finset.univ x → (b.π x ≫ b.ι x) ≫ m = b.π x ≫ s.ι.app { as := x }
⊢ Eq.{v + 1} (α := b.pt ⟶ s.pt) (∑ j : J, (b.π j ≫ b.ι j) ≫ m) (∑ j : J, b.π j ≫ s.ι.app { as := j })

Tactic:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl