case tfae_1_iff_2
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0

C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_1_iff_2 : Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ TFAE [Exact f g, f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0, imageSubobject f = kernelSubobject g]
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ TFAE [Exact f g, f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0, imageSubobject f = kernelSubobject g]
tfae_have 1 ↔ 2
case tfae_1_iff_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_1_iff_2 : Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ Exact f g ↔ imageSubobject f = kernelSubobject g

C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_1_iff_2 : Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
tfae_1_iff_3 : Exact f g ↔ imageSubobject f = kernelSubobject g
⊢ TFAE [Exact f g, f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0, imageSubobject f = kernelSubobject g]
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_1_iff_2 : Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ TFAE [Exact f g, f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0, imageSubobject f = kernelSubobject g]
tfae_have 1 ↔ 3
no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_1_iff_2 : Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
tfae_1_iff_3 : Exact f g ↔ imageSubobject f = kernelSubobject g
⊢ TFAE [Exact f g, f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0, imageSubobject f = kernelSubobject g]
tfae_finish
no goals
case tfae_1_iff_2
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
apply exact_iff
no goals
case tfae_1_iff_3
C : Type u₁
inst✝¹ : Category C
inst✝ : Abelian C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
tfae_1_iff_2 : Exact f g ↔ f ≫ g = 0 ∧ kernel.ι g ≫ cokernel.π f = 0
⊢ Exact f g ↔ imageSubobject f = kernelSubobject g
apply exact_iff_image_eq_kernel