awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J K : Type
inst_2 : Finite J
inst_3 : HasFiniteBiproducts.{v, u} C
inst_4 : Fintype K
f : J → C
g : K → C
m : (j : J) → (k : K) → f j ⟶ g k
P : C
x : (k : K) → g k ⟶ P
j : J
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j : f j ⟶ biproduct.{0, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
          (desc x : biproduct.{0, v, u} g ⟶ P) :
        biproduct.{0, v, u} f ⟶ P) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (desc fun (j : J) ↦ ∑ k : K, m j k ≫ x k)

Tactic:
simp [lift_desc]

Premises used: CategoryTheory.Limits.biproduct.lift_desc
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J K : Type
inst_2 : Finite J
inst_3 : HasFiniteBiproducts.{v, u} C
inst_4 : Finite K
f : J → C
g h : K → C
m : (j : J) → (k : K) → f j ⟶ g k
n : (k : K) → g k ⟶ h k
w :
  ∀ (j : K) (j_1 : J),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1 : f j_1 ⟶ biproduct.{0, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} h)
            (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
              (map n : biproduct.{0, v, u} g ⟶ biproduct.{0, v, u} h))
            (π h j) :
          biproduct.{0, v, u} f ⟶ h j) =
      CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1 : f j_1 ⟶ biproduct.{0, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} h)
            (matrix fun (j : J) (k : K) ↦ m j k ≫ n k : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} h)
            (π h j : biproduct.{0, v, u} h ⟶ h j) :
          biproduct.{0, v, u} f ⟶ h j)
⊢ Eq (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} h)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
        (map n : biproduct.{0, v, u} g ⟶ biproduct.{0, v, u} h) :
      biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} h)
    (matrix fun (j : J) (k : K) ↦ m j k ≫ n k : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} h)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J K : Type
inst_2 : Finite J
inst_3 : HasFiniteBiproducts.{v, u} C
inst_4 : Finite K
f : J → C
g h : K → C
m : (j : J) → (k : K) → f j ⟶ g k
n : (k : K) → g k ⟶ h k
j : K
j_1 : J
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1 : f j_1 ⟶ biproduct.{0, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} h)
          (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
            (map n : biproduct.{0, v, u} g ⟶ biproduct.{0, v, u} h))
          (π h j) :
        biproduct.{0, v, u} f ⟶ h j) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1 : f j_1 ⟶ biproduct.{0, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} h)
          (matrix fun (j : J) (k : K) ↦ m j k ≫ n k : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} h)
          (π h j : biproduct.{0, v, u} h ⟶ h j) :
        biproduct.{0, v, u} f ⟶ h j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J K : Type
inst_2 : Finite J
inst_3 : HasFiniteBiproducts.{v, u} C
inst_4 : Finite K
f g : J → C
h : K → C
m : (k : J) → f k ⟶ g k
n : (j : J) → (k : K) → g j ⟶ h k
w :
  ∀ (j : K) (j_1 : J),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} h)
          (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (map m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
              (matrix n : biproduct.{0, v, u} g ⟶ biproduct.{0, v, u} h) :
            biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} h)
          (π h j : biproduct.{0, v, u} h ⟶ h j)) =
      CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1 : f j_1 ⟶ biproduct.{0, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} h)
            (matrix fun (j : J) (k : K) ↦ m j ≫ n j k : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} h)
            (π h j : biproduct.{0, v, u} h ⟶ h j) :
          biproduct.{0, v, u} f ⟶ h j)
⊢ Eq (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} h)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (map m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
        (matrix n : biproduct.{0, v, u} g ⟶ biproduct.{0, v, u} h) :
      biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} h)
    (matrix fun (j : J) (k : K) ↦ m j ≫ n j k : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} h)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J K : Type
inst_2 : Finite J
inst_3 : HasFiniteBiproducts.{v, u} C
inst_4 : Finite K
f g : J → C
h : K → C
m : (k : J) → f k ⟶ g k
n : (j : J) → (k : K) → g j ⟶ h k
j : K
j_1 : J
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} h)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (map m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g)
            (matrix n : biproduct.{0, v, u} g ⟶ biproduct.{0, v, u} h) :
          biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} h)
        (π h j : biproduct.{0, v, u} h ⟶ h j)) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1 : f j_1 ⟶ biproduct.{0, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} h)
          (matrix fun (j : J) (k : K) ↦ m j ≫ n j k : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} h)
          (π h j : biproduct.{0, v, u} h ⟶ h j) :
        biproduct.{0, v, u} f ⟶ h j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
w :
  ∀ (b b' : β),
    CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b')
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
          (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b))
            (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)))
          (π (f ∘ (⇑ε : (a : β) → γ)) b)) =
      ι (f ∘ (⇑ε : (a : β) → γ)) b' ≫
        𝟙 (biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) ≫ π (f ∘ (⇑ε : (a : β) → γ)) b
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b))
      (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) =
    𝟙 (biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))

Tactic:
ext b b'
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
b b' : β
pos :
  ∀ (h : b' = b),
    CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b')
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
          (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b))
            (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)))
          (π (f ∘ (⇑ε : (a : β) → γ)) b)) =
      ι (f ∘ (⇑ε : (a : β) → γ)) b' ≫
        𝟙 (biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) ≫ π (f ∘ (⇑ε : (a : β) → γ)) b
neg :
  ∀ (h : ¬b' = b),
    CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b')
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
          (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b))
            (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)))
          (π (f ∘ (⇑ε : (a : β) → γ)) b)) =
      ι (f ∘ (⇑ε : (a : β) → γ)) b' ≫
        𝟙 (biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) ≫ π (f ∘ (⇑ε : (a : β) → γ)) b
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b')
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
        (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b))
          (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)))
        (π (f ∘ (⇑ε : (a : β) → γ)) b)) =
    ι (f ∘ (⇑ε : (a : β) → γ)) b' ≫
      𝟙 (biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) ≫ π (f ∘ (⇑ε : (a : β) → γ)) b

Tactic:
by_cases h : b' = b
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
b b' : β
h : b' = b
pos :
  CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b')
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
        (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b))
          (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)))
        (π (f ∘ (⇑ε : (a : β) → γ)) b')) =
    ι (f ∘ (⇑ε : (a : β) → γ)) b' ≫
      𝟙 (biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) ≫ π (f ∘ (⇑ε : (a : β) → γ)) b'
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b')
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
        (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b))
          (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)))
        (π (f ∘ (⇑ε : (a : β) → γ)) b)) =
    ι (f ∘ (⇑ε : (a : β) → γ)) b' ≫
      𝟙 (biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) ≫ π (f ∘ (⇑ε : (a : β) → γ)) b

Tactic:
subst h
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
b' : β
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b')
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
        (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b))
          (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)))
        (π (f ∘ (⇑ε : (a : β) → γ)) b')) =
    ι (f ∘ (⇑ε : (a : β) → γ)) b' ≫
      𝟙 (biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) ≫ π (f ∘ (⇑ε : (a : β) → γ)) b'

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
b b' : β
h : ¬b' = b
⊢ Ne (α := γ) ((ε : (a : β) → γ) b' : γ) ((ε : (a : β) → γ) b : γ)

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
b b' : β
h : ¬b' = b
⊢ Ne (α := γ) ((ε : (a : β) → γ) b' : γ) ((ε : (a : β) → γ) b : γ)

Tactic:
have : ε b' ≠ ε b := by simp [h]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
b b' : β
h : ¬b' = b
this : Ne (α := γ) ((ε : (a : β) → γ) b' : γ) ((ε : (a : β) → γ) b : γ)
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) (ι (f ∘ (⇑ε : (a : β) → γ)) b')
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
        (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b))
          (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)))
        (π (f ∘ (⇑ε : (a : β) → γ)) b)) =
    ι (f ∘ (⇑ε : (a : β) → γ)) b' ≫
      𝟙 (biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))) ≫ π (f ∘ (⇑ε : (a : β) → γ)) b

Tactic:
simp [biproduct.ι_π_ne _ h, biproduct.ι_π_ne _ this]

Premises used: CategoryTheory.Limits.biproduct.ι_π_ne
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
intro :
  ∀ (val : Fintype β),
    Eq.{v + 1} (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
        (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
      (𝟙 (biproduct.{0, v, u} f))
⊢ Eq.{v + 1} (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} f)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
      (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
    (𝟙 (biproduct.{0, v, u} f))

Tactic:
cases nonempty_fintype β

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
val : Fintype β
intro :
  ∀ (g g' : γ),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f g')
        (CategoryStruct.comp (Y := biproduct.{0, v, u} f)
          (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
            (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
          (π f g)) =
      ι f g' ≫ 𝟙 (biproduct.{0, v, u} f) ≫ π f g
⊢ Eq.{v + 1} (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} f)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
      (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
    (𝟙 (biproduct.{0, v, u} f))

Tactic:
ext g g'
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
val : Fintype β
g g' : γ
pos :
  ∀ (h : g' = g),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f g')
        (CategoryStruct.comp (Y := biproduct.{0, v, u} f)
          (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
            (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
          (π f g)) =
      ι f g' ≫ 𝟙 (biproduct.{0, v, u} f) ≫ π f g
neg :
  ∀ (h : ¬g' = g),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f g')
        (CategoryStruct.comp (Y := biproduct.{0, v, u} f)
          (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
            (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
          (π f g)) =
      ι f g' ≫ 𝟙 (biproduct.{0, v, u} f) ≫ π f g
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f g')
      (CategoryStruct.comp (Y := biproduct.{0, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
          (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
        (π f g)) =
    ι f g' ≫ 𝟙 (biproduct.{0, v, u} f) ≫ π f g

Tactic:
by_cases h : g' = g
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
val : Fintype β
g g' : γ
h : g' = g
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f g')
      (CategoryStruct.comp (Y := biproduct.{0, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
          (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
        (π f g)) =
    ι f g' ≫ 𝟙 (biproduct.{0, v, u} f) ≫ π f g

Tactic:
simp [Preadditive.sum_comp, biproduct.lift_desc, biproduct.ι_π, comp_dite,
        Equiv.apply_eq_iff_eq_symm_apply, h]

Premises used: CategoryTheory.Preadditive.sum_comp, CategoryTheory.Limits.biproduct.lift_desc, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.comp_dite, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
val : Fintype β
g g' : γ
h : ¬g' = g
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f g')
      (CategoryStruct.comp (Y := biproduct.{0, v, u} f)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
          (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
        (π f g)) =
    ι f g' ≫ 𝟙 (biproduct.{0, v, u} f) ≫ π f g

Tactic:
simp [Preadditive.sum_comp, biproduct.lift_desc, biproduct.ι_π, comp_dite,
        Equiv.apply_eq_iff_eq_symm_apply, h]

Premises used: CategoryTheory.Preadditive.sum_comp, CategoryTheory.Limits.biproduct.lift_desc, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.comp_dite, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
intro :
  ∀ (val : Fintype β),
    Eq.{v + 1} (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} f)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
        (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
      (𝟙 (biproduct.{0, v, u} f))
intro₁ :
  ∀ (val : Fintype β) (g g' : γ),
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f g')
        (CategoryStruct.comp (Y := biproduct.{0, v, u} f)
          (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
            (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
          (π f g)) =
      ι f g' ≫ 𝟙 (biproduct.{0, v, u} f) ≫ π f g
⊢ Eq.{v + 1} (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} f)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
      (lift fun (b : β) ↦ π f ((ε : (a : β) → γ) b)) (desc fun (b : β) ↦ ι f ((ε : (a : β) → γ) b)))
    (𝟙 (biproduct.{0, v, u} f))

Tactic:
classical
    cases nonempty_fintype β
    ext g g'
    by_cases h : g' = g <;>
      simp [Preadditive.sum_comp, biproduct.lift_desc, biproduct.ι_π, comp_dite,
        Equiv.apply_eq_iff_eq_symm_apply, h]

Premises used: CategoryTheory.Preadditive.sum_comp, CategoryTheory.Limits.biproduct.lift_desc, nonempty_fintype, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.comp_dite, Equiv.apply_eq_iff_eq_symm_apply
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone.{0, v, 0, u} (pair X Y)
j : Discrete WalkingPair
left :
  Eq (α := s.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    ((BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left })
    (s.π.app { as := WalkingPair.left })
right :
  Eq (α := s.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    ((BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.right })
    (s.π.app { as := WalkingPair.right })
⊢ (BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app j = s.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := s.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    ((BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.left })
    (s.π.app { as := WalkingPair.left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := s.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    ((BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr) ≫ b.toCone.π.app { as := WalkingPair.right })
    (s.π.app { as := WalkingPair.right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone.{0, v, 0, u} (pair X Y)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete WalkingPair), m ≫ b.toCone.π.app j = s.π.app j
⊢ Eq (α := s.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ b.toCone.π.app { as := WalkingPair.left }) (s.π.app { as := WalkingPair.left })

Tactic:
have hₗ := h ⟨.left⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone.{0, v, 0, u} (pair X Y)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete WalkingPair), m ≫ b.toCone.π.app j = s.π.app j
hₗ :
  Eq (α := s.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ b.toCone.π.app { as := WalkingPair.left }) (s.π.app { as := WalkingPair.left })
⊢ Eq (α := s.pt ⟶ obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (m ≫ b.toCone.π.app { as := WalkingPair.right }) (s.π.app { as := WalkingPair.right })

Tactic:
have hᵣ := h ⟨.right⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X Y : C
b : BinaryBicone.{v, u} X Y
total : b.fst ≫ b.inl + b.snd ≫ b.inr = 𝟙 b.pt
s : Cone.{0, v, 0, u} (pair X Y)
m : s.pt ⟶ b.toCone.pt
h : ∀ (j : Discrete WalkingPair), m ≫ b.toCone.π.app j = s.π.app j
hₗ : m ≫ b.fst = s.π.app { as := WalkingPair.left }
hᵣ : m ≫ b.snd = s.π.app { as := WalkingPair.right }
⊢ m = BinaryFan.fst s ≫ b.inl + BinaryFan.snd s ≫ b.inr

Tactic:
simpa [← hₗ, ← hᵣ] using m ≫= total.symm

Premises used: Eq.symm