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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁✝ i₁'✝ : I₂
i₂✝ i₂'✝ : I₁
h₂ : c₂.Rel i₁✝ i₁'✝
h₁ : c₁.Rel i₂✝ i₂'✝
⊢ ((match (i₁✝, i₂✝) with
      | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂)) *
      match (i₁✝, i₂'✝) with
      | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂)) =
    (-match (i₁✝, i₂✝) with
        | (i₂, i₁) => c₁.ε₂ c₂ c₁₂ (i₁, i₂)) *
      match (i₁'✝, i₂✝) with
      | (i₂, i₁) => c₁.ε₁ c₂ c₁₂ (i₁, i₂)

Tactic:
by
    rw [neg_mul, ComplexShape.ε₂_ε₁ c₁₂ h₁ h₂, neg_mul, neg_neg]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' = 0

Tactic:
by_cases h₂ : c₂.Rel i₂ (c₂.next i₂)

Goal state after:
case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₂ : c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' = 0

case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₂ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' = 0
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
⊢ c₁.σ c₂ c i₁ i₂ • K.d₂ c i₁ i₂ j' =
    K.flip.d₁ c i₂ i₁ j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
by_cases h₂ : c₂.Rel i₂ (c₂.next i₂)

Goal state after:
case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.σ c₂ c i₁ i₂ • K.d₂ c i₁ i₂ j' =
    K.flip.d₁ c i₂ i₁ j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

case neg
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ c₁.σ c₂ c i₁ i₂ • K.d₂ c i₁ i₂ j' =
    K.flip.d₁ c i₂ i₁ j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ (f ≫ biprod.inl) ≫ s.π - (g ≫ biprod.inr) ≫ s.π = 0

Tactic:
← Preadditive.sub_comp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
sq : CommSq f g inl inr
h : IsColimit (PushoutCocone.mk inl inr ⋯)
s : Cofork (biprod.lift f (-g)) 0
⊢ (f ≫ biprod.inl - g ≫ biprod.inr) ≫ s.π = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
hm : n + 1 = m
hp : m + 1 = p
⊢ (Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯) ≫
      AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m) =
    0

Tactic:
ext x

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
hm : n + 1 = m
hp : m + 1 = p
x : ↑(KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯).pt
⊢ (AddCommGrpCat.Hom.hom
        ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯) ≫
          AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)))
      x =
    (AddCommGrpCat.Hom.hom 0) x
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
hm : n + 1 = m
hp : m + 1 = p
s : Cofork ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯)) 0
l : (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt ⟶ s.pt
hl : Cofork.π (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯) ≫ l = s.π
⊢ l = AddCommGrpCat.ofHom (CohomologyClass.descAddMonoidHom (AddCommGrpCat.Hom.hom s.π) ⋯)

Tactic:
ext x

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
hm : n + 1 = m
hp : m + 1 = p
s : Cofork ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯)) 0
l : (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt ⟶ s.pt
hl : Cofork.π (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯) ≫ l = s.π
x : ↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt
⊢ (AddCommGrpCat.Hom.hom l) x =
    (AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (CohomologyClass.descAddMonoidHom (AddCommGrpCat.Hom.hom s.π) ⋯))) x
Module: Mathlib.Algebra.Homology.DerivedCategory.KInjective

Goal state before:
pp: case e'_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝¹ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst✝ : L.IsKInjective
this : HasDerivedCategory C := ⋯
e_2✝ :
  ((HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj K ⟶
      (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)) =
    (Qh.obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ⟶
      Qh.obj
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
          ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L)))
⊢ ⇑(((quotientCompQhIso C).symm.app K).homCongr
          ((Functor.commShiftIso Q n).symm.app L ≪≫
            (quotientCompQhIso C).symm.app ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L))) ∘
      ⇑(SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) Q) ∘ toSmallShiftedHom =
    Qh.map ∘ ⇑toHom

Tactic:
ext x

Goal state after:
case e'_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝¹ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
inst✝ : L.IsKInjective
this : HasDerivedCategory C := HasDerivedCategory.standard C
e_2✝ :
  ((HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj K ⟶
      (HomotopyCategory.quotient C (ComplexShape.up ℤ) ⋙ Qh).obj
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)) =
    (Qh.obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K) ⟶
      Qh.obj
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
          ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n).obj L)))
x : CohomologyClass K L n
⊢ (⇑(((quotientCompQhIso C).symm.app K).homCongr
            ((Functor.commShiftIso Q n).symm.app L ≪≫
              (quotientCompQhIso C).symm.app ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L))) ∘
        ⇑(SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) Q) ∘ toSmallShiftedHom)
      x =
    (Qh.map ∘ ⇑toHom) x
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
H_zero : H 0
n : ℤ
X : C
hX : t.ge 1 ((shiftFunctor C n).obj X)
⊢ t.ge n X

Tactic:
rw [← t.shift_ge n 0 n (add_zero n)]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
H : ℕ → Prop := fun a ↦ ∀ (n : ℤ), t.ge (n + ↑a) ≤ t.ge n
H_zero : H 0
n : ℤ
X : C
hX : t.ge 1 ((shiftFunctor C n).obj X)
⊢ (t.ge 0).shift n X
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
X : C
n a n' : ℤ
hn' : a + n' = n
inst✝ : t.IsGE ((shiftFunctor C a).obj X) n'
⊢ t.IsGE X n

Tactic:
have h := t.isGE_shift (X⟦a⟧) n' (-a) n
  exact t.isGE_of_iso (show X⟦a⟧⟦-a⟧ ≅ X from (shiftEquiv C a).unitIso.symm.app X) n

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
K : CochainComplex C ℤ
n : ℤ
inst✝ : K.IsGE n
⊢ (Q.obj K).IsGE n

Tactic:
rw [isGE_Q_obj_iff]
  infer_instance

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : WeakEquivalence f
⊢ WeakEquivalence f.op

Tactic:
weakEquivalences_op_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : WeakEquivalence f
⊢ WeakEquivalence f
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h✝¹ : LeftHomotopyRel f g
Z : C
i : Z ⟶ X
P : Cylinder X
left✝ : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder Z
h✝ : Q.IsVeryGood
sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
⊢ Q.i₁ ≫ sq.lift ≫ h.h = i ≫ g

Tactic:
by
        have := coprod.inr ≫= sq.fac_left
        simp only [Q.inr_i_assoc, coprod.inr_desc] at this
        simp [reassoc_of% this]

Goal state after:
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 ℤ
hK : CochainComplex.plus C K
⊢ CochainComplex.plus C (cylinder K)

Tactic:
obtain ⟨n, hn⟩ := hK
  refine ⟨n - 1, ?_⟩
  rw [CochainComplex.isStrictlyGE_iff]
  intro i hi
  dsimp [cylinder]
  refine homotopyCofiber.isZero_X _ _ ?_ (fun j hj ↦ ?_)
  · refine IsZero.of_iso ?_ ((HomologicalComplex.eval C (.up ℤ) i).mapBiprod _ _)
    simpa using K.isZero_of_isStrictlyGE n i
  · simp only [ComplexShape.up_Rel] at hj
    exact K.isZero_of_isStrictlyGE n _ (by lia)

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
X : C
⊢ t.IsGE X n₁ ↔ IsIso ((t.truncGTπ n₀).app X)

Tactic:
rw [t.isGE_iff_isIso_truncGEπ_app n₁ X]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
X : C
⊢ IsIso ((t.truncGEπ n₁).app X) ↔ IsIso ((t.truncGTπ n₀).app X)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ t.IsGE X n₁ ↔ IsZero ((t.truncLE n₀).obj X)

Tactic:
rw [t.isGE_iff_isIso_truncGEπ_app n₁ X]

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ IsIso ((t.truncGEπ n₁).app X) ↔ IsZero ((t.truncLE n₀).obj X)
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful

Tactic:
let := Localization.preadditive L₁ (B.inverseImage A.ι).trW

Goal state after:
C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : Category.{v_2, u_2} D
inst✝¹³ : Category.{v_3, u_3} D₁
inst✝¹² : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
this : Preadditive D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful
Module: Mathlib.Algebra.Homology.Factorizations.CM5b

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
inst✝¹ : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
inst✝ : K.IsStrictlyGE n
⊢ (I K).IsStrictlyGE n

Tactic:
by
  rw [isStrictlyGE_iff]
  intro i hi
  exact Injective.isZero_under _ (K.isZero_of_isStrictlyGE n i hi)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr) ≫ (biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s) + (g₁ ≫ g₂) ≫ σ₂.s ≫ σ₁.s =
    𝟙 X

Tactic:
have h := g₁ ≫= σ₂.id =≫ σ₁.s

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
I₁ : C
w✝¹ : Injective I₁
f₁ : I₁ ⟶ X
w₁ : f₁ ≫ g₁ = 0
σ₁ : { X₁ := I₁, X₂ := X, X₃ := Y, f := f₁, g := g₁, zero := w₁ }.Splitting
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
h :
  g₁ ≫
      (σ₂.r ≫ { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.f +
          { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.g ≫ σ₂.s) ≫
        σ₁.s =
    g₁ ≫ 𝟙 { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.X₂ ≫ σ₁.s
⊢ (σ₁.r ≫ biprod.inl + g₁ ≫ σ₂.r ≫ biprod.inr) ≫ (biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s) + (g₁ ≫ g₂) ≫ σ₂.s ≫ σ₁.s =
    𝟙 X
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
X Y : C
p : X ⟶ Y
A B : C
i : A ⟶ B
inst✝ : Mono i
I : C
w✝ : Injective I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs }.Splitting
hI : (MorphismProperty.monomorphisms C).rlp 0
⊢ IsLimit (PullbackCone.mk σ.r p ⋯)

Tactic:
refine PullbackCone.IsLimit.mk _ (fun t ↦ t.fst ≫ s + t.snd ≫ σ.s)
    (fun t ↦ by simp [dsimp% σ.f_r]) (fun t ↦ by simp [hs, dsimp% σ.s_g]) (fun t m hm₁ hm₂ ↦ ?_)

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
X Y : C
p : X ⟶ Y
A B : C
i : A ⟶ B
inst✝ : Mono i
I : C
w✝ : Injective I
s : I ⟶ X
hs : s ≫ p = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs }.Splitting
hI : (MorphismProperty.monomorphisms C).rlp 0
t : PullbackCone 0 0
m : t.pt ⟶ { X₁ := I, X₂ := X, X₃ := Y, f := s, g := p, zero := hs }.X₂
hm₁ : m ≫ σ.r = t.fst
hm₂ : m ≫ p = t.snd
⊢ m = t.fst ≫ s + t.snd ≫ σ.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 : ℤ
Y X : C
f₁ f₂ : Y ⟶ (t.truncLT n).obj X
h : f₁ ≫ (t.truncLTι n).app X = f₂ ≫ (t.truncLTι n).app X
inst✝ : t.IsLE Y (n - 1)
f : Y ⟶ (t.truncLT n).obj X
hf : f ≫ (t.truncLTι n).app X = 0
g : Y ⟶ ((t.triangleLTGE n).obj X).invRotate.obj₁
hg : f = g ≫ ((t.triangleLTGE n).obj X).invRotate.mor₁
⊢ t.IsGE ((t.triangleLTGE n).obj X).invRotate.obj₁ (n + 1)

Tactic:
dsimp; apply (t.isGE_shift _ n (-1) (n + 1) (by lia))

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i j : ℕ
h : i = j
⊢ X i = X j

Tactic:
by rw [h]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i j : ℕ
h : i = j
⊢ X (j + 1) = X (i + 1)

Tactic:
by rw [h]

Goal state after:
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₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
hX : ∀ (Y : C) (f : X ⟶ Y), t.IsGE Y n₁ → f = 0
⊢ t.IsLE X n₀

Tactic:
rw [t.isLE_iff_isZero_truncGE_obj n₀ n₁ h, IsZero.iff_id_eq_zero]

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₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
hX : ∀ (Y : C) (f : X ⟶ Y), t.IsGE Y n₁ → f = 0
⊢ 𝟙 ((t.truncGE n₁).obj X) = 0
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 : ℤ
⊢ IsIso ((t.truncLT n).map f) ↔
    ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n

Tactic:
by
  refine ⟨fun hf ↦ ?_, fun ⟨Z, g, h, mem, _⟩ ↦ ?_⟩
  · refine ⟨(t.truncGE n).obj Y, (t.truncGEπ n).app Y,
      (t.truncGEδLT n).app Y ≫ (inv ((t.truncLT n).map f))⟦1⟧',
      isomorphic_distinguished _ (t.triangleLTGE_distinguished n Y) _ ?_, inferInstance⟩
    exact Triangle.isoMk _ _ (asIso ((t.truncLT n).map f)) (Iso.refl _) (Iso.refl _)
  · obtain ⟨e, he⟩ := t.triangle_iso_exists
      mem (t.triangleLTGE_distinguished n Y) (Iso.refl _) (n - 1) n
      (by dsimp; infer_instance) (by dsimp; infer_instance)
      (by dsimp; infer_instance) (by dsimp; infer_instance)
    suffices ((t.truncLT n).map f) = e.hom.hom₁ by rw [this]; infer_instance
    exact t.to_truncLT_obj_ext (Eq.trans (by cat_disch) e.hom.comm₁)

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case neg
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
a b : ℤ
X : C
h : ¬a ≤ b
⊢ IsIso ((t.truncGELTToLTGE a b).app X)

Tactic:
simp at h

Goal state after:
case neg
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
a b : ℤ
X : C
h : b < a
⊢ IsIso ((t.truncGELTToLTGE a b).app X)
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₁ i : ℤ
hi : i ≠ n₁
⊢ IsIso ((π K L n₁).f i)

Tactic:
refine ⟨(biprod.inr : _ ⟶ mid K L n₁).f i, ?_, by simp⟩
  rw [biprodX_ext_to_iff]
  constructor
  · apply (isZero_single_obj_X (.up ℤ) _ _ _ hi).eq_of_tgt
  · simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
inst✝² : IsCofibrant X
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
⊢ Function.Bijective fun f ↦ f.postcomp g

Tactic:
constructor
  · intro f₀ f₁ h
    obtain ⟨f₀, rfl⟩ := f₀.mk_surjective
    obtain ⟨f₁, rfl⟩ := f₁.mk_surjective
    simp only [postcomp_mk, mk_eq_mk_iff] at h
    obtain ⟨P, _, ⟨h⟩⟩ := h.exists_good_cylinder
    have sq : CommSq (coprod.desc f₀ f₁) P.i g h.h := { }
    rw [mk_eq_mk_iff]
    exact ⟨P,
      ⟨{h := sq.lift
        h₀ := by
          have := coprod.inl ≫= sq.fac_left
          rwa [P.inl_i_assoc, coprod.inl_desc] at this
        h₁ := by
          have := coprod.inr ≫= sq.fac_left
          rwa [P.inr_i_assoc, coprod.inr_desc] at this }⟩⟩
  · intro φ
    obtain ⟨φ, rfl⟩ := φ.mk_surjective
    have sq : CommSq (initial.to Y) (initial.to X) g φ := { }
    exact ⟨mk sq.lift, by simp⟩

Goal state after: