awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
g : X ⟶ Y
I : C
w_1 : Injective.{v_1, u_1} I
f : I ⟶ X
w : f ≫ g = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
this : IsSplitEpi g
e : I ≅ kernel g :=
  ⋯.fIsKernel.conePointUniqueUpToIso
    (limit.isLimit
      (parallelPair { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w : ShortComplex.{v_1, u_1} C }.g 0))
⊢ epiWithInjectiveKernel g

Tactic:
exact ⟨inferInstance, Injective.of_iso e inferInstance⟩
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
rw :
  ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f_1 : I ⟶ X) (w : f_1 ≫ f = 0),
    Nonempty.{v_1 + 1} { X₁ := I, X₂ := X, X₃ := Y, f := f_1, g := f, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
⊢ epiWithInjectiveKernel f

Tactic:
rw [epiWithInjectiveKernel_iff]

Premises used: CategoryTheory.Abelian.epiWithInjectiveKernel_iff
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
⊢ Eq (α := 0 ⟶ Y) (0 ≫ f) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
⊢ IsIso (X := ShortComplex.X₂ (ShortComplex.mk (X₁ := 0) 0 f ⋯)) (ShortComplex.g (ShortComplex.mk (X₁ := 0) 0 f ⋯))

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
inst_2 : IsIso f
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f_1 : I ⟶ X) (w : f_1 ≫ f = 0),
    Nonempty.{v_1 + 1} { X₁ := I, X₂ := X, X₃ := Y, f := f_1, g := f, zero := w : ShortComplex.{v_1, u_1} C }.Splitting

Tactic:
exact ⟨0, inferInstance, 0, by simp,
    ⟨ShortComplex.Splitting.ofIsZeroOfIsIso _ (isZero_zero C) (by assumption)⟩⟩
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hY : IsZero.{v_1, u_1} Y
simp : Injective.{v_1, u_1} (kernel f) ↔ Injective.{v_1, u_1} X
⊢ epiWithInjectiveKernel f ↔ Injective.{v_1, u_1} X

Tactic:
simp only [epiWithInjectiveKernel, hY.epi f, true_and]

Premises used: CategoryTheory.Abelian.epiWithInjectiveKernel, CategoryTheory.Limits.IsZero.epi, true_and
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hY : IsZero.{v_1, u_1} Y
⊢ Injective.{v_1, u_1} (kernel f) ↔ Injective.{v_1, u_1} X

Tactic:
Injective.iso_iff
    { hom := kernel.ι f
      inv := kernel.lift _ (𝟙 X) (hY.eq_of_tgt _ _) }

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Iso.mk, CategoryTheory.Limits.IsZero.eq_of_tgt, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, CategoryTheory.Limits.kernel.ι, CategoryTheory.Limits.kernel.lift, CategoryTheory.Injective.iso_iff
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y : C
f : X ⟶ Y
hY : IsZero.{v_1, u_1} Y
⊢ Injective.{v_1, u_1} (kernel f) ↔ Injective.{v_1, u_1} X

Tactic:
exact Injective.iso_iff
    { hom := kernel.ι f
      inv := kernel.lift _ (𝟙 X) (hY.eq_of_tgt _ _) }

Premises used: CategoryTheory.CategoryStruct.id, CategoryTheory.Iso.mk, CategoryTheory.Limits.IsZero.eq_of_tgt, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, CategoryTheory.Limits.kernel.ι, CategoryTheory.Limits.kernel.lift, CategoryTheory.Injective.iso_iff
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
hg₁ : epiWithInjectiveKernel g₁
hg₂ : epiWithInjectiveKernel g₂
rw :
  ∀
    (hg₁ :
      ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ = 0),
        Nonempty.{v_1 + 1}
          { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g₁, zero := w : ShortComplex.{v_1, u_1} C }.Splitting)
    (hg₂ :
      ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ Y) (w : f ≫ g₂ = 0),
        Nonempty.{v_1 + 1}
          { X₁ := I, X₂ := Y, X₃ := Z, f := f, g := g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting),
    ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
      Nonempty.{v_1 + 1}
        { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
⊢ epiWithInjectiveKernel (g₁ ≫ g₂)

Tactic:
rw [epiWithInjectiveKernel_iff] at hg₁ hg₂ ⊢

Premises used: CategoryTheory.Abelian.epiWithInjectiveKernel_iff
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
hg₁ :
  ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ = 0),
    Nonempty.{v_1 + 1} { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g₁, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
hg₂ :
  ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ Y) (w : f ≫ g₂ = 0),
    Nonempty.{v_1 + 1} { X₁ := I, X₂ := Y, X₃ := Z, f := f, g := g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
obtain :
  ∀ (I₁ : C),
    Injective.{v_1, u_1} I₁ →
      ∀ (f₁ : I₁ ⟶ X) (w₁ : f₁ ≫ g₁ = 0)
        (σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting),
        ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
          Nonempty.{v_1 + 1}
            { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting

Tactic:
obtain ⟨I₁, _, f₁, w₁, ⟨σ₁⟩⟩ := hg₁
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
hg₂ :
  ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ Y) (w : f ≫ g₂ = 0),
    Nonempty.{v_1 + 1} { X₁ := I, X₂ := Y, X₃ := Z, f := f, g := g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
obtain :
  ∀ (I₂ : C),
    Injective.{v_1, u_1} I₂ →
      ∀ (f₂ : I₂ ⟶ Y) (w₂ : f₂ ≫ g₂ = 0)
        (σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting),
        ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
          Nonempty.{v_1 + 1}
            { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting

Tactic:
obtain ⟨I₂, _, f₂, w₂, ⟨σ₂⟩⟩ := hg₂
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting

Tactic:
⟨I₁ ⊞ I₂, inferInstance, biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, ?_, ⟨?_⟩⟩

Premises used: inferInstance, CategoryTheory.Limits.biprod, Nonempty.intro, CategoryTheory.Limits.biprod.snd, HAdd.hAdd, CategoryTheory.Limits.biprod.fst, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.ShortComplex.Splitting.s
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
refine_1 : HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ = 0
refine_2 :
  { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
      f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
      zero := ⋯ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ g₁ ≫ g₂ = 0),
    Nonempty.{v_1 + 1}
      { X₁ := I, X₂ := X, X₃ := Z, f := f, g := g₁ ≫ g₂, zero := w : ShortComplex.{v_1, u_1} C }.Splitting

Tactic:
refine ⟨I₁ ⊞ I₂, inferInstance, biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s, ?_, ⟨?_⟩⟩
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
refine_1 :
  biprod.inl ≫ HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} I₁ I₂) biprod.inl 0
refine_1₁ :
  biprod.inr ≫ HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} I₁ I₂) biprod.inr 0
⊢ HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ = 0

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ biprod.inl ≫ HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} I₁ I₂) biprod.inl 0

Tactic:
simp [reassoc_of% w₁]
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ biprod.inr ≫ HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ =
    CategoryStruct.comp (Y := biprod.{v_1, u_1} I₁ I₂) biprod.inr 0

Tactic:
simp [reassoc_of% σ₁.s_g, w₂]

Premises used: CategoryTheory.ShortComplex.Splitting.s_g
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ (biprod.inl ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
              f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s),
              g := g₁ ≫ g₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.f ≫
          HAdd.hAdd (α :=
            { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₂ ⟶
              biprod.{v_1, u_1}
                { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₁
                { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₁)
            (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.fst =
    (biprod.inl ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
              f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s),
              g := g₁ ≫ g₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁) ≫
      biprod.fst

Tactic:
simp [σ₁.f_r]

Premises used: CategoryTheory.ShortComplex.Splitting.f_r
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ (biprod.inl ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
              f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s),
              g := g₁ ≫ g₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.f ≫
          HAdd.hAdd (α :=
            { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₂ ⟶
              biprod.{v_1, u_1}
                { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₁
                { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₁)
            (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inl ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
              f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s),
              g := g₁ ≫ g₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁) ≫
      biprod.snd

Tactic:
simp [reassoc_of% w₁]
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ (biprod.inr ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
              f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s),
              g := g₁ ≫ g₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.f ≫
          HAdd.hAdd (α :=
            { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₂ ⟶
              biprod.{v_1, u_1}
                { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₁
                { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₁)
            (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.fst =
    (biprod.inr ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
              f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s),
              g := g₁ ≫ g₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁) ≫
      biprod.fst

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ (biprod.inr ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
              f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s),
              g := g₁ ≫ g₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.f ≫
          HAdd.hAdd (α :=
            { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₂ ⟶
              biprod.{v_1, u_1}
                { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₁
                { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₁)
            (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr)) ≫
      biprod.snd =
    (biprod.inr ≫
        𝟙
          { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
              f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s),
              g := g₁ ≫ g₂, zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₁) ≫
      biprod.snd

Tactic:
simp [reassoc_of% σ₁.s_g, σ₂.f_r]

Premises used: CategoryTheory.ShortComplex.Splitting.s_g, CategoryTheory.ShortComplex.Splitting.f_r
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ (σ₂.s ≫ σ₁.s) ≫
      { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
          f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
          zero := ⋯ : ShortComplex.{v_1, u_1} C }.g =
    𝟙
      { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
          f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
          zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₃

Tactic:
simp [reassoc_of% σ₁.s_g, σ₂.s_g]

Premises used: CategoryTheory.ShortComplex.Splitting.s_g
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
dsimp :
  HAdd.hAdd (α := X ⟶ biprod.{v_1, u_1} I₁ I₂) (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr) ≫
        HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s) +
      (g₁ ≫ g₂) ≫ σ₂.s ≫ σ₁.s =
    𝟙 X
⊢ HAdd.hAdd (α :=
          { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₂ ⟶
            biprod.{v_1, u_1}
              { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.X₁
              { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₁)
          (σ₁.r ≫ biprod.inl) (g₁ ≫ σ₂.r ≫ biprod.inr) ≫
        { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
            f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
            zero := ⋯ : ShortComplex.{v_1, u_1} C }.f +
      { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
            f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
            zero := ⋯ : ShortComplex.{v_1, u_1} C }.g ≫
        σ₂.s ≫ σ₁.s =
    𝟙
      { X₁ := I₁ ⊞ I₂, X₂ := X, X₃ := Z,
          f := HAdd.hAdd (α := biprod.{v_1, u_1} I₁ I₂ ⟶ X) (biprod.fst ≫ f₁) (biprod.snd ≫ f₂ ≫ σ₁.s), g := g₁ ≫ g₂,
          zero := ⋯ : ShortComplex.{v_1, u_1} C }.X₂

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
⊢ g₁ ≫
      (σ₂.r ≫ { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.f +
          { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.g ≫ σ₂.s) ≫
        σ₁.s =
    g₁ ≫ 𝟙 { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₂ ≫ σ₁.s

Tactic:
have h := g₁ ≫= σ₂.id =≫ σ₁.s
-- Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w : Injective.{v_1, u_1} I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.Splitting
I₂ : C
w_1 : Injective.{v_1, u_1} I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.Splitting
h :
  g₁ ≫
      (σ₂.r ≫ { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.f +
          { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.g ≫ σ₂.s) ≫
        σ₁.s =
    g₁ ≫ 𝟙 { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ : ShortComplex.{v_1, u_1} C }.X₂ ≫ σ₁.s
⊢ g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s = g₁ ≫ σ₁.s

Tactic:
simp only [add_comp, assoc, comp_add, id_comp] at h

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add, CategoryTheory.Category.id_comp