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 ≫ δ
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✝³ : IsIso α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : IsIso ε
⊢ Mono γ
apply mono_of_epi_of_mono_of_mono comm₁ comm₂ comm₃ hfg hgh hf'g' <;> infer_instance
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 ≫ δ
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✝³ : IsIso α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : IsIso ε
this : Mono γ
⊢ Epi γ
apply epi_of_epi_of_epi_of_mono comm₂ comm₃ comm₄ hhi hg'h' hh'i' <;> infer_instance