awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
simp : (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst = 0
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst + ((0 ≫ biprod.inr) ≫ inv f) ≫ biprod.fst = 0

Tactic:
simp only [zero_comp, add_zero]

Premises used: CategoryTheory.Limits.zero_comp, add_zero
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : biprod.inl ≫ f ≫ biprod.fst
a₃ : biprod.inl
a₄ : inv f
a₅ : biprod.fst
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst

Tactic:
slice 1 3
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : 0
| biprod.inl ≫ f ≫ biprod.fst

Tactic:
rw [a₁]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : 0
a₃ : biprod.inl
a₄ : inv f
a₅ : biprod.fst
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst

Tactic:
slice 1 3
      rw [a₁]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
conv_lhs : Eq (α := W ⟶ W) (((0 ≫ biprod.inl) ≫ inv f) ≫ biprod.fst) 0
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst = 0

Tactic:
conv_lhs =>
      slice 1 3
      rw [a₁]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ Eq (α := W ⟶ W) (((0 ≫ biprod.inl) ≫ inv f) ≫ biprod.fst) 0

Tactic:
simp only [zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
⊢ x = 0

Tactic:
have h₀ : x = 0 := by
    dsimp [x]
    rw [← Category.id_comp (inv f), Category.assoc, ← biprod.total]
    conv_lhs =>
      slice 2 3
      rw [comp_add]
    simp only [Category.assoc]
    rw [comp_add_assoc, add_comp]
    conv_lhs =>
      congr
      next => skip
      slice 1 3
      rw [a₂]
    simp only [zero_comp, add_zero]
    conv_lhs =>
      slice 1 3
      rw [a₁]
    simp only [zero_comp]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
h₀ : x = 0
⊢ False

Tactic:
nz (h₁.symm.trans h₀)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
h₀ : x = 0
⊢ False

Tactic:
exact nz (h₁.symm.trans h₀)

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
intro :
  ∀ (val : Fintype τ), (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
⊢ (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0

Tactic:
cases nonempty_fintype τ

Premises used: nonempty_fintype
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
t : τ
W : C
h : T t ⟶ W
⊢ biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
⊢ ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h

Tactic:
have reassoced {t : τ} {W : C} (h : _ ⟶ W) :
    biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h := by grind
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
⊢ x = 𝟙 (S s)

Tactic:
simp [x]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
⊢ x = 𝟙 (S s)

Tactic:
have h₁ : x = 𝟙 (S s) := by simp [x]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
dsimp : biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s = 0
⊢ x = 0

Tactic:
dsimp [x]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
rw : biproduct.ι S s ≫ f ≫ (∑ j : τ, biproduct.π T j ≫ biproduct.ι T j) ≫ inv f ≫ biproduct.π S s = 0
⊢ biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s = 0

Tactic:
rw [← Category.id_comp (inv f), Category.assoc, ← biproduct.total]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biproduct.total, CategoryTheory.inv, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
simp :
  Eq (α := S s ⟶ S s) ((∑ j : τ, biproduct.ι S s ≫ f ≫ biproduct.π T j ≫ biproduct.ι T j) ≫ inv f ≫ biproduct.π S s) 0
⊢ biproduct.ι S s ≫ f ≫ (∑ j : τ, biproduct.π T j ≫ biproduct.ι T j) ≫ inv f ≫ biproduct.π S s = 0

Tactic:
simp only [comp_sum_assoc]

Premises used: CategoryTheory.Preadditive.comp_sum_assoc
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ Eq (α := S s ⟶ S s) ((∑ j : τ, biproduct.ι S s ≫ f ≫ biproduct.π T j ≫ biproduct.ι T j) ≫ inv f ≫ biproduct.π S s) 0

Tactic:
grind [CategoryTheory.Limits.zero_comp, Finset.sum_const_zero]

Premises used: Finset.sum_const_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
⊢ x = 0

Tactic:
have h₀ : x = 0 := by
    dsimp [x]
    rw [← Category.id_comp (inv f), Category.assoc, ← biproduct.total]
    simp only [comp_sum_assoc]
    grind [CategoryTheory.Limits.zero_comp, Finset.sum_const_zero]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
h₀ : x = 0
⊢ Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0

Tactic:
h₁.symm.trans h₀

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Finite τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
val : Fintype τ
z : ∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0
reassoced : ∀ {t : τ} {W : C} (h : T t ⟶ W), biproduct.ι S s ≫ f ≫ biproduct.π T t ≫ h = 0 ≫ h
x : S s ⟶ S s := biproduct.ι S s ≫ f ≫ inv f ≫ biproduct.π S s
h₁ : x = 𝟙 (S s)
h₀ : x = 0
⊢ Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0

Tactic:
exact h₁.symm.trans h₀

Premises used: Eq.symm, Eq.trans
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
h : ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
⊢ Trunc ((t : τ) ×' biproduct.ι S s ≫ f ≫ biproduct.π T t ≠ 0)

Tactic:
apply truncSigmaOfExists

Premises used: truncSigmaOfExists
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
⊢ (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0

Tactic:
have t := Biproduct.column_nonzero_of_iso'.{v} s f
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
h : ∀ (h : ¬∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0), False
⊢ ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0

Tactic:
by_contra h
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
h : ¬∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
⊢ ∀ (x : τ), biproduct.ι S s ≫ f ≫ biproduct.π T x = 0

Tactic:
simp only [not_exists_not] at h

Premises used: Classical.not_exists_not
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
h : ∀ (x : τ), biproduct.ι S s ≫ f ≫ biproduct.π T x = 0
⊢ False

Tactic:
nz (t h)
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
h : ∀ (x : τ), biproduct.ι S s ≫ f ≫ biproduct.π T x = 0
⊢ False

Tactic:
exact nz (t h)
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
σ τ : Type
inst_2 : Fintype τ
S : σ → C
inst_3 : HasBiproduct.{0, v, u} S
T : τ → C
inst_4 : HasBiproduct.{0, v, u} T
s : σ
nz : Ne.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0
f : biproduct.{0, v, u} S ⟶ biproduct.{0, v, u} T
inst_5 : IsIso f
h : ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
h₁ :
  ∀ (t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0),
    ∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0
h₂ :
  ∀ (t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0)
    (h : ¬∃ (a : τ), biproduct.ι S s ≫ f ≫ biproduct.π T a ≠ 0), False
h₃ :
  ∀ (t : (∀ (t : τ), biproduct.ι S s ≫ f ≫ biproduct.π T t = 0) → Eq.{v + 1} (α := S s ⟶ S s) (𝟙 (S s)) 0)
    (h : ∀ (x : τ), biproduct.ι S s ≫ f ≫ biproduct.π T x = 0), False
⊢ Trunc ((t : τ) ×' biproduct.ι S s ≫ f ≫ biproduct.π T t ≠ 0)

Tactic:
classical
    apply truncSigmaOfExists
    have t := Biproduct.column_nonzero_of_iso'.{v} s f
    by_contra h
    simp only [not_exists_not] at h
    exact nz (t h)

Premises used: truncSigmaOfExists, Classical.not_exists_not
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : PreservesBiproduct f F
c : Cone.{u_1, v, u_1, u} (Discrete.functor f)
hc : IsLimit c
val : Fintype J
as : J
⊢ Eq (α :=
    obj.{u_1, v', u_1, u'}
        (obj (const (Discrete J))
          ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj
              (Bicone.toCone (F.mapBicone (Bicone.ofLimitCone hc)))).pt)
        { as := as : Discrete J } ⟶
      (Discrete.functor f ⋙ F).obj { as := as })
    (((Cone.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj
            (Bicone.toCone (F.mapBicone (Bicone.ofLimitCone hc)))).π.app
      { as := as })
    (Iso.hom
        (Iso.refl
          ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).inv).obj
              (Bicone.toCone (F.mapBicone (Bicone.ofLimitCone hc)))).pt) ≫
      (F.mapCone c).π.app { as := as })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : PreservesLimit (Discrete.functor f) F
b : Bicone.{u_1, v, u} f
hb : b.IsBilimit
val : Fintype J
as : J
⊢ Eq (α :=
    obj.{u_1, v', u_1, u'}
        (obj (const (Discrete J))
          ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).pt)
        { as := as : Discrete J } ⟶
      obj.{u_1, v', u_1, u'} (Discrete.functor (F.obj ∘ f)) { as := as : Discrete J })
    (((Cone.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).π.app { as := as })
    (Iso.hom (Iso.refl ((Cone.postcompose (Discrete.compNatIsoDiscrete f F).hom).obj (F.mapCone b.toCone)).pt) ≫
      (Bicone.toCone (F.mapBicone b)).π.app { as := as })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
change : HasProduct.{u_1, v', u'} (F.obj ∘ f)
⊢ HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)

Tactic:
change HasProduct (F.obj ∘ f)

Premises used: CategoryTheory.Limits.HasProduct, Function.comp, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
⊢ HasProduct.{u_1, v', u'} (F.obj ∘ f)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
D : Type u'
inst_2 : Category.{v', u'} D
inst_3 : Preadditive.{v', u'} D
F : Functor.{v, v', u, u'} C D
inst_4 : F.PreservesZeroMorphisms
J : Type u_1
inst_5 : Finite J
f : J → C
inst_6 : HasBiproduct.{u_1, v, u} f
inst_7 : HasBiproduct.{u_1, v', u'} (F.obj ∘ f)
inst_8 :
  Mono (X := F.obj (biproduct.{u_1, v, u} f)) (Y := biproduct.{u_1, v', u'} (F.obj ∘ f)) (F.biproductComparison f)
⊢ HasProduct.{u_1, v', u'} (C := D) fun (b : J) ↦ F.obj (f b)

Tactic:
haveI : HasProduct fun b => F.obj (f b) := by
    change HasProduct (F.obj ∘ f)
    infer_instance