mathlib-initiative/mathlib-tactics huggingface dataset:
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₁)
⊢ 0 ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
zero_comp

Goal state after:
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₁)
⊢ 0 = 0
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₁₂'
⊢ 0 ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
zero_comp

Goal state after:
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₁₂'
⊢ 0 = 0
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₁₂'
⊢ K.D₁ c₁₂ i₁₂ i₁₂' ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
· rw [K.D₁_shape c₁₂ _ _ h₁, zero_comp]

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₂)
⊢ 0 ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
zero_comp

Goal state after:
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₂)
⊢ 0 = 0
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₁₂'
⊢ 0 ≫ K.D₂ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
zero_comp

Goal state after:
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₁₂'
⊢ 0 = 0
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₁)
h₄ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ 0 ≫ K.D₁ c₁₂ i₁₂' i₁₂'' = 0

Tactic:
zero_comp

Goal state after:
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₁)
h₄ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case neg
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
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ 0 = 0 ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
zero_comp

Goal state after:
case neg
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
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ 0 = 0
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case neg
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
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ 0 = 0 ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
zero_comp

Goal state after:
case neg
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
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ 0 = 0
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₁)
⊢ 0 = 0 ≫ hom₁ h₁ f₂ F c (c.next j) j

Tactic:
zero_comp

Goal state after:
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₁)
⊢ 0 = 0
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 (c₁.prev i₁) i₁
⊢ 0 = 0 ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).D₁ c (c.prev j) j

Tactic:
zero_comp

Goal state after:
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 (c₁.prev i₁) i₁
⊢ 0 = 0
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 (c₁.prev i₁) i₁
h₄ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ 0 ≫ hom₁ h₁ f₂ F c (c.next j) j = 0

Tactic:
zero_comp

Goal state after:
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 (c₁.prev i₁) i₁
h₄ : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ 0 = 0
Module: Mathlib.CategoryTheory.ObjectProperty.Orthogonal

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P : ObjectProperty C
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : P.rightOrthogonal X✝
X : C
f : X ⟶ Y✝
hX : P X
⊢ f ≫ e.inv = 0 ≫ e.inv

Tactic:
zero_comp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
P : ObjectProperty C
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : P.rightOrthogonal X✝
X : C
f : X ⟶ Y✝
hX : P X
⊢ f ≫ e.inv = 0
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: case refine_3
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.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
x✝ : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
hX₃ : P X₃
α : X₁ ⟶ Y
⊢ ∃ a, (fun g ↦ f ≫ g) a = α

Tactic:
· obtain ⟨β, rfl⟩ := Triangle.yoneda_exact₂ _ (inv_rot_of_distTriang _ hT)
      α (hY _ (P.le_shift _ _ hX₃))
    exact ⟨β, rfl⟩

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
⊢ (e₁.inv ≫ f) ≫ e₂.hom = 0 ≫ e₂.hom

Tactic:
zero_comp

Goal state after:
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
⊢ (e₁.inv ≫ f) ≫ e₂.hom = 0
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
inst✝ : Nonempty ι
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i p → (ofHoms fun x ↦ i).rlp p

Tactic:
rintro _ _ _ _ ⟨⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
inst✝ : Nonempty ι
A B X✝ Y✝ : C
i : A ⟶ B
p : X✝ ⟶ Y✝
a✝ : HasLiftingProperty i p
X Y : C
i✝ : ι
⊢ HasLiftingProperty i p
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
inst✝ : Nonempty ι
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i p → (ofHoms fun x ↦ p).llp i

Tactic:
rintro _ _ _ _ ⟨⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
inst✝ : Nonempty ι
A B X✝ Y✝ : C
i : A ⟶ B
p : X✝ ⟶ Y✝
a✝ : HasLiftingProperty i p
X Y : C
i✝ : ι
⊢ HasLiftingProperty i p
Module: Mathlib.CategoryTheory.MorphismProperty.RetractArgument

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₁.IsStableUnderRetracts
h₁ : W₁ ≤ W₂.llp
A B : C
i : A ⟶ B
hi : W₂.llp i
⊢ W₁ i

Tactic:
have h := factorizationData W₁ W₂ i
    have := hi _ h.hp
    simpa using of_retract (RetractArrow.ofLeftLiftingProperty h.fac) h.hi

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithFibrations C
inst✝¹ : (fibrations C).IsStableUnderRetracts
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (trivialFibrations C).IsStableUnderRetracts

Tactic:
dsimp [trivialFibrations]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithFibrations C
inst✝¹ : (fibrations C).IsStableUnderRetracts
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (fibrations C ⊓ weakEquivalences C).IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hY : IsCofibrant Y
⊢ Cofibration coprod.inl

Tactic:
by
  rw [isCofibrant_iff] at hY
  rw [cofibration_iff] at hY ⊢
  exact MorphismProperty.of_isPushout
    ((IsPushout.of_isColimit_binaryCofan_of_isInitial
    (colimit.isColimit (pair X Y)) initialIsInitial).flip) hY

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A : C
P : Cylinder A
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (codiag A)
⊢ Cofibration (ofFactorizationData h).i

Tactic:
simpa using inferInstanceAs (Cofibration h.i)

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

Goal state before:
pp: case e_a
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₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j j' : ι₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
i₂₃ : ι₂₃ := c₂.π c₃ c₂₃ (i₂, i₃)
h₁ : c₂₃.Rel i₂₃ (c₂₃.next i₂₃)
h₂ : ¬c₁.π c₂₃ c₄ (i₁, c₂₃.next i₂₃) = j'
⊢ 0 = d₂ F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j'

Tactic:
by_cases h₃ : c₂.Rel i₂ (c₂.next i₂)
          · rw [d₂_eq _ _ _ _ _ _ _ _ _ h₃, ιOrZero_eq_zero, comp_zero, smul_zero]
            intro h₄
            apply h₂
            rw [← h₄]
            dsimp [ComplexShape.r]
            rw [ComplexShape.assoc c₁ c₂ c₃ c₁₂ c₂₃ c₄, ComplexShape.next_π₁ c₃ c₂₃ h₃ i₃]
          · rw [d₂_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h₃]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h✝¹ : LeftHomotopyRel f g
Z : C
i : Z ⟶ X
P : Cylinder X
left✝ : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder Z
h✝ : Q.IsVeryGood
sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
this : coprod.inl ≫ Q.i ≫ sq.lift = coprod.inl ≫ coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)
⊢ Q.i₀ ≫ sq.lift ≫ h.h = i ≫ f

Tactic:
simp only [Q.inl_i_assoc, coprod.inl_desc] at this

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsFibrant Y
h✝¹ : LeftHomotopyRel f g
Z : C
i : Z ⟶ X
P : Cylinder X
left✝ : P.IsVeryGood
h : P.LeftHomotopy f g
Q : Cylinder Z
h✝ : Q.IsVeryGood
sq : CommSq (coprod.desc (i ≫ P.i₀) (i ≫ P.i₁)) Q.i P.π (Q.π ≫ i)
this : Q.i₀ ≫ sq.lift = i ≫ P.i₀
⊢ Q.i₀ ≫ sq.lift ≫ h.h = i ≫ f
Module: Mathlib.CategoryTheory.Localization.OfQuotient

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
r : HomRel C
W : MorphismProperty C
hW : W.IsInvertedBy (functor r)
hr : ∀ ⦃X Y : C⦄ (f₀ f₁ : X ⟶ Y), r f₀ f₁ → ∃ P x, W P.π
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Quotient r ⥤ E
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ F₁ = F₂

Tactic:
fapply Functor.ext
    · rintro ⟨X⟩
      exact Functor.congr_obj h X
    · rintro ⟨X⟩ ⟨Y⟩ ⟨f⟩
      exact Functor.congr_hom h f

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 : HomologicalComplex.Acyclic K
L : CochainComplex C ℤ
n : ℤ
hn : L.IsStrictlyGE n
φ : K ⟶ L
⊢ ∃ Z a b,
    HomotopyCategory.plus C Z ∧
      HomotopyCategory.subcategoryAcyclic C Z ∧ a ≫ b = (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ

Tactic:
refine ⟨(HomotopyCategory.quotient _ _).obj (K.truncGE n),
      (HomotopyCategory.quotient _ _).map (K.πTruncGE n),
      (HomotopyCategory.quotient _ _).map (CochainComplex.truncGEMap φ n ≫ inv (L.πTruncGE n)),
      ?_, ?_, by simp [← Functor.map_comp]⟩

Goal state after:
case refine_1
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
hK : HomologicalComplex.Acyclic K
L : CochainComplex C ℤ
n : ℤ
hn : L.IsStrictlyGE n
φ : K ⟶ L
⊢ HomotopyCategory.plus C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj (K.truncGE n))

case refine_2
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
hK : HomologicalComplex.Acyclic K
L : CochainComplex C ℤ
n : ℤ
hn : L.IsStrictlyGE n
φ : K ⟶ L
⊢ HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj (K.truncGE n))
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: case mpr.refine_3
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
Z : C
a : Y.obj ⟶ Z
b : Z ⟶ (shiftFunctor C 1).obj X.obj
h : Triangle.mk f.hom a b ∈ Pretriangulated.distinguishedTriangles
hZ : (A ⊓ B) Z
⊢ (A.ι.mapTriangle.obj (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).mor₃ ≫
      (shiftFunctor C 1).map
        (Iso.refl
            (A.ι.mapTriangle.obj
                (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₁).hom =
    (Iso.refl
          (A.ι.mapTriangle.obj
              (Triangle.mk f (homMk a) (homMk (b ≫ (Functor.commShiftIso A.ι 1).inv.app X)))).obj₃).hom ≫
      (Triangle.mk f.hom a b).mor₃

Tactic:
· simp [dsimp% (A.ι.commShiftIso (1 : ℤ)).inv_hom_id_app X]

Goal state after: