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

Proof state:
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₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
this✝ : Mono (homologyMap φ.τ₃ i)
this : Epi (homologyMap φ.τ₃ i)
⊢ IsIso (homologyMap φ.τ₃ i)

Tactic:
apply isIso_of_mono_of_epi

Result:
no goals

Proof state:
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₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
this : Mono (homologyMap φ.τ₃ i)
j : ι
hij : c.Rel i j
⊢ Epi (homologyMap φ.τ₁ j)

Tactic:
have := h₃ j hij

Result:
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₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
this✝ : Mono (homologyMap φ.τ₃ i)
j : ι
hij : c.Rel i j
this : IsIso (homologyMap φ.τ₁ j)
⊢ Epi (homologyMap φ.τ₁ j)

Proof state:
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₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
⊢ Mono (homologyMap φ.τ₁ j)

Tactic:
have := h₃ j hij

Result:
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₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
this : IsIso (homologyMap φ.τ₁ j)
⊢ Mono (homologyMap φ.τ₁ j)

Proof state:
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₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
j : ι
hij : c.Rel i j
this : IsIso (homologyMap φ.τ₁ j)
⊢ Mono (homologyMap φ.τ₁ j)

Tactic:
infer_instance

Result:
no goals

Proof state:
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₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
⊢ IsIso (homologyMap φ.τ₃ i)

Tactic:
have := mono_homologyMap_τ₃ φ hS₁ hS₂ i h₁ (IsIso.mono_of_iso _) (fun j hij => by
  have := h₃ j hij
  infer_instance)

Result:
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₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
this : Mono (homologyMap φ.τ₃ i)
⊢ IsIso (homologyMap φ.τ₃ i)

Proof state:
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₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
this✝ : Mono (homologyMap φ.τ₃ i)
j : ι
hij : c.Rel i j
this : IsIso (homologyMap φ.τ₁ j)
⊢ Epi (homologyMap φ.τ₁ j)

Tactic:
infer_instance

Result:
no goals

Proof state:
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₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
this : Mono (homologyMap φ.τ₃ i)
⊢ IsIso (homologyMap φ.τ₃ i)

Tactic:
have := epi_homologyMap_τ₃ φ hS₁ hS₂ i inferInstance (fun j hij => by
  have := h₃ j hij
  infer_instance) h₄

Result:
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₂ : IsIso (homologyMap φ.τ₂ i)
h₃ : ∀ (j : ι), c.Rel i j → IsIso (homologyMap φ.τ₁ j)
h₄ : ∀ (j : ι), c.Rel i j → Mono (homologyMap φ.τ₂ j)
this✝ : Mono (homologyMap φ.τ₃ i)
this : Epi (homologyMap φ.τ₃ i)
⊢ IsIso (homologyMap φ.τ₃ i)