mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
        (i m₃).inv.app ((shiftFunctor C (m₁ + m₂)).obj X) ≫
          (s m₃).map (F.map ((shiftFunctorAdd C m₁ m₂).hom.app X)) ≫
            (s m₃).map ((i m₂).inv.app ((shiftFunctor C m₁).obj X)) ≫
              𝟙 ((s m₃).obj ((F ⋙ s m₂).obj ((shiftFunctor C m₁).obj X))) =
    (eqToHom ⋯).app (F.obj X) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
          (i (m₂ + m₃)).inv.app ((shiftFunctor C m₁).obj X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X))

Tactic:
Category.comp_id,

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
⊢ (i (m₁ + m₂ + m₃)).hom.app X ≫
      F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
        (i m₃).inv.app ((shiftFunctor C (m₁ + m₂)).obj X) ≫
          (s m₃).map (F.map ((shiftFunctorAdd C m₁ m₂).hom.app X)) ≫
            (s m₃).map ((i m₂).inv.app ((shiftFunctor C m₁).obj X)) =
    (eqToHom ⋯).app (F.obj X) ≫
      (i (m₁ + (m₂ + m₃))).hom.app X ≫
        F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
          (i (m₂ + m₃)).inv.app ((shiftFunctor C m₁).obj X) ≫
            (s (m₂ + m₃)).map ((i m₁).inv.app X) ≫
              (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X)) ≫ (s m₃).map ((s m₂).map ((i m₁).hom.app X))
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ : ℤ
γ✝ γ₁ γ₂ : Cochain K L n✝
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p + n' = p'
⊢ p + n' + a = p' + a

Tactic:
hp'

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ : ℤ
γ✝ γ₁ γ₂ : Cochain K L n✝
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p + n' = p'
⊢ p' + a = p' + a
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
n : A
X : C
⊢ eqToHom ⋯ ≫
      (i n).hom.app X ≫
        eqToHom ⋯ ≫
          F.map ((shiftFunctorAdd C n 0).hom.app X) ≫
            (i 0).inv.app ((shiftFunctor C n).obj X) ≫ 𝟙 ((s 0).obj (F.obj ((shiftFunctor C n).obj X))) =
    (eqToHom ⋯).app (F.obj X) ≫ (Induced.zero F s i).inv.app ((s n).obj (F.obj X)) ≫ (s 0).map ((i n).hom.app X)

Tactic:
Category.comp_id,

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
n : A
X : C
⊢ eqToHom ⋯ ≫
      (i n).hom.app X ≫
        eqToHom ⋯ ≫ F.map ((shiftFunctorAdd C n 0).hom.app X) ≫ (i 0).inv.app ((shiftFunctor C n).obj X) =
    (eqToHom ⋯).app (F.obj X) ≫ (Induced.zero F s i).inv.app ((s n).obj (F.obj X)) ≫ (s 0).map ((i n).hom.app X)
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 : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
⊢ T₁ ≅ T₂

Tactic:
by
  have h := exists_iso_of_arrow_iso T₁ T₂ hT₁ hT₂ (Arrow.isoMk e₁ e₂ comm.symm)
  exact Triangle.isoMk _ _ e₁ e₂ (Triangle.π₃.mapIso h.choose) comm (by
    have eq := h.choose_spec.2
    dsimp at eq ⊢
    conv_rhs => rw [← eq, ← TriangleMorphism.comm₂]) (by
    have eq := h.choose_spec.1
    dsimp at eq ⊢
    conv_lhs => rw [← eq, TriangleMorphism.comm₃])

Goal state after:
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
φ : V ⥤q C
⊢ of V ⋙q (lift φ).toPrefunctor = φ

Tactic:
fapply Prefunctor.ext

Goal state after:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
φ : V ⥤q C
⊢ ∀ (X : V), (of V ⋙q (lift φ).toPrefunctor).obj X = φ.obj X

case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
φ : V ⥤q C
⊢ ∀ (X Y : V) (f : X ⟶ Y), (of V ⋙q (lift φ).toPrefunctor).map f = Eq.recOn ⋯ (Eq.recOn ⋯ (φ.map f))
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
hG : G.FullyFaithful
⊢ Nonempty (Φ.localizedFunctor W₁.Q W₂.Q).FullyFaithful

Tactic:
Φ.nonempty_fullyFaithful_iff W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q) L₁ L₂ G

Goal state after:
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
hG : G.FullyFaithful
⊢ Nonempty G.FullyFaithful
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
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₃} C₃
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
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₂
h : Φ.IsLocalizedFullyFaithful
inst✝ : CatCommSq Φ.functor L₁ L₂ G
⊢ Nonempty G.FullyFaithful

Tactic:
rw [Φ.nonempty_fullyFaithful_iff L₁ L₂ G W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)]
    exact h.nonempty_fullyFaithful

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: case hφ₂
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f₁ f₂ : L.obj X ⟶ L.obj Y
g : L.obj Y ⟶ L.obj Z
α : W.LeftFraction₂ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
β : W.LeftFraction Y Z
hβ : g = β.map L ⋯
γ : W.LeftFraction α.Y' β.Y'
hγ : β.f ≫ γ.s = α.s ≫ γ.f
⊢ f₂ ≫ g = { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f' ≫ γ.f, s := β.s ≫ γ.s, hs := ⋯ }.snd.map L ⋯

Tactic:
rw [h₂, hβ]
    exact LeftFraction.map_comp_map_eq_map _ _ _ hγ _

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
a b : A
X : C
| F'.map
      ((commShiftIso L b).inv.app ((shiftFunctor C a).obj X) ≫
        𝟙 (L.obj ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)))) ≫
    (Lifting.iso L W F F').hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
          (shiftFunctorAdd E a b).inv.app (F.obj X) ≫ (shiftFunctor E (a + b)).map ((Lifting.iso L W F F').inv.app X)

Tactic:
Category.comp_id,

Goal state after:
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
a b : A
X : C
| F'.map ((commShiftIso L b).inv.app ((shiftFunctor C a).obj X)) ≫
    (Lifting.iso L W F F').hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
          (shiftFunctorAdd E a b).inv.app (F.obj X) ≫ (shiftFunctor E (a + b)).map ((Lifting.iso L W F F').inv.app X)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
inst✝⁷ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁶ : L.IsLocalization W
E : Type u_3
inst✝⁵ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝⁴ : W.HasLeftCalculusOfFractions
inst✝³ : Preadditive D
inst✝² : Preadditive E
inst✝¹ : L.Additive
inst✝ : F.Additive
h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0
X₁ X₂ : C
f g : X₁ ⟶ X₂
hfg : F.map (L.map f) = F.map (L.map g)
⊢ L.map f = L.map g

Tactic:
rw [← sub_eq_zero, ← L.map_sub]

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
inst✝⁷ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁶ : L.IsLocalization W
E : Type u_3
inst✝⁵ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝⁴ : W.HasLeftCalculusOfFractions
inst✝³ : Preadditive D
inst✝² : Preadditive E
inst✝¹ : L.Additive
inst✝ : F.Additive
h : ∀ ⦃X₁ X₂ : C⦄ (f : X₁ ⟶ X₂), F.map (L.map f) = 0 → L.map f = 0
X₁ X₂ : C
f g : X₁ ⟶ X₂
hfg : F.map (L.map f) = F.map (L.map g)
⊢ L.map (f - g) = 0
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
a : α
X : C
hX : (P.limitsClosure J).LimitOfShape (J a) X
⊢ P.limitsClosure J X

Tactic:
exact .of_limitPresentation hX.toLimitPresentation hX.prop_diag_obj

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

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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map L.op ⋯
⊢ φ.map L.op ⋯ = (φ.unop.map L ⋯).op

Tactic:
MorphismProperty.RightFraction.op_map

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
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
f : L.obj X ⟶ L.obj Y
φ : W.op.LeftFraction (Opposite.op Y) (Opposite.op X)
eq : f.op = φ.map L.op ⋯
⊢ φ.map L.op ⋯ = φ.unop.op.map L.op ⋯
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 : C
a : M
f : ShiftedHom X Y a
m₀ : M
hm₀ : m₀ = 0
⊢ f.comp (mk₀ m₀ hm₀ (𝟙 Y)) ⋯ = f

Tactic:
simp [comp_mk₀]

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

Goal state before:
pp: case h₁₂
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 T : C
f : X ⟶ Y
g : Y ⟶ Z
d : M
h : ShiftedHom Z T d
⊢ 0 + 0 = 0

pp: case h
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 T : C
f : X ⟶ Y
g : Y ⟶ Z
d : M
h : ShiftedHom Z T d
⊢ d + 0 + 0 = d

Tactic:
all_goals simp

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

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
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
a : A
X : C
⊢ (F.shiftIso 0 a a ⋯).hom.app X = (shiftFunctorZero D A).hom.app ((F.functor a).obj X)

Tactic:
rw [shiftIso_zero]

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
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
a : A
X : C
⊢ ((F.functor a).isoWhiskerLeft (shiftFunctorZero D A)).hom.app X = (shiftFunctorZero D A).hom.app ((F.functor a).obj X)
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

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
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
a : A
X : C
⊢ (F.shiftIso 0 a a ⋯).inv.app X = (shiftFunctorZero D A).inv.app ((F.functor a).1 X)

Tactic:
rw [shiftIso_zero]

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
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : SingleFunctors C D A
a : A
X : C
⊢ ((F.functor a).isoWhiskerLeft (shiftFunctorZero D A)).inv.app X = (shiftFunctorZero D A).inv.app ((F.functor a).1 X)
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
Y Z✝ Z' : C
f₁ f₂ : Y ⟶ Z✝
s : Z✝ ⟶ Z'
hf₁ : f₁ ≫ s = f₂ ≫ s
Z : C
g : Z ⟶ Z✝
h : Z' ⟶ (shiftFunctor C 1).obj Z
H : Triangle.mk g s h ∈ distinguishedTriangles
mem : P Z
⊢ (f₁ - f₂) ≫ s = 0

Tactic:
rw [sub_comp, hf₁, sub_self]

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
F : C ⥤ D
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : F.Full
n : ℤ
Y : D
X : C
e : F.obj X ≅ Y
⊢ F.essImage.shift n Y

Tactic:
exact ⟨X⟦n⟧, ⟨(F.commShiftIso n).app _ ≪≫ (shiftFunctor D n).mapIso e⟩⟩

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
hT : DerivedCategory.Q.mapTriangle.obj T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ DerivedCategory.HomologySequence.δ (DerivedCategory.Q.mapTriangle.obj T) n₀ n₁ ⋯ ≫
      (DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₁ ≫ homologyMap T.mor₁ n₁ =
    (DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃ ≫ 0

Tactic:
← DerivedCategory.homologyFunctorFactors_hom_naturality

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
hT : DerivedCategory.Q.mapTriangle.obj T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ DerivedCategory.HomologySequence.δ (DerivedCategory.Q.mapTriangle.obj T) n₀ n₁ ⋯ ≫
      (DerivedCategory.homologyFunctor C n₁).map (DerivedCategory.Q.map T.mor₁) ≫
        (DerivedCategory.homologyFunctorFactors C n₁).hom.app T.obj₂ =
    (DerivedCategory.homologyFunctorFactors C n₀).hom.app T.obj₃ ≫ 0
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: ι : Type u_1
V : Type u_2
inst✝² : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝¹ : HasZeroMorphisms V
K : HomologicalComplex V c
i : ι
inst✝ : K.HasHomology i
j : ι
⊢ (K.fromOpcycles i j).op ≫ (K.cyclesOpIso i).inv = K.op.toCycles j i

Tactic:
by
  by_cases hij : c.Rel i j
  · obtain rfl := c.next_eq' hij
    exact (K.sc i).fromOpcycles_op_cyclesOpIso_inv
  · rw [K.op.toCycles_eq_zero hij, K.fromOpcycles_eq_zero hij, op_zero, zero_comp]

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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝ : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
⊢ ((K.truncGE' e).sc' i j k).HasHomology

Tactic:
let φ := (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)

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.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hi : c.prev j = i
hk : c.next j = k
hj : ¬e.BoundaryGE j
this✝ : (K.restriction e).HasHomology j
this : ((K.restriction e).sc' i j k).HasHomology
φ : (shortComplexFunctor' C c i j k).obj (K.restriction e) ⟶ (shortComplexFunctor' C c i j k).obj (K.truncGE' e) :=
  (shortComplexFunctor' C c i j k).map (K.restrictionToTruncGE' e)
⊢ ((K.truncGE' e).sc' i j k).HasHomology
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'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : c.Rel j k
hk'' : e.f k = k'
⊢ K.d j k ≫ (K.extendXIso e hk'').inv = Cofork.π cocone ≫ f''

Tactic:
← cancel_epi (extendXIso K e hj').hom,

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'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : c.Rel j k
hk'' : e.f k = k'
⊢ (K.extendXIso e hj').hom ≫ K.d j k ≫ (K.extendXIso e hk'').inv = (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f''
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'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
h₁ : f' = 0
⊢ Cofork.π cocone ≫ f'' = Cofork.π cocone ≫ 0

Tactic:
← cancel_epi (extendXIso K e hj').hom,

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'
i j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk' : c'.next j' = k'
cocone : CokernelCofork (K.d i j)
hcocone : IsColimit cocone
W : C
f' : cocone.pt ⟶ K.X k
hf' : Cofork.π cocone ≫ f' = K.d j k
f'' : cocone.pt ⟶ (K.extend e).X k'
hf'' : (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extend e).d j' k'
φ : W ⟶ cocone.pt
hjk : ¬c.Rel j k
h₁ : f' = 0
⊢ (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ f'' = (K.extendXIso e hj').hom ≫ Cofork.π cocone ≫ 0
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 : HomologicalComplex C c
φ : K ⟶ L
e : c.Embedding c'
inst✝¹ : ∀ (j : ι), K.HasHomology j
inst✝ : ∀ (j : ι), L.HasHomology j
⊢ QuasiIso (extendMap φ e) ↔ QuasiIso φ

Tactic:
simp only [quasiIso_iff, ← fun j ↦ quasiIsoAt_extendMap_iff φ e (j := j) (hj' := rfl)]
  constructor
  · tauto
  · intro h j'
    by_cases hj' : ∃ j, e.f j = j'
    · obtain ⟨j, rfl⟩ := hj'
      exact h j
    · rw [quasiIsoAt_iff_exactAt]
      all_goals
        exact extend_exactAt _ _ _ (by simpa using hj')

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✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncLE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ (K.truncLE e).op.Acyclic ↔ K.op.IsSupportedOutside e.op

Tactic:
exact K.op.acyclic_truncGE_iff_isSupportedOutside e.op

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 ℤ
n : ℤ
⊢ K.IsGE n ↔ ∀ i < n, ExactAt K i

Tactic:
by
  constructor
  · intro _ i hi
    exact K.exactAt_of_isGE n i hi
  · intro h
    refine IsSupported.mk (fun i hi ↦ ?_)
    rw [notMem_range_embeddingUpIntGE_iff] at hi
    exact h i hi

Goal state after: