mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: case mpr
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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
X Y : C
f : L.obj X ⟶ L.obj Y
⊢ ∀ (g : L.obj X ⟶ L.obj Y), G.map (f + g) = G.map f + G.map g

Tactic:
g

Goal state after:
case mpr
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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
X Y : C
f g : L.obj X ⟶ L.obj Y
⊢ G.map (f + g) = G.map f + G.map g
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} (P.strictLimitsClosureIter J (Order.succ b))

Tactic:
rw [strictLimitsClosureIter, transfiniteIterate_succ _ _ _ hb,
      strictLimitsClosureStep]

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 ⊔
      ⨆ a, (transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) b P).strictLimitsOfShape (J a))
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P.IsStableUnderShift A
⊢ P.shiftClosure A = P

Tactic:
refine le_antisymm ?_ P.le_shiftClosure
  rintro X ⟨Y, a, i, hY⟩
  exact P.prop_of_iso i.symm (P.le_shift a Y hY)

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
f : X ⟶ Y
g : Y ⟶ Z
h : 0 + 0 = 0
⊢ (mk₀ 0 ⋯ f).comp (mk₀ 0 ⋯ g) h = mk₀ 0 ⋯ (f ≫ g)

Tactic:
rw [mk₀_comp, mk₀, mk₀, assoc]

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
R : Type u_5
inst✝² : Ring R
inst✝¹ : Preadditive C
inst✝ : Linear R C
r : R
a b c : M
α : ShiftedHom X Y a
β : ShiftedHom Y Z b
h : b + a = c
⊢ (r • α).comp β h = r • α.comp β h

Tactic:
by
  rw [comp, comp, Linear.smul_comp]

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 Q : ObjectProperty C
inst✝ : P.ContainsZero
⊢ Q ≤ P.extensionProduct Q

Tactic:
by
  intro X hX
  rw [← extensionProduct_isoClosure_left]
  obtain ⟨Z, hZ, hP⟩ := P.exists_prop_of_containsZero
  refine ⟨_, _, _, _, _, inv_rot_of_distTriang _ (contractible_distinguished X), ?_, hX⟩
  exact ⟨Z, hP, ⟨IsZero.iso (Functor.map_isZero _ (isZero_zero C)) hZ⟩⟩

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

Goal state before:
pp: case zero
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✝ : IsTriangulated C
n n' : ℕ
h : n = n' + 1
⊢ P.extensionProductIter n = (P.extensionProductIter n').extensionProduct (P.extensionProductIter 0)

Tactic:
extensionProductIter_zero,

Goal state after:
case zero
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✝ : IsTriangulated C
n n' : ℕ
h : n = n' + 1
⊢ P.extensionProductIter n = (P.extensionProductIter n').extensionProduct P
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case zero
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✝ : IsTriangulated C
m m' : ℕ
h : m = m' + 1
⊢ P.extensionProductIter m = (P.extensionProductIter 0).extensionProduct (P.extensionProductIter m')

Tactic:
extensionProductIter_zero,

Goal state after:
case zero
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✝ : IsTriangulated C
m m' : ℕ
h : m = m' + 1
⊢ P.extensionProductIter m = P.extensionProduct (P.extensionProductIter m')
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.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
⊢ P.trW g ↔ ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P X

Tactic:
by
  rw [P.trW_iff]
  constructor
  · rintro ⟨Z, g, h, H, mem⟩
    exact ⟨_, _, _, inv_rot_of_distTriang _ H, P.le_shift (-1) _ mem⟩
  · rintro ⟨Z, g, h, H, mem⟩
    exact ⟨_, _, _, rot_of_distTriang _ H, P.le_shift 1 _ mem⟩

Goal state after:
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
f : Arrow (HomotopyCategory C c)
⊢ ∀ (g : Arrow (HomotopyCategory C c)) (x : f ≅ g), quasiIso C c f.hom → quasiIso C c g.hom

Tactic:
g

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
f g : Arrow (HomotopyCategory C c)
⊢ ∀ (x : f ≅ g), quasiIso C c f.hom → quasiIso C c g.hom
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
a : ℤ
K : HomologicalComplex C (up ℤ)
⊢ (ShiftSequence.shiftIso C 0 a a ⋯).hom.app K =
    (Functor.isoWhiskerRight (shiftFunctorZero (HomologicalComplex C (up ℤ)) ℤ) (homologyFunctor C (up ℤ) a) ≪≫
            (homologyFunctor C (up ℤ) a).leftUnitor).hom.app
      K

Tactic:
dsimp [homologyMap]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
a : ℤ
K : HomologicalComplex C (up ℤ)
⊢ (ShiftSequence.shiftIso C 0 a a ⋯).hom.app K =
    ShortComplex.homologyMap
        ((shortComplexFunctor C (up ℤ) a).map ((shiftFunctorZero (HomologicalComplex C (up ℤ)) ℤ).hom.app K)) ≫
      𝟙 (K.homology a)
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
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : HomologicalComplex C (up ℤ)
⊢ (ShiftSequence.shiftIso C (m + n) a a'' ⋯).hom.app K =
    (Functor.isoWhiskerRight (shiftFunctorAdd (HomologicalComplex C (up ℤ)) m n) (homologyFunctor C (up ℤ) a) ≪≫
            (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) m).associator
                (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n) (homologyFunctor C (up ℤ) a) ≪≫
              (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) m).isoWhiskerLeft
                  (ShiftSequence.shiftIso C n a a' ha') ≪≫
                ShiftSequence.shiftIso C m a' a'' ha'').hom.app
      K

Tactic:
dsimp [homologyMap]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : HomologicalComplex C (up ℤ)
⊢ (ShiftSequence.shiftIso C (m + n) a a'' ⋯).hom.app K =
    ShortComplex.homologyMap
        ((shortComplexFunctor C (up ℤ) a).map ((shiftFunctorAdd (HomologicalComplex C (up ℤ)) m n).hom.app K)) ≫
      𝟙
          (((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).obj
                ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) m).obj K)).homology
            a) ≫
        (ShiftSequence.shiftIso C n a a' ha').hom.app
            ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) m).obj K) ≫
          (ShiftSequence.shiftIso C m a' a'' ha'').hom.app K
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝³ : Preadditive C
inst✝² : CategoryWithHomology C
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
K L : HomologicalComplex C c
f : K ⟶ L
⊢ ∀ (f₂ : K ⟶ L), homotopic C c f f₂ → Q.map f = Q.map f₂

Tactic:
g

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝³ : Preadditive C
inst✝² : CategoryWithHomology C
inst✝¹ : (HomologicalComplex.quasiIso C c).HasLocalization
inst✝ : c.QFactorsThroughHomotopy C
K L : HomologicalComplex C c
f g : K ⟶ L
⊢ homotopic C c f g → Q.map f = Q.map g
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ i, c.Rel i j
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
E : Type u_3
inst✝ : Category.{v_2, u_3} E
F : HomologicalComplex C c ⥤ E
hF : (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy F
K L : HomologicalComplex C c
f : K ⟶ L
⊢ ∀ (f₂ : K ⟶ L), homotopic C c f f₂ → F.map f = F.map f₂

Tactic:
g

Goal state after:
ι : Type u_1
c : ComplexShape ι
hc : ∀ (j : ι), ∃ i, c.Rel i j
C : Type u_2
inst✝³ : Category.{v_1, u_2} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
E : Type u_3
inst✝ : Category.{v_2, u_3} E
F : HomologicalComplex C c ⥤ E
hF : (HomologicalComplex.homotopyEquivalences C c).IsInvertedBy F
K L : HomologicalComplex C c
f g : K ⟶ L
⊢ homotopic C c f g → F.map f = F.map g
Module: Mathlib.Algebra.Homology.DerivedCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ 𝟙 (Qh.obj (((HomotopyCategory.singleFunctors C).functor n).obj X)) ≫
      𝟙 ((singleFunctor C n).obj X) ≫
        𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) =
    𝟙 (((singleFunctors C).functor n).obj X)

Tactic:
Category.id_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ 𝟙 (Qh.obj (((HomotopyCategory.singleFunctors C).functor n).obj X)) ≫
      𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) =
    𝟙 (((singleFunctors C).functor n).obj X)
Module: Mathlib.Algebra.Homology.DerivedCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ 𝟙 (Qh.obj (((HomotopyCategory.singleFunctors C).functor n).obj X)) ≫
      𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) =
    𝟙 (((singleFunctors C).functor n).obj X)

Tactic:
Category.id_comp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ 𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) =
    𝟙 (((singleFunctors C).functor n).obj 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✝ : P.IsTriangulated
X Y : P.FullSubcategory
f : X ⟶ Y
⊢ ∃ Z g h, Triangle.mk f g h ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles

Tactic:
obtain ⟨Z', g', h', mem⟩ := distinguished_cocone_triangle (P.ι.map f)

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
X Y : P.FullSubcategory
f : X ⟶ Y
Z' : C
g' : P.ι.obj Y ⟶ Z'
h' : Z' ⟶ (shiftFunctor C 1).obj (P.ι.obj X)
mem : Triangle.mk (P.ι.map f) g' h' ∈ distinguishedTriangles
⊢ ∃ Z g h, Triangle.mk f g h ∈ P.ι.mapTriangle.obj ⁻¹' distinguishedTriangles
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
X : (HomologicalComplex V c)ᵒᵖ
i✝ : ι
⊢ ((opFunctor V c).map ((opUnitIso V c).hom.app X) ≫ (opCounitIso V c).hom.app ((opFunctor V c).obj X)).f i✝ =
    (𝟙 ((opFunctor V c).obj X)).f i✝

Tactic:
simp only [opUnitIso, opCounitIso, NatIso.ofComponents_hom_app, Iso.op_hom, comp_f,
      opFunctor_map_f, Hom.isoOfComponents_hom_f]

Goal state after:
ι : Type u_1
V : Type u_2
inst✝¹ : Category.{v_1, u_2} V
c : ComplexShape ι
inst✝ : HasZeroMorphisms V
X : (HomologicalComplex V c)ᵒᵖ
i✝ : ι
⊢ ((Hom.isoOfComponents (fun x ↦ Iso.refl ((unop X).op.unopSymm.X x)) ⋯).hom.op.unop.f i✝).op ≫
      (Iso.refl (((opInverse V c ⋙ opFunctor V c).obj ((opFunctor V c).obj X)).X i✝)).hom =
    (𝟙 ((opFunctor V c).obj X)).f i✝
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 L : HomologicalComplex V c
φ : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ QuasiIsoAt ((opFunctor V c).map φ.op) i ↔ QuasiIsoAt φ i

Tactic:
simp only [quasiIsoAt_iff]
  exact ShortComplex.quasiIso_opMap_iff ((shortComplexFunctor V c i).map φ)

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁✝ X₂✝ X₃✝ : CochainComplex C ℤ
f : X₁✝ ⟶ X₂✝
g : X₂✝ ⟶ X₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ (Triangle.mk ((quotient C (ComplexShape.up ℤ)).map α.hom₃) ((quotient C (ComplexShape.up ℤ)).map β.hom₃)
          (((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₃ ≫
              (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone.triangle u₂₃).obj₁) ≫
            (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
              ((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₂))).mor₂ ≫
      (Iso.refl
          (Triangle.mk ((quotient C (ComplexShape.up ℤ)).map α.hom₃) ((quotient C (ComplexShape.up ℤ)).map β.hom₃)
              (((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₃ ≫
                  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone.triangle u₂₃).obj₁) ≫
                (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
                  ((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₂))).obj₃).hom =
    (Iso.refl
          (Triangle.mk ((quotient C (ComplexShape.up ℤ)).map α.hom₃) ((quotient C (ComplexShape.up ℤ)).map β.hom₃)
              (((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₂₃).mor₃ ≫
                  (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone.triangle u₂₃).obj₁) ≫
                (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
                  ((quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₂))).obj₂).hom ≫
      (mappingConeCompTriangleh u₁₂ u₂₃).mor₂

Tactic:
by dsimp [β, mappingConeCompTriangleh]; simp

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
i j k : ι
i' j' k' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
hk : c.next j = k
hk' : c'.next j' = k'
h : (K.sc' i j k).LeftHomologyData
⊢ (h.i ≫ (K.extendXIso e hj').inv) ≫ ((K.extend e).sc' i' j' k').g = 0

Tactic:
by
    dsimp
    rw [assoc, ← comp_d_eq_zero_iff K e hj' hk hk']
    exact h.wi

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

Tactic:
simp [K.truncGE'_d_eq_fromOpcycles e hjk hj' rfl hj]

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

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i' : ι'
hi' : ¬∃ j', c'.Rel i' j'
⊢ Epi (homologyMap (K.shortComplexTruncLE e).g i')

Tactic:
exact epi_homologyMap_of_epi_of_not_rel _ _ (by simpa using hi')

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 i : ℤ
hi : i < n
inst✝ : K.IsStrictlyGE n
⊢ ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i

Tactic:
simpa only [notMem_range_embeddingUpIntGE_iff] using hi

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 i : ℤ
hi : i < n
inst✝ : K.IsGE n
⊢ ∀ (i_1 : ℕ), (embeddingUpIntGE n).f i_1 ≠ i

Tactic:
simpa only [notMem_range_embeddingUpIntGE_iff] using hi

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

Goal state before:
pp: C₁ : Type u_2
C₂ : Type u_3
D₁ : Type u_5
D₂ : Type u_6
inst✝⁵ : Category.{v_2, u_2} C₁
inst✝⁴ : Category.{v_3, u_3} C₂
inst✝³ : Category.{v_5, u_5} D₁
inst✝² : Category.{v_6, u_6} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝¹ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝ : L₂.IsLocalization W₂
X Y : C₁
f : X ⟶ Y
⊢ Φ.homMap L₁ L₂ (L₁.map f) = L₂.map (Φ.functor.map f)

Tactic:
by
  dsimp [homMap]
  simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasDerivedCategory C
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
n : ℤ
inst✝ : Y.IsStrictlyGE n
⊢ ∃ Y', ∃ (_ : Y'.IsStrictlyGE n), ∃ g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)

Tactic:
by
  obtain ⟨Y', g, s, hs, rfl⟩ := left_fac f
  have : IsIso (Q.map (CochainComplex.truncGEMap s n)) := by
    rw [isIso_Q_map_iff_quasiIso, CochainComplex.quasiIso_truncGEMap_iff]
    rw [isIso_Q_map_iff_quasiIso] at hs
    infer_instance
  refine ⟨Y'.truncGE n, inferInstance, X.πTruncGE n ≫ CochainComplex.truncGEMap g n,
    Y.πTruncGE n ≫ CochainComplex.truncGEMap s n, ?_, ?_⟩
  · rw [Q.map_comp]
    infer_instance
  · have eq := Q.congr_map (CochainComplex.πTruncGE_naturality s n)
    have eq' := Q.congr_map (CochainComplex.πTruncGE_naturality g n)
    simp only [Functor.map_comp] at eq eq'
    simp only [Functor.map_comp, ← cancel_mono (Q.map (CochainComplex.πTruncGE Y n)
      ≫ Q.map (CochainComplex.truncGEMap s n)), assoc, IsIso.inv_hom_id, comp_id]
    simp only [eq, IsIso.inv_hom_id_assoc, eq']

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

Goal state before:
pp: C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : CochainComplex C ℤ
inst✝ : ∀ (i : ℤ), HasHomology K i
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ IsSupportedOutside K (embeddingUpIntLE n₀) ↔ K.IsGE n₁

Tactic:
(Embedding.embeddingUpInt_areComplementary n₀ n₁ h).isSupportedOutside₁_iff

Goal state after:
C : Type u_2
inst✝³ : Category.{u_3, u_2} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : CochainComplex C ℤ
inst✝ : ∀ (i : ℤ), HasHomology K i
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ IsSupported K (embeddingUpIntGE n₁) ↔ K.IsGE n₁