-- Mathlib/CategoryTheory/Abelian/EpiWithInjectiveKernel.lean
/-- A morphism `g : X ⟶ Y` is epi with an injective kernel iff there exists a morphism
`f : I ⟶ X` with `I` injective such that `f ≫ g = 0` and
the short complex `I ⟶ X ⟶ Y` has a splitting. -/
lemma epiWithInjectiveKernel_iff {X Y : C} (g : X ⟶ Y) :
    epiWithInjectiveKernel g ↔ ∃ (I : C) (_ : Injective I) (f : I ⟶ X) (w : f ≫ g = 0),
      Nonempty (ShortComplex.mk f g w).Splitting

Proof state:
case mpr.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
I : C
w✝ : Injective I
f : I ⟶ X
w : f ≫ g = 0
σ : (ShortComplex.mk f g w).Splitting
this : IsSplitEpi g
e : I ≅ kernel g := ⋯.fIsKernel.conePointUniqueUpToIso (limit.isLimit (parallelPair (ShortComplex.mk f g w).g 0))
⊢ epiWithInjectiveKernel g

Tactic:
exact ⟨inferInstance, Injective.of_iso e inferInstance⟩

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
⊢ epiWithInjectiveKernel g →
    ∃ I, ∃ (_ : Injective I), ∃ f, ∃ (w : f ≫ g = 0), Nonempty (ShortComplex.mk f g w).Splitting

Tactic:
rintro ⟨_, _⟩

Result:
case mp.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
left✝ : Epi g
right✝ : Injective (kernel g)
⊢ ∃ I, ∃ (_ : Injective I), ∃ f, ∃ (w : f ≫ g = 0), Nonempty (ShortComplex.mk f g w).Splitting

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
⊢ epiWithInjectiveKernel g ↔
    ∃ I, ∃ (_ : Injective I), ∃ f, ∃ (w : f ≫ g = 0), Nonempty (ShortComplex.mk f g w).Splitting

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
⊢ epiWithInjectiveKernel g →
    ∃ I, ∃ (_ : Injective I), ∃ f, ∃ (w : f ≫ g = 0), Nonempty (ShortComplex.mk f g w).Splitting

case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
⊢ (∃ I, ∃ (_ : Injective I), ∃ f, ∃ (w : f ≫ g = 0), Nonempty (ShortComplex.mk f g w).Splitting) →
    epiWithInjectiveKernel g

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
left✝ : Epi g
right✝ : Injective (kernel g)
S : ShortComplex C := ShortComplex.mk (kernel.ι g) g ⋯
⊢ S.f ≫ Injective.factorThru (𝟙 S.X₁) (kernel.ι g) = 𝟙 S.X₁

Tactic:
simp [S]

Result:
no goals

Proof state:
case mp.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
left✝ : Epi g
right✝ : Injective (kernel g)
⊢ ∃ I, ∃ (_ : Injective I), ∃ f, ∃ (w : f ≫ g = 0), Nonempty (ShortComplex.mk f g w).Splitting

Tactic:
let S := ShortComplex.mk (kernel.ι g) g (by simp)

Result:
case mp.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
left✝ : Epi g
right✝ : Injective (kernel g)
S : ShortComplex C := ShortComplex.mk (kernel.ι g) g ⋯
⊢ ∃ I, ∃ (_ : Injective I), ∃ f, ∃ (w : f ≫ g = 0), Nonempty (ShortComplex.mk f g w).Splitting

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
left✝ : Epi g
right✝ : Injective (kernel g)
⊢ kernel.ι g ≫ g = 0

Tactic:
simp

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
I : C
w✝ : Injective I
f : I ⟶ X
w : f ≫ g = 0
σ : (ShortComplex.mk f g w).Splitting
this : IsSplitEpi g
⊢ epiWithInjectiveKernel g

Tactic:
let e : I ≅ kernel g :=
  IsLimit.conePointUniqueUpToIso σ.shortExact.fIsKernel (limit.isLimit _)

Result:
case mpr.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
I : C
w✝ : Injective I
f : I ⟶ X
w : f ≫ g = 0
σ : (ShortComplex.mk f g w).Splitting
this : IsSplitEpi g
e : I ≅ kernel g := ⋯.fIsKernel.conePointUniqueUpToIso (limit.isLimit (parallelPair (ShortComplex.mk f g w).g 0))
⊢ epiWithInjectiveKernel g

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
⊢ (∃ I, ∃ (_ : Injective I), ∃ f, ∃ (w : f ≫ g = 0), Nonempty (ShortComplex.mk f g w).Splitting) →
    epiWithInjectiveKernel g

Tactic:
rintro ⟨I, _,  f, w, ⟨σ⟩⟩

Result:
case mpr.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
I : C
w✝ : Injective I
f : I ⟶ X
w : f ≫ g = 0
σ : (ShortComplex.mk f g w).Splitting
⊢ epiWithInjectiveKernel g

Proof state:
case mp.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
left✝ : Epi g
right✝ : Injective (kernel g)
S : ShortComplex C := ShortComplex.mk (kernel.ι g) g ⋯
⊢ ∃ I, ∃ (_ : Injective I), ∃ f, ∃ (w : f ≫ g = 0), Nonempty (ShortComplex.mk f g w).Splitting

Tactic:
exact ⟨_, inferInstance, _, S.zero,
  ⟨ShortComplex.Splitting.ofExactOfRetraction S
    (S.exact_of_f_is_kernel (kernelIsKernel g)) (Injective.factorThru (𝟙 _) (kernel.ι g))
    (by simp [S]) inferInstance⟩⟩

Result:
no goals

Proof state:
case mpr.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
I : C
w✝ : Injective I
f : I ⟶ X
w : f ≫ g = 0
σ : (ShortComplex.mk f g w).Splitting
⊢ epiWithInjectiveKernel g

Tactic:
have : IsSplitEpi g := ⟨σ.s, σ.s_g⟩

Result:
case mpr.intro.intro.intro.intro.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
I : C
w✝ : Injective I
f : I ⟶ X
w : f ≫ g = 0
σ : (ShortComplex.mk f g w).Splitting
this : IsSplitEpi g
⊢ epiWithInjectiveKernel g