-- Mathlib/Algebra/Homology/ShortComplex/Retract.lean
lemma quasiIso_of_retract (h : RetractArrow f₁ f₂) [hf₂ : QuasiIso f₂] :
    QuasiIso f₁

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
⊢ Arrow.homMk
        (homologyMap
          (let_fun this := h.i.left;
          this))
        (homologyMap
          (let_fun this := h.i.right;
          this))
        ⋯ ≫
      Arrow.homMk
        (homologyMap
          (let_fun this := h.r.left;
          this))
        (homologyMap
          (let_fun this := h.r.right;
          this))
        ⋯ =
    𝟙 (Arrow.mk (homologyMap f₁))

Tactic:
ext <;> simp [← homologyMap_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
⊢ homologyMap
        (let_fun this := h.i.left;
        this) ≫
      (Arrow.mk (homologyMap f₂)).hom =
    (Arrow.mk (homologyMap f₁)).hom ≫
      homologyMap
        (let_fun this := h.i.right;
        this)

Tactic:
simp [← homologyMap_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
⊢ homologyMap
        (let_fun this := h.r.left;
        this) ≫
      (Arrow.mk (homologyMap f₁)).hom =
    (Arrow.mk (homologyMap f₂)).hom ≫
      homologyMap
        (let_fun this := h.r.right;
        this)

Tactic:
simp [← homologyMap_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
⊢ IsIso (homologyMap f₁)

Tactic:
have h : RetractArrow (homologyMap f₁) (homologyMap f₂) :=
  { i := Arrow.homMk (u := homologyMap (show S₁ ⟶ S₂ from h.i.left))
      (v := homologyMap (show T₁ ⟶ T₂ from h.i.right)) (by simp [← homologyMap_comp])
    r := Arrow.homMk (u := homologyMap (show S₂ ⟶ S₁ from h.r.left))
      (v := homologyMap (show T₂ ⟶ T₁ from h.r.right)) (by simp [← homologyMap_comp])
    retract := by ext <;> simp [← homologyMap_comp] }

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h✝ : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
h : RetractArrow (homologyMap f₁) (homologyMap f₂)
⊢ IsIso (homologyMap f₁)

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h✝ : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
h : RetractArrow (homologyMap f₁) (homologyMap f₂)
⊢ IsIso (homologyMap f₁)

Tactic:
exact (MorphismProperty.isomorphisms C).of_retract h hf₂

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : QuasiIso f₂
⊢ QuasiIso f₁

Tactic:
rw [quasiIso_iff] at hf₂ ⊢

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : HasZeroMorphisms C
S₁ T₁ S₂ T₂ : ShortComplex C
inst✝³ : S₁.HasHomology
inst✝² : T₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : T₂.HasHomology
f₁ : S₁ ⟶ T₁
f₂ : S₂ ⟶ T₂
h : RetractArrow f₁ f₂
hf₂ : IsIso (homologyMap f₂)
⊢ IsIso (homologyMap f₁)