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

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₁'
inst✝⁵ : Category.{v_3, u_3} C₂
inst✝⁴ : Category.{v_4, u_4} C₂'
inst✝³ : Category.{v_5, u_5} D
inst✝² : Preadditive D
inst✝¹ : HasShift D ℤ
inst✝ : ∀ (n : ℤ), (shiftFunctor D n).Additive
x✝² x✝¹ x✝ : ℤ × ℤ
⊢ (-1) ^ ((x✝² + x✝¹).1 * x✝.2) * (-1) ^ (x✝².1 * x✝¹.2) = (-1) ^ (x✝².1 * (x✝¹ + x✝).2) * (-1) ^ (x✝¹.1 * x✝.2)

Tactic:
dsimp
    rw [← zpow_add, ← zpow_add]
    #adaptation_note /-- After https://github.com/leanprover/lean4/pull/13593
    we need to re-enable model-based theory combination in `lia` for this to go through. -/
    lia +mbtc

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
p q p' q' : ℤ
hp : p + p' = 0
hq : q + q' = 0
⊢ (homotopyOp h).hom p q =
    (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ (h.hom q' p').op ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op

Tactic:
obtain rfl : p' = -p := by lia

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy f g
p q q' : ℤ
hq : q + q' = 0
hp : p + -p = 0
⊢ (homotopyOp h).hom p q =
    (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ (h.hom q' (-p)).op ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
Module: Mathlib.Algebra.Homology.CochainComplexPlus

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).LimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
⊢ CochainComplex.plus C K

Tactic:
refine ⟨n, ?_⟩

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasLimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).LimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
⊢ K.IsStrictlyGE n
Module: Mathlib.Algebra.Homology.CochainComplexPlus

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).ColimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
⊢ CochainComplex.plus C K

Tactic:
refine ⟨n, ?_⟩

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
J : Type u_2
inst✝² : SmallCategory J
inst✝¹ : FinCategory J
inst✝ : HasColimitsOfShape J C
K : CochainComplex C ℤ
p : (CochainComplex.plus C).ColimitOfShape J K
n : ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE n
⊢ K.IsStrictlyGE n
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ h.hom n (n - 1) ≫ (K.d (-n) (-(n - 1))).op =
    (((HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom (- -n) (- -(n - 1))) ≫
        (HomologicalComplex.XIsoOfEq K ⋯).hom.op) ≫
      (K.d (-n) (-(n - 1))).op

Tactic:
simp [H (- -n) (- -(n - 1)) n (n - 1) (by lia) (by lia), ← op_comp_assoc]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
p q p' q' : ℤ
hp : p + p' = 0
hq : q + q' = 0
⊢ (homotopyUnop h).hom p q =
    (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom q' p').unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom

Tactic:
obtain rfl : p' = -p := by lia

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
p q q' : ℤ
hq : q + q' = 0
hp : p + -p = 0
⊢ (homotopyUnop h).hom p q =
    (HomologicalComplex.XIsoOfEq K ⋯).hom ≫ (h.hom q' (-p)).unop ≫ (HomologicalComplex.XIsoOfEq L ⋯).hom
Module: Mathlib.Algebra.Homology.ConcreteCategory

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))
hx₃ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.d i j))) x₃ = 0
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.g.f i))) x₂ = x₃
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
hk : c.next j = k
| (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.toCycles i j ≫ S.X₂.iCycles j))) x₂

Tactic:
HomologicalComplex.toCycles_i

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type v
inst✝⁵ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝⁴ : ConcreteCategory C FC
inst✝³ : HasForget₂ C Ab
inst✝² : Abelian C
inst✝¹ : (forget₂ C Ab).Additive
inst✝ : (forget₂ C Ab).PreservesHomology
ι : Type u_2
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
x₃ : ↑((forget₂ C Ab).obj (S.X₃.X i))
hx₃ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₃.d i j))) x₃ = 0
x₂ : ↑((forget₂ C Ab).obj (S.X₂.X i))
hx₂ : (ConcreteCategory.hom ((forget₂ C Ab).map (S.g.f i))) x₂ = x₃
x₁ : ↑((forget₂ C Ab).obj (S.X₁.X j))
hx₁ :
  (ConcreteCategory.hom ((forget₂ C Ab).map (S.f.f j))) x₁ = (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) x₂
k : ι
hk : c.next j = k
| (ConcreteCategory.hom ((forget₂ C Ab).map (S.X₂.d i j))) 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 Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE Y n₁
⊢ f = 0

Tactic:
by
  have := t.isLE_shift X n₀ n₀ 0 (add_zero n₀)
  have := t.isGE_shift Y n₁ n₀ (n₁ - n₀)
  have := t.isGE_of_ge (Y⟦n₀⟧) 1 (n₁ - n₀)
  apply (shiftFunctor C n₀).map_injective
  simp only [Functor.map_zero]
  apply t.zero'
  · apply t.le_of_isLE
  · apply t.ge_of_isGE

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

Goal state before:
pp: case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
K : CochainComplex C ℤ
e : X ≅ Q.obj K
h✝ : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ IsZero ((homologyFunctor C i).obj X)

Tactic:
apply ((K.exactAt_of_isLE n i hi).isZero_homology).of_iso

Goal state after:
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
n : ℤ
K : CochainComplex C ℤ
e : X ≅ Q.obj K
h✝ : K.IsStrictlyLE n
i : ℤ
hi : n < i
⊢ (homologyFunctor C i).obj X ≅ HomologicalComplex.homology K i
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
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ WeakEquivalence f.unop

Tactic:
weakEquivalences_unop_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithWeakEquivalences C
X Y : Cᵒᵖ
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ WeakEquivalence f
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]

Goal state after:
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
⊢ weakEquivalences C (pushout.inl f g)
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 f
inst✝ : WeakEquivalence f
⊢ WeakEquivalence (pushout.inr f g)

Tactic:
rw [weakEquivalence_iff]

Goal state after:
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 f
inst✝ : WeakEquivalence f
⊢ weakEquivalences C (pushout.inr f g)
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 ⟶ Z
g : Y ⟶ Z
inst✝³ : HasPullback f g
inst✝² : (trivialFibrations C).IsStableUnderBaseChange
inst✝¹ : Fibration f
inst✝ : WeakEquivalence f
⊢ WeakEquivalence (pullback.snd f g)

Tactic:
rw [weakEquivalence_iff]

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : CategoryWithWeakEquivalences C
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝³ : HasPullback f g
inst✝² : (trivialFibrations C).IsStableUnderBaseChange
inst✝¹ : Fibration f
inst✝ : WeakEquivalence f
⊢ weakEquivalences C (pullback.snd f g)
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 ⟶ Z
g : Y ⟶ Z
inst✝³ : HasPullback f g
inst✝² : (trivialFibrations C).IsStableUnderBaseChange
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
⊢ WeakEquivalence (pullback.fst f g)

Tactic:
rw [weakEquivalence_iff]

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : CategoryWithWeakEquivalences C
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝³ : HasPullback f g
inst✝² : (trivialFibrations C).IsStableUnderBaseChange
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
⊢ weakEquivalences C (pullback.fst f g)
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
J✝ : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst✝³ : HasCoproduct X
inst✝² : HasCoproduct Y
h : ∀ (i : J), Cofibration (f i)
inst✝¹ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝ : ∀ (i : J), WeakEquivalence (f i)
⊢ WeakEquivalence (Limits.Sigma.map f)

Tactic:
rw [weakEquivalence_iff]

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : CategoryWithWeakEquivalences C
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
J✝ : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst✝³ : HasCoproduct X
inst✝² : HasCoproduct Y
h : ∀ (i : J), Cofibration (f i)
inst✝¹ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝ : ∀ (i : J), WeakEquivalence (f i)
⊢ weakEquivalences C (Limits.Sigma.map f)
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
J✝ : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst✝³ : HasProduct X
inst✝² : HasProduct Y
h : ∀ (i : J), Fibration (f i)
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : ∀ (i : J), WeakEquivalence (f i)
⊢ WeakEquivalence (Limits.Pi.map f)

Tactic:
rw [weakEquivalence_iff]

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : CategoryWithWeakEquivalences C
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
J✝ : Type w
J : Type u_1
X Y : J → C
f : (i : J) → X i ⟶ Y i
inst✝³ : HasProduct X
inst✝² : HasProduct Y
h : ∀ (i : J), Fibration (f i)
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : ∀ (i : J), WeakEquivalence (f i)
⊢ weakEquivalences C (Limits.Pi.map f)
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 : C
f : X ⟶ Y
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝¹ : (weakEquivalences C).IsStableUnderRetracts
inst✝ : IsIso f
h : (trivialCofibrations C).MapFactorizationData (fibrations C) f
⊢ WeakEquivalence f

Tactic:
rw [weakEquivalence_iff]

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X Y : C
f : X ⟶ Y
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝¹ : (weakEquivalences C).IsStableUnderRetracts
inst✝ : IsIso f
h : (trivialCofibrations C).MapFactorizationData (fibrations C) f
⊢ weakEquivalences C f
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
inst✝ : (weakEquivalences C).ContainsIdentities
X : C
⊢ WeakEquivalence (𝟙 X)

Tactic:
rw [weakEquivalence_iff]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (weakEquivalences C).ContainsIdentities
X : C
⊢ weakEquivalences C (𝟙 X)
Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
A : C
P✝ : Cylinder A
inst✝¹ : IsCofibrant A
P P' : Cylinder A
inst✝ : P'.IsGood
⊢ WeakEquivalence ((P.i₀ ≫ pushout.inl P.i₁ P'.i₀) ≫ pushout.desc P.π P'.π ⋯)

Tactic:
simp only [assoc, colimit.ι_desc, PushoutCocone.mk_ι_app,
        Precylinder.i₀_π]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
A : C
P✝ : Cylinder A
inst✝¹ : IsCofibrant A
P P' : Cylinder A
inst✝ : P'.IsGood
⊢ WeakEquivalence (𝟙 A)
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
⊢ IsStrictlyGE (cylinder K) (n - 1)

Tactic:
rw [CochainComplex.isStrictlyGE_iff]

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 : ℤ), autoParam (i < n - 1) isStrictlyGE_iff._auto_1 → IsZero ((cylinder K).X i)
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
⊢ IsStrictlyGE (pathObject K) (n - 1)

Tactic:
rw [CochainComplex.isStrictlyGE_iff]

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 : ℤ), autoParam (i < n - 1) isStrictlyGE_iff._auto_1 → IsZero ((pathObject K).X i)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
⊢ CochainComplex.plus C T.obj₁.as

Tactic:
by
      rwa [← plus_quotient_obj_iff]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
A : Type u_3
inst✝³ : Category.{v_3, u_3} A
inst✝² : Abelian A
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h✝ : CochainComplex.IsStrictlyGE T.obj₁.as n₁
⊢ CochainComplex.plus C T.obj₂.as

Tactic:
by
      rwa [← plus_quotient_obj_iff]

Goal state after:
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✝ : A.IsVerdierLeftLocalizing B
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hX : B.unop X✝
hY : A.unop Y✝
⊢ ∃ Z a b, A.unop Z ∧ B.unop Z ∧ a ≫ b = f

Tactic:
by
    obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierLeftLocalizing.fac f.op hY hX
    exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩

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
inst✝¹ : IsTriangulated C
X : C
a b : ℤ
inst✝ : t.IsLE X b
⊢ t.IsLE ((t.truncGT a).obj X) b

Tactic:
dsimp [truncGT]; infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
⊢ Qh.IsLocalization (HomotopyCategory.Plus.quasiIso C)

Tactic:
rw [HomotopyCategory.Plus.quasiIso_eq_subcategoryAcyclic_trW]
  infer_instance

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
X : C
n : ℤ
inst✝ : t.IsGE X n
⊢ IsIso ((t.truncGEπ n).app X)

Tactic:
by
  rw [← isGE_iff_isIso_truncGEπ_app]
  infer_instance

Goal state after:
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
p q : ℤ
hpq : p + 2 = q
⊢ (HomComplex.δ 1 2 (HomComplex.Cochain.mk fun p q x ↦ K.d p q ≫ Injective.ι (K.X q))).v p q hpq =
    HomComplex.Cochain.v 0 p q hpq

Tactic:
simp [HomComplex.δ_v 1 2 (by lia) _ p q hpq (p + 1) (p + 1) (by lia) rfl]

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
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsLE T.obj₁ n
h₃ : t.IsLE T.obj₃ n
Y : C
f : T.obj₂ ⟶ Y
hY : t.IsGE Y (n + 1)
f' : T.obj₃ ⟶ Y
hf' : f = T.mor₂ ≫ f'
⊢ f = 0

Tactic:
hf',

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
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsLE T.obj₁ n
h₃ : t.IsLE T.obj₃ n
Y : C
f : T.obj₂ ⟶ Y
hY : t.IsGE Y (n + 1)
f' : T.obj₃ ⟶ Y
hf' : f = T.mor₂ ≫ f'
⊢ T.mor₂ ≫ f' = 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
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsGE T.obj₁ n
h₃ : t.IsGE T.obj₃ n
Y : C
f : Y ⟶ T.obj₂
hY : t.IsLE Y (n - 1)
f' : Y ⟶ T.obj₁
hf' : f = f' ≫ T.mor₁
⊢ f = 0

Tactic:
hf',

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
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsGE T.obj₁ n
h₃ : t.IsGE T.obj₃ n
Y : C
f : Y ⟶ T.obj₂
hY : t.IsLE Y (n - 1)
f' : Y ⟶ T.obj₁
hf' : f = f' ≫ T.mor₁
⊢ f' ≫ T.mor₁ = 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
inst✝ : IsTriangulated C
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
⊢ (t.truncGEπ a).app ((t.truncLT b).obj X) ≫ t.liftTruncLT m₁ (b - 1) b ⋯ ≫ (t.truncLTι b).app ((t.truncGE a).obj X) =
    (t.truncGEπ a).app ((t.truncLT b).obj X) ≫ (t.truncGELTToLTGE a b).app X ≫ (t.truncLTι b).app ((t.truncGE a).obj X)

Tactic:
by simpa using H.comm₁

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : FibrantObject C
f g : X ⟶ Y
h : homRel C f g
⊢ weakEquivalences (FibrantObject C) f ↔ weakEquivalences (FibrantObject C) g

Tactic:
by
    simp only [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]
    obtain ⟨P, ⟨h⟩⟩ := h
    apply h.weakEquivalence_iff

Goal state after: