awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)))
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 ⋯)
          (π 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)))

Tactic:
by_cases h : k = e j

Premises used: DFunLike.coe
-- 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
k : K
j : J
h : k = (e : (a : J) → K) j
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 ⋯)
        (π g ((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)))

Tactic:
subst h
-- 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
j : J
⊢ 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 ⋯)
        (π g ((e : (a : J) → K) j))))

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
k : K
j : J
h : ¬k = (e : (a : J) → K) j
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 ⋯)
⊢ 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)))

Tactic:
simp only [ι_desc_assoc, Category.assoc, lift_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.ι_desc_assoc, CategoryTheory.Limits.biproduct.lift_π
-- 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
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 ⋯
neg₁ : j ≠ (e.symm : (a : K) → J) k
neg₂ : (e : (a : J) → K) j ≠ k
⊢ (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 ⋯)

Tactic:
rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]

Premises used: CategoryTheory.Limits.biproduct.ι_π_ne, CategoryTheory.Limits.biproduct.ι_π_ne_assoc
-- 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
k : K
j : J
h : ¬k = (e : (a : J) → K) j
⊢ (w j).inv ≫ 0 = 0 ≫ Iso.inv (w ((e.symm : (a : K) → J) k)) ≫ eqToHom ⋯

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
k : K
h : ¬k = (e : (a : J) → K) ((e.symm : (a : K) → J) k : J)
⊢ False

Tactic:
simp at h
-- 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
k : K
j : J
h : ¬k = (e : (a : J) → K) j
⊢ (e : (a : J) → K) j ≠ k

Tactic:
Ne.symm h

Premises used: Ne.symm
-- 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
k : K
j : J
h : ¬k = (e : (a : J) → K) j
⊢ (e : (a : J) → K) j ≠ k

Tactic:
exact Ne.symm h

Premises used: Ne.symm
-- 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₁ :
  ∀ (j : J) (k : K),
    Eq.{v + 1} (α := g k ⟶ f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
          (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
          (π f j)))
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
          (π f j)))
⊢ Eq.{v + 1} (α := biproduct.{u_1, v, u} g ⟶ biproduct.{w, v, u} f)
    (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
    (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)

Tactic:
ext j k
-- 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
j : J
k : K
pos :
  ∀ (h : k = (e : (a : J) → K) j),
    Eq.{v + 1} (α := g k ⟶ f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
          (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
          (π f j)))
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
          (π f j)))
neg :
  ∀ (h : ¬k = (e : (a : J) → K) j),
    Eq.{v + 1} (α := g k ⟶ f j)
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
          (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
          (π f j)))
      (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
        (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
          (π f j)))
⊢ Eq.{v + 1} (α := g k ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
        (π f j)))
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
        (π f j)))

Tactic:
by_cases h : k = e j

Premises used: DFunLike.coe
-- 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
j : J
k : K
h : k = (e : (a : J) → K) j
pos :
  Eq.{v + 1} (α := g ((e : (a : J) → K) j) ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g ((e : (a : J) → K) j))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
        (π f j)))
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g ((e : (a : J) → K) j))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
        (π f j)))
⊢ Eq.{v + 1} (α := g k ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
        (π f j)))
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
        (π f j)))

Tactic:
subst h
-- 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
j : J
⊢ Eq.{v + 1} (α := g ((e : (a : J) → K) j) ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g ((e : (a : J) → K) j))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
        (π f j)))
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g ((e : (a : J) → K) j))
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
        (π f j)))

Tactic:
simp only [ι_desc_assoc, ← eqToHom_iso_hom_naturality_assoc w (e.symm_apply_apply j).symm,
      Equiv.symm_apply_apply, eqToHom_comp_ι, Category.assoc, bicone_ι_π_self, Category.comp_id,
      lift_π, bicone_ι_π_self_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.bicone_ι_π_self_assoc, CategoryTheory.eqToHom_iso_hom_naturality_assoc, Equiv.symm_apply_apply, CategoryTheory.Category.comp_id, CategoryTheory.Limits.bicone_ι_π_self, CategoryTheory.Limits.biproduct.eqToHom_comp_ι, CategoryTheory.Limits.biproduct.ι_desc_assoc, CategoryTheory.Limits.biproduct.lift_π, Eq.symm
-- 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
j : J
k : K
h : ¬k = (e : (a : J) → K) j
neg :
  eqToHom ⋯ ≫
      Iso.hom (w ((e.symm : (a : K) → J) k)) ≫
        CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f ((e.symm : (a : K) → J) k)) (π f j) =
    CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k) (π g ((e : (a : J) → K) j) ≫ (w j).hom)
⊢ Eq.{v + 1} (α := g k ⟶ f j)
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f)
        (desc fun (k : K) ↦ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ ι f ((e.symm : (a : K) → J) k))
        (π f j)))
    (CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k)
      (CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift fun (j : J) ↦ π g ((e : (a : J) → K) j) ≫ (w j).hom)
        (π f j)))

Tactic:
simp only [ι_desc_assoc, Category.assoc, lift_π]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.ι_desc_assoc, CategoryTheory.Limits.biproduct.lift_π
-- 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
j : J
k : K
h : ¬k = (e : (a : J) → K) j
neg : eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ 0 = 0 ≫ (w j).hom
neg₁ : k ≠ (e : (a : J) → K) j
neg₂ : (e.symm : (a : K) → J) k ≠ j
⊢ eqToHom ⋯ ≫
      Iso.hom (w ((e.symm : (a : K) → J) k)) ≫
        CategoryStruct.comp (Y := biproduct.{w, v, u} f) (ι f ((e.symm : (a : K) → J) k)) (π f j) =
    CategoryStruct.comp (Y := biproduct.{u_1, v, u} g) (ι g k) (π g ((e : (a : J) → K) j) ≫ (w j).hom)

Tactic:
rw [biproduct.ι_π_ne, biproduct.ι_π_ne_assoc]

Premises used: CategoryTheory.Limits.biproduct.ι_π_ne, CategoryTheory.Limits.biproduct.ι_π_ne_assoc
-- 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
j : J
k : K
h : ¬k = (e : (a : J) → K) j
⊢ eqToHom ⋯ ≫ Iso.hom (w ((e.symm : (a : K) → J) k)) ≫ 0 = 0 ≫ (w j).hom

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
j : J
k : K
h : ¬k = (e : (a : J) → K) j
⊢ k ≠ (e : (a : J) → K) j

Tactic:
h
-- 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
j : J
k : K
h : ¬k = (e : (a : J) → K) j
⊢ k ≠ (e : (a : J) → K) j

Tactic:
exact h
-- 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
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst_6 : ∀ (i : ι), HasBiproduct.{u_2, v, u} (g i)
inst_7 : HasBiproduct.{u_3, v, u} (C := C) fun (i : ι) ↦ biproduct.{u_2, v, u} (g i)
x_1 x_2 : (i : ι) × f i
j : ι
x : f j
⊢ Eq.{v + 1} (α :=
    g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)) ⟶
      g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)))
    (CategoryStruct.comp (Y := biproduct.{u_3, v, u} fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
      (CategoryStruct.comp (Y :=
        biproduct.{u_2, v, u} (J := f ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
        (biproduct.ι (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)))
        (biproduct.ι.{u_3, v, u} (C := C) (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
      (biproduct.π (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)) ≫
        biproduct.π (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i))))
    (eqToHom ⋯)

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
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst_6 : ∀ (i : ι), HasBiproduct.{u_2, v, u} (g i)
inst_7 : HasBiproduct.{u_3, v, u} (C := C) fun (i : ι) ↦ biproduct.{u_2, v, u} (g i)
x_1 x_2 : (i : ι) × f i
j : ι
x : f j
j' : ι
y : f j'
h : ¬Sigma.mk (β := fun (i : ι) ↦ f i) j x = Sigma.mk (β := fun (i : ι) ↦ f i) j' y
⊢ j = j' → ¬x ≍ y

Tactic:
simp only [Sigma.mk.inj_iff, not_and] at h

Premises used: Sigma.mk.inj_iff, not_and
-- 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
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst_6 : ∀ (i : ι), HasBiproduct.{u_2, v, u} (g i)
inst_7 : HasBiproduct.{u_3, v, u} (C := C) fun (i : ι) ↦ biproduct.{u_2, v, u} (g i)
x_1 x_2 : (i : ι) × f i
j : ι
x y : f j
h : j = j → ¬x ≍ y
⊢ ¬x = y

Tactic:
simp only [heq_eq_eq, forall_true_left] at h

Premises used: forall_true_left, heq_eq_eq
-- 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
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst_6 : ∀ (i : ι), HasBiproduct.{u_2, v, u} (g i)
inst_7 : HasBiproduct.{u_3, v, u} (C := C) fun (i : ι) ↦ biproduct.{u_2, v, u} (g i)
x_1 x_2 : (i : ι) × f i
j : ι
x y : f j
h : ¬x = y
⊢ Eq.{v + 1} (α :=
    g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)) ⟶
      g ((Sigma.mk (β := fun (i : ι) ↦ f i) j y).fst (β := fun (i : ι) ↦ f i))
        ((Sigma.mk (β := fun (i : ι) ↦ f i) j y).snd (β := fun (i : ι) ↦ f i)))
    (CategoryStruct.comp (Y := biproduct.{u_3, v, u} fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
      (CategoryStruct.comp (Y :=
        biproduct.{u_2, v, u} (J := f ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
        (biproduct.ι (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).snd (β := fun (i : ι) ↦ f i)))
        (biproduct.ι.{u_3, v, u} (C := C) (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j x).fst (β := fun (i : ι) ↦ f i))))
      (biproduct.π (fun (i : ι) ↦ biproduct.{u_2, v, u} (g i))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j y).fst (β := fun (i : ι) ↦ f i)) ≫
        biproduct.π (g ((Sigma.mk (β := fun (i : ι) ↦ f i) j y).fst (β := fun (i : ι) ↦ f i)))
          ((Sigma.mk (β := fun (i : ι) ↦ f i) j y).snd (β := fun (i : ι) ↦ f i))))
    0

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

Premises used: CategoryTheory.Limits.biproduct.ι_π_ne