V : Type u
inst✝¹ : Category 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
V : Type u
inst✝¹ : Category 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
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 _ _
V : Type u
inst✝¹ : Category 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
V : Type u
inst✝¹ : Category 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
let y : R ⟶ pushout r g' := pushout.inl
V : Type u
inst✝¹ : Category 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
V : Type u
inst✝¹ : Category 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
let z : C' ⟶ pushout r g' := pushout.inr
V : Type u
inst✝¹ : Category 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
V : Type u
inst✝¹ : Category 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
have : Mono (cokernel.desc f' g' hf'g'.w) := mono_cokernel_desc_of_exact _ _ hf'g'
V : Type u
inst✝¹ : Category 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
V : Type u
inst✝¹ : Category 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
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 _)
V : Type u
inst✝¹ : Category 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
V : Type u
inst✝¹ : Category 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
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 _ _
V : Type u
inst✝¹ : Category 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
V : Type u
inst✝¹ : Category 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
let v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
V : Type u
inst✝¹ : Category 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
V : Type u
inst✝¹ : Category 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
let w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
V : Type u
inst✝¹ : Category 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
V : Type u
inst✝¹ : Category 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
have : Mono (cokernel.desc g h hgh.w) := mono_cokernel_desc_of_exact _ _ hgh
V : Type u
inst✝¹ : Category 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
V : Type u
inst✝¹ : Category 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
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 _)
V : Type u
inst✝¹ : Category 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
V : Type u
inst✝¹ : Category 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
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₃]
V : Type u
inst✝¹ : Category 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
V : Type u
inst✝¹ : Category 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
suffices (r ≫ y) ≫ v = 0 from zero_of_comp_mono _ (zero_of_comp_mono _ this)
no goals
V : Type u
inst✝¹ : Category 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
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 _ _
no goals
V : Type u
inst✝¹ : Category 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
rw [reassoc_of% comm₁]
no goals
V : Type u
inst✝¹ : Category 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
rw [hβr]
no goals
V : Type u
inst✝¹ : Category 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'
simp
no goals
V : Type u
inst✝¹ : Category 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
simp
no goals
V : Type u
inst✝¹ : Category 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
rw [← reassoc_of% comm₂]
no goals
V : Type u
inst✝¹ : Category 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
rw [← pushout.condition]
no goals
V : Type u
inst✝¹ : Category 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
rw [reassoc_of% hβr]
no goals
V : Type u
inst✝¹ : Category 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 ≫ δ
simp
no goals
V : Type u
inst✝¹ : Category 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
simp
no goals
V : Type u
inst✝¹ : Category 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
rw [← Category.assoc, pushout.condition, Category.assoc]
no goals
V : Type u
inst✝¹ : Category 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
rw [reassoc_of% comm₃]
no goals
V : Type u
inst✝¹ : Category 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
rw [pushout.condition, Category.assoc]
no goals
V : Type u
inst✝¹ : Category 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
rw [hzv]