awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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₂
⊢ (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.snd =
    (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.snd

Tactic:
simp only [add_comp, comp_add, add_zero, zero_add, biprod.inl_fst,
      biprod.inl_snd, biprod.inr_fst, biprod.inr_snd, biprod.inl_fst_assoc, biprod.inl_snd_assoc,
      biprod.inr_fst_assoc, biprod.inr_snd_assoc, comp_zero, zero_comp, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inl_snd_assoc, CategoryTheory.Limits.biprod.inr_snd_assoc, CategoryTheory.Limits.biprod.inr_fst, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.biprod.inl_fst, CategoryTheory.Limits.biprod.inl_snd, zero_add, CategoryTheory.Preadditive.add_comp, CategoryTheory.Limits.biprod.inr_fst_assoc, CategoryTheory.Preadditive.comp_add, CategoryTheory.Limits.zero_comp, add_zero, CategoryTheory.Limits.biprod.inr_snd, CategoryTheory.Limits.biprod.inl_fst_assoc
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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.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:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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.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:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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.fst : 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.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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₁ : -f₂₁ ≫ inv f₁₁ ≫ f₁₂ + f₂₂ = f₂₂ - f₂₁ ≫ inv f₁₁ ≫ 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

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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₁₁
⊢ -f₂₁ ≫ inv f₁₁ ≫ f₁₂ + f₂₂ = f₂₂ - f₂₁ ≫ inv f₁₁ ≫ f₁₂

Tactic:
abel
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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)
rwa rwa₁ rwa₂ 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₂₂
⊢ (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

Premises used: CategoryTheory.Biprod.ofComponents_eq
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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₂)
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₂
⊢ X₂ ≅ Y₂

Tactic:
obtain ⟨L, R, g, w⟩ := Biprod.gaussian' f₁₁ f₁₂ f₂₁ f₂₂

Premises used: CategoryTheory.Biprod.gaussian'
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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₂)
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
rw : IsIso (L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom)
⊢ IsIso (X := biprod.{v, u} X₁ X₂) (Y := biprod.{v, u} Y₁ Y₂) (biprod.map f₁₁ g)

Tactic:
rw [← w]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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₂)
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
⊢ IsIso (L.hom ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ R.hom)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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₂)
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
this_1 : IsIso (X := biprod.{v, u} X₁ X₂) (Y := biprod.{v, u} Y₁ Y₂) (biprod.map f₁₁ g) := ⋯
this : IsIso g := ⋯
⊢ X₂ ≅ Y₂

Tactic:
exact asIso g

Premises used: CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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.hom ≫ biprod.fst)
simp : IsIso f.hom
⊢ IsIso (X := biprod.{v, u} X₁ X₂) (Y := biprod.{v, u} Y₁ Y₂)
    (ofComponents (biprod.inl ≫ f.hom ≫ biprod.fst) (biprod.inl ≫ f.hom ≫ biprod.snd) (biprod.inr ≫ f.hom ≫ biprod.fst)
        (biprod.inr ≫ f.hom ≫ biprod.snd) :
      biprod.{v, u} X₁ X₂ ⟶ biprod.{v, u} Y₁ Y₂)

Tactic:
simp only [Biprod.ofComponents_eq]

Premises used: CategoryTheory.Biprod.ofComponents_eq
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
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.hom ≫ biprod.fst)
⊢ IsIso f.hom

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
by_contra! :
  ∀ (nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0) (a₁ : biprod.inl ≫ f ≫ biprod.fst = 0)
    (a₂ : biprod.inl ≫ f ≫ biprod.snd = 0), False
⊢ Eq.{v + 1} (α := W ⟶ W) (𝟙 W) 0 ∨ biprod.inl ≫ f ≫ biprod.fst ≠ 0 ∨ biprod.inl ≫ f ≫ biprod.snd ≠ 0

Tactic:
by_contra! ⟨nz, a₁, a₂⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
⊢ x = 𝟙 W

Tactic:
simp [x]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
⊢ x = 𝟙 W

Tactic:
have h₁ : x = 𝟙 W := by simp [x]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
dsimp : biprod.inl ≫ f ≫ inv f ≫ biprod.fst = 0
⊢ x = 0

Tactic:
dsimp [x]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
rw :
  biprod.inl ≫
      f ≫
        HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
          inv f ≫ biprod.fst =
    0
⊢ biprod.inl ≫ f ≫ inv f ≫ biprod.fst = 0

Tactic:
rw [← Category.id_comp (inv f), Category.assoc, ← biprod.total]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.total, CategoryTheory.inv, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : f ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr)
a₃ : inv f
a₄ : biprod.fst
a₅ : biprod.inl
| biprod.inl ≫
    f ≫
      HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst

Tactic:
slice 2 3
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl) (f ≫ biprod.snd ≫ biprod.inr)
| f ≫ HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr)

Tactic:
rw [comp_add]

Premises used: CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl) (f ≫ biprod.snd ≫ biprod.inr)
a₃ : inv f
a₄ : biprod.fst
a₅ : biprod.inl
| biprod.inl ≫
    f ≫
      HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst

Tactic:
slice 2 3
      rw [comp_add]

Premises used: CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
conv_lhs :
  biprod.inl ≫
      (HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl)
            (f ≫ biprod.snd ≫ biprod.inr) ≫
          inv f) ≫
        biprod.fst =
    0
⊢ biprod.inl ≫
      f ≫
        HAdd.hAdd (α := biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) (biprod.fst ≫ biprod.inl) (biprod.snd ≫ biprod.inr) ≫
          inv f ≫ biprod.fst =
    0

Tactic:
conv_lhs =>
      slice 2 3
      rw [comp_add]

Premises used: CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
simp :
  biprod.inl ≫
      HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl)
          (f ≫ biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst =
    0
⊢ biprod.inl ≫
      (HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl)
            (f ≫ biprod.snd ≫ biprod.inr) ≫
          inv f) ≫
        biprod.fst =
    0

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
rw :
  (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
      (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst =
    0
⊢ biprod.inl ≫
      HAdd.hAdd (α := biprod.{v, u} W X ⟶ biprod.{v, u} Y Z) (f ≫ biprod.fst ≫ biprod.inl)
          (f ≫ biprod.snd ≫ biprod.inr) ≫
        inv f ≫ biprod.fst =
    0

Tactic:
rw [comp_add_assoc, add_comp]

Premises used: CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add_assoc
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
congr : (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst
a : (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
    (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst

Tactic:
next => skip
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : biprod.inl ≫ f ≫ biprod.snd
a₃ : biprod.inr
a₄ : inv f
a₅ : biprod.fst
| (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst

Tactic:
slice 1 3
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : 0
| biprod.inl ≫ f ≫ biprod.snd

Tactic:
rw [a₂]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
a : 0
a₃ : biprod.inr
a₄ : inv f
a₅ : biprod.fst
| (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
    (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst

Tactic:
congr
      next => skip
      slice 1 3
      rw [a₂]
-- Module: Mathlib.CategoryTheory.Preadditive.Biproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z
inst_3 : IsIso f
nz : Ne.{v + 1} (α := W ⟶ W) (𝟙 W) 0
a₁ : biprod.inl ≫ f ≫ biprod.fst = 0
a₂ : biprod.inl ≫ f ≫ biprod.snd = 0
x : W ⟶ W := biprod.inl ≫ f ≫ inv f ≫ biprod.fst
h₁ : x = 𝟙 W
conv_lhs : (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst + ((0 ≫ biprod.inr) ≫ inv f) ≫ biprod.fst = 0
⊢ (biprod.inl ≫ f ≫ biprod.fst ≫ biprod.inl) ≫ inv f ≫ biprod.fst +
      (biprod.inl ≫ f ≫ biprod.snd ≫ biprod.inr) ≫ inv f ≫ biprod.fst =
    0

Tactic:
conv_lhs =>
      congr
      next => skip
      slice 1 3
      rw [a₂]