chore: trivial generalization of the five lemma (#6181)

leanprover-community · Jul 28, 2023 · 0536332 · 0536332
1 parent aefe18a
commit 0536332
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/Mathlib/Algebra/Homology/ShortExact/Abelian.lean b/Mathlib/Algebra/Homology/ShortExact/Abelian.lean
@@ -35,7 +35,7 @@ theorem isIso_of_shortExact_of_isIso_of_isIso (h : ShortExact f g) (h' : ShortEx
     (comm₂ : i₂ ≫ g' = g ≫ i₃ := by aesop_cat) [IsIso i₁] [IsIso i₃] : IsIso i₂ := by
   obtain ⟨_⟩ := h
   obtain ⟨_⟩ := h'
-  refine @Abelian.isIso_of_isIso_of_isIso_of_isIso_of_isIso 𝒜 _ _ 0 _ _ _ 0 _ _ _ 0 f g 0 f' g'
+  refine @Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono 𝒜 _ _ 0 _ _ _ 0 _ _ _ 0 f g 0 f' g'
       0 i₁ i₂ i₃ ?_ comm₁ comm₂ 0 0 0 0 0 ?_ ?_ ?_ ?_ ?_ ?_ ?_ _ _ _ _
   all_goals try simp
   all_goals try assumption

diff --git a/Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean b/Mathlib/CategoryTheory/Abelian/DiagramLemmas/Four.lean
@@ -192,7 +192,7 @@ variable (hfg : Exact f g) (hgh : Exact g h) (hhi : Exact h i)
 
 variable (hf'g' : Exact f' g') (hg'h' : Exact g' h') (hh'i' : Exact h' i')
 
-variable [IsIso α] [IsIso β] [IsIso δ] [IsIso ε]
+variable [Epi α] [IsIso β] [IsIso δ] [Mono ε]
 
 /-- The five lemma. For names of objects and morphisms, refer to the following diagram:
 
@@ -205,13 +205,13 @@ v         v         v         v         v
 A' --f'-> B' --g'-> C' --h'-> D' --i'-> E'
 ```
 -/
-theorem isIso_of_isIso_of_isIso_of_isIso_of_isIso : IsIso γ :=
+theorem isIso_of_epi_of_isIso_of_isIso_of_mono : IsIso γ :=
   have : Mono γ := by
     apply mono_of_epi_of_mono_of_mono comm₁ comm₂ comm₃ hfg hgh hf'g' <;> infer_instance
   have : Epi γ := by
     apply epi_of_epi_of_epi_of_mono comm₂ comm₃ comm₄ hhi hg'h' hh'i' <;> infer_instance
   isIso_of_mono_of_epi _
-#align category_theory.abelian.is_iso_of_is_iso_of_is_iso_of_is_iso_of_is_iso CategoryTheory.Abelian.isIso_of_isIso_of_isIso_of_isIso_of_isIso
+#align category_theory.abelian.is_iso_of_is_iso_of_is_iso_of_is_iso_of_is_iso CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono
 
 end Five