awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
pos :
  ∀ (h : c.Rel i (c.next i)),
    f.f (c.next i) =
      HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
          (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
            (ho.hom (c.next (c.next i)) (c.next i)))
          (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
        g.f (c.next i)
⊢ f.f (c.next i) =
    (if c.Rel i (c.next i) then
          CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
            (ho.hom (c.next (c.next i)) (c.next i))
        else
          HSub.hSub (α := K.X (c.next i) ⟶ L.X (c.next i)) (f.f (c.next i)) (g.f (c.next i)) -
            ho.hom (c.next i) i ≫ L.d i (c.next i)) +
        ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)
have neg : ∀ (h : ¬c.Rel i (c.next i)),
  f.f (c.next i) =
    HSub.hSub (α := K.X (c.next i) ⟶ L.X (c.next i)) (f.f (c.next i)) (g.f (c.next i)) -
          ho.hom (c.next i) i ≫ L.d i (c.next i) +
        ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel i (c.next i)
⊢ f.f (c.next i) =
    HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
        (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
      g.f (c.next i)
have pos : HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i)) (β := K.X (c.next i) ⟶ L.X (c.next i))
      ((dNext (c.next i) : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X (c.next i) ⟶ L.X (c.next i)) ho.hom :
        K.X (c.next i) ⟶ L.X (c.next i))
      ((prevD (c.next i) : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X (c.next i) ⟶ L.X (c.next i)) ho.hom :
        K.X (c.next i) ⟶ L.X (c.next i)) +
    g.f (c.next i) =
  HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
      (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
        (ho.hom (c.next (c.next i)) (c.next i)))
      (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
    g.f (c.next i)
Tactic: rw [ho.comm (c.next i)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel i (c.next i)
⊢ HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i)) (β := K.X (c.next i) ⟶ L.X (c.next i))
        ((dNext (c.next i) : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X (c.next i) ⟶ L.X (c.next i)) ho.hom :
          K.X (c.next i) ⟶ L.X (c.next i))
        ((prevD (c.next i) : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X (c.next i) ⟶ L.X (c.next i)) ho.hom :
          K.X (c.next i) ⟶ L.X (c.next i)) +
      g.f (c.next i) =
    HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
        (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
      g.f (c.next i)
have pos : HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
      (CategoryStruct.comp (Y := K.xNext (c.next i)) (K.d (c.next i) (c.next (c.next i)))
        (ho.hom (c.next (c.next i)) (c.next i)))
      (CategoryStruct.comp (Y := L.xPrev (c.next i)) (ho.hom (c.next i) (c.prev (c.next i)))
        (L.d (c.prev (c.next i)) (c.next i))) +
    g.f (c.next i) =
  HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
      (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
        (ho.hom (c.next (c.next i)) (c.next i)))
      (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
    g.f (c.next i)
Tactic: dsimp [dFrom, dTo, fromNext, toPrev]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel i (c.next i)
⊢ HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (CategoryStruct.comp (Y := K.xNext (c.next i)) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
        (CategoryStruct.comp (Y := L.xPrev (c.next i)) (ho.hom (c.next i) (c.prev (c.next i)))
          (L.d (c.prev (c.next i)) (c.next i))) +
      g.f (c.next i) =
    HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
        (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
      g.f (c.next i)
have pos : HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
      (CategoryStruct.comp (Y := K.xNext (c.next i)) (K.d (c.next i) (c.next (c.next i)))
        (ho.hom (c.next (c.next i)) (c.next i)))
      (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
    g.f (c.next i) =
  HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
      (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
        (ho.hom (c.next (c.next i)) (c.next i)))
      (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
    g.f (c.next i)
Tactic: rw [congr_arg (fun j => ho.hom (c.next i) j ≫ L.d j (c.next i)) (c.prev_eq' h)]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst_5 : K.HasHomology i
inst_6 : L.HasHomology i
⊢ CategoryStruct.comp (Y := L.homology i) (homologyMap h.hom i) (homologyMap h.inv i) = 𝟙 (K.homology i)
have rw : homologyMap (h.hom ≫ h.inv) i = 𝟙 (K.homology i)
Tactic: rw [← homologyMap_comp, h.homotopyHomInvId.homologyMap_eq, homologyMap_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst_5 : K.HasHomology i
inst_6 : L.HasHomology i
rw : homologyMap (h.hom ≫ h.inv) i = 𝟙 (K.homology i)
⊢ CategoryStruct.comp (Y := L.homology i) (homologyMap h.hom i) (homologyMap h.inv i) = 𝟙 (K.homology i)
have rw₁ : homologyMap (𝟙 K) i = 𝟙 (K.homology i)
Tactic: rw [← homologyMap_comp, h.homotopyHomInvId.homologyMap_eq, homologyMap_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst_5 : K.HasHomology i
inst_6 : L.HasHomology i
rw : homologyMap (h.hom ≫ h.inv) i = 𝟙 (K.homology i)
rw₁ : homologyMap (𝟙 K) i = 𝟙 (K.homology i)
⊢ CategoryStruct.comp (Y := L.homology i) (homologyMap h.hom i) (homologyMap h.inv i) = 𝟙 (K.homology i)
have rw₂ : Eq.{v_1 + 1} (α := K.homology i ⟶ K.homology i) (𝟙 (K.homology i)) (𝟙 (K.homology i))
Tactic: rw [← homologyMap_comp, h.homotopyHomInvId.homologyMap_eq, homologyMap_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst_5 : K.HasHomology i
inst_6 : L.HasHomology i
⊢ CategoryStruct.comp (Y := K.homology i) (homologyMap h.inv i) (homologyMap h.hom i) = 𝟙 (L.homology i)
have rw : homologyMap (h.inv ≫ h.hom) i = 𝟙 (L.homology i)
Tactic: rw [← homologyMap_comp, h.homotopyInvHomId.homologyMap_eq, homologyMap_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst_5 : K.HasHomology i
inst_6 : L.HasHomology i
rw : homologyMap (h.inv ≫ h.hom) i = 𝟙 (L.homology i)
⊢ CategoryStruct.comp (Y := K.homology i) (homologyMap h.inv i) (homologyMap h.hom i) = 𝟙 (L.homology i)
have rw₁ : homologyMap (𝟙 L) i = 𝟙 (L.homology i)
Tactic: rw [← homologyMap_comp, h.homotopyInvHomId.homologyMap_eq, homologyMap_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst_5 : K.HasHomology i
inst_6 : L.HasHomology i
rw : homologyMap (h.inv ≫ h.hom) i = 𝟙 (L.homology i)
rw₁ : homologyMap (𝟙 L) i = 𝟙 (L.homology i)
⊢ CategoryStruct.comp (Y := K.homology i) (homologyMap h.inv i) (homologyMap h.hom i) = 𝟙 (L.homology i)
have rw₂ : Eq.{v_1 + 1} (α := L.homology i ⟶ L.homology i) (𝟙 (L.homology i)) (𝟙 (L.homology i))
Tactic: rw [← homologyMap_comp, h.homotopyInvHomId.homologyMap_eq, homologyMap_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Acyclic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
⊢ subcategoryAcyclic C (Functor.obj (quotient C (ComplexShape.up ℤ)) K) ↔ ∀ (n : ℤ), HomologicalComplex.ExactAt K n
have rw : (∀ (n : ℤ),
    IsZero.{v, u}
      (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) (Functor.obj (quotient C (ComplexShape.up ℤ)) K))) ↔
  ∀ (n : ℤ), HomologicalComplex.ExactAt K n
Tactic: rw [mem_subcategoryAcyclic_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Acyclic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
⊢ (∀ (n : ℤ),
      IsZero.{v, u}
        (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) (Functor.obj (quotient C (ComplexShape.up ℤ)) K))) ↔
    ∀ (n : ℤ), HomologicalComplex.ExactAt K n
have refine : ∀ (n : ℤ),
  IsZero.{v, u}
      (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) (Functor.obj (quotient C (ComplexShape.up ℤ)) K)) ↔
    HomologicalComplex.ExactAt K n
Tactic: refine forall_congr' (fun n => ?_)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Acyclic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ IsZero.{v, u}
      (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) (Functor.obj (quotient C (ComplexShape.up ℤ)) K)) ↔
    HomologicalComplex.ExactAt K n
have simp : IsZero.{v, u} (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) (Functor.obj (quotient C (ComplexShape.up ℤ)) K)) ↔
  IsZero.{v, u} (HomologicalComplex.homology K n)
Tactic: simp only [HomologicalComplex.exactAt_iff_isZero_homology]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Acyclic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ Eq (α := MorphismProperty (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))) (quasiIso C (ComplexShape.up ℤ))
    (ObjectProperty.trW (subcategoryAcyclic C))
have h : ∀ ⦃K L : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)⦄ (f : K ⟶ L),
  quasiIso C (ComplexShape.up ℤ) f ↔ ObjectProperty.trW (subcategoryAcyclic C) f
Tactic: ext K L f
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.Acyclic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ MorphismProperty.IsCompatibleWithShift (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (quasiIso C (ComplexShape.up ℤ)) ℤ
have rw : MorphismProperty.IsCompatibleWithShift (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
  (ObjectProperty.trW (subcategoryAcyclic C)) ℤ
Tactic: rw [quasiIso_eq_trW_subcategoryAcyclic]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
⊢ Eq.{v + 1} (α := Cochain S.X₃ S.X₁ 2)
    (δ 1 2 (Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)) 0
have h : ∀ (p : ℤ),
  Eq.{v + 1} (α := S.X₃.X p ⟶ S.X₁.X (p + 2))
    (Cochain.v (δ 1 2 (Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)) p (p + 2) sorry)
    (Cochain.v 0 p (p + 2) sorry)
Tactic: ext p _ rfl
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
p : ℤ
⊢ Eq.{v + 1} (α := S.X₃.X p ⟶ S.X₁.X (p + 2))
    (Cochain.v (δ 1 2 (Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)) p (p + 2) ⋯)
    (Cochain.v 0 p (p + 2) ⋯)
have this : Mono (X := ShortComplex.X₁ (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
  (ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
Tactic: have := mono_of_mono_fac (σ (p + 2)).f_r
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
p : ℤ
this :
  Mono (X := ShortComplex.X₁ (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
    (ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
⊢ Eq.{v + 1} (α := S.X₃.X p ⟶ S.X₁.X (p + 2))
    (Cochain.v (δ 1 2 (Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)) p (p + 2) ⋯)
    (Cochain.v 0 p (p + 2) ⋯)
have r_f : ∀ (n : ℤ),
  (σ n).r ≫ ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) n)) =
    𝟙 (ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) n))) -
      ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) n)) ≫ (σ n).s
Tactic: have r_f := fun n => (σ n).r_f
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
p : ℤ
this :
  Mono (X := ShortComplex.X₁ (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
    (ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
r_f :
  ∀ (n : ℤ),
    (σ n).r ≫ ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) n)) =
      𝟙 (ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) n))) -
        ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) n)) ≫ (σ n).s
⊢ Eq.{v + 1} (α := S.X₃.X p ⟶ S.X₁.X (p + 2))
    (Cochain.v (δ 1 2 (Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)) p (p + 2) ⋯)
    (Cochain.v 0 p (p + 2) ⋯)
have s_g : ∀ (n : ℤ),
  (σ n).s ≫ ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) n)) =
    𝟙 (ShortComplex.X₃ (S.map (eval C (ComplexShape.up ℤ) n)))
Tactic: have s_g := fun n => (σ n).s_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
p : ℤ
this :
  Mono (X := ShortComplex.X₁ (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
    (ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
r_f :
  ∀ (n : ℤ),
    (σ n).r ≫ ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) n)) =
      𝟙 (ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) n))) -
        ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) n)) ≫ (σ n).s
s_g :
  ∀ (n : ℤ),
    (σ n).s ≫ ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) n)) =
      𝟙 (ShortComplex.X₃ (S.map (eval C (ComplexShape.up ℤ) n)))
⊢ Eq.{v + 1} (α := S.X₃.X p ⟶ S.X₁.X (p + 2))
    (Cochain.v (δ 1 2 (Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)) p (p + 2) ⋯)
    (Cochain.v 0 p (p + 2) ⋯)
have h : Eq.{v + 1} (α := S.X₃.X p ⟶ S.X₁.X (p + 2))
  (Cochain.v (δ 1 2 (Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)) p (p + 2) sorry) 0
Tactic: dsimp at this r_f s_g ⊢
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (goal)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
p q : ℤ
hpq : p + 1 = q
⊢ HSub.hSub (α := (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) q)))
        (Cochain.v
            (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
            q hpq ≫
          (σ q).s)
        (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) q ⋯) ≫
      HSub.hSub (α := S.X₂.X q ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
        (S.g.f q ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) q p ⋯)
        ((σ q).r ≫ (XIsoOfEq S.X₁ ⋯).hom ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) =
    𝟙 ((mappingCone (homOfDegreewiseSplit S σ)).X p)
have subst : HSub.hSub (α :=
      (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
      (Cochain.v
          (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
          (p + 1) sorry ≫
        ShortComplex.Splitting.s (σ (p + 1)))
      (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p sorry ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) sorry) ≫
    HSub.hSub (α := S.X₂.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
      (S.g.f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p sorry)
      (ShortComplex.Splitting.r (σ (p + 1)) ≫
        (XIsoOfEq S.X₁ sorry).hom ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) =
  𝟙 ((mappingCone (homOfDegreewiseSplit S σ)).X p)
Tactic: subst hpq
Cleared hypotheses: q, hpq
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
p : ℤ
⊢ HSub.hSub (α :=
        (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
        (Cochain.v
            (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
            (p + 1) ⋯ ≫
          ShortComplex.Splitting.s (σ (p + 1)))
        (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) ⋯) ≫
      HSub.hSub (α := S.X₂.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
        (S.g.f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯)
        (ShortComplex.Splitting.r (σ (p + 1)) ≫
          (XIsoOfEq S.X₁ ⋯).hom ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) =
    𝟙 ((mappingCone (homOfDegreewiseSplit S σ)).X p)
have s_g : ShortComplex.Splitting.s (σ (p + 1)) ≫ ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) (p + 1))) =
  𝟙 (ShortComplex.X₃ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
Tactic: have s_g := (σ (p + 1)).s_g
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit (hypothesis)
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
inst_2 : HasBinaryBiproducts.{v, u_1} C
p : ℤ
s_g :
  ShortComplex.Splitting.s (σ (p + 1)) ≫ ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) (p + 1))) =
    𝟙 (ShortComplex.X₃ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
⊢ HSub.hSub (α :=
        (mappingCone (homOfDegreewiseSplit S σ)).X p ⟶ ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
        (Cochain.v
            (↑(mappingCone.fst (homOfDegreewiseSplit S σ)) : Cochain (mappingCone (homOfDegreewiseSplit S σ)) S.X₃ 1) p
            (p + 1) ⋯ ≫
          ShortComplex.Splitting.s (σ (p + 1)))
        (Cochain.v (mappingCone.snd (homOfDegreewiseSplit S σ)) p p ⋯ ≫ (Cochain.ofHom S.f).v (p + 1) (p + 1) ⋯) ≫
      HSub.hSub (α := S.X₂.X (p + 1) ⟶ (mappingCone (homOfDegreewiseSplit S σ)).X p)
        (S.g.f (p + 1) ≫ Cochain.v (mappingCone.inl (homOfDegreewiseSplit S σ)) (p + 1) p ⋯)
        (ShortComplex.Splitting.r (σ (p + 1)) ≫
          (XIsoOfEq S.X₁ ⋯).hom ≫ Hom.f (mappingCone.inr (homOfDegreewiseSplit S σ)) p) =
    𝟙 ((mappingCone (homOfDegreewiseSplit S σ)).X p)
have f_r : ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 1))) ≫ ShortComplex.Splitting.r (σ (p + 1)) =
  𝟙 (ShortComplex.X₁ (S.map (eval C (ComplexShape.up ℤ) (p + 1))))
Tactic: have f_r := (σ (p + 1)).f_r