mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.succ ≤ i
k : Fin (n + 1)
hk : j.rev = k
⊢ ∃ l, ↑i = ↑j + 1 + l

Tactic:
Fin.le_def

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : ↑j.succ ≤ ↑i
k : Fin (n + 1)
hk : j.rev = k
⊢ ∃ l, ↑i = ↑j + 1 + l
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : SimplexCategory
d : SimplexCategoryᵒᵖ
⊢ Finite (unop d ⟶ n)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: X : SSet
n : ℕ
f : Δ[n] ⟶ X
⊢ (Subcomplex.range f).toSSet.Finite

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case zero
n d : ℕ
hd : #∅ ≤ d
hm : #∅ = 0
⊢ ⊥.toSSet.HasDimensionLT d

Tactic:
infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case mp
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ IsIso (toOfSimplex x) → Mono (yonedaEquiv.symm x)

Tactic:
intro

Goal state after:
case mp
X : SSet
n : ℕ
x : X _⦋n⦌
a✝ : IsIso (toOfSimplex x)
⊢ Mono (yonedaEquiv.symm x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case mp
X : SSet
n : ℕ
x : X _⦋n⦌
a✝ : IsIso (toOfSimplex x)
⊢ Mono (toOfSimplex x ≫ (ofSimplex x).ι)

Tactic:
infer_instance

Goal state after:
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₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
p q : ℤ
⊢ (p * q).negOnePow * p.negOnePow = 1 * (p * (q + 1)).negOnePow

Tactic:
rw [one_mul, ← Int.negOnePow_add, mul_add, mul_one]

Goal state after:
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₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ i₂' : I₂
h₂ : c₂.Rel i₂ i₂'
i₁ : I₁
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * (c₂.ε₁ c₁ c₁₂ (i₂, i₁) * c₁.ε₂ c₂ c₁₂ (i₁, i₂)) =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)

Tactic:
mul_comm

Goal state after:
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₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ i₂' : I₂
h₂ : c₂.Rel i₂ i₂'
i₁ : I₁
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * (c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₂.ε₁ c₁ c₁₂ (i₂, i₁)) =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁ i₂' * c₁.ε₂ c₂ c₁₂ (i₁, i₂)
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₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ : I₂
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * (c₂.ε₂ c₁ c₁₂ (i₂, i₁) * c₁.ε₁ c₂ c₁₂ (i₁, i₂)) =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)

Tactic:
mul_comm

Goal state after:
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₁₂
inst✝¹ : TotalComplexShape c₂ c₁ c₁₂
inst✝ : TotalComplexShapeSymmetry c₁ c₂ c₁₂
i₂ : I₂
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
⊢ c₁.σ c₂ c₁₂ i₁ i₂ * (c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₂.ε₂ c₁ c₁₂ (i₂, i₁)) =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) * c₁.σ c₂ c₁₂ i₁' i₂ * c₁.ε₁ c₂ c₁₂ (i₁, i₂)
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case mp
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
⊢ K.flip.HasTotal c → K.HasTotal c

Tactic:
intro

Goal state after:
case mp
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
a✝ : K.flip.HasTotal c
⊢ K.HasTotal c
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case mp
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
a✝ : K.flip.HasTotal c
this : TotalComplexShapeSymmetry c₂ c₁ c
⊢ K.flip.flip.HasTotal c

Tactic:
infer_instance

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

Goal state before:
pp: case mpr
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
⊢ K.HasTotal c → K.flip.HasTotal c

Tactic:
intro

Goal state after:
case mpr
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
a✝ : K.HasTotal c
⊢ K.flip.HasTotal c
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case mpr
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
a✝ : K.HasTotal c
⊢ K.flip.HasTotal c

Tactic:
infer_instance

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝¹³ : Category.{v_1, u_1} C₁
inst✝¹² : Category.{v_2, u_2} C₂
inst✝¹¹ : Category.{v_3, u_3} D
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
inst✝¹⁰ : HasZeroMorphisms C₁
inst✝⁹ : HasZeroMorphisms C₂
inst✝⁸ : Preadditive D
K₁ L₁ : HomologicalComplex C₁ c₁
φ₁ : K₁ ⟶ L₁
K₂ L₂ : HomologicalComplex C₂ c₂
φ₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁷ : F.PreservesZeroMorphisms
inst✝⁶ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
c : ComplexShape J
inst✝⁵ : TotalComplexShape c₁ c₂ c
inst✝⁴ : TotalComplexShape c₂ c₁ c
inst✝³ : TotalComplexShapeSymmetry c₁ c₂ c
inst✝² : DecidableEq J
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
⊢ K₁.HasMapBifunctor K₂ F c

Tactic:
infer_instance

Goal state after:
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:
t.assoc a b c

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 b c)).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.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
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₁' M
inst✝³ : HasShift C₂ M
inst✝² : HasShift D M
F : C₁' ⥤ C₁
inst✝¹ : F.CommShift M
G : C₁ ⥤ C₂ ⥤ D
h : CommShift₂Setup D M
inst✝ : G.CommShift₂ h
X₁' Y₁' : C₁'
f : X₁' ⟶ Y₁'
⊢ NatTrans.CommShift (G.map (F.map f)) M

Tactic:
infer_instance

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

Goal state before:
pp: case fst
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 a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}
⊢ (↑((fun x_1 ↦
            match x_1 with
            | ⟨(a, b), h⟩ => ⟨(a - x, b), ⋯⟩)
          ((fun x_1 ↦
              match x_1 with
              | ⟨(a, b), h⟩ => ⟨(a + x, b), ⋯⟩)
            ⟨(a, b), h⟩))).1 =
    (↑⟨(a, b), h⟩).1

Tactic:
dsimp
          lia

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

Goal state before:
pp: case fst
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 a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}
⊢ (↑((fun x_1 ↦
            match x_1 with
            | ⟨(a, b), h⟩ => ⟨(a + x, b), ⋯⟩)
          ((fun x_1 ↦
              match x_1 with
              | ⟨(a, b), h⟩ => ⟨(a - x, b), ⋯⟩)
            ⟨(a, b), h⟩))).1 =
    (↑⟨(a, b), h⟩).1

Tactic:
dsimp
          lia

Goal state after:
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
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₂' M
inst✝³ : HasShift C₂ M
inst✝² : HasShift D M
F : C₂' ⥤ C₂
inst✝¹ : F.CommShift M
G : C₁ ⥤ C₂ ⥤ D
h : CommShift₂Setup D M
inst✝ : G.CommShift₂ h
X₁ Y₁ : C₁
f : X₁ ⟶ Y₁
⊢ NatTrans.CommShift (F.whiskerLeft (G.map f)) M

Tactic:
infer_instance

Goal state after:
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 ℤ)
⊢ ((shiftFunctor₁ C x).obj ((shiftFunctor₂ C y).obj K)).HasTotal (up ℤ)

Tactic:
infer_instance

Goal state after:
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 ℤ)
⊢ ((shiftFunctor₂ C y).obj ((shiftFunctor₁ C x).obj K)).HasTotal (up ℤ)

Tactic:
infer_instance

Goal state after:
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
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₂ M
inst✝³ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝² : G₁.CommShift₂ h
inst✝¹ : G₂.CommShift₂ h
inst✝ : G₃.CommShift₂ h
x✝ : C₁
⊢ CommShift (𝟙 (G₁.obj x✝)) M

Tactic:
infer_instance

Goal state after:
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
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₂ M
inst✝³ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝² : G₁.CommShift₂ h
inst✝¹ : G₂.CommShift₂ h
inst✝ : G₃.CommShift₂ h
x✝ : C₂
⊢ CommShift (𝟙 (G₁.flip.obj x✝)) M

Tactic:
infer_instance

Goal state after:
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
M : Type u_6
inst✝⁸ : AddCommMonoid M
inst✝⁷ : HasShift C₁ M
inst✝⁶ : HasShift C₂ M
inst✝⁵ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝⁴ : G₁.CommShift₂ h
inst✝³ : G₂.CommShift₂ h
inst✝² : G₃.CommShift₂ h
inst✝¹ : CommShift₂ τ h
inst✝ : CommShift₂ τ' h
x✝ : C₁
⊢ CommShift (τ.app x✝ ≫ τ'.app x✝) M

Tactic:
infer_instance

Goal state after:
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
M : Type u_6
inst✝⁸ : AddCommMonoid M
inst✝⁷ : HasShift C₁ M
inst✝⁶ : HasShift C₂ M
inst✝⁵ : HasShift D M
G₁ G₂ G₃ : C₁ ⥤ C₂ ⥤ D
τ : G₁ ⟶ G₂
τ' : G₂ ⟶ G₃
h : CommShift₂Setup D M
inst✝⁴ : G₁.CommShift₂ h
inst✝³ : G₂.CommShift₂ h
inst✝² : G₃.CommShift₂ h
inst✝¹ : CommShift₂ τ h
inst✝ : CommShift₂ τ' h
x✝ : C₂
⊢ CommShift (((flipFunctor C₁ C₂ D).map τ).app x✝ ≫ ((flipFunctor C₁ C₂ D).map τ').app x✝) M

Tactic:
infer_instance

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

Goal state before:
pp: case pos.e_a
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
  (Homotopy.ofEq ⋯).trans
    ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
          (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
      (Homotopy.ofEq ⋯))
j j' : J
i₁ : I₁
i₂ : I₂
hj : c₁.π c₂ c (i₁, i₂) = j
hj' : c₁.π c₂ c (i₁, c₂.prev i₂) = j'
hi₂ : c₂.Rel (c₂.prev i₂) i₂
⊢ c₁.ε₂ c₂ c (i₁, c₂.prev i₂) = c₁.σ c₂ c i₁ i₂ * c₂.ε₁ c₁ c (c₂.prev i₂, i₁) * c₁.σ c₂ c i₁ (c₂.prev i₂)

Tactic:
mul_comm

Goal state after:
case pos.e_a
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
  (Homotopy.ofEq ⋯).trans
    ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
          (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
      (Homotopy.ofEq ⋯))
j j' : J
i₁ : I₁
i₂ : I₂
hj : c₁.π c₂ c (i₁, i₂) = j
hj' : c₁.π c₂ c (i₁, c₂.prev i₂) = j'
hi₂ : c₂.Rel (c₂.prev i₂) i₂
⊢ c₁.ε₂ c₂ c (i₁, c₂.prev i₂) = c₂.ε₁ c₁ c (c₂.prev i₂, i₁) * c₁.σ c₂ c i₁ i₂ * c₁.σ c₂ c i₁ (c₂.prev i₂)
Module: Mathlib.Algebra.Homology.CochainComplexPlus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteLimits C
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
⊢ HasLimitsOfShape J (Plus C)

Tactic:
infer_instance

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
inst✝ : HasFiniteColimits C
J : Type
x✝¹ : SmallCategory J
x✝ : FinCategory J
⊢ HasColimitsOfShape J (Plus C)

Tactic:
infer_instance

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
inst✝ : CategoryWithHomology C
⊢ ((HomologicalComplex.quasiIso C (ComplexShape.up ℤ)).inverseImage (ι C)).HasTwoOutOfThreeProperty

Tactic:
infer_instance

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
inst✝ : CategoryWithHomology C
⊢ ((HomologicalComplex.quasiIso C (ComplexShape.up ℤ)).inverseImage (ι C)).IsStableUnderRetracts

Tactic:
infer_instance

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

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
F : C ⥤ D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
inst✝ : F.PreservesZeroMorphisms
K : CochainComplex.Plus C
i : ℤ
hi : K.obj.IsStrictlyGE i
⊢ ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj K.obj).IsStrictlyGE i

Tactic:
infer_instance

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

Goal state before:
pp: case mp
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
⊢ t.IsLE ((shiftFunctor C a).obj X) n' → t.IsLE X n

Tactic:
intro

Goal state after:
case mp
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
a✝ : t.IsLE ((shiftFunctor C a).obj X) n'
⊢ t.IsLE X n
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case mpr
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
⊢ t.IsLE X n → t.IsLE ((shiftFunctor C a).obj X) n'

Tactic:
intro

Goal state after:
case mpr
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
a✝ : t.IsLE X n
⊢ t.IsLE ((shiftFunctor C a).obj X) n'
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case mp
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
⊢ t.IsGE ((shiftFunctor C a).obj X) n' → t.IsGE X n

Tactic:
intro

Goal state after:
case mp
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
a✝ : t.IsGE ((shiftFunctor C a).obj X) n'
⊢ t.IsGE X n
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

Goal state before:
pp: case mpr
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
⊢ t.IsGE X n → t.IsGE ((shiftFunctor C a).obj X) n'

Tactic:
intro

Goal state after:
case mpr
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
a✝ : t.IsGE X n
⊢ t.IsGE ((shiftFunctor C a).obj X) n'
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 : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ IsIso ((HomotopyCategory.quotient C c').map (extendMap f e)) ↔
    IsIso ((HomotopyCategory.quotient C c ⋙ e.extendHomotopyFunctor C).map f)

Tactic:
NatIso.isIso_map_iff (e.extendHomotopyFunctorFactors C) f

Goal state after:
ι : 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 : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
⊢ IsIso ((HomotopyCategory.quotient C c').map (extendMap f e)) ↔
    IsIso ((e.extendFunctor C ⋙ HomotopyCategory.quotient C c').map f)
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
⊢ (t.plus ⊓ t.minus).IsClosedUnderIsomorphisms

Tactic:
infer_instance

Goal state after:
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
⊢ (t.plus ⊓ t.minus).IsStableUnderShift ℤ

Tactic:
infer_instance

Goal state after: