awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
⊢ Eq.{v_1 + 1} (α := colimit (F ⋙ eval C c n) ⟶ colimit (F ⋙ eval C c m))
    (colimMap { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ }) 0
have w : ∀ (j : J),
  Eq (α := (F ⋙ eval C c n).obj j ⟶ colimit (F ⋙ eval C c m))
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j)
      (colimMap { app := fun (j : J) ↦ (F.obj j).d n m, naturality := sorry }))
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
Tactic: ext j
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
⊢ Eq (α := (F ⋙ eval C c n).obj j ⟶ colimit (F ⋙ eval C c m))
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j)
      (colimMap { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ }))
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
have w : Eq (α := (F ⋙ eval C c n).obj j ⟶ colimit (F ⋙ eval C c m))
  (NatTrans.app { app := fun (j : J) ↦ (F.obj j).d n m, naturality := sorry } j ≫ colimit.ι (F ⋙ eval C c m) j)
  (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
Tactic: rw [ι_colimMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
⊢ Eq (α := (F ⋙ eval C c n).obj j ⟶ colimit (F ⋙ eval C c m))
    (NatTrans.app { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ } j ≫ colimit.ι (F ⋙ eval C c m) j)
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
have w : Eq (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) ((F.obj j).d n m ≫ colimit.ι (F ⋙ eval C c m) j)
  (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
⊢ Eq (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) ((F.obj j).d n m ≫ colimit.ι (F ⋙ eval C c m) j)
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
have w : Eq (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) (0 ≫ colimit.ι (F ⋙ eval C c m) j)
  (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
Tactic: rw [(F.obj j).shape _ _ h, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
w :
  Eq (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) (0 ≫ colimit.ι (F ⋙ eval C c m) j)
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
⊢ Eq (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) ((F.obj j).d n m ≫ colimit.ι (F ⋙ eval C c m) j)
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
have w₁ : Eq (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) 0
  (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
Tactic: rw [(F.obj j).shape _ _ h, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
n m : ι
h : ¬c.Rel n m
j : J
w :
  Eq (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) (0 ≫ colimit.ι (F ⋙ eval C c m) j)
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
w₁ :
  Eq (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) 0
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
⊢ Eq (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) ((F.obj j).d n m ≫ colimit.ι (F ⋙ eval C c m) j)
    (CategoryStruct.comp (Y := colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) j) 0)
have w₂ : Eq.{v_1 + 1} (α := (F.obj j).X n ⟶ colimit (F ⋙ eval C c m)) 0 0
Tactic: rw [(F.obj j).shape _ _ h, zero_comp, comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
⊢ Eq (α :=
    F.obj i ⟶
      Functor.obj
        (Functor.obj (Functor.const J)
          { X := fun (n : ι) ↦ colimit (F ⋙ eval C c n),
            d := fun (n m : ι) ↦
              colimMap
                { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ : NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
            shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v_1, u_1, u_2} C c })
        j)
    (F.map φ ≫ { f := fun (n : ι) ↦ colimit.ι (F ⋙ eval C c n) j, comm' := ⋯ })
    ({ f := fun (n : ι) ↦ colimit.ι (F ⋙ eval C c n) i, comm' := ⋯ } ≫
      CategoryTheory.Functor.map
        (Functor.obj (Functor.const J)
          { X := fun (n : ι) ↦ colimit (F ⋙ eval C c n),
            d := fun (n m : ι) ↦
              colimMap
                { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ : NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
            shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v_1, u_1, u_2} C c })
        φ)
have h : ∀ (n : ι),
  Eq (α :=
    (F.obj i).X n ⟶
      (Functor.obj
            (Functor.obj (Functor.const J)
              { X := fun (n : ι) ↦ colimit (F ⋙ eval C c n),
                d := fun (n m : ι) ↦
                  colimMap
                    { app := fun (j : J) ↦ (F.obj j).d n m, naturality := sorry :
                      NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
                shape := sorry, d_comp_d' := sorry : HomologicalComplex.{v_1, u_1, u_2} C c })
            j).X
        n)
    (Hom.f (F.map φ ≫ { f := fun (n : ι) ↦ colimit.ι (F ⋙ eval C c n) j, comm' := sorry }) n)
    (Hom.f
      ({ f := fun (n : ι) ↦ colimit.ι (F ⋙ eval C c n) i, comm' := sorry } ≫
        CategoryTheory.Functor.map
          (Functor.obj (Functor.const J)
            { X := fun (n : ι) ↦ colimit (F ⋙ eval C c n),
              d := fun (n m : ι) ↦
                colimMap
                  { app := fun (j : J) ↦ (F.obj j).d n m, naturality := sorry :
                    NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
              shape := sorry, d_comp_d' := sorry : HomologicalComplex.{v_1, u_1, u_2} C c })
          φ)
      n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
n : ι
⊢ Eq (α :=
    (F.obj i).X n ⟶
      (Functor.obj
            (Functor.obj (Functor.const J)
              { X := fun (n : ι) ↦ colimit (F ⋙ eval C c n),
                d := fun (n m : ι) ↦
                  colimMap
                    { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ :
                      NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
                shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v_1, u_1, u_2} C c })
            j).X
        n)
    (Hom.f (F.map φ ≫ { f := fun (n : ι) ↦ colimit.ι (F ⋙ eval C c n) j, comm' := ⋯ }) n)
    (Hom.f
      ({ f := fun (n : ι) ↦ colimit.ι (F ⋙ eval C c n) i, comm' := ⋯ } ≫
        CategoryTheory.Functor.map
          (Functor.obj (Functor.const J)
            { X := fun (n : ι) ↦ colimit (F ⋙ eval C c n),
              d := fun (n m : ι) ↦
                colimMap
                  { app := fun (j : J) ↦ (F.obj j).d n m, naturality := ⋯ :
                    NatTrans (F ⋙ eval C c n) (F ⋙ eval C c m) },
              shape := ⋯, d_comp_d' := ⋯ : HomologicalComplex.{v_1, u_1, u_2} C c })
          φ)
      n)
have h : (F.map φ).f n ≫ colimit.ι (F ⋙ eval C c n) j = colimit.ι (F ⋙ eval C c n) i ≫ 𝟙 (colimit (F ⋙ eval C c n))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
n : ι
⊢ (F.map φ).f n ≫ colimit.ι (F ⋙ eval C c n) j = colimit.ι (F ⋙ eval C c n) i ≫ 𝟙 (colimit (F ⋙ eval C c n))
have h : Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n)) ((F.map φ).f n ≫ colimit.ι (F ⋙ eval C c n) j)
  (colimit.ι (F ⋙ eval C c n) i)
Tactic: simp only [Category.comp_id]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
n : ι
⊢ Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n)) ((F.map φ).f n ≫ colimit.ι (F ⋙ eval C c n) j)
    (colimit.ι (F ⋙ eval C c n) i)
have h : Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n))
  (CategoryTheory.Functor.map (eval C c n) (F.map φ) ≫ colimit.ι (F ⋙ eval C c n) j :
    (F.obj i).X n ⟶ colimit (F ⋙ eval C c n))
  (colimit.ι (F ⋙ eval C c n) i : (F ⋙ eval C c n).obj i ⟶ colimit (F ⋙ eval C c n))
Tactic: rw [← eval_map, ← Functor.comp_map, colimit.w]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
n : ι
h :
  Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n))
    (CategoryTheory.Functor.map (eval C c n) (F.map φ) ≫ colimit.ι (F ⋙ eval C c n) j :
      (F.obj i).X n ⟶ colimit (F ⋙ eval C c n))
    (colimit.ι (F ⋙ eval C c n) i : (F ⋙ eval C c n).obj i ⟶ colimit (F ⋙ eval C c n))
⊢ Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n)) ((F.map φ).f n ≫ colimit.ι (F ⋙ eval C c n) j)
    (colimit.ι (F ⋙ eval C c n) i)
have h₁ : Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n)) ((F ⋙ eval C c n).map φ ≫ colimit.ι (F ⋙ eval C c n) j)
  (colimit.ι (F ⋙ eval C c n) i)
Tactic: rw [← eval_map, ← Functor.comp_map, colimit.w]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
F : J ⥤ HomologicalComplex.{v_1, u_1, u_2} C c
inst_3 : ∀ (n : ι), HasColimit (F ⋙ eval C c n)
i j : J
φ : i ⟶ j
n : ι
h :
  Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n))
    (CategoryTheory.Functor.map (eval C c n) (F.map φ) ≫ colimit.ι (F ⋙ eval C c n) j :
      (F.obj i).X n ⟶ colimit (F ⋙ eval C c n))
    (colimit.ι (F ⋙ eval C c n) i : (F ⋙ eval C c n).obj i ⟶ colimit (F ⋙ eval C c n))
h₁ :
  Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n)) ((F ⋙ eval C c n).map φ ≫ colimit.ι (F ⋙ eval C c n) j)
    (colimit.ι (F ⋙ eval C c n) i)
⊢ Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n)) ((F.map φ).f n ≫ colimit.ι (F ⋙ eval C c n) j)
    (colimit.ι (F ⋙ eval C c n) i)
have h₂ : Eq (α := (F.obj i).X n ⟶ colimit (F ⋙ eval C c n)) (colimit.ι (F ⋙ eval C c n) i) (colimit.ι (F ⋙ eval C c n) i)
Tactic: rw [← eval_map, ← Functor.comp_map, colimit.w]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasFiniteColimits.{v_1, u_1} C
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
inst_4 : Epi φ
n : ι
⊢ Epi (φ.f n)
have change : Epi (X := Functor.obj (eval C c n) K) (CategoryTheory.Functor.map (eval C c n) φ)
Tactic: change Epi ((HomologicalComplex.eval C c n).map φ)
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
i j : ι
⊢ PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
have pos : ∀ (h : j = i),
  PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
i j : ι
pos :
  ∀ (h : j = i),
    PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
      (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
⊢ PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
have neg : ∀ (h : ¬j = i),
  PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
i j : ι
h : j = i
⊢ PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
have pos : PreservesLimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
  (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c j) (eval C c j))
Tactic: subst h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
i j : ι
⊢ PreservesColimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
have pos : ∀ (h : j = i),
  PreservesColimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
i j : ι
pos :
  ∀ (h : j = i),
    PreservesColimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
      (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
⊢ PreservesColimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
have neg : ∀ (h : ¬j = i),
  PreservesColimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
Tactic: by_cases h : j = i
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimits (goal)
Goal:
C : Type u_1
ι : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_3} J
c : ComplexShape ι
inst_2 : HasZeroMorphisms.{v_1, u_1} C
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : DecidableEq ι
i j : ι
h : j = i
⊢ PreservesColimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
    (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c i) (eval C c j))
have pos : PreservesColimitsOfShape.{v_2, u_3, v_1, v_1, u_1, u_1} J
  (Functor.comp (D := HomologicalComplex.{v_1, u_1, u_2} C c) (single C c j) (eval C c j))
Tactic: subst h
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant (goal)
Goal:
C : Type u_1
J : Type u_2
ι : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_5, u_2} J
c : ComplexShape ι
inst_2 : IsCofiltered.{u_5, u_2} J
inst_3 : HasZeroMorphisms.{u_4, u_1} C
F : J ⥤ HomologicalComplex.{u_4, u_1, u_3} C c
inst_4 : ∀ (j : ι), HasLimit (F ⋙ eval C c j)
cF : Cone F
hcF : IsLimit cF
inst_5 : CategoryWithHomology.{u_4, u_1} C
q₀ q₁ q₂ : ι
h₀ : c.prev q₁ = q₀
h₂ : c.next q₁ = q₂
j : J
hq₀ : (F ⋙ eval C c q₀).IsEventuallyConstantTo j
hq₁ : (F ⋙ eval C c q₁).IsEventuallyConstantTo j
hq₂ : (F ⋙ eval C c q₂).IsEventuallyConstantTo j
⊢ QuasiIsoAt (cF.π.app j) q₁
have rw : ShortComplex.QuasiIso (S₁ :=
  Functor.obj (shortComplexFunctor' C c q₀ q₁ q₂) (Functor.obj (Functor.obj (Functor.const J) cF.pt) j))
  (CategoryTheory.Functor.map (shortComplexFunctor' C c q₀ q₁ q₂) (cF.π.app j))
Tactic: rw [quasiIsoAt_iff' _ q₀ q₁ q₂ h₀ h₂]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant (hypothesis)
Goal:
C : Type u_1
J : Type u_2
ι : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_5, u_2} J
c : ComplexShape ι
inst_2 : IsCofiltered.{u_5, u_2} J
inst_3 : HasZeroMorphisms.{u_4, u_1} C
F : J ⥤ HomologicalComplex.{u_4, u_1, u_3} C c
inst_4 : ∀ (j : ι), HasLimit (F ⋙ eval C c j)
cF : Cone F
hcF : IsLimit cF
inst_5 : CategoryWithHomology.{u_4, u_1} C
q₀ q₁ q₂ : ι
h₀ : c.prev q₁ = q₀
h₂ : c.next q₁ = q₂
j : J
hq₀ : (F ⋙ eval C c q₀).IsEventuallyConstantTo j
hq₁ : (F ⋙ eval C c q₁).IsEventuallyConstantTo j
hq₂ : (F ⋙ eval C c q₂).IsEventuallyConstantTo j
φ : Functor.obj (shortComplexFunctor' C c q₀ q₁ q₂) (Functor.obj (Functor.obj (Functor.const J) cF.pt) j) ⟶
  Functor.obj (shortComplexFunctor' C c q₀ q₁ q₂) (F.obj j) :=
  CategoryTheory.Functor.map (shortComplexFunctor' C c q₀ q₁ q₂) (cF.π.app j)
⊢ ShortComplex.QuasiIso (S₁ :=
    Functor.obj (shortComplexFunctor' C c q₀ q₁ q₂) (Functor.obj (Functor.obj (Functor.const J) cF.pt) j))
    (CategoryTheory.Functor.map (shortComplexFunctor' C c q₀ q₁ q₂) (cF.π.app j))
have this : IsIso φ.τ₁
Tactic: have : IsIso φ.τ₁ := isIso_π_f_of_isLimit_of_isEventuallyConstantTo F hcF _ _ hq₀
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant (hypothesis)
Goal:
C : Type u_1
J : Type u_2
ι : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_5, u_2} J
c : ComplexShape ι
inst_2 : IsCofiltered.{u_5, u_2} J
inst_3 : HasZeroMorphisms.{u_4, u_1} C
F : J ⥤ HomologicalComplex.{u_4, u_1, u_3} C c
inst_4 : ∀ (j : ι), HasLimit (F ⋙ eval C c j)
cF : Cone F
hcF : IsLimit cF
inst_5 : CategoryWithHomology.{u_4, u_1} C
q₀ q₁ q₂ : ι
h₀ : c.prev q₁ = q₀
h₂ : c.next q₁ = q₂
j : J
hq₀ : (F ⋙ eval C c q₀).IsEventuallyConstantTo j
hq₁ : (F ⋙ eval C c q₁).IsEventuallyConstantTo j
hq₂ : (F ⋙ eval C c q₂).IsEventuallyConstantTo j
φ : Functor.obj (shortComplexFunctor' C c q₀ q₁ q₂) (Functor.obj (Functor.obj (Functor.const J) cF.pt) j) ⟶
  Functor.obj (shortComplexFunctor' C c q₀ q₁ q₂) (F.obj j) :=
  CategoryTheory.Functor.map (shortComplexFunctor' C c q₀ q₁ q₂) (cF.π.app j)
this : IsIso φ.τ₁
⊢ ShortComplex.QuasiIso (S₁ :=
    Functor.obj (shortComplexFunctor' C c q₀ q₁ q₂) (Functor.obj (Functor.obj (Functor.const J) cF.pt) j))
    (CategoryTheory.Functor.map (shortComplexFunctor' C c q₀ q₁ q₂) (cF.π.app j))
have this₁ : IsIso φ.τ₂
Tactic: have : IsIso φ.τ₂ := isIso_π_f_of_isLimit_of_isEventuallyConstantTo F hcF _ _ hq₁
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant (hypothesis)
Goal:
C : Type u_1
J : Type u_2
ι : Type u_3
inst : Category.{u_4, u_1} C
inst_1 : Category.{u_5, u_2} J
c : ComplexShape ι
inst_2 : IsCofiltered.{u_5, u_2} J
inst_3 : HasZeroMorphisms.{u_4, u_1} C
F : J ⥤ HomologicalComplex.{u_4, u_1, u_3} C c
inst_4 : ∀ (j : ι), HasLimit (F ⋙ eval C c j)
cF : Cone F
hcF : IsLimit cF
inst_5 : CategoryWithHomology.{u_4, u_1} C
q₀ q₁ q₂ : ι
h₀ : c.prev q₁ = q₀
h₂ : c.next q₁ = q₂
j : J
hq₀ : (F ⋙ eval C c q₀).IsEventuallyConstantTo j
hq₁ : (F ⋙ eval C c q₁).IsEventuallyConstantTo j
hq₂ : (F ⋙ eval C c q₂).IsEventuallyConstantTo j
φ : Functor.obj (shortComplexFunctor' C c q₀ q₁ q₂) (Functor.obj (Functor.obj (Functor.const J) cF.pt) j) ⟶
  Functor.obj (shortComplexFunctor' C c q₀ q₁ q₂) (F.obj j) :=
  CategoryTheory.Functor.map (shortComplexFunctor' C c q₀ q₁ q₂) (cF.π.app j)
this_1 : IsIso φ.τ₁
this : IsIso φ.τ₂
⊢ ShortComplex.QuasiIso (S₁ :=
    Functor.obj (shortComplexFunctor' C c q₀ q₁ q₂) (Functor.obj (Functor.obj (Functor.const J) cF.pt) j))
    (CategoryTheory.Functor.map (shortComplexFunctor' C c q₀ q₁ q₂) (cF.π.app j))
have this₁ : IsIso φ.τ₃
Tactic: have : IsIso φ.τ₃ := isIso_π_f_of_isLimit_of_isEventuallyConstantTo F hcF _ _ hq₂
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
inst_2 : K.HasHomology i
inst_3 : K.HasHomology j
⊢ Eq (α := K.opcycles i ⟶ K.X j) (CategoryStruct.comp (Y := K.cycles j) (K.opcyclesToCycles i j) (K.iCycles j))
    (K.fromOpcycles i j)
have dsimp : Eq (α := K.opcycles i ⟶ K.X j)
  (CategoryStruct.comp (Y := K.cycles j) (K.liftCycles (K.fromOpcycles i j) (c.next j) sorry sorry) (K.iCycles j))
  (K.fromOpcycles i j)
Tactic: dsimp only [opcyclesToCycles]
-- Lean 4 proof step from Mathlib.Algebra.Homology.HomologySequence (goal)
Goal:
C : Type u_1
ι : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hij : c.Rel i j
inst_2 : K.HasHomology i
inst_3 : K.HasHomology j
⊢ Mono
    ((composableArrows₃ K i j).map' 0 1 instMonoMap'ComposableArrows₃OfNatNat._proof_1
      instMonoMap'ComposableArrows₃OfNatNat._proof_3)
have dsimp : Mono (X := K.homology i) (K.homologyι i)
Tactic: dsimp