mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X : C
⊢ F.map (𝟙 X) = 𝟙 (F.obj X)

Tactic:
F.map_id

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X : C
⊢ 𝟙 (F.obj X) = 𝟙 (F.obj X)
Module: Mathlib.CategoryTheory.Localization.Triangulated

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
fac : L.map T₁.mor₁ ≫ γ.map L ⋯ = a ≫ L.map T₂.mor₁ ≫ L.map β.s
hγ : b ≫ L.map β.s = γ.map L ⋯
⊢ L.map (α.f ≫ β.f ≫ γ.s) = L.map (T₁.mor₁ ≫ γ.f)

Tactic:
← cancel_mono (L.map γ.s),

Goal state after:
C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
fac : (L.map T₁.mor₁ ≫ γ.map L ⋯) ≫ L.map γ.s = (a ≫ L.map T₂.mor₁ ≫ L.map β.s) ≫ L.map γ.s
hγ : b ≫ L.map β.s = γ.map L ⋯
⊢ L.map (α.f ≫ β.f ≫ γ.s) = L.map (T₁.mor₁ ≫ γ.f)
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P Q : ObjectProperty C
inst✝ : Q.ContainsZero
⊢ P ≤ P.extensionProduct Q

Tactic:
intro X hX

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P Q : ObjectProperty C
inst✝ : Q.ContainsZero
X : C
hX : P X
⊢ P.extensionProduct Q X
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P Q : ObjectProperty C
inst✝ : P.ContainsZero
⊢ Q ≤ P.extensionProduct Q

Tactic:
intro X hX

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P Q : ObjectProperty C
inst✝ : P.ContainsZero
X : C
hX : Q X
⊢ P.extensionProduct Q X
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P Q : ObjectProperty C
hPQ : P ≤ Q
n : ℕ
⊢ P.extensionProductIter n ≤ Q.extensionProductIter n

Tactic:
induction n with
  | zero => exact hPQ
  | succ n h => grw [extensionProductIter_succ, extensionProductIter_succ,
    monotone_extensionProduct_left _ hPQ, monotone_extensionProduct_right _ h]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
a : ℤ
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K).τ₁ =
    ((shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)).τ₁

pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
a : ℤ
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K).τ₂ =
    ((shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)).τ₂

pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
a : ℤ
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K).τ₃ =
    ((shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)).τ₃

Tactic:
<;>

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
a : ℤ
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K).τ₁ =
    ((shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
a : ℤ
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K).τ₂ =
    ((shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
a : ℤ
K : CochainComplex C ℤ
⊢ ((shiftShortComplexFunctorIso C 0 a a ⋯).hom.app K).τ₃ =
    ((shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (CochainComplex C ℤ) ℤ).hom.app K)).τ₃
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ mn.negOnePow • (XIsoOfEq K ⋯).hom =
    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K).f ((up ℤ).prev a) ≫
      (n.negOnePow • (XIsoOfEq ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ⋯).hom) ≫
        (m.negOnePow • (XIsoOfEq K ⋯).hom)

pp: case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ (XIsoOfEq K ⋯).hom =
    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K).f a ≫
      (XIsoOfEq ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ⋯).hom ≫ (XIsoOfEq K ⋯).hom

pp: case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ mn.negOnePow • (XIsoOfEq K ⋯).hom =
    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K).f ((up ℤ).next a) ≫
      (n.negOnePow • (XIsoOfEq ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ⋯).hom) ≫
        (m.negOnePow • (XIsoOfEq K ⋯).hom)

Tactic:
<;>

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ mn.negOnePow • (XIsoOfEq K ⋯).hom =
    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K).f ((up ℤ).prev a) ≫
      (n.negOnePow • (XIsoOfEq ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ⋯).hom) ≫
        (m.negOnePow • (XIsoOfEq K ⋯).hom)

case h₂
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ (XIsoOfEq K ⋯).hom =
    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K).f a ≫
      (XIsoOfEq ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ⋯).hom ≫ (XIsoOfEq K ⋯).hom

case h₃
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ mn.negOnePow • (XIsoOfEq K ⋯).hom =
    ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K).f ((up ℤ).next a) ≫
      (n.negOnePow • (XIsoOfEq ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ⋯).hom) ≫
        (m.negOnePow • (XIsoOfEq K ⋯).hom)
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝³ : Preadditive C
inst✝² : CategoryWithHomology C
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
⊢ (HomotopyCategory.quasiIso C c).IsInvertedBy Qh

Tactic:
by
  rintro ⟨K⟩ ⟨L⟩ φ
  obtain ⟨φ, rfl⟩ := (HomotopyCategory.quotient C c).map_surjective φ
  rw [HomotopyCategory.quotient_map_mem_quasiIso_iff φ,
    ← HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso]
  exact (NatIso.isIso_map_iff (quotientCompQhIso C c) φ).2

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    -((snd (mappingConeCompTriangle f g).mor₁).comp
            ((↑(fst (f ≫ g))).comp
                ((inl f).comp (δ (-1) 0 (inl (mappingConeCompTriangle f g).mor₁)) ⋯ +
                  -(δ (-1) 0 (inl f)).comp (inl (mappingConeCompTriangle f g).mor₁) ⋯)
                ⋯ +
              (δ 1 2 ↑(fst (f ≫ g))).comp
                ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
            ⋯ +
          -(δ 0 1 (snd (mappingConeCompTriangle f g).mor₁)).comp
              ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                ⋯)
              ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))

Tactic:
δ_inl,

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    -((snd (mappingConeCompTriangle f g).mor₁).comp
            ((↑(fst (f ≫ g))).comp
                ((inl f).comp
                    (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁)) ⋯ +
                  -(δ (-1) 0 (inl f)).comp (inl (mappingConeCompTriangle f g).mor₁) ⋯)
                ⋯ +
              (δ 1 2 ↑(fst (f ≫ g))).comp
                ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
            ⋯ +
          -(δ 0 1 (snd (mappingConeCompTriangle f g).mor₁)).comp
              ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                ⋯)
              ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    -((snd (mappingConeCompTriangle f g).mor₁).comp
            ((↑(fst (f ≫ g))).comp
                ((inl f).comp
                    (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁)) ⋯ +
                  -(δ (-1) 0 (inl f)).comp (inl (mappingConeCompTriangle f g).mor₁) ⋯)
                ⋯ +
              (δ 1 2 ↑(fst (f ≫ g))).comp
                ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
            ⋯ +
          -(δ 0 1 (snd (mappingConeCompTriangle f g).mor₁)).comp
              ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                ⋯)
              ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))

Tactic:
δ_inl,

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    -((snd (mappingConeCompTriangle f g).mor₁).comp
            ((↑(fst (f ≫ g))).comp
                ((inl f).comp
                    (Cochain.ofHom ((mappingConeCompTriangle f g).mor₁ ≫ inr (mappingConeCompTriangle f g).mor₁)) ⋯ +
                  -(Cochain.ofHom (f ≫ inr f)).comp (inl (mappingConeCompTriangle f g).mor₁) ⋯)
                ⋯ +
              (δ 1 2 ↑(fst (f ≫ g))).comp
                ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
            ⋯ +
          -(δ 0 1 (snd (mappingConeCompTriangle f g).mor₁)).comp
              ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1)
                ⋯)
              ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝ : HasBinaryBiproducts C
⊢ (triangle φ).rotate.mor₂ ≫
      ((shiftFunctorCompIsoId (CochainComplex C ℤ) (-1) 1 triangle._proof_2).app (mappingCone φ)).hom =
    (Iso.refl (triangle φ).rotate.obj₂).hom ≫ (mappingCone.triangle φ).mor₂

Tactic:
by simp [triangle]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
hT : DerivedCategory.Q.mapTriangle.obj T ∈ distinguishedTriangles
n : ℤ
⊢ { X₁ := homology T.obj₁ n, X₂ := homology T.obj₂ n, X₃ := homology T.obj₃ n, f := homologyMap T.mor₁ n,
      g := homologyMap T.mor₂ n, zero := ⋯ }.Exact

Tactic:
refine ShortComplex.exact_of_iso ?_ (DerivedCategory.HomologySequence.exact₂ _ hT n)

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
hT : DerivedCategory.Q.mapTriangle.obj T ∈ distinguishedTriangles
n : ℤ
⊢ { X₁ := (DerivedCategory.homologyFunctor C n).obj (DerivedCategory.Q.mapTriangle.obj T).obj₁,
      X₂ := (DerivedCategory.homologyFunctor C n).obj (DerivedCategory.Q.mapTriangle.obj T).obj₂,
      X₃ := (DerivedCategory.homologyFunctor C n).obj (DerivedCategory.Q.mapTriangle.obj T).obj₃,
      f := (DerivedCategory.homologyFunctor C n).map (DerivedCategory.Q.mapTriangle.obj T).mor₁,
      g := (DerivedCategory.homologyFunctor C n).map (DerivedCategory.Q.mapTriangle.obj T).mor₂, zero := ⋯ } ≅
    { X₁ := homology T.obj₁ n, X₂ := homology T.obj₂ n, X₃ := homology T.obj₃ n, f := homologyMap T.mor₁ n,
      g := homologyMap T.mor₂ n, zero := ⋯ }
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V c
x✝⁴ x✝³ x✝² : ι
x✝¹ : c.symm.Rel x✝⁴ x✝³
x✝ : c.symm.Rel x✝³ x✝²
⊢ (X.d x✝³ x✝⁴).op ≫ (X.d x✝² x✝³).op = 0

Tactic:
by rw [← op_comp, X.d_comp_d, op_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : HomologicalComplex V c.symm
x✝⁴ x✝³ x✝² : ι
x✝¹ : c.Rel x✝⁴ x✝³
x✝ : c.Rel x✝³ x✝²
⊢ (X.d x✝³ x✝⁴).op ≫ (X.d x✝² x✝³).op = 0

Tactic:
by rw [← op_comp, X.d_comp_d, op_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case none
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
⊢ d K none none = 0

pp: case some
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
val✝ : ι
⊢ d K (some val✝) none = 0

Tactic:
<;>

Goal state after:
case none
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
⊢ d K none none = 0

case some
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
val✝ : ι
⊢ d K (some val✝) none = 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: case pos
ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
hij : c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j

Tactic:
obtain rfl := c.prev_eq' hij
    exact (K.sc i).opcyclesOpIso_hom_toCycles_op

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case inr.inr.inl
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
hk' : e.r k' = none
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

pp: case inr.inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0

Tactic:
· rw [extend.d_none_eq_zero' K _ _ hk', comp_zero]

Goal state after:
case inr.inr.inr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i' j' k' : ι'
x✝¹ : c'.Rel i' j'
x✝ : c'.Rel j' k'
i : ι
hi : e.r i' = some i
j : ι
hj : e.r j' = some j
k : ι
hk : e.r k' = some k
⊢ extend.d K (e.r i') (e.r j') ≫ extend.d K (e.r j') (e.r k') = 0
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
i : ι
hi : e.f i = i'
hi' : ¬c.Rel i (c.next i)
⊢ (K.extend e).d i' j' = 0

Tactic:
by
  obtain hj' | ⟨j, hj⟩ := (e.r j').eq_none_or_eq_some
  · exact extend.d_none_eq_zero' _ _ _ hj'
  · rw [extend_d_eq K e hi (e.f_eq_of_r_eq_some hj), K.shape, zero_comp, comp_zero]
    intro hij
    obtain rfl := c.next_eq' hij
    exact hi' hij

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
hj' : c.Rel j (c.next j)
⊢ c'.Rel (e.f j) (c'.next (e.f j))

Tactic:
← e.rel_iff

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsTruncGE
j k : ι
hjk : c.next j = k
hj : ¬c'.Rel (e.f j) (c'.next (e.f j))
hj' : c'.Rel (e.f j) (e.f (c.next j))
⊢ c'.Rel (e.f j) (c'.next (e.f j))
Module: Mathlib.Algebra.Homology.Embedding.TruncGE

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
h✝ : e.BoundaryGE i
⊢ ((XIsoOpcycles K e h✝).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (XIso K e ⋯).inv) ≫
      (XIso K e ⋯).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv =
    0

pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
h✝ : ¬e.BoundaryGE i
⊢ ((XIso K e h✝).hom ≫ K.d (e.f i) (e.f j) ≫ (XIso K e ⋯).inv) ≫
      (XIso K e ⋯).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv =
    0

Tactic:
<;>

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
h✝ : e.BoundaryGE i
⊢ ((XIsoOpcycles K e h✝).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (XIso K e ⋯).inv) ≫
      (XIso K e ⋯).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv =
    0

case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
h✝ : ¬e.BoundaryGE i
⊢ ((XIso K e h✝).hom ≫ K.d (e.f i) (e.f j) ≫ (XIso K e ⋯).inv) ≫
      (XIso K e ⋯).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv =
    0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
cocone : CokernelCofork (hcone.lift (KernelFork.ofι (K.d i j) ⋯))
hcocone : IsColimit cocone
⊢ (isLimitKernelFork K e hj' hk hk' cone hcone).lift (KernelFork.ofι ((K.extend e).d i' j') ⋯) ≫ Cofork.π cocone = 0

Tactic:
← lift_d_comp_eq_zero_iff K e hj' hi hi' hk hk' cone hcone

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
cocone : CokernelCofork (hcone.lift (KernelFork.ofι (K.d i j) ⋯))
hcocone : IsColimit cocone
⊢ hcone.lift (KernelFork.ofι (K.d i j) ⋯) ≫ Cofork.π cocone = 0