awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
inst_2 : IsIso g
rw : f = 0 ≫ inv g ↔ f = 0
⊢ f ≫ g = 0 ↔ f = 0
have rw₁ : f = 0 ↔ f = 0
Tactic: rw [← IsIso.eq_comp_inv, Limits.zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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)
⊢ Fork.ι c ≫ f = Fork.ι c ≫ g
have rw : Fork.ι c ≫ f - Fork.ι c ≫ g = 0
Tactic: rw [← sub_eq_zero, ← comp_sub, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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)
rw : Fork.ι c ≫ f - Fork.ι c ≫ g = 0
⊢ Fork.ι c ≫ f = Fork.ι c ≫ g
have rw₁ : Fork.ι c ≫ (f - g) = 0
Tactic: rw [← sub_eq_zero, ← comp_sub, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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)
rw : Fork.ι c ≫ f - Fork.ι c ≫ g = 0
rw₁ : Fork.ι c ≫ (f - g) = 0
⊢ Fork.ι c ≫ f = Fork.ι c ≫ g
have rw₂ : Eq.{v + 1} (α := c.pt ⟶ Y) 0 0
Tactic: rw [← sub_eq_zero, ← comp_sub, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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
⊢ c.ι ≫ (f - g) = c.ι ≫ 0
have rw : c.ι ≫ f - c.ι ≫ g = c.ι ≫ 0
Tactic: rw [comp_sub, comp_zero, sub_eq_zero, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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
rw : c.ι ≫ f - c.ι ≫ g = c.ι ≫ 0
⊢ c.ι ≫ (f - g) = c.ι ≫ 0
have rw₁ : c.ι ≫ f - c.ι ≫ g = 0
Tactic: rw [comp_sub, comp_zero, sub_eq_zero, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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
rw : c.ι ≫ f - c.ι ≫ g = c.ι ≫ 0
rw₁ : c.ι ≫ f - c.ι ≫ g = 0
⊢ c.ι ≫ (f - g) = c.ι ≫ 0
have rw₂ : c.ι ≫ f = c.ι ≫ g
Tactic: rw [comp_sub, comp_zero, sub_eq_zero, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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
rw : c.ι ≫ f - c.ι ≫ g = c.ι ≫ 0
rw₁ : c.ι ≫ f - c.ι ≫ g = 0
rw₂ : c.ι ≫ f = c.ι ≫ g
⊢ c.ι ≫ (f - g) = c.ι ≫ 0
have rw₃ : c.ι ≫ g = c.ι ≫ g
Tactic: rw [comp_sub, comp_zero, sub_eq_zero, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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
m : s.pt ⟶ (forkOfKernelFork c).pt
h : m ≫ (forkOfKernelFork c).ι = s.ι
⊢ m = i.lift (kernelForkOfFork s)
have apply : m ≫ Fork.ι c = i.lift (kernelForkOfFork s) ≫ Fork.ι c
Tactic: apply Fork.IsLimit.hom_ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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.ι
⊢ m = i.lift (forkOfKernelFork s)
have apply : m ≫ c.ι = i.lift (forkOfKernelFork s) ≫ c.ι
Tactic: apply Fork.IsLimit.hom_ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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)
⊢ f ≫ Cofork.π c = g ≫ Cofork.π c
have rw : f ≫ Cofork.π c - g ≫ Cofork.π c = 0
Tactic: rw [← sub_eq_zero, ← sub_comp, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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
⊢ f ≫ Cofork.π c = g ≫ Cofork.π c
have rw₁ : (f - g) ≫ Cofork.π c = 0
Tactic: rw [← sub_eq_zero, ← sub_comp, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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
⊢ f ≫ Cofork.π c = g ≫ Cofork.π c
have rw₂ : Eq.{v + 1} (α := X ⟶ c.pt) 0 0
Tactic: rw [← sub_eq_zero, ← sub_comp, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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
⊢ (f - g) ≫ c.π = 0 ≫ c.π
have rw : f ≫ c.π - g ≫ c.π = 0 ≫ c.π
Tactic: rw [sub_comp, zero_comp, sub_eq_zero, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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.π
⊢ (f - g) ≫ c.π = 0 ≫ c.π
have rw₁ : f ≫ c.π - g ≫ c.π = 0
Tactic: rw [sub_comp, zero_comp, sub_eq_zero, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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
⊢ (f - g) ≫ c.π = 0 ≫ c.π
have rw₂ : f ≫ c.π = g ≫ c.π
Tactic: rw [sub_comp, zero_comp, sub_eq_zero, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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.π
⊢ (f - g) ≫ c.π = 0 ≫ c.π
have rw₃ : g ≫ c.π = g ≫ c.π
Tactic: rw [sub_comp, zero_comp, sub_eq_zero, c.condition]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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.π
⊢ m = i.desc (cokernelCoforkOfCofork s)
have apply : Cofork.π c ≫ m = Cofork.π c ≫ i.desc (cokernelCoforkOfCofork s)
Tactic: apply Cofork.IsColimit.hom_ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Basic (goal)
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.π
⊢ m = i.desc (coforkOfCokernelCofork s)
have apply : c.π ≫ m = c.π ≫ i.desc (coforkOfCokernelCofork s)
Tactic: apply Cofork.IsColimit.hom_ext i
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ (∑ j : J, s.π.app { as := j } ≫ b.ι j) ≫ b.toCone.π.app j = s.π.app j
have 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 })
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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 })
    ((∑ j : J, s.π.app { as := j } ≫ b.ι j) ≫ b.toCone.π.app { as := as : Discrete J }) (s.π.app { as := as })
have 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 sorry
    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 only [sum_comp, Category.assoc, Bicone.toCone_π_app, b.ι_π, comp_dite]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ (∑ j : J, s.π.app { as := j } ≫ b.ι j) ≫ b.toCone.π.app j = s.π.app j
have 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 })
Tactic: classical
        cases j
        simp only [sum_comp, Category.assoc, Bicone.toCone_π_app, b.ι_π, comp_dite]
        simp
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
have 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 sorry
      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: classical
        cases j
        simp only [sum_comp, Category.assoc, Bicone.toCone_π_app, b.ι_π, comp_dite]
        simp
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = ∑ j : J, s.π.app { as := j } ≫ b.ι j
have rw : m ≫ 𝟙 b.toCone.pt = ∑ j : J, s.π.app { as := j } ≫ b.ι j
Tactic: rw [← Category.comp_id m]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m ≫ 𝟙 b.toCone.pt = ∑ j : J, s.π.app { as := j } ≫ b.ι j
have dsimp : m ≫ 𝟙 b.pt = ∑ j : J, s.π.app { as := j } ≫ b.ι j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m ≫ 𝟙 b.pt = ∑ j : J, s.π.app { as := j } ≫ b.ι j
have rw : Eq.{v + 1} (α := s.pt ⟶ b.pt) (∑ j : J, m ≫ b.π j ≫ b.ι j) (∑ j : J, s.π.app { as := j } ≫ b.ι j)
Tactic: rw [← total, comp_sum]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ Eq.{v + 1} (α := s.pt ⟶ b.pt) (∑ j : J, m ≫ b.π j ≫ b.ι j) (∑ j : J, s.π.app { as := j } ≫ b.ι j)
have apply : ∀ (x : J), Membership.mem (γ := Finset J) Finset.univ x → m ≫ b.π x ≫ b.ι x = s.π.app { as := x } ≫ b.ι x
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m ≫ b.π j ≫ b.ι j = s.π.app { as := j } ≫ b.ι j
have rw : s.π.app { as := j : Discrete J } ≫ b.ι j = s.π.app { as := j } ≫ b.ι j
Tactic: rw [reassoced]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ b.toCocone.ι.app j ≫ ∑ j : J, b.π j ≫ s.ι.app { as := j } = s.ι.app j
have 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 })
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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)
    (b.toCocone.ι.app { as := as : Discrete J } ≫ ∑ j : J, b.π j ≫ s.ι.app { as := j }) (s.ι.app { as := as })
have 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 sorry ≫ s.ι.app { as := x } else CategoryStruct.comp (Y := f x) 0 (s.ι.app { as := x }))
  (s.ι.app { as := as })
Tactic: simp only [comp_sum, ← Category.assoc, Bicone.toCocone_ι_app, b.ι_π, dite_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ b.toCocone.ι.app j ≫ ∑ j : J, b.π j ≫ s.ι.app { as := j } = s.ι.app j
have 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 })
Tactic: classical
        cases j
        simp only [comp_sum, ← Category.assoc, Bicone.toCocone_ι_app, b.ι_π, dite_comp]
        simp
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
have 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 sorry ≫ s.ι.app { as := x } else CategoryStruct.comp (Y := f x) 0 (s.ι.app { as := x }))
    (s.ι.app { as := as })
Tactic: classical
        cases j
        simp only [comp_sum, ← Category.assoc, Bicone.toCocone_ι_app, b.ι_π, dite_comp]
        simp
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ m = ∑ j : J, b.π j ≫ s.ι.app { as := j }
have rw : 𝟙 b.toCocone.pt ≫ m = ∑ j : J, b.π j ≫ s.ι.app { as := j }
Tactic: rw [← Category.id_comp m]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ 𝟙 b.toCocone.pt ≫ m = ∑ j : J, b.π j ≫ s.ι.app { as := j }
have dsimp : 𝟙 b.pt ≫ m = ∑ j : J, b.π j ≫ s.ι.app { as := j }
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ 𝟙 b.pt ≫ m = ∑ j : J, b.π j ≫ s.ι.app { as := j }
have rw : Eq.{v + 1} (α := b.pt ⟶ s.pt) (∑ j : J, (b.π j ≫ b.ι j) ≫ m) (∑ j : J, b.π j ≫ s.ι.app { as := j })
Tactic: rw [← total, sum_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
⊢ Eq.{v + 1} (α := b.pt ⟶ s.pt) (∑ j : J, (b.π j ≫ b.ι j) ≫ m) (∑ j : J, b.π j ≫ s.ι.app { as := j })
have apply : ∀ (x : J), Membership.mem (γ := Finset J) Finset.univ x → (b.π x ≫ b.ι x) ≫ m = b.π x ≫ s.ι.app { as := x }
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
i : b.IsBilimit
j : Discrete J
⊢ (∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app j = 𝟙 b.pt ≫ b.toCone.π.app j
have mk : ∀ (as : J),
  Eq (α := b.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
    ((∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app { as := as : Discrete J }) (𝟙 b.pt ≫ b.toCone.π.app { as := as })
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
i : b.IsBilimit
j : Discrete J
⊢ (∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app j = 𝟙 b.pt ≫ b.toCone.π.app j
have mk : ∀ (as : J),
  Eq (α := b.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
    ((∑ j : J, b.π j ≫ b.ι j) ≫ b.toCone.π.app { as := as : Discrete J }) (𝟙 b.pt ≫ b.toCone.π.app { as := as })
Tactic: classical
    cases j
    simp [sum_comp, b.ι_π, comp_dite]
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
t : Bicone.{u_1, v, u} f
ht : IsLimit t.toCone
j : Discrete J
⊢ (∑ j : J, t.π j ≫ t.ι j) ≫ t.toCone.π.app j = 𝟙 t.pt ≫ t.toCone.π.app j
have mk : ∀ (as : J),
  Eq (α := t.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
    ((∑ j : J, t.π j ≫ t.ι j) ≫ t.toCone.π.app { as := as : Discrete J }) (𝟙 t.pt ≫ t.toCone.π.app { as := as })
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
t : Bicone.{u_1, v, u} f
ht : IsLimit t.toCone
j : Discrete J
⊢ (∑ j : J, t.π j ≫ t.ι j) ≫ t.toCone.π.app j = 𝟙 t.pt ≫ t.toCone.π.app j
have mk : ∀ (as : J),
  Eq (α := t.pt ⟶ obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J })
    ((∑ j : J, t.π j ≫ t.ι j) ≫ t.toCone.π.app { as := as : Discrete J }) (𝟙 t.pt ≫ t.toCone.π.app { as := as })
Tactic: classical
      cases j
      simp [sum_comp, t.ι_π, comp_dite]
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
t : Bicone.{u_1, v, u} f
ht : IsColimit t.toCocone
j : Discrete J
⊢ t.toCocone.ι.app j ≫ ∑ j : J, t.π j ≫ t.ι j = t.toCocone.ι.app j ≫ 𝟙 t.pt
have mk : ∀ (as : J),
  Eq (α := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J } ⟶ t.pt)
    (t.toCocone.ι.app { as := as : Discrete J } ≫ ∑ j : J, t.π j ≫ t.ι j)
    (t.toCocone.ι.app { as := as : Discrete J } ≫ 𝟙 t.pt)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
t : Bicone.{u_1, v, u} f
ht : IsColimit t.toCocone
as : J
⊢ Eq (α := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J } ⟶ t.pt)
    (t.toCocone.ι.app { as := as : Discrete J } ≫ ∑ j : J, t.π j ≫ t.ι j)
    (t.toCocone.ι.app { as := as : Discrete J } ≫ 𝟙 t.pt)
have mk : (∑ x : J, if h : as = x then eqToHom sorry ≫ t.ι x else 0 ≫ t.ι x) = t.ι as ≫ 𝟙 t.pt
Tactic: simp_rw [Bicone.toCocone_ι_app, comp_sum, ← Category.assoc, t.ι_π, dite_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
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
t : Bicone.{u_1, v, u} f
ht : IsColimit t.toCocone
j : Discrete J
⊢ t.toCocone.ι.app j ≫ ∑ j : J, t.π j ≫ t.ι j = t.toCocone.ι.app j ≫ 𝟙 t.pt
have mk : ∀ (as : J),
  Eq (α := obj.{u_1, v, u_1, u} (Discrete.functor f) { as := as : Discrete J } ⟶ t.pt)
    (t.toCocone.ι.app { as := as : Discrete J } ≫ ∑ j : J, t.π j ≫ t.ι j)
    (t.toCocone.ι.app { as := as : Discrete J } ≫ 𝟙 t.pt)
Tactic: classical
      cases j
      simp_rw [Bicone.toCocone_ι_app, comp_sum, ← Category.assoc, t.ι_π, dite_comp]
      simp
Cleared hypotheses: j