awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
dsimp :
  f.f (c.next i) =
    (if c.Rel i (c.next i) then
          CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
            (ho.hom (c.next (c.next i)) (c.next i))
        else
          HSub.hSub (α := K.X (c.next i) ⟶ L.X (c.next i)) (f.f (c.next i)) (g.f (c.next i)) -
            ho.hom (c.next i) i ≫ L.d i (c.next i)) +
        ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)
⊢ ShortComplex.Hom.τ₃ (CategoryTheory.Functor.map (shortComplexFunctor C c i) f) =
    (if c.Rel i (c.next i) then
          CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
            (ho.hom (c.next (c.next i)) (c.next i))
        else
          HSub.hSub (α := K.X (c.next i) ⟶ L.X (c.next i)) (f.f (c.next i)) (g.f (c.next i)) -
            ho.hom (c.next i) i ≫ L.d i (c.next i)) +
        ho.hom (c.next i) i ≫ (Functor.obj (shortComplexFunctor C c i) L).g +
      ShortComplex.Hom.τ₃ (CategoryTheory.Functor.map (shortComplexFunctor C c i) g)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
pos :
  ∀ (h : c.Rel i (c.next i)),
    f.f (c.next i) =
      HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
          (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
            (ho.hom (c.next (c.next i)) (c.next i)))
          (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
        g.f (c.next i)
neg :
  ∀ (h : ¬c.Rel i (c.next i)),
    f.f (c.next i) =
      HSub.hSub (α := K.X (c.next i) ⟶ L.X (c.next i)) (f.f (c.next i)) (g.f (c.next i)) -
            ho.hom (c.next i) i ≫ L.d i (c.next i) +
          ho.hom (c.next i) i ≫ L.d i (c.next i) +
        g.f (c.next i)
⊢ f.f (c.next i) =
    (if c.Rel i (c.next i) then
          CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
            (ho.hom (c.next (c.next i)) (c.next i))
        else
          HSub.hSub (α := K.X (c.next i) ⟶ L.X (c.next i)) (f.f (c.next i)) (g.f (c.next i)) -
            ho.hom (c.next i) i ≫ L.d i (c.next i)) +
        ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)

Tactic:
split_ifs with h
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel i (c.next i)
pos :
  HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i)) (β := K.X (c.next i) ⟶ L.X (c.next i))
        ((dNext (c.next i) : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X (c.next i) ⟶ L.X (c.next i)) ho.hom :
          K.X (c.next i) ⟶ L.X (c.next i))
        ((prevD (c.next i) : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X (c.next i) ⟶ L.X (c.next i)) ho.hom :
          K.X (c.next i) ⟶ L.X (c.next i)) +
      g.f (c.next i) =
    HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
        (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
      g.f (c.next i)
⊢ f.f (c.next i) =
    HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
        (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
      g.f (c.next i)

Tactic:
rw [ho.comm (c.next i)]

Premises used: ComplexShape.next, Homotopy.comm
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel i (c.next i)
pos :
  HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (CategoryStruct.comp (Y := K.xNext (c.next i)) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
        (CategoryStruct.comp (Y := L.xPrev (c.next i)) (ho.hom (c.next i) (c.prev (c.next i)))
          (L.d (c.prev (c.next i)) (c.next i))) +
      g.f (c.next i) =
    HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
        (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
      g.f (c.next i)
⊢ HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i)) (β := K.X (c.next i) ⟶ L.X (c.next i))
        ((dNext (c.next i) : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X (c.next i) ⟶ L.X (c.next i)) ho.hom :
          K.X (c.next i) ⟶ L.X (c.next i))
        ((prevD (c.next i) : (a : (i j : ι) → K.X i ⟶ L.X j) → K.X (c.next i) ⟶ L.X (c.next i)) ho.hom :
          K.X (c.next i) ⟶ L.X (c.next i)) +
      g.f (c.next i) =
    HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
        (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
      g.f (c.next i)

Tactic:
dsimp [dFrom, dTo, fromNext, toPrev]

Premises used: fromNext, HomologicalComplex.dTo, HomologicalComplex.dFrom, toPrev
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel i (c.next i)
pos pos₁ :
  HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (CategoryStruct.comp (Y := K.xNext (c.next i)) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
        (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
      g.f (c.next i) =
    HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
        (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
      g.f (c.next i)
⊢ HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (CategoryStruct.comp (Y := K.xNext (c.next i)) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
        (CategoryStruct.comp (Y := L.xPrev (c.next i)) (ho.hom (c.next i) (c.prev (c.next i)))
          (L.d (c.prev (c.next i)) (c.next i))) +
      g.f (c.next i) =
    HAdd.hAdd (α := K.X (c.next i) ⟶ L.X (c.next i))
        (CategoryStruct.comp (Y := K.X (c.next (c.next i))) (K.d (c.next i) (c.next (c.next i)))
          (ho.hom (c.next (c.next i)) (c.next i)))
        (ho.hom (c.next i) i ≫ L.d i (c.next i)) +
      g.f (c.next i)

Tactic:
rw [congr_arg (fun j => ho.hom (c.next i) j ≫ L.d j (c.next i)) (c.prev_eq' h)]

Premises used: Homotopy.hom, ComplexShape.prev_eq', congr_arg, ComplexShape.next, CategoryTheory.CategoryStruct.comp, HomologicalComplex.d
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : ¬c.Rel i (c.next i)
⊢ f.f (c.next i) =
    HSub.hSub (α := K.X (c.next i) ⟶ L.X (c.next i)) (f.f (c.next i)) (g.f (c.next i)) -
          ho.hom (c.next i) i ≫ L.d i (c.next i) +
        ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)

Tactic:
abel
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
C : Type u_2
inst : Category.{v_1, u_2} C
inst_1 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq (α := K.homology i ⟶ L.homology i) (homologyMap f i) (homologyMap g i)

Tactic:
open scoped Classical in ShortComplex.Homotopy.homologyMap_congr (ho.toShortComplex i)

Premises used: Homotopy.toShortComplex, HomologicalComplex.homologyMap, CategoryTheory.ShortComplex.Homotopy.homologyMap_congr, HomologicalComplex.homology
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst_5 : K.HasHomology i
inst_6 : L.HasHomology i
rw : homologyMap (h.hom ≫ h.inv) i = 𝟙 (K.homology i)
rw₁ : homologyMap (𝟙 K) i = 𝟙 (K.homology i)
rw₂ rw₃ : Eq.{v_1 + 1} (α := K.homology i ⟶ K.homology i) (𝟙 (K.homology i)) (𝟙 (K.homology i))
⊢ CategoryStruct.comp (Y := L.homology i) (homologyMap h.hom i) (homologyMap h.inv i) = 𝟙 (K.homology i)

Tactic:
rw [← homologyMap_comp, h.homotopyHomInvId.homologyMap_eq, homologyMap_id]

Premises used: Homotopy.homologyMap_eq, HomologicalComplex.homologyMap_id, HomologicalComplex.homologyMap_comp, HomotopyEquiv.homotopyHomInvId
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι_1 : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c_1 : ComplexShape ι_1
C_1 D E : HomologicalComplex.{v, u, u_1} V c_1
f_1 g_1 : C_1 ⟶ D
h_1 k : D ⟶ E
i_1 : ι_1
C : Type u_2
inst_2 : Category.{v_1, u_2} C
inst_3 : Preadditive.{v_1, u_2} C
ι : Type u_3
c : ComplexShape ι
inst_4 : DecidableRel c.Rel
K L : HomologicalComplex.{v_1, u_2, u_3} C c
f g : K ⟶ L
h : HomotopyEquiv K L
i : ι
inst_5 : K.HasHomology i
inst_6 : L.HasHomology i
rw : homologyMap (h.inv ≫ h.hom) i = 𝟙 (L.homology i)
rw₁ : homologyMap (𝟙 L) i = 𝟙 (L.homology i)
rw₂ rw₃ : Eq.{v_1 + 1} (α := L.homology i ⟶ L.homology i) (𝟙 (L.homology i)) (𝟙 (L.homology i))
⊢ CategoryStruct.comp (Y := K.homology i) (homologyMap h.inv i) (homologyMap h.hom i) = 𝟙 (L.homology i)

Tactic:
rw [← homologyMap_comp, h.homotopyInvHomId.homologyMap_eq, homologyMap_id]

Premises used: Homotopy.homologyMap_eq, HomologicalComplex.homologyMap_id, HomotopyEquiv.homotopyInvHomId, HomologicalComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ ObjectProperty.IsTriangulated (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (Functor.homologicalKernel (homologyFunctor C (ComplexShape.up ℤ) 0))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ ObjectProperty.IsClosedUnderIsomorphisms (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (Functor.homologicalKernel (homologyFunctor C (ComplexShape.up ℤ) 0))

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
⊢ subcategoryAcyclic C X ↔ ∀ (n : ℤ), IsZero.{v, u} (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) X)

Tactic:
Functor.mem_homologicalKernel_iff _ X

Premises used: CategoryTheory.Functor.mem_homologicalKernel_iff, HomotopyCategory.subcategoryAcyclic
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
rw :
  (∀ (n : ℤ),
      IsZero.{v, u}
        (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) (Functor.obj (quotient C (ComplexShape.up ℤ)) K))) ↔
    ∀ (n : ℤ), HomologicalComplex.ExactAt K n
⊢ subcategoryAcyclic C (Functor.obj (quotient C (ComplexShape.up ℤ)) K) ↔ ∀ (n : ℤ), HomologicalComplex.ExactAt K n

Tactic:
rw [mem_subcategoryAcyclic_iff]

Premises used: HomotopyCategory.mem_subcategoryAcyclic_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
⊢ (∀ (n : ℤ),
      IsZero.{v, u}
        (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) (Functor.obj (quotient C (ComplexShape.up ℤ)) K))) ↔
    ∀ (n : ℤ), HomologicalComplex.ExactAt K n

Tactic:
forall_congr' (fun n => ?_)

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
refine :
  ∀ (n : ℤ),
    IsZero.{v, u}
        (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) (Functor.obj (quotient C (ComplexShape.up ℤ)) K)) ↔
      HomologicalComplex.ExactAt K n
⊢ (∀ (n : ℤ),
      IsZero.{v, u}
        (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) (Functor.obj (quotient C (ComplexShape.up ℤ)) K))) ↔
    ∀ (n : ℤ), HomologicalComplex.ExactAt K n

Tactic:
refine forall_congr' (fun n => ?_)

Premises used: forall_congr'
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
simp :
  IsZero.{v, u}
      (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) (Functor.obj (quotient C (ComplexShape.up ℤ)) K)) ↔
    IsZero.{v, u} (HomologicalComplex.homology K n)
⊢ IsZero.{v, u}
      (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) (Functor.obj (quotient C (ComplexShape.up ℤ)) K)) ↔
    HomologicalComplex.ExactAt K n

Tactic:
simp only [HomologicalComplex.exactAt_iff_isZero_homology]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ IsZero.{v, u}
      (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) (Functor.obj (quotient C (ComplexShape.up ℤ)) K)) ↔
    IsZero.{v, u} (HomologicalComplex.homology K n)

Tactic:
((homologyFunctorFactors C (ComplexShape.up ℤ) n).app K).isZero_iff

Premises used: HomotopyCategory.homologyFunctorFactors, Int, CategoryTheory.ShortComplex.homology, CategoryTheory.Iso.isZero_iff, CategoryTheory.Iso.app, HomologicalComplex.homology, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
n : ℤ
⊢ IsZero.{v, u}
      (Functor.obj (homologyFunctor C (ComplexShape.up ℤ) n) (Functor.obj (quotient C (ComplexShape.up ℤ)) K)) ↔
    IsZero.{v, u} (HomologicalComplex.homology K n)

Tactic:
exact ((homologyFunctorFactors C (ComplexShape.up ℤ) n).app K).isZero_iff

Premises used: HomotopyCategory.homologyFunctorFactors, Int, CategoryTheory.Iso.isZero_iff, CategoryTheory.Iso.app, ComplexShape.up
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K : CochainComplex.{v, u, 0} C ℤ
⊢ subcategoryAcyclic C (Functor.obj (quotient C (ComplexShape.up ℤ)) K) ↔ HomologicalComplex.Acyclic K

Tactic:
quotient_obj_mem_subcategoryAcyclic_iff_exactAt _

Premises used: HomologicalComplex.Acyclic, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
h :
  ∀ ⦃K L : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)⦄ (f : K ⟶ L),
    quasiIso C (ComplexShape.up ℤ) f ↔ ObjectProperty.trW (subcategoryAcyclic C) f
⊢ Eq (α := MorphismProperty (HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))) (quasiIso C (ComplexShape.up ℤ))
    (ObjectProperty.trW (subcategoryAcyclic C))

Tactic:
ext K L f
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
f : K ⟶ L
⊢ quasiIso C (ComplexShape.up ℤ) f ↔ ObjectProperty.trW (subcategoryAcyclic C) f

Tactic:
((homologyFunctor C (ComplexShape.up ℤ) 0).mem_homologicalKernel_trW_iff f).symm

Premises used: Int, HomotopyCategory.quasiIso, HomotopyCategory.subcategoryAcyclic, HomotopyCategory.homologyFunctor, OfNat.ofNat, Iff.symm, ComplexShape.up, CategoryTheory.Functor.mem_homologicalKernel_trW_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
K L : HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ)
f : K ⟶ L
⊢ quasiIso C (ComplexShape.up ℤ) f ↔ ObjectProperty.trW (subcategoryAcyclic C) f

Tactic:
exact ((homologyFunctor C (ComplexShape.up ℤ) 0).mem_homologicalKernel_trW_iff f).symm

Premises used: Int, HomotopyCategory.homologyFunctor, OfNat.ofNat, Iff.symm, ComplexShape.up, CategoryTheory.Functor.mem_homologicalKernel_trW_iff
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
rw :
  MorphismProperty.IsCompatibleWithShift (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (ObjectProperty.trW (subcategoryAcyclic C)) ℤ
⊢ MorphismProperty.IsCompatibleWithShift (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (quasiIso C (ComplexShape.up ℤ)) ℤ

Tactic:
rw [quasiIso_eq_trW_subcategoryAcyclic]

Premises used: HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
⊢ MorphismProperty.IsCompatibleWithShift (C := HomotopyCategory.{v, u, 0} C (ComplexShape.up ℤ))
    (ObjectProperty.trW (subcategoryAcyclic C)) ℤ

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
⊢ HAdd.hAdd (α := ℤ) 1 1 = 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
h :
  ∀ (p : ℤ),
    Eq.{v + 1} (α := S.X₃.X p ⟶ S.X₁.X (p + 2))
      (Cochain.v (δ 1 2 (Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)) p (p + 2) ⋯)
      (Cochain.v 0 p (p + 2) ⋯)
⊢ Eq.{v + 1} (α := Cochain S.X₃ S.X₁ 2)
    (δ 1 2 (Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)) 0

Tactic:
ext p _ rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
p : ℤ
⊢ Mono (X := ShortComplex.X₁ (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
    (ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 2))))

Tactic:
have := mono_of_mono_fac (σ (p + 2)).f_r
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
p : ℤ
this :
  Mono (X := ShortComplex.X₁ (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
    (ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
⊢ ∀ (n : ℤ),
    (σ n).r ≫ ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) n)) =
      𝟙 (ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) n))) -
        ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) n)) ≫ (σ n).s

Tactic:
have r_f := fun n => (σ n).r_f
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
p : ℤ
this :
  Mono (X := ShortComplex.X₁ (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
    (ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
r_f :
  ∀ (n : ℤ),
    (σ n).r ≫ ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) n)) =
      𝟙 (ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) n))) -
        ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) n)) ≫ (σ n).s
⊢ ∀ (n : ℤ),
    (σ n).s ≫ ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) n)) =
      𝟙 (ShortComplex.X₃ (S.map (eval C (ComplexShape.up ℤ) n)))

Tactic:
have s_g := fun n => (σ n).s_g
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
p : ℤ
this :
  Mono (X := ShortComplex.X₁ (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
    (ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) (p + 2))))
r_f :
  ∀ (n : ℤ),
    (σ n).r ≫ ShortComplex.f (S.map (eval C (ComplexShape.up ℤ) n)) =
      𝟙 (ShortComplex.X₂ (S.map (eval C (ComplexShape.up ℤ) n))) -
        ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) n)) ≫ (σ n).s
s_g :
  ∀ (n : ℤ),
    (σ n).s ≫ ShortComplex.g (S.map (eval C (ComplexShape.up ℤ) n)) =
      𝟙 (ShortComplex.X₃ (S.map (eval C (ComplexShape.up ℤ) n)))
h :
  Eq.{v + 1} (α := S.X₃.X p ⟶ S.X₁.X (p + 2))
    (Cochain.v (δ 1 2 (Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)) p (p + 2) ⋯) 0
⊢ Eq.{v + 1} (α := S.X₃.X p ⟶ S.X₁.X (p + 2))
    (Cochain.v (δ 1 2 (Cochain.mk fun (p q : ℤ) (x : p + 1 = q) ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)) p (p + 2) ⋯)
    (Cochain.v 0 p (p + 2) ⋯)

Tactic:
dsimp at this r_f s_g ⊢
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
p : ℤ
this : Mono (X := S.X₁.X (p + 2)) (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ HAdd.hAdd (α := ℤ) 1 1 = 2

Tactic:
lia
-- Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
Goal:
C : Type u_1
inst : Category.{v, u_1} C
inst_1 : Preadditive.{v, u_1} C
S : ShortComplex (CochainComplex.{v, u_1, 0} C ℤ)
σ : (n : ℤ) → ShortComplex.Splitting (S.map (eval C (ComplexShape.up ℤ) n))
p : ℤ
this : Mono (X := S.X₁.X (p + 2)) (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ p + 2 = p + 2

Tactic:
lia