awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ((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

Tactic:
simp [cocycle₁]

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ι)
α : 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 ι) ⋯) ⋯
rw₁ rw₂ :
  (Cochain.ofHom π).comp ((↑(cocycle₁ sq hsq hQ hK) : Cochain Q K 1).comp (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)

Tactic:
rw [← comp_coe_cocycle₁_comp sq hsq hQ hK, hα]

Premises used: CochainComplex.Lifting.comp_coe_cocycle₁_comp
-- 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ι)
α : 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)

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α]
-- 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ι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
⊢ HAdd.hAdd (α := ℤ) 0 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ι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
h :
  ∀ (p_1 : ℤ),
    Cochain.v (δ 0 1 (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯)) p_1 (p_1 + 1) ⋯ =
      Cochain.v 0 p_1 (p_1 + 1) ⋯
⊢ Eq (α := Cochain B X 1) (δ 0 1 (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯)) 0

Tactic:
ext p _ 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_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 ((Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯) p (p + 1) ⋯ =
    (↑(cocycle₁' sq hsq) : Cochain B X 1).v p (p + 1) ⋯

Tactic:
replace hα := Cochain.congr_v hα p _ 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_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
p : ℤ
hα :
  Cochain.v ((Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯) p (p + 1) ⋯ =
    (↑(cocycle₁' sq hsq) : Cochain B X 1).v p (p + 1) ⋯
⊢ π.f p ≫ α.v p p ⋯ ≫ K.d p (p + 1) ≫ ι.f (p + 1) - B.d p (p + 1) ≫ π.f (p + 1) ≫ α.v (p + 1) (p + 1) ⋯ ≫ ι.f (p + 1) =
    HSub.hSub (α := B.X p ⟶ X.X (p + 1)) ((hsq p).l ≫ X.d p (p + 1)) (B.d p (p + 1) ≫ CommSq.LiftStruct.l (hsq (p + 1)))

Tactic:
simp only [Cochain.zero_cochain_comp_v, Cochain.ofHom_v, Cochain.comp_zero_cochain_v,
              δ_zero_cochain_v, Preadditive.sub_comp, Category.assoc, Preadditive.comp_sub,
              HomologicalComplex.Hom.comm_assoc, cocycle₁', Cocycle.mk_coe, Cochain.ofHoms_v,
              HomologicalComplex.eval_obj, HomologicalComplex.eval_map] at hα

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.eval_map, CochainComplex.HomComplex.Cochain.comp_zero_cochain_v, CochainComplex.HomComplex.Cochain.zero_cochain_comp_v, CochainComplex.HomComplex.Cochain.ofHom_v, CochainComplex.Lifting.cocycle₁', CochainComplex.HomComplex.Cochain.ofHoms_v, HomologicalComplex.eval_obj, CochainComplex.HomComplex.δ_zero_cochain_v, HomologicalComplex.Hom.comm_assoc, CategoryTheory.Preadditive.comp_sub, CochainComplex.HomComplex.Cocycle.mk_coe, CategoryTheory.Preadditive.sub_comp
-- 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_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
p : ℤ
hα :
  π.f p ≫ α.v p p ⋯ ≫ K.d p (p + 1) ≫ ι.f (p + 1) - B.d p (p + 1) ≫ π.f (p + 1) ≫ α.v (p + 1) (p + 1) ⋯ ≫ ι.f (p + 1) =
    HSub.hSub (α := B.X p ⟶ X.X (p + 1)) ((hsq p).l ≫ X.d p (p + 1)) (B.d p (p + 1) ≫ CommSq.LiftStruct.l (hsq (p + 1)))
⊢ Cochain.v (δ 0 1 (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯)) p (p + 1) ⋯ =
    Cochain.v 0 p (p + 1) ⋯

Tactic:
simp [hα]
-- 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ι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
h : ∀ (n : ℤ), (i ≫ l.homOf).f n = t.f n
⊢ i ≫ l.homOf = t

Tactic:
ext n
-- 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ι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
⊢ i.f n ≫ π.f n = 0

Tactic:
simp [← HomologicalComplex.comp_f, hπ]

Premises used: HomologicalComplex.comp_f
-- 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ι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
⊢ i.f n ≫ π.f n = 0

Tactic:
have h₁ : i.f n ≫ π.f n = 0 := by
          simp [← HomologicalComplex.comp_f, hπ]
-- 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ι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
h₁ : i.f n ≫ π.f n = 0
⊢ CategoryTheory.Functor.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n) i ≫ (hsq n).l =
    CategoryTheory.Functor.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n) t

Tactic:
have h₂ := (hsq n).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) ⋯
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)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
h₁ : i.f n ≫ π.f n = 0
h₂ : i.f n ≫ (hsq n).l = t.f n
⊢ (i ≫ l.homOf).f n = t.f n

Tactic:
simp [l, reassoc_of% h₁, h₂]
-- 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ι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
h : ∀ (n : ℤ), (l.homOf ≫ p).f n = b.f n
⊢ l.homOf ≫ p = b

Tactic:
ext n
-- 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ι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
⊢ ι.f n ≫ p.f n = 0

Tactic:
simp [← HomologicalComplex.comp_f, hι]

Premises used: HomologicalComplex.comp_f
-- 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ι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
⊢ ι.f n ≫ p.f n = 0

Tactic:
have : ι.f n ≫ p.f n = 0 := by
          simp [← HomologicalComplex.comp_f, hι]
-- 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ι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp (Cochain.comp (δ 0 1 α) (Cochain.ofHom ι) ⋯) ⋯ = (↑(cocycle₁' sq hsq) : Cochain B X 1)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
this : ι.f n ≫ p.f n = 0
⊢ (l.homOf ≫ p).f n = b.f n

Tactic:
simpa [l, this] using (hsq n).fac_right

Premises used: CategoryTheory.CommSq.LiftStruct.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) ⋯
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)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
⊢ Nonempty.{v_1 + 1} sq.LiftStruct

Tactic:
exact ⟨{
      l := l.homOf
      fac_left := by
        ext n
        have h₁ : i.f n ≫ π.f n = 0 := by
          simp [← HomologicalComplex.comp_f, hπ]
        have h₂ := (hsq n).fac_left
        dsimp at h₁ h₂
        simp [l, reassoc_of% h₁, h₂]
      fac_right := by
        ext n
        have : ι.f n ≫ p.f n = 0 := by
          simp [← HomologicalComplex.comp_f, hι]
        simpa [l, this] using (hsq n).fac_right }⟩
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
K₁ K₂ : HomologicalComplex.{v_1, u_1, u_2} C c
inst_8 : GradedObject.HasTensor.{u_2, v_1, u_1} K₁.X K₂.X
⊢ K₁.HasTensor K₂

Tactic:
assumption
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
K₁ K₂ K₃ : HomologicalComplex.{v_1, u_1, u_2} C c
inst_8 : GradedObject.HasGoodTensor₁₂Tensor.{u_2, v_1, u_1} K₁.X K₂.X K₃.X
⊢ K₁.HasGoodTensor₁₂ K₂ K₃

Tactic:
inferInstanceAs (GradedObject.HasGoodTensor₁₂Tensor K₁.X K₂.X K₃.X)

Premises used: _private.0.HomologicalComplex.instHasGoodTensor₁₂OfHasGoodTensor₁₂TensorX._proof_1
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
K₁ K₂ K₃ : HomologicalComplex.{v_1, u_1, u_2} C c
inst_8 : GradedObject.HasGoodTensorTensor₂₃.{u_2, v_1, u_1} K₁.X K₂.X K₃.X
⊢ K₁.HasGoodTensor₂₃ K₂ K₃

Tactic:
inferInstanceAs (GradedObject.HasGoodTensorTensor₂₃ K₁.X K₂.X K₃.X)

Premises used: _private.0.HomologicalComplex.instHasGoodTensor₂₃OfHasGoodTensorTensor₂₃X._proof_1
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_8 : DecidableEq I
inst_9 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
⊢ GradedObject.HasTensor.{u_2, v_1, u_1} (X.{v_1, u_1, u_2} (tensorUnit C c)) K.X

Tactic:
GradedObject.hasTensor_of_iso (tensorUnitIso C c) (Iso.refl _)

Premises used: HomologicalComplex.tensorUnitIso, CategoryTheory.Iso.refl, CategoryTheory.GradedObject.hasTensor_of_iso
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_8 : DecidableEq I
inst_9 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
⊢ HasTensor (tensorUnit C c) K

Tactic:
inferInstanceAs (GradedObject.HasTensor (tensorUnit C c).X K.X)

Premises used: _private.0.HomologicalComplex.instHasTensorTensorUnit._proof_1
-- Module: Mathlib.Algebra.Homology.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Functor.Additive (D := CategoryTheory.Functor.{v_1, v_1, u_1, u_1} C C) (curriedTensor C)
inst_5 : ∀ (X₁ : C), Functor.Additive.{v_1, u_1, v_1, u_1} (Functor.obj (curriedTensor C) X₁)
I : Type u_2
inst_6 : AddMonoid I
c : ComplexShape I
inst_7 : c.TensorSigns
K : HomologicalComplex.{v_1, u_1, u_2} C c
inst_8 : DecidableEq I
inst_9 :
  ∀ (X₂ : C),
    PreservesColimit.{0, 0, v_1, v_1, u_1, u_1} (Functor.empty C) (Functor.obj (Functor.flip (curriedTensor C)) X₂)
i₁ i₂ j : I
pos :
  ∀ (h₁ : c.Rel i₁ (c.next i₁)),
    Eq (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j) 0
neg :
  ∀ (h₁ : ¬c.Rel i₁ (c.next i₁)),
    Eq (α :=
      Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁))
          (K.X i₂) ⟶
        X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
      (mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j) 0
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) (X.{v_1, u_1, u_2} (tensorUnit C c) i₁)) (K.X i₂) ⟶
      X (mapBifunctor (tensorUnit C c) K (curriedTensor C) c) j)
    (mapBifunctor.d₁ (tensorUnit C c) K (curriedTensor C) c i₁ i₂ j) 0

Tactic:
by_cases h₁ : c.Rel i₁ (c.next i₁)

Premises used: ComplexShape.next, ComplexShape.Rel