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

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ 𝟙 A ≫ f ≫ 𝟙 B = f

Tactic:
comp_id,

Goal state after:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
A B : V
f : A ⟶ B
⊢ 𝟙 A ≫ f = f
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
φ : C ⟶ (single₀ V).obj X
⊢ C.d 1 0 ≫ φ.f 0 = 0

Tactic:
← φ.comm 1 0,

Goal state after:
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
inst✝ : HasZeroObject V
C : ChainComplex V ℕ
X : V
φ : C ⟶ (single₀ V).obj X
⊢ φ.f 1 ≫ ((single₀ V).obj X).d 1 0 = 0
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
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
a : S
⊢ D a - a • D 1 = D a

Tactic:
D.map_one_eq_zero,

Goal state after:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
M : Type u_1
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
D : Derivation R S M
a : S
⊢ D a - a • 0 = D a
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X✝ : α → V
d_X : (n : α) → X✝ n ⟶ X✝ (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y✝ : α → V
d_Y : (n : α) → Y✝ n ⟶ Y✝ (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
X Y : CochainComplex V α
f : (i : α) → X.X i ⟶ Y.X i
comm : ∀ (i : α), f i ≫ Y.d i (i + 1) = X.d i (i + 1) ≫ f (i + 1)
n m : α
⊢ (ComplexShape.up α).Rel n m → f n ≫ Y.d n m = X.d n m ≫ f m

Tactic:
simp only [ComplexShape.up_Rel]
    rintro rfl
    simpa using comm n

Goal state after:
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
inst✝ : EssFiniteType R S
⊢ (ideal R S).FG

Tactic:
use (EssFiniteType.finset R S).image (fun s ↦ (1 : S) ⊗ₜ[R] s - s ⊗ₜ[R] (1 : S))

Goal state after:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : EssFiniteType R S
⊢ Ideal.span ↑(Finset.image (fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) (EssFiniteType.finset R S)) = ideal R S
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
⊢ (derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S) = (kerTotal R S).mkQ

Tactic:
apply Finsupp.lhom_ext

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ ∀ (a b : S), ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)) (single a b) = b𝖣a
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: case pos
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
inst✝ : K.HasHomology i
hij : c.Rel i j
⊢ K.iCycles i ≫ K.d i j = 0

Tactic:
obtain rfl := c.next_eq' hij
    exact (K.sc i).iCycles_g

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a.tmul.add
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
r : B
f✝ g✝ : A →₀ A
a✝¹ : r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) f✝)) = 0
a✝ : r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) g✝)) = 0
⊢ r • (map R A B B) ((map R R A B) ((linearCombination A ⇑(D R A)) (f✝ + g✝))) = 0

Tactic:
simp [smul_add, *]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
A : C
i : ι
f g : (K ⊞ L).X i ⟶ A
h₁ : biprod.inl.f i ≫ f = biprod.inl.f i ≫ g
h₂ : biprod.inr.f i ≫ f = biprod.inr.f i ≫ g
⊢ f = g

Tactic:
simp [biprodX_ext_from_iff, h₁, h₂]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case e'_3
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
⊢ (map R A B B).ker = Submodule.map (linearCombination B ⇑(D R B)) (kerTotal A B)

pp: case a.convert_2
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
⊢ Submodule.map (linearCombination B ⇑(D R B)) (kerTotal A B) ≤ (mapBaseChange R A B).range

Tactic:
· rw [KaehlerDifferential.ker_map]
      congr 1
      convert! Submodule.comap_id _
      · ext; simp

Goal state after:
case a.convert_2
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
⊢ Submodule.map (linearCombination B ⇑(D R B)) (kerTotal A B) ≤ (mapBaseChange R A B).range
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✝ : ι
f g : D ⟶ E
h : Homotopy f g
e : C ⟶ D
i : ι
⊢ e.f i ≫ ((dNext i) h.hom + (prevD i) h.hom) + e.f i ≫ g.f i =
    e.f i ≫ (dNext i) h.hom + e.f i ≫ (prevD i) h.hom + e.f i ≫ g.f i

Tactic:
Preadditive.comp_add

Goal state after:
ι : 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✝ : ι
f g : D ⟶ E
h : Homotopy f g
e : C ⟶ D
i : ι
⊢ e.f i ≫ (dNext i) h.hom + e.f i ≫ (prevD i) h.hom + e.f i ≫ g.f i =
    e.f i ≫ (dNext i) h.hom + e.f i ≫ (prevD i) h.hom + e.f i ≫ g.f i
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₂ : ℤ
hq₂ : p + 1 = q₂
hq₁ : p + n = q - 1
⊢ (δ n m z).v p q hpq = z.v p (p + n) ⋯ ≫ G.d (p + n) q + m.negOnePow • F.d p q₂ ≫ z.v q₂ q ⋯

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

Goal state after:
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
hq₁ : p + n = q - 1
hq₂ : p + 1 = p + m - n
⊢ (δ n m z).v p q hpq = z.v p (p + n) ⋯ ≫ G.d (p + n) q + m.negOnePow • F.d p (p + m - n) ≫ z.v (p + m - n) 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₀ : ι
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]
  rw [dNext_eq hom r₁₀, prevD, AddMonoidHom.mk'_apply, D.shape, comp_zero, add_zero]
  exact hk₁ _

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 : ℤ
r : R
z : Cocycle F G n
⊢ r • ↑z ∈ cocycle F G n

Tactic:
by
    have hz := z.2
    rw [mem_iff n (n + 1) rfl] at hz ⊢
    simp only [δ_smul, hz, smul_zero]

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 φ
p q : ℤ
hpq : p + 1 = q
⊢ (↑(fst φ)).v p q hpq ≫ (inl φ).v q p ⋯ + (snd φ).v p p ⋯ ≫ (inr φ).f p = 𝟙 ((mappingCone φ).X p)

Tactic:
simpa only [Cochain.add_v, Cochain.comp_zero_cochain_v, Cochain.ofHom_v, id_f,
    Cochain.comp_v _ _ (add_neg_cancel 1) p q p hpq (by lia)]
    using Cochain.congr_v (id φ) p p (add_zero p)

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 φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ (inl φ).v i j hij ≫ (mappingCone φ).d j i = φ.f i ≫ (inr φ).f i - F.d i k ≫ (inl φ).v k i hik

Tactic:
dsimp [mappingCone, inl, inr]
  rw [homotopyCofiber.inlX_d φ j i k (by dsimp; lia) (by dsimp; lia)]
  abel

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
      (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1) =
    ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
      (mapHomologicalComplexXIso φ H (n + 1)).hom

Tactic:
ext_to_iff _ _ (n + 2) (by lia),

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ ((mapHomologicalComplexXIso φ H n).hom ≫
          (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1)) ≫
        (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
          (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
          (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    ((mapHomologicalComplexXIso φ H n).hom ≫
          (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1)) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯ =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯
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
p' : ℤ
hp' : p' + n = q
⊢ (γ.leftShift a n' hn').v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p p' ⋯).hom ≫ γ.v p' q hp'

Tactic:
by
  obtain rfl : p' = p + a := by lia
  dsimp only [leftShift]
  simp only [mk_v]

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 ℤ
a n' : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ ((γ.leftUnshift n hn').leftShift a n' hn').v p q hpq = γ.v p q hpq

Tactic:
(γ.leftUnshift n hn').leftShift_v a n' hn' p q hpq (q - n) (by lia),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
a n' : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ (a * n' + a * (a - 1) / 2).negOnePow •
      (K.shiftFunctorObjXIso a p (q - n) ⋯).hom ≫ (γ.leftUnshift n hn').v (q - n) q ⋯ =
    γ.v p q hpq
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
⊢ ((γ₁ + γ₂).leftShift a n' hn').v p q hpq = (γ₁.leftShift a n' hn').v p q hpq + (γ₂.leftShift a n' hn').v p q hpq

Tactic:
simp only [leftShift_v _ a n' hn' p q hpq (p + a) (by lia), add_v, comp_add, smul_add]

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

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
this : HasShift D A := HasShift.induced F A s i
a b : A
X : C
⊢ (i (a + b)).inv.app X = (isoAdd (i a).symm (i b).symm).hom.app X

Tactic:
simp only [isoAdd_hom_app, Iso.symm_hom, shiftFunctorAdd_inv_app_obj_of_induced,
          shiftFunctor_of_induced]

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
this : HasShift D A := HasShift.induced F A s i
a b : A
X : C
⊢ (i (a + b)).inv.app X =
    F.map ((shiftFunctorAdd C a b).hom.app X) ≫
      (i b).inv.app ((shiftFunctor C a).obj X) ≫
        (s b).map ((i a).inv.app X) ≫
          (s b).map ((i a).hom.app X) ≫
            (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X
Module: Mathlib.CategoryTheory.Triangulated.Rotate

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
X : C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
⊢ (invRotate C).IsEquivalence

Tactic:
by
  change (triangleRotation C).inverse.IsEquivalence
  infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ u₁₃ ≫ 𝟙 X₃ = u₁₂ ≫ u₂₃

Tactic:
comp_id,

Goal state after:
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
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ u₁₃ = u₁₂ ≫ u₂₃
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
h₁ : T.mor₁ = 0
h₃ : T.mor₃ = 0
this : Epi T.mor₂
f : T.obj₃ ⟶ T.obj₂
hf : 𝟙 T.obj₂ = T.mor₂ ≫ f
⊢ T.mor₂ ≫ f ≫ T.mor₂ = T.mor₂ ≫ 𝟙 T.obj₃

Tactic:
comp_id,

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.mor₁ = 0
h₃ : T.mor₃ = 0
this : Epi T.mor₂
f : T.obj₃ ⟶ T.obj₂
hf : 𝟙 T.obj₂ = T.mor₂ ≫ f
⊢ T.mor₂ ≫ f ≫ T.mor₂ = 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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
n : ℤ
H : ℤ → Prop := fun n ↦ ∀ T ∈ distinguishedTriangles, (shiftFunctor C n).obj T ∈ distinguishedTriangles
H_zero : H 0
H_one : H 1
⊢ H n

Tactic:
have H_neg_one : H (-1) := fun T hT =>
    isomorphic_distinguished _ (inv_rot_of_distTriang _
      (inv_rot_of_distTriang _ (inv_rot_of_distTriang _ hT))) _
        ((invRotateInvRotateInvRotateIso C).symm.app T)

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
n : ℤ
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 n
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
      (desc (inr φ) 0 (triangle φ).mor₃ ⋯ ≫
        lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 ⋯) (-(inl φ).leftShift 1 0 ⋯) ⋯) =
    δ (-1) 0 (-(snd (inr φ)).comp ((snd φ).comp (inl (inr φ)) ⋯) ⋯) + Cochain.ofHom (𝟙 (mappingCone (inr φ)))

Tactic:
by
      ext n
      -- the following list of lemmas has been obtained by doing
      -- simp? [ext_to_iff _ _ (n + 1) rfl, ext_from_iff _ (n + 1) _ rfl,
      --   δ_zero_cochain_comp _ _ _ (neg_add_cancel 1),
      --   (inl φ).leftShift_v 1 0 (neg_add_cancel 1) n n (add_zero n) (n + 1) (by lia),
      --   (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) n (n + 1) rfl (n + 1) (by lia),
      --   Cochain.comp_v _ _ (add_neg_cancel 1) n (n + 1) n rfl (by lia)]
      simp only [Int.reduceNeg, Cochain.ofHom_comp, ofHom_desc, ofHom_lift, Cocycle.coe_neg,
        Cocycle.leftShift_coe, Cocycle.ofHom_coe, Cochain.comp_zero_cochain_v,
        shiftFunctor_obj_X', δ_neg, δ_zero_cochain_comp _ _ _ (neg_add_cancel 1), δ_inl,
        Int.negOnePow_neg, Int.negOnePow_one, δ_snd, Cochain.neg_comp,
        Cochain.comp_assoc_of_second_is_zero_cochain, smul_neg, Units.neg_smul, one_smul,
        neg_neg, Cochain.comp_add, inr_snd_assoc, neg_add_rev, Cochain.add_v, Cochain.neg_v,
        Cochain.comp_v _ _ (add_neg_cancel 1) n (n + 1) n rfl (by lia),
        Cochain.zero_cochain_comp_v, Cochain.ofHom_v, HomologicalComplex.id_f,
        ext_to_iff _ _ (n + 1) rfl, assoc, liftCochain_v_fst_v,
        (Cochain.ofHom φ).leftShift_v 1 1 (zero_add 1) n (n + 1) rfl (n + 1) (by lia),
        shiftFunctor_obj_X, mul_one, sub_self, mul_zero, Int.zero_ediv, add_zero,
        shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, id_comp,
        Preadditive.add_comp, Preadditive.neg_comp, inl_v_fst_v, comp_id, inr_f_fst_v, comp_zero,
        neg_zero, neg_add_cancel_comm, ext_from_iff _ (n + 1) _ rfl, inl_v_descCochain_v_assoc,
        Cochain.zero_v, zero_comp, Preadditive.comp_neg, inl_v_snd_v_assoc,
        inr_f_descCochain_v_assoc, inr_f_snd_v_assoc, inl_v_triangle_mor₃_f_assoc, triangle_obj₁,
        Iso.refl_inv, inl_v_fst_v_assoc, inr_f_triangle_mor₃_f_assoc, inr_f_fst_v_assoc, and_self,
        liftCochain_v_snd_v,
        (inl φ).leftShift_v 1 0 (neg_add_cancel 1) n n (add_zero n) (n + 1) (by lia),
        Int.negOnePow_zero, inl_v_snd_v, inr_f_snd_v, zero_add, inl_v_descCochain_v,
        inr_f_descCochain_v, inl_v_triangle_mor₃_f, inr_f_triangle_mor₃_f, neg_add_cancel]

Goal state after:
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
⊢ (-(CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
          ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ)) ≫
      𝟙
        ((CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).obj
          ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)) =
    ((Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).inv.app K ≫
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (rotateHomotopyEquiv φ).hom) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle (inr φ)).mor₃ ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app L

Tactic:
comp_id,

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
⊢ -(CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ) =
    ((Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).inv.app K ≫
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (rotateHomotopyEquiv φ).hom) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle (inr φ)).mor₃ ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app L
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✝ : F.Faithful
X Y : Triangle C
f g : X ⟶ Y
h : F.mapTriangle.map f = F.mapTriangle.map g
⊢ f = g

Tactic:
by
    ext <;> apply F.map_injective
    · exact congr_arg TriangleMorphism.hom₁ h
    · exact congr_arg TriangleMorphism.hom₂ h
    · exact congr_arg TriangleMorphism.hom₃ h

Goal state after: