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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i : ℕ
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f i =
    (𝟙 C).f i

Tactic:
cases i

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f 0 =
    (𝟙 C).f 0

case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
n✝ : ℕ
⊢ ({ f := fun x ↦ 𝟙 (C.X x), comm' := ⋯ } ≫ { f := fun x ↦ 𝟙 ((truncate.obj (C.augment f w)).X x), comm' := ⋯ }).f
      (n✝ + 1) =
    (𝟙 C).f (n✝ + 1)
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i 0 →
    (match i with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d i 0 =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d i 0 ≫
        match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

Tactic:
cases i

Goal state after:
case zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ (ComplexShape.up ℕ).Rel 0 0 →
    (match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d 0 0 =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d 0 0 ≫
        match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

case zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ (ComplexShape.up ℕ).Rel (n✝ + 1) 0 →
    (match n✝ + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d (n✝ + 1) 0 =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d (n✝ + 1) 0 ≫
        match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ (ComplexShape.up ℕ).Rel i (0 + 1) →
    (match i with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d i (0 + 1) =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d i (0 + 1) ≫
        match 0 + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

Tactic:
cases i

Goal state after:
case succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ (ComplexShape.up ℕ).Rel 0 (0 + 1) →
    (match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d 0 (0 + 1) =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d 0 (0 + 1) ≫
        match 0 + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

case succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ (ComplexShape.up ℕ).Rel (n✝ + 1) (0 + 1) →
    (match n✝ + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d (n✝ + 1) (0 + 1) =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d (n✝ + 1) (0 + 1) ≫
        match 0 + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i j : ℕ
⊢ (ComplexShape.up ℕ).Rel i (j + 1 + 1) →
    (match i with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d i (j + 1 + 1) =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d i (j + 1 + 1) ≫
        match j + 1 + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

Tactic:
cases i

Goal state after:
case succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
j : ℕ
⊢ (ComplexShape.up ℕ).Rel 0 (j + 1 + 1) →
    (match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d 0 (j + 1 + 1) =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d 0 (j + 1 + 1) ≫
        match j + 1 + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

case succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
j n✝ : ℕ
⊢ (ComplexShape.up ℕ).Rel (n✝ + 1) (j + 1 + 1) →
    (match n✝ + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d (n✝ + 1) (j + 1 + 1) =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d (n✝ + 1) (j + 1 + 1) ≫
        match j + 1 + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))
Module: Mathlib.Algebra.Homology.TotalComplex

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

Tactic:
totalAux.d₁_eq' K c₁₂ h i₂ i₁₂,

Goal state after:
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₁₂
⊢ c₁.ε₁ c₂ c₁₂ (i₁, i₂) • (K.d i₁ i₁').f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ = 0
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
inst✝ :
  ∀ (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃),
    ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₁ Y₁ : GradedObject I₁ C₁
φ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
ψ : X₂ ⟶ Y₂
X₃ : GradedObject I₃ C₃
j : J
i₁ : I₁
i₂ : I₂
i₃ : I₃
h : p (i₁, i₂, i₃) = j
⊢ ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      mapTrifunctorMapMap F p (𝟙 X₁) ψ (𝟙 X₃) j ≫ mapTrifunctorMapMap F p φ (𝟙 Y₂) (𝟙 X₃) j =
    ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
      mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃) j ≫ mapTrifunctorMapMap F p (𝟙 Y₁) ψ (𝟙 X₃) j

Tactic:
simp only [ι_mapTrifunctorMapMap_assoc, categoryOfGradedObjects_id, Functor.map_id,
          NatTrans.id_app, ι_mapTrifunctorMapMap, id_comp,
          NatTrans.naturality_app_assoc]

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

Goal state before:
pp: case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' i₁₂'' : 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₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂' ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
rw [K.d₂_eq_zero c₁₂ _ _ _ h₃, zero_comp]

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
⊢ (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
      (F.obj (L₁.X i₁)).map (f₂.f i₂ ≫ L₂.d i₂ i₂') ≫
        (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj' =
    (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
      (F.obj (L₁.X i₁)).map (K₂.d i₂ i₂' ≫ f₂.f i₂') ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂' j hj'

Tactic:
f₂.comm

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
⊢ (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
      (F.obj (L₁.X i₁)).map (K₂.d i₂ i₂' ≫ f₂.f i₂') ≫
        (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).ιTotal c i₁ i₂' j hj' =
    (F.map (h₁.hom i₁' i₁)).app (K₂.X i₂) ≫
      (F.obj (L₁.X i₁)).map (K₂.d i₂ i₂' ≫ f₂.f i₂') ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂' j hj'
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case neg
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 i₁ (c₁.next i₁)
⊢ (F.map (K₁.d i₁ (c₁.next i₁))).app (K₂.X i₂) ≫
      (F.map (h₁.hom (c₁.next i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    (((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₁ c i₁ i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j

Tactic:
rw [K₁.shape _ _ h₃, Functor.map_zero, zero_app, zero_comp,
        HomologicalComplex₂.d₁_eq_zero _ _ _ _ _ h₃, zero_comp]

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 ℤ)
n n' : ℤ
h : n + y = n'
⊢ ((((shiftFunctor₂ C y).obj K).totalDesc fun p q hpq ↦ (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n' ⋯) ≫
      K.totalDesc fun p q hpq ↦
        (p * y).negOnePow •
          (XXIsoOfEq C (up ℤ) (up ℤ) K ⋯ ⋯).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p (q - y) n ⋯) =
    𝟙 ((((shiftFunctor₂ C y).obj K).total (up ℤ)).X n)

Tactic:
by
    ext p q h
    dsimp
    simp only [ι_totalDesc_assoc, Linear.units_smul_comp, ι_totalDesc, smul_smul,
      Int.units_mul_self, one_smul, comp_id]
    exact ((shiftFunctor₂ C y).obj K).XXIsoOfEq_inv_ιTotal _ rfl (by lia) _ _

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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomologicalComplex C c
φ : (i j : ι) → K.X i ⟶ L.X j
i' j' : Option ι
i j : ι
hi : i' = some i
hj : j' = some j
⊢ homAux φ i' j' = (extend.XIso K hi).hom ≫ φ i j ≫ (extend.XIso L hj).inv

Tactic:
subst hi hj
  simp [homAux, extend.XIso, extend.X]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
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_5} C₃
inst✝¹⁹ : Category.{v_4, u_6} C₄
inst✝¹⁸ : Category.{v_6, u_4} 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✝¹² : G₂₃.PreservesZeroMorphisms
inst✝¹¹ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁰ : F.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : 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 ι₂₃
c₄ : ComplexShape ι₄
inst✝⁷ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁶ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁵ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁴ : TotalComplexShape c₁ c₂₃ c₄
inst✝³ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝² : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝¹ : DecidableEq ι₂₃
inst✝ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j j' : ι₄
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
⊢ ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h ≫ D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j' = d₁ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'

Tactic:
dsimp only [D₁]
  rw [ι_eq _ _ _ _ _ _ _ _ _ _ _ _ _ rfl
      (by rw [← h, ← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄]; rfl),
    assoc, mapBifunctor.ι_D₁]
  by_cases h₁ : c₁.Rel i₁ (c₁.next i₁)
  · rw [d₁_eq _ _ _ _ _ _ _ _ h₁]
    by_cases h₂ : ComplexShape.π c₁ c₂₃ c₄ (c₁.next i₁, ComplexShape.π c₂ c₃ c₂₃ (i₂, i₃)) = j'
    · rw [mapBifunctor.d₁_eq _ _ _ _ h₁ _ _ h₂, ιOrZero_eq,
        Linear.comp_units_smul, NatTrans.naturality_assoc]
      · rfl
      · rw [← h₂, ← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄]
        rfl
    · rw [mapBifunctor.d₁_eq_zero' _ _ _ _ h₁ _ _ h₂, comp_zero,
        ιOrZero_eq_zero _ _ _ _ _ _ _ _ _ _ _ _
          (by simpa only [← ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄] using! h₂),
        comp_zero, smul_zero]
  · rw [mapBifunctor.d₁_eq_zero _ _ _ _ _ _ _ h₁,
      d₁_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₁, comp_zero]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : PathObject Y
h : P.RightHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
⊢ L.map P.p₀ = L.map P.p₁

Tactic:
have := Localization.inverts L (weakEquivalences C) P.ι (by
    rw [← weakEquivalence_iff]
    infer_instance)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : CategoryWithWeakEquivalences C
X Y : C
f g : X ⟶ Y
P : PathObject Y
h : P.RightHomotopy f g
L : C ⥤ (weakEquivalences C).Localization := (weakEquivalences C).Q
this : IsIso (L.map P.ι)
⊢ L.map P.p₀ = L.map P.p₁
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Induced

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
P : ObjectProperty C
t : TStructure C
inst✝ : IsTriangulated C
X : C
a : ℤ
h✝ : t.IsGE X a
n : ℤ
⊢ t.plus ((t.truncLE n).obj X) ∧ t.plus ((t.truncGE n).obj X)

Tactic:
exact ⟨⟨a, inferInstance⟩, ⟨a, inferInstance⟩⟩

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

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
P : ObjectProperty C
t : TStructure C
inst✝ : IsTriangulated C
X : C
a : ℤ
h✝ : t.IsLE X a
n : ℤ
⊢ t.minus ((t.truncLE n).obj X) ∧ t.minus ((t.truncGE n).obj X)

Tactic:
exact ⟨⟨a, inferInstance⟩, ⟨a, inferInstance⟩⟩

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
K : CochainComplex C ℤ
hK : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
L : CochainComplex C ℤ
hL : HomotopyCategory.plus C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
φ : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L
⊢ ∃ Z a b, HomotopyCategory.plus C Z ∧ HomotopyCategory.subcategoryAcyclic C Z ∧ a ≫ b = φ

Tactic:
simp only [HomotopyCategory.plus_quotient_obj_iff] at hL

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
hK : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
L : CochainComplex C ℤ
φ : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L
hL : CochainComplex.plus C L
⊢ ∃ Z a b, HomotopyCategory.plus C Z ∧ HomotopyCategory.subcategoryAcyclic C Z ∧ a ≫ b = φ
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

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

Tactic:
simp [hs, dsimp% σ.s_g]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
x✝¹ x✝ : X ⟶ Y
h : LeftHomotopyRel x✝¹ x✝
⊢ RightHomotopyRel x✝¹ x✝

Tactic:
exact h.rightHomotopyRel

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
i : ℤ
hi : i ≤ n₀ + ↑q₁
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

Tactic:
wlog hq' : q₁ + 1 = q₂ generalizing q₁ q₂

Goal state after:
case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
i : ℤ
hi : i ≤ n₀ + ↑q₁
this : ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂), i ≤ n₀ + ↑q₁ → q₁ + 1 = q₂ → IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
hq' : ¬q₁ + 1 = q₂
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
i : ℤ
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
hi : i ≤ n₀ + ↑q₁
hq' : q₁ + 1 = q₂
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
Module: Mathlib.CategoryTheory.Localization.StructuredArrow

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
X₀ : Paths (LocQuiver W) := { obj := X }
this : ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀), P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
Y : C
g : W.Q.obj X ⟶ W.Q.obj Y
⊢ P (StructuredArrow.mk g)

Tactic:
obtain ⟨g, rfl⟩ := (Quotient.functor (relations W)).map_surjective g

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
X₀ : Paths (LocQuiver W) := { obj := X }
this : ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀), P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
Y : C
g : (Paths.of (LocQuiver W)).obj { obj := X } ⟶ (Paths.of (LocQuiver W)).obj { obj := Y }
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map g))