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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X) =
    (shiftFunctorComm C n 0).hom.app X ≫ (shiftFunctor C n).map ((shiftFunctorZero C A).hom.app X)

Tactic:
← shiftFunctorAdd'_zero_add_inv_app n X,

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
n : A
⊢ (shiftFunctorZero C A).hom.app ((shiftFunctor C n).obj X) =
    (shiftFunctorComm C n 0).hom.app X ≫ (shiftFunctorAdd' C 0 n n ⋯).inv.app X
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
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
i j : ι
⊢ (dite (c.Rel j i) (hom i j) fun x ↦ 0) ≫ g.f j = dite (c.Rel j i) ((fun i j hij ↦ hom i j hij ≫ g.f j) i j) fun x ↦ 0

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
i j : ι
h✝ : c.Rel j i
⊢ hom i j h✝ ≫ g.f j = (fun i j hij ↦ hom i j hij ≫ g.f j) i j h✝

case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
i j : ι
h✝ : ¬c.Rel j i
⊢ 0 ≫ g.f j = 0
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 : C ⟶ D
hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)
i j : ι
⊢ (f.f i ≫ dite (c.Rel j i) (hom i j) fun x ↦ 0) = dite (c.Rel j i) ((fun i j hij ↦ f.f i ≫ hom i j hij) i j) fun x ↦ 0

Tactic:
split_ifs

Goal state after:
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)
i j : ι
h✝ : c.Rel j i
⊢ f.f i ≫ hom i j h✝ = (fun i j hij ↦ f.f i ≫ hom i j hij) i j h✝

case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomologicalComplex V c
f : C ⟶ D
hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)
i j : ι
h✝ : ¬c.Rel j i
⊢ f.f i ≫ 0 = 0
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 : 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 : ι
⊢ G.map (dite (c.Rel j i) (hom i j) fun x ↦ 0) = dite (c.Rel j i) ((fun i j hij ↦ G.map (hom i j hij)) i j) fun x ↦ 0

Tactic:
split_ifs

Goal state after:
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✝

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 : ℤ
z₁ : Cochain F G n
⊢ z₁.comp (ofHom (𝟙 G)) ⋯ = z₁

Tactic:
by
  ext p q hpq
  simp only [comp_zero_cochain_v, ofHom_v, HomologicalComplex.id_f, comp_id]

Goal state after:
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 : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun x ↦ 0) + (dite (c.Rel k₂ k₁) (h k₁ k₂) fun x ↦ 0) ≫ D.d k₂ k₁ =
    C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Tactic:
split_ifs

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁
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 : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (dite (c.Rel k₁ k₀) (h k₀ k₁) fun x ↦ 0) ≫ D.d k₁ k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀

Tactic:
split_ifs

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ h k₀ k₁ r₁₀ ≫ D.d k₁ k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀
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 : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun x ↦ 0) = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀

Tactic:
split_ifs

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀
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 K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
i : ι
⊢ (inrX φ i ≫
      if hj : c.Rel i (c.next i) then fstX φ i (c.next i) hj ≫ hα.hom (c.next i) i + sndX φ i ≫ α.f i
      else sndX φ i ≫ α.f i) =
    α.f i

Tactic:
split_ifs

Goal state after:
case pos
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
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
i : ι
h✝ : c.Rel i (c.next i)
⊢ inrX φ i ≫ (fstX φ i (c.next i) h✝ ≫ hα.hom (c.next i) i + sndX φ i ≫ α.f i) = α.f i

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
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
i : ι
h✝ : ¬c.Rel i (c.next i)
⊢ inrX φ i ≫ sndX φ i ≫ α.f i = α.f i
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case neg
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:
· rw [δ_shape]
    lia

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

Goal state before:
pp: case pos.h₁
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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
hj : c.Rel j (c.next j)
⊢ inlX φ (c.next j) j hj ≫ f.f j =
    inlX φ (c.next j) j hj ≫
      (desc φ (inr φ ≫ f) ((Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))).f j

pp: case pos.h₂
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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
hj : c.Rel j (c.next j)
⊢ inrX φ j ≫ f.f j =
    inrX φ j ≫
      (desc φ (inr φ ≫ f) ((Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))).f j

Tactic:
· simp [inrCompHomotopy_hom _ _ _ _ hj]

Goal state after:
case pos.h₂
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
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
hj : c.Rel j (c.next j)
⊢ inrX φ j ≫ f.f j =
    inrX φ j ≫
      (desc φ (inr φ ≫ f) ((Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))).f j
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 ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
i j : ι
hij : c.Rel j i
hj : ∃ k, c.Rel k j
⊢ inlX K i j hij ≫
      (Homotopy.nullHomotopicMap' fun i j hij ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ biprod.snd.f i ≫ inlX K i j hij).f
        j =
    inlX K i j hij ≫ ((π K).f j ≫ (ι₀ K).f j - 𝟙 (homotopyCofiber.X (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
obtain ⟨k, hjk⟩ := hj

Goal state after:
case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
i j : ι
hij : c.Rel j i
k : ι
hjk : c.Rel k j
⊢ inlX K i j hij ≫
      (Homotopy.nullHomotopicMap' fun i j hij ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ biprod.snd.f i ≫ inlX K i j hij).f
        j =
    inlX K i j hij ≫ ((π K).f j ≫ (ι₀ K).f j - 𝟙 (homotopyCofiber.X (biprod.lift (𝟙 K) (-𝟙 K)) j))
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 ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∃ k, c.Rel j k
⊢ inrX K j ≫
      (Homotopy.nullHomotopicMap' fun i j hij ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ biprod.snd.f i ≫ inlX K i j hij).f
        j =
    inrX K j ≫ ((π K).f j ≫ (ι₀ K).f j - 𝟙 (homotopyCofiber.X (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
obtain ⟨k, hjk⟩ := hj

Goal state after:
case pos
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ inrX K j ≫
      (Homotopy.nullHomotopicMap' fun i j hij ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ biprod.snd.f i ≫ inlX K i j hij).f
        j =
    inrX K j ≫ ((π K).f j ≫ (ι₀ K).f j - 𝟙 (homotopyCofiber.X (biprod.lift (𝟙 K) (-𝟙 K)) j))
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 n' : ℤ
hn' : n' + a = n
⊢ rightShift 0 a n' hn' = 0

Tactic:
by
  change rightShiftAddEquiv K L n a n' hn' 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
X : C
a b : A
h : a + b = 0
eq :
  F.map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) =
    F.map ((shiftFunctorAdd' C a b 0 h).hom.app X) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd' D a b 0 h).inv.app (F.obj X)
⊢ F.map ((shiftFunctorAdd' C a b 0 h).inv.app X ≫ (shiftFunctorZero C A).hom.app X) =
    (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫
        (shiftFunctorAdd' D a b 0 h).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.obj X)

Tactic:
← cancel_epi (F.map ((shiftFunctorAdd' C a b 0 h).hom.app X)),

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
X : C
a b : A
h : a + b = 0
eq :
  F.map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) =
    F.map ((shiftFunctorAdd' C a b 0 h).hom.app X) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd' D a b 0 h).inv.app (F.obj X)
⊢ F.map ((shiftFunctorAdd' C a b 0 h).hom.app X) ≫
      F.map ((shiftFunctorAdd' C a b 0 h).inv.app X ≫ (shiftFunctorZero C A).hom.app X) =
    F.map ((shiftFunctorAdd' C a b 0 h).hom.app X) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫
          (shiftFunctorAdd' D a b 0 h).inv.app (F.obj X) ≫ (shiftFunctorZero D A).hom.app (F.obj X)
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
⊢ -(CategoryTheory.shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁ = 0 ∧
      T.mor₁ = 0 ↔
    T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
simp only [neg_eq_zero, IsIso.comp_right_eq_zero, Functor.map_eq_zero_iff]

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
⊢ T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case negSucc.zero
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
⊢ H (Int.negSucc 0)

Tactic:
exact H_neg_one

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
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : Mono f
X : C
g : X ⟶ X✝
h : Y✝ ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk g f h ∈ distinguishedTriangles
⊢ (Triangle.mk g f h).mor₁ ≫ 𝟙 (Triangle.mk g f h).obj₂ = 0

Tactic:
Triangle.mor₁_eq_zero_of_mono₂ _ hT hf,

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
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : Mono f
X : C
g : X ⟶ X✝
h : Y✝ ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk g f h ∈ distinguishedTriangles
⊢ 0 ≫ 𝟙 (Triangle.mk g f h).obj₂ = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T ∈ distinguishedTriangles C → T.rotate ∈ distinguishedTriangles C

Tactic:
exact rotate_distinguished_triangle' T

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

Goal state before:
pp: 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✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasZeroObject E
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : Preadditive E
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
⊢ ∀ (X₁ X₃ : C), IsIso (prodComparison F X₁ X₃)

Tactic:
intro X₁

Goal state after:
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✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasZeroObject E
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : Preadditive E
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
X₁ : C
⊢ ∀ (X₃ : C), IsIso (prodComparison F X₁ X₃)
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: case refine_1
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
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ (shiftFunctor C 1).map v₁₃ = (shiftFunctor C 1).map v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ : (shiftFunctor C 1).map v₁₃ ≫ (shiftFunctor C 1).map u₁₂ = o.m₃ ≫ (shiftFunctor C 1).map v₂₃
⊢ (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₂ ≫
      (shiftFunctor C (-1)).map (o.m₁ ≫ (shiftFunctor C 1).map v₁₃) ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X₁ =
    v₁₂

Tactic:
eq₂,

Goal state after:
case refine_1
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
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ (shiftFunctor C 1).map v₁₃ = (shiftFunctor C 1).map v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ : (shiftFunctor C 1).map v₁₃ ≫ (shiftFunctor C 1).map u₁₂ = o.m₃ ≫ (shiftFunctor C 1).map v₂₃
⊢ (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₂ ≫
      (shiftFunctor C (-1)).map ((shiftFunctor C 1).map v₁₂) ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X₁ =
    v₁₂
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case refine_1
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
X : C
⊢ G₁.obj { as := { obj := X } } = G₂.obj { as := { obj := X } }

Tactic:
apply Functor.congr_obj h

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

Goal state before:
pp: case refine_1.mk
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
obj✝ : C
⊢ (Quotient.functor (relations W) ⋙ G₁).obj { obj := obj✝ } = (Quotient.functor (relations W) ⋙ G₂).obj { obj := obj✝ }

Tactic:
apply Functor.congr_obj h

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

Goal state before:
pp: case refine_2.inr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
hw' : G₁.map (wIso w hw✝).hom = eqToHom ⋯ ≫ G₂.map (wIso w hw✝).hom ≫ eqToHom ⋯
⊢ (Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) =
    eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inr ⟨w, hw✝⟩)) ≫ eqToHom ⋯

Tactic:
refine Functor.congr_inv_of_congr_hom _ _ _ ?_ ?_ hw'

Goal state after:
case refine_2.inr.refine_1
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
hw' : G₁.map (wIso w hw✝).hom = eqToHom ⋯ ≫ G₂.map (wIso w hw✝).hom ≫ eqToHom ⋯
⊢ G₁.obj (W.Q.obj Y) = G₂.obj (W.Q.obj Y)

case refine_2.inr.refine_2
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
hw' : G₁.map (wIso w hw✝).hom = eqToHom ⋯ ≫ G₂.map (wIso w hw✝).hom ≫ eqToHom ⋯
⊢ G₁.obj (W.Q.obj X) = G₂.obj (W.Q.obj X)
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case refine_2.inr.refine_1
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : { obj := Y }.obj ⟶ { obj := X }.obj
hw✝ : W w
hw : W.Q.map w = (wIso w hw✝).hom
hw' : G₁.map (wIso w hw✝).hom = eqToHom ⋯ ≫ G₂.map (wIso w hw✝).hom ≫ eqToHom ⋯
⊢ G₁.obj (W.Q.obj Y) = G₂.obj (W.Q.obj Y)

Tactic:
apply Functor.congr_obj h

Goal state after: