awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
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₂
⊢ A₁.str ≫ F.map (n • α.f) = (n • α.f) ≫ A₂.str
have rw : A₁.str ≫ (n • F.map α.f) = (n • α.f) ≫ A₂.str
Tactic: rw [Functor.map_nsmul, comp_nsmul, Endofunctor.Coalgebra.Hom.h, nsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
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
⊢ A₁.str ≫ F.map (n • α.f) = (n • α.f) ≫ A₂.str
have rw₁ : n • A₁.str ≫ F.map α.f = (n • α.f) ≫ A₂.str
Tactic: rw [Functor.map_nsmul, comp_nsmul, Endofunctor.Coalgebra.Hom.h, nsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
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
⊢ A₁.str ≫ F.map (n • α.f) = (n • α.f) ≫ A₂.str
have rw₂ : n • α.f ≫ A₂.str = (n • α.f) ≫ A₂.str
Tactic: rw [Functor.map_nsmul, comp_nsmul, Endofunctor.Coalgebra.Hom.h, nsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
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
⊢ A₁.str ≫ F.map (n • α.f) = (n • α.f) ≫ A₂.str
have rw₃ : n • α.f ≫ A₂.str = n • α.f ≫ A₂.str
Tactic: rw [Functor.map_nsmul, comp_nsmul, Endofunctor.Coalgebra.Hom.h, nsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
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₂
⊢ A₁.str ≫ F.map (r • α.f) = (r • α.f) ≫ A₂.str
have rw : A₁.str ≫ (r • F.map α.f) = (r • α.f) ≫ A₂.str
Tactic: rw [Functor.map_zsmul, comp_zsmul, Endofunctor.Coalgebra.Hom.h, zsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
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
⊢ A₁.str ≫ F.map (r • α.f) = (r • α.f) ≫ A₂.str
have rw₁ : r • A₁.str ≫ F.map α.f = (r • α.f) ≫ A₂.str
Tactic: rw [Functor.map_zsmul, comp_zsmul, Endofunctor.Coalgebra.Hom.h, zsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
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
⊢ A₁.str ≫ F.map (r • α.f) = (r • α.f) ≫ A₂.str
have rw₂ : r • α.f ≫ A₂.str = (r • α.f) ≫ A₂.str
Tactic: rw [Functor.map_zsmul, comp_zsmul, Endofunctor.Coalgebra.Hom.h, zsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.EndoFunctor (goal)
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
⊢ A₁.str ≫ F.map (r • α.f) = (r • α.f) ≫ A₂.str
have rw₃ : r • α.f ≫ A₂.str = r • α.f ≫ A₂.str
Tactic: rw [Functor.map_zsmul, comp_zsmul, Endofunctor.Coalgebra.Hom.h, zsmul_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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)
⊢ s i = s (f (↑k : α))
have rcases : ∀ (k : α) (j : (↑(g ⁻¹' {f k}) : Type)), s (f k) = s (f (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k sorry) : α))
Tactic: rcases k with ⟨k, ⟨⟩⟩
Cleared hypotheses: i, j, k
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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)
⊢ s (g (↑j : β)) = s i
have rcases : ∀ (j : β) (k : (↑(f ⁻¹' {g j}) : Type)), s (g (↑(Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {g j}) j sorry) : β)) = s (g j)
Tactic: rcases j with ⟨j, ⟨⟩⟩
Cleared hypotheses: i, j, k
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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))
⊢ (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
have 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 sorry)
                      (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f j}) j sorry) ≫
                    eqToHom sorry
                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 sorry ≫ biproduct.components z (↑k : α) (↑j : β) ≫ eqToHom sorry)
            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: ext j k
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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 : α
⊢ 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
have w : (if h : f k = g j then (eqToHom sorry ≫ biproduct.components z k j ≫ eqToHom sorry) ≫ eqToHom sorry else 0) =
  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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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 : α
⊢ (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
have pos : ∀ (h : f k = g j),
  (eqToHom sorry ≫ biproduct.components z k j ≫ eqToHom sorry) ≫ eqToHom sorry =
    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
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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
⊢ (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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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
⊢ (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
have 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
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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
⊢ 0 = biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j
have neg : biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) k ≫ z ≫ biproduct.π (fun (b : β) ↦ s (g b)) j = 0
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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))
⊢ (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
have 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 sorry ≫ biproduct.components z (↑k : α) (↑j : β) ≫ eqToHom sorry)
      ((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 sorry)
                    (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f j}) j sorry) ≫
                  eqToHom sorry
              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 sorry) =
    z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k sorry)
Tactic: ext i ⟨j, w⟩ ⟨k, ⟨⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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}
⊢ (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 ⋯)
have h : (if h : f k = g j then
      z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j sorry)
          (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k sorry) ≫
        eqToHom sorry
    else 0) ≫
    eqToHom sorry =
  z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k sorry)
Tactic: simp only [eqToHom_refl, biproduct.matrix_components, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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}
⊢ (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 ⋯)
have pos : ∀ (h : f k = g j),
  (z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j sorry) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k sorry) ≫
        eqToHom sorry) ≫
      eqToHom sorry =
    z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k sorry)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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 ⋯)
⊢ (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 ⋯)
have neg : ∀ (h : ¬f k = g j),
  0 ≫ eqToHom sorry =
    z (f k) (Subtype.mk (p := fun (x : β) ↦ x ∈ g ⁻¹' {f k}) j w) (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f k}) k sorry)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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
⊢ 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 ⋯)
have neg : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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))
⊢ Equiv.toFun o.matrixDecomposition (w + z) = Equiv.toFun o.matrixDecomposition w + Equiv.toFun o.matrixDecomposition z
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
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)
⊢ Equiv.toFun o.matrixDecomposition (w + z) x i j =
    (Equiv.toFun o.matrixDecomposition w + Equiv.toFun o.matrixDecomposition z) x i j
have h : eqToHom sorry ≫
    (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) (↑j : α) ≫
        (w + z) ≫ biproduct.π (fun (b : β) ↦ s (g b)) (↑i : β)) ≫
      eqToHom sorry =
  eqToHom sorry ≫
      (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) (↑j : α) ≫
          w ≫ biproduct.π (fun (b : β) ↦ s (g b)) (↑i : β)) ≫
        eqToHom sorry +
    eqToHom sorry ≫
      (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) (↑j : α) ≫
          z ≫ biproduct.π (fun (b : β) ↦ s (g b)) (↑i : β)) ≫
        eqToHom sorry
Tactic: dsimp [biproduct.components]