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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
A : C
i : ι
γ : A ⟶ K.homology i
j : ι
hj : c.next i = j
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ z, ∃ (hz : z ≫ K.d i j = 0), π ≫ γ = K.liftCycles z j hj hz ≫ K.homologyπ i

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
A : C
x₂ : A ⟶ K.X j
hx₂ : x₂ ≫ K.d j k = 0
⊢ K.liftCycles x₂ k hk hx₂ ≫ K.homologyπ j = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ K.d i j

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
A : C
x₂ x₂' : A ⟶ K.X j
hx₂ : x₂ ≫ K.d j k = 0
hx₂' : x₂' ≫ K.d j k = 0
⊢ K.liftCycles x₂ k hk hx₂ ≫ K.homologyπ j = K.liftCycles x₂' k hk hx₂' ≫ K.homologyπ j ↔
    ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = π ≫ x₂' + x₁ ≫ K.d i j

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hi : c.prev j = i
A : C
z₂ : A ⟶ K.cycles j
⊢ z₂ ≫ K.homologyπ j = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ z₂ = x₁ ≫ K.toCycles i j

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hi : c.prev j = i
A : C
z₂ z₂' : A ⟶ K.cycles j
⊢ z₂ ≫ K.homologyπ j = z₂' ≫ K.homologyπ j ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ z₂ = π ≫ z₂' + x₁ ≫ K.toCycles i j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n : ℕ
α : Ext X Y n
m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
⊢ α.comp (-β) h = -α.comp β h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z : C
n m : ℕ
β : Ext Y Z m
p : ℕ
h : n + m = p
⊢ comp 0 β h = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K : HomologicalComplex C c
A : C
i : ι
z : A ⟶ K.X i
j : ι
hj : c.prev i = j
⊢ z ≫ K.pOpcycles i = 0 ↔ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ z = x ≫ K.d j i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁✝ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃✝ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
f₂ : A ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₁ : C
π₁ : A₁ ⟶ A
w✝² : Epi π₁
f₁ :
  A₁ ⟶
    ((mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
            (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).sc
        ⋯ 0 ⋯).X₁
hf₁ : π₁ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
h₃ : (f₁ ≫ app' φ 1 ⋯) ≫ R₂.map' 1 2 ⋯ ⋯ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
w✝¹ : Epi π₂
g₀ :
  A₂ ⟶
    ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
            (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
        ⋯ 0 ⋯).X₁
hg₀ :
  π₂ ≫ f₁ ≫ app' φ 1 ⋯ =
    g₀ ≫
      ((mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
              (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).sc
          ⋯ 0 ⋯).f
A₃ : C
π₃ : A₃ ⟶ A₂
w✝ : Epi π₃
f₀ : A₃ ⟶ R₁.obj' 0 mono_of_epi_of_mono_of_mono'._proof_13
hf₀ : π₃ ≫ g₀ = f₀ ≫ app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13
⊢ f₀ ≫ R₁.map' 0 1 ⋯ ⋯ = π₃ ≫ π₂ ≫ f₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
Z : C
m p : ℕ
h : n + m = p
⊢ α.comp 0 h = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
⊢ Mono (homologyMap φ j) ↔
    ∀ ⦃A : C⦄ (x₂ : A ⟶ K.X j),
      x₂ ≫ K.d j k = 0 →
        ∀ (y₁ : A ⟶ L.X i), x₂ ≫ φ.f j = y₁ ≫ L.d i j → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ K.d i j

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
⊢ (mk₀ (𝟙 X)).comp α ⋯ = α

Tactic:
by

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
K L : HomologicalComplex C c
φ : K ⟶ L
i j k : ι
hi : c.prev j = i
hk : c.next j = k
⊢ Epi (homologyMap φ j) ↔
    ∀ ⦃A : C⦄ (y₂ : A ⟶ L.X j),
      y₂ ≫ L.d j k = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₂, ∃ (_ : x₂ ≫ K.d j k = 0), ∃ y₁, π ≫ y₂ = x₂ ≫ φ.f j + y₁ ≫ L.d i j

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C₁ : Type u₁
inst✝¹⁷ : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst✝¹⁶ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst✝¹⁵ : AddMonoid M
inst✝¹⁴ : HasShift C₁ M
inst✝¹³ : HasShift C₂ M
inst✝¹² : Φ.functor.CommShift M
X₁ Y₁ Z₁ : C₁
X₂ Y₂ Z₂ : C₂
inst✝¹¹ : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst✝¹⁰ : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst✝⁹ : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst✝⁸ : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor.obj X₁ ≅ X₂
eY : Φ.functor.obj Y₁ ≅ Y₂
eZ : Φ.functor.obj Z₁ ≅ Z₂
inst✝⁷ : W₁.IsCompatibleWithShift M
inst✝⁶ : W₂.IsCompatibleWithShift M
inst✝⁵ : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst✝⁴ : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst✝³ : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst✝² : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst✝¹ : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst✝ : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
⊢ Φ.smallShiftedHomMap eX eZ (f.comp g h) = (Φ.smallShiftedHomMap eX eY f).comp (Φ.smallShiftedHomMap eY eZ g) h

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
n : ℕ
α : Ext X Y n
⊢ α.comp (mk₀ (𝟙 Y)) ⋯ = α

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
⊢ mk₀ 0 = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
T : Triangle (CochainComplex C ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ 1 + n₀ = n₁

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
T : Triangle (CochainComplex C ℤ)
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (homologyFunctor C (up ℤ) 0).homologySequenceδ ((quotient C (up ℤ)).mapTriangle.obj T) n₀ n₁ h =
    (homologyFunctorFactors C (up ℤ) n₀).hom.app T.obj₃ ≫
      (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap T.mor₃ n₀ n₁ ⋯ ≫
        (homologyFunctorFactors C (up ℤ) n₁).inv.app T.obj₁

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
⊢ HomComplex.δ (-1) 0 0 = HomComplex.Cochain.ofHom (S.f ≫ S.g)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
⊢ inr S.f ≫ descShortComplex S = S.g

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
f g : X ⟶ Y
⊢ mk₀ (f + g) = mk₀ f + mk₀ g

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
⊢ Q.map (CochainComplex.mappingCone.descShortComplex S) ≫ triangleOfSESδ hS =
    Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
n : ℕ
x y : Ext X Y 0
⊢ homEquiv₀.symm (homEquiv₀.toFun (x + y)) = homEquiv₀.symm (homEquiv₀.toFun x + homEquiv₀.toFun y)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
n : ℤ
⊢ (inr S.f).f n ≫ (descShortComplex S).f n = S.g.f n

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
f : X ⟶ Y
⊢ mk₀ (-f) = -mk₀ f

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
i j : ℤ
h : i + -1 = j
⊢ (inl S.f).v i j h ≫ (descShortComplex S).f j = 0

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
f : S₁ ⟶ S₂
⊢ map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ descShortComplex S₂ = descShortComplex S₁ ≫ f.τ₃

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
Y : C
n : ℕ
X₁ X₂ : C
α β : Ext (X₁ ⊞ X₂) Y n
h₁ : (mk₀ biprod.inl).comp α ⋯ = (mk₀ biprod.inl).comp β ⋯
h₂ : (mk₀ biprod.inr).comp α ⋯ = (mk₀ biprod.inr).comp β ⋯
⊢ α = β

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
⊢ β.hom = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
β : Ext 0 Y n := 0
hβ : β.hom = 0
⊢ 0 = comp 0 β ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
⊢ hom 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
⊢ α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
hS₁ : S₁.ShortExact
hS₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ triangleOfSESδ hS₁ ≫ (shiftFunctor (DerivedCategory C) 1).map (Q.map f.τ₁) = Q.map f.τ₃ ≫ triangleOfSESδ hS₂

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α ⋯
β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
⊢ α' + β' = homEquiv.symm (α'.hom + β'.hom)

Tactic:
by

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
A : C
x : A ⟶ (HomologicalComplex.homologyFunctor C (up ℤ) n₀).obj (mappingCone S.f)
⊢ (up ℤ).next n₀ = n₁

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
⊢ triangleOfSES hS ≅ Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0
hR₁' :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
⊢ Mono (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
⊢ triangleOfSES hS ∈ distinguishedTriangles

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (triangleOfSES h₁).mor₁ ≫ Q.map f.τ₂ = Q.map f.τ₁ ≫ (triangleOfSES h₂).mor₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ : R₁.Exact
hR₂ : R₂.Exact
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₁ : Mono (app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
⊢ R₁.map' 0 2 mono_of_epi_of_mono_of_mono'._proof_2 mono_of_epi_of_mono_of_mono'._proof_4 = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (triangleOfSES h₁).mor₂ ≫ Q.map f.τ₃ = Q.map f.τ₂ ≫ (triangleOfSES h₂).mor₂

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Q.map ((CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map f.τ₁) ≫
      (Functor.commShiftIso Q 1).hom.app S₂.X₁ =
    Q.map (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯) ≫
      Q.map (CochainComplex.mappingCone.triangle S₂.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S₂.X₁

Tactic:
← Functor.map_comp_assoc

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ Q.map ((CochainComplex.mappingCone.triangle S₁.f).mor₃ ≫ (shiftFunctor (CochainComplex C ℤ) 1).map f.τ₁) ≫
      (Functor.commShiftIso Q 1).hom.app S₂.X₁ =
    Q.map (CochainComplex.mappingCone.map S₁.f S₂.f f.τ₁ f.τ₂ ⋯ ≫ (CochainComplex.mappingCone.triangle S₂.f).mor₃) ≫
      (Functor.commShiftIso Q 1).hom.app S₂.X₁
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
A₁ : C
π₁ : A₁ ⟶ A
w✝ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4
⊢ f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
S₁ S₂ : ShortComplex (CochainComplex C ℤ)
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ (triangleOfSES h₁).mor₃ ≫ (shiftFunctor (DerivedCategory C) 1).map (Q.map f.τ₁) = Q.map f.τ₃ ≫ (triangleOfSES h₂).mor₃

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
⊢ hS.singleTriangle ≅ triangleOfSES ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
S₁ S₂ : ShortComplex C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ h₁.singleTriangle.mor₁ ≫ (singleFunctor C 0).map f.τ₂ = (singleFunctor C 0).map f.τ₁ ≫ h₂.singleTriangle.mor₁

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
S₁ S₂ : ShortComplex C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ h₁.singleTriangle.mor₂ ≫ (singleFunctor C 0).map f.τ₃ = (singleFunctor C 0).map f.τ₂ ≫ h₂.singleTriangle.mor₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
R₁ R₂ : ComposableArrows C 3
φ : R₁ ⟶ R₂
hR₁ :
  (mk₂ (R₁.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)
      (R₁.map' 2 3 mono_of_epi_of_mono_of_mono'._proof_4 mono_of_epi_of_mono_of_mono'._proof_7)).Exact
hR₂ :
  (mk₂ (R₂.map' 0 1 mono_of_epi_of_mono_of_mono'._proof_9 mono_of_epi_of_mono_of_mono'._proof_11)
      (R₂.map' 1 2 mono_of_epi_of_mono_of_mono'._proof_6 mono_of_epi_of_mono_of_mono'._proof_4)).Exact
hR₂' : R₂.map' 1 3 mono_of_epi_of_mono_of_mono'._proof_11 mono_of_epi_of_mono_of_mono'._proof_7 = 0
h₀ : Epi (app' φ 0 mono_of_epi_of_mono_of_mono'._proof_13)
h₂✝ : Epi (app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4)
h₃✝ : Mono (app' φ 3 mono_of_epi_of_mono_of_mono'._proof_7)
A : C
g₁ : A ⟶ R₂.obj' 1 mono_of_epi_of_mono_of_mono'._proof_11
A₁ : C
π₁ : A₁ ⟶ A
w✝¹ : Epi π₁
f₂ : A₁ ⟶ R₁.obj' 2 mono_of_epi_of_mono_of_mono'._proof_4
h₁ : π₁ ≫ g₁ ≫ R₂.map' 1 2 ⋯ ⋯ = f₂ ≫ app' φ 2 mono_of_epi_of_mono_of_mono'._proof_4
h₂ : f₂ ≫ R₁.map' 2 3 ⋯ ⋯ = 0
A₂ : C
π₂ : A₂ ⟶ A₁
w✝ : Epi π₂
f₁ : A₂ ⟶ R₁.obj 1
h₃ : π₂ ≫ f₂ = f₁ ≫ R₁.map (homOfLE ⋯)
⊢ (π₂ ≫ π₁ ≫ g₁ - f₁ ≫ app' φ 1 mono_of_epi_of_mono_of_mono'._proof_11) ≫ R₂.map' 1 2 ⋯ ⋯ = 0

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α β : Ext X Y n
⊢ (α + β).hom = α.hom + β.hom

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
S₁ S₂ : ShortComplex C
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
f : S₁ ⟶ S₂
⊢ h₁.singleTriangle.mor₃ ≫ (shiftFunctor (DerivedCategory C) 1).map ((singleFunctor C 0).map f.τ₁) =
    (singleFunctor C 0).map f.τ₃ ≫ h₂.singleTriangle.mor₃

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
n : ℕ
inst✝ : HasDerivedCategory C
α : Ext X Y n
⊢ (-α).hom = -α.hom

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y Z T : C
n✝ : ℕ
inst✝ : HasDerivedCategory C
n : ℕ
⊢ ∀ (x y : Ext X Y n), homEquiv.toFun (x + y) = homEquiv.toFun x + homEquiv.toFun y

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y Z T : C
n a b c : ℕ
h : a + b = c
α : Ext X Y a
⊢ ∀ (a_1 b_1 : Ext Y Z b), α.comp (a_1 + b_1) h = α.comp a_1 h + α.comp b_1 h

Tactic:
by

Goal state after: