awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ t.toCocone.ι.app j ≫ ∑ j : J, t.π j ≫ t.ι j = t.toCocone.ι.app j ≫ 𝟙 t.pt
have mk₁ : ∀ (as : J), (∑ x : J, if h : as = x then eqToHom sorry ≫ t.ι x else 0 ≫ t.ι x) = t.ι as ≫ 𝟙 t.pt
Tactic: classical
      cases j
      simp_rw [Bicone.toCocone_ι_app, comp_sum, ← Category.assoc, t.ι_π, 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 : Finite J
f : J → C
inst_3 : HasProduct.{u_1, v, u} f
⊢ HasBiproduct.{u_1, v, u} f
have intro : ∀ (val : Fintype J), HasBiproduct.{u_1, v, u} f
Tactic: cases nonempty_fintype 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 : Finite J
f : J → C
inst_3 : HasCoproduct.{u_1, v, u} f
⊢ HasBiproduct.{u_1, v, u} f
have intro : ∀ (val : Fintype J), HasBiproduct.{u_1, v, u} f
Tactic: cases nonempty_fintype 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
inst_2 : Fintype J
f : J → C
inst_3 : HasBiproduct.{0, v, u} f
T : C
g : (j : J) → T ⟶ f j
⊢ Eq (α := T ⟶ biproduct.{0, v, u} f) (lift g) (∑ j : J, g j ≫ ι f j)
have w : ∀ (j : J),
  CategoryStruct.comp (Y := biproduct.{0, v, u} f) (lift g) (π f j) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (∑ j : J, g j ≫ ι f j) (π f j)
Tactic: ext 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
inst_2 : Fintype J
f : J → C
inst_3 : HasBiproduct.{0, v, u} f
T : C
g : (j : J) → T ⟶ f j
⊢ Eq (α := T ⟶ biproduct.{0, v, u} f) (lift g) (∑ j : J, g j ≫ ι f j)
have w : ∀ (j : J),
  CategoryStruct.comp (Y := biproduct.{0, v, u} f) (lift g) (π f j) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (∑ j : J, g j ≫ ι f j) (π f j)
Tactic: classical
  ext j
  simp only [sum_comp, biproduct.ι_π, comp_dite, biproduct.lift_π, Category.assoc, comp_zero,
    Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, if_true]
-- 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
inst_2 : Fintype J
f : J → C
inst_3 : HasBiproduct.{0, v, u} f
T : C
g : (j : J) → f j ⟶ T
⊢ Eq (α := biproduct.{0, v, u} f ⟶ T) (desc g) (∑ j : J, π f j ≫ g j)
have w : ∀ (j : J),
  CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (desc g) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (∑ j : J, π f j ≫ g j)
Tactic: ext 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
inst_2 : Fintype J
f : J → C
inst_3 : HasBiproduct.{0, v, u} f
T : C
g : (j : J) → f j ⟶ T
⊢ Eq (α := biproduct.{0, v, u} f ⟶ T) (desc g) (∑ j : J, π f j ≫ g j)
have w : ∀ (j : J),
  CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (desc g) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j) (∑ j : J, π f j ≫ g j)
Tactic: classical
  ext j
  simp [comp_sum, biproduct.ι_π_assoc, 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
inst_2 : Fintype J
inst_3 : HasFiniteBiproducts.{v, u} C
f g : J → C
h : (j : J) → f j ⟶ g j
⊢ Eq (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g) (map h) (∑ j : J, π f j ≫ h j ≫ ι g j)
have w : ∀ (j j_1 : J),
  CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (map h) (π g j)) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (∑ j : J, π f j ≫ h j ≫ ι g j) (π g j))
Tactic: ext
-- 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
inst_2 : Fintype J
inst_3 : HasFiniteBiproducts.{v, u} C
f g : J → C
h : (j : J) → f j ⟶ g j
⊢ Eq (α := biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g) (map h) (∑ j : J, π f j ≫ h j ≫ ι g j)
have w : ∀ (j j_1 : J),
  CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (map h) (π g j)) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} f) (ι f j_1)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} g) (∑ j : J, π f j ≫ h j ≫ ι g j) (π g j))
Tactic: classical
  ext
  simp [biproduct.ι_π, biproduct.ι_π_assoc, sum_comp, comp_dite, 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
inst_2 : Fintype J
K : Type
inst_3 : Finite K
inst_4 : HasFiniteBiproducts.{v, u} C
f : J → C
g : K → C
P : C
x : (j : J) → P ⟶ f j
m : (j : J) → (k : K) → f j ⟶ g k
⊢ Eq (α := P ⟶ biproduct.{0, v, u} g)
    (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (lift x : P ⟶ biproduct.{0, v, u} f)
        (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g) :
      P ⟶ biproduct.{0, v, u} g)
    (lift fun (k : K) ↦ ∑ j : J, x j ≫ m j k : P ⟶ biproduct.{0, v, u} g)
have w : ∀ (j : K),
  CategoryStruct.comp (Y := biproduct.{0, v, u} g)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} f) (lift x : P ⟶ biproduct.{0, v, u} f)
          (matrix m : biproduct.{0, v, u} f ⟶ biproduct.{0, v, u} g) :
        P ⟶ biproduct.{0, v, u} g)
      (π g j : biproduct.{0, v, u} g ⟶ g j) =
    CategoryStruct.comp (Y := biproduct.{0, v, u} g) (lift fun (k : K) ↦ ∑ j : J, x j ≫ m j k) (π g j)
Tactic: ext
-- 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 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
⊢ Eq (α := biproduct.{0, v, u} f ⟶ P)
    (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)
    (desc fun (j : J) ↦ ∑ k : K, m j k ≫ x k : biproduct.{0, v, u} f ⟶ P)
have w : ∀ (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: ext
-- 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 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
⊢ 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)
have 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)
Tactic: ext
-- 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 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
⊢ 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)
have 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)
Tactic: ext
-- 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
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{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)) =
    𝟙 (biproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ)))
have 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
Tactic: ext b b'
-- 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
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
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
have 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
Tactic: by_cases h : b' = b
-- 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
β γ : 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
⊢ 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
have 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
Tactic: by_cases h : b' = b
-- 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
β γ : 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
⊢ 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
have 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'
Tactic: subst h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
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
⊢ 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
have this : Ne (α := γ) ((ε : (a : β) → γ) b' : γ) ((ε : (a : β) → γ) b : γ)
Tactic: have : ε b' ≠ ε b := by simp [h]
-- 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
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
⊢ 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))
have 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))
Tactic: cases nonempty_fintype β
-- 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
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
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))
have 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
Tactic: ext g g'
-- 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
β γ : 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' : γ
⊢ 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
have 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
Tactic: by_cases h : g' = g
-- 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
β γ : 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
⊢ 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
have 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
Tactic: by_cases h : g' = g
-- 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
β γ : Type
inst_2 : Finite β
ε : β ≃ γ
f : γ → C
inst_3 : HasBiproduct.{0, v, u} f
inst_4 : HasBiproduct.{0, v, u} (J := β) (f ∘ (⇑ε : (a : β) → γ))
⊢ 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))
have 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))
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]