mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) ↔ n < p

Tactic:
by

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:
by

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

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
K L : HomologicalComplex C c'
e' : K ≅ L
φ : K ⟶ L
e : c.Embedding c'
inst✝ : K.IsStrictlySupported e
⊢ K.op.IsStrictlySupported e.op

Tactic:
by

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

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
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝² : ∀ (i : ι'), K.HasHomology i
inst✝¹ : ∀ (i : ι'), L.HasHomology i
inst✝ : QuasiIso φ
⊢ K.IsSupported e ↔ L.IsSupported e

Tactic:
by

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

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
K L : HomologicalComplex C c'
e' : K ≅ L
φ : K ⟶ L
e : c.Embedding c'
inst✝ : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ K.ExactAt i'

Tactic:
by

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₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ { X₁ := homology T.obj₂ n₀, X₂ := homology T.obj₃ n₀, X₃ := homology T.obj₁ n₁, f := homologyMap T.mor₂ n₀,
      g := homologyδOfTriangle T n₀ n₁ h, zero := ⋯ }.Exact

Tactic:
by

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

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
K : HomologicalComplex C c'
e : c.Embedding c'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ¬∃ i, e.f i = n
⊢ ∀ (i : ι), e.f i ≠ n

Tactic:
by

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

Goal state before:
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'
h₁ : K.IsStrictlySupported e
h₂ : K.IsStrictlySupportedOutside e
n : ι'
hn : ¬∃ i, e.f i = n
⊢ IsZero (K.X n)

Tactic:
· exact K.isZero_X_of_isStrictlySupported e _ (by simpa using hn)

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

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
K : HomologicalComplex C c'
e : c.Embedding c'
⊢ IsZero K ↔ K.IsStrictlySupported e ∧ K.IsStrictlySupportedOutside e

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_4} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
K : HomologicalComplex C c'
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
e : c.Embedding c'
inst✝ : K.IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ IsZero (((F.mapHomologicalComplex c').obj K).X i')

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
D : Type u_4
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_4} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
K : HomologicalComplex C c'
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
e : c.Embedding c'
inst✝ : F.Faithful
⊢ ((F.mapHomologicalComplex c').obj K).IsStrictlySupported e ↔ K.IsStrictlySupported e

Tactic:
by

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ g.op ≫ f.op = 0

Tactic:
by

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ f ≫ factorThruImage g = 0

Tactic:
by

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.op f.op ⋯ =
    (imageSubobjectIso g.op ≪≫ (imageOpOp g).symm).hom ≫
      (cokernel.desc f (factorThruImage g) ⋯).op ≫ (kernelSubobjectIso f.op ≪≫ kernelOpOp f).inv

Tactic:
by

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ g.unop ≫ f.unop = 0

Tactic:
by

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ f ≫ factorThruImage g = 0

Tactic:
by

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

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : Vᵒᵖ
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.unop f.unop ⋯ =
    (imageSubobjectIso g.unop ≪≫ (imageUnopUnop g).symm).hom ≫
      (cokernel.desc f (factorThruImage g) ⋯).unop ≫ (kernelSubobjectIso f.unop ≪≫ kernelUnopUnop f).inv

Tactic:
by

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
i j : ι
hij : ¬c.symm.Rel i j
⊢ (X.d j i).op = 0

Tactic:
by

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₃
n : ℤ
⊢ n + 1 = n + 1

Tactic:
by

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
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

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₃
n : ℤ
⊢ n + 1 + -1 = n

Tactic:
by

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
i j : ι
hij : ¬c.Rel i j
⊢ (X.d j i).op = 0

Tactic:
by

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₃
n : ℤ
⊢ n + 2 + -2 = n

Tactic:
by

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₃
n : ℤ
⊢ n + 2 + -1 = n + 1

Tactic:
by

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

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
i j : ι
hij : ¬c.symm.Rel i j
⊢ (X.d j i).unop = 0

Tactic:
by

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
x✝⁴ x✝³ x✝² : ι
x✝¹ : c.symm.Rel x✝⁴ x✝³
x✝ : c.symm.Rel x✝³ x✝²
⊢ (X.d x✝³ x✝⁴).unop ≫ (X.d x✝² x✝³).unop = 0

Tactic:
by

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
i j : ι
hij : ¬c.Rel i j
⊢ (X.d j i).unop = 0

Tactic:
by

Goal state after:
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 L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i : Option ι
j : ι
hj : i = some j
⊢ X K i = K.X j

Tactic:
by

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

Goal state before:
pp: ι : 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
i : Option ι
hi : i = none
⊢ IsZero (X K i)

Tactic:
by

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✝⁴).unop ≫ (X.d x✝² x✝³).unop = 0

Tactic:
by

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

Goal state before:
pp: ι : 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
i j : Option ι
hi : i = none
⊢ d K i j = 0

Tactic:
by

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✝ Y✝ : (HomologicalComplex V c)ᵒᵖ
f : X✝ ⟶ Y✝
i j : ι
x✝ : c.symm.Rel i j
⊢ (f.unop.f i).op ≫ (unop Y✝).op.d i j = (unop X✝).op.d i j ≫ (f.unop.f j).op

Tactic:
by

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) =
    δ (-1) 0
        (-(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:
by

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✝ Y✝ : HomologicalComplex Vᵒᵖ c.symm
f : X✝ ⟶ Y✝
i j : ι
x✝ : c.Rel i j
⊢ (f.f i).unop ≫ X✝.unopSymm.d i j = Y✝.unopSymm.d i j ≫ (f.f j).unop

Tactic:
by

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

Goal state before:
pp: ι : 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
i j : Option ι
hj : j = none
⊢ d K i j = 0

Tactic:
by

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)ᵒᵖ
i j : ι
x✝ : c.Rel i j
⊢ (Iso.refl ((unop X).op.unopSymm.X i)).hom ≫ (unop X).d i j =
    (unop X).op.unopSymm.d i j ≫ (Iso.refl ((unop X).op.unopSymm.X j)).hom

Tactic:
by

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₃
⊢ MappingConeCompHomotopyEquiv.hom f g ≫ MappingConeCompHomotopyEquiv.inv f g = 𝟙 (mappingCone g)

Tactic:
by

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

Goal state before:
pp: ι : 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
i j : Option ι
a b : ι
hi : i = some a
hj : j = some b
⊢ d K i j = (XIso K hi).hom ≫ K.d a b ≫ (XIso K hj).inv

Tactic:
by

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₃
⊢ (mappingConeCompHomotopyEquiv f g).hom ≫ (mappingConeCompHomotopyEquiv f g).inv = 𝟙 (mappingCone g)

Tactic:
by

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

Goal state before:
pp: ι : 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
i j x✝ : Option ι
⊢ (XOpIso K none).hom ≫ (d K x✝ none).op = d K.op none x✝ ≫ (XOpIso K x✝).hom

Tactic:
by

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₃
⊢ inr (map f (f ≫ g) (𝟙 X₁) g ⋯) ≫ (mappingConeCompHomotopyEquiv f g).inv = (mappingConeCompTriangle f g).mor₂

Tactic:
by

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₃
⊢ (mappingConeCompHomotopyEquiv f g).hom ≫ (triangle (mappingConeCompTriangle f g).mor₁).mor₃ =
    (mappingConeCompTriangle f g).mor₃

Tactic:
by

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 Y : (HomologicalComplex V c)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (HomologicalComplex V c)ᵒᵖ).map f ≫
        (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom =
      (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫
        (opFunctor V c ⋙ opInverse V c).map f

Tactic:
by

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 Y : (HomologicalComplex V c)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (HomologicalComplex V c)ᵒᵖ).map f ≫
        (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom =
      (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫
        (opFunctor V c ⋙ opInverse V c).map f

Tactic:
by
      intro X Y f
      refine Quiver.Hom.unop_inj ?_
      ext x
      simp

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)ᵒᵖ
⊢ (opFunctor V c).map ((opUnitIso V c).hom.app X) ≫ (opCounitIso V c).hom.app ((opFunctor V c).obj X) =
    𝟙 ((opFunctor V c).obj X)

Tactic:
by

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

Goal state before:
pp: ι : 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
i✝ j✝ : Option ι
i j : ι
⊢ (XOpIso K (some i)).hom ≫ (d K (some j) (some i)).op = d K.op (some i) (some j) ≫ (XOpIso K (some j)).hom

Tactic:
by

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✝ Y✝ : (HomologicalComplex Vᵒᵖ c)ᵒᵖ
f : X✝ ⟶ Y✝
i j : ι
x✝ : c.symm.Rel i j
⊢ (f.unop.f i).unop ≫ (unop Y✝).unop.d i j = (unop X✝).unop.d i j ≫ (f.unop.f j).unop

Tactic:
by

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✝ Y✝ : HomologicalComplex V c.symm
f : X✝ ⟶ Y✝
i j : ι
x✝ : c.Rel i j
⊢ (f.f i).op ≫ X✝.opSymm.d i j = Y✝.opSymm.d i j ≫ (f.f j).op

Tactic:
by

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

Goal state before:
pp: ι : 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
i j : Option ι
val✝ : ι
⊢ (XOpIso K (some val✝)).hom ≫ (d K none (some val✝)).op = d K.op (some val✝) none ≫ (XOpIso K none).hom

Tactic:
by

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)ᵒᵖ
i j : ι
x✝ : c.Rel i j
⊢ (Iso.refl ((unop X).op.unopSymm.X i)).hom ≫ (unop X).d i j =
    (unop X).op.unopSymm.d i j ≫ (Iso.refl ((unop X).op.unopSymm.X j)).hom

Tactic:
by

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₃
⊢ (mappingConeCompTriangleh f g).mor₂ ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (inr (mappingConeCompTriangle f g).mor₁)

Tactic:
by

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₃
inst✝ : HasZeroObject C
⊢ (mappingConeCompTriangleh f g).mor₁ ≫ (Iso.refl (mappingConeCompTriangleh f g).obj₂).hom =
    (Iso.refl (mappingConeCompTriangleh f g).obj₁).hom ≫ (mappingCone.triangleh (mappingConeCompTriangle f g).mor₁).mor₁

Tactic:
by

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₃
inst✝ : HasZeroObject C
⊢ (mappingConeCompTriangleh f g).mor₂ ≫ (isoOfHomotopyEquiv (mappingConeCompHomotopyEquiv f g)).hom =
    (Iso.refl (mappingConeCompTriangleh f g).obj₂).hom ≫ (mappingCone.triangleh (mappingConeCompTriangle f g).mor₁).mor₂

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
i : Option ι
a : ι
hi : i = some a
⊢ mapX φ i = (XIso K hi).hom ≫ φ.f a ≫ (XIso L hi).inv

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : K ⟶ L
i : Option ι
hi : i = none
⊢ mapX φ i = 0

Tactic:
by

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 Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (HomologicalComplex Vᵒᵖ c)ᵒᵖ).map f ≫
        (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom =
      (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫
        (unopFunctor V c ⋙ unopInverse V c).map f

Tactic:
by

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 Y : (HomologicalComplex Vᵒᵖ c)ᵒᵖ} (f : X ⟶ Y),
    (𝟭 (HomologicalComplex Vᵒᵖ c)ᵒᵖ).map f ≫
        (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop Y).op.unopSymm.X x)) ⋯).op.hom =
      (Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).op.hom ≫
        (unopFunctor V c ⋙ unopInverse V c).map f

Tactic:
by
      intro X Y f
      refine Quiver.Hom.unop_inj ?_
      ext x
      simp

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₃
inst✝ : HasZeroObject C
⊢ (quotient C (ComplexShape.up ℤ)).map
        ((mappingCone.triangle g).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (mappingCone.inr f)) ≫
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone f) =
    (quotient C (ComplexShape.up ℤ)).map (mappingConeCompHomotopyEquiv f g).hom ≫
      (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯)).mor₃ ≫
        (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone f)

Tactic:
← Functor.map_comp_assoc

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₃
inst✝ : HasZeroObject C
⊢ (quotient C (ComplexShape.up ℤ)).map
        ((mappingCone.triangle g).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (mappingCone.inr f)) ≫
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone f) =
    (quotient C (ComplexShape.up ℤ)).map
        ((mappingConeCompHomotopyEquiv f g).hom ≫ (mappingCone.triangle (mappingCone.map f (f ≫ g) (𝟙 X₁) g ⋯)).mor₃) ≫
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone f)
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)ᵒᵖ
⊢ (unopFunctor V c).map ((unopUnitIso V c).hom.app X) ≫ (unopCounitIso V c).hom.app ((unopFunctor V c).obj X) =
    𝟙 ((unopFunctor V c).obj X)

Tactic:
by

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
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
⊢ ((opFunctor V c).obj (op K)).HasHomology i

Tactic:
by

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₃
inst✝ : HasZeroObject C
⊢ mappingConeCompTriangleh f g ∈ distinguishedTriangles

Tactic:
by

Goal state after: