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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
T : Triangle C
⊢ (shiftFunctorAdd' C (a + b) c (a + b + c) ⋯).hom.app T ≫
      (shiftFunctor C c).map ((shiftFunctorAdd' C a b (a + b) ⋯).hom.app T) =
    eqToHom ⋯ ≫
      (shiftFunctorAdd' C a (b + c) (a + (b + c)) ⋯).hom.app T ≫
        (shiftFunctorAdd' C b c (b + c) ⋯).hom.app ((shiftFunctor C a).obj T)

Tactic:
ext
        all_goals
          dsimp
          rw [← shiftFunctorAdd'_assoc_hom_app a b c _ _ _ rfl rfl (add_assoc a b c)]
          dsimp only [CategoryTheory.shiftFunctorAdd']
          simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
⊢ shiftFunctorAdd (Triangle C) a b = shiftFunctorAdd' C a b (a + b) ⋯

Tactic:
apply shiftFunctorAdd_eq

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
a : (contractibleTriangle X).obj₁ ⟶ T.obj₁
ha₁ : (contractibleTriangle X).mor₁ ≫ f = a ≫ T.mor₁
right✝ : (contractibleTriangle X).mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map a = 0 ≫ T.mor₃
⊢ f = a ≫ T.mor₁

Tactic:
by simpa using ha₁

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₂ : IsZero T.obj₂
h₁ : 𝟙 T.obj₁ = 0
⊢ 𝟙 ((CategoryTheory.shiftFunctor C 1).obj T.obj₁) = 0

Tactic:
← Functor.map_id,

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₂ : IsZero T.obj₂
h₁ : 𝟙 T.obj₁ = 0
⊢ (CategoryTheory.shiftFunctor C 1).map (𝟙 T.obj₁) = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₁ : T.mor₁ = 0
h₃ : T.mor₃ = 0
this : Epi T.mor₂
f : T.obj₃ ⟶ T.obj₂
hf : 𝟙 T.obj₂ = T.mor₂ ≫ f
⊢ f ≫ T.mor₂ = 𝟙 T.obj₃

Tactic:
rw [← cancel_epi T.mor₂, comp_id, ← reassoc_of% hf]

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

Goal state before:
pp: case h₃
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Category.{v_3, u_3} E
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasShift D ℤ
inst✝³ : HasShift E ℤ
F : C ⥤ D
inst✝² : F.CommShift ℤ
G : D ⥤ E
inst✝¹ : G.CommShift ℤ
inst✝ : F.Faithful
X Y : Triangle C
f g : X ⟶ Y
h : F.mapTriangle.map f = F.mapTriangle.map g
⊢ F.map f.hom₃ = F.map g.hom₃

Tactic:
exact congr_arg TriangleMorphism.hom₃ h

Goal state after:
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

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

Tactic:
ext X
    dsimp
    simp only [id_comp, ← Functor.map_comp]
    congr
    simpa only [← cancel_epi ((shiftFunctor C a).map ((shiftFunctorAdd C m n).hom.app X)),
      shiftFunctorAdd'_eq_shiftFunctorAdd, ← Functor.map_comp_assoc, Iso.hom_inv_id_app,
      Functor.map_id, id_comp] using! shiftFunctorAdd'_assoc_inv_app m n a (m + n) a' a'' rfl ha'
        (by rw [← ha'', ← ha', add_assoc]) X

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (whiskeringLeftFunctor L W E).IsEquivalence

Tactic:
let iso : (whiskeringLeft (MorphismProperty.Localization W) D E).obj
    (equivalenceFromModel L W).functor ⋙
      (Construction.whiskeringLeftEquivalence W E).functor ≅ whiskeringLeftFunctor L W E :=
    NatIso.ofComponents (fun F => eqToIso (by
      ext
      change (W.Q ⋙ Localization.Construction.lift L (inverts L W)) ⋙ F = L ⋙ F
      rw [Construction.fac])) (fun τ => by
        ext
        dsimp [Construction.whiskeringLeftEquivalence, equivalenceFromModel, whiskerLeft]
        rw [ObjectProperty.eqToHom_hom, ObjectProperty.eqToHom_hom, eqToHom_app, eqToHom_app,
          eqToHom_refl, eqToHom_refl]
        dsimp
        rw [comp_id, id_comp]
        rfl)

Goal state after:
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
iso : (whiskeringLeft W.Localization D E).obj (equivalenceFromModel L W).functor ⋙
    (Construction.whiskeringLeftEquivalence W E).functor ≅
  whiskeringLeftFunctor L W E :=
  NatIso.ofComponents (fun F ↦ eqToIso ⋯) ⋯
⊢ (whiskeringLeftFunctor L W E).IsEquivalence
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₄, u₄} D₁
inst✝⁴ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝³ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝² : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝¹ : CatCommSq Φ.functor L₁ L₂ G
inst✝ : G.IsEquivalence
⊢ (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence

Tactic:
by
    rw [Φ.isEquivalence_iff W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q) L₁ L₂ G]
    exact inferInstance

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
⊢ CommShift (Lifting.iso L W F F').hom A

Tactic:
let := Functor.commShiftOfLocalization L W A F F'
  constructor
  intro a
  ext X
  simp only [comp_app, Functor.whiskerRight_app, Functor.whiskerLeft_app,
    Functor.commShiftIso_comp_hom_app,
    Functor.commShiftOfLocalization_iso_hom_app,
    Category.assoc, ← Functor.map_comp, ← Functor.map_comp_assoc,
    Iso.hom_inv_id_app, Functor.map_id, Iso.inv_hom_id_app,
    Category.comp_id, Category.id_comp, Functor.comp_obj]

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case succ
C : Type u
inst✝⁵ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁴ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝³ : LinearOrder β
inst✝² : OrderBot β
inst✝¹ : SuccOrder β
inst✝ : WellFoundedLT β
b : β
hb : ¬IsMax b
hb' : P.strictLimitsClosureIter J b ≤ P.limitsClosure J
⊢ transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (Order.succ b) P ≤ P.limitsClosure J

Tactic:
transfiniteIterate_succ _ _ _ hb,

Goal state after:
case succ
C : Type u
inst✝⁵ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁴ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝³ : LinearOrder β
inst✝² : OrderBot β
inst✝¹ : SuccOrder β
inst✝ : WellFoundedLT β
b : β
hb : ¬IsMax b
hb' : P.strictLimitsClosureIter J b ≤ P.limitsClosure J
⊢ (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) b P).strictLimitsClosureStep J ≤ P.limitsClosure J
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case succ
C : Type u
inst✝¹⁰ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁹ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁸ : LinearOrder β
inst✝⁷ : OrderBot β
inst✝⁶ : SuccOrder β
inst✝⁵ : WellFoundedLT β
inst✝⁴ : ObjectProperty.Small.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β}, b ≤ c → ∀ [Small.{w, w'} ↑(Set.Iio c)], Small.{w, w'} ↑(Set.Iio b)
b : β
hb : ¬IsMax b
hb' : ∀ [hb₀ : Small.{w, w'} ↑(Set.Iio b)], ObjectProperty.Small.{w, v, u} (P.strictLimitsClosureIter J b)
hb₀ : Small.{w, w'} ↑(Set.Iio (Order.succ b))
this : Small.{w, w'} ↑(Set.Iio b)
⊢ ObjectProperty.Small.{w, v, u} (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (Order.succ b) P)

Tactic:
transfiniteIterate_succ _ _ _ hb,

Goal state after:
case succ
C : Type u
inst✝¹⁰ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁹ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝⁸ : LinearOrder β
inst✝⁷ : OrderBot β
inst✝⁶ : SuccOrder β
inst✝⁵ : WellFoundedLT β
inst✝⁴ : ObjectProperty.Small.{w, v, u} P
inst✝³ : LocallySmall.{w, v, u} C
inst✝² : Small.{w, t} α
inst✝¹ : ∀ (a : α), Small.{w, u'} (J a)
inst✝ : ∀ (a : α), LocallySmall.{w, v', u'} (J a)
H : ∀ {b c : β}, b ≤ c → ∀ [Small.{w, w'} ↑(Set.Iio c)], Small.{w, w'} ↑(Set.Iio b)
b : β
hb : ¬IsMax b
hb' : ∀ [hb₀ : Small.{w, w'} ↑(Set.Iio b)], ObjectProperty.Small.{w, v, u} (P.strictLimitsClosureIter J b)
hb₀ : Small.{w, w'} ↑(Set.Iio (Order.succ b))
this : Small.{w, w'} ↑(Set.Iio b)
⊢ ObjectProperty.Small.{w, v, u}
    ((transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) b P).strictLimitsClosureStep J)
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
E : Type u_3
inst✝⁴ : Category.{v_2, u_3} E
inst✝³ : HasShift E A
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
a : G
⊢ ⨆ a, P.shift a ≤ (⨆ a, P.shift a).shift a

Tactic:
rw [shift_iSup]

Goal state after:
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
E : Type u_3
inst✝⁴ : Category.{v_2, u_3} E
inst✝³ : HasShift E A
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
a : G
⊢ ⨆ a, P.shift a ≤ ⨆ i, (P.shift i).shift a
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasShift D ℤ
inst✝⁹ : Preadditive D
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁷ : Pretriangulated D
inst✝⁶ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝⁵ : HasZeroObject C
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : Abelian A
inst✝ : F.IsHomological
X₁ X₂ : C
this✝¹ : HasBinaryBiproduct (F.obj X₁) (F.obj X₂)
this✝ : Mono (F.biprodComparison X₁ X₂)
this : PreservesBinaryBiproduct X₁ X₂ F
⊢ PreservesLimit (pair X₁ X₂) F

Tactic:
apply Limits.preservesBinaryProduct_of_preservesBinaryBiproduct

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

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasShift C ℤ
inst✝¹ : Category.{v_3, u_3} A
F : C ⥤ A
inst✝ : F.ShiftSequence ℤ
T T' : Triangle C
φ : T ⟶ T'
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (F.shift n₀).map φ.hom₃ ≫ F.shiftMap T'.mor₃ n₀ n₁ ⋯ = F.shiftMap T.mor₃ n₀ n₁ ⋯ ≫ (F.shift n₁).map φ.hom₁

Tactic:
rw [← shiftMap_comp', ← φ.comm₃, shiftMap_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
⊢ (mk₀ m₀ hm₀ f).comp g ⋯ = f ≫ g

Tactic:
subst hm₀

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
⊢ (mk₀ 0 ⋯ f).comp g ⋯ = f ≫ g
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
g : Y ⟶ Z
⊢ f.comp (mk₀ m₀ hm₀ g) ⋯ = f ≫ (shiftFunctor C a).map g

Tactic:
subst hm₀

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
a : M
f : ShiftedHom X Y a
g : Y ⟶ Z
⊢ f.comp (mk₀ 0 ⋯ g) ⋯ = f ≫ (shiftFunctor C a).map g
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
X Y : C
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
F : C ⥤ D
inst✝ : F.CommShift M
⊢ (mk₀ m₀ hm₀ f).map F = mk₀ m₀ hm₀ (F.map f)

Tactic:
subst hm₀

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
X Y : C
f : X ⟶ Y
F : C ⥤ D
inst✝ : F.CommShift M
⊢ (mk₀ 0 ⋯ f).map F = mk₀ 0 ⋯ (F.map f)
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
P : ObjectProperty C
F : D ⥤ C
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor D 1).obj X
hT : Triangle.mk s g h ∈ distinguishedTriangles
eq₁ : (P.inverseImage F).trW s ↔ P.inverseImage F Z
eq₂ : P.trW (F.map s) ↔ P (F.obj Z)
⊢ (P.inverseImage F).trW s ↔ P.trW (F.map s)

Tactic:
eq₁,

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
P : ObjectProperty C
F : D ⥤ C
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : P.IsClosedUnderIsomorphisms
X Y : D
s : X ⟶ Y
Z : D
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor D 1).obj X
hT : Triangle.mk s g h ∈ distinguishedTriangles
eq₁ : (P.inverseImage F).trW s ↔ P.inverseImage F Z
eq₂ : P.trW (F.map s) ↔ P (F.obj Z)
⊢ P.inverseImage F Z ↔ P.trW (F.map s)
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
F₁ F₂ : SingleFunctors C D A
φ : F₁ ⟶ F₂
n a a' : A
ha' : n + a = a'
X : C
⊢ (((F₁.postcomp G).shiftIso n a a' ha').hom ≫ whiskerRight (φ.hom a) G).app X =
    (whiskerRight (whiskerRight (φ.hom a') G) (shiftFunctor E n) ≫ ((F₂.postcomp G).shiftIso n a a' ha').hom).app X

Tactic:
simpa using G.congr_map (congr_app (φ.comm n a a' ha') X)

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
J : Type
x✝ : Finite J
⊢ P.isoClosure.trW.IsStableUnderProductsOfShape J

Tactic:
refine MorphismProperty.IsStableUnderProductsOfShape.mk _ _ ?_

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
J : Type
x✝ : Finite J
⊢ ∀ (X₁ X₂ : J → C) [inst : HasProduct X₁] [inst_1 : HasProduct X₂] (f : (j : J) → X₁ j ⟶ X₂ j),
    (∀ (j : J), P.isoClosure.trW (f j)) → P.isoClosure.trW (Limits.Pi.map f)
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 : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ K.d i' (e.f j) ≫ (eqToIso ⋯).hom ≫ ψ.f (e.f j) ≫ (L.extendXIso e ⋯).hom = 0

Tactic:
eqToIso_refl,

Goal state after:
ι : 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 : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
j : ι
hj : e.BoundaryGE j
i' : ι'
hij' : c'.Rel i' (e.f j)
this : (L.extend e).d i' (e.f j) = 0
⊢ K.d i' (e.f j) ≫ (Iso.refl ((K.restriction e).X j)).hom ≫ ψ.f (e.f j) ≫ (L.extendXIso e ⋯).hom = 0
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
j k : ι
j' : ι'
hj' : e.f j = j'
hj : e.BoundaryGE j
hjk : ¬c.Rel j k
⊢ (K.homologyι j' ≫ (K.truncGE'XIsoOpcycles e hj' hj).inv) ≫ (K.truncGE' e).d j k = 0

Tactic:
· rw [shape _ _ _ hjk, comp_zero]

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

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 M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁵ : e.IsTruncGE
inst✝⁴ : ∀ (i' : ι'), K.HasHomology i'
inst✝³ : ∀ (i' : ι'), L.HasHomology i'
inst✝² : ∀ (i' : ι'), M.HasHomology i'
inst✝¹ : HasZeroObject C
ι'' : Type u_4
c'' : ComplexShape ι''
e' : c''.Embedding c'
inst✝ : K.IsStrictlySupported e'
⊢ ∀ (i' : ι'), (∀ (i : ι''), e'.f i ≠ i') → IsZero ((K.truncGE e).X i')

Tactic:
by
    intro i' hi'
    by_cases hi'' : ∃ i, e.f i = i'
    · obtain ⟨i, hi⟩ := hi''
      by_cases hi''' : e.BoundaryGE i
      · rw [IsZero.iff_id_eq_zero, ← cancel_epi
          ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIsoOpcycles e hi hi''').inv,
          ← cancel_epi (HomologicalComplex.pOpcycles _ _)]
        apply (K.isZero_X_of_isStrictlySupported e' i' hi').eq_of_src
      · exact (K.isZero_X_of_isStrictlySupported e' i' hi').of_iso
          ((K.truncGE' e).extendXIso e hi ≪≫ K.truncGE'XIso e hi hi''')
    · exact (K.truncGE e).isZero_X_of_isStrictlySupported e _ (by simpa using hi'')

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

Goal state before:
pp: case hK
ι : 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₂
K L : HomologicalComplex C c
inst✝¹ : K.IsStrictlySupported e₁
inst✝ : L.IsStrictlySupported e₂
φ : K ⟶ L
⊢ K.IsStrictlySupportedOutside e₂

Tactic:
rw [ac.isStrictlySupportedOutside₂_iff]

Goal state after:
case hK
ι : 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₂
K L : HomologicalComplex C c
inst✝¹ : K.IsStrictlySupported e₁
inst✝ : L.IsStrictlySupported e₂
φ : K ⟶ L
⊢ K.IsStrictlySupported e₁
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
inst✝ : HasSmallLocalizedShiftedHom W M X Y
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
⊢ (equiv W L) (mk₀ W m₀ hm₀ f) = ShiftedHom.mk₀ m₀ hm₀ (L.map f)

Tactic:
subst hm₀

Goal state after:
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
inst✝ : HasSmallLocalizedShiftedHom W M X Y
f : X ⟶ Y
⊢ (equiv W L) (mk₀ W 0 ⋯ f) = ShiftedHom.mk₀ 0 ⋯ (L.map f)
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
X Y : C
inst✝⁴ : HasSmallLocalizedShiftedHom W M X Y
inst✝³ : HasSmallLocalizedShiftedHom W M Y Y
inst✝² : HasSmallLocalizedShiftedHom W M Y X
inst✝¹ : W.IsCompatibleWithShift M
inst✝ : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
⊢ m₀ + m₀ = m₀

Tactic:
subst hm₀

Goal state after:
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
X Y : C
inst✝⁴ : HasSmallLocalizedShiftedHom W M X Y
inst✝³ : HasSmallLocalizedShiftedHom W M Y Y
inst✝² : HasSmallLocalizedShiftedHom W M Y X
inst✝¹ : W.IsCompatibleWithShift M
inst✝ : W.RespectsIso
f : Y ⟶ X
hf : W f
⊢ 0 + 0 = 0