awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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 ⋯)
left_1 : Mono i
left_2 : QuasiIso i
hp : degreewiseEpiWithInjectiveKernel p
fac : i ≫ p = f
rwa :
  Cofibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
rwa₁ :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
⊢ cofibrations (Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
have rwa₂ : Mono (C := CochainComplex.{u_2, u_1, 0} C ℤ) (X :=
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
    (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K sorry))
  (Y :=
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
    (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' sorry))
  (InducedCategory.Hom.hom (ObjectProperty.homMk (P := CochainComplex.plus C) i))
Tactic: rwa [← HomotopicalAlgebra.cofibration_iff, cofibration_iff, Plus.mono_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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
⊢ ∀ {Y : Plus.{u_2, u_1} C} (f : ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯ ⟶ Y),
    Nonempty
      (MorphismProperty.MapFactorizationData (cofibrations (Plus.{u_2, u_1} C)) (trivialFibrations (Plus.{u_2, u_1} C))
        f)
have this : ∀ (L : CochainComplex.{u_2, u_1, 0} C ℤ) (m : ℤ) (hm : L.IsStrictlyGE m)
  (f :
    Quiver.Hom (V := Plus.{u_2, u_1} C) (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K sorry)
      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry)),
  Nonempty
    (MorphismProperty.MapFactorizationData (cofibrations (Plus.{u_2, u_1} C)) (trivialFibrations (Plus.{u_2, u_1} C)) f)
Tactic: ⟨L, m, hm⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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 :
      Quiver.Hom (V := Plus.{u_2, u_1} C) (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯)
        (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L ⋯)),
    Nonempty
      (MorphismProperty.MapFactorizationData (cofibrations (Plus.{u_2, u_1} C)) (trivialFibrations (Plus.{u_2, u_1} C))
        f)
have this : ∀
  (f :
    ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
        (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K sorry) ⟶
      ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
        (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry)),
  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 sorry)
      (Y := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry)
      { 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 sorry)
          (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry) })
Tactic: ⟨f⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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 ⋯)
⊢ 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 ⋯) })
have obtain : ∀ (d : ℤ),
  K.IsStrictlyGE (d + 1) →
    L.IsStrictlyGE d →
      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 sorry) (Y :=
          ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry)
          { 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 sorry)
              (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry) })
Tactic: obtain ⟨d, _, _⟩ : ∃ (d : ℤ), K.IsStrictlyGE (d + 1) ∧ L.IsStrictlyGE d :=
      ⟨min (n - 1) m, K.isStrictlyGE_of_ge _ n (by grind),
        L.isStrictlyGE_of_ge _ m (by simp)⟩
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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
⊢ 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 ⋯) })
have obtain : ∀ (K' : CochainComplex.{u_2, u_1, 0} C ℤ),
  K'.IsStrictlyGE d →
    ∀
      (i :
        ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
            (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K sorry) ⟶
          K')
      (p :
        K' ⟶
          ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
            (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry)),
      Mono i →
        ∀ (hp : degreewiseEpiWithInjectiveKernel p),
          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 sorry) (Y :=
                  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry)
                  { 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 sorry)
                      (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) L sorry) })
Tactic: obtain ⟨K', _, i, p, _, hp, _, fac⟩ := cm5b f d
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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
⊢ cofibrations (Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
have rwa : Cofibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K sorry) (Y :=
  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' sorry)
  (ObjectProperty.homMk (P := CochainComplex.plus C) i)
Tactic: rwa [← HomotopicalAlgebra.cofibration_iff, cofibration_iff, Plus.mono_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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
rwa :
  Cofibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
⊢ cofibrations (Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
have rwa₁ : Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K sorry) (Y :=
  ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' sorry)
  (ObjectProperty.homMk (P := CochainComplex.plus C) i)
Tactic: rwa [← HomotopicalAlgebra.cofibration_iff, cofibration_iff, Plus.mono_iff]
-- Lean 4 proof step from Mathlib.Algebra.Homology.ModelCategory.Injective (goal)
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
rwa :
  Cofibration (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
rwa₁ :
  Mono (C := Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
⊢ cofibrations (Plus.{u_2, u_1} C) (X := ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K ⋯) (Y :=
    ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' ⋯)
    (ObjectProperty.homMk (P := CochainComplex.plus C) i)
have rwa₂ : Mono (C := CochainComplex.{u_2, u_1, 0} C ℤ) (X :=
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
    (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K sorry))
  (Y :=
  ObjectProperty.FullSubcategory.obj (P := CochainComplex.plus C)
    (ObjectProperty.FullSubcategory.mk (P := CochainComplex.plus C) K' sorry))
  (InducedCategory.Hom.hom (ObjectProperty.homMk (P := CochainComplex.plus C) i))
Tactic: rwa [← HomotopicalAlgebra.cofibration_iff, cofibration_iff, Plus.mono_iff]
-- 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) ⋯
n m : ℤ
hnm : n + 1 = m
⊢ (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm ≫ p.f m = 0
have fac_right : ∀ (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
-- 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) ⋯
n m : ℤ
hnm : n + 1 = m
⊢ i.f n ≫ (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm = 0
have fac_left : ∀ (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
-- 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ι)
n m : ℤ
hnm : n + 1 = m
⊢ ∃ (φ : Q.X n ⟶ K.X m), π.f n ≫ φ ≫ ι.f m = (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm
have this : Epi π
Tactic: have : Epi π := Cofork.IsColimit.epi hQ
-- 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ι)
n m : ℤ
hnm : n + 1 = m
this : Epi π
⊢ ∃ (φ : Q.X n ⟶ K.X m), π.f n ≫ φ ≫ ι.f m = (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm
have 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
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)
-- 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ι)
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
⊢ ∃ (φ : Q.X n ⟶ K.X m), π.f n ≫ φ ≫ ι.f m = (↑(cocycle₁' sq hsq) : Cochain B X 1).v n m hnm
have 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
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])
-- 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ι)
⊢ Eq (α := Cochain Q K 2) (δ 1 2 (cochain₁ sq hsq hQ hK)) 0
have this : Epi π
Tactic: have : Epi π := Cofork.IsColimit.epi hQ
-- 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 : Epi π
⊢ Eq (α := Cochain Q K 2) (δ 1 2 (cochain₁ sq hsq hQ hK)) 0
have this₁ : Mono ι
Tactic: have : Mono ι := Fork.IsLimit.mono hK
-- 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 : Mono ι
⊢ Eq (α := Cochain Q K 2) (δ 1 2 (cochain₁ sq hsq hQ hK)) 0
have h : ∀ (n : ℤ), Cochain.v (δ 1 2 (cochain₁ sq hsq hQ hK)) n (n + 2) sorry = Cochain.v 0 n (n + 2) sorry
Tactic: ext n _ rfl