awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
j : J
⊢ Eq (α := f j ⟶ biproduct.{w, v, u} g) (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (map p)) (p j ≫ ι g j)
have rw : Eq (α := f j ⟶ biproduct.{w, v, u} g) (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (map' p)) (p j ≫ ι g j)
Tactic: rw [biproduct.map_eq_map']
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
P : C
k : (j : J) → g j ⟶ P
⊢ Eq (α := biproduct.{w, v, u} f ⟶ P) (CategoryStruct.comp (Y := biproduct.{w, v, u} g) (map p) (desc k))
    (desc fun (j : J) ↦ p j ≫ k j)
have w : ∀ (j : J),
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} g) (map p) (desc k)) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j) (desc fun (j : J) ↦ p j ≫ k j)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{w, v, u} g
P : C
k : (j : J) → P ⟶ f j
p : (j : J) → f j ⟶ g j
⊢ Eq (α := P ⟶ biproduct.{w, v, u} g) (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift k) (map p))
    (lift fun (j : J) ↦ k j ≫ p j)
have w : ∀ (j : J),
  CategoryStruct.comp (Y := biproduct.{w, v, u} g) (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift k) (map p))
      (π g j) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} g) (lift fun (j : J) ↦ k j ≫ p j) (π g j)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
inst_8 : ∀ (j : J), Epi (p j)
⊢ Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p)
    (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))
have w : ∀ (j j_1 : J),
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j_1)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} g) (map p) (π g j)) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j_1)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} g)
        (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g)) (π g j))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
inst_8 : ∀ (j : J), Epi (p j)
j j_1 : J
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j_1)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} g) (map p) (π g j)) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j_1)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} g)
        (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g)) (π g j))
have w : Eq.{v + 1} ((if h : j_1 = j then eqToHom sorry else 0) ≫ p j) (p j_1 ≫ if h : j_1 = j then eqToHom sorry else 0)
Tactic: simp only [map_π, ι_π_assoc, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc,
      Sigma.ι_map_assoc, colimit.ι_desc_assoc, Discrete.functor_obj_eq_as, Cofan.mk_pt,
      Cofan.mk_ι_app, ι_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
inst_8 : ∀ (j : J), Epi (p j)
j j_1 : J
⊢ Eq.{v + 1} ((if h : j_1 = j then eqToHom ⋯ else 0) ≫ p j) (p j_1 ≫ if h : j_1 = j then eqToHom ⋯ else 0)
have w : ∀ (h : j_1 = j), eqToHom sorry ≫ p j = p j_1 ≫ eqToHom sorry
Tactic: split
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
inst_8 : ∀ (j : J), Epi (p j)
j j_1 : J
w : ∀ (h : j_1 = j), eqToHom ⋯ ≫ p j = p j_1 ≫ eqToHom ⋯
⊢ Eq.{v + 1} ((if h : j_1 = j then eqToHom ⋯ else 0) ≫ p j) (p j_1 ≫ if h : j_1 = j then eqToHom ⋯ else 0)
have w₁ : ¬j_1 = j → Eq.{v + 1} (0 ≫ p j) (p j_1 ≫ 0)
Tactic: split
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (hypothesis)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
inst_8 : ∀ (j : J), Epi (p j)
⊢ Epi (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g) (map p)
have this : Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p)
  (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))
Tactic: have : biproduct.map p =
      (biproduct.isoCoproduct _).hom ≫ Sigma.map p ≫ (biproduct.isoCoproduct _).inv := by
    ext
    simp only [map_π, ι_π_assoc, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc,
      Sigma.ι_map_assoc, colimit.ι_desc_assoc, Discrete.functor_obj_eq_as, Cofan.mk_pt,
      Cofan.mk_ι_app, ι_π]
    split
    all_goals simp_all
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
inst_8 : ∀ (j : J), Epi (p j)
this :
  Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p)
    (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))
⊢ Epi (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g) (map p)
have rw : Epi (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g)
  (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
inst_8 : ∀ (j : J), Epi (p j)
⊢ Epi (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g) (map p)
have have : Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p)
  (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))
Tactic: classical
  have : biproduct.map p =
      (biproduct.isoCoproduct _).hom ≫ Sigma.map p ≫ (biproduct.isoCoproduct _).inv := by
    ext
    simp only [map_π, ι_π_assoc, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc,
      Sigma.ι_map_assoc, colimit.ι_desc_assoc, Discrete.functor_obj_eq_as, Cofan.mk_pt,
      Cofan.mk_ι_app, ι_π]
    split
    all_goals simp_all
  rw [this]
  infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
inst_8 : ∀ (j : J), Epi (p j)
have :
  Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p)
    (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))
⊢ Epi (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g) (map p)
have have₁ : ∀
  (this :
    Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p)
      (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))),
  Epi (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g) (map p)
Tactic: classical
  have : biproduct.map p =
      (biproduct.isoCoproduct _).hom ≫ Sigma.map p ≫ (biproduct.isoCoproduct _).inv := by
    ext
    simp only [map_π, ι_π_assoc, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc,
      Sigma.ι_map_assoc, colimit.ι_desc_assoc, Discrete.functor_obj_eq_as, Cofan.mk_pt,
      Cofan.mk_ι_app, ι_π]
    split
    all_goals simp_all
  rw [this]
  infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
inst_8 : ∀ (j : J), Epi (p j)
have :
  Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p)
    (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))
have₁ :
  ∀
    (this :
      Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p)
        (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))),
    Epi (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g) (map p)
have₂ :
  Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p)
    (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))
have₃ have₄ :
  ∀
    (this :
      Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p)
        (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))),
    Epi (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g) (map p)
⊢ Epi (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g) (map p)
have have₅ : ∀
  (this :
    Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p)
      (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))),
  Epi (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g)
    (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))
Tactic: classical
  have : biproduct.map p =
      (biproduct.isoCoproduct _).hom ≫ Sigma.map p ≫ (biproduct.isoCoproduct _).inv := by
    ext
    simp only [map_π, ι_π_assoc, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc,
      Sigma.ι_map_assoc, colimit.ι_desc_assoc, Discrete.functor_obj_eq_as, Cofan.mk_pt,
      Cofan.mk_ι_app, ι_π]
    split
    all_goals simp_all
  rw [this]
  infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
inst_8 : ∀ (j : J), Epi (p j)
⊢ Epi (X := piObj.{w, v, u} f) (Y := piObj.{w, v, u} g) (map p)
have rw : Epi (X := piObj.{w, v, u} f) (Y := piObj.{w, v, u} g)
  (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (Iso.inv (biproduct.isoProduct f))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} g) (biproduct.map p) (Iso.hom (biproduct.isoProduct g))) :
    piObj.{w, v, u} f ⟶ piObj.{w, v, u} g)
Tactic: rw [show Pi.map p = (biproduct.isoProduct _).inv ≫ biproduct.map p ≫
    (biproduct.isoProduct _).hom by aesop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
inst_8 : ∀ (j : J), Mono (p j)
⊢ Mono (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g) (map p)
have rw : Mono (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g)
  (Iso.hom (isoProduct f) ≫ Pi.map p ≫ Iso.inv (isoProduct g))
Tactic: rw [show biproduct.map p = (biproduct.isoProduct _).hom ≫ Pi.map p ≫
    (biproduct.isoProduct _).inv by aesop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
F : J_1 → C_1
J : Type w
K : Type u_1
C : Type u
inst_4 : Category.{v, u} C
inst_5 : HasZeroMorphisms.{v, u} C
f g : J → C
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{w, v, u} g
p : (j : J) → f j ⟶ g j
inst_8 : ∀ (j : J), Mono (p j)
⊢ Mono (X := sigmaObj.{w, v, u} f) (Y := sigmaObj.{w, v, u} g) (map p)
have rw : Mono (X := sigmaObj.{w, v, u} f) (Y := sigmaObj.{w, v, u} g)
  (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (Iso.inv (biproduct.isoCoproduct f))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} g) (biproduct.map p) (Iso.hom (biproduct.isoCoproduct g))) :
    sigmaObj.{w, v, u} f ⟶ sigmaObj.{w, v, u} g)
Tactic: rw [show Sigma.map p = (biproduct.isoCoproduct _).inv ≫ biproduct.map p ≫
    (biproduct.isoCoproduct _).hom by aesop]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
⊢ Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ biproduct.{u_1, v, u} g)
    (desc fun (j : J) ↦ (w j).inv ≫ ι g ((e : (a : J) → K) j))
    (lift fun (k : K) ↦ π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom ⋯)
have w₁ : ∀ (k : K) (j : J),
  Eq.{v + 1} (α := f j ⟶ g k)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (desc fun (j : J) ↦ (w j).inv ≫ ι g ((e : (a : J) → K) j))
        (π g k)))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g)
        (lift fun (k : K) ↦ π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom sorry)
        (π g k)))
Tactic: ext k j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
k : K
j : J
⊢ Eq.{v + 1} (α := f j ⟶ g k)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (desc fun (j : J) ↦ (w j).inv ≫ ι g ((e : (a : J) → K) j))
        (π g k)))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g)
        (lift fun (k : K) ↦ π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom ⋯)
        (π g k)))
have pos : ∀ (h : k = (e : (a : J) → K) j),
  Eq.{v + 1} (α := f j ⟶ g k)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (desc fun (j : J) ↦ (w j).inv ≫ ι g ((e : (a : J) → K) j))
        (π g k)))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g)
        (lift fun (k : K) ↦ π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom sorry)
        (π g k)))
Tactic: by_cases h : k = e j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
k : K
j : J
pos :
  ∀ (h : k = (e : (a : J) → K) j),
    Eq.{v + 1} (α := f j ⟶ g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
        (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (desc fun (j : J) ↦ (w j).inv ≫ ι g ((e : (a : J) → K) j))
          (π g k)))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
        (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g)
          (lift fun (k : K) ↦ π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom ⋯)
          (π g k)))
⊢ Eq.{v + 1} (α := f j ⟶ g k)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (desc fun (j : J) ↦ (w j).inv ≫ ι g ((e : (a : J) → K) j))
        (π g k)))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g)
        (lift fun (k : K) ↦ π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom ⋯)
        (π g k)))
have neg : ∀ (h : ¬k = (e : (a : J) → K) j),
  Eq.{v + 1} (α := f j ⟶ g k)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (desc fun (j : J) ↦ (w j).inv ≫ ι g ((e : (a : J) → K) j))
        (π g k)))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g)
        (lift fun (k : K) ↦ π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom sorry)
        (π g k)))
Tactic: by_cases h : k = e j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
k : K
j : J
h : k = (e : (a : J) → K) j
⊢ Eq.{v + 1} (α := f j ⟶ g k)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (desc fun (j : J) ↦ (w j).inv ≫ ι g ((e : (a : J) → K) j))
        (π g k)))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g)
        (lift fun (k : K) ↦ π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom ⋯)
        (π g k)))
have pos : Eq.{v + 1} (α := f j ⟶ g ((e : (a : J) → K) j))
  (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (desc fun (j : J) ↦ (w j).inv ≫ ι g ((e : (a : J) → K) j))
      (π g ((e : (a : J) → K) j))))
  (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g)
      (lift fun (k : K) ↦ π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom sorry)
      (π g ((e : (a : J) → K) j))))
Tactic: subst h
Cleared hypotheses: k, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
k : K
j : J
h : ¬k = (e : (a : J) → K) j
⊢ Eq.{v + 1} (α := f j ⟶ g k)
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (desc fun (j : J) ↦ (w j).inv ≫ ι g ((e : (a : J) → K) j))
        (π g k)))
    (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g)
        (lift fun (k : K) ↦ π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom ⋯)
        (π g k)))
have neg : (w j).inv ≫ CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g ((e : (a : J) → K) j)) (π g k) =
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
    (π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom sorry)
Tactic: simp only [ι_desc_assoc, Category.assoc, lift_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
k : K
j : J
h : ¬k = (e : (a : J) → K) j
⊢ (w j).inv ≫ CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g ((e : (a : J) → K) j)) (π g k) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom ⋯)
have neg : (w j).inv ≫ 0 = 0 ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom sorry
Tactic: rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J : Type w
K : Type u_1
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_2 : HasBiproduct.{w, v, u} f
inst_3 : HasBiproduct.{u_1, v, u} g
k : K
j : J
h : ¬k = (e : (a : J) → K) j
neg : (w j).inv ≫ 0 = 0 ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom ⋯
⊢ (w j).inv ≫ CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g ((e : (a : J) → K) j)) (π g k) =
    CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f j)
      (π f ((e.symm : (a : K) → J) k) ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom ⋯)
have neg₁ : j ≠ (e.symm : (a : K) → J) k
Tactic: rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]