-- Mathlib/Algebra/Homology/HomologySequenceLemmas.lean
lemma epi_homologyMap_τ₃ (i : ι)
    (h₁ : Epi (homologyMap φ.τ₂ i))
    (h₂ : ∀ j, c.Rel i j → Epi (homologyMap φ.τ₁ j))
    (h₃ : ∀ j, c.Rel i j → Mono (homologyMap φ.τ₂ j)) :
    Epi (homologyMap φ.τ₃ i)

Proof state:
case pos
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ∃ j, c.Rel i j
⊢ Epi (homologyMap φ.τ₃ i)

Tactic:
obtain ⟨j, hij⟩ := hi

Result:
case pos.intro
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi (homologyMap φ.τ₃ i)

Proof state:
case pos.intro.hR₁
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ ((δ₀Functor ⋙ δlastFunctor).obj (composableArrows₅ hS₁ i j hij)).Exact

Tactic:
exact (composableArrows₅_exact hS₁ i j hij).δ₀.δlast

Result:
no goals

Proof state:
case pos.intro.h₀
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 0 ⋯)

Tactic:
exact h₁

Result:
no goals

Proof state:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ¬∃ j, c.Rel i j
this✝ : Epi S₂.g
eq : homologyMap φ.τ₂ i ≫ homologyMap S₂.g i = homologyMap S₁.g i ≫ homologyMap φ.τ₃ i
this : Epi (homologyMap S₂.g i)
⊢ Epi (homologyMap φ.τ₃ i)

Tactic:
exact epi_of_epi_fac eq.symm

Result:
no goals

Proof state:
case pos.intro
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi (homologyMap φ.τ₃ i)

Tactic:
apply epi_of_epi_of_epi_of_mono
  ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij))

Result:
case pos.intro.hR₁
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ ((δ₀Functor ⋙ δlastFunctor).obj (composableArrows₅ hS₁ i j hij)).Exact

case pos.intro.hR₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ ((δ₀Functor ⋙ δlastFunctor).obj (composableArrows₅ hS₂ i j hij)).Exact

case pos.intro.h₀
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 0 ⋯)

case pos.intro.h₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Epi (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 2 ⋯)

case pos.intro.h₃
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Mono (app' ((δ₀Functor ⋙ δlastFunctor).map (mapComposableArrows₅ φ hS₁ hS₂ i j hij)) 3 ⋯)

Proof state:
case pos.intro.hR₂
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ ((δ₀Functor ⋙ δlastFunctor).obj (composableArrows₅ hS₂ i j hij)).Exact

Tactic:
exact (composableArrows₅_exact hS₂ i j hij).δ₀.δlast

Result:
no goals

Proof state:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ¬∃ j, c.Rel i j
this : Epi S₂.g
eq : (homologyFunctor C c i).map (φ.τ₂ ≫ S₂.g) = (homologyFunctor C c i).map (S₁.g ≫ φ.τ₃)
⊢ Epi (homologyMap φ.τ₃ i)

Tactic:
dsimp at eq

Result:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S₁ S₂ : ShortComplex (HomologicalComplex C c)
φ : S₁ ⟶ S₂
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
i : ι
h₁ : Epi (homologyMap φ.τ₂ i)
h₂ : ∀ (j : ι), c.Rel i j → Epi (homologyMap φ.τ₁ j)
h₃ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
hi : ¬∃ j, c.Rel i j
this : Epi S₂.g
eq : homologyMap (φ.τ₂ ≫ S₂.g) i = homologyMap (S₁.g ≫ φ.τ₃) i
⊢ Epi (homologyMap φ.τ₃ i)