awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
      X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₁ :
  X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
        X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₂ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫
      X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ X.πE (𝟙 i₀) f₁ (𝟙 i₁) n₁ n₂ n₃ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₃ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫ X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ (X.cyclesIsoH f₁ n₂ n₃ ⋯).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
⊢ X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
have rw₄ : X.δ f₁ f₂ n₁ n₂ hn₂ ≫ X.toCycles (𝟙 i₀) f₁ f₁ sorry n₂ ≫ (X.cyclesIsoH f₁ n₂ n₃ sorry).hom =
  X.toCycles (𝟙 i₁) f₂ f₂ sorry n₁ ≫ (X.cyclesIsoH f₂ n₁ n₂ sorry).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
Tactic: rw [← cancel_epi (X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles (𝟙 i₁) f₂ f₂ (by simp) n₁),
    X.toCycles_πE_d_assoc (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) f₁ (by simp) _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_EIsoH_hom .., πE_EIsoH_hom_assoc .., cyclesIsoH_inv_hom_id ..,
    comp_id, cyclesIsoH_inv_hom_id_assoc ..]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
      X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₁ :
  X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
        X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₂ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫
      X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ X.πE (𝟙 i₀) f₁ (𝟙 i₁) n₁ n₂ n₃ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₃ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫ X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ (X.cyclesIsoH f₁ n₂ n₃ ⋯).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₄ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫ X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ (X.cyclesIsoH f₁ n₂ n₃ ⋯).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫ (X.cyclesIsoH f₂ n₁ n₂ ⋯).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
⊢ X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
have rw₅ : X.δ f₁ f₂ n₁ n₂ hn₂ ≫ 𝟙 ((X.H n₂).obj (mk₁ f₁)) =
  X.toCycles (𝟙 i₁) f₂ f₂ sorry n₁ ≫ (X.cyclesIsoH f₂ n₁ n₂ sorry).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
Tactic: rw [← cancel_epi (X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles (𝟙 i₁) f₂ f₂ (by simp) n₁),
    X.toCycles_πE_d_assoc (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) f₁ (by simp) _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_EIsoH_hom .., πE_EIsoH_hom_assoc .., cyclesIsoH_inv_hom_id ..,
    comp_id, cyclesIsoH_inv_hom_id_assoc ..]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
      X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₁ :
  X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
        X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₂ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫
      X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ X.πE (𝟙 i₀) f₁ (𝟙 i₁) n₁ n₂ n₃ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₃ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫ X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ (X.cyclesIsoH f₁ n₂ n₃ ⋯).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₄ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫ X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ (X.cyclesIsoH f₁ n₂ n₃ ⋯).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫ (X.cyclesIsoH f₂ n₁ n₂ ⋯).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₅ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫ 𝟙 ((X.H n₂).obj (mk₁ f₁)) =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫ (X.cyclesIsoH f₂ n₁ n₂ ⋯).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
⊢ X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
have rw₆ : X.δ f₁ f₂ n₁ n₂ hn₂ = X.toCycles (𝟙 i₁) f₂ f₂ sorry n₁ ≫ (X.cyclesIsoH f₂ n₁ n₂ sorry).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
Tactic: rw [← cancel_epi (X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles (𝟙 i₁) f₂ f₂ (by simp) n₁),
    X.toCycles_πE_d_assoc (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) f₁ (by simp) _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_EIsoH_hom .., πE_EIsoH_hom_assoc .., cyclesIsoH_inv_hom_id ..,
    comp_id, cyclesIsoH_inv_hom_id_assoc ..]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.Differentials (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} ι
inst_2 : Abelian.{v_1, u_1} C
X : SpectralObject.{u_1, u_2, v_1, v_2} C ι
i₀ i₁ i₂ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
n₀ n₁ n₂ n₃ : ℤ
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
rw :
  X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
      X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₁ :
  X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫
        X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₂ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫
      X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ X.πE (𝟙 i₀) f₁ (𝟙 i₁) n₁ n₂ n₃ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₃ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫ X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ (X.cyclesIsoH f₁ n₂ n₃ ⋯).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫
      X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂ ≫ (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₄ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫ X.toCycles (𝟙 i₀) f₁ f₁ ⋯ n₂ ≫ (X.cyclesIsoH f₁ n₂ n₃ ⋯).hom =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫ (X.cyclesIsoH f₂ n₁ n₂ ⋯).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₅ :
  X.δ f₁ f₂ n₁ n₂ hn₂ ≫ 𝟙 ((X.H n₂).obj (mk₁ f₁)) =
    X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫ (X.cyclesIsoH f₂ n₁ n₂ ⋯).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
rw₆ : X.δ f₁ f₂ n₁ n₂ hn₂ = X.toCycles (𝟙 i₁) f₂ f₂ ⋯ n₁ ≫ (X.cyclesIsoH f₂ n₁ n₂ ⋯).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
⊢ X.d (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃ ≫ (X.EIsoH f₁ n₁ n₂ n₃ hn₂ hn₃).hom =
    (X.EIsoH f₂ n₀ n₁ n₂ hn₁ hn₂).hom ≫ X.δ f₁ f₂ n₁ n₂ hn₂
have rw₇ : X.δ f₁ f₂ n₁ n₂ hn₂ = X.δ f₁ f₂ n₁ n₂ hn₂
Tactic: rw [← cancel_epi (X.πE (𝟙 i₁) f₂ (𝟙 i₂) n₀ n₁ n₂ hn₁ hn₂),
    ← cancel_epi (X.toCycles (𝟙 i₁) f₂ f₂ (by simp) n₁),
    X.toCycles_πE_d_assoc (𝟙 i₀) f₁ (𝟙 i₁) f₂ (𝟙 i₂) f₁ (by simp) _ _ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃,
    πE_EIsoH_hom .., πE_EIsoH_hom_assoc .., cyclesIsoH_inv_hom_id ..,
    comp_id, cyclesIsoH_inv_hom_id_assoc ..]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
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₃'
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁ f₂ f₃'
n₀ n₁ n₂ n₃ : ℤ
hα₀ : α.app 0 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 0)
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Epi (X.cyclesMap f₁ f₂ f₁ f₂ (𝟙 (mk₂ f₁ f₂)) n₁)
have rw : Epi.{v_1, u_1} (𝟙 (X.cycles f₁ f₂ n₁))
Tactic: rw [X.cyclesMap_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (hypothesis)
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₃
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂ f₃
n₀ n₁ n₂ n₃ : ℤ
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hα₃ : α.app 3 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 3)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Mono (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ hn₁ hn₂)
have this : Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry ⟶ X.opcycles f₂ f₃ n₁)
  (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ sorry sorry ≫ X.ιE f₁' f₂ f₃ n₀ n₁ n₂ sorry sorry)
  (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry ≫ X.opcyclesMap f₂ f₃ f₂ f₃ (𝟙 (mk₂ f₂ f₃)) n₁)
Tactic: have := X.map_ιE _ _ _ _ _ _ α (𝟙 _) n₀ n₁ n₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (hypothesis)
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₃
α : mk₃ f₁ f₂ f₃ ⟶ mk₃ f₁' f₂ f₃
n₀ n₁ n₂ n₃ : ℤ
hα₁ : α.app 1 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 1)
hα₂ : α.app 2 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 2)
hα₃ : α.app 3 = 𝟙 ((mk₃ f₁ f₂ f₃).obj 3)
hn₁ : n₀ + 1 = n₁
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
this :
  Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ⟶ X.opcycles f₂ f₃ n₁)
    (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ ⋯ ⋯ ≫ X.ιE f₁' f₂ f₃ n₀ n₁ n₂ ⋯ ⋯)
    (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ ⋯ ⋯ ≫ X.opcyclesMap f₂ f₃ f₂ f₃ (𝟙 (mk₂ f₂ f₃)) n₁)
⊢ Mono (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ hn₁ hn₂)
have this₁ : Eq (α := X.E f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry ⟶ X.opcycles f₂ f₃ n₁)
  (X.map f₁ f₂ f₃ f₁' f₂ f₃ α n₀ n₁ n₂ sorry sorry ≫ X.ιE f₁' f₂ f₃ n₀ n₁ n₂ sorry sorry) (X.ιE f₁ f₂ f₃ n₀ n₁ n₂ sorry sorry)
Tactic: rw [opcyclesMap_id, comp_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
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.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)
have h₁ : Epi (X := (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry).X₁) (Y := (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ sorry sorry).X₁)
  (ShortComplex.Hom.τ₁ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ sorry sorry) :
    (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry).X₁ ⟶ (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ sorry sorry).X₁)
Tactic: apply ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
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₁)
⊢ IsIso (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)
have h₂ : IsIso (X := (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry).X₂) (Y := (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ sorry sorry).X₂)
  (ShortComplex.Hom.τ₂ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ sorry sorry) :
    (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry).X₂ ⟶ (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ sorry sorry).X₂)
Tactic: apply ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
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₂)
⊢ IsIso (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)
have h₃ : Mono (X := (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry).X₃) (Y := (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ sorry sorry).X₃)
  (ShortComplex.Hom.τ₃ (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ sorry sorry) :
    (X.shortComplex f₁ f₂ f₃ n₁ n₂ n₃ sorry sorry).X₃ ⟶ (X.shortComplex f₁ f₂ f₃₄ n₁ n₂ n₃ sorry sorry).X₃)
Tactic: apply ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
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 := (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₂)
have 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)) sorry))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
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 := (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)) ⋯))
have h₁ : homMk₁ (𝟙 i₁) (𝟙 (Precomp.obj (mk₂ f₂ f₃) i₀ 2)) sorry = 𝟙 (mk₁ f₂)
Tactic: convert! (inferInstance : IsIso ((X.H n₂).map (𝟙 _)))
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
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₃)
have h₃ : Mono (X := (X.H n₃).obj (mk₁ f₁)) (Y := (X.H n₃).obj (mk₁ f₁)) ((X.H n₃).map (homMk₁ (𝟙 i₀) (𝟙 i₁) sorry))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
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.H n₃).obj (mk₁ f₁)) (Y := (X.H n₃).obj (mk₁ f₁)) ((X.H n₃).map (homMk₁ (𝟙 i₀) (𝟙 i₁) ⋯))
have h₁ : homMk₁ (𝟙 i₀) (𝟙 i₁) sorry = 𝟙 (mk₁ f₁)
Tactic: convert! (inferInstance : Mono ((X.H n₃).map (𝟙 (mk₁ f₁))))
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
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.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)
have h₁ : Epi (X := (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ sorry sorry).X₁) (Y := (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry).X₁)
  (ShortComplex.Hom.τ₁ (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ sorry sorry) :
    (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ sorry sorry).X₁ ⟶ (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry).X₁)
Tactic: apply ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
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₁)
⊢ IsIso (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)
have h₂ : IsIso (X := (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ sorry sorry).X₂) (Y := (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry).X₂)
  (ShortComplex.Hom.τ₂ (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ sorry sorry) :
    (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ sorry sorry).X₂ ⟶ (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry).X₂)
Tactic: apply ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
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₂)
⊢ IsIso (X.map f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ hn₁ hn₂)
have h₃ : Mono (X := (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ sorry sorry).X₃) (Y := (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry).X₃)
  (ShortComplex.Hom.τ₃ (X.shortComplexMap f₂₃ f₄ f₅ f₃ f₄ f₅ (fourδ₁Toδ₀ f₂ f₃ f₄ f₅ f₂₃ h₂₃) n₀ n₁ n₂ sorry sorry) :
    (X.shortComplex f₂₃ f₄ f₅ n₀ n₁ n₂ sorry sorry).X₃ ⟶ (X.shortComplex f₃ f₄ f₅ n₀ n₁ n₂ sorry sorry).X₃)
Tactic: apply ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'
-- Lean 4 proof step from Mathlib.Algebra.Homology.SpectralObject.EpiMono (goal)
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₁)
have 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)) sorry))
Tactic: dsimp