awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
⊢ Eq (α := K.homology i ⟶ L.opcycles i) (homologyMap φ i ≫ L.homologyι i) (K.homologyι i ≫ opcyclesMap φ i)

Tactic:
ShortComplex.homologyι_naturality _

Premises used: CategoryTheory.ShortComplex.homologyι_naturality, HomologicalComplex.opcycles, HomologicalComplex.opcyclesMap, HomologicalComplex.homologyι, HomologicalComplex.homologyMap, HomologicalComplex.homology
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
⊢ Eq (α := K.cycles i ⟶ K.opcycles i) (K.homologyπ i ≫ K.homologyι i) (K.iCycles i ≫ K.pOpcycles i)

Tactic:
(K.sc i).homology_π_ι

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.homology_π_ι, HomologicalComplex.iCycles, HomologicalComplex.opcycles, HomologicalComplex.homologyι, HomologicalComplex.sc, HomologicalComplex.pOpcycles, HomologicalComplex.homology, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
⊢ CategoryStruct.comp (Y := L.homology i) (homologyMap iso.hom i) (homologyMap iso.inv i) = 𝟙 (K.homology i)

Tactic:
simp [← homologyMap_comp]

Premises used: HomologicalComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
⊢ CategoryStruct.comp (Y := K.homology i) (homologyMap iso.inv i) (homologyMap iso.hom i) = 𝟙 (L.homology i)

Tactic:
simp [← homologyMap_comp]

Premises used: HomologicalComplex.homologyMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
⊢ CategoryStruct.comp (Y := L.cycles i) (cyclesMap iso.hom i) (cyclesMap iso.inv i) = 𝟙 (K.cycles i)

Tactic:
simp [← cyclesMap_comp]

Premises used: HomologicalComplex.cyclesMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
⊢ CategoryStruct.comp (Y := K.cycles i) (cyclesMap iso.inv i) (cyclesMap iso.hom i) = 𝟙 (L.cycles i)

Tactic:
simp [← cyclesMap_comp]

Premises used: HomologicalComplex.cyclesMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
⊢ CategoryStruct.comp (Y := L.opcycles i) (opcyclesMap iso.hom i) (opcyclesMap iso.inv i) = 𝟙 (K.opcycles i)

Tactic:
simp [← opcyclesMap_comp]

Premises used: HomologicalComplex.opcyclesMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j k : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
⊢ CategoryStruct.comp (Y := K.opcycles i) (opcyclesMap iso.inv i) (opcyclesMap iso.hom i) = 𝟙 (L.opcycles i)

Tactic:
simp [← opcyclesMap_comp]

Premises used: HomologicalComplex.opcyclesMap_comp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ_1 : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
A : C
k : L.X i ⟶ A
j : ι
hj : c.prev i = j
hk : L.d j i ≫ k = 0
φ : K ⟶ L
rw : φ.f j ≫ L.d j i ≫ k = 0
rw₁ : Eq (α := K.X j ⟶ A) (φ.f j ≫ 0) 0
rw₂ rw₃ : Eq.{v_1 + 1} (α := K.X j ⟶ A) 0 0
⊢ K.d j i ≫ φ.f i ≫ k = 0

Tactic:
rw [← φ.comm_assoc, hk, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, HomologicalComplex.Hom.comm_assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
A : C
k : L.X i ⟶ A
j : ι
hj : c.prev i = j
hk : L.d j i ≫ k = 0
φ : K ⟶ L
⊢ Eq (α := K.opcycles i ⟶ A) (CategoryStruct.comp (Y := L.opcycles i) (opcyclesMap φ i) (L.descOpcycles k j hj hk))
    (K.descOpcycles (φ.f i ≫ k) j hj ⋯)

Tactic:
simp only [← cancel_epi (K.pOpcycles i), p_opcyclesMap_assoc, p_descOpcycles]

Premises used: HomologicalComplex.pOpcycles, CategoryTheory.cancel_epi, HomologicalComplex.p_opcyclesMap_assoc, HomologicalComplex.p_descOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L M : HomologicalComplex.{v_1, u_1, u_2} C c
φ_1 : K ⟶ L
iso : K ≅ L
ψ : L ⟶ M
i j_1 k_1 : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : M.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
φ : K ⟶ L
rw : k ≫ φ.f i ≫ L.d i j = 0
rw₁ : k ≫ K.d i j ≫ φ.f j = 0
rw₂ : Eq (α := A ⟶ L.X j) (0 ≫ φ.f j) 0
rw₃ rw₄ : Eq.{v_1 + 1} (α := A ⟶ L.X j) 0 0
⊢ (k ≫ φ.f i) ≫ L.d i j = 0

Tactic:
rw [assoc, φ.comm, reassoc_of% hk, zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.zero_comp, HomologicalComplex.Hom.comm
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
A : C
k : A ⟶ K.X i
j : ι
hj : c.next i = j
hk : k ≫ K.d i j = 0
φ : K ⟶ L
⊢ Eq (α := A ⟶ L.cycles i) (CategoryStruct.comp (Y := K.cycles i) (K.liftCycles k j hj hk) (cyclesMap φ i))
    (L.liftCycles (k ≫ φ.f i) j hj ⋯)

Tactic:
simp only [← cancel_mono (L.iCycles i), assoc, cyclesMap_i, liftCycles_i_assoc, liftCycles_i]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.iCycles, CategoryTheory.cancel_mono, HomologicalComplex.liftCycles_i_assoc, HomologicalComplex.liftCycles_i, HomologicalComplex.cyclesMap_i
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hj : c.next i = j
h : K.d i j = 0
inst_2 : K.HasHomology i
⊢ Eq (α := K.X i ⟶ K.X (c.next i)) (K.d i (c.next i)) 0

Tactic:
subst hj
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
h : Eq (α := K.X i ⟶ K.X (c.next i)) (K.d i (c.next i)) 0
⊢ IsIso (X := K.cycles i) (K.iCycles i)

Tactic:
ShortComplex.isIso_iCycles _ h

Premises used: CategoryTheory.ShortComplex.isIso_iCycles, HomologicalComplex.iCycles, HomologicalComplex.cycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
h : Eq (α := K.X i ⟶ K.X (c.next i)) (K.d i (c.next i)) 0
⊢ IsIso (X := K.cycles i) (K.iCycles i)

Tactic:
exact ShortComplex.isIso_iCycles _ h

Premises used: CategoryTheory.ShortComplex.isIso_iCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hj : c.next i = j
h : K.d i j = 0
inst_2 : K.HasHomology i
⊢ K.iCycles i ≫ Iso.inv (K.iCyclesIso i j hj h) = 𝟙 (K.cycles i)

Tactic:
(K.iCyclesIso i j hj h).hom_inv_id

Premises used: HomologicalComplex.iCycles, CategoryTheory.Iso.hom_inv_id, HomologicalComplex.iCyclesIso, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hj : c.next i = j
h : K.d i j = 0
inst_2 : K.HasHomology i
⊢ CategoryStruct.comp (Y := K.cycles i) (Iso.inv (K.iCyclesIso i j hj h)) (K.iCycles i) = 𝟙 (K.X i)

Tactic:
(K.iCyclesIso i j hj h).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, HomologicalComplex.iCycles, HomologicalComplex.iCyclesIso, CategoryTheory.ShortComplex.iCycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hj : c.next i = j
h : K.d i j = 0
inst_2 : K.HasHomology i
⊢ K.homologyι i ≫ Iso.inv (K.isoHomologyι i j hj h) = 𝟙 (K.homology i)

Tactic:
(K.isoHomologyι i j hj h).hom_inv_id

Premises used: CategoryTheory.Iso.hom_inv_id, HomologicalComplex.homologyι, HomologicalComplex.isoHomologyι, CategoryTheory.ShortComplex.homologyι
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hj : c.next i = j
h : K.d i j = 0
inst_2 : K.HasHomology i
⊢ Iso.inv (K.isoHomologyι i j hj h) ≫ K.homologyι i = 𝟙 (K.opcycles i)

Tactic:
(K.isoHomologyι i j hj h).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, HomologicalComplex.homologyι, HomologicalComplex.isoHomologyι, CategoryTheory.ShortComplex.homologyι
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hi : c.prev j = i
h : K.d i j = 0
inst_2 : K.HasHomology j
⊢ Eq (α := K.X (c.prev j) ⟶ K.X j) (K.d (c.prev j) j) 0

Tactic:
obtain rfl := hi

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
inst_2 : K.HasHomology j
h : Eq (α := K.X (c.prev j) ⟶ K.X j) (K.d (c.prev j) j) 0
⊢ IsIso (Y := K.opcycles j) (K.pOpcycles j)

Tactic:
ShortComplex.isIso_pOpcycles _ h

Premises used: CategoryTheory.ShortComplex.isIso_pOpcycles, HomologicalComplex.opcycles, HomologicalComplex.pOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
j : ι
inst_2 : K.HasHomology j
h : Eq (α := K.X (c.prev j) ⟶ K.X j) (K.d (c.prev j) j) 0
⊢ IsIso (Y := K.opcycles j) (K.pOpcycles j)

Tactic:
exact ShortComplex.isIso_pOpcycles _ h

Premises used: CategoryTheory.ShortComplex.isIso_pOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hi : c.prev j = i
h : K.d i j = 0
inst_2 : K.HasHomology j
⊢ CategoryStruct.comp (Y := K.opcycles j) (K.pOpcycles j) (Iso.inv (K.pOpcyclesIso i j hi h)) = 𝟙 (K.X j)

Tactic:
(K.pOpcyclesIso i j hi h).hom_inv_id

Premises used: CategoryTheory.ShortComplex.pOpcycles, CategoryTheory.Iso.hom_inv_id, HomologicalComplex.pOpcyclesIso, HomologicalComplex.pOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hi : c.prev j = i
h : K.d i j = 0
inst_2 : K.HasHomology j
⊢ Iso.inv (K.pOpcyclesIso i j hi h) ≫ K.pOpcycles j = 𝟙 (K.opcycles j)

Tactic:
(K.pOpcyclesIso i j hi h).inv_hom_id

Premises used: CategoryTheory.Iso.inv_hom_id, CategoryTheory.ShortComplex.pOpcycles, HomologicalComplex.pOpcyclesIso, HomologicalComplex.pOpcycles
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hi : c.prev j = i
h : K.d i j = 0
inst_2 : K.HasHomology j
⊢ K.homologyπ j ≫ Iso.inv (K.isoHomologyπ i j hi h) = 𝟙 (K.cycles j)

Tactic:
(K.isoHomologyπ i j hi h).hom_inv_id

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.homologyπ, CategoryTheory.Iso.hom_inv_id, HomologicalComplex.isoHomologyπ
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j : ι
hi : c.prev j = i
h : K.d i j = 0
inst_2 : K.HasHomology j
⊢ Iso.inv (K.isoHomologyπ i j hi h) ≫ K.homologyπ j = 𝟙 (K.homology j)

Tactic:
(K.isoHomologyπ i j hi h).inv_hom_id

Premises used: HomologicalComplex.homologyπ, CategoryTheory.ShortComplex.homologyπ, CategoryTheory.Iso.inv_hom_id, HomologicalComplex.isoHomologyπ
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
i : ι
inst_2 : K.HasHomology i
inst_3 : L.HasHomology i
inst_4 : Epi (φ.f i)
hi : ∀ (j : ι), ¬c.Rel i j
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : c.Rel i (c.next i) → False
⊢ ¬c.Rel i (c.next i)

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K L : HomologicalComplex.{v_1, u_1, u_2} C c
φ : K ⟶ L
j : ι
inst_2 : K.HasHomology j
inst_3 : L.HasHomology j
inst_4 : Mono (φ.f j)
hj : ∀ (i : ι), ¬c.Rel i j
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ : c.Rel (c.prev j) j → False
⊢ ¬c.Rel (c.prev j) j

Tactic:
tauto
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
⊢ K.ExactAt i ↔ (K.sc i).Exact

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
hK : K.ExactAt i
L : HomologicalComplex.{v_1, u_1, u_2} C c
e : K ≅ L
rw : ∀ (hK : (K.sc i).Exact) {L : HomologicalComplex.{v_1, u_1, u_2} C c} (e : K ≅ L), (L.sc i).Exact
⊢ L.ExactAt i

Tactic:
rw [exactAt_iff] at hK ⊢

Premises used: HomologicalComplex.exactAt_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
hK : (K.sc i).Exact
L : HomologicalComplex.{v_1, u_1, u_2} C c
e : K ≅ L
⊢ (L.sc i).Exact

Tactic:
ShortComplex.exact_of_iso ((shortComplexFunctor C c i).mapIso e) hK

Premises used: HomologicalComplex.shortComplexFunctor, CategoryTheory.ShortComplex.exact_of_iso, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
hK : (K.sc i).Exact
L : HomologicalComplex.{v_1, u_1, u_2} C c
e : K ≅ L
⊢ (L.sc i).Exact

Tactic:
exact ShortComplex.exact_of_iso ((shortComplexFunctor C c i).mapIso e) hK

Premises used: HomologicalComplex.shortComplexFunctor, CategoryTheory.ShortComplex.exact_of_iso, CategoryTheory.Functor.mapIso
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
h : IsZero.{v_1, u_1} (K.X i)
⊢ K.ExactAt i

Tactic:
ShortComplex.exact_of_isZero_X₂ _ h

Premises used: HomologicalComplex.ExactAt, CategoryTheory.ShortComplex.exact_of_isZero_X₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
⊢ K.ExactAt j ↔ (K.sc' i j k).Exact

Tactic:
ShortComplex.exact_iff_of_iso (K.isoSc' i j k hi hk)

Premises used: HomologicalComplex.ExactAt, CategoryTheory.ShortComplex.exact_iff_of_iso, HomologicalComplex.isoSc'
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
rw : (K.sc i).Exact ↔ IsZero.{v_1, u_1} (K.sc i).homology
rw₁ rw₂ : IsZero.{v_1, u_1} (K.sc i).homology ↔ IsZero.{v_1, u_1} (K.sc i).homology
⊢ K.ExactAt i ↔ IsZero.{v_1, u_1} (K.sc i).homology

Tactic:
rw [exactAt_iff, ShortComplex.exact_iff_isZero_homology]

Premises used: CategoryTheory.ShortComplex.exact_iff_isZero_homology, HomologicalComplex.exactAt_iff
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
i : ι
inst_2 : K.HasHomology i
h rwa rwa₁ rwa₂ rwa₃ : K.ExactAt i
⊢ IsZero.{v_1, u_1} (K.homology i)

Tactic:
rwa [← exactAt_iff_isZero_homology]

Premises used: HomologicalComplex.exactAt_iff_isZero_homology
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
⊢ K.Acyclic ↔ ∀ (i : ι), K.ExactAt i

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
hK : IsZero K
i : ι
h : IsZero.{v_1, u_1} (K.sc i).X₂
⊢ K.ExactAt i

Tactic:
apply ShortComplex.exact_of_isZero_X₂

Premises used: CategoryTheory.ShortComplex.exact_of_isZero_X₂
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
hK : IsZero K
i : ι
⊢ IsZero.{v_1, u_1} (K.sc i).X₂

Tactic:
(eval _ _ i).map_isZero hK

Premises used: HomologicalComplex.eval, CategoryTheory.Functor.map_isZero
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
hK : IsZero K
i : ι
⊢ IsZero.{v_1, u_1} (K.sc i).X₂

Tactic:
exact (eval _ _ i).map_isZero hK

Premises used: HomologicalComplex.eval, CategoryTheory.Functor.map_isZero
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : ChainComplex.{v_1, u_1, 0} C ℕ
φ : K ⟶ L
inst_2 : HomologicalComplex.HasHomology K 0
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : ChainComplex.{v_1, u_1, 0} C ℕ
φ : K ⟶ L
inst_2 : HomologicalComplex.HasHomology K 0
⊢ Eq (α := K.X 0 ⟶ K.X 0) (K.d 0 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : ChainComplex.{v_1, u_1, 0} C ℕ
φ : K ⟶ L
inst_2 : HomologicalComplex.HasHomology K 0
⊢ Eq (α := K.X 0 ⟶ K.X ((ComplexShape.down ℕ).next 0)) (K.d 0 ((ComplexShape.down ℕ).next 0)) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : ChainComplex.{v_1, u_1, 0} C ℕ
φ : K ⟶ L
inst_2 : HomologicalComplex.HasHomology K 0
inst_3 : HomologicalComplex.HasHomology L 0
⊢ Eq (α := HomologicalComplex.opcycles K 0 ⟶ HomologicalComplex.homology L 0)
    (Iso.inv K.isoHomologyι₀ ≫ HomologicalComplex.homologyMap φ 0)
    (HomologicalComplex.opcyclesMap φ 0 ≫ Iso.inv L.isoHomologyι₀)

Tactic:
simp only [assoc, ← cancel_mono (L.homologyι 0),
    HomologicalComplex.homologyι_naturality, HomologicalComplex.isoHomologyι_inv_hom_id_assoc,
    HomologicalComplex.isoHomologyι_inv_hom_id, comp_id]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.isoHomologyι_inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, HomologicalComplex.homologyι, HomologicalComplex.homologyι_naturality, OfNat.ofNat, HomologicalComplex.isoHomologyι_inv_hom_id_assoc
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℕ
φ : K ⟶ L
inst_2 : HomologicalComplex.HasHomology K 0
⊢ (ComplexShape.up ℕ).prev 0 = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℕ
φ : K ⟶ L
inst_2 : HomologicalComplex.HasHomology K 0
⊢ Eq (α := K.X 0 ⟶ K.X 0) (K.d 0 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
K L : CochainComplex.{v_1, u_1, 0} C ℕ
φ : K ⟶ L
inst_2 : HomologicalComplex.HasHomology K 0
⊢ Eq (α := K.X ((ComplexShape.up ℕ).prev 0) ⟶ K.X 0) (K.d ((ComplexShape.up ℕ).prev 0) 0) 0

Tactic:
simp