-- Mathlib/Algebra/Homology/ShortComplex/QuasiIso.lean
lemma quasiIso_of_arrow_mk_iso (φ : S₁ ⟶ S₂) (φ' : S₃ ⟶ S₄) (e : Arrow.mk φ ≅ Arrow.mk φ')
    [hφ : QuasiIso φ] : QuasiIso φ'

Proof state:
C : Type u_2
inst✝⁵ : Category.{u_1, u_2} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := e.inv.left
β : S₂ ⟶ S₄ := e.hom.right
this : φ' = α ≫ φ ≫ β
⊢ QuasiIso φ'

Tactic:
rw [this]

Result:
C : Type u_2
inst✝⁵ : Category.{u_1, u_2} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := e.inv.left
β : S₂ ⟶ S₄ := e.hom.right
this : φ' = α ≫ φ ≫ β
⊢ QuasiIso (α ≫ φ ≫ β)

Proof state:
C : Type u_2
inst✝⁵ : Category.{u_1, u_2} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := e.inv.left
⊢ QuasiIso φ'

Tactic:
let β : S₂ ⟶ S₄ := e.hom.right

Result:
C : Type u_2
inst✝⁵ : Category.{u_1, u_2} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := e.inv.left
β : S₂ ⟶ S₄ := e.hom.right
⊢ QuasiIso φ'

Proof state:
C : Type u_2
inst✝⁵ : Category.{u_1, u_2} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := e.inv.left
β : S₂ ⟶ S₄ := e.hom.right
this : φ' = α ≫ φ ≫ β
⊢ QuasiIso (α ≫ φ ≫ β)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_2
inst✝⁵ : Category.{u_1, u_2} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
⊢ QuasiIso φ'

Tactic:
let α : S₃ ⟶ S₁ := e.inv.left

Result:
C : Type u_2
inst✝⁵ : Category.{u_1, u_2} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := e.inv.left
⊢ QuasiIso φ'

Proof state:
C : Type u_2
inst✝⁵ : Category.{u_1, u_2} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := e.inv.left
β : S₂ ⟶ S₄ := e.hom.right
⊢ QuasiIso φ'

Tactic:
suffices φ' = α ≫ φ ≫ β by
  rw [this]
  infer_instance

Result:
C : Type u_2
inst✝⁵ : Category.{u_1, u_2} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := e.inv.left
β : S₂ ⟶ S₄ := e.hom.right
⊢ φ' = α ≫ φ ≫ β

Proof state:
C : Type u_2
inst✝⁵ : Category.{u_1, u_2} C
inst✝⁴ : HasZeroMorphisms C
S₁ S₂ S₃ S₄ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : S₂.HasHomology
inst✝¹ : S₃.HasHomology
inst✝ : S₄.HasHomology
φ : S₁ ⟶ S₂
φ' : S₃ ⟶ S₄
e : Arrow.mk φ ≅ Arrow.mk φ'
hφ : QuasiIso φ
α : S₃ ⟶ S₁ := e.inv.left
β : S₂ ⟶ S₄ := e.hom.right
⊢ φ' = α ≫ φ ≫ β

Tactic:
simp only [α, β, Arrow.w_mk_right_assoc, Arrow.mk_left, Arrow.mk_right, Arrow.mk_hom,
  ← Arrow.comp_right, e.inv_hom_id, Arrow.id_right, comp_id]

Result:
no goals