-- Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
lemma quasiIso_opMap_iff (φ : S₁ ⟶ S₂) :
    QuasiIso (opMap φ) ↔ QuasiIso φ

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ QuasiIso (opMap φ) ↔ QuasiIso φ

Tactic:
rw [γ.left.quasiIso_iff, γ.op.right.quasiIso_iff]

Result:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ IsIso γ.op.right.φH ↔ IsIso γ.left.φH

Proof state:
case mp
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ IsIso γ.left.φH.op → IsIso γ.left.φH

Tactic:
intro h

Result:
case mp
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
h : IsIso γ.left.φH.op
⊢ IsIso γ.left.φH

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ IsIso γ.op.right.φH ↔ IsIso γ.left.φH

Tactic:
dsimp

Result:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ IsIso γ.left.φH.op ↔ IsIso γ.left.φH

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ IsIso γ.left.φH.op ↔ IsIso γ.left.φH

Tactic:
constructor

Result:
case mp
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ IsIso γ.left.φH.op → IsIso γ.left.φH

case mpr
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ IsIso γ.left.φH → IsIso γ.left.φH.op

Proof state:
case mpr
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ IsIso γ.left.φH → IsIso γ.left.φH.op

Tactic:
intro h

Result:
case mpr
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
h : IsIso γ.left.φH
⊢ IsIso γ.left.φH.op

Proof state:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
⊢ QuasiIso (opMap φ) ↔ QuasiIso φ

Tactic:
have γ : HomologyMapData φ S₁.homologyData S₂.homologyData := default

Result:
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
⊢ QuasiIso (opMap φ) ↔ QuasiIso φ

Proof state:
case mpr
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
h : IsIso γ.left.φH
⊢ IsIso γ.left.φH.op

Tactic:
infer_instance

Result:
no goals

Proof state:
case mp
C : Type u_2
inst✝³ : Category.{u_1, u_2} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
φ : S₁ ⟶ S₂
γ : HomologyMapData φ S₁.homologyData S₂.homologyData
h : IsIso γ.left.φH.op
⊢ IsIso γ.left.φH

Tactic:
apply isIso_of_op

Result:
no goals