awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
T : Monad.{v₁, u₁} C
inst_2 : T.Additive
U : Comonad.{v₁, u₁} C
inst_3 : U.Additive
F G : U.Coalgebra
α : F ⟶ G
⊢ F.a ≫ U.map (-α.f) = (-α.f) ≫ G.a

Tactic:
simp only [Functor.map_neg, comp_neg, Comonad.Coalgebra.Hom.h, neg_comp]

Premises used: CategoryTheory.Preadditive.comp_neg, CategoryTheory.Comonad.Coalgebra.Hom.h, CategoryTheory.Preadditive.neg_comp, CategoryTheory.Functor.map_neg
-- Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
T : Monad.{v₁, u₁} C
inst_2 : T.Additive
U : Comonad.{v₁, u₁} C
inst_3 : U.Additive
F G : U.Coalgebra
α β : F ⟶ G
⊢ F.a ≫ U.map (α.f - β.f) = (α.f - β.f) ≫ G.a

Tactic:
simp only [Functor.map_sub, comp_sub, Comonad.Coalgebra.Hom.h, sub_comp]

Premises used: CategoryTheory.Comonad.Coalgebra.Hom.h, CategoryTheory.Functor.map_sub, CategoryTheory.Preadditive.comp_sub, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
T : Monad.{v₁, u₁} C
inst_2 : T.Additive
U : Comonad.{v₁, u₁} C
inst_3 : U.Additive
F G : U.Coalgebra
r : ℤ
α : F ⟶ G
rw : F.a ≫ (r • U.map α.f) = (r • α.f) ≫ G.a
rw₁ : r • F.a ≫ U.map α.f = (r • α.f) ≫ G.a
rw₂ : r • α.f ≫ G.a = (r • α.f) ≫ G.a
rw₃ rw₄ : r • α.f ≫ G.a = r • α.f ≫ G.a
⊢ F.a ≫ U.map (r • α.f) = (r • α.f) ≫ G.a

Tactic:
rw [Functor.map_zsmul, comp_zsmul, Comonad.Coalgebra.Hom.h, zsmul_comp]

Premises used: CategoryTheory.Functor.map_zsmul, CategoryTheory.Comonad.Coalgebra.Hom.h, CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.Preadditive.zsmul_comp
-- Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
α β : A₁ ⟶ A₂
⊢ F.map (α.f + β.f) ≫ A₂.str = A₁.str ≫ (α.f + β.f)

Tactic:
simp only [Functor.map_add, add_comp, Endofunctor.Algebra.Hom.h, comp_add]

Premises used: CategoryTheory.Functor.map_add, CategoryTheory.Preadditive.add_comp, CategoryTheory.Endofunctor.Algebra.Hom.h, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
⊢ F.map 0 ≫ A₂.str = A₁.str ≫ 0

Tactic:
simp only [Functor.map_zero, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
n : ℕ
α : A₁ ⟶ A₂
rw : F.map (n • α.f) ≫ A₂.str = n • A₁.str ≫ α.f
rw₁ : (n • F.map α.f) ≫ A₂.str = n • A₁.str ≫ α.f
rw₂ : n • F.map α.f ≫ A₂.str = n • A₁.str ≫ α.f
rw₃ rw₄ : n • A₁.str ≫ α.f = n • A₁.str ≫ α.f
⊢ F.map (n • α.f) ≫ A₂.str = A₁.str ≫ (n • α.f)

Tactic:
rw [comp_nsmul, Functor.map_nsmul, nsmul_comp, Endofunctor.Algebra.Hom.h]

Premises used: CategoryTheory.Preadditive.nsmul_comp, CategoryTheory.Endofunctor.Algebra.Hom.h, CategoryTheory.Preadditive.comp_nsmul, CategoryTheory.Functor.map_nsmul
-- Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
α : A₁ ⟶ A₂
⊢ F.map (-α.f) ≫ A₂.str = A₁.str ≫ (-α.f)

Tactic:
simp only [Functor.map_neg, neg_comp, Endofunctor.Algebra.Hom.h, comp_neg]

Premises used: CategoryTheory.Preadditive.comp_neg, CategoryTheory.Endofunctor.Algebra.Hom.h, CategoryTheory.Preadditive.neg_comp, CategoryTheory.Functor.map_neg
-- Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
α β : A₁ ⟶ A₂
⊢ F.map (α.f - β.f) ≫ A₂.str = A₁.str ≫ (α.f - β.f)

Tactic:
simp only [Functor.map_sub, sub_comp, Endofunctor.Algebra.Hom.h, comp_sub]

Premises used: CategoryTheory.Functor.map_sub, CategoryTheory.Endofunctor.Algebra.Hom.h, CategoryTheory.Preadditive.comp_sub, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Algebra F
r : ℤ
α : A₁ ⟶ A₂
rw : F.map (r • α.f) ≫ A₂.str = r • A₁.str ≫ α.f
rw₁ : (r • F.map α.f) ≫ A₂.str = r • A₁.str ≫ α.f
rw₂ : r • F.map α.f ≫ A₂.str = r • A₁.str ≫ α.f
rw₃ rw₄ : r • A₁.str ≫ α.f = r • A₁.str ≫ α.f
⊢ F.map (r • α.f) ≫ A₂.str = A₁.str ≫ (r • α.f)

Tactic:
rw [comp_zsmul, Functor.map_zsmul, zsmul_comp, Endofunctor.Algebra.Hom.h]

Premises used: CategoryTheory.Functor.map_zsmul, CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.Endofunctor.Algebra.Hom.h, CategoryTheory.Preadditive.zsmul_comp
-- Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Coalgebra F
α β : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (α.f + β.f) = (α.f + β.f) ≫ A₂.str

Tactic:
simp only [Functor.map_add, comp_add, Endofunctor.Coalgebra.Hom.h, add_comp]

Premises used: CategoryTheory.Functor.map_add, CategoryTheory.Preadditive.add_comp, CategoryTheory.Endofunctor.Coalgebra.Hom.h, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Coalgebra F
⊢ A₁.str ≫ F.map 0 = 0 ≫ A₂.str

Tactic:
simp only [Functor.map_zero, zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Functor.map_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Coalgebra F
n : ℕ
α : A₁ ⟶ A₂
rw : A₁.str ≫ (n • F.map α.f) = (n • α.f) ≫ A₂.str
rw₁ : n • A₁.str ≫ F.map α.f = (n • α.f) ≫ A₂.str
rw₂ : n • α.f ≫ A₂.str = (n • α.f) ≫ A₂.str
rw₃ rw₄ : n • α.f ≫ A₂.str = n • α.f ≫ A₂.str
⊢ A₁.str ≫ F.map (n • α.f) = (n • α.f) ≫ A₂.str

Tactic:
rw [Functor.map_nsmul, comp_nsmul, Endofunctor.Coalgebra.Hom.h, nsmul_comp]

Premises used: CategoryTheory.Preadditive.nsmul_comp, CategoryTheory.Endofunctor.Coalgebra.Hom.h, CategoryTheory.Preadditive.comp_nsmul, CategoryTheory.Functor.map_nsmul
-- Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Coalgebra F
α : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (-α.f) = (-α.f) ≫ A₂.str

Tactic:
simp only [Functor.map_neg, comp_neg, Endofunctor.Coalgebra.Hom.h, neg_comp]

Premises used: CategoryTheory.Preadditive.comp_neg, CategoryTheory.Endofunctor.Coalgebra.Hom.h, CategoryTheory.Preadditive.neg_comp, CategoryTheory.Functor.map_neg
-- Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Coalgebra F
α β : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (α.f - β.f) = (α.f - β.f) ≫ A₂.str

Tactic:
simp only [Functor.map_sub, comp_sub, Endofunctor.Coalgebra.Hom.h, sub_comp]

Premises used: CategoryTheory.Functor.map_sub, CategoryTheory.Endofunctor.Coalgebra.Hom.h, CategoryTheory.Preadditive.comp_sub, CategoryTheory.Preadditive.sub_comp
-- Module: Mathlib.CategoryTheory.Preadditive.EndoFunctor
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
F : Functor.{v₁, v₁, u₁, u₁} C C
inst_2 : F.Additive
A₁ A₂ : Coalgebra F
r : ℤ
α : A₁ ⟶ A₂
rw : A₁.str ≫ (r • F.map α.f) = (r • α.f) ≫ A₂.str
rw₁ : r • A₁.str ≫ F.map α.f = (r • α.f) ≫ A₂.str
rw₂ : r • α.f ≫ A₂.str = (r • α.f) ≫ A₂.str
rw₃ rw₄ : r • α.f ≫ A₂.str = r • α.f ≫ A₂.str
⊢ A₁.str ≫ F.map (r • α.f) = (r • α.f) ≫ A₂.str

Tactic:
rw [Functor.map_zsmul, comp_zsmul, Endofunctor.Coalgebra.Hom.h, zsmul_comp]

Premises used: CategoryTheory.Functor.map_zsmul, CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.Endofunctor.Coalgebra.Hom.h, CategoryTheory.Preadditive.zsmul_comp
-- Module: Mathlib.CategoryTheory.Preadditive.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
n : ℕ
α : F ⟶ G
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ (n • α.app) Y = (n • α.app) X ≫ G.map f

Tactic:
simp only [Pi.smul_apply, comp_nsmul, NatTrans.naturality, nsmul_comp]

Premises used: CategoryTheory.Preadditive.nsmul_comp, CategoryTheory.NatTrans.naturality, CategoryTheory.Preadditive.comp_nsmul, Pi.smul_apply
-- Module: Mathlib.CategoryTheory.Preadditive.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
n : ℤ
α : F ⟶ G
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ (n • α.app) Y = (n • α.app) X ≫ G.map f

Tactic:
simp only [Pi.smul_apply, comp_zsmul, NatTrans.naturality, zsmul_comp]

Premises used: CategoryTheory.Preadditive.comp_zsmul, CategoryTheory.NatTrans.naturality, CategoryTheory.Preadditive.zsmul_comp, Pi.smul_apply
-- Module: Mathlib.CategoryTheory.Preadditive.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
X : C
⊢ Eq.{v_2 + 1} (α := F.obj X ⟶ G.obj X) (app 0 X) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
X : C
α β : F ⟶ G
⊢ (α + β).app X = α.app X + β.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
X : C
α β : F ⟶ G
⊢ (α - β).app X = α.app X - β.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
X : C
α : F ⟶ G
⊢ (-α).app X = -α.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
X : C
α : F ⟶ G
n : ℕ
⊢ (n • α).app X = n • α.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
X : C
α : F ⟶ G
n : ℤ
⊢ (n • α).app X = n • α.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
X : C
α : F ⟶ G
n : ℤˣ
⊢ (n • α).app X = n • α.app X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Preadditive.FunctorCategory
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Preadditive.{v_2, u_2} D
F G : Functor.{v_1, v_2, u_1, u_2} C D
ι : Type u_3
s : Finset ι
X : C
α : ι → (F ⟶ G)
⊢ Eq.{v_2 + 1} (α := F.obj X ⟶ G.obj X) (app (∑ i ∈ s, α i) X) (∑ i ∈ s, (α i).app X)

Tactic:
simp only [← appHom_apply, map_sum]

Premises used: map_sum, CategoryTheory.NatTrans.appHom_apply
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
i j : ι
w : i ≠ j
f : s i ⟶ s j
⊢ f = 0

Tactic:
(o w).elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_3 : Finite α
inst_4 : Finite β
f : α → ι
g : β → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
i : ι
j : (↑(g ⁻¹' {i}) : Type)
k : (↑(f ⁻¹' {i}) : Type)
rcases :
  ∀ (k : α) (j : (↑(g ⁻¹' {f k}) : Type)), s (f k) = s (f (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯) : α))
⊢ s i = s (f (↑k : α))

Tactic:
rcases k with ⟨k, ⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_3 : Finite α
inst_4 : Finite β
f : α → ι
g : β → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
k : α
j : (↑(g ⁻¹' {f k}) : Type)
⊢ s (f k) = s (f (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯) : α))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_3 : Finite α
inst_4 : Finite β
f : α → ι
g : β → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
i : ι
j : (↑(g ⁻¹' {i}) : Type)
k : (↑(f ⁻¹' {i}) : Type)
rcases :
  ∀ (j : β) (k : (↑(f ⁻¹' {g j}) : Type)), s (g (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {g j}) j ⋯) : β)) = s (g j)
⊢ s (g (↑j : β)) = s i

Tactic:
rcases j with ⟨j, ⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_3 : Finite α
inst_4 : Finite β
f : α → ι
g : β → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
j : β
k : (↑(f ⁻¹' {g j}) : Type)
⊢ s (g (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {g j}) j ⋯) : β)) = s (g j)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_3 : Finite α
inst_4 : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i))
j : α
k : β
h : f j = g k
⊢ k ∈ g ⁻¹' {f j}

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_3 : Finite α
inst_4 : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i))
j : α
k : β
h : f j = g k
⊢ j ∈ f ⁻¹' {f j}

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_3 : Finite α
inst_4 : Finite β
f : α → ι
g : β → ι
z : (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i))
j : α
k : β
h : f j = g k
⊢ s (f j) = s (g k)

Tactic:
simp [h]
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_3 : Finite α
inst_4 : Finite β
f : α → ι
g : β → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
w :
  ∀ (j : β) (k : α),
    CategoryStruct.comp (Y := biproduct.{0, v, u} fun (a : α) ↦ s (f a))
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k)
        (CategoryStruct.comp (Y := biproduct.{0, v, u} fun (b : β) ↦ s (g b))
          ((fun (z : (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i))) ↦
              (biproduct.matrix fun (j : α) (k : β) ↦
                  if h : f j = g k then
                    z (f j) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f j}) k ⋯)
                        (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f j}) j ⋯) ≫
                      eqToHom ⋯
                  else 0 :
                Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                  (biproduct.{0, v, u} fun (b : β) ↦ s (g b))))
            ((fun
                  (z :
                    Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                      (biproduct.{0, v, u} fun (b : β) ↦ s (g b)))
                  (i : ι) (j : (↑(g ⁻¹' {i}) : Type)) (k : (↑(f ⁻¹' {i}) : Type)) ↦
                eqToHom ⋯ ≫ biproduct.components z (↑k : α) (↑j : β) ≫ eqToHom ⋯)
              z))
          (biproduct.π (fun (b : β) ↦ s (g b)) j)) =
      biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j
⊢ (fun (z : (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i))) ↦
        (biproduct.matrix fun (j : α) (k : β) ↦
            if h : f j = g k then
              z (f j) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f j}) k ⋯)
                  (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f j}) j ⋯) ≫
                eqToHom ⋯
            else 0 :
          Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
            (biproduct.{0, v, u} fun (b : β) ↦ s (g b))))
      ((fun
            (z :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                (biproduct.{0, v, u} fun (b : β) ↦ s (g b)))
            (i : ι) (j : (↑(g ⁻¹' {i}) : Type)) (k : (↑(f ⁻¹' {i}) : Type)) ↦
          eqToHom ⋯ ≫ biproduct.components z (↑k : α) (↑j : β) ≫ eqToHom ⋯)
        z) =
    z

Tactic:
ext j k
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_3 : Finite α
inst_4 : Finite β
f : α → ι
g : β → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
j : β
k : α
w :
  (if h : f k = g j then (eqToHom ⋯ ≫ biproduct.components z k j ≫ eqToHom ⋯) ≫ eqToHom ⋯ else 0) =
    biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j
⊢ CategoryStruct.comp (Y := biproduct.{0, v, u} fun (a : α) ↦ s (f a))
      (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k)
      (CategoryStruct.comp (Y := biproduct.{0, v, u} fun (b : β) ↦ s (g b))
        ((fun (z : (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i))) ↦
            (biproduct.matrix fun (j : α) (k : β) ↦
                if h : f j = g k then
                  z (f j) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f j}) k ⋯)
                      (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f j}) j ⋯) ≫
                    eqToHom ⋯
                else 0 :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                (biproduct.{0, v, u} fun (b : β) ↦ s (g b))))
          ((fun
                (z :
                  Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                    (biproduct.{0, v, u} fun (b : β) ↦ s (g b)))
                (i : ι) (j : (↑(g ⁻¹' {i}) : Type)) (k : (↑(f ⁻¹' {i}) : Type)) ↦
              eqToHom ⋯ ≫ biproduct.components z (↑k : α) (↑j : β) ≫ eqToHom ⋯)
            z))
        (biproduct.π (fun (b : β) ↦ s (g b)) j)) =
    biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j

Tactic:
simp only [biproduct.matrix_π, biproduct.ι_desc]

Premises used: CategoryTheory.Limits.biproduct.ι_desc, CategoryTheory.Limits.biproduct.matrix_π
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_3 : Finite α
inst_4 : Finite β
f : α → ι
g : β → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
j : β
k : α
pos :
  ∀ (h : f k = g j),
    (eqToHom ⋯ ≫ biproduct.components z k j ≫ eqToHom ⋯) ≫ eqToHom ⋯ =
      biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j
neg :
  ∀ (h : ¬f k = g j),
    0 = biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j
⊢ (if h : f k = g j then (eqToHom ⋯ ≫ biproduct.components z k j ≫ eqToHom ⋯) ≫ eqToHom ⋯ else 0) =
    biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j

Tactic:
split_ifs with h
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_3 : Finite α
inst_4 : Finite β
f : α → ι
g : β → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
j : β
k : α
h : f k = g j
pos :
  biproduct.components z k j =
    biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j
⊢ (eqToHom ⋯ ≫ biproduct.components z k j ≫ eqToHom ⋯) ≫ eqToHom ⋯ =
    biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_3 : Finite α
inst_4 : Finite β
f : α → ι
g : β → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
j : β
k : α
h : f k = g j
⊢ biproduct.components z k j =
    biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_3 : Finite α
inst_4 : Finite β
f : α → ι
g : β → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
j : β
k : α
h : ¬f k = g j
neg : biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j = 0
⊢ 0 = biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j

Tactic:
symm