[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
⊢ pseudoApply δ (pseudoApply h c) = pseudoApply h' (pseudoApply γ c)
[PROOFSTEP]
rw [← Pseudoelement.comp_apply, ← comm₃, Pseudoelement.comp_apply]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
⊢ pseudoApply h' (pseudoApply γ c) = pseudoApply h' 0
[PROOFSTEP]
rw [hc]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
this : pseudoApply h c = 0
b : Pseudoelement B
hb : pseudoApply g b = c
⊢ pseudoApply g' (pseudoApply β b) = pseudoApply γ (pseudoApply g b)
[PROOFSTEP]
rw [← Pseudoelement.comp_apply, comm₂, Pseudoelement.comp_apply]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
this : pseudoApply h c = 0
b : Pseudoelement B
hb : pseudoApply g b = c
⊢ pseudoApply γ (pseudoApply g b) = pseudoApply γ c
[PROOFSTEP]
rw [hb]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
this✝ : pseudoApply h c = 0
b : Pseudoelement B
hb : pseudoApply g b = c
this : pseudoApply g' (pseudoApply β b) = 0
a' : Pseudoelement A'
ha' : pseudoApply f' a' = pseudoApply β b
a : Pseudoelement A
ha : pseudoApply α a = a'
⊢ pseudoApply β (pseudoApply f a) = pseudoApply f' (pseudoApply α a)
[PROOFSTEP]
rw [← Pseudoelement.comp_apply, ← comm₁, Pseudoelement.comp_apply]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
this✝ : pseudoApply h c = 0
b : Pseudoelement B
hb : pseudoApply g b = c
this : pseudoApply g' (pseudoApply β b) = 0
a' : Pseudoelement A'
ha' : pseudoApply f' a' = pseudoApply β b
a : Pseudoelement A
ha : pseudoApply α a = a'
⊢ pseudoApply f' (pseudoApply α a) = pseudoApply f' a'
[PROOFSTEP]
rw [ha]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
this✝¹ : pseudoApply h c = 0
b : Pseudoelement B
hb : pseudoApply g b = c
this✝ : pseudoApply g' (pseudoApply β b) = 0
a' : Pseudoelement A'
ha' : pseudoApply f' a' = pseudoApply β b
a : Pseudoelement A
ha : pseudoApply α a = a'
this : pseudoApply f a = b
⊢ pseudoApply g b = pseudoApply g (pseudoApply f a)
[PROOFSTEP]
rw [this]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
⊢ r = 0
[PROOFSTEP]
have hf'r : f' ≫ r = 0 :=
  Limits.zero_of_epi_comp α <|
    calc
      α ≫ f' ≫ r = f ≫ β ≫ r := by rw [reassoc_of% comm₁]
      _ = f ≫ 0 := by rw [hβr]
      _ = 0 := HasZeroMorphisms.comp_zero _ _
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
⊢ α ≫ f' ≫ r = f ≫ β ≫ r
[PROOFSTEP]
rw [reassoc_of% comm₁]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
⊢ f ≫ β ≫ r = f ≫ 0
[PROOFSTEP]
rw [hβr]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
⊢ r = 0
[PROOFSTEP]
let y : R ⟶ pushout r g' := pushout.inl
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
⊢ r = 0
[PROOFSTEP]
let z : C' ⟶ pushout r g' := pushout.inr
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
⊢ r = 0
[PROOFSTEP]
have : Mono (cokernel.desc f' g' hf'g'.w) := mono_cokernel_desc_of_exact _ _ hf'g'
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
⊢ r = 0
[PROOFSTEP]
have : Mono y :=
  mono_inl_of_factor_thru_epi_mono_factorization r g' (cokernel.π f') (cokernel.desc f' g' hf'g'.w) (by simp)
    (cokernel.desc f' r hf'r) (by simp) _ (colimit.isColimit _)
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
⊢ cokernel.π f' ≫ cokernel.desc f' g' (_ : f' ≫ g' = 0) = g'
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
⊢ cokernel.π f' ≫ cokernel.desc f' r hf'r = r
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
⊢ r = 0
[PROOFSTEP]
have hz : g ≫ γ ≫ z = 0 :=
  calc
    g ≫ γ ≫ z = β ≫ g' ≫ z := by rw [← reassoc_of% comm₂]
    _ = β ≫ r ≫ y := by rw [← pushout.condition]
    _ = 0 ≫ y := by rw [reassoc_of% hβr]
    _ = 0 := HasZeroMorphisms.zero_comp _ _
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
⊢ g ≫ γ ≫ z = β ≫ g' ≫ z
[PROOFSTEP]
rw [← reassoc_of% comm₂]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
⊢ β ≫ g' ≫ z = β ≫ r ≫ y
[PROOFSTEP]
rw [← pushout.condition]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
⊢ β ≫ r ≫ y = 0 ≫ y
[PROOFSTEP]
rw [reassoc_of% hβr]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
hz : g ≫ γ ≫ z = 0
⊢ r = 0
[PROOFSTEP]
let v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
⊢ r = 0
[PROOFSTEP]
let w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
⊢ r = 0
[PROOFSTEP]
have : Mono (cokernel.desc g h hgh.w) := mono_cokernel_desc_of_exact _ _ hgh
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝¹ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this : Mono (cokernel.desc g h (_ : g ≫ h = 0))
⊢ r = 0
[PROOFSTEP]
have : Mono v :=
  mono_inl_of_factor_thru_epi_mono_factorization _ _ (cokernel.π g) (cokernel.desc g h hgh.w ≫ δ) (by simp)
    (cokernel.desc _ _ hz) (by simp) _ (colimit.isColimit _)
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝¹ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this : Mono (cokernel.desc g h (_ : g ≫ h = 0))
⊢ cokernel.π g ≫ cokernel.desc g h (_ : g ≫ h = 0) ≫ δ = h ≫ δ
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝¹ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this : Mono (cokernel.desc g h (_ : g ≫ h = 0))
⊢ cokernel.π g ≫ cokernel.desc g (γ ≫ z) hz = γ ≫ z
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
⊢ r = 0
[PROOFSTEP]
have hzv : z ≫ v = h' ≫ w :=
  (cancel_epi γ).1 <|
    calc
      γ ≫ z ≫ v = h ≫ δ ≫ w := by rw [← Category.assoc, pushout.condition, Category.assoc]
      _ = γ ≫ h' ≫ w := by rw [reassoc_of% comm₃]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
⊢ γ ≫ z ≫ v = h ≫ δ ≫ w
[PROOFSTEP]
rw [← Category.assoc, pushout.condition, Category.assoc]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
⊢ h ≫ δ ≫ w = γ ≫ h' ≫ w
[PROOFSTEP]
rw [reassoc_of% comm₃]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
hzv : z ≫ v = h' ≫ w
⊢ r = 0
[PROOFSTEP]
suffices (r ≫ y) ≫ v = 0 from zero_of_comp_mono _ (zero_of_comp_mono _ this)
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
hzv : z ≫ v = h' ≫ w
⊢ (r ≫ y) ≫ v = 0
[PROOFSTEP]
calc
  (r ≫ y) ≫ v = g' ≫ z ≫ v := by rw [pushout.condition, Category.assoc]
  _ = g' ≫ h' ≫ w := by rw [hzv]
  _ = 0 ≫ w := (hg'h'.w_assoc _)
  _ = 0 := HasZeroMorphisms.zero_comp _ _
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
hzv : z ≫ v = h' ≫ w
⊢ (r ≫ y) ≫ v = g' ≫ z ≫ v
[PROOFSTEP]
rw [pushout.condition, Category.assoc]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
hzv : z ≫ v = h' ≫ w
⊢ g' ≫ z ≫ v = g' ≫ h' ≫ w
[PROOFSTEP]
rw [hzv]
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
⊢ Mono γ
[PROOFSTEP]
apply mono_of_epi_of_mono_of_mono comm₁ comm₂ comm₃ hfg hgh hf'g'
[GOAL]
case hα
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
⊢ Epi α
[PROOFSTEP]
infer_instance
[GOAL]
case hβ
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
⊢ Mono β
[PROOFSTEP]
infer_instance
[GOAL]
case hδ
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
⊢ Mono δ
[PROOFSTEP]
infer_instance
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
this : Mono γ
⊢ Epi γ
[PROOFSTEP]
apply epi_of_epi_of_epi_of_mono comm₂ comm₃ comm₄ hhi hg'h' hh'i'
[GOAL]
case hα
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
this : Mono γ
⊢ Epi β
[PROOFSTEP]
infer_instance
[GOAL]
case hγ
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
this : Mono γ
⊢ Epi δ
[PROOFSTEP]
infer_instance
[GOAL]
case hδ
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
this : Mono γ
⊢ Mono ε
[PROOFSTEP]
infer_instance
