awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j = 0

Tactic:
apply o.eq_zero h

Premises used: CategoryTheory.HomOrthogonal.eq_zero
-- 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))
h :
  ∀ (j : β) (k : α) (w : j ∈ g ⁻¹' {f k}),
    (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 ⋯)
        ((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))))
          z)
        (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯) =
      z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯)
⊢ (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 ⋯)
      ((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))))
        z) =
    z

Tactic:
ext i ⟨j, w⟩ ⟨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 : (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
h :
  (if h : f k = g j then
        z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j ⋯)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯) ≫
          eqToHom ⋯
      else 0) ≫
      eqToHom ⋯ =
    z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯)
⊢ (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 ⋯)
      ((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))))
        z)
      (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯) =
    z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯)

Tactic:
simp only [eqToHom_refl, biproduct.matrix_components, Category.id_comp]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Limits.biproduct.matrix_components, CategoryTheory.Category.id_comp
-- 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 : α
w : j ∈ g ⁻¹' {f k}
pos :
  ∀ (h : f k = g j),
    (z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j ⋯)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯) ≫
          eqToHom ⋯) ≫
        eqToHom ⋯ =
      z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯)
neg :
  ∀ (h : ¬f k = g j),
    0 ≫ eqToHom ⋯ =
      z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯)
⊢ (if h : f k = g j then
        z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j ⋯)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯) ≫
          eqToHom ⋯
      else 0) ≫
      eqToHom ⋯ =
    z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯)

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 : (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
h : f k = g j
⊢ (z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j ⋯) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯) ≫
        eqToHom ⋯) ≫
      eqToHom ⋯ =
    z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w) (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 : (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i))
j : β
k : α
w : j ∈ g ⁻¹' {f k}
h : ¬f k = g j
neg : False
⊢ 0 ≫ eqToHom ⋯ =
    z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k ⋯)

Tactic:
exfalso
-- 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 : α
w : j ∈ g ⁻¹' {f k}
h : ¬f k = g j
⊢ False

Tactic:
h w.symm

Premises used: Eq.symm
-- 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 : α
w : j ∈ g ⁻¹' {f k}
h : ¬f k = g j
⊢ False

Tactic:
exact h w.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{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 : β → ι
w 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))
h :
  ∀ (x : ι) (i : (↑(g ⁻¹' {x}) : Type)) (j : (↑(f ⁻¹' {x}) : Type)),
    Equiv.toFun o.matrixDecomposition (w + z) x i j =
      (Equiv.toFun o.matrixDecomposition w + Equiv.toFun o.matrixDecomposition z) x i j
⊢ Equiv.toFun o.matrixDecomposition (w + z) = Equiv.toFun o.matrixDecomposition w + Equiv.toFun o.matrixDecomposition z

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{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 : β → ι
w 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))
x : ι
i : (↑(g ⁻¹' {x}) : Type)
j : (↑(f ⁻¹' {x}) : Type)
h :
  eqToHom ⋯ ≫
      (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) (↑j : α) ≫
          (w + z) ≫ biproduct.π (fun (b : β) ↦ s (g b)) (↑i : β)) ≫
        eqToHom ⋯ =
    eqToHom ⋯ ≫
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) (↑j : α) ≫
            w ≫ biproduct.π (fun (b : β) ↦ s (g b)) (↑i : β)) ≫
          eqToHom ⋯ +
      eqToHom ⋯ ≫
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) (↑j : α) ≫
            z ≫ biproduct.π (fun (b : β) ↦ s (g b)) (↑i : β)) ≫
          eqToHom ⋯
⊢ Equiv.toFun o.matrixDecomposition (w + z) x i j =
    (Equiv.toFun o.matrixDecomposition w + Equiv.toFun o.matrixDecomposition z) x i j

Tactic:
dsimp [biproduct.components]

Premises used: CategoryTheory.Limits.biproduct.components
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{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 : β → ι
w 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))
x : ι
i : (↑(g ⁻¹' {x}) : Type)
j : (↑(f ⁻¹' {x}) : Type)
⊢ eqToHom ⋯ ≫
      (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) (↑j : α) ≫
          (w + z) ≫ biproduct.π (fun (b : β) ↦ s (g b)) (↑i : β)) ≫
        eqToHom ⋯ =
    eqToHom ⋯ ≫
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) (↑j : α) ≫
            w ≫ biproduct.π (fun (b : β) ↦ s (g b)) (↑i : β)) ≫
          eqToHom ⋯ +
      eqToHom ⋯ ≫
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) (↑j : α) ≫
            z ≫ biproduct.π (fun (b : β) ↦ s (g b)) (↑i : β)) ≫
          eqToHom ⋯

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α : Type
inst_3 : Finite α
f : α → ι
i : ι
a :
  ∀ (b a : α) (j_property : a ∈ f ⁻¹' {f b}),
    Eq.{v + 1} (α := End (s (f b)))
      (((o.matrixDecomposition :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                  (biproduct.{0, v, u} fun (b : α) ↦ s (f b)) ≃
                ((i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))) :
            (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : α) ↦ s (f b)) →
              (i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
          (𝟙 (biproduct.{0, v, u} fun (a : α) ↦ s (f a))) (f b) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) b ⋯)
          (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property) :
        End (s (f b)))
      (1 (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) b ⋯)
          (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property) :
        End (s (f b)))
⊢ Eq.{v + 1} (α := Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
    (((o.matrixDecomposition :
            Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                (biproduct.{0, v, u} fun (b : α) ↦ s (f b)) ≃
              ((i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))) :
          (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : α) ↦ s (f b)) →
            (i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
        (𝟙 (biproduct.{0, v, u} fun (a : α) ↦ s (f a))) i :
      Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
    (1 : Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))

Tactic:
ext ⟨b, ⟨⟩⟩ ⟨a, j_property⟩
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α : Type
inst_3 : Finite α
f : α → ι
b a : α
j_property : a ∈ f ⁻¹' {f b}
⊢ f a = f b

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property

Premises used: Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α : Type
inst_3 : Finite α
f : α → ι
b a : α
j_property_1 : a ∈ f ⁻¹' {f b}
j_property : f a = f b
a₁ :
  Eq.{v + 1} (α := End (s (f b)))
    (eqToHom ⋯ ≫
      CategoryStruct.comp (Y := biproduct.{0, v, u} fun (a : α) ↦ s (f a))
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a) (biproduct.π (fun (b : α) ↦ s (f b)) b))
    (if
        Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) b ⋯ =
          Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property_1 then
      𝟙 (s (f b))
    else 0)
⊢ Eq.{v + 1} (α := End (s (f b)))
    (((o.matrixDecomposition :
            Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                (biproduct.{0, v, u} fun (b : α) ↦ s (f b)) ≃
              ((i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))) :
          (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : α) ↦ s (f b)) →
            (i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
        (𝟙 (biproduct.{0, v, u} fun (a : α) ↦ s (f a))) (f b) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) b ⋯)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property_1) :
      End (s (f b)))
    (1 (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) b ⋯)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property_1) :
      End (s (f b)))

Tactic:
simp only [Category.comp_id, Category.id_comp, End.one_def, eqToHom_refl,
    Matrix.one_apply, HomOrthogonal.matrixDecomposition_apply, biproduct.components]

Premises used: Matrix.one_apply, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.HomOrthogonal.matrixDecomposition_apply, CategoryTheory.End.one_def, CategoryTheory.Limits.biproduct.components, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α : Type
inst_3 : Finite α
f : α → ι
b a : α
j_property_1 : a ∈ f ⁻¹' {f b}
j_property : f a = f b
pos :
  ∀
    (h :
      Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) b ⋯ =
        Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property_1),
    Eq.{v + 1} (α := End (s (f b)))
      (eqToHom ⋯ ≫
        CategoryStruct.comp (Y := biproduct.{0, v, u} fun (a : α) ↦ s (f a))
          (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a) (biproduct.π (fun (b : α) ↦ s (f b)) b))
      (𝟙 (s (f b)))
neg :
  ∀
    (h :
      ¬Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) b ⋯ =
          Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property_1),
    Eq.{v + 1} (α := End (s (f b)))
      (eqToHom ⋯ ≫
        CategoryStruct.comp (Y := biproduct.{0, v, u} fun (a : α) ↦ s (f a))
          (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a) (biproduct.π (fun (b : α) ↦ s (f b)) b))
      0
⊢ Eq.{v + 1} (α := End (s (f b)))
    (eqToHom ⋯ ≫
      CategoryStruct.comp (Y := biproduct.{0, v, u} fun (a : α) ↦ s (f a))
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a) (biproduct.π (fun (b : α) ↦ s (f b)) b))
    (if
        Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) b ⋯ =
          Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property_1 then
      𝟙 (s (f b))
    else 0)

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 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α : Type
inst_3 : Finite α
f : α → ι
b a : α
j_property_1 : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) b ⋯ = Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property_1
pos :
  ∀ (j_property : b ∈ f ⁻¹' {f b}) (j_property_2 : f b = f b),
    Eq.{v + 1} (α := End (s (f b)))
      (eqToHom ⋯ ≫
        CategoryStruct.comp (Y := biproduct.{0, v, u} fun (a : α) ↦ s (f a))
          (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) b) (biproduct.π (fun (b : α) ↦ s (f b)) b))
      (𝟙 (s (f b)))
⊢ Eq.{v + 1} (α := End (s (f b)))
    (eqToHom ⋯ ≫
      CategoryStruct.comp (Y := biproduct.{0, v, u} fun (a : α) ↦ s (f a))
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a) (biproduct.π (fun (b : α) ↦ s (f b)) b))
    (𝟙 (s (f b)))

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α : Type
inst_3 : Finite α
f : α → ι
b : α
j_property_1 : b ∈ f ⁻¹' {f b}
j_property : f b = f b
⊢ Eq.{v + 1} (α := End (s (f b)))
    (eqToHom ⋯ ≫
      CategoryStruct.comp (Y := biproduct.{0, v, u} fun (a : α) ↦ s (f a))
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) b) (biproduct.π (fun (b : α) ↦ s (f b)) b))
    (𝟙 (s (f b)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α : Type
inst_3 : Finite α
f : α → ι
b a : α
j_property_1 : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h :
  ¬Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) b ⋯ = Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property_1
⊢ ¬b = a

Tactic:
simp only [Subtype.mk.injEq] at h

Premises used: Subtype.mk.injEq
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α : Type
inst_3 : Finite α
f : α → ι
b a : α
j_property_1 : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬b = a
⊢ Eq.{v + 1} (α := s (f b) ⟶ s (f b)) (eqToHom ⋯ ≫ 0) 0

Tactic:
comp_zero

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α : Type
inst_3 : Finite α
f : α → ι
b a : α
j_property_1 : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬b = a
h₁ :
  Eq.{v + 1} (α := s (f a) ⟶ s (f b))
    (CategoryStruct.comp (Y := biproduct.{0, v, u} fun (a : α) ↦ s (f a))
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a) (biproduct.π (fun (b : α) ↦ s (f b)) b) :
      s (f a) ⟶ s (f b))
    (0 : s (f a) ⟶ s (f b))
⊢ Eq.{v + 1} (α := End (s (f b)))
    (eqToHom ⋯ ≫
      CategoryStruct.comp (Y := biproduct.{0, v, u} fun (a : α) ↦ s (f a))
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a) (biproduct.π (fun (b : α) ↦ s (f b)) b))
    0

Tactic:
convert! comp_zero

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α : Type
inst_3 : Finite α
f : α → ι
b a : α
j_property_1 : a ∈ f ⁻¹' {f b}
j_property : f a = f b
h : ¬b = a
⊢ Eq.{v + 1} (α := s (f a) ⟶ s (f b))
    (CategoryStruct.comp (Y := biproduct.{0, v, u} fun (a : α) ↦ s (f a))
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a) (biproduct.π (fun (b : α) ↦ s (f b)) b) :
      s (f a) ⟶ s (f b))
    (0 : s (f a) ⟶ s (f b))

Tactic:
simpa using biproduct.ι_π_ne _ (Ne.symm h)

Premises used: Ne.symm, CategoryTheory.Limits.biproduct.ι_π_ne
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β γ : Type
inst_3 : Finite α
inst_4 : Fintype β
inst_5 : Finite γ
f : α → ι
g : β → ι
h : γ → ι
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 : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) (biproduct.{0, v, u} fun (c : γ) ↦ s (h c))
c : γ
a : α
j_property : a ∈ f ⁻¹' {h c}
⊢ f a = h c

Tactic:
simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property

Premises used: Set.mem_singleton_iff, Set.mem_preimage
-- Module: Mathlib.CategoryTheory.Preadditive.HomOrthogonal
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β γ : Type
inst_3 : Finite α
inst_4 : Fintype β
inst_5 : Finite γ
f : α → ι
g : β → ι
h : γ → ι
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 : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) (biproduct.{0, v, u} fun (c : γ) ↦ s (h c))
c : γ
a : α
j_property_1 : a ∈ f ⁻¹' {h c}
j_property : f a = h c
rw :
  eqToHom ⋯ ≫
    biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
      z ≫
        ((∑ j : β, biproduct.π (fun (b : β) ↦ s (g b)) j ≫ biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) j) ≫
            w) ≫
          biproduct.π (fun (b : γ) ↦ s (h b)) c
| eqToHom ⋯ ≫ biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫ z ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c

Tactic:
rw [← Category.id_comp w, ← biproduct.total]

Premises used: CategoryTheory.Limits.biproduct.total, CategoryTheory.Category.id_comp