awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Epi (X := (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₁) (Y := (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₁)
    (ShortComplex.Hom.τ₁ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₁ ⟶ (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₁)

Tactic:
(X.exact₂ f₃ f₄ f₃₄ h₃₄ _).epi_f h

Premises used: CategoryTheory.ComposableArrows.Mk₁.obj, CategoryTheory.Abelian.SpectralObject.exact₂, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ShortComplex.Exact.epi_f, CategoryTheory.ComposableArrows.twoδ₂Toδ₁
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Epi (X := (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₁) (Y := (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₁)
    (ShortComplex.Hom.τ₁ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₁ ⟶ (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₁)

Tactic:
exact (X.exact₂ f₃ f₄ f₃₄ h₃₄ _).epi_f h

Premises used: CategoryTheory.Abelian.SpectralObject.exact₂, CategoryTheory.ShortComplex.Exact.epi_f
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
h₂ :
  IsIso (X := (X.H n₂).obj (mk₁ f₂)) (Y := (X.H n₂).obj (mk₁ f₂))
    ((X.H n₂).map (homMk₁ (𝟙 i₁) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i₀ 2)) ⋯))
⊢ IsIso (X := (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₂) (Y := (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₂)
    (ShortComplex.Hom.τ₂ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₂ ⟶ (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₂)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ IsIso ((X.H n₂).map (𝟙 (mk₁ f₂)))

Tactic:
(inferInstance : IsIso ((X.H n₂).map (𝟙 _)))

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
h₁ : homMk₁ (𝟙 i₁) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i₀ 2)) ⋯ = 𝟙 (mk₁ f₂)
⊢ IsIso (X := (X.H n₂).obj (mk₁ f₂)) (Y := (X.H n₂).obj (mk₁ f₂))
    ((X.H n₂).map (homMk₁ (𝟙 i₁) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i₀ 2)) ⋯))

Tactic:
convert! (inferInstance : IsIso ((X.H n₂).map (𝟙 _)))

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
h₃ : Mono (X := (X.H n₃).obj (mk₁ f₁)) (Y := (X.H n₃).obj (mk₁ f₁)) ((X.H n₃).map (homMk₁ (𝟙 i₀) (𝟙 i₁) ⋯))
⊢ Mono (X := (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₃) (Y := (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₃)
    (ShortComplex.Hom.τ₃ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯) :
      (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ ⋯ ⋯).X₃ ⟶ (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ ⋯ ⋯).X₃)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Mono ((X.H n₃).map (𝟙 (mk₁ f₁)))

Tactic:
(inferInstance : Mono ((X.H n₃).map (𝟙 (mk₁ f₁))))

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
h₁ : homMk₁ (𝟙 i₀) (𝟙 i₁) ⋯ = 𝟙 (mk₁ f₁)
⊢ Mono (X := (X.H n₃).obj (mk₁ f₁)) (Y := (X.H n₃).obj (mk₁ f₁)) ((X.H n₃).map (homMk₁ (𝟙 i₀) (𝟙 i₁) ⋯))

Tactic:
convert! (inferInstance : Mono ((X.H n₃).map (𝟙 (mk₁ f₁))))

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : IsZero.{v_1, u_1} ((X.H n₁).obj (mk₁ f₄))
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ IsIso (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)

Tactic:
X.isIso_map_fourδ₄Toδ₃ _ _ _ _ _ _ _ _ _ (h.eq_of_tgt _ _)

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt, CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₄Toδ₃
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ i₃ i₄ i₅ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂ ≫
      X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ =
    0

Tactic:
simp [← cancel_mono (X.ιE f₁ f₂ f₃ n₁ n₂ n₃ hn₂ hn₃),
    ← cancel_mono (X.fromOpcycles f₂ f₃ f₂₃ h₂₃ n₂),
    X.d_ιE_fromOpcycles f₁ f₂ f₃ f₄ f₅ f₂₃ h₂₃ _ rfl _ rfl n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃, X.map_ιE_assoc
    f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) (𝟙 _) n₀ n₁ n₂ (by cat_disch) hn₁ hn₂]

Premises used: CategoryTheory.Abelian.SpectralObject.d_ιE_fromOpcycles, CategoryTheory.ComposableArrows.fourδ₁Toδ₀, CategoryTheory.CategoryStruct.id, CategoryTheory.Abelian.SpectralObject.map_ιE_assoc, CategoryTheory.Abelian.SpectralObject.fromOpcycles, CategoryTheory.cancel_mono, CategoryTheory.Abelian.SpectralObject.ιE, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
ι' : Type u_3
κ : Type u_4
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
inst_3 : Preorder ι'
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
X' : SpectralObject.{u_1, u_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ i₅ i₆ i₇ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)

Tactic:
X.mono_map _ _ _ _ _ _ _ _ _ rfl rfl rfl _ _ rfl

Premises used: CategoryTheory.Abelian.SpectralObject.mono_map, rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h₁ :
  Epi (X := (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₁) (Y := (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₁)
    (ShortComplex.Hom.τ₁ (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₁ ⟶ (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₁)
h₂ :
  IsIso (X := (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₂) (Y := (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₂)
    (ShortComplex.Hom.τ₂ (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₂ ⟶ (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₂)
h₃ :
  Mono (X := (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₃) (Y := (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₃)
    (ShortComplex.Hom.τ₃ (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₃ ⟶ (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₃)
⊢ IsIso (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)

Tactic:
apply ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'

Premises used: CategoryTheory.ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h₁ :
  Epi (X := (X.H n₀).obj (mk₁ f₅)) (Y := (X.H n₀).obj (mk₁ f₅))
    ((X.H n₀).map (homMk₁ (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 2)) (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 3)) ⋯))
⊢ Epi (X := (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₁) (Y := (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₁)
    (ShortComplex.Hom.τ₁ (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₁ ⟶ (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₁)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Epi ((X.H n₀).map (𝟙 (mk₁ f₅)))

Tactic:
(inferInstance : Epi ((X.H n₀).map (𝟙 _)))

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h₁ : homMk₁ (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 2)) (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 3)) ⋯ = 𝟙 (mk₁ f₅)
⊢ Epi (X := (X.H n₀).obj (mk₁ f₅)) (Y := (X.H n₀).obj (mk₁ f₅))
    ((X.H n₀).map (homMk₁ (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 2)) (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 3)) ⋯))

Tactic:
convert! (inferInstance : Epi ((X.H n₀).map (𝟙 _)))

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h₂ :
  IsIso (X := (X.H n₁).obj (mk₁ f₄)) (Y := (X.H n₁).obj (mk₁ f₄))
    ((X.H n₁).map (homMk₁ (𝟙 i₃) (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 2)) ⋯))
⊢ IsIso (X := (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₂) (Y := (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₂)
    (ShortComplex.Hom.τ₂ (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₂ ⟶ (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₂)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso ((X.H n₁).map (𝟙 (mk₁ f₄)))

Tactic:
(inferInstance : IsIso ((X.H n₁).map (𝟙 _)))

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
h₁ : homMk₁ (𝟙 i₃) (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 2)) ⋯ = 𝟙 (mk₁ f₄)
⊢ IsIso (X := (X.H n₁).obj (mk₁ f₄)) (Y := (X.H n₁).obj (mk₁ f₄))
    ((X.H n₁).map (homMk₁ (𝟙 i₃) (𝟙 (Precomp.obj (mk₂ f₄ f₅) i₁ 2)) ⋯))

Tactic:
convert! (inferInstance : IsIso ((X.H n₁).map (𝟙 _)))

Premises used: inferInstance
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono (X := (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₃) (Y := (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₃)
    (ShortComplex.Hom.τ₃ (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₃ ⟶ (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₃)

Tactic:
(X.exact₂ f₂ f₃ f₂₃ h₂₃ n₂).mono_g h

Premises used: CategoryTheory.Abelian.SpectralObject.exact₂, CategoryTheory.ShortComplex.Exact.mono_g, CategoryTheory.ComposableArrows.Precomp.obj, CategoryTheory.ComposableArrows.twoδ₁Toδ₀
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : (X.H n₂).map (twoδ₂Toδ₁ f₂ f₃ f₂₃ h₂₃) = 0
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Mono (X := (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₃) (Y := (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₃)
    (ShortComplex.Hom.τ₃ (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ ⋯ ⋯) :
      (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₃ ⟶ (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ ⋯ ⋯).X₃)

Tactic:
exact (X.exact₂ f₂ f₃ f₂₃ h₂₃ n₂).mono_g h

Premises used: CategoryTheory.Abelian.SpectralObject.exact₂, CategoryTheory.ShortComplex.Exact.mono_g
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Category.{v_2, u_2} ι
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₁ i₂ i₃ i₄ i₅ : ι
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₅ : i₄ ⟶ i₅
f₂₃ : i₁ ⟶ i₃
h₂₃ : f₂ ≫ f₃ = f₂₃
n₀ n₁ n₂ : ℤ
h : IsZero.{v_1, u_1} ((X.H n₂).obj (mk₁ f₂))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)

Tactic:
X.isIso_map_fourδ₁Toδ₀ _ _ _ _ _ _ _ _ _ (h.eq_of_src _ _)

Premises used: CategoryTheory.Limits.IsZero.eq_of_src, CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι' : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι'
X' : SpectralObject.{u_1, u_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ i₅ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
hi₄₅ : i₄ ≤ i₅
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X'.mapFourδ₁Toδ₀' i₀ i₁ i₃ i₄ i₅ hi₀₁ ⋯ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂ ≫
      X'.mapFourδ₁Toδ₀' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂ =
    X'.mapFourδ₁Toδ₀' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂

Tactic:
(X'.map_comp (hn₁ := hn₁) (hn₂ := hn₂) ..).symm

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.ComposableArrows.fourδ₁Toδ₀, CategoryTheory.Abelian.SpectralObject.map_comp, CategoryTheory.ComposableArrows.homMk₃, CategoryTheory.ComposableArrows.homMkSucc, CategoryTheory.ComposableArrows.homMk, Eq.symm
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι' : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι'
X' : SpectralObject.{u_1, u_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ i₅ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
hi₄₅ : i₄ ≤ i₅
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂ ≫
      X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₄ i₅ hi₀₁ hi₁₂ ⋯ hi₄₅ n₀ n₁ n₂ hn₁ hn₂ =
    X'.mapFourδ₄Toδ₃' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯ n₀ n₁ n₂ hn₁ hn₂

Tactic:
(X'.map_comp (hn₁ := hn₁) (hn₂ := hn₂) ..).symm

Premises used: CategoryTheory.ComposableArrows.fourδ₄Toδ₃, CategoryTheory.NatTrans.vcomp, CategoryTheory.Abelian.SpectralObject.map_comp, CategoryTheory.ComposableArrows.homMk₃, CategoryTheory.ComposableArrows.homMkSucc, CategoryTheory.ComposableArrows.homMk, Eq.symm
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι' : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι'
X' : SpectralObject.{u_1, u_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ i₅ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
hi₄₅ : i₄ ≤ i₅
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
rw :
  Eq (α :=
    X'.E (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂ ⟶
      X'.E (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂)
    (X'.map (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE ⋯)
      (fourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ ≫ fourδ₄Toδ₃' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅) n₀ n₁ n₂ ⋯ ⋯)
    (X'.map (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE ⋯)
      (fourδ₄Toδ₃' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ ≫ fourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯) n₀ n₁ n₂ ⋯ ⋯)
⊢ X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂ ≫
      X'.mapFourδ₄Toδ₃' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂ =
    X'.mapFourδ₄Toδ₃' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂ ≫
      X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯ n₀ n₁ n₂ hn₁ hn₂

Tactic:
rw [← map_comp .., ← map_comp ..]

Premises used: CategoryTheory.Abelian.SpectralObject.map_comp
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι' : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι'
X' : SpectralObject.{u_1, u_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ i₅ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
hi₄₅ : i₄ ≤ i₅
n₀ n₁ n₂ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ Eq (α :=
    X'.E (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂ ⟶
      X'.E (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂)
    (X'.map (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE ⋯)
      (fourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ ≫ fourδ₄Toδ₃' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅) n₀ n₁ n₂ ⋯ ⋯)
    (X'.map (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE ⋯)
      (fourδ₄Toδ₃' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ ≫ fourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₅ hi₀₁ hi₁₂ hi₂₃ ⋯) n₀ n₁ n₂ ⋯ ⋯)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι' : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι'
X' : SpectralObject.{u_1, u_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
n₀ n₁ n₂ : ℤ
h : IsZero.{v_1, u_1} ((X'.H n₂).obj (mk₁ (homOfLE hi₀₁)))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ IsIso (X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂)

Tactic:
X'.isIso_map_fourδ₁Toδ₀_of_isZero _ _ _ _ _ _ _ _ _ h

Premises used: CategoryTheory.Abelian.SpectralObject.isIso_map_fourδ₁Toδ₀_of_isZero
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι' : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι'
X' : SpectralObject.{u_1, u_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
n₀ n₁ n₂ : ℤ
h : IsZero.{v_1, u_1} ((X'.H n₂).obj (mk₁ (homOfLE hi₀₁)))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂ ≫
      (X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv =
    𝟙 (X'.E (homOfLE ⋯) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂)

Tactic:
(X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).hom_inv_id

Premises used: CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.Iso.hom_inv_id, CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.LeftHomologyData.descH, CategoryTheory.Abelian.SpectralObject.map, CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀', CategoryTheory.ShortComplex.homologyMap
-- Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono
Goal:
C : Type u_1
ι' : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
inst_2 : Preorder ι'
X' : SpectralObject.{u_1, u_3, v_1, u_3} C ι'
i₀ i₁ i₂ i₃ i₄ : ι'
hi₀₁ : i₀ ≤ i₁
hi₁₂ : i₁ ≤ i₂
hi₂₃ : i₂ ≤ i₃
hi₃₄ : i₃ ≤ i₄
n₀ n₁ n₂ : ℤ
h : IsZero.{v_1, u_1} ((X'.H n₂).obj (mk₁ (homOfLE hi₀₁)))
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
⊢ (X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv ≫
      X'.mapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ hn₁ hn₂ =
    𝟙 (X'.E (homOfLE hi₁₂) (homOfLE hi₂₃) (homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂)

Tactic:
(X'.isoMapFourδ₁Toδ₀' i₀ i₁ i₂ i₃ i₄ hi₀₁ hi₁₂ hi₂₃ hi₃₄ n₀ n₁ n₂ h hn₁ hn₂).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.leftHomologyMap', CategoryTheory.ShortComplex.homologyMap', CategoryTheory.ShortComplex.LeftHomologyData.descH, CategoryTheory.Abelian.SpectralObject.map, CategoryTheory.Abelian.SpectralObject.isoMapFourδ₁Toδ₀', CategoryTheory.ShortComplex.homologyMap