mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.6
inst✝ : Category.{v_1, ?u.6} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ g') =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) g'
this : f ≫ g'.cons p = Quiver.Path.cons (f ≫ g') p
⊢ Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (Quiver.Path.cons (f ≫ g') p) =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (g'.cons p)

Tactic:
simp only at ih ⊢

Goal state after:
case cons
V : Type u₁
inst✝¹ : Quiver V
C : Type ?u.6
inst✝ : Category.{v_1, ?u.6} C
φ : V ⥤q C
X✝ Y✝ Z✝ : Paths V
f : X✝ ⟶ Y✝
b✝ c✝ : Paths V
g' : Quiver.Path Y✝ b✝
p : b✝ ⟶ c✝
ih :
  Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ g') =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) g'
this : f ≫ g'.cons p = Quiver.Path.cons (f ≫ g') p
⊢ Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) (f ≫ g') ≫ φ.map p =
    Quiver.Path.rec (𝟙 (φ.obj X✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) f ≫
      Quiver.Path.rec (𝟙 (φ.obj Y✝)) (fun {b c} x f ihp ↦ ihp ≫ φ.map f) g' ≫ φ.map p
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
⊢ { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := cyclesMap S.f i, g := cyclesMap S.g i,
      zero := ⋯ }.Exact

Tactic:
have hi := (hS.map (HomologicalComplex.eval C c i)).fIsKernel

Goal state after:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
⊢ { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := cyclesMap S.f i, g := cyclesMap S.g i,
      zero := ⋯ }.Exact
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : V
f : X ⟶ Y
X' Y' : V
hX : X = X'
hY : Y = Y'
X'' Y'' : W
hX' : e X' = X''
hY' : e Y' = Y''
⊢ e Y' = Y''

Tactic:
hY'

Goal state after:
V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : V
f : X ⟶ Y
X' Y' : V
hX : X = X'
hY : Y = Y'
X'' Y'' : W
hX' : e X' = X''
hY' : e Y' = Y''
⊢ Y'' = Y''
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ⥤ C₂
L : C₁ ≌ C₃
R : C₂ ≌ C₄
B : C₃ ⥤ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ (iso T L.symm.inverse R.symm.inverse B).hom.app X = (iso T L.symm.inverse R.symm.inverse B).hom.app X

Tactic:
rw [vInv_iso_hom_app]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ⥤ C₂
L : C₁ ≌ C₃
R : C₂ ≌ C₄
B : C₃ ⥤ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ R.symm.inverse.map (T.map (L.symm.counitIso.inv.app X)) ≫
      R.symm.inverse.map ((iso B L.symm.functor R.symm.functor T).inv.app (L.symm.inverse.obj X)) ≫
        R.symm.unitIso.inv.app (B.obj (L.symm.inverse.obj X)) =
    (iso T L.symm.inverse R.symm.inverse B).hom.app X
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
⊢ Octahedron' comm h₁₂ h₂₃ h₁₃

Tactic:
by
  let o := someOctahedron comm (rot_of_distTriang _ h₁₂) (rot_of_distTriang _ h₂₃)
    (rot_of_distTriang _ h₁₃)
  let m₁ := (shiftShiftNeg Z₁₂ 1).inv ≫ o.m₁⟦-1⟧' ≫ (shiftShiftNeg Z₁₃ 1).hom
  let m₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ o.m₃⟦-1⟧' ≫ (shiftShiftNeg Z₂₃ 1).hom
  have eq₁ := o.comm₁
  have eq₂ := o.comm₂
  have eq₃ := o.comm₃
  have eq₄ := o.comm₄
  dsimp only [Triangle.mk_obj₁, Triangle.mk_obj₂, Triangle.mk_mor₁, Triangle.mk_mor₃]
    at eq₁ eq₂ eq₃ eq₄
  rw [comp_neg, neg_inj] at eq₂
  rw [neg_comp, comp_neg, neg_inj] at eq₄
  refine ⟨m₁, m₃, ?_, ?_, ?_, ?_, ?_⟩
  · rw [← shiftFunctorCompIsoId_naturality_1 v₁₃ 1 (-1) (Int.add_right_neg 1)]
    dsimp [m₁]
    rw [assoc, assoc, Iso.hom_inv_id_app_assoc]
    nth_rw 2 [← assoc]
    rw [← Functor.map_comp, eq₂, shiftFunctorCompIsoId_naturality_1]
  · dsimp [m₁]
    rw [Functor.map_comp, Functor.map_comp, shift_shiftFunctorCompIsoId_hom_app,
      shift_shiftFunctorCompIsoId_inv_app, shiftFunctorCompIsoId_naturality_1, eq₁]
  · dsimp [m₃]
    rw [Functor.map_comp, Functor.map_comp, shift_shiftFunctorCompIsoId_hom_app,
      shift_shiftFunctorCompIsoId_inv_app, shiftFunctorCompIsoId_naturality_1, eq₃]
  · rw [← shiftFunctorCompIsoId_naturality_1 v₂₃ 1 (-1) (Int.add_right_neg 1)]
    dsimp [m₃]
    rw [assoc, assoc, Iso.hom_inv_id_app_assoc]
    nth_rw 2 [← assoc]
    rw [← Functor.map_comp, ← eq₄, ← Functor.map_comp, shiftFunctorCompIsoId_naturality_1]
  · apply isomorphic_distinguished _ ((Triangle.shift_distinguished_iff _ (-1 : ℤ)).mpr o.mem)
    refine Triangle.isoMk _ _ (shiftShiftNeg Z₁₂ (1 : ℤ)).symm
      (-(shiftShiftNeg Z₁₃ (1 : ℤ)).symm) (shiftShiftNeg Z₂₃ (1 : ℤ)).symm (comm₃ := ?_)
    dsimp
    simp only [Int.reduceNeg, assoc, Int.negOnePow_neg, Int.negOnePow_one, neg_comp,
      Functor.map_neg, Functor.map_comp, smul_neg, Units.neg_smul, one_smul, neg_neg]
    rw [shift_shift_neg', shift_shift_neg', shift_shiftFunctorCompIsoId_inv_app,
      shiftFunctorComm_hom_app_of_add_eq_zero _ _ (Int.add_right_neg 1)]
    simp

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

Goal state before:
pp: case refine_2
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
⊢ ∀ (X Y : W.FunctorsInverting D) (f : X ⟶ Y),
    (inverse W D ⋙ functor W D).map f = eqToHom ⋯ ≫ (𝟭 (W.FunctorsInverting D)).map f ≫ eqToHom ⋯

Tactic:
rintro ⟨G₁, hG₁⟩ ⟨G₂, hG₂⟩ f
        ext
        dsimp
        -- Why does `rw` work but not `simp`?
        rw [NatTransExtension.app_eq, InducedCategory.eqToHom_hom,
          InducedCategory.eqToHom_hom]
        simp

Goal state after:
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₂
h : Φ.IsLocalizedEquivalence
inst✝ : CatCommSq Φ.functor L₁ L₂ G
⊢ G.IsEquivalence

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

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₂
h : Φ.IsLocalizedEquivalence
inst✝ : CatCommSq Φ.functor L₁ L₂ G
⊢ (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: case mp.refine_2
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.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s ≫ u = t₁ ≫ α.f ≫ u
fac' : t₂ ≫ α.f ≫ u ≫ u' = t₂' ≫ α.s ≫ u ≫ u'
⊢ ψ.f ≫ t₂ ≫ α.f ≫ u ≫ u' = ψ.f ≫ t₂' ≫ α.s ≫ u ≫ u'

Tactic:
fac'

Goal state after:
case mp.refine_2
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.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
Z''' : C
u' : Z'' ⟶ Z'''
hu' : W u'
fac : t₁' ≫ α.s ≫ u = t₁ ≫ α.f ≫ u
fac' : t₂ ≫ α.f ≫ u ≫ u' = t₂' ≫ α.s ≫ u ≫ u'
⊢ ψ.f ≫ t₂' ≫ α.s ≫ u ≫ u' = ψ.f ≫ t₂' ≫ α.s ≫ u ≫ u'
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
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst.map L ⋯
hβ₂ : g₂ = β.snd.map L ⋯
γ : W.LeftFraction₂ α.Y' β.Y'
hγ₁ : β.f ≫ γ.s = α.s ≫ γ.f
hγ₂ : β.f' ≫ γ.s = α.s ≫ γ.f'
⊢ f ≫ g₁ = { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f ≫ γ.f', s := β.s ≫ γ.s, hs := ⋯ }.fst.map L ⋯

Tactic:
by simpa only [hα, hβ₁] using! LeftFraction.map_comp_map_eq_map α β.fst γ.fst hγ₁ L

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

Tactic:
rw [← Functor.map_comp_assoc, ← map_comp, Iso.hom_inv_id_app]

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 ((shiftFunctor D b).map (𝟙 ((shiftFunctor C a ⋙ L).obj X))) ≫
    (commShiftOfLocalization.iso L W F F' b).hom.app (L.obj ((shiftFunctor C a).obj X)) ≫
      (shiftFunctor E b).map ((Lifting.iso L W F F').hom.app ((shiftFunctor C a).obj X)) ≫
        (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
          (shiftFunctor E b).map ((shiftFunctor E a).map ((Lifting.iso L W F F').inv.app X)) ≫
            (shiftFunctorAdd E a b).inv.app (F'.obj (L.obj X))
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: T₁ T₂ : Type w
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : Cardinal.mk T₁ < κ
h₂ : Cardinal.mk T₂ < κ
⊢ Cardinal.mk (T₁ × T₂) < κ

Tactic:
simpa using Cardinal.mul_lt_of_lt hκ h₁ h₂

Goal state after:
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
a : A
inst✝ : P.IsStableUnderShiftBy a
⊢ P.isoClosure ≤ P.isoClosure.shift a

Tactic:
by
    rintro X ⟨Y, hY, ⟨e⟩⟩
    exact ⟨Y⟦a⟧, P.le_shift a _ hY, ⟨(shiftFunctor C a).mapIso e⟩⟩

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

Goal state before:
pp: case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
⊢ P.shiftClosure G ≤ ⨆ x, P.shift x

Tactic:
rw [shiftClosure_le_iff]

Goal state after:
case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
⊢ P ≤ ⨆ x, P.shift x
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✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ (F.shift n₀).map T.mor₂ ≫ F.shiftMap T.mor₃ n₀ n₁ ⋯ = 0

Tactic:
← F.shiftMap_comp',

Goal state after:
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✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ F.shiftMap (T.mor₂ ≫ T.mor₃) n₀ n₁ ⋯ = 0
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
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₃
X Y : C
a : X ⟶ Y
hX : P X
hY : P Y
⊢ ∃ Z, ∃ (_ : P Z), ∃ b c, Triangle.mk a b c ∈ distinguishedTriangles

Tactic:
obtain ⟨Z, b, c, h⟩ := distinguished_cocone_triangle a
  obtain ⟨Z', hZ', ⟨e⟩⟩ := P.ext_of_isTriangulatedClosed₃' _ h hX hY
  exact ⟨Z', hZ', b ≫ e.hom, e.inv ≫ c, isomorphic_distinguished _ h _
    (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) e.symm )⟩

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
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso mn a a'' ⋯).hom.app X =
    (shiftFunctorAdd' D m n mn hnm).hom.app ((F.functor a'').obj X) ≫
      (shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').hom.app X) ≫ (F.shiftIso n a a' ha').hom.app X

Tactic:
by
  simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']

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
n m mn : A
hnm : m + n = mn
a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso mn a a'' ⋯).inv.app X =
    (F.shiftIso n a a' ha').inv.app X ≫
      (shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X) ≫
        (shiftFunctorAdd' D m n mn hnm).inv.app ((F.functor a'').obj X)

Tactic:
by
  simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']

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 ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
p q : ℤ
hpq : p + 1 = q
r : ℤ
hr : q + m = r
⊢ (↑(inr φ)).v p q hpq ≫ (descCochain φ α β h).v q r hr = β.v p r ⋯

Tactic:
obtain rfl : p = q + -1 := by lia

Goal state after:
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 ℤ
n m : ℤ
α : Cochain K M m
β : Cochain L M n
h : m + 1 = n
q r : ℤ
hr : q + m = r
hpq : q + -1 + 1 = q
⊢ (↑(inr φ)).v (q + -1) q hpq ≫ (descCochain φ α β h).v q r hr = β.v (q + -1) r ⋯
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ g.op ≫ f.op = 0

Tactic:
rw [← op_comp, w, op_zero]

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

Goal state before:
pp: case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntGE p).BoundaryGE (n + 1)
⊢ n + 1 = 0

Tactic:
· have := h.2 n
      dsimp at this
      lia

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

Goal state before:
pp: case mp.succ
p : ℤ
n : ℕ
h : (embeddingUpIntLE p).BoundaryLE (n + 1)
⊢ n + 1 = 0

Tactic:
· have := h.2 n
      dsimp at this
      lia

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

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
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ (K.extendXIso e hj').inv = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
h₁ : f' = 0
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0

Tactic:
have h₂ : f'' = 0 := by
      apply Fork.IsLimit.hom_ext hcone
      rw [← cancel_mono (extendXIso K e hj').inv, assoc, hf'', zero_comp, zero_comp,
        K.extend_d_to_eq_zero e i' j' j hj']
      rw [hi]
      exact hij

Goal state after:
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
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j k : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
cone : KernelFork (K.d j k)
hcone : IsLimit cone
W : C
f' : K.X i ⟶ cone.pt
hf' : f' ≫ Fork.ι cone = K.d i j
f'' : (K.extend e).X i' ⟶ cone.pt
hf'' : f'' ≫ Fork.ι cone ≫ (K.extendXIso e hj').inv = (K.extend e).d i' j'
φ : cone.pt ⟶ W
hij : ¬c.Rel i j
h₁ : f' = 0
h₂ : f'' = 0
⊢ f' ≫ φ = 0 ↔ f'' ≫ φ = 0
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 : ℤ
x✝¹ x✝ : C
f₁ f₂ : x✝¹ ⟶ x✝
h : (singleFunctor C n).map f₁ = (singleFunctor C n).map f₂
eq₁ :
  (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₁) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    f₁
eq₂ :
  (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₂) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    f₂
⊢ f₁ = f₂

Tactic:
← eq₁,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
x✝¹ x✝ : C
f₁ f₂ : x✝¹ ⟶ x✝
h : (singleFunctor C n).map f₁ = (singleFunctor C n).map f₂
eq₁ :
  (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₁) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    f₁
eq₂ :
  (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₂) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    f₂
⊢ (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₁) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    f₂
Module: Mathlib.CategoryTheory.Localization.SmallHom

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

Tactic:
simp only [hasSmallLocalizedHom_iff W W.Q]
  exact small_congr (Iso.homCongr (Iso.refl _) (Localization.isoOfHom W.Q W f hf))

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

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

Tactic:
intro h X Y n hn
    lift n to ℕ using hn
    exact h X Y n

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

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_3
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
F G : C ⥤ D
inst✝² : F.CommShift A
inst✝¹ : G.CommShift A
τ : F ⟶ G
inst✝ : CommShift τ A
x✝ : A
⊢ (Functor.commShiftIso (OppositeShift.functor A G) x✝).hom ≫
      Functor.whiskerRight (OppositeShift.natTrans A τ) (shiftFunctor (OppositeShift D A) x✝) =
    (shiftFunctor (OppositeShift C A) x✝).whiskerLeft (OppositeShift.natTrans A τ) ≫
      (Functor.commShiftIso (OppositeShift.functor A F) x✝).hom

Tactic:
ext
    rw [← cancel_mono (((OppositeShift.functor A F).commShiftIso _).inv.app _),
      ← cancel_epi (((OppositeShift.functor A G).commShiftIso _).inv.app _)]
    simp only [Functor.comp_obj, comp_app, Functor.whiskerRight_app, assoc,
      Iso.inv_hom_id_app_assoc, Functor.whiskerLeft_app, Iso.hom_inv_id_app, comp_id]
    exact (op_inj_iff _ _).mpr (NatTrans.shift_app_comm τ _ (unop _))

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Opposite.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasShift C ℤ
X : Cᵒᵖ
⊢ (shiftFunctorCompIsoId C 0 0 ⋯).inv.app (Opposite.unop X) ≫
      (shiftFunctor C 0).map ((shiftFunctorOpIso C 0 0 ⋯).hom.app X).unop =
    (shiftFunctorZero C ℤ).inv.app (Opposite.unop X) ≫ (shiftFunctor C 0).map ((shiftFunctorZero Cᵒᵖ ℤ).hom.app X).unop

Tactic:
rw [shiftFunctorZero_op_hom_app, unop_comp, Quiver.Hom.unop_op, Functor.map_comp,
    shiftFunctorCompIsoId_zero_zero_inv_app, assoc]

Goal state after: