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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c * t.z a b)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫ (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom =
    (↑(t.z a (b + c)) * ↑(t.z b c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      eqToHom ⋯ ≫
        ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom

Tactic:
← Units.val_mul,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
a b c : A
X : t.Category
⊢ (↑(t.z (a + b) c * t.z a b)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      ((shiftFunctorAdd C (a + b) c).app X).hom ≫ (shiftFunctor C c).map ((shiftFunctorAdd C a b).app X).hom =
    (↑(t.z a (b + c) * t.z b c)).app ((shiftFunctor C (a + b + c)).obj X) ≫
      eqToHom ⋯ ≫
        ((shiftFunctorAdd C a (b + c)).app X).hom ≫ ((shiftFunctorAdd C b c).app ((shiftFunctor C a).obj X)).hom
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
i j k : A
h : i + j = k
X : t.Category
this : (shiftFunctorAdd' t.Category i j k h).hom.app X = ↑(t.z i j) • (shiftFunctorAdd' C i j k h).hom.app X
⊢ (shiftFunctorAdd' t.Category i j k h).hom.app X =
    ↑(t.z i j) •
      (t.shiftIso k).hom.app X ≫
        (shiftFunctorAdd' C i j k h).hom.app X ≫
          (shiftFunctor C j).map ((t.shiftIso i).inv.app X) ≫ (t.shiftIso j).inv.app ((shiftFunctor t.Category i).obj X)

Tactic:
rw [this]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
i j k : A
h : i + j = k
X : t.Category
this : (shiftFunctorAdd' t.Category i j k h).hom.app X = ↑(t.z i j) • (shiftFunctorAdd' C i j k h).hom.app X
⊢ ↑(t.z i j) • (shiftFunctorAdd' C i j k h).hom.app X =
    ↑(t.z i j) •
      (t.shiftIso k).hom.app X ≫
        (shiftFunctorAdd' C i j k h).hom.app X ≫
          (shiftFunctor C j).map ((t.shiftIso i).inv.app X) ≫ (t.shiftIso j).inv.app ((shiftFunctor t.Category i).obj X)
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
i j k : A
h : i + j = k
X : t.Category
this : (shiftFunctorAdd' t.Category i j k h).inv.app X = ↑(t.z i j)⁻¹ • (shiftFunctorAdd' C i j k h).inv.app X
⊢ (shiftFunctorAdd' t.Category i j k h).inv.app X =
    ↑(t.z i j)⁻¹ •
      (t.shiftIso j).hom.app ((shiftFunctor t.Category i).obj X) ≫
        (shiftFunctor C j).map ((t.shiftIso i).hom.app X) ≫
          (shiftFunctorAdd' C i j k h).inv.app X ≫ (t.shiftIso k).inv.app X

Tactic:
rw [this]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
i j k : A
h : i + j = k
X : t.Category
this : (shiftFunctorAdd' t.Category i j k h).inv.app X = ↑(t.z i j)⁻¹ • (shiftFunctorAdd' C i j k h).inv.app X
⊢ ↑(t.z i j)⁻¹ • (shiftFunctorAdd' C i j k h).inv.app X =
    ↑(t.z i j)⁻¹ •
      (t.shiftIso j).hom.app ((shiftFunctor t.Category i).obj X) ≫
        (shiftFunctor C j).map ((t.shiftIso i).hom.app X) ≫
          (shiftFunctorAdd' C i j k h).inv.app X ≫ (t.shiftIso k).inv.app X
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n n' : ℤ
h : n + x = n'
⊢ ((K.totalDesc fun p q hpq ↦
        (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯).inv ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p - x) q n ⋯) ≫
      ((shiftFunctor₁ C x).obj K).totalDesc fun p q hpq ↦ K.ιTotal (up ℤ) (p + x) q n' ⋯) =
    𝟙 ((K.total (up ℤ)).X n')

Tactic:
by
    ext
    dsimp
    simp only [ι_totalDesc_assoc, Category.assoc, ι_totalDesc, XXIsoOfEq_inv_ιTotal, comp_id]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
x✝ : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
hX₃ : P X₃
⊢ Function.Injective fun g ↦ f ≫ g

Tactic:
suffices ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0 from fun α₁ α₂ hα ↦ by
      simpa [sub_eq_zero] using this (α₁ - α₂) (by simpa [sub_eq_zero] using hα)

Goal state after:
case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
x✝ : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
hX₃ : P X₃
⊢ ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
α : Cochain K L (-1)
n : ℤ
hα : (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst✝ : Injective (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
eq : α.v n (n - 1) ⋯ ≫ L.d (n - 1) n + K.d n (n + 1) ≫ α.v (n + 1) n ⋯ = f.f n
⊢ K.d n (n + 1) ≫ u = 0

Tactic:
simp only [u, comp_sub, HomologicalComplex.d_comp_d_assoc, zero_comp,
      ← f.comm, ← eq, add_comp, Category.assoc, L.d_comp_d, comp_zero, zero_add, sub_self]

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
inst✝¹ : X.IsGE n
inst✝ : X.IsLE n
K : CochainComplex C ℤ
w✝¹ : K.IsStrictlyGE n
w✝ : K.IsStrictlyLE n
e : X ≅ Q.obj K
⊢ ∃ Y, Nonempty (X ≅ (singleFunctor C n).obj Y)

Tactic:
obtain ⟨Y, ⟨e'⟩⟩ := CochainComplex.exists_iso_single K n

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Abelian C
inst✝² : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
inst✝¹ : X.IsGE n
inst✝ : X.IsLE n
K : CochainComplex C ℤ
w✝¹ : K.IsStrictlyGE n
w✝ : K.IsStrictlyLE n
e : X ≅ Q.obj K
Y : C
e' : K ≅ (HomologicalComplex.single C (ComplexShape.up ℤ) n).obj Y
⊢ ∃ Y, Nonempty (X ≅ (singleFunctor C n).obj Y)
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : CategoryWithWeakEquivalences C
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst✝³ : HasPushout f g
inst✝² : (trivialCofibrations C).IsStableUnderCobaseChange
inst✝¹ : Cofibration g
inst✝ : WeakEquivalence g
⊢ WeakEquivalence (pushout.inl f g)

Tactic:
rw [weakEquivalence_iff]
  exact (MorphismProperty.of_isPushout (IsPushout.of_hasPushout f g)
    (mem_trivialCofibrations g)).2

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
A : C
inst✝⁴ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝³ : HasBinaryCoproducts C
inst✝² : CategoryWithCofibrations C
inst✝¹ : P.IsGood
inst✝ : (cofibrations C).RespectsIso
hi : cofibrations C P.i
⊢ cofibrations C ((coprod.braiding A A).hom ≫ P.i)

Tactic:
refine ((cofibrations C).arrow_mk_iso_iff ?_).2 hi

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
A : C
inst✝⁴ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝³ : HasBinaryCoproducts C
inst✝² : CategoryWithCofibrations C
inst✝¹ : P.IsGood
inst✝ : (cofibrations C).RespectsIso
hi : cofibrations C P.i
⊢ Arrow.mk ((coprod.braiding A A).hom ≫ P.i) ≅ Arrow.mk P.i
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
j : ℤ
hj : (ComplexShape.up ℤ).Rel i j
⊢ IsZero (K.X j)

Tactic:
simp only [ComplexShape.up_Rel] at hj

Goal state after:
case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
j : ℤ
hj : i + 1 = j
⊢ IsZero (K.X j)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
j : ℤ
hj : (ComplexShape.up ℤ).Rel j i
⊢ IsZero (K.X j)

Tactic:
simp only [ComplexShape.up_Rel] at hj

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n - 1) isStrictlyGE_iff._auto_1
j : ℤ
hj : j + 1 = i
⊢ IsZero (K.X j)
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : Cᵒᵖ⦄ (s : X ⟶ Y), A.op X → B.op.trW s → ∃ Z s' b, A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s'
X Y : C
s : X ⟶ Y
hY : A Y
hs : B.trW s
⊢ ∃ Z s' a, A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'

Tactic:
obtain ⟨Z', s', b, hZ', hs', fac⟩ := hA s.op hY (by simpa [trW_op_iff])

Goal state after:
case refine_1
C : Type u_1
inst✝⁸ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : A.IsTriangulated
inst✝¹ : B.IsTriangulated
inst✝ : B.IsClosedUnderIsomorphisms
hA : ∀ ⦃X Y : Cᵒᵖ⦄ (s : X ⟶ Y), A.op X → B.op.trW s → ∃ Z s' b, A.op Z ∧ (A.op ⊓ B.op).trW s' ∧ s ≫ b = s'
X Y : C
s : X ⟶ Y
hY : A Y
hs : B.trW s
Z' : Cᵒᵖ
s' : op Y ⟶ Z'
b : op X ⟶ Z'
hZ' : A.op Z'
hs' : (A.op ⊓ B.op).trW s'
fac : s.op ≫ b = s'
⊢ ∃ Z s' a, A Z ∧ (A ⊓ B).trW s' ∧ a ≫ s = s'
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ : ℤ
X : C
x✝ : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = (Iso.refl X).hom
he' : e.inv.hom₂ = 𝟙 X
this : (t.truncLTι (n₀ + 1)).app X = e.inv.hom₁
⊢ IsIso ((t.truncLTι (n₀ + 1)).app X)

Tactic:
rw [this]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ : ℤ
X : C
x✝ : t.IsLE X n₀
e : contractibleTriangle X ≅ (t.triangleLTGE (n₀ + 1)).obj X
he : e.hom.hom₂ = (Iso.refl X).hom
he' : e.inv.hom₂ = 𝟙 X
this : (t.truncLTι (n₀ + 1)).app X = e.inv.hom₁
⊢ IsIso e.inv.hom₁
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case mp
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X : C
h : t.IsGE X n
e : (contractibleTriangle X).invRotate ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = 𝟙 X
this : (t.truncGEπ n).app X = e.hom.hom₃
⊢ IsIso ((t.truncGEπ n).app X)

Tactic:
rw [this]

Goal state after:
case mp
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X : C
h : t.IsGE X n
e : (contractibleTriangle X).invRotate ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = 𝟙 X
this : (t.truncGEπ n).app X = e.hom.hom₃
⊢ IsIso e.hom.hom₃
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
e : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ≅ (t.triangleLTGE n).obj Y
he : e.hom.hom₂ = (Iso.refl (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₂).hom
this : (t.truncLT n).map f = e.hom.hom₁
⊢ IsIso ((t.truncLT n).map f)

Tactic:
rw [this]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
e : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ≅ (t.triangleLTGE n).obj Y
he : e.hom.hom₂ = (Iso.refl (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₂).hom
this : (t.truncLT n).map f = e.hom.hom₁
⊢ IsIso e.hom.hom₁
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
x✝ : ∃ X f h, ∃ (_ : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles), t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles
h✝ : t.IsLE X n₀
e : (t.triangleLTGE n₁).obj Y ≅ Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h
he : e.hom.hom₂ = (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂).hom
this : (t.truncGE n₁).map g = e.hom.hom₃
⊢ IsIso ((t.truncGE n₁).map g)

Tactic:
rw [this]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
x✝ : ∃ X f h, ∃ (_ : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles), t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles
h✝ : t.IsLE X n₀
e : (t.triangleLTGE n₁).obj Y ≅ Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h
he : e.hom.hom₂ = (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂).hom
this : (t.truncGE n₁).map g = e.hom.hom₃
⊢ IsIso e.hom.hom₃
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
⊢ IsIso ((t.truncGE n₁).map T.mor₂)

Tactic:
rw [isIso_truncGE_map_iff _ _ _ _ h]
  obtain ⟨X, f, k, mem⟩ := distinguished_cocone_triangle₁ (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃)
  refine ⟨_, _, _, mem, ?_⟩
  subst h
  have H := someOctahedron rfl (rot_of_distTriang _ hT)
    (rot_of_distTriang _ (t.triangleLTGE_distinguished (n₀ + 1) T.obj₃))
    (rot_of_distTriang _ mem)
  have : t.IsLE (X⟦(1 : ℤ)⟧) (n₀ - 1) :=
    t.isLE₂ _ H.mem (n₀ - 1) (t.isLE_shift T.obj₁ n₀ 1 (n₀ - 1) (by lia))
      (t.isLE_shift ((t.truncLT (n₀ + 1)).obj T.obj₃) n₀ 1 (n₀-1) (by lia))
  exact t.isLE_of_shift X n₀ 1 (n₀ - 1) (by lia)

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this✝¹ : Epi π
this✝ : Mono ι
n : ℤ
this : (δ 1 2 ↑(cocycle₁' sq hsq)).v n (n + 2) ⋯ = Cochain.v 0 n (n + 2) ⋯
⊢ (δ 1 2 (cochain₁ sq hsq hQ hK)).v n (n + 2) ⋯ = Cochain.v 0 n (n + 2) ⋯

Tactic:
Cochain.zero_v,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this✝¹ : Epi π
this✝ : Mono ι
n : ℤ
this : (δ 1 2 ↑(cocycle₁' sq hsq)).v n (n + 2) ⋯ = 0
⊢ (δ 1 2 (cochain₁ sq hsq hQ hK)).v n (n + 2) ⋯ = 0
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: case hL
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
X : Plus C
⊢ IsZero (⊤_ Plus C).obj

Tactic:
exact Functor.map_isZero (Plus.ι C) (IsZero.of_mono_zero _ X)

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₁ : ℤ
⊢ degreewiseEpiWithInjectiveKernel (π K L n₁)

Tactic:
intro q

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₁ q : ℤ
⊢ epiWithInjectiveKernel ((π K L n₁).f q)
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: case inr
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : A ⟶ B
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono i
p : X ⟶ Y
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel p
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : A ⟶ X
b : B ⟶ Y
sq✝ : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
sq : CommSq t i p b
sq' : ∀ (n : ℤ), CommSq (t.f n) (i.f n) (p.f n) (b.f n)
this✝¹ : ∀ (n : ℤ), ⋯.HasLift
β : Cocycle (cokernel i) (kernel p) 1 :=
  Lifting.cocycle₁ sq (fun n ↦ { l := ⋯.lift, fac_left := ⋯, fac_right := ⋯ }) (cokernelIsCokernel i) (kernelIsKernel p)
this✝ : ∀ (n : ℤ), Injective ((kernel p).X n)
this : (kernel p).IsKInjective
h✝ : QuasiIso p
⊢ ∃ α, δ 0 1 α = ↑β

Tactic:
· refine IsKInjective.eq_δ_of_cocycle' β ?_ 0 (by simp)
        have := hp.epi
        have : (ShortComplex.mk _ _ (kernel.condition p)).ShortExact :=
          { exact := ShortComplex.exact_kernel p }
        exact this.acyclic_X₁ (by dsimp; infer_instance)

Goal state after:
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: case mp
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_4, u_4} D₁
inst✝ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
this : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom
⊢ w.GuitartExact

Tactic:
rw [this]

Goal state after:
case mp
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_4, u_4} D₁
inst✝ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
this : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom
⊢ ((w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom).GuitartExact
Module: Mathlib.CategoryTheory.GuitartExact.Opposite

Goal state before:
pp: case mp
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
a✝ : w.op.GuitartExact
w₁ : TwoSquare T (opOp C₁) (opOp C₂) T.op.op := 𝟙 (T ⋙ opOp C₂)
w₂ : TwoSquare B.op.op (unopUnop C₃) (unopUnop C₄) B := 𝟙 (B.op.op ⋙ unopUnop C₄)
this : w = (w₁ ≫ᵥ w.op.op) ≫ᵥ w₂
⊢ w.GuitartExact

Tactic:
rw [this]

Goal state after:
case mp
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
a✝ : w.op.GuitartExact
w₁ : TwoSquare T (opOp C₁) (opOp C₂) T.op.op := 𝟙 (T ⋙ opOp C₂)
w₂ : TwoSquare B.op.op (unopUnop C₃) (unopUnop C₄) B := 𝟙 (B.op.op ⋙ unopUnop C₄)
this : w = (w₁ ≫ᵥ w.op.op) ≫ᵥ w₂
⊢ ((w₁ ≫ᵥ w.op.op) ≫ᵥ w₂).GuitartExact