mathlib-initiative/mathlib-tactics huggingface dataset:
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₃
⊢ δ (-1) 0 ((Cochain.ofHom f).comp (inl g) ⋯) = Cochain.ofHom ((f ≫ g) ≫ inr g)

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

Tactic:
ext n
  simp [hom, inv, lift_desc_f _ _ _ _ _ _ _ n (n + 1) rfl, ext_from_iff _ (n + 1) _ rfl]

Goal state after:
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✝ : HasHomotopyCofiber φ
M : CochainComplex C ℤ
α : M ⟶ K
β : Cochain M L (-1)
hαβ : δ (-1) 0 β + Cochain.ofHom (α ≫ φ) = 0
⊢ -1 + 1 = 0

Tactic:
by simp

Goal state after:
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₁ ≫ (Iso.refl (triangle φ).rotate.obj₂).hom =
    (Iso.refl (triangle φ).rotate.obj₁).hom ≫ (mappingCone.triangle φ).mor₁

Tactic:
by simp

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

Goal state before:
pp: case mpr
p n : ℤ
⊢ p < n → ∀ (i : ℕ), (embeddingUpIntLE p).f i ≠ n

Tactic:
intros
    dsimp
    lia

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

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

Tactic:
intros
    dsimp
    lia

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 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
⊢ (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 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
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
⊢ (quotient C (ComplexShape.up ℤ)).map u₁₂ ≫ (Iso.refl { as := X₂ }).hom =
    (Iso.refl { as := X₁ }).hom ≫ (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₁

Tactic:
by 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
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
⊢ (quotient C (ComplexShape.up ℤ)).map u₂₃ ≫ (Iso.refl { as := X₃ }).hom =
    (Iso.refl { as := X₂ }).hom ≫ (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₁

Tactic:
by 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
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
⊢ u₁₂ ≫ u₂₃ = 𝟙 X₁ ≫ u₁₂ ≫ u₂₃

Tactic:
by rw [id_comp]

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
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
⊢ ∀ (i_1 : ι'),
    c'.Rel i_1 i' →
      (((single C c i).obj X).extend e).d i_1 i' ≫
          (((single C c i).obj X).extendXIso e h).hom ≫ (singleObjXSelf c i X).hom =
        0

Tactic:
by simp

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
inst✝¹ : DecidableEq ι
e : c.Embedding c'
X : C
inst✝ : DecidableEq ι'
i : ι
i' : ι'
h : e.f i = i'
⊢ ∀ (k : ι'),
    c'.Rel i' k →
      ((singleObjXSelf c i X).inv ≫ (((single C c i).obj X).extendXIso e h).inv) ≫
          (((single C c i).obj X).extend e).d i' k =
        0

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K K' : HomologicalComplex C c'
L L' : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
⊢ (fun φ ↦ e.liftExtend ↑φ ⋯) ((fun ψ ↦ ⟨e.homRestrict ψ, ⋯⟩) ψ) = ψ

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K K' : HomologicalComplex C c'
L L' : HomologicalComplex C c
inst✝ : e.IsRelIff
φ : { φ // e.HasLift φ }
⊢ (fun ψ ↦ ⟨e.homRestrict ψ, ⋯⟩) ((fun φ ↦ e.liftExtend ↑φ ⋯) φ) = φ

Tactic:
by simp

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

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✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : ∀ (i' : ι'), L.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hk' : c'.next j' = e.f k
hjk : c.Rel j k
⊢ (parallelPair ((K.truncGE' e).d j k) 0).map WalkingParallelPairHom.right ≫ (K.truncGE'XIso e ⋯ ⋯).hom =
    (K.truncGE'XIsoOpcycles e hj' hj).hom ≫
      (parallelPair (K.fromOpcycles j' (e.f k)) 0).map WalkingParallelPairHom.right

Tactic:
by simp

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

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'
inst✝² : e.IsRelIff
i j k : ι
hi : c.prev j = i
hk : c.next j = k
i' j' k' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hk' : e.f k = k'
hi'' : c'.prev j' = i'
hk'' : c'.next j' = k'
inst✝¹ : K.HasHomology j'
inst✝ : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
⊢ (K.sc' i' j' k').HasHomology

Tactic:
by subst hi'' hk''; assumption

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

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝¹ : Category.{v_1, u_4} C
inst✝ : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i : ι
⊢ ac.equiv (ac.equiv.symm i) = i

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₁ : ι₁
⊢ ac.equiv (Sum.inl i₁) = ac.equiv (ac.equiv.symm (e₁.f i₁))

Tactic:
by simp

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

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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
this : ∀ (i : ι) (i' : ι'), e.f i = i' → (QuasiIsoAt (truncGEMap φ e) i' ↔ QuasiIsoAt φ i')
h : ∀ (i : ι) (i' : ι'), e.f i = i' → QuasiIsoAt φ i'
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ QuasiIsoAt (truncGEMap φ e) i'

Tactic:
obtain ⟨i, hi⟩ := hi'
      simpa only [this i i' hi] using h i i' hi

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

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' j' : ι'
hj' : c'.Rel i' j'
⊢ { X₁ := (K.shortComplexTruncLE e).X₂.homology i', X₂ := (K.shortComplexTruncLE e).X₃.homology i',
        X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g i',
        g := ⋯.δ i' j' hj', zero := ⋯ }.g =
    0

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
X : ι → Type u_5
x₁ : (i₁ : ι₁) → X (e₁.f i₁)
x₂ : (i₂ : ι₂) → X (e₂.f i₂)
i₂ : ι₂
⊢ ac.equiv (Sum.inr i₂) = ac.equiv (ac.equiv.symm (e₂.f i₂))

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝¹ : HasZeroObject C
inst✝ : ∀ (i : ℤ), HasHomology K i
q : ℤ
k : ℕ
hq : q ≤ q + ↑k
⊢ (embeddingUpIntLE (q + ↑k)).f k = q

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝¹ : HasZeroObject C
inst✝ : ∀ (i : ℤ), HasHomology K i
n : ℤ
k : ℕ
hq : n ≤ n + ↑k
⊢ (embeddingUpIntGE n).f k = n + ↑k

Tactic:
by simp

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ (i : ℤ), n < i → ExactAt K i) → K.IsLE n

Tactic:
· intro h
    refine IsSupported.mk (fun i hi ↦ ?_)
    rw [notMem_range_embeddingUpIntLE_iff] at hi
    exact h i hi

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝² : HasZeroObject C
n : ℤ
inst✝¹ : K.IsStrictlyGE n
inst✝ : K.IsStrictlyLE n
⊢ mkHomToSingle (𝟙 (K.X n)) ⋯ ≫ mkHomFromSingle (𝟙 (K.X n)) ⋯ = 𝟙 K

Tactic:
ext i
        obtain hi | rfl | hi := lt_trichotomy i n
        · apply (K.isZero_of_isStrictlyGE n i (by lia)).eq_of_src
        · simp
        · apply (K.isZero_of_isStrictlyLE n i (by lia)).eq_of_tgt

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
A B : C
X : CochainComplex C ℤ
w✝² : X.IsStrictlyGE n
w✝¹ : X.IsStrictlyLE n
s : X ⟶ (CochainComplex.singleFunctor C n).obj A
w✝ : IsIso (Q.map s)
g : X ⟶ (CochainComplex.singleFunctor C n).obj B
A₀ : C
e : X ≅ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj A₀
φ : A₀ ⟶ A
hφ : (CochainComplex.singleFunctor C n).map φ = e.inv ≫ s
this✝² : IsIso ((singleFunctor C n).map φ)
this✝¹ : IsIso φ
this✝ : IsIso (e.inv ≫ s)
this : IsIso s
⊢ inv (Q.map s) ≫ Q.map g = Q.map (inv s ≫ g)

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ ((single C c j).obj A).d j (c.next j) = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
A : C
n : ℕ
⊢ n + 1 ≠ 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
inst✝ : L.IsLocalization W
X Y : C
⊢ HasSmallLocalizedHom W X Y

Tactic:
by
  rw [hasSmallLocalizedHom_iff W L]
  infer_instance

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

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n : ℤ
⊢ (embeddingUpIntGE n).f 0 = n

Tactic:
by simp

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

Goal state before:
pp: C✝ : Type u_1
inst✝⁵ : Category.{v_1, u_1} C✝
C : Type u_2
inst✝⁴ : Category.{?u.7, u_2} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n✝ n : ℤ
⊢ (embeddingUpIntLE n).f 0 = n

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K : CochainComplex C ℤ
n₀ n₁ : ℤ
inst✝² : Injective (K.X n₀)
inst✝¹ : Injective (K.X n₁)
inst✝ : K.IsStrictlyGE n₀
hK : ExactAt K n₀
h : n₀ + 1 = n₁
⊢ K.d n₀ n₁ ≫ pOpcycles K n₁ = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
K : CochainComplex C ℤ
n₀ n₁ : ℤ
inst✝² : Injective (K.X n₀)
inst✝¹ : Injective (K.X n₁)
inst✝ : K.IsStrictlyGE n₀
hK : ExactAt K n₀
h : n₀ + 1 = n₁
S : ShortComplex C :=
  { X₁ := K.X n₀, X₂ := K.X n₁, X₃ := opcycles K n₁, f := K.d n₀ n₁, g := pOpcycles K n₁, zero := ⋯ }
T : ShortComplex C := sc' K (n₀ - 1) n₀ n₁
⊢ (up ℤ).prev n₀ = n₀ - 1

Tactic:
by simp

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
a b : ℤ
inst✝ : HasDerivedCategory C
this :
  ∀ (a b : ℤ),
    Small.{w, w'}
      ((shiftFunctor (DerivedCategory C) a).obj ((singleFunctor C 0).obj X) ⟶
        (shiftFunctor (DerivedCategory C) b).obj ((singleFunctor C 0).obj Y))
φ : (singleFunctor C a).obj X ⟶ (singleFunctor C b).obj Y
⊢ -a + a = 0

Tactic:
by simp

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
a b : ℤ
inst✝ : HasDerivedCategory C
this :
  ∀ (a b : ℤ),
    Small.{w, w'}
      ((shiftFunctor (DerivedCategory C) a).obj ((singleFunctor C 0).obj X) ⟶
        (shiftFunctor (DerivedCategory C) b).obj ((singleFunctor C 0).obj Y))
φ : (singleFunctor C a).obj X ⟶ (singleFunctor C b).obj Y
⊢ -b + b = 0

Tactic:
by simp

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
f : X ⟶ Y
⊢ ↑0 = 0

Tactic:
by simp

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
f : X ⟶ Y
⊢ ↑0 = 0

Tactic:
by simp

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
this : HasDerivedCategory C := HasDerivedCategory.standard C
h : (singleFunctor C 0).FullyFaithful
⊢ ↑0 = 0

Tactic:
by simp

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
e : Φ.functor ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q :=
  CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)
⊢ b + 0 + 0 = b

Tactic:
by simp

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 simp

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

Goal state before:
pp: case h₁
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 := ⋯
β' : Ext (X ⊞ X) Y n := ⋯
eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') ⋯
⊢ (mk₀ biprod.inl).comp (α' + β') ⋯ = (mk₀ biprod.inl).comp (homEquiv.symm (α'.hom + β'.hom)) ⋯

Tactic:
ext; simp [α', β', ← Functor.map_comp]

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

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

Tactic:
ext; simp [α', β', ← Functor.map_comp]

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 simp

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)
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 ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀) ≫ (mappingCone S.f).d n₀ n₁) ≫ (↑(fst S.f)).v n₁ (n₁ + 1) ⋯ =
      0 ≫ (↑(fst S.f)).v n₁ (n₁ + 1) ⋯ ∧
    ((a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀) ≫ (mappingCone S.f).d n₀ n₁) ≫ (snd S.f).v n₁ n₁ ⋯ =
      0 ≫ (snd S.f).v n₁ n₁ ⋯
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h

Tactic:
add_comp,

Goal state after:
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 ≫ (inl S.f).v n₁ n₀ ⋯) ≫ (mappingCone S.f).d n₀ n₁ + (b ≫ (inr S.f).f n₀) ≫ (mappingCone S.f).d n₀ n₁) ≫
        (↑(fst S.f)).v n₁ (n₁ + 1) ⋯ =
      0 ≫ (↑(fst S.f)).v n₁ (n₁ + 1) ⋯ ∧
    ((a ≫ (inl S.f).v n₁ n₀ ⋯) ≫ (mappingCone S.f).d n₀ n₁ + (b ≫ (inr S.f).f n₀) ≫ (mappingCone S.f).d n₀ n₁) ≫
        (snd S.f).v n₁ n₁ ⋯ =
      0 ≫ (snd S.f).v n₁ n₁ ⋯
hab : x' = a ≫ (inl S.f).v n₁ n₀ ⋯ + b ≫ (inr S.f).f n₀
⊢ HomologicalComplex.liftCycles (mappingCone S.f) x' n₁ ⋯ w✝ ≫
      HomologicalComplex.homologyπ (mappingCone S.f) n₀ ≫
        (HomologicalComplex.homologyFunctor C (up ℤ) 0).shiftMap (triangle S.f).mor₃ n₀ n₁ ⋯ =
    HomologicalComplex.liftCycles S.X₃ (x' ≫ (descShortComplex S).f n₀) n₁ ⋯ ⋯ ≫
      HomologicalComplex.homologyπ S.X₃ n₀ ≫ hS.δ n₀ n₁ h
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 simp

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
n : ℕ
X₁ X₂ : Cᵒᵖ
f : X₁ ⟶ X₂
Y : C
⊢ ∀ (a b : Ext (Opposite.unop X₁) Y n),
    (Ext.mk₀ f.unop).comp (a + b) ⋯ = (Ext.mk₀ f.unop).comp a ⋯ + (Ext.mk₀ f.unop).comp b ⋯

Tactic:
by simp

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
J : Type u_1
inst✝ : Fintype J
X : J → C
c : Bicone X
hc : c.IsBilimit
Y : C
n : ℕ
x✝ : (i : J) → Ext (X i) Y n
i : J
⊢ i ∉ Finset.univ → (mk₀ (c.ι i ≫ c.π i)).comp (x✝ i) ⋯ = 0

Tactic:
by simp

Goal state after: