mathlib-initiative/mathlib-tactics huggingface dataset:
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
a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T a₃
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h : a₁ + a₂ + a₃ = a
⊢ a₁ + a₂₃ = a

Tactic:
by lia

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
a₁ a₂ a₃ a₁₂ a₂₃ a : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T a₃
h₁₂ : a₁ + a₂ = a₁₂
h₂₃ : a₂ + a₃ = a₂₃
h : a₁ + a₂ + a₃ = a
⊢ ↑a₃ + ↑a₂ + ↑a₁ = ↑a

Tactic:
by lia

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
a₁ a₃ a₁₃ : ℕ
α : Ext X Y a₁
β : Ext Y Z 0
γ : Ext Z T a₃
h₁₃ : a₁ + a₃ = a₁₃
⊢ (α.comp β ⋯).comp γ h₁₃ = α.comp (β.comp γ ⋯) h₁₃

Tactic:
apply comp_assoc
  lia

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
a₁ a₂ a₁₂ : ℕ
α : Ext X Y a₁
β : Ext Y Z a₂
γ : Ext Z T 0
h₁₂ : a₁ + a₂ = a₁₂
⊢ (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ ⋯) h₁₂

Tactic:
apply comp_assoc
  lia

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
inst✝ : HasDerivedCategory C
a b : ℕ
α : Ext X Y a
β : Ext Y Z b
c : ℕ
h : a + b = c
⊢ ↑b + ↑a = ↑c

Tactic:
by lia

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

Goal state before:
pp: case pos
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∃ j, c.Rel i j
⊢ IsZero (S.X₃.homology i)

pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
⊢ IsZero (S.X₃.homology i)

Tactic:
·

Goal state after:
case pos
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∃ j, c.Rel i j
⊢ IsZero (S.X₃.homology i)
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.hf
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ }.f =
    0

pp: case pos.hg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ }.g =
    0

Tactic:
·

Goal state after:
case pos.hf
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ }.f =
    0
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case pos.hg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ }.g =
    0

Tactic:
·

Goal state after:
case pos.hg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
j : ι
hij : c.Rel i j
this : Mono (HomologicalComplex.homologyMap S.f j)
⊢ { X₁ := S.X₂.homology i, X₂ := S.X₃.homology i, X₃ := S.X₁.homology j, f := HomologicalComplex.homologyMap S.g i,
        g := hS.δ i j hij, zero := ⋯ }.g =
    0
Module: Mathlib.Algebra.Homology.HomologySequenceLemmas

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
⊢ IsZero (S.X₃.homology i)

Tactic:
·

Goal state after:
case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h₁ : Epi (HomologicalComplex.homologyMap S.f i)
h₂ : ∀ (j : ι), c.Rel i j → Mono (HomologicalComplex.homologyMap S.f j)
hi : ∀ (j : ι), ¬c.Rel i j
⊢ IsZero (S.X₃.homology i)
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 lia

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

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₁ ≫
      (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₂).hom =
    (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom ≫ (triangleOfSES hS).mor₁

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₂ ≫
      (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom =
    (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₂).hom ≫ (triangleOfSES hS).mor₂

pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map
        (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom =
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom ≫ (triangleOfSES hS).mor₃

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₁ ≫
      (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₂).hom =
    (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom ≫ (triangleOfSES hS).mor₁
Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₂ ≫
      (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom =
    (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₂).hom ≫ (triangleOfSES hS).mor₂

pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map
        (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom =
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom ≫ (triangleOfSES hS).mor₃

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₂ ≫
      (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom =
    (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₂).hom ≫ (triangleOfSES hS).mor₂
Module: Mathlib.Algebra.Homology.DerivedCategory.ShortExact

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map
        (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom =
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom ≫ (triangleOfSES hS).mor₃

Tactic:
·

Goal state after:
case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).mor₃ ≫
      (shiftFunctor (DerivedCategory C) 1).map
        (Iso.refl (Q.mapTriangle.obj (CochainComplex.mappingCone.triangle S.f)).obj₁).hom =
    (asIso (Q.map (CochainComplex.mappingCone.descShortComplex S))).hom ≫ (triangleOfSES hS).mor₃
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case e_a
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 (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp α'.hom ⋯ = α.hom

pp: case e_a
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 (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp β'.hom ⋯ = β.hom

Tactic:
·

Goal state after:
case e_a
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 (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp α'.hom ⋯ = α.hom
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case e_a
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 (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp β'.hom ⋯ = β.hom

Tactic:
·

Goal state after:
case e_a
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 (α' + β') ⋯
eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom)
⊢ (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).hom.comp β'.hom ⋯ = β.hom
Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₁ ≫ (e.app S.X₂).hom = (e.app S.X₁).hom ≫ (triangleOfSES ⋯).mor₁

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₂ ≫ (e.app S.X₃).hom = (e.app S.X₂).hom ≫ (triangleOfSES ⋯).mor₂

pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₃ ≫ (shiftFunctor (DerivedCategory C) 1).map (e.app S.X₁).hom =
    (e.app S.X₃).hom ≫ (triangleOfSES ⋯).mor₃

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₁ ≫ (e.app S.X₂).hom = (e.app S.X₁).hom ≫ (triangleOfSES ⋯).mor₁
Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₂ ≫ (e.app S.X₃).hom = (e.app S.X₂).hom ≫ (triangleOfSES ⋯).mor₂

pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₃ ≫ (shiftFunctor (DerivedCategory C) 1).map (e.app S.X₁).hom =
    (e.app S.X₃).hom ≫ (triangleOfSES ⋯).mor₃

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₂ ≫ (e.app S.X₃).hom = (e.app S.X₂).hom ≫ (triangleOfSES ⋯).mor₂
Module: Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle

Goal state before:
pp: case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₃ ≫ (shiftFunctor (DerivedCategory C) 1).map (e.app S.X₁).hom =
    (e.app S.X₃).hom ≫ (triangleOfSES ⋯).mor₃

Tactic:
·

Goal state after:
case refine_3
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
S : ShortComplex C
hS : S.ShortExact
e : (SingleFunctors.evaluation C (DerivedCategory C) 0).obj (singleFunctors C) ≅
  (SingleFunctors.evaluation C (DerivedCategory C) 0).obj ((CochainComplex.singleFunctors C).postcomp Q) :=
  (SingleFunctors.evaluation C (DerivedCategory C) 0).mapIso (singleFunctorsPostcompQIso C)
⊢ hS.singleTriangle.mor₃ ≫ (shiftFunctor (DerivedCategory C) 1).map (e.app S.X₁).hom =
    (e.app S.X₃).hom ≫ (triangleOfSES ⋯).mor₃
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 0 = 0

Tactic:
zero_hom

Goal state after:
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
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := ⋯
⊢ (∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w', max u v}
          ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))) →
    ∀ (X Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)

pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := ⋯
⊢ (∀ (X Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)) →
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w', max u v}
          ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := ⋯
⊢ (∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w', max u v}
          ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))) →
    ∀ (X Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := ⋯
⊢ (∀ (X Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)) →
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w', max u v}
          ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
this : HasDerivedCategory C := ⋯
⊢ (∀ (X Y : C) (n : ℕ), Small.{w', max u v} (ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) ↑n)) →
    ∀ (X Y : C) (n : ℤ),
      0 ≤ n →
        Small.{w', max u v}
          ((singleFunctor C 0).obj X ⟶ (shiftFunctor (DerivedCategory C) n).obj ((singleFunctor C 0).obj Y))
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)
A' : C
π : A' ⟶ A
w✝¹ : Epi π
x' : A' ⟶ (mappingCone S.f).X n₀
w✝ : x' ≫ (mappingCone S.f).d n₀ n₁ = 0
hx' :
  π ≫ x = HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫ HomologicalComplex.homologyπ (mappingCone S.f) n₀
a : A' ⟶ S.X₁.X n₁
b : A' ⟶ S.X₂.X n₀
w : a ≫ S.X₁.d n₁ (n₁ + 1) = 0 ∧ a ≫ S.f.f n₁ + b ≫ S.X₂.d n₀ n₁ = 0
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ 1 + n₀ = n₁

Tactic:
by lia

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ 0 + 1 = 1

Tactic:
by lia

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ 1 + n = n'

Tactic:
by lia

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₁ Y n
n' : ℕ
h : 1 + n = n'
⊢ 0 + 1 + n = n'

Tactic:
by lia

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ 1 + 0 = 1

Tactic:
by lia

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ 0 + n = n

Tactic:
by lia

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
γ : Ext S.X₂ Y n
n' : ℕ
h : 1 + n = n'
⊢ 1 + 0 + n = n'

Tactic:
by lia

Goal state after: