mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map
          ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X) ≫
            (shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X) ≫
              (shiftFunctor C m).map ((shiftFunctorAdd' C n' m' p' ⋯).inv.app X) ≫
                (shiftFunctorAdd' C p' m n' ⋯).inv.app X) ≫
        (shiftFunctorAdd' C n' n 0 ⋯).inv.app X

Tactic:
shiftFunctorAdd'_assoc_inv_app n' m' m p' 0 n' _ hm
      (by rw [add_assoc, hm, add_zero]),

Goal state after:
case e_a
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
X : C
m n p m' n' p' : A
hm : m' + m = 0
hn : n' + n = 0
hp : p' + p = 0
h : m + n = p
⊢ 𝟙 ((shiftFunctor C 0).obj X) =
    (shiftFunctorAdd' C n' n 0 hn).hom.app X ≫
      (shiftFunctor C n).map
          ((shiftFunctorZero C A).inv.app ((shiftFunctor C n').obj X) ≫
            (shiftFunctorAdd' C m' m 0 hm).hom.app ((shiftFunctor C n').obj X) ≫
              (shiftFunctorAdd' C m' m 0 hm).inv.app ((shiftFunctor C n').obj X) ≫
                (shiftFunctorAdd' C n' 0 n' ⋯).inv.app X) ≫
        (shiftFunctorAdd' C n' n 0 ⋯).inv.app X
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (linearCombination S ⇑(D R S)).range = ⊤

Tactic:
range_linearCombination,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.span S (Set.range ⇑(D R S)) = ⊤
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
h : Homotopy (f - g) 0
i : ι
⊢ f.f i = (((dNext i) fun i j ↦ h.hom i j) + (prevD i) fun i j ↦ h.hom i j) + g.f i

Tactic:
by simpa [sub_eq_iff_eq_add] using h.comm i

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel i j
A : C
f g : A ⟶ X φ i
h₁ : f ≫ fstX φ i j hij = g ≫ fstX φ i j hij
h₂ : f ≫ sndX φ i = g ≫ sndX φ i
⊢ f = g

Tactic:
have := HasHomotopyCofiber.hasBinaryBiproduct φ _ _ hij
  rw [← cancel_mono (XIsoBiprod φ i j hij).hom]
  apply biprod.hom_ext
  · simpa using! h₁
  · obtain rfl := c.next_eq' hij
    simpa [sndX, dif_pos hij] using! h₂

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
⊢ (inl φ).comp ↑(fst φ) ⋯ = Cochain.ofHom (𝟙 F)

Tactic:
ext p

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p : ℤ
⊢ ((inl φ).comp ↑(fst φ) ⋯).v p p ⋯ = (Cochain.ofHom (𝟙 F)).v p p ⋯
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 0
p q : ℤ
hpq : p + 1 = q
⊢ (δ 0 1 z).v p q hpq = z.v p p ⋯ ≫ G.d p q - F.d p q ≫ z.v q q ⋯

Tactic:
by
  simp only [δ_v 0 1 (zero_add 1) z p q hpq p q (by lia) hpq, Int.negOnePow_one, Units.neg_smul,
    one_smul, sub_eq_add_neg]

Goal state after:
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 ℤ
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
⊢ δ (-1) 0 (Cochain.ofHomotopy h) = Cochain.ofHom φ₁ - Cochain.ofHom φ₂

Tactic:
ext p

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
p : ℤ
⊢ (δ (-1) 0 (Cochain.ofHomotopy h)).v p p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯
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)
⊢ δ (-1) 0 z = Cochain.ofHom (Homotopy.nullHomotopicMap' fun i j hij ↦ z.v i j ⋯)

Tactic:
ext p

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z : Cochain F G (-1)
p : ℤ
⊢ (δ (-1) 0 z).v p p ⋯ = (Cochain.ofHom (Homotopy.nullHomotopicMap' fun i j hij ↦ z.v i j ⋯)).v p p ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
⊢ δ (-1) 0 (inl φ) = Cochain.ofHom (φ ≫ inr φ)

Tactic:
ext p

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p : ℤ
⊢ (δ (-1) 0 (inl φ)).v p p ⋯ = (Cochain.ofHom (φ ≫ inr φ)).v p p ⋯
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case e_a.e_a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f g : C ⟶ D
h k : D ⟶ E
i✝ : ι
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q ⋯).hom

Tactic:
simp [xPrevIso, comp_id]

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

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
F G K L : CochainComplex C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
⊢ φ₁.f p =
    (((dNext p) fun i j ↦ if hij : i + -1 = j then (↑z).v i j hij else 0) +
        (prevD p) fun i j ↦ if hij : i + -1 = j then (↑z).v i j hij else 0) +
      φ₂.f p

Tactic:
have eq := Cochain.congr_v z.2 p p (add_zero p)

Goal state after:
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
z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p : ℤ
eq : (ofHom φ₁).v p p ⋯ = (δ (-1) 0 ↑z + ofHom φ₂).v p p ⋯
⊢ φ₁.f p =
    (((dNext p) fun i j ↦ if hij : i + -1 = j then (↑z).v i j hij else 0) +
        (prevD p) fun i j ↦ if hij : i + -1 = j then (↑z).v i j hij else 0) +
      φ₂.f p
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case pos
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i : ι
hi : c.Rel i (c.next i)
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫ (mapHomologicalComplexObjXIso φ H i).inv = H.map (inrX φ i)

pp: case neg
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i : ι
hi : ¬c.Rel i (c.next i)
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫ (mapHomologicalComplexObjXIso φ H i).inv = H.map (inrX φ i)

Tactic:
· simp [mapHomologicalComplexObjXIso, dif_pos hi, ← Functor.map_comp]

Goal state after:
case neg
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i : ι
hi : ¬c.Rel i (c.next i)
⊢ inrX ((H.mapHomologicalComplex c).map φ) i ≫ (mapHomologicalComplexObjXIso φ H i).inv = H.map (inrX φ i)
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case neg
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫ (mapHomologicalComplexObjXIso φ H i).inv ≫ H.map (d φ i j) =
    inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫
      d ((H.mapHomologicalComplex c).map φ) i j ≫ (mapHomologicalComplexObjXIso φ H j).inv

Tactic:
· simp [← Functor.map_comp, inlX_d' _ _ _ _ hj, inlX_d'_assoc _ _ _ _ hj]

Goal state after:
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 : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn') (-γ) = -γ.rightShift a n' hn'

Tactic:
apply map_neg

Goal state after:
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 : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn).symm (-γ) = -γ.rightUnshift n hn

Tactic:
apply map_neg

Goal state after:
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 : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn') (-γ) = -γ.leftShift a n' hn'

Tactic:
apply map_neg

Goal state after:
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 : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn).symm (-γ) = -γ.leftUnshift n hn

Tactic:
apply map_neg

Goal state after:
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 : ℤ
γ : Cochain K L n
a : ℤ
⊢ (shiftAddHom K L n a) (-γ) = -γ.shift a

Tactic:
apply map_neg

Goal state after:
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 : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ ((γ.rightShift a n' hn').leftShift a n hn').v p q hpq = ((a * n + a * (a - 1) / 2).negOnePow • γ.shift a).v p q hpq

Tactic:
simp only [leftShift_v _ a n hn' p q hpq (p + a) (by lia),
    rightShift_v _ a n' hn' (p + a) q (by lia) (q + a) (by lia), units_smul_v, shift_v']

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n = q
⊢ (a * n + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (p + a) ⋯).hom ≫ γ.v (p + a) (q + a) ⋯ ≫ (L.shiftFunctorObjXIso a q (q + a) ⋯).inv =
    (a * n + a * (a - 1) / 2).negOnePow • γ.v (p + a) (q + a) ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
⊢ mapOfHomotopy H ≫ (triangle φ₂).mor₃ = (triangle φ₁).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a

Tactic:
ext p

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K₁ L₁ K₂ L₂ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
H : Homotopy (φ₁ ≫ b) (a ≫ φ₂)
p : ℤ
⊢ (mapOfHomotopy H ≫ (triangle φ₂).mor₃).f p =
    ((triangle φ₁).mor₃ ≫ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map a).f p
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
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
⊢ productTriangle T ∈ distinguishedTriangles

Tactic:
have h₂ : φ'.hom₂ = 𝟙 _ := by cat_disch

Goal state after:
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
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
⊢ productTriangle T ∈ distinguishedTriangles
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ Cochain.ofHom ((triangle φ).mor₃ ≫ (rotateHomotopyEquiv φ).hom) =
    δ (-1) 0 (-(snd φ).comp (inl (inr φ)) ⋯) + Cochain.ofHom (inr (inr φ))

Tactic:
ext p

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
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ (Cochain.ofHom ((triangle φ).mor₃ ≫ (rotateHomotopyEquiv φ).hom)).v p p ⋯ =
    (δ (-1) 0 (-(snd φ).comp (inl (inr φ)) ⋯) + Cochain.ofHom (inr (inr φ))).v p p ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (rotateHomotopyEquiv φ).hom ≫ (triangle (inr φ)).mor₃ = -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ

Tactic:
ext p

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
p : ℤ
⊢ ((rotateHomotopyEquiv φ).hom ≫ (triangle (inr φ)).mor₃).f p =
    (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map φ).f p
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ δ (-1) 0 (n.negOnePow • (inl φ).shift n) =
    Cochain.ofHom
      ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ ≫
        (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ))

Tactic:
ext p

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
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (δ (-1) 0 (n.negOnePow • (inl φ).shift n)).v p p ⋯ =
    (Cochain.ofHom
          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ ≫
            (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ))).v
      p p ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ lift ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (fst φ).shift n) ((snd φ).shift n)
        ⋯ ≫
      desc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (inl φ).shift n)
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ)) ⋯ =
    𝟙 ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj (mappingCone φ))

Tactic:
ext p

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
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (lift ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (fst φ).shift n) ((snd φ).shift n)
            ⋯ ≫
          desc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (inl φ).shift n)
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ)) ⋯).f
      p =
    (𝟙 ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj (mappingCone φ))).f p
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ desc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (inl φ).shift n)
        ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ)) ⋯ ≫
      lift ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (fst φ).shift n)
        ((snd φ).shift n) ⋯ =
    𝟙 (mappingCone ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ))

Tactic:
ext p

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
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (desc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (inl φ).shift n)
            ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (inr φ)) ⋯ ≫
          lift ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) (n.negOnePow • (fst φ).shift n)
            ((snd φ).shift n) ⋯).f
      p =
    (𝟙 (mappingCone ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ))).f p
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₂ ≫ (shiftIso φ n).hom =
    (n.negOnePow • Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₂).hom ≫
      (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₂

Tactic:
ext p

Goal state after:
case refine_2
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₂ ≫ (shiftIso φ n).hom).f p =
    ((n.negOnePow • Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₂).hom ≫
          (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₂).f
      p
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_3
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₃ ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map
        (Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₁).hom =
    (shiftIso φ n).hom ≫ (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₃

Tactic:
ext p

Goal state after:
case refine_3
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n p : ℤ
⊢ (((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).mor₃ ≫
          (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map
            (Iso.refl ((Triangle.shiftFunctor (CochainComplex C ℤ) n).obj (triangle φ)).obj₁).hom).f
      p =
    ((shiftIso φ n).hom ≫ (triangle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)).mor₃).f p
Module: Mathlib.CategoryTheory.Triangulated.Functor

Goal state before:
pp: case h₂
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Category.{v_3, u_3} E
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasShift D ℤ
inst✝³ : HasShift E ℤ
F : C ⥤ D
inst✝² : F.CommShift ℤ
G : D ⥤ E
inst✝¹ : G.CommShift ℤ
inst✝ : F.Faithful
X Y : Triangle C
f g : X ⟶ Y
h : F.mapTriangle.map f = F.mapTriangle.map g
⊢ F.map f.hom₂ = F.map g.hom₂

Tactic:
exact congr_arg TriangleMorphism.hom₂ h

Goal state after: