mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

Goal state before:
pp: case pos.hf
ι : 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 : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ homologyMap (K.ιTruncLE e) (e.f i) ≫
      { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
          X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
          g := ⋯.δ (e.f i) j' hj', zero := ⋯ }.f =
    0

Tactic:
]

Goal state after:
case pos.hf
ι : 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 : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ homologyMap (K.ιTruncLE e) (e.f i) ≫
      { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
          X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
          g := ⋯.δ (e.f i) j' hj', zero := ⋯ }.f =
    0
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

Goal state before:
pp: case pos.hf
ι : 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 : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ 0 = 0

Tactic:
]

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 (e.f i) j'
this : IsIso (homologyMap (K.shortComplexTruncLE e).f (e.f i))
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: case hK
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝³ : Category.{v_1, u_4} C
inst✝² : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex C c
inst✝¹ : K.IsStrictlySupported e₁
inst✝ : L.IsStrictlySupported e₂
φ : K ⟶ L
⊢ K.IsStrictlySupported e₁

Tactic:
]

Goal state after:
case hK
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝³ : Category.{v_1, u_4} C
inst✝² : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex C c
inst✝¹ : K.IsStrictlySupported e₁
inst✝ : L.IsStrictlySupported e₂
φ : K ⟶ L
⊢ K.IsStrictlySupported e₁
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case hL
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝³ : Category.{v_1, u_4} C
inst✝² : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex C c
inst✝¹ : K.IsStrictlySupported e₁
inst✝ : L.IsStrictlySupported e₂
φ : K ⟶ L
⊢ L.IsStrictlySupported e₂

Tactic:
]

Goal state after:
case hL
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝³ : Category.{v_1, u_4} C
inst✝² : HasZeroMorphisms C
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
ac : e₁.AreComplementary e₂
K L : HomologicalComplex C c
inst✝¹ : K.IsStrictlySupported e₁
inst✝ : L.IsStrictlySupported e₂
φ : K ⟶ L
⊢ L.IsStrictlySupported e₂
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 : n < i
inst✝ : K.IsStrictlyLE n
⊢ ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i

Tactic:
simpa only [notMem_range_embeddingUpIntLE_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 : n < i
inst✝ : K.IsLE n
⊢ ∀ (i_1 : ℕ), (embeddingUpIntLE n).f i_1 ≠ i

Tactic:
simpa only [notMem_range_embeddingUpIntLE_iff] using hi

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)
i : ℤ
hi : i < n
⊢ IsZero (K.X i)

Tactic:
]

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)
i : ℤ
hi : i < n
⊢ IsZero (K.X i)
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero (K.X i)
i : ℤ
hi : n < i
⊢ IsZero (K.X i)

Tactic:
]

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → IsZero (K.X i)
i : ℤ
hi : n < i
⊢ IsZero (K.X i)
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
i : ℤ
hi : i < n
⊢ ExactAt K i

Tactic:
]

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ i < n, ExactAt K i
i : ℤ
hi : i < n
⊢ ExactAt K i
Module: Mathlib.Algebra.Homology.Embedding.AreComplementary

Goal state before:
pp: case inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝³ : Category.{v_1, u_4} C
inst✝² : Abelian C
K : HomologicalComplex C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst✝¹ : e₁.IsTruncLE
inst✝ : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i₂ : ι₂
this : QuasiIsoAt (K.shortComplexTruncLE e₁).g (e₂.f i₂)
⊢ QuasiIsoAt (K.πTruncGE e₂) (e₂.f i₂)

Tactic:
]

Goal state after:
case inr
ι : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
c : ComplexShape ι
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
C : Type u_4
inst✝³ : Category.{v_1, u_4} C
inst✝² : Abelian C
K : HomologicalComplex C c
e₁ : c₁.Embedding c
e₂ : c₂.Embedding c
inst✝¹ : e₁.IsTruncLE
inst✝ : e₂.IsTruncGE
ac : e₁.AreComplementary e₂
i₂ : ι₂
this : QuasiIsoAt (K.shortComplexTruncLE e₁).g (e₂.f i₂)
⊢ QuasiIsoAt (K.πTruncGE e₂) (e₂.f i₂)
Module: Mathlib.Algebra.Homology.Embedding.CochainComplex

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
i : ℤ
hi : n < i
⊢ ExactAt K i

Tactic:
]

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
h : ∀ (i : ℤ), n < i → ExactAt K i
i : ℤ
hi : n < i
⊢ ExactAt K i
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 ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyLE p
⊢ ∀ (i : ℤ), q < i → IsZero (K.X i)

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyLE p
⊢ ∀ (i : ℤ), q < i → IsZero (K.X i)
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 ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyGE q
⊢ ∀ (i : ℤ), autoParam (i < p) isStrictlyGE_iff._auto_1 → IsZero (K.X i)

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsStrictlyGE q
⊢ ∀ (i : ℤ), autoParam (i < p) isStrictlyGE_iff._auto_1 → IsZero (K.X i)
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (HomotopyCategory.subcategoryAcyclic C).trW.HasLeftCalculusOfFractions

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (HomotopyCategory.subcategoryAcyclic C).trW.HasLeftCalculusOfFractions
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 ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsLE p
⊢ ∀ (i : ℤ), q < i → ExactAt K i

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsLE p
⊢ ∀ (i : ℤ), q < i → ExactAt K i
Module: Mathlib.Algebra.Homology.DerivedCategory.Fractions

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (HomotopyCategory.subcategoryAcyclic C).trW.HasRightCalculusOfFractions

Tactic:
]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ (HomotopyCategory.subcategoryAcyclic C).trW.HasRightCalculusOfFractions
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 ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsGE q
⊢ ∀ i < p, ExactAt K i

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K : CochainComplex C ℤ
p q : ℤ
hpq : p ≤ q
inst✝ : K.IsGE q
⊢ ∀ i < p, ExactAt K i
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
X' : HomologicalComplex C (ComplexShape.up ℤ)
s : X' ⟶ X
hs✝ : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s)
hs : IsIso (Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s))
g : X' ⟶ Y
hφ :
  f =
    { X' := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X',
          s := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s, hs := hs✝,
          f := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map g }.map
      Qh ⋯
⊢ ∃ X' s, ∃ (x : IsIso (Q.map s)), ∃ g, f = inv (Q.map s) ≫ Q.map g

Tactic:
]

Goal state after:
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
X' : HomologicalComplex C (ComplexShape.up ℤ)
s : X' ⟶ X
hs✝ : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s)
hs : IsIso (Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s))
g : X' ⟶ Y
hφ :
  f =
    { X' := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X',
          s := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s, hs := hs✝,
          f := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map g }.map
      Qh ⋯
⊢ ∃ X' s, ∃ (x : IsIso (Q.map s)), ∃ g, f = inv (Q.map s) ≫ Q.map g
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
⊢ ∃ X' s, ∃ (x : IsIso (Q.map s)), ∃ g, f = inv (Q.map s) ≫ Q.map g

Tactic:
have ⟨φ, hφ⟩ := Localization.exists_rightFraction Qh (HomotopyCategory.quasiIso C _) f
  obtain ⟨X', s, hs, g, rfl⟩ := φ.cases
  obtain ⟨X', rfl⟩ := HomotopyCategory.quotient_obj_surjective X'
  obtain ⟨s, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective s
  obtain ⟨g, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective g
  rw [← isIso_Qh_map_iff] at hs
  exact ⟨X', s, hs, g, hφ⟩

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 L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝ : HasZeroObject C
A : C
n : ℤ
⊢ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (((single C (up ℤ) n).obj A).X i)

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝ : HasZeroObject C
A : C
n : ℤ
⊢ ∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (((single C (up ℤ) n).obj A).X i)
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₂
⊢ (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₂) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝ =
    (singleFunctorCompHomologyFunctorIso C n).inv.app x✝¹ ≫
      (homologyFunctor C n).map ((singleFunctor C n).map f₂) ≫ (singleFunctorCompHomologyFunctorIso C n).hom.app x✝

Tactic:
]

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 L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝ : HasZeroObject C
A : C
n : ℤ
⊢ ∀ (i : ℤ), n < i → IsZero (((single C (up ℤ) n).obj A).X i)

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝ : HasZeroObject C
A : C
n : ℤ
⊢ ∀ (i : ℤ), n < i → IsZero (((single C (up ℤ) n).obj A).X i)
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 e.inv ≫ Q.map s)

Tactic:
]

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: 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
X' : HomologicalComplex C (ComplexShape.up ℤ)
s : Y ⟶ X'
hs✝ : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s)
hs : IsIso (Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s))
g : X ⟶ X'
hφ :
  f =
    { Y' := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X',
          f := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map g,
          s := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s, hs := hs✝ }.map
      Qh ⋯
⊢ ∃ Y' g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)

Tactic:
]

Goal state after:
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
X' : HomologicalComplex C (ComplexShape.up ℤ)
s : Y ⟶ X'
hs✝ : HomotopyCategory.quasiIso C (ComplexShape.up ℤ) ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s)
hs : IsIso (Qh.map ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s))
g : X ⟶ X'
hφ :
  f =
    { Y' := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj X',
          f := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map g,
          s := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map s, hs := hs✝ }.map
      Qh ⋯
⊢ ∃ Y' g s, ∃ (x : IsIso (Q.map s)), f = Q.map g ≫ inv (Q.map s)
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
this✝ : IsIso ((singleFunctor C n).map φ)
this : IsIso φ
⊢ IsIso ((CochainComplex.singleFunctor C n).map φ)

Tactic:
]

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
this✝ : IsIso ((singleFunctor C n).map φ)
this : IsIso φ
⊢ IsIso ((CochainComplex.singleFunctor C n).map φ)
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 ℤ
n : ℤ
inst✝ : X.IsStrictlyLE n
X' : CochainComplex C ℤ
s : X' ⟶ X
hs : IsIso (Q.map s)
g : X' ⟶ Y
⊢ ∀ i ≤ n, QuasiIsoAt s i

Tactic:
]

Goal state after:
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
⊢ ∀ i ≤ n, QuasiIsoAt s i
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 ℤ
n : ℤ
inst✝ : X.IsStrictlyLE n
X' : CochainComplex C ℤ
s : X' ⟶ X
hs : QuasiIso s
g : X' ⟶ Y
⊢ ∀ i ≤ n, QuasiIsoAt s i

Tactic:
]

Goal state after:
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 : QuasiIso s
g : X' ⟶ Y
⊢ ∀ i ≤ n, QuasiIsoAt s i
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 L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝³ : HasZeroObject C
inst✝² : ∀ (i : ℤ), HasHomology K i
inst✝¹ : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst✝ : K.IsGE n
⊢ K.IsGE n

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝³ : HasZeroObject C
inst✝² : ∀ (i : ℤ), HasHomology K i
inst✝¹ : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst✝ : K.IsGE n
⊢ K.IsGE n
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 L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝³ : HasZeroObject C
inst✝² : ∀ (i : ℤ), HasHomology K i
inst✝¹ : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst✝ : K.IsLE n
⊢ K.IsLE n

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
e : K ≅ L
inst✝³ : HasZeroObject C
inst✝² : ∀ (i : ℤ), HasHomology K i
inst✝¹ : ∀ (i : ℤ), HasHomology L i
n : ℤ
inst✝ : K.IsLE n
⊢ K.IsLE 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 : C
⊢ ((single C c j).obj A).iCycles j ≫ ((single C c j).obj A).pOpcycles j =
    ((single C c j).obj A).iCycles j ≫ ((single C c j).obj A).pOpcycles j

Tactic:
]

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 L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i') ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ (∀ (i : ℕ) (i' : ℤ), (embeddingUpIntGE n).f i = i' → QuasiIsoAt φ i') ↔ ∀ (i : ℤ), n ≤ i → QuasiIsoAt φ i
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) ≫ Q.map (X.ιTruncLE n))

Tactic:
]

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 : C
⊢ 𝟙 A = 𝟙 A

Tactic:
]

Goal state after:
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 : C
⊢ (singleObjOpcyclesSelfIso c j A).hom = (singleObjOpcyclesSelfIso c j A).hom

Tactic:
]

Goal state after:
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 : C
this : IsIso (((single C c j).obj A).iCycles j)
⊢ ((single C c j).obj A).iCycles j ≫ (singleObjXSelf c j A).hom =
    ((single C c j).obj A).iCycles j ≫ (singleObjXSelf c j A).hom

Tactic:
]

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 ℤ
n : ℤ
inst✝ : Y.IsStrictlyGE n
Y' : CochainComplex C ℤ
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
⊢ ∀ (i : ℤ), n ≤ i → QuasiIsoAt s i

Tactic:
]

Goal state after:
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)
⊢ ∀ (i : ℤ), n ≤ i → QuasiIsoAt s i