-- Mathlib/Algebra/Homology/Embedding/TruncGEHomology.lean
lemma hasHomology_sc'_of_not_mem_boundary (hj : ¬ e.BoundaryGE j) :
    ((K.truncGE' e).sc' i j k).HasHomology

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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝ : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
⊢ ((K.truncGE' e).sc' i j k).HasHomology

Tactic:
have : Epi φ.τ₁ := by dsimp [φ]; infer_instance

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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝¹ : (K.restriction e).HasHomology j
this✝ : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
this : Epi φ.τ₁
⊢ ((K.truncGE' e).sc' i j k).HasHomology

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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝² : (K.restriction e).HasHomology j
this✝¹ : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
this✝ : Epi φ.τ₁
this : IsIso φ.τ₂
⊢ ((K.truncGE' e).sc' i j k).HasHomology

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

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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝³ : (K.restriction e).HasHomology j
this✝² : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
this✝¹ : Epi φ.τ₁
this✝ : IsIso φ.τ₂
this : IsIso φ.τ₃
⊢ ((K.truncGE' e).sc' i j k).HasHomology

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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝ : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
⊢ ((K.truncGE' e).sc' i j k).HasHomology

Tactic:
let φ := (shortComplexFunctor' C c i j k).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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝ : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
⊢ ((K.truncGE' e).sc' i j k).HasHomology

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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝ : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
⊢ Epi ((K.restrictionToTruncGE' e).f i)

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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
⊢ ((K.truncGE' e).sc' i j k).HasHomology

Tactic:
have : (K.restriction e).HasHomology j :=
  restriction.hasHomology K e i j k hi hk rfl rfl rfl
    (e.prev_f_of_not_boundaryGE hi hj) (e.next_f hk)

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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this : (K.restriction e).HasHomology j
⊢ ((K.truncGE' e).sc' i j k).HasHomology

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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝³ : (K.restriction e).HasHomology j
this✝² : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
this✝¹ : Epi φ.τ₁
this✝ : IsIso φ.τ₂
this : IsIso φ.τ₃
⊢ ((K.truncGE' e).sc' i j k).HasHomology

Tactic:
exact ShortComplex.hasHomology_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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this : (K.restriction e).HasHomology j
⊢ ((K.truncGE' e).sc' i j k).HasHomology

Tactic:
have := ShortComplex.hasHomology_of_iso ((K.restriction e).isoSc' i j k hi hk)

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'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝ : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
⊢ ((K.truncGE' e).sc' i j k).HasHomology