awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (hypothesis)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
⊢ f + g = f + g
have h₂ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
Tactic: have h₂ := @biprod.add_eq_lift_id_desc _ _ b _ _ f g
      (by convert! (inferInstance : HasBinaryBiproduct X X); subsingleton)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
h₂ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
⊢ f + g = f + g
have homGroup : CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g) =
  CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
Tactic: refine h₁.trans (Eq.trans ?_ h₂.symm)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
h₂ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
⊢ CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g) =
    CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
have homGroup : Eq (α := HasZeroMorphisms.{v, u} C) preadditiveHasZeroMorphisms preadditiveHasZeroMorphisms
Tactic: congr! 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.Biproducts (goal)
Goal:
C_1 : Type u
inst : Category.{v, u} C_1
inst_1 : Preadditive.{v, u} C_1
C : Type u
inst_2 : Category.{v, u} C
inst_3 : HasZeroMorphisms.{v, u} C
inst_4 : HasBinaryBiproducts.{v, u} C
a b : Preadditive.{v, u} C
X Y : C
f g : X ⟶ Y
h₁ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
h₂ : f + g = CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
homGroup : Eq (α := HasZeroMorphisms.{v, u} C) preadditiveHasZeroMorphisms preadditiveHasZeroMorphisms
⊢ CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g) =
    CategoryStruct.comp (Y := biprod.{v, u} X X) (biprod.lift (𝟙 X) (𝟙 X)) (biprod.desc f g)
have homGroup₁ : biprod.{v, u} X X = biprod.{v, u} X X →
  Eq (α := HasZeroMorphisms.{v, u} C) preadditiveHasZeroMorphisms preadditiveHasZeroMorphisms
Tactic: congr! 2
-- 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₂ : C
f : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂
⊢ ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
      (biprod.inr ≫ f ≫ biprod.snd) =
    f
have h₀ : CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
    (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
        (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
            (biprod.inr ≫ f ≫ biprod.snd) :
          biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
      X₁ ⟶ biprod.{v, u} Y₁ Y₂)
    (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
  (biprod.inl ≫ f) ≫ biprod.fst
Tactic: ext
-- 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₂ : C
f : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₁ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
    (biprod.inl ≫ f) ≫ biprod.fst
⊢ ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
      (biprod.inr ≫ f ≫ biprod.snd) =
    f
have h₁ : CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
    (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
        (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
            (biprod.inr ≫ f ≫ biprod.snd) :
          biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
      X₁ ⟶ biprod.{v, u} Y₁ Y₂)
    (biprod.snd : biprod.{v, u} Y₁ Y₂ ⟶ Y₂) =
  (biprod.inl ≫ f) ≫ biprod.snd
Tactic: ext
-- 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₂ : C
f : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₁ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
    (biprod.inl ≫ f) ≫ biprod.fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₁ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.snd : biprod.{v, u} Y₁ Y₂ ⟶ Y₂) =
    (biprod.inl ≫ f) ≫ biprod.snd
⊢ ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
      (biprod.inr ≫ f ≫ biprod.snd) =
    f
have h₂ : CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
    (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inr : X₂ ⟶ biprod.{v, u} X₁ X₂)
        (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
            (biprod.inr ≫ f ≫ biprod.snd) :
          biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
      X₂ ⟶ biprod.{v, u} Y₁ Y₂)
    (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
  (biprod.inr ≫ f) ≫ biprod.fst
Tactic: ext
-- 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₂ : C
f : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₁ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
    (biprod.inl ≫ f) ≫ biprod.fst
h₁ :
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₁ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.snd : biprod.{v, u} Y₁ Y₂ ⟶ Y₂) =
    (biprod.inl ≫ f) ≫ biprod.snd
h₂ :
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inr : X₂ ⟶ biprod.{v, u} X₁ X₂)
          (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₂ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
    (biprod.inr ≫ f) ≫ biprod.fst
⊢ ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
      (biprod.inr ≫ f ≫ biprod.snd) =
    f
have h₃ : CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
    (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inr : X₂ ⟶ biprod.{v, u} X₁ X₂)
        (ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
            (biprod.inr ≫ f ≫ biprod.snd) :
          biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
      X₂ ⟶ biprod.{v, u} Y₁ Y₂)
    (biprod.snd : biprod.{v, u} Y₁ Y₂ ⟶ Y₂) =
  (biprod.inr ≫ f) ≫ biprod.snd
Tactic: ext
-- 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₂
⊢ Eq (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂)
    (CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
        (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
        (ofComponents g₁₁ g₁₂ g₂₁ g₂₂ : biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Z₁ Z₂) :
      biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂)
    (ofComponents (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) :
      biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Z₁ Z₂)
have dsimp : (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
Tactic: dsimp [Biprod.ofComponents]
-- 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₂
⊢ (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.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
Tactic: ext
-- 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
⊢ (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.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
Tactic: ext
-- 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₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst_3 : IsIso f₁₁
⊢ Eq (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
    (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂)
        (Iso.hom (unipotentLower (-f₂₁ ≫ inv f₁₁)) : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} X₁ X₂)
        (CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
            (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
            (Iso.hom (unipotentUpper (-inv f₁₁ ≫ f₁₂)) : biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Y₁ Y₂) :
          biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
      biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
    (biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂) : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
have h₀ : CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
    (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
        (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂)
            (Iso.hom (unipotentLower (-f₂₁ ≫ inv f₁₁)) : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} X₁ X₂)
            (CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
                (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
                (Iso.hom (unipotentUpper (-inv f₁₁ ≫ f₁₂)) : biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Y₁ Y₂) :
              biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
          biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
      X₁ ⟶ biprod.{v, u} Y₁ Y₂)
    (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
    (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) biprod.inl (biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂))) biprod.fst
Tactic: ext
-- 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₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst_3 : IsIso f₁₁
h₀ :
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
          (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂)
              (Iso.hom (unipotentLower (-f₂₁ ≫ inv f₁₁)) : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} X₁ X₂)
              (CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
                  (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
                  (Iso.hom (unipotentUpper (-inv f₁₁ ≫ f₁₂)) : biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Y₁ Y₂) :
                biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₁ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.fst : biprod.{v, u} Y₁ Y₂ ⟶ Y₁) =
    CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) biprod.inl (biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)))
      biprod.fst
⊢ Eq (α := biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
    (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂)
        (Iso.hom (unipotentLower (-f₂₁ ≫ inv f₁₁)) : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} X₁ X₂)
        (CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
            (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
            (Iso.hom (unipotentUpper (-inv f₁₁ ≫ f₁₂)) : biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Y₁ Y₂) :
          biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
      biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
    (biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂) : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
have h₁ : CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
    (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inl : X₁ ⟶ biprod.{v, u} X₁ X₂)
        (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂)
            (Iso.hom (unipotentLower (-f₂₁ ≫ inv f₁₁)) : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} X₁ X₂)
            (CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
                (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
                (Iso.hom (unipotentUpper (-inv f₁₁ ≫ f₁₂)) : biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Y₁ Y₂) :
              biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
          biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
      X₁ ⟶ biprod.{v, u} Y₁ Y₂)
    (biprod.snd : biprod.{v, u} Y₁ Y₂ ⟶ Y₂) =
  CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
    (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) biprod.inl (biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂))) biprod.snd
Tactic: ext
-- 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₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst_3 : IsIso f₁₁
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) (biprod.inr : X₂ ⟶ biprod.{v, u} X₁ X₂)
          (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂)
              (Iso.hom (unipotentLower (-f₂₁ ≫ inv f₁₁)) : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} X₁ X₂)
              (CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
                  (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
                  (Iso.hom (unipotentUpper (-inv f₁₁ ≫ f₁₂)) : biprod.{v, u} Y₁ Y₂ ⟶ biprod.{v, u} Y₁ Y₂) :
                biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
            biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂) :
        X₂ ⟶ biprod.{v, u} Y₁ Y₂)
      (biprod.snd : biprod.{v, u} Y₁ Y₂ ⟶ Y₂) =
    CategoryStruct.comp (Y := biprod.{v, u} Y₁ Y₂)
      (CategoryStruct.comp (Y := biprod.{v, u} X₁ X₂) biprod.inr (biprod.map f₁₁ (f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂)))
      biprod.snd
have h₁ : -f₂₁ ≫ inv f₁₁ ≫ f₁₂ + f₂₂ = f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂
Tactic: simp
-- 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₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
f : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂
inst_3 : IsIso (biprod.inl ≫ f ≫ biprod.fst)
this : (L : biprod.{v, u} X₁ X₂ ≅ biprod.{v, u} X₁ X₂) ×'
  (R : biprod.{v, u} Y₁ Y₂ ≅ biprod.{v, u} Y₁ Y₂) ×'
    (g₂₂ : X₂ ⟶ Y₂) ×'
      L.hom ≫
          ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
              (biprod.inr ≫ f ≫ biprod.snd) ≫
            R.hom =
        biprod.map (biprod.inl ≫ f ≫ biprod.fst) g₂₂ :=
  gaussian' (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd) (biprod.inr ≫ f ≫ biprod.fst)
    (biprod.inr ≫ f ≫ biprod.snd)
⊢ (L : biprod.{v, u} X₁ X₂ ≅ biprod.{v, u} X₁ X₂) ×'
    (R : biprod.{v, u} Y₁ Y₂ ≅ biprod.{v, u} Y₁ Y₂) ×'
      (g₂₂ : X₂ ⟶ Y₂) ×' L.hom ≫ f ≫ R.hom = biprod.map (biprod.inl ≫ f ≫ biprod.fst) g₂₂
have rwa : (this :
    (L : biprod.{v, u} X₁ X₂ ≅ biprod.{v, u} X₁ X₂) ×'
      (R : biprod.{v, u} Y₁ Y₂ ≅ biprod.{v, u} Y₁ Y₂) ×'
        (g₂₂ : X₂ ⟶ Y₂) ×' L.hom ≫ f ≫ R.hom = biprod.map (biprod.inl ≫ f ≫ biprod.fst) g₂₂) →
  (L : biprod.{v, u} X₁ X₂ ≅ biprod.{v, u} X₁ X₂) ×'
    (R : biprod.{v, u} Y₁ Y₂ ≅ biprod.{v, u} Y₁ Y₂) ×'
      (g₂₂ : X₂ ⟶ Y₂) ×' L.hom ≫ f ≫ R.hom = biprod.map (biprod.inl ≫ f ≫ biprod.fst) g₂₂
Tactic: rwa [Biprod.ofComponents_eq] at this
Cleared hypotheses: this
-- 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₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
inst_3 : IsIso f₁₁
inst_4 :
  IsIso (X := biprod.{v, u} X₁ X₂) (Y := biprod.{v, u} Y₁ Y₂)
    (ofComponents f₁₁ f₁₂ f₂₁ f₂₂ : biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)
⊢ X₂ ≅ Y₂
have obtain : (L : biprod.{v, u} X₁ X₂ ≅ biprod.{v, u} X₁ X₂) →
  (R : biprod.{v, u} Y₁ Y₂ ≅ biprod.{v, u} Y₁ Y₂) →
    (g : X₂ ⟶ Y₂) → (w : L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom = biprod.map f₁₁ g) → X₂ ≅ Y₂
Tactic: obtain ⟨L, R, g, w⟩ := Biprod.gaussian' f₁₁ f₁₂ f₂₁ f₂₂