mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℤ
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ q - n + n = q

Tactic:
sub_add_cancel

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 : ℤ
z : Cochain F G n
p q : ℤ
hpq : p + m = q
⊢ q = q
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₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁

Tactic:
dsimp only [nullHomotopicMap]

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₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (dNext k₁) hom + (prevD k₁) hom = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ 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₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (dNext k₁) hom + (prevD k₁) hom = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁

Tactic:
rw [dNext_eq hom r₁₀, prevD_eq hom r₂₁]

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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₀ = hom k₀ k₁ ≫ D.d k₁ k₀

Tactic:
dsimp only [nullHomotopicMap]

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
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (dNext k₀) hom + (prevD k₀) hom = hom k₀ k₁ ≫ 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₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁

Tactic:
dsimp only [nullHomotopicMap]

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₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (dNext k₁) hom + (prevD k₁) hom = C.d k₁ k₀ ≫ hom k₀ k₁
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 n₂ : ℤ
z₁ : Cochain F G 0
z₂ : Cochain G K n₂
m₂ : ℤ
h₂ : n₂ + 1 = m₂
⊢ 1 + n₂ = m₂

Tactic:
add_comm,

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 n₂ : ℤ
z₁ : Cochain F G 0
z₂ : Cochain G K n₂
m₂ : ℤ
h₂ : n₂ + 1 = m₂
⊢ n₂ + 1 = m₂
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
F' F'' G' G'' : HomologicalComplex C c
φ' : F' ⟶ G'
φ'' : F'' ⟶ G''
inst✝¹ : HasHomotopyCofiber φ'
inst✝ : HasHomotopyCofiber φ''
H : ∀ (j : ι), ∃ i, c.Rel i j
α : Arrow.mk φ ≅ Arrow.mk φ'
⊢ mapArrowHom φ' φ H α.inv ≫ mapArrowHom φ φ' H α.hom = 𝟙 (homotopyCofiber φ')

Tactic:
by rw [← mapArrowHom_comp, Iso.inv_hom_id, mapArrowHom_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
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
⊢ (single f n).v p q hpq = f

Tactic:
dsimp [single]
  rw [if_pos, id_comp, comp_id]
  tauto

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

Goal state before:
pp: case neg
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:
rw [single_v_eq_zero', single_v_eq_zero', zero_comp]

Goal state after:
case neg.hq'
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
⊢ q'' ≠ q'

case neg.hq'
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
⊢ q'' - 1 ≠ q
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P Q : Quotient r
iZ : Zero (P ⟶ Q) := { zero := Quot.mk (HomRel.CompClosure r) 0 }
iA : Add (P ⟶ Q) := { add := Preadditive.add r hr }
iN : Neg (P ⟶ Q) := { neg := Preadditive.neg r hr }
⊢ ∀ (a : P ⟶ Q), 0 + a = a

Tactic:
by rintro ⟨_⟩; exact congr_arg (functor r).map (zero_add _)

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 : HomologicalComplex C c
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✝⁴ : ∀ (i : ι), HasBinaryBiproduct (F.X i) (F.X i)
inst✝³ : HasHomotopyCofiber (biprod.lift (𝟙 F) (-𝟙 F))
inst✝² :
  ∀ (i : ι), HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i) (((H.mapHomologicalComplex c).obj F).X i)
inst✝¹ :
  HasHomotopyCofiber (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ (H.mapHomologicalComplex c).map (ι₁ F) ≫ (mapHomologicalComplexObjIso F H hc).hom =
    ι₁ ((H.mapHomologicalComplex c).obj F)

Tactic:
dsimp [mapHomologicalComplexObjIso, ι₁, homotopyCofiber.mapArrowHom]

Goal state after:
C : Type u_1
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F : HomologicalComplex C c
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✝⁴ : ∀ (i : ι), HasBinaryBiproduct (F.X i) (F.X i)
inst✝³ : HasHomotopyCofiber (biprod.lift (𝟙 F) (-𝟙 F))
inst✝² :
  ∀ (i : ι), HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i) (((H.mapHomologicalComplex c).obj F).X i)
inst✝¹ :
  HasHomotopyCofiber (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ (H.mapHomologicalComplex c).map (biprod.inr ≫ homotopyCofiber.inr (biprod.lift (𝟙 F) (-𝟙 F))) ≫
      (homotopyCofiber.mapHomologicalComplexObjIso (biprod.lift (𝟙 F) (-𝟙 F)) H).hom ≫
        homotopyCofiber.desc ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))
          (biprod.lift ((H.mapHomologicalComplex c).map biprod.fst) ((H.mapHomologicalComplex c).map biprod.snd) ≫
            homotopyCofiber.inr
              (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F))))
          ((Homotopy.ofEq ⋯).trans
            (((homotopyCofiber.inrCompHomotopy
                      (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))
                      hc).compLeft
                  (𝟙 ((H.mapHomologicalComplex c).obj F))).trans
              (Homotopy.ofEq ⋯))) =
    biprod.inr ≫
      homotopyCofiber.inr (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))
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 M : CochainComplex C ℤ
n✝ : ℤ
γ✝ γ₁ γ₂ : Cochain K L n✝
n a n' : ℤ
hn : n + a = n'
x : R
γ : Cochain K L n
⊢ (leftShiftAddEquiv K L n a n' hn) (x • γ) = x • (leftShiftAddEquiv K L n a n' hn) γ

Tactic:
dsimp; simp only [leftShift_smul]

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₃ : Triangle C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
f : T₁ ⟶ T₂
⊢ -f + f = 0

Tactic:
ext <;> apply neg_add_cancel

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' m' : ℤ
hn' : n' + a = n
m : ℤ
hm' : m' + a = m
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

Tactic:
by_cases hnm : n + 1 = m
  · have hnm' : n' + 1 = m' := by lia
    ext p q hpq
    dsimp
    rw [(δ n m γ).rightShift_v a m' hm' p q hpq _ rfl,
      δ_v n m hnm _ p (p + m) rfl (p + n) (p + 1) (by lia) rfl,
      δ_v n' m' hnm' _ p q hpq (p + n') (p + 1) (by lia) rfl,
      γ.rightShift_v a n' hn' p (p + n') rfl (p + n) rfl,
      γ.rightShift_v a n' hn' (p + 1) q _ (p + m) (by lia)]
    simp only [shiftFunctorObjXIso, shiftFunctor_obj_d',
      Linear.comp_units_smul, assoc, HomologicalComplex.XIsoOfEq_inv_comp_d,
      add_comp, HomologicalComplex.d_comp_XIsoOfEq_inv, Linear.units_smul_comp, smul_add,
      add_right_inj, smul_smul]
    simp only [← hm', add_comm m', Int.negOnePow_add, ← mul_assoc,
      Int.units_mul_self, one_mul]
  · have hnm' : ¬ n' + 1 = m' := fun _ => hnm (by lia)
    rw [δ_shape _ _ hnm', δ_shape _ _ hnm, rightShift_zero, smul_zero]

Goal state after:
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
n : ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₁)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₂)
          (n.negOnePow •
            (CategoryTheory.shiftFunctor C n).map X✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app X✝.obj₁)).mor₁ ≫
      (CategoryTheory.shiftFunctor C n).map f.hom₂ =
    (CategoryTheory.shiftFunctor C n).map f.hom₁ ≫
      (mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₁)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₂)
          (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₃ ≫ (shiftFunctorComm C 1 n).hom.app Y✝.obj₁)).mor₁

Tactic:
dsimp
        simp only [Linear.units_smul_comp, Linear.comp_units_smul, ← Functor.map_comp, f.comm₁]

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

Goal state before:
pp: case pos.e_a.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ m'.negOnePow * ((a * n' + a * (a - 1) / 2).negOnePow * a.negOnePow) =
    a.negOnePow * ((a * m' + a * (a - 1) / 2).negOnePow * m.negOnePow)

Tactic:
simp only [← Int.negOnePow_add, ← hn', ← hm', ← hnm]

Goal state after:
case pos.e_a.e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
hnm : n + 1 = m
hnm' : n' + 1 = m'
p q : ℤ
hpq : p + m' = q
⊢ (n + 1 + a + (a * (n + a) + a * (a - 1) / 2 + a)).negOnePow =
    (a + (a * (n + 1 + a) + a * (a - 1) / 2 + (n + 1))).negOnePow
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 : ℤ), (shiftFunctor C n).Additive
T : Triangle C
⊢ ((-(shiftFunctor C (-1)).map T.mor₃ ≫
            (shiftFunctorAdd' C 1 (-1) 0 ⋯).inv.app T.obj₁ ≫ (shiftFunctorZero C ℤ).hom.app T.obj₁) ≫
        (shiftFunctorZero C ℤ).inv.app T.obj₁ ≫ (shiftFunctorAdd' C (-1) 1 0 ⋯).hom.app T.obj₁) ≫
      (shiftFunctor C 1).map (𝟙 ((shiftFunctor C (-1)).obj T.obj₁)) =
    𝟙 ((shiftFunctor C (-1)).obj T.obj₃) ≫
      ((-1).negOnePow • (shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorComm C 1 (-1)).hom.app T.obj₁)

Tactic:
simp [shiftFunctorComm_eq C _ _ _ (add_neg_cancel (1 : ℤ))]

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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
h : IsZero T.obj₂
⊢ T.rotate ∈ distinguishedTriangles ↔ IsIso T.mor₃

Tactic:
distinguished_iff_of_isZero₁ _ h

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
h : IsZero T.obj₂
⊢ IsIso T.rotate.mor₂ ↔ IsIso T.mor₃
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 : Triangle C
hT : T ∈ distinguishedTriangles
hT₀ : T.mor₃ = 0
inr : T.obj₃ ⟶ T.obj₂
inr_snd : inr ≫ T.mor₂ = 𝟙 T.obj₃
fst : T.obj₂ ⟶ T.obj₁
total : fst ≫ T.mor₁ + T.mor₂ ≫ inr = 𝟙 T.obj₂
this : Mono T.mor₁
eq : fst ≫ T.mor₁ = 𝟙 T.obj₂ - T.mor₂ ≫ inr
⊢ T.mor₁ ≫ fst = 𝟙 T.obj₁

Tactic:
simp only [← cancel_mono T.mor₁, assoc, id_comp, eq, comp_sub, comp_id,
            comp_distTriang_mor_zero₁₂_assoc _ hT, zero_comp, sub_zero]

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

Goal state before:
pp: case h₀
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 : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
d : BinaryBiproductData T.obj₁ T.obj₃ := ⋯
⊢ (T.mor₁ ≫ (biprod.uniqueUpToIso T.obj₁ T.obj₃ d.isBilimit).hom) ≫ biprod.fst = biprod.inl ≫ biprod.fst

Tactic:
simpa [d] using d.bicone.inl_fst

Goal state after:
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 ((shiftFunctor C 1).map v₁₃)) ≫
        (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X₁ =
    v₁₂

Tactic:
rw [← Functor.map_comp, eq₂, shiftFunctorCompIsoId_naturality_1]

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

Goal state before:
pp: V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp ↦ ihp ≫ Φ.map f.toPath) p
⊢ Φ.map (p.cons f') = Φ.map p ≫ Φ.map f'.toPath

Tactic:
convert! Functor.map_comp Φ p (Quiver.Hom.toPath f')

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

Goal state before:
pp: case h₁
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✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsColimit (ShortComplex.π₁.mapCocone (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))

Tactic:
exact (CokernelCofork.isColimitMapCoconeEquiv _ _).symm
        ((composableArrows₃_exact _ i j hij).exact 1).gIsCokernel

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

Goal state before:
pp: case h₂
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✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsColimit (ShortComplex.π₂.mapCocone (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))

Tactic:
exact (CokernelCofork.isColimitMapCoconeEquiv _ _).symm
        ((composableArrows₃_exact _ i j hij).exact 1).gIsCokernel

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

Goal state before:
pp: case h₃
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✝ j✝ : ι
hij✝ : c.Rel i✝ j✝
hS : S.ShortExact
i j : ι
hij : c.Rel i j
⊢ IsColimit (ShortComplex.π₃.mapCocone (CokernelCofork.ofπ (S.mapNatTrans (natTransHomologyπ C c j)) ⋯))

Tactic:
exact (CokernelCofork.isColimitMapCoconeEquiv _ _).symm
        ((composableArrows₃_exact _ i j hij).exact 1).gIsCokernel

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ e.hom.map (e.inv.map f) = Quiver.homOfEq f ⋯ ⋯

Tactic:
rw [← Prefunctor.comp_map]

Goal state after:
V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ (e.inv ⋙q e.hom).map f = Quiver.homOfEq f ⋯ ⋯
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case mpr
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
P : MorphismProperty W.Localization
inst✝ : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)
X Y : W.Localization
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂ : Paths (LocQuiver W)
p : X₁ ⟶ X₂
⊢ P (G.map p)

Tactic:
induction p with
    | nil => simpa only [Functor.map_id] using! hP₁ (𝟙 X₁.obj)
    | @cons X₂ X₃ p g hp =>
      let p' : X₁ ⟶ X₂ := p
      rw [show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl, G.map_comp]
      refine P.comp_mem _ _ hp ?_
      rcases g with (g | ⟨g, hg⟩)
      · apply hP₁
      · apply hP₂

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows

Goal state before:
pp: case zero
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
this : L.EssSurj
Y : ComposableArrows D 0
⊢ (L.mapComposableArrows 0).essImage Y

Tactic:
obtain ⟨Y, rfl⟩ := mk₀_surjective Y
      exact ⟨mk₀ _, ⟨isoMk₀ (L.objObjPreimageIso Y)⟩⟩

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

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
P : MorphismProperty D
inst✝¹ : P.RespectsIso
inst✝ : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (Construction.wInv f hf) ≫ e.hom.app X

Tactic:
Construction.wInv_eq_isoOfHom_inv,

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
P : MorphismProperty D
inst✝¹ : P.RespectsIso
inst✝ : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X
Module: Mathlib.CategoryTheory.Localization.Predicate

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
h : L.map f = L.map g
⊢ W.Q.map f = W.Q.map g

Tactic:
let e := Localization.compUniqFunctor L W.Q W

Goal state after:
case mpr
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
h : L.map f = L.map g
e : L ⋙ (Localization.uniq L W.Q W).functor ≅ W.Q := Localization.compUniqFunctor L W.Q W
⊢ W.Q.map f = W.Q.map g
Module: Mathlib.CategoryTheory.Shift.Localization

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
⊢ (commShiftOfLocalization.iso L W F F' 0).hom = (CommShift.isoZero F' A).hom

Tactic:
apply natTrans_ext L W

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
⊢ ∀ (X : C), (commShiftOfLocalization.iso L W F F' 0).hom.app (L.obj X) = (CommShift.isoZero F' A).hom.app (L.obj X)