mathlib-initiative/mathlib-tactics huggingface dataset:
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 T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
α : ShiftedHom X Y a₁
β : ShiftedHom Y Z a₂
γ : ShiftedHom Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ (α.comp β h₁₂).comp γ ⋯ = α.comp (β.comp γ h₂₃) ⋯

Tactic:
simp only [comp, assoc, Functor.map_comp,
    shiftFunctorAdd'_assoc_inv_app a₃ a₂ a₁ a₂₃ a₁₂ a h₂₃ h₁₂ h,
    ← NatTrans.naturality_assoc, Functor.comp_map]

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

Goal state before:
pp: C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁷ : Category.{v_2, u_2} D
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
X Y : C
inst✝³ : Preadditive C
inst✝² : Preadditive D
a : M
α₁ α₂ : ShiftedHom X Y a
F : C ⥤ D
inst✝¹ : F.CommShift M
inst✝ : F.Additive
⊢ (α₁ + α₂).map F = α₁.map F + α₂.map F

Tactic:
by
  simp [ShiftedHom.map, F.map_add]

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M K' L' : HomologicalComplex C c
f : K ⟶ L
inst✝² : IsIso f
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
⊢ ShortComplex.QuasiIso ((shortComplexFunctor C c i).map f)

Tactic:
infer_instance

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

Goal state before:
pp: case mp
ι : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K L : HomologicalComplex C c
f : K ⟶ L
i : ι
inst✝¹ : K.HasHomology i
inst✝ : L.HasHomology i
hK : IsZero (K.sc i).homology
h : IsIso (ShortComplex.homologyMap ((shortComplexFunctor C c i).map f))
⊢ IsZero (L.sc i).homology

Tactic:
exact IsZero.of_iso hK (@asIso _ _ _ _ _ h).symm

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

Goal state before:
pp: case succ
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 Q R : ObjectProperty C
inst✝ : P.Nonempty
n : ℕ
h : (P.extensionProductIter n).Nonempty
⊢ (P.extensionProduct (P.extensionProductIter n)).Nonempty

Tactic:
infer_instance

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

Goal state before:
pp: case mp
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
⊢ QuasiIsoAt (φ ≫ φ') i → QuasiIsoAt φ' i

Tactic:
intro

Goal state after:
case mp
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
a✝ : QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt φ' i
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
⊢ QuasiIsoAt φ' i → QuasiIsoAt (φ ≫ φ') i

Tactic:
intro

Goal state after:
case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
a✝ : QuasiIsoAt φ' i
⊢ QuasiIsoAt (φ ≫ φ') i
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ : QuasiIsoAt φ i
a✝ : QuasiIsoAt φ' i
⊢ QuasiIsoAt (φ ≫ φ') i

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso (φ ≫ φ')

Tactic:
infer_instance

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

Goal state before:
pp: case mp
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
⊢ QuasiIsoAt (φ ≫ φ') i → QuasiIsoAt φ i

Tactic:
intro

Goal state after:
case mp
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
a✝ : QuasiIsoAt (φ ≫ φ') i
⊢ QuasiIsoAt φ i
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
⊢ QuasiIsoAt φ i → QuasiIsoAt (φ ≫ φ') i

Tactic:
intro

Goal state after:
case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
a✝ : QuasiIsoAt φ i
⊢ QuasiIsoAt (φ ≫ φ') i
Module: Mathlib.Algebra.Homology.QuasiIso

Goal state before:
pp: case mpr
ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
i : ι
inst✝² : K.HasHomology i
inst✝¹ : L.HasHomology i
inst✝ : M.HasHomology i
hφ' : QuasiIsoAt φ' i
a✝ : QuasiIsoAt φ i
⊢ QuasiIsoAt (φ ≫ φ') i

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
c : ComplexShape ι
K L M : HomologicalComplex C c
φ : K ⟶ L
φ' : L ⟶ M
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : ∀ (i : ι), M.HasHomology i
hφ : QuasiIso φ'
hφφ' : QuasiIso (φ ≫ φ')
⊢ QuasiIso (φ ≫ φ')

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
c : ComplexShape ι
K L M K' L' : HomologicalComplex C c
inst✝ : CategoryWithHomology C
x✝ : HomologicalComplex C c
⊢ QuasiIso (𝟙 x✝)

Tactic:
infer_instance

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

Goal state before:
pp: case succ
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 Q R : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
n : ℕ
h : (P.extensionProductIter n).IsStableUnderShift ℤ
⊢ (P.extensionProduct (P.extensionProductIter n)).IsStableUnderShift ℤ

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
c : ComplexShape ι
K L M K' L' : HomologicalComplex C c
inst✝ : CategoryWithHomology C
X✝ Y✝ Z✝ : HomologicalComplex C c
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
hf : QuasiIso x✝¹
hg : QuasiIso x✝
⊢ QuasiIso (x✝¹ ≫ x✝)

Tactic:
infer_instance

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

Goal state before:
pp: case succ
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 Q R : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
n : ℕ
H : (P.extensionProductIter n).IsStableUnderShift ℤ
⊢ (P.extensionProduct (P.extensionProductIter n)).IsStableUnderShift ℤ

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
c : ComplexShape ι
K L M K' L' : HomologicalComplex C c
inst✝ : CategoryWithHomology C
x✝³ x✝² : HomologicalComplex C c
x✝¹ : x✝³ ⟶ x✝²
x✝ : IsIso x✝¹
⊢ QuasiIso x✝¹

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
c : ComplexShape ι
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
e : HomotopyEquiv K L
⊢ QuasiIso e.hom

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (homologyFunctor C (ComplexShape.up ℤ) 0).homologicalKernel.IsTriangulated

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (homologyFunctor C (ComplexShape.up ℤ) 0).homologicalKernel.IsClosedUnderIsomorphisms

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
⊢ (subcategoryAcyclic C).trW.IsCompatibleWithShift ℤ

Tactic:
infer_instance

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✝¹ : HasZeroMorphisms C
inst✝ : CategoryWithHomology C
i : ι
x✝² x✝¹ : HomologicalComplex C c
x✝ : x✝² ⟶ x✝¹
hf : QuasiIso x✝
⊢ IsIso (homologyMap x✝ i)

Tactic:
infer_instance

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

Goal state before:
pp: case mp
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝² : HasZeroMorphisms C
inst✝¹ : CategoryWithHomology C
inst✝ : (HomologicalComplex.quasiIso C c).HasLocalization
K L : HomologicalComplex C c
f : K ⟶ L
h : IsIso (Q.map f)
i : ι
⊢ IsIso ((homologyFunctor C c i).map (Q.map f))

Tactic:
infer_instance

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
K L : HomologicalComplex C c
f : K ⟶ L
⊢ quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f

Tactic:
have eq := fun (i : ι) => NatIso.isIso_map_iff (homologyFunctorFactors C c i) f

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
K L : HomologicalComplex C c
f : K ⟶ L
eq :
  ∀ (i : ι),
    IsIso ((quotient C c ⋙ homologyFunctor C c i).map f) ↔ IsIso ((HomologicalComplex.homologyFunctor C c i).map f)
⊢ quasiIso C c ((quotient C c).map f) ↔ HomologicalComplex.quasiIso C c f
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
K : HomotopyCategory C c
⊢ ∀ (n : ι), IsIso ((homologyFunctor C c n).map (𝟙 K))

Tactic:
infer_instance

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
X✝ Y✝ Z✝ : HomotopyCategory C c
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : ∀ (n : ι), IsIso ((homologyFunctor C c n).map f)
hg : ∀ (n : ι), IsIso ((homologyFunctor C c n).map g)
⊢ ∀ (n : ι), IsIso ((homologyFunctor C c n).map f ≫ (homologyFunctor C c n).map g)

Tactic:
infer_instance

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 : ℤ
inst✝ : QuasiIso φ
⊢ QuasiIso φ

Tactic:
infer_instance

Goal state after:
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 g : K ⟶ L
h : Homotopy f g
⊢ DecidableRel c.Rel

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n : ℤ
⊢ (single C (ComplexShape.up ℤ) n).Additive

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
n : ℤ
⊢ ((CochainComplex.singleFunctors C).functor n ⋙ quotient C (ComplexShape.up ℤ)).Additive

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ HomologicalComplexUpToQuasiIso.Q.IsLocalization (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ HomologicalComplexUpToQuasiIso.Qh.IsLocalization (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ Qh.IsLocalization (HomotopyCategory.quasiIso C (ComplexShape.up ℤ))

Tactic:
infer_instance

Goal state after:
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 : ℤ
⊢ ((HomotopyCategory.singleFunctors C).functor n ⋙ Qh).Additive

Tactic:
infer_instance

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

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : HomotopyCategory C (ComplexShape.up ℤ)
f : X ⟶ Y
hf : IsIso (Qh.map f)
n : ℤ
⊢ IsIso ((homologyFunctor C n).map (Qh.map f))

Tactic:
infer_instance

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 : E ⥤ C
hF : ∀ (X : E), P (F.obj X)
inst✝⁵ : Preadditive E
inst✝⁴ : F.CommShift ℤ
inst✝³ : HasZeroObject E
inst✝² : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
⊢ F.IsTriangulated

Tactic:
infer_instance

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
D : Type u_4
inst✝⁸ : Category.{u_5, u_4} D
inst✝⁷ : HasZeroObject D
inst✝⁶ : Preadditive D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
F : C ⥤ D
inst✝² : F.CommShift ℤ
inst✝¹ : F.IsTriangulated
inst✝ : F.Full
⊢ (P.ι ⋙ F).essImage.IsTriangulated

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ ∀ (i₁ i₂ : A), i₁ + a = i₂ ↔ i₁ + b + a = i₂ + b

Tactic:
add_right_comm _ b a,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ ∀ (i₁ i₂ : A), i₁ + a = i₂ ↔ i₁ + a + b = i₂ + b
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ (Embedding.mk' (up' a) (up' a) (fun x ↦ x + b) ⋯ ⋯).IsRelIff

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ ∀ (i₁ i₂ : A), i₂ + a = i₁ ↔ i₂ + b + a = i₁ + b

Tactic:
add_right_comm _ b a,

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ ∀ (i₁ i₂ : A), i₂ + a = i₁ ↔ i₂ + a + b = i₁ + b
Module: Mathlib.Algebra.Homology.Embedding.Basic

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
A : Type u_3
inst✝² : AddCommSemigroup A
inst✝¹ : IsRightCancelAdd A
inst✝ : One A
a b : A
⊢ (Embedding.mk' (down' a) (down' a) (fun x ↦ x + b) ⋯ ⋯).IsRelIff

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
⊢ (Embedding.mk' (up ℕ) (up ℤ) (fun n ↦ ↑n) ⋯ embeddingUpNat._proof_3).IsRelIff

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
⊢ (Embedding.mk' (down ℕ) (up ℤ) (fun n ↦ -↑n) ⋯ embeddingDownNat._proof_3).IsRelIff

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
⊢ (Embedding.mk' (up ℕ) (up ℤ) (fun n ↦ p + ↑n) ⋯ ⋯).IsRelIff

Tactic:
infer_instance

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
p : ℤ
⊢ (Embedding.mk' (down ℕ) (up ℤ) (fun n ↦ p - ↑n) ⋯ ⋯).IsRelIff

Tactic:
infer_instance

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

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'
e' : K ≅ L
φ : K ⟶ L
e : c.Embedding c'
inst✝ : K.IsStrictlySupported e
⊢ K.IsStrictlySupported e

Tactic:
infer_instance

Goal state after:
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✝ : ι
⊢ ((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✝

Tactic:
exact Category.comp_id _

Goal state after:
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✝ : ι
⊢ ((unopFunctor V c).map ((unopUnitIso V c).hom.app X)).f i✝ ≫
      ((unopCounitIso V c).hom.app ((unopFunctor V c).obj X)).f i✝ =
    (𝟙 ((unopFunctor V c).obj X)).f i✝

Tactic:
exact Category.comp_id _

Goal state after:
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
⊢ K.op.HasHomology i

Tactic:
infer_instance

Goal state after:
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
⊢ K.unop.HasHomology i

Tactic:
infer_instance

Goal state after:
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
inst✝ : QuasiIsoAt φ i
⊢ QuasiIsoAt φ i

Tactic:
infer_instance

Goal state after:
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
inst✝ : QuasiIsoAt φ i
⊢ QuasiIsoAt φ i

Tactic:
infer_instance

Goal state after:
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
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : QuasiIso φ
⊢ QuasiIso φ

Tactic:
infer_instance

Goal state after:
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
inst✝² : ∀ (i : ι), K.HasHomology i
inst✝¹ : ∀ (i : ι), L.HasHomology i
inst✝ : QuasiIso φ
⊢ QuasiIso φ

Tactic:
infer_instance

Goal state after: