mathlib-initiative/mathlib-tactics huggingface dataset:
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
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₄
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₁ Y₁ : GradedObject I₁ C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : GradedObject I₃ C₃
f₃ : X₃ ⟶ Y₃
inst✝¹ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : p (i₁, i₂, i₃) = j
⊢ ((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      (((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫ ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃)) ≫
        (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h =
    ((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
          (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h

Tactic:
assoc

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
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₄
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₁ Y₁ : GradedObject I₁ C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : GradedObject I₂ C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : GradedObject I₃ C₃
f₃ : X₃ ⟶ Y₃
inst✝¹ : ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
inst✝ : ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃).HasMap p
i₁ : I₁
i₂ : I₂
i₃ : I₃
j : J
h : p (i₁, i₂, i₃) = j
⊢ ((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
          (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h =
    ((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
      ((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
        ((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫
          (((mapTrifunctorObj F Y₁ I₂ I₃).obj Y₂).obj Y₃).ιMapObj p (i₁, i₂, i₃) j h
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₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁₂.next (c₁.π c₂ c₁₂ (c₁.next i₁, i₂)) = i₁₂''

Tactic:
← ComplexShape.next_π₁ c₂ c₁₂ h₃,

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₁)
h₄ : c₁.Rel (c₁.next i₁) (c₁.next (c₁.next i₁))
⊢ c₁₂.next (c₁₂.next (c₁.π c₂ c₁₂ (i₁, 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₁₂'' : 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₂)
h₅ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
⊢ c₁.π c₂ c₁₂ (c₁.next i₁, c₂.next i₂) = c₁₂.next i₁₂'

Tactic:
← ComplexShape.next_π₁ c₂ c₁₂ h₃,

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₁₂'' : 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₂)
h₅ : c₁.π c₂ c₁₂ (i₁, c₂.next i₂) = i₁₂'
⊢ c₁₂.next (c₁.π c₂ c₁₂ (i₁, c₂.next i₂)) = c₁₂.next i₁₂'
Module: Mathlib.Algebra.Homology.TotalComplexSymmetry

Goal state before:
pp: case pos
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
⊢ c₁.σ c₂ c i₁ i₂ • K.d₂ c i₁ i₂ j' =
    K.flip.ιTotal c i₂ i₁ j h₁ ≫
      K.flip.D₁ c j j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
ι_D₁_assoc

Goal state after:
case pos
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
⊢ c₁.σ c₂ c i₁ i₂ • K.d₂ c i₁ i₂ j' =
    K.flip.d₁ c i₂ i₁ j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯
Module: Mathlib.CategoryTheory.Center.NegOnePow

Goal state before:
pp: case inl
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X : C
n : ℤ
⊢ (↑((-1) ^ (n + n))).app X = (n + n).negOnePow • 𝟙 X

Tactic:
simp [zpow_add, ← mul_zpow, Int.negOnePow_even _ (Even.add_self n)]

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

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

Tactic:
ιMapBifunctor_hom₁_assoc _ _ _ _ _ _ _ _ _ _ rfl

Goal state after:
case 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₂ : 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)
⊢ (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    (c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
        (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
          (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ (c.prev j)) ≫
      (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).D₁ c (c.prev j) j
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case 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₂ : 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)
⊢ K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫
      hom₁ h₁ f₂ F c j (c.prev j) ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).D₂ c (c.prev j) j =
    -(((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:
ιMapBifunctor_hom₁_assoc _ _ _ _ _ _ _ _ _ _ rfl

Goal state after:
case 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₂ : 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)
⊢ (c₁.ε₁ c₂ c (c₁.prev i₁, i₂) •
        (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
          (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ L₁.ιMapBifunctorOrZero L₂ F c (c₁.prev i₁) i₂ (c.prev j)) ≫
      (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).D₂ c (c.prev j) j =
    -(((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁ i₂ (c.next j) ≫ hom₁ h₁ f₂ F c (c.next j) j
Module: Mathlib.Algebra.Homology.CochainComplexOpposite

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
m : ℤ
hK : HomologicalComplex.ExactAt K (-m)
hm : -m + m = 0
⊢ HomologicalComplex.ExactAt ((opEquivalence C).functor.obj (op K)) m

Tactic:
rw [HomologicalComplex.exactAt_iff' _ (m - 1) m (m + 1) (by simp) (by simp),
    ← ShortComplex.exact_unop_iff]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
m : ℤ
hK : HomologicalComplex.ExactAt K (-m)
hm : -m + m = 0
⊢ (HomologicalComplex.sc' ((opEquivalence C).functor.obj (op K)) (m - 1) m (m + 1)).unop.Exact
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 y : Cocycle K L n
h : toHom (mk x) = toHom (mk y)
⊢ x - y ∈ coboundaries K L n

Tactic:
← toHom_mk_eq_zero_iff,

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
x y : Cocycle K L n
h : toHom (mk x) = toHom (mk y)
⊢ toHom (mk (x - y)) = 0
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
Y : C
hY : P.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₃
this : ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0
α₁ α₂ : X₂ ⟶ Y
hα : (fun g ↦ f ≫ g) α₁ = (fun g ↦ f ≫ g) α₂
⊢ f ≫ (α₁ - α₂) = 0

Tactic:
simpa [sub_eq_zero] using hα

Goal state after:
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
X : C
hX : P.leftOrthogonal X
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
Y : C
⊢ Function.Bijective L.map

Tactic:
rw [← isColocal_trW] at hX

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
X : C
hX : P.trW.isColocal X
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
Y : C
⊢ Function.Bijective L.map
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
n : ℤ
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : t.IsGE X✝ n
⊢ t.IsGE Y✝ n

Tactic:
exact t.isGE_of_iso e _

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
X✝ Y✝ : C
e : X✝ ≅ Y✝
⊢ t.minus X✝ → t.minus Y✝

Tactic:
rintro ⟨n, _⟩; exact ⟨_, t.isLE_of_iso e n⟩

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

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.retracts ≤ T.rlp.llp

Tactic:
exact T.retracts_le_llp_rlp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (fibrations C).IsStableUnderBaseChange

Tactic:
← trivialCofibrations_rlp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (trivialCofibrations C).rlp.IsStableUnderBaseChange
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (fibrations C).IsMultiplicative

Tactic:
← trivialCofibrations_rlp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (trivialCofibrations C).rlp.IsMultiplicative
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
J : Type w
⊢ (fibrations C).IsStableUnderProductsOfShape J

Tactic:
← trivialCofibrations_rlp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
J : Type w
⊢ (trivialCofibrations C).rlp.IsStableUnderProductsOfShape J
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
inst✝² : IsCofibrant A
P P' : Cylinder A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : P.I ⨿ A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr P.i₁ P'.i₀
sq : IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr P.i₁ P'.i₀)
⊢ Cofibration ψ

Tactic:
rw [cofibration_iff]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : Cylinder A
inst✝² : IsCofibrant A
P P' : Cylinder A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : P.I ⨿ A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr P.i₁ P'.i₀
sq : IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr P.i₁ P'.i₀)
⊢ cofibrations C ψ
Module: Mathlib.AlgebraicTopology.ModelCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CategoryWithFibrations C
inst✝⁶ : CategoryWithCofibrations C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : HasFiniteLimits C
inst✝³ : HasFiniteColimits C
inst✝² : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
h : RetractArrow f w
hw : weakEquivalences C w
⊢ weakEquivalences C f

Tactic:
rw [← weakEquivalence_iff] at hw
    have hf := factorizationData (trivialCofibrations C) (fibrations C) f
    have : Cofibration hf.i := by
      simpa only [cofibration_iff] using hf.hi.1
    have : WeakEquivalence hf.i := by
      simpa only [weakEquivalence_iff] using hf.hi.2
    let φ : pushout hf.i h.i.left ⟶ Y :=
      pushout.desc (hf.p ≫ h.i.right) w (by simp)
    have : Fibration hf.p := by simpa only [fibration_iff] using hf.hp
    have : WeakEquivalence (pushout.inr _ _ ≫ φ) := by simpa [φ]
    have := weakEquivalence_of_precomp (pushout.inr _ _) φ
    have hp : RetractArrow hf.p φ :=
      { i := Arrow.homMk (pushout.inl _ _) h.i.right
        r := Arrow.homMk (pushout.desc (𝟙 _) (h.r.left ≫ hf.i) (by simp)) h.r.right }
    have := mk'.cm3a_aux hp
    rw [← weakEquivalence_iff, ← hf.fac]
    infer_instance

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
P : Cylinder X
f g : X ⟶ Y
h : P.LeftHomotopy f g
d : (cofibrations C).MapFactorizationData (trivialFibrations C) P.i :=
  (cofibrations C).factorizationData (trivialFibrations C) P.i
⊢ Cofibration
    { I := d.Z, i₀ := coprod.inl ≫ d.i, i₁ := coprod.inr ≫ d.i, π := d.p ≫ P.π, i₀_π := ⋯, i₁_π := ⋯,
        weakEquivalence_π := ⋯ }.i

Tactic:
rw [cofibration_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
P : Cylinder X
f g : X ⟶ Y
h : P.LeftHomotopy f g
d : (cofibrations C).MapFactorizationData (trivialFibrations C) P.i :=
  (cofibrations C).factorizationData (trivialFibrations C) P.i
⊢ cofibrations C
    { I := d.Z, i₀ := coprod.inl ≫ d.i, i₁ := coprod.inr ≫ d.i, π := d.p ≫ P.π, i₀_π := ⋯, i₁_π := ⋯,
        weakEquivalence_π := ⋯ }.i
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
h : CochainComplex.plus C L
hL : (quotient C (ComplexShape.up ℤ)).obj L = (quotient C (ComplexShape.up ℤ)).obj K
⊢ CochainComplex.plus C K

Tactic:
obtain rfl : L = K := congr_arg Quotient.as hL

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
L : CochainComplex C ℤ
h : CochainComplex.plus C L
hL : (quotient C (ComplexShape.up ℤ)).obj L = (quotient C (ComplexShape.up ℤ)).obj L
⊢ CochainComplex.plus C L
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: case zero.succ.succ.zero
C : Type u_1
inst✝ : Category.{v_1, u_1} C
j : ℕ
hj :
  ∀ {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (k : ℕ) (hij : 0 ≤ j) (hjk : j ≤ k),
    map f 0 k ⋯ = map f 0 j hij ≫ map f j k hjk
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
hij : 0 ≤ j + 1
hjk : j + 1 ≤ 0 + 1
⊢ map f 0 (0 + 1) ⋯ = map f 0 (j + 1) hij ≫ map f (j + 1) (0 + 1) hjk

Tactic:
obtain rfl : j = 0 := by lia
            rw [map_id, comp_id]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
e : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ≅ (t.triangleLTGE n).obj Y
he : e.hom.hom₂ = (Iso.refl (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₂).hom
⊢ IsIso ((t.truncLT n).map f)

Tactic:
suffices ((t.truncLT n).map f) = e.hom.hom₁ by rw [this]; infer_instance

Goal state after:
case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
e : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ≅ (t.triangleLTGE n).obj Y
he : e.hom.hom₂ = (Iso.refl (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₂).hom
⊢ (t.truncLT n).map f = e.hom.hom₁
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
x✝ : ∃ X f h, ∃ (_ : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles), t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles
h✝ : t.IsLE X n₀
⊢ t.IsLE ((t.triangleLTGE n₁).obj Y).obj₁ n₀

Tactic:
by dsimp; rw [← hn]; infer_instance

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
g : Y ⟶ Z
inst✝¹ : Fibration g
inst✝ : WeakEquivalence g
f₀ f₁ : X ⟶ Y
h✝ : LeftHomotopyRel (f₀ ≫ g) (f₁ ≫ g)
P : Cylinder X
left✝ : P.IsGood
h : P.LeftHomotopy (f₀ ≫ g) (f₁ ≫ g)
sq : CommSq (coprod.desc f₀ f₁) P.i g h.h
⊢ P.i₁ ≫ sq.lift = f₁

Tactic:
by
          have := coprod.inr ≫= sq.fac_left
          rwa [P.inr_i_assoc, coprod.inr_desc] at this

Goal state after: