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

Goal state before:
pp: case pos
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{v_1, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
i j : ι
h✝ : c.Rel j i
⊢ G.map (hom i j h✝) = (fun i j hij ↦ G.map (hom i j hij)) i j h✝

pp: case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{v_1, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
i j : ι
h✝ : ¬c.Rel j i
⊢ G.map 0 = 0

Tactic:
· rfl

Goal state after:
case neg
ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
W : Type u_2
inst✝² : Category.{v_1, u_2} W
inst✝¹ : Preadditive W
G : V ⥤ W
inst✝ : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
i j : ι
h✝ : ¬c.Rel j i
⊢ G.map 0 = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n m : ℤ
hnm : n + 1 = m
z : Cochain F G n
p q : ℤ
hpq : p + m = q
q₁ q₂ : ℤ
hq₁ : q₁ = q - 1
hq₂ : p + 1 = q₂
⊢ (δ n m z).v p q hpq = z.v p q₁ ⋯ ≫ G.d q₁ q + m.negOnePow • F.d p q₂ ≫ z.v q₂ q ⋯

Tactic:
by
  obtain rfl : q₁ = p + n := by lia
  obtain rfl : q₂ = p + m - n := by lia
  rfl

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
p : ℤ
φ : F ⟶ G
h : p = 1
⊢ δ 0 p (Cochain.ofHom φ) = 0

Tactic:
subst h

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
⊢ δ 0 1 (Cochain.ofHom φ) = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z : Cochain F G (-1)
p : ℤ
⊢ z.v p (p - 1) ⋯ ≫ G.d (p - 1) p + F.d p (p + 1) ≫ z.v (p + 1) p ⋯ =
    (Homotopy.nullHomotopicMap' fun i j hij ↦ z.v i j ⋯).f p

Tactic:
Homotopy.nullHomotopicMap'_f (show (ComplexShape.up ℤ).Rel (p - 1) p by simp)
    (show (ComplexShape.up ℤ).Rel p (p + 1) by simp)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z : Cochain F G (-1)
p : ℤ
⊢ z.v p (p - 1) ⋯ ≫ G.d (p - 1) p + F.d p (p + 1) ≫ z.v (p + 1) p ⋯ =
    F.d p (p + 1) ≫ z.v (p + 1) p ⋯ + z.v p (p - 1) ⋯ ≫ G.d (p - 1) p
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
h : i + -1 = j
⊢ (ofHomotopy ho).v i j h = ho.hom i j

pp: case neg
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
h : ¬i + -1 = j
⊢ 0 = ho.hom i j

Tactic:
· rfl

Goal state after:
case neg
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
i j : ℤ
h : ¬i + -1 = j
⊢ 0 = ho.hom i j
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h : p'' = p
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''

Tactic:
subst h

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
q n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
f : K.X p'' ⟶ L.X q
hp' : p' + 1 = p''
h : q = q'' - 1
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''

Tactic:
subst h

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
hm : n + 1 = m
p' q' p'' q'' : ℤ
hpq'' : p'' + m = q''
hp' : p' + 1 = p''
hq' : q'' - 1 + 1 = q'
f : K.X p'' ⟶ L.X (q'' - 1)
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d (q'' - 1) q') m).v p'' q'' hpq''
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
h : q'' = q
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''

Tactic:
subst h

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
h : p'' = p'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''

Tactic:
subst h

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p n q' p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
hp' : p'' + 1 = p
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p'' p ≫ f) (n + 1)).v p'' q'' hpq''
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: case h_map
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ ∀ (X Y : Quotient r) (f : X ⟶ Y), Φ.map f ≍ (lift r (functor r ⋙ Φ) H).map f

Tactic:
rintro _ _ f

Goal state after:
case h_map
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ Φ.map f ≍ (lift r (functor r ⋙ Φ) H).map f
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n₁ n₂ n₁₂ : ℤ
h : n₁ + n₂ = n₁₂
K : CochainComplex C ℤ
x✝² x✝¹ : ℤ
x✝ : (ComplexShape.up ℤ).Rel x✝² x✝¹
⊢ (K.shiftFunctorObjXIso n₁₂ x✝² (x✝² + n₂ + n₁) ⋯).hom ≫ ((shiftFunctor C n₁ ⋙ shiftFunctor C n₂).obj K).d x✝² x✝¹ =
    ((shiftFunctor C n₁₂).obj K).d x✝² x✝¹ ≫ (K.shiftFunctorObjXIso n₁₂ x✝¹ (x✝¹ + n₂ + n₁) ⋯).hom

Tactic:
subst h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n₁ n₂ : ℤ
K : CochainComplex C ℤ
x✝² x✝¹ : ℤ
x✝ : (ComplexShape.up ℤ).Rel x✝² x✝¹
⊢ (K.shiftFunctorObjXIso (n₁ + n₂) x✝² (x✝² + n₂ + n₁) ⋯).hom ≫
      ((shiftFunctor C n₁ ⋙ shiftFunctor C n₂).obj K).d x✝² x✝¹ =
    ((shiftFunctor C (n₁ + n₂)).obj K).d x✝² x✝¹ ≫ (K.shiftFunctorObjXIso (n₁ + n₂) x✝¹ (x✝¹ + n₂ + n₁) ⋯).hom
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).inv.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
subst h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).inv.app K).f n = (XIsoOfEq K ⋯).hom
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
subst h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).hom.app K).f n = (XIsoOfEq K ⋯).hom
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a : ℤ
⊢ shift 0 a = 0

Tactic:
change shiftAddHom K L n a 0 = 0
  apply map_zero

Goal state after:
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a : A
h : a = 0
⊢ commShiftIso F a = CommShift.isoZero' F A a h

Tactic:
subst h

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
⊢ commShiftIso F 0 = CommShift.isoZero' F A 0 ⋯
Module: Mathlib.CategoryTheory.Shift.CommShift

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a b c : A
h : a + b = c
⊢ commShiftIso F c = CommShift.isoAdd' h (commShiftIso F a) (commShiftIso F b)

Tactic:
subst h

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a b : A
⊢ commShiftIso F (a + b) = CommShift.isoAdd' ⋯ (commShiftIso F a) (commShiftIso F b)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : Rˣ
⊢ (x • γ).shift a = x • γ.shift a

Tactic:
ext p q hpq
  dsimp
  simp only [shift_v', units_smul_v]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A B : Triangle C
h : A = B
⊢ A.obj₁ = B.obj₁

Tactic:
subst h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A : Triangle C
⊢ A.obj₁ = A.obj₁
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
h : A = B
⊢ (eqToHom h).hom₁ = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A : Triangle C
⊢ (eqToHom ⋯).hom₁ = eqToHom ⋯
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A B : Triangle C
h : A = B
⊢ A.obj₂ = B.obj₂

Tactic:
subst h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A : Triangle C
⊢ A.obj₂ = A.obj₂
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
h : A = B
⊢ (eqToHom h).hom₂ = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A : Triangle C
⊢ (eqToHom ⋯).hom₂ = eqToHom ⋯
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A B : Triangle C
h : A = B
⊢ A.obj₃ = B.obj₃

Tactic:
subst h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A : Triangle C
⊢ A.obj₃ = A.obj₃
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
h : A = B
⊢ (eqToHom h).hom₃ = eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A : Triangle C
⊢ (eqToHom ⋯).hom₃ = eqToHom ⋯
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
T : Triangle C
⊢ ((shiftFunctor C n).obj T).mor₁ ≫ ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₂).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₁).hom ≫ ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₁

Tactic:
subst h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ ((shiftFunctor C (a + b)).obj T).mor₁ ≫ ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).app T.obj₂).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).app T.obj₁).hom ≫
      ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₁
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
T : Triangle C
⊢ ((shiftFunctor C n).obj T).mor₂ ≫ ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₃).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₂).hom ≫ ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₂

Tactic:
subst h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ ((shiftFunctor C (a + b)).obj T).mor₂ ≫ ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).app T.obj₃).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).app T.obj₂).hom ≫
      ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₂
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b n : ℤ
h : a + b = n
T : Triangle C
⊢ ((shiftFunctor C n).obj T).mor₃ ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₁).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b n h).app T.obj₃).hom ≫ ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₃

Tactic:
subst h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ ((shiftFunctor C (a + b)).obj T).mor₃ ≫
      (CategoryTheory.shiftFunctor C 1).map ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).app T.obj₁).hom =
    ((CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).app T.obj₃).hom ≫
      ((shiftFunctor C a ⋙ shiftFunctor C b).obj T).mor₃
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b c : ℤ
h : a + b = c
⊢ CategoryTheory.shiftFunctorAdd' (Triangle C) a b c h = shiftFunctorAdd' C a b c h

Tactic:
subst h

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
⊢ CategoryTheory.shiftFunctorAdd' (Triangle C) a b (a + b) ⋯ = shiftFunctorAdd' C a b (a + b) ⋯
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.mor₂ = 0 ↔ Epi T.mor₁

Tactic:
have h := mor₃_eq_zero_iff_epi₂ _ (inv_rot_of_distTriang _ hT)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h : T.invRotate.mor₃ = 0 ↔ Epi T.invRotate.mor₂
⊢ T.mor₂ = 0 ↔ Epi T.mor₁
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case ofNat
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
H : ℤ → Prop := fun n ↦ ∀ T ∈ distinguishedTriangles, (shiftFunctor C n).obj T ∈ distinguishedTriangles
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
n : ℕ
⊢ H (Int.ofNat n)

Tactic:
induction n with
    | zero => exact H_zero
    | succ n hn => exact H_add hn H_one rfl

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
⊢ (g ≫ φ.hom₁) ≫ T'.invRotate.mor₂ = 0

Tactic:
dsimp; rw [assoc, ← φ.comm₁, hf]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit

Goal state before:
pp: case mpr
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ (∃ S σ, Nonempty (T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ)) → T ∈ distinguishedTriangles

Tactic:
rintro ⟨S, σ, ⟨e⟩⟩

Goal state after:
case mpr
C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (HomologicalComplex.eval C (ComplexShape.up ℤ) n)).Splitting
e : T ≅ CochainComplex.trianglehOfDegreewiseSplit S σ
⊢ T ∈ distinguishedTriangles
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝¹ : K.HasHomology i
inst✝ : K.HasHomology j
⊢ K.opcyclesToCycles i j ≫ K.iCycles j = K.fromOpcycles i j

Tactic:
by
  dsimp only [opcyclesToCycles]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: V : Type u₁
inst✝ : Quiver V
a : Paths V
P : {b : Paths V} → (a ⟶ b) → Prop
id : P (𝟙 a)
comp : ∀ {u v : V} (p : a ⟶ (of V).obj u) (q : u ⟶ v), P p → P (p ≫ (of V).map q)
⊢ ∀ {b : Paths V} (f : a ⟶ b), P f

Tactic:
by
  intro _ f
  induction f with
  | nil => exact id
  | cons _ w h => exact comp _ w h

Goal state after:
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
π : C ⥤ D
H : D ⥤ A
e : π ⋙ H ≅ F
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
G : Type u_5
inst✝³ : AddGroup G
inst✝² : HasShift C G
inst✝¹ : F.ShiftSequence M
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ n + a' = a

Tactic:
by rw [← ha', ← add_assoc, hnm, zero_add]

Goal state after:
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
X : Paths V
⊢ ∀ (Y : Paths V) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
Y

Goal state after:
case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
X Y : Paths V
⊢ ∀ (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: case neg
C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this✝ : Epi S.g
this : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i)
e : S.map (HomologicalComplex.homologyFunctor C c i) ≅ S.map (HomologicalComplex.opcyclesFunctor C c i)
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ }.Exact

Tactic:
exact ShortComplex.exact_of_iso e.symm (opcycles_right_exact S hS.exact i)

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X : LocQuiver W
⊢ {Y : LocQuiver W} → (X ⟶ Y) → (G.obj X.obj ⟶ G.obj Y.obj)

Tactic:
Y

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : LocQuiver W
⊢ (X ⟶ Y) → (G.obj X.obj ⟶ G.obj Y.obj)
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X : C
⊢ ∀ (Y : C) (f : X ⟶ Y), (W.Q ⋙ lift G hG).map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
Y

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : C
⊢ ∀ (f : X ⟶ Y), (W.Q ⋙ lift G hG).map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
⊢ ∀ (X Y : C) (f : X ⟶ Y), (W.Q ⋙ lift G hG).map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
intro X Y f
      simp only [Functor.comp_map, eqToHom_refl, comp_id, id_comp]
      dsimp [MorphismProperty.Q, Quot.liftOn, Quotient.functor]
      rw [composePath_toPath]

Goal state after: