awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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 (α := biproduct.{w, v, u} f ⟶ g j) (CategoryStruct.comp (Y := biproduct.{w, v, u} g) (map p) (π g j)) (π f j ≫ p j)

Tactic:
Limits.IsLimit.map_π _ _ _ (Discrete.mk j)

Premises used: CategoryTheory.Limits.IsLimit.map_π, CategoryTheory.Discrete.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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
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)
⊢ 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']

Premises used: CategoryTheory.Limits.biproduct.map_eq_map'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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)

Tactic:
apply
    Limits.IsColimit.ι_map (biproduct.isColimit f) (biproduct.bicone g).toCocone
    (Discrete.natTrans fun j => p j.as) (Discrete.mk j)

Premises used: CategoryTheory.Limits.biproduct.isColimit, CategoryTheory.Limits.biproduct.bicone, CategoryTheory.Limits.IsColimit.ι_map, CategoryTheory.Limits.Bicone.toCocone, CategoryTheory.Discrete.natTrans, CategoryTheory.Discrete.mk, CategoryTheory.Discrete.as
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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
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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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
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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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)
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))
⊢ 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:
ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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 : 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)
⊢ 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:
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, ι_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.ι_π_assoc, CategoryTheory.Limits.biproduct.isoCoproduct_inv, CategoryTheory.Limits.biproduct.map_π, CategoryTheory.Limits.Cofan.mk_ι_app, CategoryTheory.Limits.Cofan.mk_pt, CategoryTheory.Discrete.functor_obj_eq_as, CategoryTheory.Limits.biproduct.isoCoproduct_hom, CategoryTheory.Limits.Sigma.ι_map_assoc, CategoryTheory.Limits.colimit.ι_desc_assoc, CategoryTheory.Limits.biproduct.ι_π, CategoryTheory.Limits.biproduct.ι_desc_assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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 ⋯
w₁ : ¬j_1 = j → Eq.{v + 1} (0 ≫ p j) (p j_1 ≫ 0)
⊢ 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)

Tactic:
split
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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
h : j_1 = j
⊢ eqToHom ⋯ ≫ p j = p j_1 ≫ eqToHom ⋯

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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
h : ¬j_1 = j
⊢ Eq.{v + 1} (0 ≫ p j) (p j_1 ≫ 0)

Tactic:
simp_all
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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))

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
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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))
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))
⊢ Epi (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g) (map p)

Tactic:
rw [this]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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)
    (Iso.hom (isoCoproduct f) ≫ Sigma.map p ≫ Iso.inv (isoCoproduct g))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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)
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))
⊢ 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
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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 (α := piObj.{w, v, u} f ⟶ piObj.{w, v, u} g) (map p : piObj.{w, v, u} f ⟶ 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:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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)
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)
⊢ Epi (X := piObj.{w, v, u} f) (Y := piObj.{w, v, u} g) (map p)

Tactic:
rw [show Pi.map p = (biproduct.isoProduct _).inv ≫ biproduct.map p ≫
    (biproduct.isoProduct _).hom by aesop]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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)
    (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:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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)
⊢ Eq (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} g) (map p)
    (Iso.hom (isoProduct f) ≫ Pi.map p ≫ Iso.inv (isoProduct g))

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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)
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))
⊢ Mono (X := biproduct.{w, v, u} f) (Y := biproduct.{w, v, u} g) (map p)

Tactic:
rw [show biproduct.map p = (biproduct.isoProduct _).hom ≫ Pi.map p ≫
    (biproduct.isoProduct _).inv by aesop]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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)
    (Iso.hom (isoProduct f) ≫ Pi.map p ≫ Iso.inv (isoProduct g))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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)
⊢ Eq (α := sigmaObj.{w, v, u} f ⟶ sigmaObj.{w, v, u} g) (map p : sigmaObj.{w, v, u} f ⟶ 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:
aesop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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)
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)
⊢ Mono (X := sigmaObj.{w, v, u} f) (Y := sigmaObj.{w, v, u} g) (map p)

Tactic:
rw [show Sigma.map p = (biproduct.isoCoproduct _).inv ≫ biproduct.map p ≫
    (biproduct.isoCoproduct _).hom by aesop]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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)
    (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:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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 : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{u_1, v, u} g
k : K
⊢ g k = g ((e : (a : J) → K) ((e.symm : (a : K) → J) k : J))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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 : J → C
g : K → C
e : J ≃ K
w : (j : J) → g ((e : (a : J) → K) j) ≅ f j
inst_6 : HasBiproduct.{w, v, u} f
inst_7 : HasBiproduct.{u_1, v, u} g
k : K
⊢ g ((e : (a : J) → K) ((e.symm : (a : K) → J) k : J)) = g k

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts
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
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 ⋯)
          (π g k)))
⊢ 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 ⋯)

Tactic:
ext k j