-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma epi_τ₂_of_exact_of_epi {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂)
    (h₂ : S₂.Exact) [Epi S₁.g] [Epi S₂.g] [Epi φ.τ₁] [Epi φ.τ₃] : Epi φ.τ₂

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝¹ : Mono S₁.op.f
this✝ : Mono S₂.op.f
this : Mono (opMap φ).τ₁
⊢ Mono (opMap φ).τ₃

Tactic:
dsimp

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝¹ : Mono S₁.op.f
this✝ : Mono S₂.op.f
this : Mono (opMap φ).τ₁
⊢ Mono φ.τ₁.op

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
⊢ Mono S₁.op.f

Tactic:
dsimp

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
⊢ Mono S₁.g.op

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝² : Mono S₁.op.f
this✝¹ : Mono S₂.op.f
this✝ : Mono (opMap φ).τ₁
this : Mono (opMap φ).τ₃
⊢ Epi φ.τ₂

Tactic:
have := mono_τ₂_of_exact_of_mono (opMap φ) h₂.op

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝³ : Mono S₁.op.f
this✝² : Mono S₂.op.f
this✝¹ : Mono (opMap φ).τ₁
this✝ : Mono (opMap φ).τ₃
this : Mono (opMap φ).τ₂
⊢ Epi φ.τ₂

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this : Mono S₁.op.f
⊢ Epi φ.τ₂

Tactic:
have : Mono S₂.op.f := by dsimp; infer_instance

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝ : Mono S₁.op.f
this : Mono S₂.op.f
⊢ Epi φ.τ₂

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝¹ : Mono S₁.op.f
this✝ : Mono S₂.op.f
this : Mono (opMap φ).τ₁
⊢ Epi φ.τ₂

Tactic:
have : Mono (opMap φ).τ₃ := by dsimp; infer_instance

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝² : Mono S₁.op.f
this✝¹ : Mono S₂.op.f
this✝ : Mono (opMap φ).τ₁
this : Mono (opMap φ).τ₃
⊢ Epi φ.τ₂

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
⊢ Epi φ.τ₂

Tactic:
have : Mono S₁.op.f := by dsimp; infer_instance

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this : Mono S₁.op.f
⊢ Epi φ.τ₂

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this : Mono S₁.op.f
⊢ Mono S₂.op.f

Tactic:
dsimp

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this : Mono S₁.op.f
⊢ Mono S₂.g.op

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝ : Mono S₁.op.f
this : Mono S₂.op.f
⊢ Mono (opMap φ).τ₁

Tactic:
dsimp

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝ : Mono S₁.op.f
this : Mono S₂.op.f
⊢ Mono φ.τ₃.op

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝ : Mono S₁.op.f
this : Mono S₂.op.f
⊢ Mono φ.τ₃.op

Tactic:
infer_instance

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
⊢ Mono S₁.g.op

Tactic:
infer_instance

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝¹ : Mono S₁.op.f
this✝ : Mono S₂.op.f
this : Mono (opMap φ).τ₁
⊢ Mono φ.τ₁.op

Tactic:
infer_instance

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝ : Mono S₁.op.f
this : Mono S₂.op.f
⊢ Epi φ.τ₂

Tactic:
have : Mono (opMap φ).τ₁ := by dsimp; infer_instance

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝¹ : Mono S₁.op.f
this✝ : Mono S₂.op.f
this : Mono (opMap φ).τ₁
⊢ Epi φ.τ₂

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this : Mono S₁.op.f
⊢ Mono S₂.g.op

Tactic:
infer_instance

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₂.Exact
inst✝³ : Epi S₁.g
inst✝² : Epi S₂.g
inst✝¹ : Epi φ.τ₁
inst✝ : Epi φ.τ₃
this✝³ : Mono S₁.op.f
this✝² : Mono S₂.op.f
this✝¹ : Mono (opMap φ).τ₁
this✝ : Mono (opMap φ).τ₃
this : Mono (opMap φ).τ₂
⊢ Epi φ.τ₂

Tactic:
exact unop_epi_of_mono (opMap φ).τ₂

Result:
no goals