awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
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 ι
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 j) (eval C c j))

Tactic:
preservesColimitsOfShape_of_natIso (singleCompEvalIsoSelf C c j).symm

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_natIso, CategoryTheory.Iso.symm, HomologicalComplex.singleCompEvalIsoSelf
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
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 ι
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 j) (eval C c j))

Tactic:
exact preservesColimitsOfShape_of_natIso (singleCompEvalIsoSelf C c j).symm

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_natIso, CategoryTheory.Iso.symm, HomologicalComplex.singleCompEvalIsoSelf
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
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))

Tactic:
Functor.preservesColimitsOfShape_of_isZero _ (isZero_single_comp_eval C c _ _ h) _

Premises used: CategoryTheory.Functor.preservesColimitsOfShape_of_isZero, HomologicalComplex.isZero_single_comp_eval
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
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))

Tactic:
exact Functor.preservesColimitsOfShape_of_isZero _ (isZero_single_comp_eval C c _ _ h) _

Premises used: CategoryTheory.Functor.preservesColimitsOfShape_of_isZero, HomologicalComplex.isZero_single_comp_eval
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
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_1 : Type
inst_5 : SmallCategory J_1
inst_6 : FinCategory J_1
⊢ PreservesLimitsOfShape (D := HomologicalComplex.{v_1, u_1, u_2} C c) J_1 (single C c i)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimits
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_1 : Type
inst_5 : SmallCategory J_1
inst_6 : FinCategory J_1
⊢ PreservesColimitsOfShape (D := HomologicalComplex.{v_1, u_1, u_2} C c) J_1 (single C c i)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant
Goal:
C : Type u_1
J : Type u_2
ι : Type u_3
inst : Category.{u_5, u_1} C
inst_1 : Category.{u_4, u_2} J
c : ComplexShape ι
inst_2 : IsCofiltered.{u_4, u_2} J
inst_3 : HasZeroMorphisms.{u_5, u_1} C
F : J ⥤ HomologicalComplex.{u_5, u_1, u_3} C c
inst_4 : ∀ (j : ι), HasLimit (F ⋙ eval C c j)
cF : Cone F
hcF : IsLimit cF
q : ι
j : J
hq : (F ⋙ eval C c q).IsEventuallyConstantTo j
⊢ IsIso ((cF.π.app j).f q)

Tactic:
hq.isIso_π_of_isLimit (isLimitOfPreserves (eval C c q) hcF)

Premises used: HomologicalComplex.eval, CategoryTheory.Functor.IsEventuallyConstantTo.isIso_π_of_isLimit, CategoryTheory.Limits.isLimitOfPreserves
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant
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
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))
⊢ QuasiIsoAt (cF.π.app j) q₁

Tactic:
rw [quasiIsoAt_iff' _ q₀ q₁ q₂ h₀ h₂]

Premises used: quasiIsoAt_iff'
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant
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)
⊢ IsIso φ.τ₁

Tactic:
have : IsIso φ.τ₁ := isIso_π_f_of_isLimit_of_isEventuallyConstantTo F hcF _ _ hq₀
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant
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 φ.τ₁
⊢ IsIso φ.τ₂

Tactic:
have : IsIso φ.τ₂ := isIso_π_f_of_isLimit_of_isEventuallyConstantTo F hcF _ _ hq₁
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant
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 φ.τ₂
⊢ IsIso φ.τ₃

Tactic:
have : IsIso φ.τ₃ := isIso_π_f_of_isLimit_of_isEventuallyConstantTo F hcF _ _ hq₂
-- Module: Mathlib.Algebra.Homology.HomologicalComplexLimitsEventuallyConstant
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_2 : 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))

Tactic:
apply ShortComplex.quasiIso_of_epi_of_isIso_of_mono

Premises used: CategoryTheory.ShortComplex.quasiIso_of_epi_of_isIso_of_mono
-- Module: Mathlib.Algebra.Homology.HomologySequence
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 L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i j : ι
inst_2 : K.HasHomology i
inst_3 : K.HasHomology j
inst_4 : L.HasHomology i
inst_5 : L.HasHomology j
⊢ Eq (α := K.opcycles i ⟶ K.X (c.next j)) (K.fromOpcycles i j ≫ K.d j (c.next j)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologySequence
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
dsimp :
  Eq (α := K.opcycles i ⟶ K.X j)
    (CategoryStruct.comp (Y := K.cycles j) (K.liftCycles (K.fromOpcycles i j) (c.next j) ⋯ ⋯) (K.iCycles j))
    (K.fromOpcycles i 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)

Tactic:
dsimp only [opcyclesToCycles]

Premises used: HomologicalComplex.opcyclesToCycles
-- Module: Mathlib.Algebra.Homology.HomologySequence
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.liftCycles (K.fromOpcycles i j) (c.next j) ⋯ ⋯) (K.iCycles j))
    (K.fromOpcycles i j)

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologySequence
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
⊢ CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i)
      (CategoryStruct.comp (Y := K.cycles j) (K.opcyclesToCycles i j) (K.iCycles j)) =
    K.d i j

Tactic:
simp [opcyclesToCycles]

Premises used: HomologicalComplex.opcyclesToCycles
-- Module: Mathlib.Algebra.Homology.HomologySequence
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.X i ⟶ K.cycles j) (CategoryStruct.comp (Y := K.opcycles i) (K.pOpcycles i) (K.opcyclesToCycles i j))
    (K.toCycles i j)

Tactic:
simp only [← cancel_mono (K.iCycles j), assoc, opcyclesToCycles_iCycles,
    p_fromOpcycles, toCycles_i]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.toCycles_i, HomologicalComplex.p_fromOpcycles, HomologicalComplex.iCycles, CategoryTheory.cancel_mono, HomologicalComplex.opcyclesToCycles_iCycles
-- Module: Mathlib.Algebra.Homology.HomologySequence
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.homology i ⟶ K.cycles j) (K.homologyι i ≫ K.opcyclesToCycles i j) 0

Tactic:
simp only [← cancel_mono (K.iCycles j), assoc, opcyclesToCycles_iCycles,
    homologyι_comp_fromOpcycles, zero_comp]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.homologyι_comp_fromOpcycles, HomologicalComplex.iCycles, CategoryTheory.cancel_mono, CategoryTheory.Limits.zero_comp, HomologicalComplex.opcyclesToCycles_iCycles
-- Module: Mathlib.Algebra.Homology.HomologySequence
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.homology j) (K.opcyclesToCycles i j ≫ K.homologyπ j) 0

Tactic:
simp only [← cancel_epi (K.pOpcycles i),
    pOpcycles_opcyclesToCycles_assoc, toCycles_comp_homologyπ, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.toCycles_comp_homologyπ, HomologicalComplex.pOpcycles, CategoryTheory.cancel_epi, HomologicalComplex.pOpcycles_opcyclesToCycles_assoc
-- Module: Mathlib.Algebra.Homology.HomologySequence
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 L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i j : ι
inst_2 : K.HasHomology i
inst_3 : K.HasHomology j
inst_4 : L.HasHomology i
inst_5 : L.HasHomology j
⊢ Eq (α := K.opcycles i ⟶ L.cycles j)
    (CategoryStruct.comp (Y := L.opcycles i) (opcyclesMap φ i) (L.opcyclesToCycles i j))
    (CategoryStruct.comp (Y := K.cycles j) (K.opcyclesToCycles i j) (cyclesMap φ j))

Tactic:
simp only [← cancel_mono (L.iCycles j), ← cancel_epi (K.pOpcycles i),
    assoc, p_opcyclesMap_assoc, pOpcycles_opcyclesToCycles_iCycles, Hom.comm, cyclesMap_i,
    pOpcycles_opcyclesToCycles_iCycles_assoc]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.pOpcycles_opcyclesToCycles_iCycles_assoc, HomologicalComplex.iCycles, CategoryTheory.cancel_mono, HomologicalComplex.pOpcycles, HomologicalComplex.pOpcycles_opcyclesToCycles_iCycles, HomologicalComplex.cyclesMap_i, CategoryTheory.cancel_epi, HomologicalComplex.Hom.comm, HomologicalComplex.p_opcyclesMap_assoc
-- Module: Mathlib.Algebra.Homology.HomologySequence
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
dsimp : Mono (X := K.homology i) (K.homologyι i)
⊢ Mono
    ((composableArrows₃ K i j).map' 0 1 instMonoMap'ComposableArrows₃OfNatNat._proof_1
      instMonoMap'ComposableArrows₃OfNatNat._proof_3)

Tactic:
dsimp
-- Module: Mathlib.Algebra.Homology.HomologySequence
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 (X := K.homology i) (K.homologyι i)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomologySequence
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
dsimp : Epi (X := K.cycles j) (K.homologyπ j)
⊢ Epi
    ((composableArrows₃ K i j).map' 2 3 instEpiMap'ComposableArrows₃OfNatNat._proof_2
      instEpiMap'ComposableArrows₃OfNatNat._proof_3)

Tactic:
dsimp [-Fin.reduceFinMk]

Premises used: Fin.reduceFinMk
-- Module: Mathlib.Algebra.Homology.HomologySequence
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
⊢ Epi (X := K.cycles j) (K.homologyπ j)

Tactic:
infer_instance
-- Module: Mathlib.Algebra.Homology.HomologySequence
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 : CategoryWithHomology.{v_1, u_1} C
⊢ Eq (α := K.homology i ⟶ K.cycles j) (K.homologyι i ≫ K.opcyclesToCycles i j) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologySequence
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 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
⊢ Eq (α := K.homology i ⟶ K.X j) (K.homologyι i ≫ K.fromOpcycles i j) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
rw : S'.Exact
⊢ S.Exact

Tactic:
rw [ShortComplex.exact_iff_of_epi_of_isIso_of_mono ι]

Premises used: CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ S'.Exact

Tactic:
S'.exact_of_f_is_kernel (K.homologyIsKernel i j (c.next_eq' hij))

Premises used: CategoryTheory.ShortComplex.exact_of_f_is_kernel, HomologicalComplex.homologyIsKernel, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ S'.Exact

Tactic:
exact S'.exact_of_f_is_kernel (K.homologyIsKernel i j (c.next_eq' hij))

Premises used: CategoryTheory.ShortComplex.exact_of_f_is_kernel, HomologicalComplex.homologyIsKernel, ComplexShape.next_eq'
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ S.Exact

Tactic:
have hS : S.Exact := by
    rw [ShortComplex.exact_iff_of_epi_of_isIso_of_mono ι]
    exact S'.exact_of_f_is_kernel (K.homologyIsKernel i j (c.next_eq' hij))
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
⊢ Eq (α := K.opcycles i ⟶ K.homology j) (K.opcyclesToCycles i j ≫ K.homologyπ j) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
⊢ Eq (α := K.X i ⟶ K.homology j) (K.toCycles i j ≫ K.homologyπ j) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologySequence
Goal:
C : Type u_1
ι_1 : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
c : ComplexShape ι_1
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι_1
hij : c.Rel i j
inst_2 : CategoryWithHomology.{v_1, u_1} C
S : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.homology i) (X₃ := K.cycles j) (K.homologyι i) (K.opcyclesToCycles i j) ⋯
S' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₁ := K.homology i) (K.homologyι i) (K.fromOpcycles i j) ⋯
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex.{v_1, u_1} C :=
  ShortComplex.mk (X₁ := K.opcycles i) (X₂ := K.cycles j) (K.opcyclesToCycles i j) (K.homologyπ j) ⋯
T' : ShortComplex.{v_1, u_1} C := ShortComplex.mk (X₂ := K.cycles j) (K.toCycles i j) (K.homologyπ j) ⋯
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
rw : T'.Exact
⊢ T.Exact

Tactic:
rw [← ShortComplex.exact_iff_of_epi_of_isIso_of_mono π]

Premises used: CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono