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

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
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n a a' : M
ha' : n + a = a'
X : C
⊢ (F.shiftIso n a a' ha').hom.app (L.obj X) =
    (F.shift a).map ((commShiftIso L n).inv.app X) ≫
      (e' a).hom.app ((shiftFunctor C n).obj X) ≫ (G.shiftIso n a a' ha').hom.app X ≫ (e' a').inv.app X

Tactic:
apply induced.shiftIso_hom_app_obj

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
P : ObjectProperty C
inst✝ : P.IsTriangulatedClosed₂
X Z : C
c : Z ⟶ (shiftFunctor C 1).obj X
hX : P X
hZ : P Z
Y : C
a : X ⟶ Y
b : Y ⟶ Z
h : Triangle.mk a b c ∈ distinguishedTriangles
Y' : C
hY' : P Y'
e : (Triangle.mk a b c).obj₂ ≅ Y'
⊢ ∃ Y, ∃ (_ : P Y), ∃ a b, Triangle.mk a b c ∈ distinguishedTriangles

Tactic:
exact ⟨Y', hY', a ≫ e.hom, e.inv ≫ b, isomorphic_distinguished _ h _
    (Triangle.isoMk _ _ (Iso.refl _) e.symm (Iso.refl _))⟩

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
P : ObjectProperty C
i✝ w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ i✝
w✝¹ : i✝ ⟶ w✝³
w✝ : w✝³ ⟶ (shiftFunctor C 1).obj w✝⁴
left✝ : Triangle.mk w✝² w✝¹ w✝ ∈ distinguishedTriangles
h : ⊥ w✝⁴
right✝ : P w✝³
⊢ ⊥ i✝

Tactic:
exact h

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
P : ObjectProperty C
i✝ w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ i✝
w✝¹ : i✝ ⟶ w✝³
w✝ : w✝³ ⟶ (shiftFunctor C 1).obj w✝⁴
left✝¹ : Triangle.mk w✝² w✝¹ w✝ ∈ distinguishedTriangles
left✝ : P w✝⁴
h : ⊥ w✝³
⊢ ⊥ i✝

Tactic:
exact h

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ QuasiIso ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).map φ) ↔ QuasiIso φ

Tactic:
simp only [quasiIso_iff, fun i ↦ quasiIsoAt_shift_iff φ n i _ rfl]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ (∀ (i : ℤ), QuasiIsoAt φ (n + i)) ↔ ∀ (i : ℤ), QuasiIsoAt φ i
Module: Mathlib.Algebra.Homology.Opposite

Goal state before:
pp: case neg
ι : 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 : ι
hij : ¬c.Rel j i
⊢ (K.opcyclesOpIso i).hom ≫ (K.toCycles j i).op = K.op.fromOpcycles i j

Tactic:
rw [K.toCycles_eq_zero hij, K.op.fromOpcycles_eq_zero hij, op_zero, comp_zero]

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j k : ι
hj : ¬e.BoundaryGE j
hk : c.next j = k
hjk : ¬c.Rel j k
⊢ ¬e.BoundaryGE k

Tactic:
subst hk

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryGE j
hjk : ¬c.Rel j (c.next j)
⊢ ¬e.BoundaryGE (c.next j)
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij : c.prev j = i
hj : ¬e.BoundaryGE j
hij' : ¬c.Rel i j
⊢ j = i

Tactic:
by
      simpa only [c.prev_eq_self j (by simpa only [hij] using hij')] using hij

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hj : ¬e.BoundaryLE j
hk : c.prev j = i
hij : ¬c.Rel i j
⊢ ¬e.BoundaryLE i

Tactic:
subst hk

Goal state after:
case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
j : ι
hj : ¬e.BoundaryLE j
hij : ¬c.Rel (c.prev j) j
⊢ ¬e.BoundaryLE (c.prev j)
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.restriction e ⟶ L
i' : ι'
i : ι
hi : e.f i = i'
hi' : ∃ k, e.f k = i'
⊢ e.f hi'.choose = e.f i

Tactic:
by rw [hi'.choose_spec, hi]

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ ((if hi : e.BoundaryGE i then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
      else (XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (XIso K e ⋯).inv) ≫
      if hij : c.Rel j k then
        if hi : e.BoundaryGE j then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
        else (XIso K e hi).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
      else 0) =
    0

Tactic:
dif_pos hjk,

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ ((if hi : e.BoundaryGE i then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (XIso K e ⋯).inv
      else (XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (XIso K e ⋯).inv) ≫
      if hi : e.BoundaryGE j then (XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f j) (e.f k) ≫ (XIso K e ⋯).inv
      else (XIso K e hi).hom ≫ K.d (e.f j) (e.f k) ≫ (XIso K e ⋯).inv) =
    0
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case pos
ι : 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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : (e.extendFunctor C).obj K ⟶ (e.extendFunctor C).obj L
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ ((e.extendFunctor C).map { f := fun i ↦ (K.extendXIso e ⋯).inv ≫ φ.f (e.f i) ≫ (L.extendXIso e ⋯).hom, comm' := ⋯ }).f
      i' =
    φ.f i'

Tactic:
obtain ⟨i, rfl⟩ := hi'

Goal state after:
case pos
ι : 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✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K L : HomologicalComplex C c
φ : (e.extendFunctor C).obj K ⟶ (e.extendFunctor C).obj L
i : ι
⊢ ((e.extendFunctor C).map { f := fun i ↦ (K.extendXIso e ⋯).inv ≫ φ.f (e.f i) ≫ (L.extendXIso e ⋯).hom, comm' := ⋯ }).f
      (e.f i) =
    φ.f (e.f i)
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: case pos
ι : 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
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (e.liftExtend (e.homRestrict ψ) ⋯).f i' = ψ.f i'

Tactic:
obtain ⟨i, rfl⟩ := hi'

Goal state after:
case pos
ι : 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
i : ι
⊢ (e.liftExtend (e.homRestrict ψ) ⋯).f (e.f i) = ψ.f (e.f i)
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'
⊢ (K.restrictionXIso e hi').hom ≫ (K.sc' i' j' k').f = ((K.restriction e).sc' i j k).f ≫ (K.restrictionXIso e hj').hom

Tactic:
subst hi' hj'

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
k' : ι'
hk' : e.f k = k'
hk'' : c'.next (e.f j) = k'
hi'' : c'.prev (e.f j) = e.f i
⊢ (K.restrictionXIso e ⋯).hom ≫ (K.sc' (e.f i) (e.f j) k').f =
    ((K.restriction e).sc' i j k).f ≫ (K.restrictionXIso e ⋯).hom
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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : ¬e.BoundaryGE i
⊢ (truncGE'.XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (truncGE'.XIso K e ⋯).inv =
    (K.truncGE'XIso e hi' hi).hom ≫ K.d i' j' ≫ (K.truncGE'XIso e hj' ⋯).inv

Tactic:
subst hi' hj'

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 : ι
hij : c.Rel i j
hi : ¬e.BoundaryGE i
⊢ (truncGE'.XIso K e hi).hom ≫ K.d (e.f i) (e.f j) ≫ (truncGE'.XIso K e ⋯).inv =
    (K.truncGE'XIso e ⋯ hi).hom ≫ K.d (e.f i) (e.f j) ≫ (K.truncGE'XIso e ⋯ ⋯).inv
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 : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i j : ι
hij : c.Rel i j
i' j' : ι'
hi' : e.f i = i'
hj' : e.f j = j'
hi : e.BoundaryGE i
⊢ (truncGE'.XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (truncGE'.XIso K e ⋯).inv =
    (K.truncGE'XIsoOpcycles e hi' hi).hom ≫ K.fromOpcycles i' j' ≫ (K.truncGE'XIso e hj' ⋯).inv

Tactic:
subst hi' hj'

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 : ι
hij : c.Rel i j
hi : e.BoundaryGE i
⊢ (truncGE'.XIsoOpcycles K e hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (truncGE'.XIso K e ⋯).inv =
    (K.truncGE'XIsoOpcycles e ⋯ hi).hom ≫ K.fromOpcycles (e.f i) (e.f j) ≫ (K.truncGE'XIso e ⋯ ⋯).inv
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 L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ 0 =
    K.fromOpcycles j' (c'.next j') ≫
      K.pOpcycles (c'.next j') ≫ (K.truncGE'XIsoOpcycles e hk' hj).inv ≫ ((K.truncGE' e).extendXIso e hk').inv

Tactic:
← cancel_epi (K.pOpcycles _),

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
K L : HomologicalComplex C c'
φ : K ⟶ L
e : c.Embedding c'
inst✝³ : e.IsTruncGE
inst✝² : ∀ (i' : ι'), K.HasHomology i'
inst✝¹ : ∀ (i' : ι'), L.HasHomology i'
inst✝ : HasZeroObject C
i k : ι
j' : ι'
hk' : e.f k = c'.next j'
hj' : e.f k = j'
hi : c.prev k = i
hk : c.next k = k
hj : e.BoundaryGE k
hjk : ¬c.Rel k k
⊢ K.pOpcycles j' ≫ 0 =
    K.pOpcycles j' ≫
      K.fromOpcycles j' (c'.next j') ≫
        K.pOpcycles (c'.next j') ≫ (K.truncGE'XIsoOpcycles e hk' hj).inv ≫ ((K.truncGE' e).extendXIso e hk').inv
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
a✝ : K.IsSupported e
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ QuasiIsoAt (K.πTruncGE e) i'

Tactic:
obtain ⟨i, rfl⟩ := hi'

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
a✝ : K.IsSupported e
i : ι
⊢ QuasiIsoAt (K.πTruncGE e) (e.f i)
Module: Mathlib.Algebra.Homology.Embedding.TruncGEHomology

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
hK : K.IsSupportedOutside e
i' : ι'
hi' : ∃ i, e.f i = i'
⊢ (K.truncGE e).ExactAt i'

Tactic:
obtain ⟨i, rfl⟩ := hi'

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
hK : K.IsSupportedOutside e
i : ι
⊢ (K.truncGE e).ExactAt (e.f i)
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ QuasiIsoAt (K.shortComplexTruncLE e).g i'

Tactic:
rw [quasiIsoAt_iff_isIso_homologyMap]
  exact K.isIso_homologyMap_shortComplexTruncLE_g e i' hi'

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
⊢ (K.shortComplexTruncLE e).X₃.ExactAt (e.f i)

Tactic:
by
    rw [exactAt_iff_isZero_homology]
    by_cases hi : ∃ j', c'.Rel (e.f i) j'
    · obtain ⟨j', hj'⟩ := hi
      apply ((K.shortComplexTruncLE_shortExact e).homology_exact₃ (e.f i) j' hj').isZero_X₂
      · rw [← cancel_epi (homologyMap (K.ιTruncLE e) (e.f i)), comp_zero]
        dsimp [shortComplexTruncLE]
        rw [← homologyMap_comp, cokernel.condition, homologyMap_zero]
      · simp
    · have : IsIso (homologyMap (K.shortComplexTruncLE e).f (e.f i)) := by dsimp; infer_instance
      rw [IsZero.iff_id_eq_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).g (e.f i)),
        comp_id, comp_zero, ← cancel_epi (homologyMap (K.shortComplexTruncLE e).f (e.f i)),
        comp_zero, ← homologyMap_comp, ShortComplex.zero, homologyMap_zero]

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.IsStrictlyGE n ↔ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)

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

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

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

Tactic:
rw [hφ, Functor.map_comp]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : X.IsStrictlyLE n
X' : CochainComplex C ℤ
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
this : IsIso (Q.map (CochainComplex.truncLEMap s n))
⊢ IsIso (Q.map (CochainComplex.truncLEMap s n ≫ X.ιTruncLE n))

Tactic:
rw [Q.map_comp]

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : X.IsStrictlyLE n
X' : CochainComplex C ℤ
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
this : IsIso (Q.map (CochainComplex.truncLEMap s n))
⊢ IsIso (Q.map (CochainComplex.truncLEMap s n) ≫ Q.map (X.ιTruncLE n))
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
⊢ cyclesMap ((single C c j).map f) j ≫ (singleObjCyclesSelfIso c j B).hom = (singleObjCyclesSelfIso c j A).hom ≫ f

Tactic:
rw [← cancel_mono (singleObjCyclesSelfIso c j B).inv, assoc, assoc, Iso.hom_inv_id, comp_id,
    ← cancel_mono (iCycles _ _)]

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
⊢ cyclesMap ((single C c j).map f) j ≫ ((single C c j).obj B).iCycles j =
    ((singleObjCyclesSelfIso c j A).hom ≫ f ≫ (singleObjCyclesSelfIso c j B).inv) ≫ ((single C c j).obj B).iCycles j
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
this : IsIso (Q.map (CochainComplex.truncGEMap s n))
⊢ IsIso (Q.map (Y.πTruncGE n ≫ CochainComplex.truncGEMap s n))

Tactic:
rw [Q.map_comp]

Goal state after:
case refine_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
this : IsIso (Q.map (CochainComplex.truncGEMap s n))
⊢ IsIso (Q.map (Y.πTruncGE n) ≫ Q.map (CochainComplex.truncGEMap s n))
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
this : IsIso (Q.map (CochainComplex.truncGEMap s a))
⊢ IsIso (Q.map (CochainComplex.truncGEMap s a ≫ inv (X.πTruncGE a)))

Tactic:
rw [Q.map_comp]

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyGE a
inst✝¹ : X.IsStrictlyLE b
inst✝ : Y.IsStrictlyGE a
f : Q.obj X ⟶ Q.obj Y
X' : CochainComplex C ℤ
hX' : X'.IsStrictlyLE b
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
fac : f = inv (Q.map s) ≫ Q.map g
this : IsIso (Q.map (CochainComplex.truncGEMap s a))
⊢ IsIso (Q.map (CochainComplex.truncGEMap s a) ≫ Q.map (inv (X.πTruncGE a)))
Module: Mathlib.CategoryTheory.Localization.SmallHom

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y Z : C
inst✝² : HasSmallLocalizedHom W X Y
inst✝¹ : HasSmallLocalizedHom W Y Z
inst✝ : HasSmallLocalizedHom W X Z
f : X ⟶ Y
g : Y ⟶ Z
⊢ (equiv W W.Q) ((mk W f).comp (mk W g)) = (equiv W W.Q) (mk W (f ≫ g))

Tactic:
simp [equiv_comp]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W Y Y
α : SmallHom W X Y
⊢ (equiv W W.Q) (α.comp (mk W (𝟙 Y))) = (equiv W W.Q) α

Tactic:
simp [equiv_comp]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W X X
α : SmallHom W X Y
⊢ (equiv W W.Q) ((mk W (𝟙 X)).comp α) = (equiv W W.Q) α

Tactic:
simp [equiv_comp]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ IsIso (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))

Tactic:
rw [Q.map_comp]

Goal state after:
case refine_1
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ IsIso (Q.map (inv (Y.ιTruncLE b)) ≫ Q.map (CochainComplex.truncLEMap s b))