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 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 ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s = g₁ ≫ σ₁.s
rw :
  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 =
    σ₁.r ≫ { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.f +
      (g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s)
⊢ 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

Tactic:
rw [← σ₁.id, ← h]

Premises used: CategoryTheory.ShortComplex.Splitting.id
-- 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 ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s = g₁ ≫ σ₁.s
simp :
  σ₁.r ≫ f₁ + g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s =
    σ₁.r ≫ f₁ + (g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s)
⊢ 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 =
    σ₁.r ≫ { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ : ShortComplex.{v_1, u_1} C }.f +
      (g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s)

Tactic:
simp only [comp_add, add_comp, assoc, BinaryBicone.inl_fst_assoc,
              BinaryBicone.inr_fst_assoc, zero_comp, comp_zero, add_zero,
              BinaryBicone.inl_snd_assoc, BinaryBicone.inr_snd_assoc, zero_add]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.BinaryBicone.inl_fst_assoc, CategoryTheory.Limits.BinaryBicone.inl_snd_assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.BinaryBicone.inr_fst_assoc, zero_add, CategoryTheory.Preadditive.add_comp, CategoryTheory.Preadditive.comp_add, CategoryTheory.Limits.zero_comp, add_zero, CategoryTheory.Limits.BinaryBicone.inr_snd_assoc
-- 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 ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s = g₁ ≫ σ₁.s
⊢ σ₁.r ≫ f₁ + g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s =
    σ₁.r ≫ f₁ + (g₁ ≫ σ₂.r ≫ f₂ ≫ σ₁.s + g₁ ≫ g₂ ≫ σ₂.s ≫ σ₁.s)

Tactic:
abel
-- 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
⊢ { 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

Tactic:
exact
        { r := σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr
          s := σ₂.s ≫ σ₁.s
          f_r := by
            ext
            · simp [σ₁.f_r]
            · simp [reassoc_of% w₁]
            · simp
            · simp [reassoc_of% σ₁.s_g, σ₂.f_r]
          s_g := by simp [reassoc_of% σ₁.s_g, σ₂.s_g]
          id := by
            dsimp
            have h := g₁ ≫= σ₂.id =≫ σ₁.s
            simp only [add_comp, assoc, comp_add, id_comp] at h
            rw [← σ₁.id, ← h]
            simp only [comp_add, add_comp, assoc, BinaryBicone.inl_fst_assoc,
              BinaryBicone.inr_fst_assoc, zero_comp, comp_zero, add_zero,
              BinaryBicone.inl_snd_assoc, BinaryBicone.inr_snd_assoc, zero_add]
            abel }
-- 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' X Y : C
f' : X' ⟶ Y'
f : X ⟶ Y
r : RetractArrow f' f
left : Epi f
hf : Injective.{v_1, u_1} (kernel f)
⊢ Epi f'

Tactic:
have : Epi f' :=
      (MorphismProperty.epimorphisms C).of_retract r (.infer_property _)
-- 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' X Y : C
f' : X' ⟶ Y'
f : X ⟶ Y
r : RetractArrow f' f
left : Epi f
hf : Injective.{v_1, u_1} (kernel f)
this : Epi f'
h :
  CategoryStruct.comp (Y := equalizer f' 0)
      (CategoryStruct.comp (Y := kernel f) (kernel.map f' f (Arrow.Hom.left r.i) (Arrow.Hom.right r.i) ⋯)
        (kernel.map f f' (Arrow.Hom.left r.r) (Arrow.Hom.right r.r) ⋯))
      (equalizer.ι f' 0) =
    𝟙 (kernel f') ≫ equalizer.ι f' 0
⊢ CategoryStruct.comp (Y := kernel f) (kernel.map f' f (Arrow.Hom.left r.i) (Arrow.Hom.right r.i) ⋯)
      (kernel.map f f' (Arrow.Hom.left r.r) (Arrow.Hom.right r.r) ⋯) =
    𝟙 (kernel f')

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' X Y : C
f' : X' ⟶ Y'
f : X ⟶ Y
r : RetractArrow f' f
left : Epi f
hf : Injective.{v_1, u_1} (kernel f)
this : Epi f'
⊢ CategoryStruct.comp (Y := equalizer f' 0)
      (CategoryStruct.comp (Y := kernel f) (kernel.map f' f (Arrow.Hom.left r.i) (Arrow.Hom.right r.i) ⋯)
        (kernel.map f f' (Arrow.Hom.left r.r) (Arrow.Hom.right r.r) ⋯))
      (equalizer.ι f' 0) =
    𝟙 (kernel f') ≫ equalizer.ι f' 0

Tactic:
simp [dsimp% r.left.retract]

Premises used: CategoryTheory.Retract.retract, CategoryTheory.RetractArrow.left
-- 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' X Y : C
f' : X' ⟶ Y'
f : X ⟶ Y
r : RetractArrow f' f
left : Epi f
hf : Injective.{v_1, u_1} (kernel f)
this : Epi f'
r' : Retract (kernel f') (kernel f) :=
  { i := kernel.map f' f (Arrow.Hom.left r.i) (Arrow.Hom.right r.i) ⋯,
    r := kernel.map f f' (Arrow.Hom.left r.r) (Arrow.Hom.right r.r) ⋯, retract := ⋯ }
⊢ epiWithInjectiveKernel f'

Tactic:
⟨inferInstance, r'.injective⟩

Premises used: CategoryTheory.Abelian.epiWithInjectiveKernel, inferInstance, CategoryTheory.Retract.injective, And.intro
-- 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' X Y : C
f' : X' ⟶ Y'
f : X ⟶ Y
r : RetractArrow f' f
left : Epi f
hf : Injective.{v_1, u_1} (kernel f)
this : Epi f'
r' : Retract (kernel f') (kernel f) :=
  { i := kernel.map f' f (Arrow.Hom.left r.i) (Arrow.Hom.right r.i) ⋯,
    r := kernel.map f f' (Arrow.Hom.left r.r) (Arrow.Hom.right r.r) ⋯, retract := ⋯ }
⊢ epiWithInjectiveKernel f'

Tactic:
exact ⟨inferInstance, r'.injective⟩
-- 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
p : X ⟶ Y
hp : epiWithInjectiveKernel p
A B : C
i : A ⟶ B
inst_2 : Mono i
suffices : MorphismProperty.rlp (MorphismProperty.monomorphisms C) p
⊢ HasLiftingProperty i p

Tactic:
suffices (MorphismProperty.monomorphisms C).rlp p from this _ 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
p : X ⟶ Y
hp : epiWithInjectiveKernel p
A B : C
i : A ⟶ B
inst_2 : Mono i
rw :
  ∀
    (hp :
      ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ p = 0),
        Nonempty.{v_1 + 1}
          { X₁ := I, X₂ := X, X₃ := Y, f := f, g := p, zero := w : ShortComplex.{v_1, u_1} C }.Splitting)
    {A B : C} (i : A ⟶ B) [Mono i], MorphismProperty.rlp (MorphismProperty.monomorphisms C) p
⊢ MorphismProperty.rlp (MorphismProperty.monomorphisms C) p

Tactic:
rw [epiWithInjectiveKernel_iff] at hp

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
p : X ⟶ Y
hp :
  ∃ (I : C) (_ : Injective.{v_1, u_1} I) (f : I ⟶ X) (w : f ≫ p = 0),
    Nonempty.{v_1 + 1} { X₁ := I, X₂ := X, X₃ := Y, f := f, g := p, zero := w : ShortComplex.{v_1, u_1} C }.Splitting
A B : C
i : A ⟶ B
inst_2 : Mono i
obtain :
  ∀ (I : C),
    Injective.{v_1, u_1} I →
      ∀ (s : I ⟶ X) (hs : s ≫ p = 0)
        (σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.Splitting),
        MorphismProperty.rlp (MorphismProperty.monomorphisms C) p
⊢ MorphismProperty.rlp (MorphismProperty.monomorphisms C) p

Tactic:
obtain ⟨I, _, s, hs, ⟨σ⟩⟩ := hp
-- 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
p : X ⟶ Y
A B : C
i : A ⟶ B
inst_2 : Mono i
I : C
w : Injective.{v_1, u_1} I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.Splitting
⊢ MorphismProperty.rlp.{v_1, u_1} (MorphismProperty.monomorphisms C) (X := I) (Y := 0) 0

Tactic:
have hI : (MorphismProperty.monomorphisms C).rlp (0 : I ⟶ 0) :=
    fun _ _ _ _ ↦ Injective.hasLiftingProperty_of_isZero _ _ (isZero_zero C)
-- 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
p : X ⟶ Y
A B : C
i : A ⟶ B
inst_2 : Mono i
I : C
w : Injective.{v_1, u_1} I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.Splitting
hI : MorphismProperty.rlp.{v_1, u_1} (MorphismProperty.monomorphisms C) (X := I) (Y := 0) 0
⊢ CommSq (Z := 0) σ.r p 0 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
p : X ⟶ Y
A B : C
i : A ⟶ B
inst_2 : Mono i
I : C
w : Injective.{v_1, u_1} I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.Splitting
hI : MorphismProperty.rlp.{v_1, u_1} (MorphismProperty.monomorphisms C) (X := I) (Y := 0) 0
refine :
  IsLimit (F :=
    cospan (X := { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y)
      (Z := 0) 0 0)
    (PullbackCone.mk σ.r p ⋯)
⊢ MorphismProperty.rlp (MorphismProperty.monomorphisms C) p

Tactic:
refine MorphismProperty.of_isPullback (f' := σ.r) (f := 0) ⟨by simp, ⟨?_⟩⟩ hI

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.IsPullback.mk, Nonempty.intro
-- 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
p : X ⟶ Y
A B : C
i : A ⟶ B
inst_2 : Mono i
I : C
w : Injective.{v_1, u_1} I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.Splitting
hI : MorphismProperty.rlp.{v_1, u_1} (MorphismProperty.monomorphisms C) (X := I) (Y := 0) 0
t :
  PullbackCone.{v_1, u_1} (C := C) (X :=
    { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y) (Z := 0) 0 0
⊢ (fun
            (t :
              PullbackCone.{v_1, u_1} (C := C) (X :=
                { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y) (Z :=
                0) 0 0) ↦
          t.fst ≫ s + t.snd ≫ σ.s)
        t ≫
      σ.r =
    t.fst

Tactic:
simp [dsimp% σ.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 : C
p : X ⟶ Y
A B : C
i : A ⟶ B
inst_2 : Mono i
I : C
w : Injective.{v_1, u_1} I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.Splitting
hI : MorphismProperty.rlp.{v_1, u_1} (MorphismProperty.monomorphisms C) (X := I) (Y := 0) 0
t :
  PullbackCone.{v_1, u_1} (C := C) (X :=
    { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y) (Z := 0) 0 0
⊢ (fun
            (t :
              PullbackCone.{v_1, u_1} (C := C) (X :=
                { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y) (Z :=
                0) 0 0) ↦
          t.fst ≫ s + t.snd ≫ σ.s)
        t ≫
      p =
    t.snd

Tactic:
simp [hs, dsimp% σ.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 : C
p : X ⟶ Y
A B : C
i : A ⟶ B
inst_2 : Mono i
I : C
w : Injective.{v_1, u_1} I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.Splitting
hI : MorphismProperty.rlp.{v_1, u_1} (MorphismProperty.monomorphisms C) (X := I) (Y := 0) 0
refine :
  ∀
    (t :
      PullbackCone.{v_1, u_1} (C := C) (X :=
        { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y) (Z := 0) 0 0)
    (m : t.pt ⟶ { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₂)
    (hm₁ : m ≫ σ.r = t.fst) (hm₂ : m ≫ p = t.snd),
    m =
      (fun
            (t :
              PullbackCone.{v_1, u_1} (C := C) (X :=
                { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y) (Z :=
                0) 0 0) ↦
          t.fst ≫ s + t.snd ≫ σ.s)
        t
⊢ IsLimit (F :=
    cospan (X := { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y)
      (Z := 0) 0 0)
    (PullbackCone.mk σ.r p ⋯)

Tactic:
refine PullbackCone.IsLimit.mk _ (fun t ↦ t.fst ≫ s + t.snd ≫ σ.s)
    (fun t ↦ by simp [dsimp% σ.f_r]) (fun t ↦ by simp [hs, dsimp% σ.s_g]) (fun t m hm₁ hm₂ ↦ ?_)

Premises used: CategoryTheory.Limits.PullbackCone.fst, CategoryTheory.Limits.PullbackCone.IsLimit.mk, HAdd.hAdd, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.PullbackCone.snd, 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 : C
p : X ⟶ Y
A B : C
i : A ⟶ B
inst_2 : Mono i
I : C
w : Injective.{v_1, u_1} I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.Splitting
hI : MorphismProperty.rlp.{v_1, u_1} (MorphismProperty.monomorphisms C) (X := I) (Y := 0) 0
t :
  PullbackCone.{v_1, u_1} (C := C) (X :=
    { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y) (Z := 0) 0 0
m : t.pt ⟶ { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₂
hm₁ : m ≫ σ.r = t.fst
hm₂ : m ≫ p = t.snd
⊢ m =
    (fun
          (t :
            PullbackCone.{v_1, u_1} (C := C) (X :=
              { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs : ShortComplex.{v_1, u_1} C }.X₁) (Y := Y) (Z :=
              0) 0 0) ↦
        t.fst ≫ s + t.snd ≫ σ.s)
      t

Tactic:
simp [← hm₁, ← hm₂, ← Preadditive.comp_add, dsimp% σ.id]

Premises used: CategoryTheory.ShortComplex.Splitting.id, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
rw :
  Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯) ↔
    Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)
⊢ S.Exact ↔ Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)

Tactic:
rw [S.exact_iff_epi_kernel_lift]

Premises used: CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ Eq (α := S.X₁ ⟶ kernel S.g)
    (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
        (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) :
      S.X₁ ⟶ kernel S.g)
    (kernel.lift S.g S.f ⋯ : S.X₁ ⟶ kernel S.g)

Tactic:
simp only [← cancel_mono (kernel.ι _), kernel.lift_ι, imageToKernel',
      Category.assoc, image.fac]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.image.fac, CategoryTheory.cancel_mono, imageToKernel', CategoryTheory.Limits.kernel.lift_ι, CategoryTheory.Limits.kernel.ι
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ Eq (α := S.X₁ ⟶ kernel S.g)
    (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
        (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) :
      S.X₁ ⟶ kernel S.g)
    (kernel.lift S.g S.f ⋯ : S.X₁ ⟶ kernel S.g)

Tactic:
have : factorThruImage S.f ≫ imageToKernel' S.f S.g S.zero = kernel.lift S.g S.f S.zero := by
    simp only [← cancel_mono (kernel.ι _), kernel.lift_ι, imageToKernel',
      Category.assoc, image.fac]
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
this :
  Eq (α := S.X₁ ⟶ kernel S.g)
    (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
        (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) :
      S.X₁ ⟶ kernel S.g)
    (kernel.lift S.g S.f ⋯ : S.X₁ ⟶ kernel S.g)
mp :
  Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯) →
    Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)
mpr :
  Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) →
    Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
⊢ Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯) ↔
    Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
this :
  Eq (α := S.X₁ ⟶ kernel S.g)
    (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
        (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) :
      S.X₁ ⟶ kernel S.g)
    (kernel.lift S.g S.f ⋯ : S.X₁ ⟶ kernel S.g)
h : Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
⊢ Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)

Tactic:
epi_of_epi_fac this

Premises used: CategoryTheory.epi_of_epi_fac
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
this :
  Eq (α := S.X₁ ⟶ kernel S.g)
    (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
        (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) :
      S.X₁ ⟶ kernel S.g)
    (kernel.lift S.g S.f ⋯ : S.X₁ ⟶ kernel S.g)
h : Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯)
⊢ Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)

Tactic:
exact epi_of_epi_fac this

Premises used: CategoryTheory.epi_of_epi_fac
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
this :
  Eq (α := S.X₁ ⟶ kernel S.g)
    (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
        (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) :
      S.X₁ ⟶ kernel S.g)
    (kernel.lift S.g S.f ⋯ : S.X₁ ⟶ kernel S.g)
h : Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)
mpr :
  Epi (Y := kernel S.g)
    (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
        (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) :
      S.X₁ ⟶ kernel S.g)
⊢ Epi (Y := kernel S.g) (kernel.lift S.g S.f ⋯)

Tactic:
rw [← this]
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
this :
  Eq (α := S.X₁ ⟶ kernel S.g)
    (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
        (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) :
      S.X₁ ⟶ kernel S.g)
    (kernel.lift S.g S.f ⋯ : S.X₁ ⟶ kernel S.g)
h : Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g)
⊢ Epi (Y := kernel S.g)
    (CategoryStruct.comp (Y := image S.f) (factorThruImage S.f : S.X₁ ⟶ image S.f)
        (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) :
      S.X₁ ⟶ kernel S.g)

Tactic:
apply epi_comp

Premises used: CategoryTheory.epi_comp
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
rw :
  Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) ↔
    Epi (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)
⊢ S.Exact ↔
    Epi (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)

Tactic:
rw [S.exact_iff_epi_imageToKernel']

Premises used: CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel'
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
apply :
  Arrow.mk (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) ≅
    Arrow.mk (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)
⊢ Epi (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) ↔
    Epi (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)

Tactic:
apply (MorphismProperty.epimorphisms C).arrow_mk_iso_iff

Premises used: CategoryTheory.MorphismProperty.epimorphisms, CategoryTheory.MorphismProperty.arrow_mk_iso_iff
-- Module: Mathlib.CategoryTheory.Abelian.Exact
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Abelian.{v₁, u₁} C
S : ShortComplex.{v₁, u₁} C
⊢ Arrow.mk (X := image S.f) (Y := kernel S.g) (imageToKernel' S.f S.g ⋯ : image S.f ⟶ kernel S.g) ≅
    Arrow.mk (X := Functor.obj Subobject.underlying (imageSubobject S.f)) (Y :=
      Functor.obj Subobject.underlying (kernelSubobject S.g)) (imageToKernel S.f S.g ⋯)

Tactic:
exact Arrow.isoMk (imageSubobjectIso S.f).symm (kernelSubobjectIso S.g).symm

Premises used: CategoryTheory.Arrow.isoMk