-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
h₀ :
  (biprod.inl ≫
        (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) (biprod.fst ≫ f₁₁ ≫ biprod.inl)
                (biprod.fst ≫ f₁₂ ≫ biprod.inr) +
              biprod.snd ≫ f₂₁ ≫ biprod.inl +
            biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
          (HAdd.hAdd (α := biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ g₁₁ ≫ biprod.inl)
                (biprod.fst ≫ g₁₂ ≫ biprod.inr) +
              biprod.snd ≫ g₂₁ ≫ biprod.inl +
            biprod.snd ≫ g₂₂ ≫ biprod.inr)) ≫
      biprod.fst =
    (biprod.inl ≫
        (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl)
              (biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr) +
            biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
          biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr)) ≫
      biprod.fst
h₁ :
  (biprod.inl ≫
        (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) (biprod.fst ≫ f₁₁ ≫ biprod.inl)
                (biprod.fst ≫ f₁₂ ≫ biprod.inr) +
              biprod.snd ≫ f₂₁ ≫ biprod.inl +
            biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
          (HAdd.hAdd (α := biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ g₁₁ ≫ biprod.inl)
                (biprod.fst ≫ g₁₂ ≫ biprod.inr) +
              biprod.snd ≫ g₂₁ ≫ biprod.inl +
            biprod.snd ≫ g₂₂ ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inl ≫
        (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl)
              (biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr) +
            biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
          biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr)) ≫
      biprod.snd
⊢ (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) (biprod.fst ≫ f₁₁ ≫ biprod.inl)
            (biprod.fst ≫ f₁₂ ≫ biprod.inr) +
          biprod.snd ≫ f₂₁ ≫ biprod.inl +
        biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
      (HAdd.hAdd (α := biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ g₁₁ ≫ biprod.inl)
            (biprod.fst ≫ g₁₂ ≫ biprod.inr) +
          biprod.snd ≫ g₂₁ ≫ biprod.inl +
        biprod.snd ≫ g₂₂ ≫ biprod.inr) =
    HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl)
          (biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr) +
        biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
      biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr
have h₂ : (biprod.inr ≫
      (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) (biprod.fst ≫ f₁₁ ≫ biprod.inl)
              (biprod.fst ≫ f₁₂ ≫ biprod.inr) +
            biprod.snd ≫ f₂₁ ≫ biprod.inl +
          biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
        (HAdd.hAdd (α := biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ g₁₁ ≫ biprod.inl)
              (biprod.fst ≫ g₁₂ ≫ biprod.inr) +
            biprod.snd ≫ g₂₁ ≫ biprod.inl +
          biprod.snd ≫ g₂₂ ≫ biprod.inr)) ≫
    biprod.fst =
  (biprod.inr ≫
      (HAdd.hAdd (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂) (biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl)
            (biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr) +
          biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
        biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr)) ≫
    biprod.fst
Tactic: ext