-- Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean
/-- `K.restrictionToTruncGE' e` is a quasi-isomorphism in degrees that are not at the boundary. -/
lemma quasiIsoAt_restrictionToTruncGE' (hj : ¬ e.BoundaryGE j)
    [(K.restriction e).HasHomology j] [(K.truncGE' e).HasHomology j] :
    QuasiIsoAt (K.restrictionToTruncGE' e) j

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
φ : (shortComplexFunctor C c j).obj (K.restriction e) ⟶ (shortComplexFunctor C c j).obj (K.truncGE' e) :=
  (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
⊢ Epi φ.τ₁

Tactic:
dsimp [φ]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
φ : (shortComplexFunctor C c j).obj (K.restriction e) ⟶ (shortComplexFunctor C c j).obj (K.truncGE' e) :=
  (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
⊢ Epi ((K.restrictionToTruncGE' e).f (c.prev j))

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
φ : (shortComplexFunctor C c j).obj (K.restriction e) ⟶ (shortComplexFunctor C c j).obj (K.truncGE' e) :=
  (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
⊢ Epi ((K.restrictionToTruncGE' e).f (c.prev j))

Tactic:
infer_instance

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
φ : (shortComplexFunctor C c j).obj (K.restriction e) ⟶ (shortComplexFunctor C c j).obj (K.truncGE' e) :=
  (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
this✝ : Epi φ.τ₁
this : IsIso φ.τ₂
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map (K.restrictionToTruncGE' e))

Tactic:
have : IsIso φ.τ₃ := K.isIso_restrictionToTruncGE' e _ (e.not_boundaryGE_next' hj rfl)

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
φ : (shortComplexFunctor C c j).obj (K.restriction e) ⟶ (shortComplexFunctor C c j).obj (K.truncGE' e) :=
  (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
this✝¹ : Epi φ.τ₁
this✝ : IsIso φ.τ₂
this : IsIso φ.τ₃
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map (K.restrictionToTruncGE' e))

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map (K.restrictionToTruncGE' e))

Tactic:
let φ := (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
φ : (shortComplexFunctor C c j).obj (K.restriction e) ⟶ (shortComplexFunctor C c j).obj (K.truncGE' e) :=
  (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map (K.restrictionToTruncGE' e))

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
φ : (shortComplexFunctor C c j).obj (K.restriction e) ⟶ (shortComplexFunctor C c j).obj (K.truncGE' e) :=
  (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
this✝¹ : Epi φ.τ₁
this✝ : IsIso φ.τ₂
this : IsIso φ.τ₃
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map (K.restrictionToTruncGE' e))

Tactic:
exact ShortComplex.quasiIso_of_epi_of_isIso_of_mono φ

Result:
no goals

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
⊢ QuasiIsoAt (K.restrictionToTruncGE' e) j

Tactic:
rw [quasiIsoAt_iff]

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map (K.restrictionToTruncGE' e))

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
φ : (shortComplexFunctor C c j).obj (K.restriction e) ⟶ (shortComplexFunctor C c j).obj (K.truncGE' e) :=
  (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
this : Epi φ.τ₁
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map (K.restrictionToTruncGE' e))

Tactic:
have : IsIso φ.τ₂ := K.isIso_restrictionToTruncGE' e j hj

Result:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁵ : Category.{u_4, u_3} C
inst✝⁴ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
j : ι
hj : ¬e.BoundaryGE j
inst✝¹ : (K.restriction e).HasHomology j
inst✝ : (K.truncGE' e).HasHomology j
φ : (shortComplexFunctor C c j).obj (K.restriction e) ⟶ (shortComplexFunctor C c j).obj (K.truncGE' e) :=
  (shortComplexFunctor C c j).map (K.restrictionToTruncGE' e)
this✝ : Epi φ.τ₁
this : IsIso φ.τ₂
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c j).map (K.restrictionToTruncGE' e))