-- Mathlib/Algebra/Homology/ShortComplex/ShortExact.lean
lemma isIso₂_of_shortExact_of_isIso₁₃ [Balanced C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂)
    (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact) [IsIso φ.τ₁] [IsIso φ.τ₃] : IsIso φ.τ₂

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝² : Mono S₁.f
this✝¹ : Mono S₂.f
this✝ : Epi S₁.g
this : Epi S₂.g
⊢ IsIso φ.τ₂

Tactic:
have := mono_τ₂_of_exact_of_mono φ h₁.exact

Result:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝³ : Mono S₁.f
this✝² : Mono S₂.f
this✝¹ : Epi S₁.g
this✝ : Epi S₂.g
this : Mono φ.τ₂
⊢ IsIso φ.τ₂

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝⁴ : Mono S₁.f
this✝³ : Mono S₂.f
this✝² : Epi S₁.g
this✝¹ : Epi S₂.g
this✝ : Mono φ.τ₂
this : Epi φ.τ₂
⊢ IsIso φ.τ₂

Tactic:
apply isIso_of_mono_of_epi

Result:
no goals

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝¹ : Mono S₁.f
this✝ : Mono S₂.f
this : Epi S₁.g
⊢ IsIso φ.τ₂

Tactic:
have := h₂.epi_g

Result:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝² : Mono S₁.f
this✝¹ : Mono S₂.f
this✝ : Epi S₁.g
this : Epi S₂.g
⊢ IsIso φ.τ₂

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝ : Mono S₁.f
this : Mono S₂.f
⊢ IsIso φ.τ₂

Tactic:
have := h₁.epi_g

Result:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝¹ : Mono S₁.f
this✝ : Mono S₂.f
this : Epi S₁.g
⊢ IsIso φ.τ₂

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
⊢ IsIso φ.τ₂

Tactic:
have := h₁.mono_f

Result:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this : Mono S₁.f
⊢ IsIso φ.τ₂

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝³ : Mono S₁.f
this✝² : Mono S₂.f
this✝¹ : Epi S₁.g
this✝ : Epi S₂.g
this : Mono φ.τ₂
⊢ IsIso φ.τ₂

Tactic:
have := epi_τ₂_of_exact_of_epi φ h₂.exact

Result:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝⁴ : Mono S₁.f
this✝³ : Mono S₂.f
this✝² : Epi S₁.g
this✝¹ : Epi S₂.g
this✝ : Mono φ.τ₂
this : Epi φ.τ₂
⊢ IsIso φ.τ₂

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this : Mono S₁.f
⊢ IsIso φ.τ₂

Tactic:
have := h₂.mono_f

Result:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this✝ : Mono S₁.f
this : Mono S₂.f
⊢ IsIso φ.τ₂