mathlib-initiative/mathlib-tactics huggingface dataset:
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 = ComplexShape.embeddingUpIntDownInt.f (-p)

Tactic:
simp

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 : ℤ
⊢ ComplexShape.embeddingUpIntDownInt.f (-q) = q

Tactic:
simp

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)
n p q : ℤ
⊢ h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p q ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op

Tactic:
simp

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)
n : ℤ
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 = - -n

Tactic:
simp

Goal state after:
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 : J → ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE (n j)
j : J
⊢ n j ∈ Finset.image n ⊤ ∪ {0}

Tactic:
simp

Goal state after:
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 : J → ℤ
hn : ∀ (j : J), (p.diag.obj j).IsStrictlyGE (n j)
j : J
⊢ n j ∈ Finset.image n ⊤ ∪ {0}

Tactic:
simp

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)
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
⊢ (ComplexShape.up ℤ).Rel (-(n + 1)) (-n)

Tactic:
simp

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)
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
⊢ - -(n + 1) = n + 1

Tactic:
simp

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)
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
⊢ - -n = n

Tactic:
simp

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_5
C₄ : Type u_6
inst✝²⁰ : Category.{v_1, u_1} C₁
inst✝¹⁹ : Category.{v_2, u_2} C₂
inst✝¹⁸ : Category.{v_3, u_5} C₃
inst✝¹⁷ : Category.{v_4, u_6} C₄
inst✝¹⁶ : Category.{v_5, u_3} C₁₂
inst✝¹⁵ : HasZeroMorphisms C₁
inst✝¹⁴ : HasZeroMorphisms C₂
inst✝¹³ : HasZeroMorphisms C₃
inst✝¹² : Preadditive C₁₂
inst✝¹¹ : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
inst✝¹⁰ : F₁₂.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝⁸ : G.Additive
inst✝⁷ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : Type u_12
inst✝⁶ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₄ : ComplexShape ι₄
inst✝⁵ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁴ : TotalComplexShape c₁₂ c₃ c₄
inst✝³ : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝² : DecidableEq ι₁₂
inst✝¹ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
j j' : ι₄
inst✝ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₁₂ : ι₁₂ := ⋯
h₁ : c₁₂.Rel i₁₂ (c₁₂.next i₁₂)
h₂ : ¬c₁₂.π c₃ c₄ (c₁₂.next i₁₂, i₃) = j'
⊢ 0 = 0 + 0

Tactic:
simp

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
⊢ (fun h ↦ homotopyUnop h) ((fun h ↦ homotopyOp h) h) = h

Tactic:
by
    ext p q
    simp [homotopyUnop_hom_eq _ p q (-p) (-q),
      homotopyOp_hom_eq _ (-q) (-p) q p]

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 : CochainComplex C ℤ
m : ℤ
hK : HomologicalComplex.ExactAt K (-m)
hm : -m + m = 0
⊢ (ComplexShape.up ℤ).prev m = m - 1

Tactic:
simp

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 : CochainComplex C ℤ
m : ℤ
hK : HomologicalComplex.ExactAt K (-m)
hm : -m + m = 0
⊢ (ComplexShape.up ℤ).next m = m + 1

Tactic:
simp

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

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
d : ℤ
X : ℕ → Set (Cochain K L d)
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1))
p₀ : ℤ
hφ : ∀ (n : ℕ) (x : ↑(X n)), (↑(φ n x)).EqUpTo (↑x) (p₀ + ↑n)
x₀ : ↑(X 0)
n₁ : ℕ
p✝ q✝ : ℤ
hpq✝ : p✝ + d = q✝
a✝ : p✝ ≤ p₀ + ↑n₁
⊢ (↑(sequence φ x₀ n₁)).v p✝ q✝ hpq✝ = (↑(sequence φ x₀ (n₁ + 0))).v p✝ q✝ hpq✝

Tactic:
simp

Goal state after:
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 : ℤ
⊢ n - 1 + 1 = n

Tactic:
simp

Goal state after:
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 : ℤ
⊢ δ (n - 1) n 0 = ↑0

Tactic:
simp

Goal state after:
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 : ℤ
⊢ mk 0 = 0

Tactic:
simp

Goal state after:
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 : ℤ
⊢ ∀ (x y : Cocycle K L n), mk (x + y) = mk x + mk y

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x : Cocycle K L n
h✝ : Nonempty (Homotopy (Cocycle.equivHomShift.symm x) 0)
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
h : (↑x).rightShift n 0 ⋯ = δ (-1) 0 γ
⊢ n - 1 + 1 = n

Tactic:
simp

Goal state after:
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 : ℤ
⊢ (ComplexShape.up ℤ).prev n + 1 = n

Tactic:
simp

Goal state after:
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 : ℤ
⊢ n + 1 = (ComplexShape.up ℤ).next n

Tactic:
simp

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

Goal state before:
pp: 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.trW.isLocal Y
X : C
f : X ⟶ Y
hX : P X
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₁ ≫ f = (Triangle.mk 0 (𝟙 X) 0).mor₁ ≫ 0

Tactic:
simp

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

Goal state before:
pp: 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
X : C
hX : P.trW.isColocal X
Y : C
f : X ⟶ Y
hY : P Y
⊢ f ≫ (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj Y))).mor₁ = 0 ≫ (Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj Y))).mor₁

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
L₁ L₂ : CochainComplex C ℤ
e : HomotopyEquiv L₁ L₂
inst✝ : L₁.IsKInjective
K : CochainComplex C ℤ
f : K ⟶ L₂
hK : HomologicalComplex.Acyclic K
⊢ f = f ≫ 𝟙 L₂

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
L₁ L₂ : CochainComplex C ℤ
e : HomotopyEquiv L₁ L₂
inst✝ : L₁.IsKInjective
K : CochainComplex C ℤ
f : K ⟶ L₂
hK : HomologicalComplex.Acyclic K
⊢ f ≫ e.inv ≫ e.hom = (f ≫ e.inv) ≫ e.hom

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
L₁ L₂ : CochainComplex C ℤ
e : HomotopyEquiv L₁ L₂
inst✝ : L₁.IsKInjective
K : CochainComplex C ℤ
f : K ⟶ L₂
hK : HomologicalComplex.Acyclic K
⊢ 0 ≫ e.hom = 0

Tactic:
simp

Goal state after:
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) ⋯
hu : K.d n (n + 1) ≫ u = 0
⊢ (ComplexShape.up ℤ).prev (n + 1) = n

Tactic:
simp

Goal state after:
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) ⋯
hu : K.d n (n + 1) ≫ u = 0
⊢ (ComplexShape.up ℤ).next (n + 1) = n + 2

Tactic:
simp

Goal state after:
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) ⋯
hu : K.d n (n + 1) ≫ u = 0
⊢ n + 1 + 1 = n + 2
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: case inl
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.sc' K n (n + 1) (n + 2)).Exact
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) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p : ℤ
hp✝ : p ≤ n + 1
hpq : p + 0 = p
hp : p < n + 1
⊢ (δ (-1) 0 (Cochain.single β (-1))).v p p hpq = 0

Tactic:
δ_v (-1) 0 (neg_add_cancel 1) _ p p hpq (p - 1) (p + 1) rfl rfl,

Goal state after:
case inl
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.sc' K n (n + 1) (n + 2)).Exact
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) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p : ℤ
hp✝ : p ≤ n + 1
hpq : p + 0 = p
hp : p < n + 1
⊢ (Cochain.single β (-1)).v p (p - 1) ⋯ ≫ L.d (p - 1) p +
      Int.negOnePow 0 • K.d p (p + 1) ≫ (Cochain.single β (-1)).v (p + 1) p ⋯ =
    0
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 (n + ↑1) X
⊢ n + 1 = n + ↑1

Tactic:
simp

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

Goal state before:
pp: case inl
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.sc' K n (n + 1) (n + 2)).Exact
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) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p : ℤ
hp✝ : p ≤ n + 1
hpq : p + 0 = p
hp : p < n + 1
⊢ 0 ≫ L.d (p - 1) p + Int.negOnePow 0 • K.d p (p + 1) ≫ 0 = 0

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
x✝ : Homotopy f g
⊢ (fun h ↦ h.ofExtend) ((fun h ↦ h.extend e) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
x✝ : Homotopy (extendMap f e) (extendMap g e)
⊢ (fun h ↦ h.extend e) ((fun h ↦ h.ofExtend) x✝) = x✝

Tactic:
simp

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 Y : DerivedCategory C
f : X ⟶ Y
K : CochainComplex C ℤ
e₁ : X ≅ Q.obj K
h✝¹ : K.IsStrictlyLE 0
L : CochainComplex C ℤ
e₂ : Y ≅ Q.obj L
h✝ : L.IsStrictlyGE 1
⊢ 0 < 1

Tactic:
simp

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
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ (triangleOfSES h).mor₃ ≫ (shiftFunctor (DerivedCategory C) 1).map (Iso.refl (triangleOfSES h).obj₁).hom =
    (asIso (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13))).hom ≫
      (Triangle.mk (Q.map (K.ιTruncLE 0) ≫ e₂.hom) (e₂.inv ≫ Q.map (K.πTruncGE 1))
          (inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13)) ≫
            (triangleOfSES h).mor₃)).mor₃

Tactic:
simp

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : α), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasPathObject
hc : ∀ (i : α), ∃ j, c.Rel i j
⊢ ι K ≫ π₀ K = 𝟙 K

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
⊢ s ≫ u ≫ g' = s ≫ g ≫ v

Tactic:
sq.w

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
⊢ s ≫ g ≫ v = s ≫ g ≫ v
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ u ≫ g' = g ≫ v

Tactic:
sq.w

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPushout s f g t
Z' W' : C
g' : Z' ⟶ W'
inst✝ : HasLiftingProperty f g'
u : Z ⟶ Z'
v : W ⟶ W'
sq : CommSq u g g' v
w : (s ≫ u) ≫ g' = f ≫ t ≫ v
⊢ g ≫ v = g ≫ v
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
⊢ (u ≫ f) ≫ t = (f' ≫ v) ≫ t

Tactic:
sq.w

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
⊢ (f' ≫ v) ≫ t = (f' ≫ v) ≫ t
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ f' ≫ h.lift ⋯.lift v ⋯ ≫ f = u ≫ f

Tactic:
h.lift_snd,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ f' ≫ v = u ≫ f
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ f' ≫ v = u ≫ f

Tactic:
sq.w

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X Y Z W : C
f : X ⟶ Y
s : X ⟶ Z
g : Z ⟶ W
t : Y ⟶ W
h : IsPullback s f g t
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasLiftingProperty f' g
u : X' ⟶ X
v : Y' ⟶ Y
sq : CommSq u f' f v
w : (u ≫ s) ≫ g = f' ≫ v ≫ t
⊢ f' ≫ v = f' ≫ v
Module: Mathlib.CategoryTheory.LiftingProperties.Limits

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
X✝ Y✝ Z W : C
f✝ : X✝ ⟶ Y✝
s : X✝ ⟶ Z
g : Z ⟶ W
t✝ : Y✝ ⟶ W
J : Type u_2
A B : J → C
inst✝² : HasProduct A
inst✝¹ : HasProduct B
f : (j : J) → A j ⟶ B j
X Y : C
p : X ⟶ Y
inst✝ : ∀ (j : J), HasLiftingProperty p (f j)
t : X ⟶ ∏ᶜ A
b : Y ⟶ ∏ᶜ B
sq : CommSq t p (Limits.Pi.map f) b
j : J
⊢ (t ≫ Pi.π A j) ≫ f j = (t ≫ Limits.Pi.map f) ≫ Pi.π B j

Tactic:
simp

Goal state after:
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 ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : Cochain.ofHom φ = (↑z).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ 0 + n = n

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasCoproduct A
inst✝ : Limits.HasCoproduct B
f : (j : J) → A j ⟶ B j
⊢ (∀ (j : J), T.llp (f j)) → T.llp (Limits.Sigma.map f)

Tactic:
hf

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasCoproduct A
inst✝ : Limits.HasCoproduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
⊢ T.llp (Limits.Sigma.map f)
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasProduct A
inst✝ : Limits.HasProduct B
f : (j : J) → A j ⟶ B j
⊢ (∀ (j : J), T.rlp (f j)) → T.rlp (Limits.Pi.map f)

Tactic:
hf

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasProduct A
inst✝ : Limits.HasProduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
⊢ T.rlp (Limits.Pi.map f)
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 ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
⊢ -1 + 1 = 0

Tactic:
simp

Goal state after:
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 ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hL : HomologicalComplex.Acyclic L
m : ℤ
hm : m + 1 = n
β : Cochain L L (-1)
hβ : δ (-1) 0 β = ↑(Cocycle.ofHom (𝟙 L))
⊢ -1 + 1 = 0

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : CategoryWithWeakEquivalences C
inst✝¹ : (weakEquivalences C).HasTwoOutOfThreeProperty
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : WeakEquivalence g
hfg : WeakEquivalence (f ≫ g)
⊢ WeakEquivalence f

Tactic:
exact weakEquivalence_of_postcomp f g

Goal state after: