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 : 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
a₁ :
  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 =
    ∑ x : (↑(g ⁻¹' {h c}) : Type),
      eqToHom ⋯ ≫
        biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
          z ≫
            biproduct.π (fun (b : β) ↦ s (g b)) (↑x : β) ≫
              biproduct.ι.{0, v, u} (C := C) (fun (a : β) ↦ s (g a)) (↑x : β) ≫
                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 =
    ∑ x : (↑(g ⁻¹' {h c}) : Type),
      eqToHom ⋯ ≫
        biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
          z ≫
            biproduct.π (fun (b : β) ↦ s (g b)) (↑x : β) ≫
              biproduct.ι.{0, v, u} (C := C) (fun (a : β) ↦ s (g a)) (↑x : β) ≫
                w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c

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

Premises used: CategoryTheory.Limits.biproduct.total, 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 α
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
a₁ :
  Eq.{v + 1} (α := End (s (h c)))
    (∑ j : β,
      eqToHom ⋯ ≫
        biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
          z ≫
            ((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)
    (∑ x : (↑(g ⁻¹' {h c}) : Type),
      eqToHom ⋯ ≫
        biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
          z ≫
            biproduct.π (fun (b : β) ↦ s (g b)) (↑x : β) ≫
              biproduct.ι.{0, v, u} (C := C) (fun (a : β) ↦ s (g a)) (↑x : β) ≫
                w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
⊢ 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 =
    ∑ x : (↑(g ⁻¹' {h c}) : Type),
      eqToHom ⋯ ≫
        biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
          z ≫
            biproduct.π (fun (b : β) ↦ s (g b)) (↑x : β) ≫
              biproduct.ι.{0, v, u} (C := C) (fun (a : β) ↦ s (g a)) (↑x : β) ≫
                w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c

Tactic:
simp only [Preadditive.sum_comp, Preadditive.comp_sum]

Premises used: CategoryTheory.Preadditive.sum_comp, CategoryTheory.Preadditive.comp_sum
-- 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
a₁ :
  ∀ (x : β) (hx : x ∈ g ⁻¹' {h c}),
    eqToHom ⋯ ≫
        biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun (b : β) ↦ s (g b)) x ≫ biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) x) ≫ w) ≫
              biproduct.π (fun (b : γ) ↦ s (h b)) c =
      eqToHom ⋯ ≫
        biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
          z ≫
            biproduct.π (fun (b : β) ↦ s (g b)) (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {h c}) x hx) : β) ≫
              biproduct.ι.{0, v, u} (C := C) (fun (a : β) ↦ s (g a))
                  (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {h c}) x hx) : β) ≫
                w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c
a₂ :
  ∀ x ∉ g ⁻¹' {h c},
    eqToHom ⋯ ≫
        biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun (b : β) ↦ s (g b)) x ≫ biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) x) ≫ w) ≫
              biproduct.π (fun (b : γ) ↦ s (h b)) c =
      0
⊢ Eq.{v + 1} (α := End (s (h c)))
    (∑ j : β,
      eqToHom ⋯ ≫
        biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
          z ≫
            ((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)
    (∑ x : (↑(g ⁻¹' {h c}) : Type),
      eqToHom ⋯ ≫
        biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
          z ≫
            biproduct.π (fun (b : β) ↦ s (g b)) (↑x : β) ≫
              biproduct.ι.{0, v, u} (C := C) (fun (a : β) ↦ s (g a)) (↑x : β) ≫
                w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)

Tactic:
apply Finset.sum_congr_set

Premises used: Finset.sum_congr_set
-- 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
⊢ ∀ (x : β) (hx : x ∈ g ⁻¹' {h c}),
    eqToHom ⋯ ≫
        biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
          z ≫
            ((biproduct.π (fun (b : β) ↦ s (g b)) x ≫ biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) x) ≫ w) ≫
              biproduct.π (fun (b : γ) ↦ s (h b)) c =
      eqToHom ⋯ ≫
        biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
          z ≫
            biproduct.π (fun (b : β) ↦ s (g b)) (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {h c}) x hx) : β) ≫
              biproduct.ι.{0, v, u} (C := C) (fun (a : β) ↦ s (g a))
                  (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {h c}) x hx) : β) ≫
                w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c

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 α
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
b : β
nm : b ∉ g ⁻¹' {h c}
⊢ ¬g b = h c

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

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
b : β
nm : ¬g b = h c
a₁ :
  Eq (α := End (s (h c)))
    (eqToHom ⋯ ≫
      biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
        z ≫
          biproduct.π (fun (b : β) ↦ s (g b)) b ≫
            biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
    0
⊢ eqToHom ⋯ ≫
      biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
        z ≫
          ((biproduct.π (fun (b : β) ↦ s (g b)) b ≫ biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b) ≫ w) ≫
            biproduct.π (fun (b : γ) ↦ s (h b)) c =
    0

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- 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
b : β
nm : ¬g b = h c
⊢ Eq.{v + 1} (α := s (h c) ⟶ s (h c)) (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 α
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
b : β
nm : ¬g b = h c
h₁ :
  Eq (α := s (f a) ⟶ s (h c))
    (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
      z ≫
        biproduct.π (fun (b : β) ↦ s (g b)) b ≫
          biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
    0
⊢ Eq (α := End (s (h c)))
    (eqToHom ⋯ ≫
      biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
        z ≫
          biproduct.π (fun (b : β) ↦ s (g b)) b ≫
            biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
    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 α
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
b : β
nm : ¬g b = h c
⊢ Eq.{v + 1} (α := s (f a) ⟶ s (h c))
    (CategoryStruct.comp (Y := biproduct.{0, v, u} fun (a : α) ↦ s (f a))
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a) 0 :
      s (f a) ⟶ s (h c))
    (0 : s (f a) ⟶ s (h c))

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 α
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
b : β
nm : ¬g b = h c
h₁ :
  Eq (α := (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) ⟶ s (h c))
    (z ≫
      biproduct.π (fun (b : β) ↦ s (g b)) b ≫
        biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
    0
⊢ Eq (α := s (f a) ⟶ s (h c))
    (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
      z ≫
        biproduct.π (fun (b : β) ↦ s (g b)) b ≫
          biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
    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 α
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
b : β
nm : ¬g b = h c
⊢ Eq (α := (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) ⟶ s (h c)) (z ≫ 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 α
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
b : β
nm : ¬g b = h c
h₁ :
  Eq.{v + 1} (α := (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ⟶ s (h c))
    (biproduct.π (fun (b : β) ↦ s (g b)) b ≫
      biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
    0
⊢ Eq (α := (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) ⟶ s (h c))
    (z ≫
      biproduct.π (fun (b : β) ↦ s (g b)) b ≫
        biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
    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 α
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
b : β
nm : ¬g b = h c
⊢ Eq.{v + 1} (α := (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ⟶ s (h c)) (biproduct.π (fun (b : β) ↦ s (g b)) b ≫ 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 α
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
b : β
nm : ¬g b = h c
h₁ : biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c = 0
⊢ Eq.{v + 1} (α := (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ⟶ s (h c))
    (biproduct.π (fun (b : β) ↦ s (g b)) b ≫
      biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
    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 α
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
b : β
nm : ¬g b = h c
⊢ biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c = 0

Tactic:
simp only [o.eq_zero nm]

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 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
R : Type u_2
inst_3 : Semiring R
inst_4 : Linear.{u_2, v, u} R C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_5 : Finite α
inst_6 : Finite β
f : α → ι
g : β → ι
w : R
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
        (AddEquiv.toEquiv
          (o.matrixDecompositionAddEquiv :
            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 : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))))
        (w • z) x i j =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) w : R)
        (Equiv.toFun
          (AddEquiv.toEquiv
            (o.matrixDecompositionAddEquiv :
              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 : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))))
          z)
        x i j
⊢ Equiv.toFun
      (AddEquiv.toEquiv
        (o.matrixDecompositionAddEquiv :
          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 : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))))
      (w • z) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) w : R)
      (Equiv.toFun
        (AddEquiv.toEquiv
          (o.matrixDecompositionAddEquiv :
            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 : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))))
        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
R : Type u_2
inst_3 : Semiring R
inst_4 : Linear.{u_2, v, u} R C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_5 : Finite α
inst_6 : Finite β
f : α → ι
g : β → ι
w : R
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 ⋯ =
    w •
      eqToHom ⋯ ≫
        (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) (↑j : α) ≫
            z ≫ biproduct.π (fun (b : β) ↦ s (g b)) (↑i : β)) ≫
          eqToHom ⋯
⊢ Equiv.toFun
      (AddEquiv.toEquiv
        (o.matrixDecompositionAddEquiv :
          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 : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))))
      (w • z) x i j =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) w : R)
      (Equiv.toFun
        (AddEquiv.toEquiv
          (o.matrixDecompositionAddEquiv :
            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 : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))))
        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
R : Type u_2
inst_3 : Semiring R
inst_4 : Linear.{u_2, v, u} R C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_5 : Finite α
inst_6 : Finite β
f : α → ι
g : β → ι
w : R
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 ⋯ =
    w •
      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
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
⊢ ∃ (e : α ≃ β), ∀ (a : α), g ((e : (a : α) → β) a) = f a

Tactic:
⟨Equiv.ofPreimageEquiv ?_, fun a => Equiv.ofPreimageEquiv_map _ _⟩

Premises used: Equiv.ofPreimageEquiv, Equiv.ofPreimageEquiv_map, Exists.intro