awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
f : α → ι
i : ι
⊢ 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)))
have 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 sorry)
        (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 sorry)
        (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property) :
      End (s (f b)))
Tactic: ext ⟨b, ⟨⟩⟩ ⟨a, j_property⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (hypothesis)
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}
⊢ 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)))
have j_property₁ : f a = f b
Tactic: simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property
-- 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 α
f : α → ι
b a : α
j_property_1 : a ∈ f ⁻¹' {f b}
j_property : f a = 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_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)))
have a₁ : Eq.{v + 1} (α := End (s (f b)))
  (eqToHom sorry ≫
    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 sorry =
        Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property_1 then
    𝟙 (s (f b))
  else 0)
Tactic: simp only [Category.comp_id, Category.id_comp, End.one_def, eqToHom_refl,
    Matrix.one_apply, HomOrthogonal.matrixDecomposition_apply, biproduct.components]
-- 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 α
f : α → ι
b a : α
j_property_1 : a ∈ f ⁻¹' {f b}
j_property : f a = 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))
    (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)
have pos : ∀
  (h :
    Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) b sorry =
      Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property_1),
  Eq.{v + 1} (α := End (s (f b)))
    (eqToHom sorry ≫
      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: 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 : 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)))
⊢ 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)
have neg : ∀
  (h :
    ¬Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) b sorry =
        Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {f b}) a j_property_1),
  Eq.{v + 1} (α := End (s (f b)))
    (eqToHom sorry ≫
      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: 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 : 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
⊢ 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)))
have pos : ∀ (j_property : b ∈ f ⁻¹' {f b}) (j_property_2 : f b = f b),
  Eq.{v + 1} (α := End (s (f b)))
    (eqToHom sorry ≫
      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: cases h
Cleared hypotheses: a, j_property_1, j_property, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (hypothesis)
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
⊢ 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
have h₁ : ¬b = a
Tactic: simp only [Subtype.mk.injEq] at h
Cleared hypotheses: 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 : 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} (α := 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
have 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))
Tactic: convert! comp_zero
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (hypothesis)
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}
⊢ ((o.matrixDecomposition :
          Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
              (biproduct.{0, v, u} fun (b : γ) ↦ s (h b)) ≃
            ((i : ι) → Matrix (↑(h ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))) :
        (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : γ) ↦ s (h b)) →
          (i : ι) → Matrix (↑(h ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
      (z ≫ w) (h c) (Subtype.mk (p := fun (x : γ) ↦ x ∈ h ⁻¹' {h c}) c ⋯)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {h c}) a j_property) =
    HMul.hMul (α := Matrix (↑(h ⁻¹' {h c}) : Type) (↑(g ⁻¹' {h c}) : Type) (End (s (h c)))) (β :=
      Matrix (↑(g ⁻¹' {h c}) : Type) (↑(f ⁻¹' {h c}) : Type) (End (s (h c))))
      (((o.matrixDecomposition :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : β) ↦ s (g a))
                  (biproduct.{0, v, u} fun (b : γ) ↦ s (h b)) ≃
                ((i : ι) → Matrix (↑(h ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))) :
            (a : (⨁ fun (a : β) ↦ s (g a)) ⟶ ⨁ fun (b : γ) ↦ s (h b)) →
              (i : ι) → Matrix (↑(h ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))
          w (h c) :
        Matrix (↑(h ⁻¹' {h c}) : Type) (↑(g ⁻¹' {h c}) : Type) (End (s (h c))))
      (((o.matrixDecomposition :
              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)))) :
            (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : β) ↦ s (g b)) →
              (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
          z (h c) :
        Matrix (↑(g ⁻¹' {h c}) : Type) (↑(f ⁻¹' {h c}) : Type) (End (s (h c))))
      (Subtype.mk (p := fun (x : γ) ↦ x ∈ h ⁻¹' {h c}) c ⋯)
      (Subtype.mk (p := fun (x : α) ↦ x ∈ f ⁻¹' {h c}) a j_property)
have j_property₁ : f a = h c
Tactic: simp only [Set.mem_preimage, Set.mem_singleton_iff] at j_property
-- 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 : 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
| eqToHom ⋯ ≫ biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫ z ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c
have rw : eqToHom sorry ≫
  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
Tactic: rw [← Category.id_comp w, ← biproduct.total]
-- 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 : 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
⊢ 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
have a₁ : eqToHom sorry ≫
    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 sorry ≫
      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]
-- 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 : 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
⊢ 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
have a₁ : Eq.{v + 1} (α := End (s (h c)))
  (∑ j : β,
    eqToHom sorry ≫
      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 sorry ≫
      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]
-- 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 : 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
⊢ 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)
have a₁ : ∀ (x : β) (hx : x ∈ g ⁻¹' {h c}),
  eqToHom sorry ≫
      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 sorry ≫
      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: apply Finset.sum_congr_set
-- 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 : 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
⊢ 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)
have a₂ : ∀ x ∉ g ⁻¹' {h c},
  eqToHom sorry ≫
      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
Tactic: apply Finset.sum_congr_set
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (hypothesis)
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}
⊢ 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
have nm₁ : ¬g b = h c
Tactic: simp only [Set.mem_preimage, Set.mem_singleton_iff] at nm
Cleared hypotheses: nm