awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this_1 : Epi π
this : Mono ι
n : ℤ
⊢ Cochain.v (δ 1 2 (cochain₁ sq hsq hQ hK)) n (n + 2) ⋯ = Cochain.v 0 n (n + 2) ⋯
have this₁ : Eq (α := B.X n ⟶ X.X (n + 2)) (Cochain.v (δ 1 2 (↑(cocycle₁' sq hsq) : Cochain B X 1)) n (n + 2) sorry)
  (Cochain.v 0 n (n + 2) sorry)
Tactic: have this := Cochain.congr_v ((cocycle₁' sq hsq).δ_eq_zero 2) n _ rfl
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this_1 : Epi π
this_2 : Mono ι
n : ℤ
this :
  Eq (α := B.X n ⟶ X.X (n + 2)) (Cochain.v (δ 1 2 (↑(cocycle₁' sq hsq) : Cochain B X 1)) n (n + 2) ⋯)
    (Cochain.v 0 n (n + 2) ⋯)
⊢ Cochain.v (δ 1 2 (cochain₁ sq hsq hQ hK)) n (n + 2) ⋯ = Cochain.v 0 n (n + 2) ⋯
have h : ∀
  (this :
    CategoryStruct.comp (Y := X.X (n + 1)) ((↑(cocycle₁' sq hsq) : Cochain B X 1).v n (n + 1) sorry) (X.d (n + 1) (n + 2)) +
        B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) sorry =
      0),
  HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) sorry ≫ K.d (n + 1) (n + 2))
      (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) sorry) =
    0
Tactic: rw [Cochain.zero_v, δ_v _ _ (by simp) _ _ _ _ (n + 1) _ (by lia) rfl,
      Int.negOnePow_even 2 ⟨1, by simp⟩, one_smul] at this ⊢
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this_1 : Epi π
this_2 : Mono ι
n : ℤ
this :
  CategoryStruct.comp (Y := X.X (n + 1)) ((↑(cocycle₁' sq hsq) : Cochain B X 1).v n (n + 1) ⋯) (X.d (n + 1) (n + 2)) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) ⋯ =
    0
⊢ HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
      (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) =
    0
have h : HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) sorry ≫ K.d (n + 1) (n + 2))
      (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) sorry) ≫
    ι.f (n + 2) =
  0 ≫ ι.f (n + 2)
Tactic: rwa [← cancel_mono (ι.f (n + 2)), ← cancel_epi (π.f n),
      Preadditive.add_comp, Category.assoc, Category.assoc, Preadditive.comp_add,
      HomologicalComplex.Hom.comm_assoc,
      π_f_cochain₁_v_ι_f, zero_comp, comp_zero, ← ι.comm,
      π_f_cochain₁_v_ι_f_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this_1 : Epi π
this_2 : Mono ι
n : ℤ
this :
  CategoryStruct.comp (Y := X.X (n + 1)) ((↑(cocycle₁' sq hsq) : Cochain B X 1).v n (n + 1) ⋯) (X.d (n + 1) (n + 2)) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) ⋯ =
    0
h :
  HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
        (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫
      ι.f (n + 2) =
    0 ≫ ι.f (n + 2)
⊢ HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
      (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) =
    0
have h₁ : π.f n ≫
    HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) sorry ≫ K.d (n + 1) (n + 2))
        (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) sorry) ≫
      ι.f (n + 2) =
  π.f n ≫ 0 ≫ ι.f (n + 2)
Tactic: rwa [← cancel_mono (ι.f (n + 2)), ← cancel_epi (π.f n),
      Preadditive.add_comp, Category.assoc, Category.assoc, Preadditive.comp_add,
      HomologicalComplex.Hom.comm_assoc,
      π_f_cochain₁_v_ι_f, zero_comp, comp_zero, ← ι.comm,
      π_f_cochain₁_v_ι_f_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this_1 : Epi π
this_2 : Mono ι
n : ℤ
this :
  CategoryStruct.comp (Y := X.X (n + 1)) ((↑(cocycle₁' sq hsq) : Cochain B X 1).v n (n + 1) ⋯) (X.d (n + 1) (n + 2)) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) ⋯ =
    0
h :
  HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
        (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫
      ι.f (n + 2) =
    0 ≫ ι.f (n + 2)
h₁ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
          (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫
        ι.f (n + 2) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
⊢ HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
      (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) =
    0
have h₂ : π.f n ≫
    HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) (((cochain₁ sq hsq hQ hK).v n (n + 1) sorry ≫ K.d (n + 1) (n + 2)) ≫ ι.f (n + 2))
      ((Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) sorry) ≫ ι.f (n + 2)) =
  π.f n ≫ 0 ≫ ι.f (n + 2)
Tactic: rwa [← cancel_mono (ι.f (n + 2)), ← cancel_epi (π.f n),
      Preadditive.add_comp, Category.assoc, Category.assoc, Preadditive.comp_add,
      HomologicalComplex.Hom.comm_assoc,
      π_f_cochain₁_v_ι_f, zero_comp, comp_zero, ← ι.comm,
      π_f_cochain₁_v_ι_f_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this_1 : Epi π
this_2 : Mono ι
n : ℤ
this :
  CategoryStruct.comp (Y := X.X (n + 1)) ((↑(cocycle₁' sq hsq) : Cochain B X 1).v n (n + 1) ⋯) (X.d (n + 1) (n + 2)) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) ⋯ =
    0
h :
  HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
        (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫
      ι.f (n + 2) =
    0 ≫ ι.f (n + 2)
h₁ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
          (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫
        ι.f (n + 2) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₂ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) (((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2)) ≫ ι.f (n + 2))
        ((Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
⊢ HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
      (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) =
    0
have h₃ : π.f n ≫
    HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) sorry ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
      ((Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) sorry) ≫ ι.f (n + 2)) =
  π.f n ≫ 0 ≫ ι.f (n + 2)
Tactic: rwa [← cancel_mono (ι.f (n + 2)), ← cancel_epi (π.f n),
      Preadditive.add_comp, Category.assoc, Category.assoc, Preadditive.comp_add,
      HomologicalComplex.Hom.comm_assoc,
      π_f_cochain₁_v_ι_f, zero_comp, comp_zero, ← ι.comm,
      π_f_cochain₁_v_ι_f_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this_1 : Epi π
this_2 : Mono ι
n : ℤ
this :
  CategoryStruct.comp (Y := X.X (n + 1)) ((↑(cocycle₁' sq hsq) : Cochain B X 1).v n (n + 1) ⋯) (X.d (n + 1) (n + 2)) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) ⋯ =
    0
h :
  HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
        (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫
      ι.f (n + 2) =
    0 ≫ ι.f (n + 2)
h₁ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
          (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫
        ι.f (n + 2) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₂ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) (((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2)) ≫ ι.f (n + 2))
        ((Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₃ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
        ((Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
⊢ HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
      (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) =
    0
have h₄ : π.f n ≫
    HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) sorry ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
      (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) sorry ≫ ι.f (n + 2)) =
  π.f n ≫ 0 ≫ ι.f (n + 2)
Tactic: rwa [← cancel_mono (ι.f (n + 2)), ← cancel_epi (π.f n),
      Preadditive.add_comp, Category.assoc, Category.assoc, Preadditive.comp_add,
      HomologicalComplex.Hom.comm_assoc,
      π_f_cochain₁_v_ι_f, zero_comp, comp_zero, ← ι.comm,
      π_f_cochain₁_v_ι_f_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this_1 : Epi π
this_2 : Mono ι
n : ℤ
this :
  CategoryStruct.comp (Y := X.X (n + 1)) ((↑(cocycle₁' sq hsq) : Cochain B X 1).v n (n + 1) ⋯) (X.d (n + 1) (n + 2)) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) ⋯ =
    0
h :
  HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
        (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫
      ι.f (n + 2) =
    0 ≫ ι.f (n + 2)
h₁ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
          (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫
        ι.f (n + 2) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₂ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) (((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2)) ≫ ι.f (n + 2))
        ((Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₃ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
        ((Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₄ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
        (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯ ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
⊢ HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
      (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) =
    0
have h₅ : HAdd.hAdd (α := B.X n ⟶ X.X (n + 2)) (π.f n ≫ (cochain₁ sq hsq hQ hK).v n (n + 1) sorry ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
    (π.f n ≫ Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) sorry ≫ ι.f (n + 2)) =
  π.f n ≫ 0 ≫ ι.f (n + 2)
Tactic: rwa [← cancel_mono (ι.f (n + 2)), ← cancel_epi (π.f n),
      Preadditive.add_comp, Category.assoc, Category.assoc, Preadditive.comp_add,
      HomologicalComplex.Hom.comm_assoc,
      π_f_cochain₁_v_ι_f, zero_comp, comp_zero, ← ι.comm,
      π_f_cochain₁_v_ι_f_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this_1 : Epi π
this_2 : Mono ι
n : ℤ
this :
  CategoryStruct.comp (Y := X.X (n + 1)) ((↑(cocycle₁' sq hsq) : Cochain B X 1).v n (n + 1) ⋯) (X.d (n + 1) (n + 2)) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) ⋯ =
    0
h :
  HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
        (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫
      ι.f (n + 2) =
    0 ≫ ι.f (n + 2)
h₁ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
          (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫
        ι.f (n + 2) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₂ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) (((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2)) ≫ ι.f (n + 2))
        ((Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₃ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
        ((Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₄ :
  π.f n ≫
      HAdd.hAdd (α := Q.X n ⟶ X.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
        (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯ ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
h₅ :
  HAdd.hAdd (α := B.X n ⟶ X.X (n + 2))
      (π.f n ≫ (cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
      (π.f n ≫ Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯ ≫ ι.f (n + 2)) =
    π.f n ≫ 0 ≫ ι.f (n + 2)
⊢ HAdd.hAdd (α := Q.X n ⟶ K.X (n + 2)) ((cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2))
      (Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯) =
    0
have h₆ : HAdd.hAdd (α := B.X n ⟶ X.X (n + 2)) (π.f n ≫ (cochain₁ sq hsq hQ hK).v n (n + 1) sorry ≫ K.d (n + 1) (n + 2) ≫ ι.f (n + 2))
    (B.d n (n + 1) ≫ π.f (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) sorry ≫ ι.f (n + 2)) =
  π.f n ≫ 0 ≫ ι.f (n + 2)
Tactic: rwa [← cancel_mono (ι.f (n + 2)), ← cancel_epi (π.f n),
      Preadditive.add_comp, Category.assoc, Category.assoc, Preadditive.comp_add,
      HomologicalComplex.Hom.comm_assoc,
      π_f_cochain₁_v_ι_f, zero_comp, comp_zero, ← ι.comm,
      π_f_cochain₁_v_ι_f_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
⊢ (Cochain.ofHom π).comp ((↑(cocycle₁ sq hsq hQ hK) : Cochain Q K 1).comp (Cochain.ofHom ι) ⋯) ⋯ =
    (↑(cocycle₁' sq hsq) : Cochain B X 1)
have h : ∀ (n m : ℤ) (hnm : n + 1 = m),
  ((Cochain.ofHom π).comp ((↑(cocycle₁ sq hsq hQ hK) : Cochain Q K 1).comp (Cochain.ofHom ι) sorry) sorry).v n m hnm =
    (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm
Tactic: ext n m hnm
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : δ 0 1 α = (↑(cocycle₁ sq hsq hQ hK) : Cochain Q K 1)
⊢ (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
have rw : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) sorry) sorry =
  (Cochain.ofHom π).comp ((↑(cocycle₁ sq hsq hQ hK) : Cochain Q K 1).comp (Cochain.ofHom ι) sorry) sorry
Tactic: rw [← comp_coe_cocycle₁_comp sq hsq hQ hK, hα]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : δ 0 1 α = (↑(cocycle₁ sq hsq hQ hK) : Cochain Q K 1)
rw :
  (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ =
    (Cochain.ofHom π).comp ((↑(cocycle₁ sq hsq hQ hK) : Cochain Q K 1).comp (Cochain.ofHom ι) ⋯) ⋯
⊢ (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
have rw₁ : (Cochain.ofHom π).comp ((↑(cocycle₁ sq hsq hQ hK) : Cochain Q K 1).comp (Cochain.ofHom ι) sorry) sorry =
  (Cochain.ofHom π).comp ((↑(cocycle₁ sq hsq hQ hK) : Cochain Q K 1).comp (Cochain.ofHom ι) sorry) sorry
Tactic: rw [← comp_coe_cocycle₁_comp sq hsq hQ hK, hα]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : δ 0 1 α = (↑(cocycle₁ sq hsq hQ hK) : Cochain Q K 1)
⊢ Nonempty.{v_1 + 1} sq.LiftStruct
have hα₁ : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) sorry) sorry = (↑(cocycle₁' sq hsq) : Cochain B X 1)
Tactic: replace hα : (Cochain.ofHom π).comp ((δ 0 1 α).comp (.ofHom ι) (add_zero 1)) (zero_add 1) =
        (cocycle₁' sq hsq).1 := by
      rw [← comp_coe_cocycle₁_comp sq hsq hQ hK, hα]
Cleared hypotheses: hα
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
⊢ Eq (α := Cochain B X 1) (δ 0 1 (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯)) 0
have h : ∀ (p_1 : ℤ),
  Cochain.v (δ 0 1 (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) sorry) sorry)) p_1 (p_1 + 1) sorry =
    Cochain.v 0 p_1 (p_1 + 1) sorry
Tactic: ext p _ rfl
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Lifting (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Abelian.{v_1, u_1} C
A B X Y : CochainComplex.{v_1, u_1, 0} C ℤ
t : A ⟶ X
i : A ⟶ B
p_1 : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p_1 b
hsq : (n : ℤ) → CommSq.LiftStruct (A := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A) ⋯
Q : CochainComplex.{v_1, u_1, 0} C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex.{v_1, u_1, 0} C ℤ
ι : K ⟶ X
hι : ι ≫ p_1 = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
p : ℤ
⊢ Cochain.v (δ 0 1 (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯)) p (p + 1) ⋯ =
    Cochain.v 0 p (p + 1) ⋯
have hα₁ : Cochain.v ((Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) sorry) sorry) p (p + 1) sorry =
  (↑(cocycle₁' sq hsq) : Cochain B X 1).v p (p + 1) sorry
Tactic: replace hα := Cochain.congr_v hα p _ rfl
Cleared hypotheses: hα