mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), P.trW f → P.trW g → P.trW (f ≫ g)

Tactic:
rw [← trW_isoClosure]

Goal state after:
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
⊢ ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), P.isoClosure.trW f → P.isoClosure.trW g → P.isoClosure.trW (f ≫ g)
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : Category.{v_4, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
⊢ (G.shiftIso n a a' ha').hom ≫ (iso a).inv ≫ (iso a).hom =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom

Tactic:
Iso.inv_hom_id,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : Category.{v_4, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
⊢ (G.shiftIso n a a' ha').hom ≫ 𝟙 (G.functor a) =
    whiskerRight (iso a').inv (shiftFunctor D n) ≫ (F.shiftIso n a a' ha').hom ≫ (iso a).hom
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : Category.{v_4, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
⊢ (G.shiftIso n a a' ha').hom =
    whiskerRight ((iso a').inv ≫ (iso a').hom) (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom

Tactic:
Iso.inv_hom_id,

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Category.{v_3, u_3} E
inst✝⁴ : Category.{v_4, u_4} E'
A : Type u_5
inst✝³ : AddMonoid A
inst✝² : HasShift D A
inst✝¹ : HasShift E A
inst✝ : HasShift E' A
F G H : SingleFunctors C D A
iso : (a : A) → F.functor a ≅ G.functor a
comm :
  ∀ (n a a' : A) (ha' : n + a = a'),
    (F.shiftIso n a a' ha').hom ≫ (iso a).hom =
      whiskerRight (iso a').hom (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
n a a' : A
ha' : n + a = a'
⊢ (G.shiftIso n a a' ha').hom = whiskerRight (𝟙 (G.functor a')) (shiftFunctor D n) ≫ (G.shiftIso n a a' ha').hom
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
E' : Type u_4
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Category.{v_3, u_3} E
inst✝⁵ : Category.{v_4, u_4} E'
A : Type u_5
inst✝⁴ : AddMonoid A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : HasShift E' A
F G✝ H : SingleFunctors C D A
G : D ⥤ E
inst✝ : G.CommShift A
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
⊢ (F.functor a'').associator G (shiftFunctor E (m + n)) ≪≫
      (F.functor a'').isoWhiskerLeft (commShiftIso G (m + n)).symm ≪≫
        ((F.functor a'').associator (shiftFunctor D (m + n)) G).symm ≪≫ isoWhiskerRight (F.shiftIso (m + n) a a'' ⋯) G =
    (F.functor a'' ⋙ G).isoWhiskerLeft (shiftFunctorAdd E m n) ≪≫
      ((F.functor a'' ⋙ G).associator (shiftFunctor E m) (shiftFunctor E n)).symm ≪≫
        isoWhiskerRight
            ((F.functor a'').associator G (shiftFunctor E m) ≪≫
              (F.functor a'').isoWhiskerLeft (commShiftIso G m).symm ≪≫
                ((F.functor a'').associator (shiftFunctor D m) G).symm ≪≫ isoWhiskerRight (F.shiftIso m a' a'' ha'') G)
            (shiftFunctor E n) ≪≫
          (F.functor a').associator G (shiftFunctor E n) ≪≫
            (F.functor a').isoWhiskerLeft (commShiftIso G n).symm ≪≫
              ((F.functor a').associator (shiftFunctor D n) G).symm ≪≫ isoWhiskerRight (F.shiftIso n a a' ha') G

Tactic:
by
    ext X
    dsimp
    simp only [F.shiftIso_add_hom_app n m a a' a'' ha' ha'', Functor.commShiftIso_add,
      Functor.CommShift.isoAdd_inv_app, Functor.map_comp, id_comp, assoc,
      Functor.commShiftIso_inv_naturality_assoc]
    simp only [← G.map_comp, Iso.inv_hom_id_app_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasZeroObject C
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : Pretriangulated C
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P : ObjectProperty C
inst✝ : P.IsTriangulated
⊢ P.trW.IsStableUnderFiniteProducts

Tactic:
rw [← trW_isoClosure]

Goal state after:
C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasZeroObject C
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : Pretriangulated C
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P : ObjectProperty C
inst✝ : P.IsTriangulated
⊢ P.isoClosure.trW.IsStableUnderFiniteProducts
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: case mp
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i₁ i₂ : ι
⊢ c'.Rel (e.f i₁) (e.f i₂) → c.Rel i₁ i₂

pp: case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i₁ i₂ : ι
⊢ c.Rel i₁ i₂ → c'.Rel (e.f i₁) (e.f i₂)

Tactic:
· apply IsRelIff.rel'

Goal state after:
case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i₁ i₂ : ι
⊢ c.Rel i₁ i₂ → c'.Rel (e.f i₁) (e.f i₂)
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.Embedding.IsSupported

Goal state before:
pp: case mpr
ι : 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
⊢ IsZero K

Tactic:
IsZero.iff_id_eq_zero

Goal state after:
case mpr
ι : 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
⊢ 𝟙 K = 0
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:
IsZero.iff_id_eq_zero

Goal state after:
ι : 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'
⊢ 𝟙 (((F.mapHomologicalComplex c').obj K).X i') = 0
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
x✝ : ((F.mapHomologicalComplex c').obj K).IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ IsZero (K.X i')

Tactic:
IsZero.iff_id_eq_zero

Goal state after:
ι : 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
x✝ : ((F.mapHomologicalComplex c').obj K).IsStrictlySupported e
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ 𝟙 (K.X i') = 0
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mpr.right
p : ℤ
i : ℕ
hi : (up ℤ).Rel ((embeddingUpIntGE p).f i) ((embeddingUpIntGE p).f 0)
⊢ False

Tactic:
dsimp at hi

Goal state after:
case mpr.right
p : ℤ
i : ℕ
hi : p + ↑i + 1 = p + 0
⊢ False
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: case mpr.right
p : ℤ
i : ℕ
hi : (up ℤ).Rel ((embeddingUpIntLE p).f 0) ((embeddingUpIntLE p).f i)
⊢ False

Tactic:
dsimp at hi

Goal state after:
case mpr.right
p : ℤ
i : ℕ
hi : p - 0 + 1 = p - ↑i
⊢ False
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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

Tactic:
rw [← d_comp_eq_zero_iff K e hj' hi hi' cocone.π, cocone.condition]

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
⊢ K.homologyπ j' ≫
      (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').inv ≫
        (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').inv ≫
      (K.restriction e).homologyπ j ≫ (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom

Tactic:
Iso.inv_hom_id,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
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
⊢ K.homologyπ j' ≫ 𝟙 (K.homology j') =
    (K.restrictionCyclesIso e j k hk hj' hk' hk'').inv ≫
      (K.restriction e).homologyπ j ≫ (K.restrictionHomologyIso e i j k hi hk hi' hj' hk' hi'' hk'').hom
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.sc j).iCycles =
    (K.sc j).homologyData.left.cyclesIso.hom ≫
      (K.sc j).homologyData.left.i ≫ (K.extendXIso e hj').inv ≫ (K.extendXIso e hj').hom

Tactic:
Iso.inv_hom_id,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (K.sc j).iCycles = (K.sc j).homologyData.left.cyclesIso.hom ≫ (K.sc j).homologyData.left.i ≫ 𝟙 (K.X j)
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.cyclesIso.hom ≫
      (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.π ≫
        (K.sc j).homologyData.left.homologyIso.inv ≫ (K.sc j).homologyData.left.homologyIso.hom =
    (K.extendCyclesIso e hj').hom ≫ (K.sc j).homologyπ ≫ (K.sc j).homologyData.left.homologyIso.hom

Tactic:
Iso.inv_hom_id,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.cyclesIso.hom ≫
      (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.π ≫
        𝟙 (extend.homologyData' K e hj' ⋯ ⋯ (K.sc j).homologyData).left.H =
    (K.extendCyclesIso e hj').hom ≫ (K.sc j).homologyπ ≫ (K.sc j).homologyData.left.homologyIso.hom
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ K.pOpcycles j ≫ (K.extendOpcyclesIso e hj').inv ≫ (K.extendOpcyclesIso e hj').hom =
    (K.extendXIso e hj').inv ≫ (K.extend e).pOpcycles j' ≫ (K.extendOpcyclesIso e hj').hom

Tactic:
Iso.inv_hom_id,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j : ι
j' : ι'
hj' : e.f j = j'
inst✝¹ : K.HasHomology j
inst✝ : (K.extend e).HasHomology j'
⊢ K.pOpcycles j ≫ 𝟙 (K.opcycles j) =
    (K.extendXIso e hj').inv ≫ (K.extend e).pOpcycles j' ≫ (K.extendOpcyclesIso e hj').hom
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
⊢ K.homologyι j' =
    K.homologyι j' ≫
      (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').inv ≫ (K.restrictionOpcyclesIso e i j hi hi' hj' hi'').hom

Tactic:
Iso.inv_hom_id,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
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
⊢ K.homologyι j' = K.homologyι j' ≫ 𝟙 (K.opcycles j')
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

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✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' j' : ι'
hij' : c'.Rel i' j'
hj : ¬∃ j, e.f j = j'
⊢ ⋯.δ i' j' hij' = 0

Tactic:
apply ((K.truncLE e).exactAt_of_isSupported e j'
      (by simpa using hj)).isZero_homology.eq_of_tgt

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 B : C
f : A ⟶ B
⊢ f = f ≫ (singleObjHomologySelfIso c j B).inv ≫ (singleObjHomologySelfIso c j B).hom

Tactic:
Iso.inv_hom_id,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ f = f ≫ 𝟙 B
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 B : C
f : A ⟶ B
⊢ opcyclesMap ((single C c j).map f) j ≫ (singleObjOpcyclesSelfIso c j B).inv ≫ (singleObjOpcyclesSelfIso c j B).hom =
    (singleObjOpcyclesSelfIso c j A).inv ≫ f ≫ (singleObjOpcyclesSelfIso c j B).hom

Tactic:
Iso.inv_hom_id,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : C
f : A ⟶ B
⊢ opcyclesMap ((single C c j).map f) j ≫ 𝟙 (((single C c j).obj B).opcycles j) =
    (singleObjOpcyclesSelfIso c j A).inv ≫ f ≫ (singleObjOpcyclesSelfIso c j B).hom
Module: Mathlib.CategoryTheory.Localization.HomEquiv

Goal state before:
pp: C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
⊢ (homEquiv W L₁ L₂) (isoOfHom L₁ W f hf).inv ≫ (isoOfHom L₂ W f hf).hom =
    (isoOfHom L₂ W f hf).inv ≫ (isoOfHom L₂ W f hf).hom

Tactic:
Iso.inv_hom_id,

Goal state after:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
⊢ (homEquiv W L₁ L₂) (isoOfHom L₁ W f hf).inv ≫ (isoOfHom L₂ W f hf).hom = 𝟙 (L₂.obj X)
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y X' Y' : C
e : X ≅ X'
e' : Y ≅ Y'
⊢ HasSmallLocalizedHom W X Y ↔ HasSmallLocalizedHom W X' Y'

Tactic:
simp only [hasSmallLocalizedHom_iff W W.Q]
  exact small_congr (Iso.homCongr (W.Q.mapIso e) (W.Q.mapIso e'))

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

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
inst✝² : HasShift D M
L : C ⥤ D
inst✝¹ : L.IsLocalization W
inst✝ : L.CommShift M
X Y : C
eq :
  ∀ (a b : M),
    Small.{w, v₂} (L.obj ((shiftFunctor C a).obj X) ⟶ L.obj ((shiftFunctor C b).obj Y)) ↔
      Small.{w, v₂} ((shiftFunctor D a).obj (L.obj X) ⟶ (shiftFunctor D b).obj (L.obj Y))
⊢ (∀ (a b : M), HasSmallLocalizedHom W ((shiftFunctor C a).obj X) ((shiftFunctor C b).obj Y)) ↔
    ∀ (a b : M), Small.{w, v₂} ((shiftFunctor D a).obj (L.obj X) ⟶ (shiftFunctor D b).obj (L.obj Y))

Tactic:
simp only [hasSmallLocalizedHom_iff _ L, eq]

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 simp [mk₀_add]

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 4
hR₁ : R₁.Exact
hR₂ : R₂.Exact
φ : R₁ ⟶ R₂
h₀ : Epi (app' φ 0 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2)
h₁ : IsIso (app' φ 1 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4)
h₃ : IsIso (app' φ 3 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6)
h₄ : Mono (app' φ 4 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7)
⊢ IsIso (app' φ 2 isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9)

Tactic:
dsimp at h₀ h₁ h₃ h₄
  have : Mono (app' φ 2) := by
    apply mono_of_epi_of_mono_of_mono (δlastFunctor.map φ) (R₁.exact_iff_δlast.1 hR₁).1
      (R₂.exact_iff_δlast.1 hR₂).1 <;> dsimp <;> infer_instance
  have : Epi (app' φ 2) := by
    apply epi_of_epi_of_epi_of_mono (δ₀Functor.map φ) (R₁.exact_iff_δ₀.1 hR₁).2
      (R₂.exact_iff_δ₀.1 hR₂).2 <;> dsimp <;> infer_instance
  apply isIso_of_mono_of_epi

Goal state after: