awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ModelCategory.Injective
Goal:
C : Type u_1
inst : Category.{u_2, u_1} C
inst_1 : Abelian.{u_2, u_1} C
inst_2 : EnoughInjectives.{u_2, u_1} C
K : CochainComplex.{u_2, u_1, 0} C ℤ
n : ℤ
hn : K.IsStrictlyGE n
L : CochainComplex.{u_2, u_1, 0} C ℤ
m : ℤ
hm : L.IsStrictlyGE m
f :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
d : ℤ
left : K.IsStrictlyGE (d + 1)
right : L.IsStrictlyGE d
K' : CochainComplex.{u_2, u_1, 0} C ℤ
w : K'.IsStrictlyGE d
i :
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) ⟶
    K'
p :
  K' ⟶
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
w_1 : Mono i
hp : degreewiseEpiWithInjectiveKernel p
w_2 : QuasiIso p
fac : i ≫ p = f
⊢ Nonempty
    (MorphismProperty.MapFactorizationData (C := Plus.{u_2, u_1} C) (cofibrations (Plus.{u_2, u_1} C))
      (trivialFibrations (Plus.{u_2, u_1} C)) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)
      { hom := f :
        InducedCategory.Hom (C :=
          ObjectProperty.FullSubcategory (C := CochainComplex.{u_2, u_1, 0} C ℤ) (CochainComplex.plus C)) (D :=
          CochainComplex.{u_2, u_1, 0} C ℤ) (F := ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C))
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯) })

Tactic:
exact ⟨{
      Z := ⟨K', d, inferInstance⟩
      i := ObjectProperty.homMk i
      p := ObjectProperty.homMk p
      hi := by rwa [← HomotopicalAlgebra.cofibration_iff, cofibration_iff, Plus.mono_iff]
      hp := ⟨hp, by assumption⟩ }⟩
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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ι)
⊢ HAdd.hAdd (α := ℤ) 1 1 = 2

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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ι)
⊢ Eq (α := Cochain B X 2) (δ 1 2 (δ 0 1 (cochain₀ sq hsq))) 0

Tactic:
simp [δ_δ]

Premises used: CochainComplex.HomComplex.δ_δ
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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) ⋯
n m : ℤ
hnm : n + 1 = m
⊢ ∀ (k : ℤ),
    (hsq k).l ≫ CategoryTheory.Functor.map (HomologicalComplex.eval C (ComplexShape.up ℤ) k) p =
      CategoryTheory.Functor.map (HomologicalComplex.eval C (ComplexShape.up ℤ) k) b

Tactic:
have fac_right (k : ℤ) := (hsq k).fac_right
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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) ⋯
n m : ℤ
hnm : n + 1 = m
fac_right : ∀ (k : ℤ), (hsq k).l ≫ p.f k = b.f k
⊢ (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm ≫ p.f m = 0

Tactic:
simp [cocycle₁', -HomologicalComplex.Hom.comm,
    ← p.comm, fac_right, reassoc_of% fac_right, b.comm]

Premises used: CochainComplex.Lifting.cocycle₁', HomologicalComplex.Hom.comm
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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) ⋯
n m : ℤ
hnm : n + 1 = m
⊢ ∀ (k : ℤ),
    CategoryTheory.Functor.map (HomologicalComplex.eval C (ComplexShape.up ℤ) k) i ≫ (hsq k).l =
      CategoryTheory.Functor.map (HomologicalComplex.eval C (ComplexShape.up ℤ) k) t

Tactic:
have fac_left (k : ℤ) := (hsq k).fac_left
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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) ⋯
n m : ℤ
hnm : n + 1 = m
fac_left : ∀ (k : ℤ), i.f k ≫ (hsq k).l = t.f k
⊢ i.f n ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm = 0

Tactic:
simp [cocycle₁', fac_left, reassoc_of% fac_left]

Premises used: CochainComplex.Lifting.cocycle₁'
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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ι)
n m : ℤ
hnm : n + 1 = m
⊢ Epi π

Tactic:
have : Epi π := Cofork.IsColimit.epi hQ
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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ι)
n m : ℤ
hnm : n + 1 = m
this : Epi π
⊢ Eq (α := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A ⟶ X.X m)
    (CategoryTheory.Functor.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n) i ≫
      (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm)
    0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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ι)
n m : ℤ
hnm : n + 1 = m
this : Epi π
obtain :
  ∀
    (l :
      Cocone.pt (F :=
          parallelPair (X := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) n) A)
            (CategoryTheory.Functor.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n) i) 0)
          ((CokernelCofork.ofπ π hπ).map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)) ⟶
        X.X m)
    (hl :
      Cofork.π ((CokernelCofork.ofπ π hπ).map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)) ≫ l =
        (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm),
    ∃ (φ : Q.X n ⟶ K.X m), π.f n ≫ φ ≫ ι.f m = (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm
⊢ ∃ (φ : Q.X n ⟶ K.X m), π.f n ≫ φ ≫ ι.f m = (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm

Tactic:
obtain ⟨l, hl⟩ := CokernelCofork.IsColimit.desc'
    ((CokernelCofork.isColimitMapCoconeEquiv _ _).1
    (isColimitOfPreserves (HomologicalComplex.eval _ _ n) hQ))
    ((cocycle₁' sq hsq).1.v n m hnm) (by simp)

Premises used: CategoryTheory.Limits.CokernelCofork.IsColimit.desc', CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv, HomologicalComplex.eval, CochainComplex.Lifting.cocycle₁', Equiv.toFun, CochainComplex.HomComplex.Cochain.v, Subtype.val, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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ι)
n m : ℤ
hnm : n + 1 = m
this : Epi π
l : Q.X n ⟶ X.X m
hl : π.f n ≫ l = (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm
⊢ Eq (α := Q.X n ⟶ Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) m) Y)
    (l ≫ CategoryTheory.Functor.map (HomologicalComplex.eval C (ComplexShape.up ℤ) m) p) 0

Tactic:
simp [← cancel_epi (π.f n), reassoc_of% hl]

Premises used: HomologicalComplex.Hom.f, CategoryTheory.cancel_epi
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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ι)
n m : ℤ
hnm : n + 1 = m
this : Epi π
l : Q.X n ⟶ X.X m
hl : π.f n ≫ l = (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm
obtain :
  ∀
    (l' :
      Q.X n ⟶
        Cone.pt (F :=
          parallelPair (X := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) m) X)
            (CategoryTheory.Functor.map (HomologicalComplex.eval C (ComplexShape.up ℤ) m) p) 0)
          ((KernelFork.ofι ι hι).map (HomologicalComplex.eval C (ComplexShape.up ℤ) m)))
    (hl' : l' ≫ Fork.ι ((KernelFork.ofι ι hι).map (HomologicalComplex.eval C (ComplexShape.up ℤ) m)) = l),
    ∃ (φ : Q.X n ⟶ K.X m), π.f n ≫ φ ≫ ι.f m = (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm
⊢ ∃ (φ : Q.X n ⟶ K.X m), π.f n ≫ φ ≫ ι.f m = (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm

Tactic:
obtain ⟨l', hl'⟩ := KernelFork.IsLimit.lift' ((KernelFork.isLimitMapConeEquiv _ _).1
    (isLimitOfPreserves (HomologicalComplex.eval _ _ m) hK)) l (by
      simp [← cancel_epi (π.f n), reassoc_of% hl])

Premises used: CategoryTheory.Limits.KernelFork.IsLimit.lift', HomologicalComplex.eval, Equiv.toFun, CategoryTheory.Limits.KernelFork.isLimitMapConeEquiv, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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ι)
n m : ℤ
hnm : n + 1 = m
this : Epi π
l : Q.X n ⟶ X.X m
hl : π.f n ≫ l = (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm
l' :
  Q.X n ⟶
    Cone.pt (F :=
      parallelPair (X := Functor.obj (HomologicalComplex.eval C (ComplexShape.up ℤ) m) X)
        (CategoryTheory.Functor.map (HomologicalComplex.eval C (ComplexShape.up ℤ) m) p) 0)
      ((KernelFork.ofι ι hι).map (HomologicalComplex.eval C (ComplexShape.up ℤ) m))
hl' : l' ≫ Fork.ι ((KernelFork.ofι ι hι).map (HomologicalComplex.eval C (ComplexShape.up ℤ) m)) = l
⊢ ∃ (φ : Q.X n ⟶ K.X m), π.f n ≫ φ ≫ ι.f m = (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm

Tactic:
exact ⟨l', by cat_disch⟩
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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ι)
n m : ℤ
hnm : n + 1 = m
⊢ π.f n ≫ (cochain₁ sq hsq hQ hK).v n m hnm ≫ ι.f m = (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm

Tactic:
(exists_hom sq hsq hQ hK n m hnm).choose_spec

Premises used: CochainComplex.Lifting.cochain₁, Exists.choose_spec, CochainComplex.Lifting.exists_hom, CochainComplex.HomComplex.Cochain.mk, CochainComplex.HomComplex.Cochain.v
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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ι)
⊢ Epi π

Tactic:
have : Epi π := Cofork.IsColimit.epi hQ
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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 : Epi π
⊢ Mono ι

Tactic:
have : Mono ι := Fork.IsLimit.mono hK
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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 ι
h : ∀ (n : ℤ), Cochain.v (δ 1 2 (cochain₁ sq hsq hQ hK)) n (n + 2) ⋯ = Cochain.v 0 n (n + 2) ⋯
⊢ Eq (α := Cochain Q K 2) (δ 1 2 (cochain₁ sq hsq hQ hK)) 0

Tactic:
ext n _ rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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 : ℤ
⊢ 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) ⋯)

Tactic:
have this := Cochain.congr_v ((cocycle₁' sq hsq).δ_eq_zero 2) n _ rfl
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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) ⋯) 0
⊢ HAdd.hAdd (α := ℤ) 1 1 = 2

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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) ⋯) 0
⊢ n + 1 = n + 2 - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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)) +
      Int.negOnePow 2 • B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) ⋯ =
    0
⊢ HAdd.hAdd (α := ℤ) 1 1 = 2

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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)) +
      Int.negOnePow 2 • B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) ⋯ =
    0
⊢ n + 1 = n + 2 - 1

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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)) +
      Int.negOnePow 2 • B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) ⋯ =
    0
⊢ 2 = HAdd.hAdd (α := ℤ) 1 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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)) +
      HSMul.hSMul (α := ℤˣ) 1 (B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v (n + 1) (n + 2) ⋯) =
    0
⊢ 2 = HAdd.hAdd (α := ℤ) 1 1

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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) ⋯)
h :
  ∀
    (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
⊢ Cochain.v (δ 1 2 (cochain₁ sq hsq hQ hK)) n (n + 2) ⋯ = Cochain.v 0 n (n + 2) ⋯

Tactic:
rw [Cochain.zero_v, δ_v _ _ (by simp) _ _ _ _ (n + 1) _ (by lia) rfl,
      Int.negOnePow_even 2 ⟨1, by simp⟩, one_smul] at this ⊢

Premises used: CochainComplex.HomComplex.δ_v, CochainComplex.HomComplex.Cochain.zero_v, one_smul, HAdd.hAdd, Exists.intro, Int.negOnePow_even, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Homology.ModelCategory.Lifting
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ι)
h :
  ∀ (n m : ℤ) (hnm : n + 1 = m),
    ((Cochain.ofHom π).comp ((↑(cocycle₁ sq hsq hQ hK) : Cochain Q K 1).comp (Cochain.ofHom ι) ⋯) ⋯).v n m hnm =
      (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm
⊢ (Cochain.ofHom π).comp ((↑(cocycle₁ sq hsq hQ hK) : Cochain Q K 1).comp (Cochain.ofHom ι) ⋯) ⋯ =
    (↑(cocycle₁' sq hsq) : Cochain B X 1)

Tactic:
ext n m hnm