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

Goal state before:
pp: n : ℕ
i j : Fin (n + 3)
h : i < j
⊢ Subcomplex.homOfLE ⋯ ≫ (faceSingletonComplIso i).inv = (facePairComplIso i j h).inv ≫ stdSimplex.δ (j.pred ⋯)

Tactic:
by
  simp [← cancel_mono (faceSingletonComplIso i).hom,
    ← cancel_mono (Subcomplex.ι _), ← cancel_epi (facePairComplIso i j h).hom,
    facePairComplIso_hom_ι']

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel 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:
neg_inj,

Goal state after:
I₁ : Type u_1
I₂ : Type u_2
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₁₂ : ComplexShape I₁₂
inst✝ : TotalComplexShape c₁ c₂ c₁₂
i₁ i₁' : I₁
i₂ i₂' : I₂
h₁ : c₁.Rel 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.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₁₂ =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h'

Tactic:
by
  rw [d₁_eq' K c₁₂ h i₂ i₁₂, K.toGradedObject.ιMapObjOrZero_eq]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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_3} C₃
inst✝³ : Category.{v_4, u_4} C₄
inst✝² : Category.{v_5, u_5} C₁₂
inst✝¹ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
inst✝ :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ Y₂ Z₂ : GradedObject I₂ C₂
φ : X₂ ⟶ Y₂
ψ : Y₂ ⟶ Z₂
⊢ { app := fun X₃ ↦ mapTrifunctorMapMap F p (𝟙 X₁) (φ ≫ ψ) (𝟙 X₃), naturality := ⋯ } =
    { app := fun X₃ ↦ mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃), naturality := ⋯ } ≫
      { app := fun X₃ ↦ mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃), naturality := ⋯ }

Tactic:
by
    ext X₃ j i₁ i₂ i₃
    simp only [ι_mapTrifunctorMapMap, categoryOfGradedObjects_id, Functor.map_id,
      NatTrans.id_app, categoryOfGradedObjects_comp, Functor.map_comp, NatTrans.comp_app,
      id_comp, assoc, ι_mapTrifunctorMapMap_assoc]

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

Goal state before:
pp: 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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, i₂) = i₁₂'

Tactic:
← ComplexShape.next_π₁ c₂ c₁₂ h₃ 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₁₂'' : I₁₂
h₁ : c₁₂.Rel 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₁)
⊢ c₁₂.next (c₁.π c₂ c₁₂ (i₁, i₂)) = i₁₂'
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: 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₁₂'' : I₁₂
h₁ : c₁₂.Rel i₁₂ i₁₂'
h₂ : c₁₂.Rel i₁₂' i₁₂''
⊢ K.D₂ c₁₂ i₁₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
ext ⟨i₁, i₂⟩ h
      simp only [totalAux.ιMapObj_D₂_assoc, comp_zero]
      by_cases h₃ : c₂.Rel i₂ (c₂.next i₂)
      · rw [totalAux.d₂_eq K c₁₂ i₁ h₃ i₁₂']; swap
        · rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃, ← c₁₂.next_eq' h₁, h]
        simp only [Linear.units_smul_comp, assoc, totalAux.ιMapObj_D₂]
        by_cases h₄ : c₂.Rel (c₂.next i₂) (c₂.next (c₂.next i₂))
        · rw [totalAux.d₂_eq K c₁₂ i₁ h₄ i₁₂'', Linear.comp_units_smul,
            HomologicalComplex.d_comp_d_assoc, zero_comp, smul_zero, smul_zero]
          rw [← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₄, ← ComplexShape.next_π₂ c₁ c₁₂ i₁ h₃,
            h, c₁₂.next_eq' h₁, c₁₂.next_eq' h₂]
        · rw [K.d₂_eq_zero c₁₂ _ _ _ h₄, comp_zero, smul_zero]
      · rw [K.d₂_eq_zero c₁₂ _ _ _ h₃, zero_comp]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Trifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₂₃ : Type u_6
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_6, u_6} C₂₃
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₂₃ : BifunctorComp₂₃IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝² : (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p
inst✝¹ : (((mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap ρ₂₃.q
H : HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃
inst✝ : ((((mapTrifunctor (bifunctorComp₂₃ F G₂₃) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap r
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : r (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      (mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃).hom j =
    ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h

Tactic:
dsimp [mapBifunctorComp₂₃MapObjIso]
  apply CofanMapObjFun.ιMapObj_iso_inv

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

Goal state before:
pp: 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₂ : K₂ ⟶ L₂
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
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ -((c₁.ε₂ c₂ c (i₁', i₂) * c₁.ε₁ c₂ c (i₁, i₂')) •
        (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
          (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
            (F.obj (L₁.X i₁)).map (L₂.d i₂ i₂') ≫
              (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj') =
    -((c₁.ε₂ c₂ c (i₁', i₂) * c₁.ε₁ c₂ c (i₁, i₂')) •
        (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
          (F.obj (L₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂') ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂' j hj')

Tactic:
neg_inj,

Goal state after:
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₂ : K₂ ⟶ L₂
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
i₁ i₁' : I₁
hi₁ : c₁.Rel i₁ i₁'
i₂ i₂' : I₂
hi₂ : c₂.Rel i₂ i₂'
j : J
hj : c₁.π c₂ c (i₁', i₂) = j
hj' : c₁.π c₂ c (i₁, i₂') = j
⊢ (c₁.ε₂ c₂ c (i₁', i₂) * c₁.ε₁ c₂ c (i₁, i₂')) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫
          (F.obj (L₁.X i₁)).map (L₂.d i₂ i₂') ≫
            (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj' =
    (c₁.ε₂ c₂ c (i₁', i₂) * c₁.ε₁ c₂ c (i₁, i₂')) •
      (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (K₂.d i₂ i₂') ≫ (F.obj (L₁.X i₁)).map (f₂.f i₂') ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂' j hj'
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: 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₂ : K₂ ⟶ L₂
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
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
h₃ : c₁.Rel (c₁.prev i₁) i₁
⊢ c₁.π c₂ c (c₁.prev i₁, i₂) = c.prev j

Tactic:
by rw [← ComplexShape.prev_π₁ c₂ c h₃, h]

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
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (((shiftFunctor₂ C y).map f).f i₁).f i₂ ≫
      ((i₁ * y).negOnePow •
        (L.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) ⋯).hom ≫
          L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫
            (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) y n (n + y) ⋯).inv) =
    ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) i₁ i₂ n h ≫ (K.totalShift₂Iso y).hom.f n ≫ (total.map f (up ℤ)).f (n + y)

Tactic:
K.ι_totalShift₂Iso_hom_f_assoc y i₁ i₂ n h _ rfl _ rfl

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
y : ℤ
inst✝¹ : K.HasTotal (up ℤ)
inst✝ : L.HasTotal (up ℤ)
n i₁ i₂ : ℤ
h : i₁ + i₂ = n
⊢ (((shiftFunctor₂ C y).map f).f i₁).f i₂ ≫
      ((i₁ * y).negOnePow •
        (L.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) ⋯).hom ≫
          L.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫
            (CochainComplex.shiftFunctorObjXIso (L.total (up ℤ)) y n (n + y) ⋯).inv) =
    ((i₁ * y).negOnePow •
        (K.shiftFunctor₂XXIso i₁ i₂ y (i₂ + y) ⋯).hom ≫
          K.ιTotal (up ℤ) i₁ (i₂ + y) (n + y) ⋯ ≫
            (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) y n (n + y) ⋯).inv) ≫
      (total.map f (up ℤ)).f (n + y)
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),
    p✝ ≤ p₀ + ↑n₁ → (↑(sequence φ x₀ n₁)).v p✝ q hpq = (↑(sequence φ x₀ (n₁ + 0))).v p✝ q hpq

Tactic:
_

Goal state after:
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✝), p✝ ≤ p₀ + ↑n₁ → (↑(sequence φ x₀ n₁)).v p✝ q✝ hpq = (↑(sequence φ x₀ (n₁ + 0))).v p✝ q✝ hpq
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✝), p✝ ≤ p₀ + ↑n₁ → (↑(sequence φ x₀ n₁)).v p✝ q✝ hpq = (↑(sequence φ x₀ (n₁ + 0))).v p✝ q✝ hpq

Tactic:
_

Goal state after:
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✝
⊢ p✝ ≤ p₀ + ↑n₁ → (↑(sequence φ x₀ n₁)).v p✝ q✝ hpq✝ = (↑(sequence φ x₀ (n₁ + 0))).v p✝ q✝ hpq✝
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✝
⊢ p✝ ≤ p₀ + ↑n₁ → (↑(sequence φ x₀ n₁)).v p✝ q✝ hpq✝ = (↑(sequence φ x₀ (n₁ + 0))).v p✝ q✝ hpq✝

Tactic:
_

Goal state after:
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✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: case refine_1
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)
⊢ ∃ m, m + 1 = n ∧ ∃ β, δ m n β = ↑x

Tactic:
obtain ⟨γ, h⟩ := Cochain.equivHomotopy _ _ h.some

Goal state after:
case refine_1
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 : Cochain.ofHom (Cocycle.equivHomShift.symm x) = δ (-1) 0 γ + Cochain.ofHom 0
⊢ ∃ m, m + 1 = n ∧ ∃ β, δ m n β = ↑x
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : P.IsTriangulated
inst✝¹ : IsTriangulated C
Y : C
hY : P.rightOrthogonal Y
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
X : C
⊢ Function.Bijective L.map

Tactic:
← isLocal_trW

Goal state after:
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : P.IsTriangulated
inst✝¹ : IsTriangulated C
Y : C
hY : P.trW.isLocal Y
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
X : C
⊢ Function.Bijective L.map
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
x✝ : L.IsKInjective
K : HomotopyCategory C (ComplexShape.up ℤ)
f : K ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L
hK : HomotopyCategory.subcategoryAcyclic C K
⊢ f = 0

Tactic:
obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective K

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
x✝ : L.IsKInjective
K : HomologicalComplex C (ComplexShape.up ℤ)
f : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L
hK : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
⊢ f = 0
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
⊢ (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

Tactic:
Cochain.single_v_eq_zero _ _ _ _ _ (by lia),

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
⊢ 0 ≫ L.d (p - 1) p + Int.negOnePow 0 • K.d p (p + 1) ≫ (Cochain.single β (-1)).v (p + 1) p ⋯ = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝³ : e.IsRelIff
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomotopyCategory C c
φ : (e.extendHomotopyFunctor C).obj K ⟶ (e.extendHomotopyFunctor C).obj L
⊢ ∃ a, (e.extendHomotopyFunctor C).map a = φ

Tactic:
obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective K

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝³ : e.IsRelIff
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
L : HomotopyCategory C c
K : HomologicalComplex C c
φ : (e.extendHomotopyFunctor C).obj ((HomotopyCategory.quotient C c).obj K) ⟶ (e.extendHomotopyFunctor C).obj L
⊢ ∃ a, (e.extendHomotopyFunctor C).map a = φ
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝³ : e.IsRelIff
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomotopyCategory C c
φ₁ φ₂ : K ⟶ L
hφ : (e.extendHomotopyFunctor C).map φ₁ = (e.extendHomotopyFunctor C).map φ₂
⊢ φ₁ = φ₂

Tactic:
obtain ⟨K, rfl⟩ := HomotopyCategory.quotient_obj_surjective K

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝³ : e.IsRelIff
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
L : HomotopyCategory C c
K : HomologicalComplex C c
φ₁ φ₂ : (HomotopyCategory.quotient C c).obj K ⟶ L
hφ : (e.extendHomotopyFunctor C).map φ₁ = (e.extendHomotopyFunctor C).map φ₂
⊢ φ₁ = φ₂
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 : ℤ
⊢ X.IsGE n → ∀ i < n, IsZero ((homologyFunctor C i).obj X)

Tactic:
rintro ⟨K, e, _⟩ i hi

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.IsStrictlyGE n
i : ℤ
hi : i < n
⊢ IsZero ((homologyFunctor C i).obj X)
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 : ℤ
⊢ X.IsLE n → ∀ (i : ℤ), n < i → IsZero ((homologyFunctor C i).obj X)

Tactic:
rintro ⟨K, e, _⟩ i hi

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
⊢ IsZero ((homologyFunctor C i).obj X)
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_1 : Limits.HasCoproduct B] (f : (j : J) → A j ⟶ B j),
    (∀ (j : J), T.llp (f j)) → T.llp (Limits.Sigma.map f)

Tactic:
_

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), (∀ (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.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:
_

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), (∀ (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.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)

Tactic:
X

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)
X : C
⊢ ∀ ⦃Y : C⦄ (g : X ⟶ Y), T g → HasLiftingProperty (Limits.Sigma.map f) g
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_1 : Limits.HasProduct B] (f : (j : J) → A j ⟶ B j),
    (∀ (j : J), T.rlp (f j)) → T.rlp (Limits.Pi.map f)

Tactic:
_

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), (∀ (j : J), T.rlp (f j)) → T.rlp (Limits.Pi.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:
_

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), (∀ (j : J), T.rlp (f j)) → T.rlp (Limits.Pi.map f)