-- Mathlib/CategoryTheory/Abelian/Exact.lean
theorem exact_iff_image_eq_kernel : S.Exact ↔ imageSubobject S.f = kernelSubobject S.g

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ ((kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯ ≫ imageToKernel S.f S.g ⋯) ≫ (kernelSubobject S.g).arrow =
    𝟙 (Subobject.underlying.obj (kernelSubobject S.g)) ≫ (kernelSubobject S.g).arrow

Tactic:
simp

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ (imageToKernel S.f S.g ⋯ ≫ (kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯) ≫ (imageSubobject S.f).arrow =
    𝟙 (Subobject.underlying.obj (imageSubobject S.f)) ≫ (imageSubobject S.f).arrow

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ S.Exact ↔ imageSubobject S.f = kernelSubobject S.g

Tactic:
rw [exact_iff_isIso_imageToKernel]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ IsIso (imageToKernel S.f S.g ⋯) ↔ imageSubobject S.f = kernelSubobject S.g

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
a✝ : IsIso (imageToKernel S.f S.g ⋯)
⊢ imageSubobject S.f = kernelSubobject S.g

Tactic:
exact Subobject.eq_of_comm (asIso (imageToKernel _ _ S.zero)) (by simp)

Result:
no goals

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ IsIso (imageToKernel S.f S.g ⋯)

Tactic:
exact ⟨Subobject.ofLE _ _ h.ge, by ext; simp, by ext; simp⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
a✝ : IsIso (imageToKernel S.f S.g ⋯)
⊢ (asIso (imageToKernel S.f S.g ⋯)).hom ≫ (kernelSubobject S.g).arrow = (imageSubobject S.f).arrow

Tactic:
simp

Result:
no goals

Proof state:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ IsIso (imageToKernel S.f S.g ⋯) → imageSubobject S.f = kernelSubobject S.g

Tactic:
intro

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
a✝ : IsIso (imageToKernel S.f S.g ⋯)
⊢ imageSubobject S.f = kernelSubobject S.g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ imageToKernel S.f S.g ⋯ ≫ (kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯ =
    𝟙 (Subobject.underlying.obj (imageSubobject S.f))

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ (imageToKernel S.f S.g ⋯ ≫ (kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯) ≫ (imageSubobject S.f).arrow =
    𝟙 (Subobject.underlying.obj (imageSubobject S.f)) ≫ (imageSubobject S.f).arrow

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ IsIso (imageToKernel S.f S.g ⋯) ↔ imageSubobject S.f = kernelSubobject S.g

Tactic:
constructor

Result:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ IsIso (imageToKernel S.f S.g ⋯) → imageSubobject S.f = kernelSubobject S.g

case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ imageSubobject S.f = kernelSubobject S.g → IsIso (imageToKernel S.f S.g ⋯)

Proof state:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ imageSubobject S.f = kernelSubobject S.g → IsIso (imageToKernel S.f S.g ⋯)

Tactic:
intro h

Result:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ IsIso (imageToKernel S.f S.g ⋯)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ (kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯ ≫ imageToKernel S.f S.g ⋯ =
    𝟙 (Subobject.underlying.obj (kernelSubobject S.g))

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
h : imageSubobject S.f = kernelSubobject S.g
⊢ ((kernelSubobject S.g).ofLE (imageSubobject S.f) ⋯ ≫ imageToKernel S.f S.g ⋯) ≫ (kernelSubobject S.g).arrow =
    𝟙 (Subobject.underlying.obj (kernelSubobject S.g)) ≫ (kernelSubobject S.g).arrow