mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case refine_2.refine_2
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
x✝ : ↥(KaehlerDifferential.ideal R S)
hx : x✝ ∈ Submodule.restrictScalars S (KaehlerDifferential.ideal R S • ⊤)
x y : ↥(KaehlerDifferential.ideal R S)
ex : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) x = 0
ey : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) y = 0
⊢ 0 + 0 = 0

Tactic:
zero_add

Goal state after:
case refine_2.refine_2
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
x✝ : ↥(KaehlerDifferential.ideal R S)
hx : x✝ ∈ Submodule.restrictScalars S (KaehlerDifferential.ideal R S • ⊤)
x y : ↥(KaehlerDifferential.ideal R S)
ex : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) x = 0
ey : (D.tensorProductTo ∘ₗ ↑S (Submodule.subtype (KaehlerDifferential.ideal R S))) y = 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map ((add hF s i a b).hom.app X) =
    (i (a + b)).hom.app X ≫
      (shiftFunctorAdd D a b).hom.app (F.obj X) ≫ (shiftFunctor D b).map ((i a).inv.app X) ≫ (i b).inv.app ((s a).obj X)

Tactic:
dsimp [add]

Goal state after:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map
      (hF.preimage
        ((i (a + b)).hom.app X ≫
          (shiftFunctorAdd D a b).hom.app (F.obj X) ≫
            𝟙 ((shiftFunctor D b).obj ((shiftFunctor D a).obj (F.obj X))) ≫
              (shiftFunctor D b).map ((i a).inv.app X) ≫
                𝟙 ((shiftFunctor D b).obj (F.obj ((s a).obj X))) ≫
                  (i b).inv.app ((s a).obj X) ≫ 𝟙 (F.obj ((s b).obj ((s a).obj X))))) =
    (i (a + b)).hom.app X ≫
      (shiftFunctorAdd D a b).hom.app (F.obj X) ≫ (shiftFunctor D b).map ((i a).inv.app X) ≫ (i b).inv.app ((s a).obj X)
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map ((add hF s i a b).inv.app X) =
    (i b).hom.app ((s a).obj X) ≫
      (shiftFunctor D b).map ((i a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (i (a + b)).inv.app X

Tactic:
dsimp [add]

Goal state after:
C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
a b : A
X : C
⊢ F.map
      (hF.preimage
        ((((((𝟙 (F.obj ((s b).obj ((s a).obj X))) ≫ (i b).hom.app ((s a).obj X)) ≫
                  𝟙 ((shiftFunctor D b).obj (F.obj ((s a).obj X)))) ≫
                (shiftFunctor D b).map ((i a).hom.app X)) ≫
              𝟙 ((shiftFunctor D b).obj ((shiftFunctor D a).obj (F.obj X)))) ≫
            (shiftFunctorAdd D a b).inv.app (F.obj X)) ≫
          (i (a + b)).inv.app X)) =
    (i b).hom.app ((s a).obj X) ≫
      (shiftFunctor D b).map ((i a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (i (a + b)).inv.app X
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝³ : Category.{v, u} C
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F : C ⥤ D
hF : F.FullyFaithful
s : A → C ⥤ C
i : (i : A) → s i ⋙ F ≅ F ⋙ shiftFunctor D i
m₁ m₂ m₃ : A
X : C
⊢ F.map ((add hF s i (m₁ + m₂) m₃).hom.app X ≫ (s m₃).map ((add hF s i m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯ ≫ (add hF s i m₁ (m₂ + m₃)).hom.app X ≫ (add hF s i m₂ m₃).hom.app ((s m₁).obj X))

Tactic:
have h := shiftFunctorAdd'_assoc_hom_app m₁ m₂ m₃ _ _ (m₁ + m₂ + m₃) rfl rfl rfl (F.obj X)
        simp only [shiftFunctorAdd'_eq_shiftFunctorAdd] at h
        rw [← cancel_mono ((i m₃).hom.app ((s m₂).obj ((s m₁).obj X)))]
        simp only [Functor.comp_obj, Functor.map_comp, map_add_hom_app,
          Category.assoc, Iso.inv_hom_id_app_assoc, NatTrans.naturality_assoc, Functor.comp_map,
          Iso.inv_hom_id_app, Category.comp_id]
        erw [(i m₃).hom.naturality]
        rw [Functor.comp_map, map_add_hom_app,
          Functor.map_comp, Functor.map_comp, Iso.inv_hom_id_app_assoc,
          ← Functor.map_comp_assoc _ ((i (m₁ + m₂)).inv.app X), Iso.inv_hom_id_app,
          Functor.map_id, Category.id_comp, reassoc_of% h,
          dcongr_arg (fun a => (i a).hom.app X) (add_assoc m₁ m₂ m₃)]
        simp [shiftFunctorAdd', eqToHom_map]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
inst✝ : Category.{v_3, u_3} C₃
W : MorphismProperty C₁
F : C₁ ⥤ C₂
G : C₂ ⥤ C₃
⊢ (W.map F).IsInvertedBy G ↔ W.IsInvertedBy (F ⋙ G)

Tactic:
simp only [IsInvertedBy.iff_map_le_isomorphisms, map_map]

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 E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ g.f i = 0 + g.f i

Tactic:
zero_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 : C ⟶ D
h : Homotopy f g
i : ι
⊢ g.f i = g.f i
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✝ : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i j : ι
w : ¬c.Rel j i
⊢ 0 + 0 = 0

Tactic:
zero_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✝ : ι
e f g : C ⟶ D
h : Homotopy e f
k : Homotopy f g
i j : ι
w : ¬c.Rel j 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 E : HomologicalComplex V c
f✝ g✝ : C ⟶ D
h✝ k : D ⟶ E
i✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i : ι
⊢ (e ≫ g).f i = (((dNext i) fun i j ↦ h.hom i j ≫ g.f j) + (prevD i) fun i j ↦ h.hom i j ≫ g.f j) + (f ≫ g).f i

Tactic:
comp_f,

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✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i : ι
⊢ e.f i ≫ g.f i = (((dNext i) fun i j ↦ h.hom i j ≫ g.f j) + (prevD i) fun i j ↦ h.hom i j ≫ g.f j) + (f ≫ g).f i
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✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i : ι
⊢ ((dNext i) h.hom + (prevD i) h.hom) ≫ g.f i + f.f i ≫ g.f i =
    (dNext i) h.hom ≫ g.f i + (prevD i) h.hom ≫ g.f i + (f ≫ g).f i

Tactic:
comp_f,

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✝ : ι
e f : C ⟶ D
h : Homotopy e f
g : D ⟶ E
i : ι
⊢ ((dNext i) h.hom + (prevD i) h.hom) ≫ g.f i + f.f i ≫ g.f i =
    (dNext i) h.hom ≫ g.f i + (prevD i) h.hom ≫ g.f i + f.f i ≫ g.f i
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).f i = (((dNext i) fun i j ↦ e.f i ≫ h.hom i j) + (prevD i) fun i j ↦ e.f i ≫ h.hom i j) + (e ≫ g).f i

Tactic:
comp_f,

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 ≫ f.f i = (((dNext i) fun i j ↦ e.f i ≫ h.hom i j) + (prevD i) fun i j ↦ e.f i ≫ h.hom i j) + (e ≫ g).f i
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 + g.f i) = e.f i ≫ (dNext i) h.hom + e.f i ≫ (prevD i) h.hom + (e ≫ g).f i

Tactic:
comp_f,

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 + (prevD i) h.hom + 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.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
⊢ (if hij : c.Rel i j then
        (if hj : c.Rel j (c.next j) then -fstX φ i j hij ≫ F.d j (c.next j) ≫ inlX φ (c.next j) j hj else 0) +
            fstX φ i j hij ≫ φ.f j ≫ inrX φ j +
          sndX φ i ≫ G.d i j ≫ inrX φ j
      else 0) ≫
      sndX φ j =
    fstX φ i j hij ≫ φ.f j + sndX φ i ≫ G.d i j

Tactic:
split_ifs with hij <;> simp

Goal state after:
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
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ (φ ≫ inr φ).f j = φ.f j ≫ inrX φ j

Tactic:
comp_f,

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 K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ φ.f j ≫ (inr φ).f j = φ.f j ≫ inrX φ j
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
⊢ 0 + hom k₀ k₁ ≫ D.d k₁ k₀ = hom k₀ k₁ ≫ D.d k₁ k₀

pp: case a
ι : 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
⊢ ¬c.Rel k₀ (c.next k₀)

Tactic:
zero_add

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
⊢ hom k₀ k₁ ≫ D.d k₁ k₀ = hom k₀ k₁ ≫ D.d k₁ k₀

case a
ι : 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
⊢ ¬c.Rel k₀ (c.next k₀)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
α β : Cochain F G n
h : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ (δ n m (α + β)).v p q hpq = (δ n m α).v p q hpq + (δ n m β).v p q hpq

Tactic:
simp only [δ_v n m h _ p q hpq _ _ rfl rfl, Cochain.add_v, add_comp, comp_add, smul_add]

Goal state after:
case pos
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
α β : Cochain F G n
h : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ α.v p (q - 1) ⋯ ≫ G.d (q - 1) q + β.v p (q - 1) ⋯ ≫ G.d (q - 1) q +
      (m.negOnePow • F.d p (p + 1) ≫ α.v (p + 1) q ⋯ + m.negOnePow • F.d p (p + 1) ≫ β.v (p + 1) q ⋯) =
    α.v p (q - 1) ⋯ ≫ G.d (q - 1) q + m.negOnePow • F.d p (p + 1) ≫ α.v (p + 1) q ⋯ +
      (β.v p (q - 1) ⋯ ≫ G.d (q - 1) q + m.negOnePow • F.d p (p + 1) ≫ β.v (p + 1) q ⋯)
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 φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
p q : ℤ
hpq : p + 1 = q
⊢ q + -1 = p

Tactic:
omega

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 φ
K L : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
n' m' : ℤ
α' : Cochain F L m'
β' : Cochain G L n'
h : n + 1 = m
h' : m' + 1 = n'
p : ℤ
hp : n + n' = p
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + n' = p₃
q : ℤ
hq : p₁ + m = q
⊢ q + m' = p₃

Tactic:
omega

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 φ
K L : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
α' : Cochain F L (-1)
β' : G ⟶ L
eq' : δ (-1) 0 α' = Cochain.ofHom (φ ≫ β')
n n' : ℤ
hnn' : n + 1 = n'
⊢ n' + -1 = n

Tactic:
omega

Goal state after:
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F G : Quotient r ⥤ D
τ₁ τ₂ : F ⟶ G
h : (functor r).whiskerLeft τ₁ = (functor r).whiskerLeft τ₂
⊢ τ₁.app = τ₂.app

Tactic:
ext1 ⟨X⟩; exact NatTrans.congr_app h X

Goal state after:
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), -a + a = 0

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

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
n : A
⊢ s (0 + n) = 𝟭 D ⋙ s n

Tactic:
zero_add

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
n : A
⊢ s n = 𝟭 D ⋙ s n
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
⊢ rightUnshift 0 n hn' = 0

Tactic:
change (rightShiftAddEquiv K L n a n' hn').symm 0 = 0

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn').symm 0 = 0
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
⊢ (-γ).rightShift a n' hn' = -γ.rightShift a n' hn'

Tactic:
change rightShiftAddEquiv K L n a n' hn' (-γ) = _
  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 + γ₂.rightUnshift n hn

Tactic:
apply map_add

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 + γ₂.leftUnshift n hn

Tactic:
apply map_add

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₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F₁.CommShift A
inst✝¹ : F₂.CommShift A
inst✝ : CommShift τ A
a : A
X : C
⊢ τ.app ((shiftFunctor C a).obj X) =
    (Functor.commShiftIso F₁ a).hom.app X ≫ (shiftFunctor D a).map (τ.app X) ≫ (Functor.commShiftIso F₂ a).inv.app X

Tactic:
by
  simp [shift_app_comm_assoc τ a X]

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

Goal state before:
pp: case pos
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
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'

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

Tactic:
· 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]

Goal state after:
case neg
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
⊢ δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (δ n m γ).rightShift a m' hm'
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
⊢ (a * n' + a * (a - 1) / 2).negOnePow = a.negOnePow * (a * m' + a * (a - 1) / 2).negOnePow

Tactic:
← 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
⊢ (a * n' + a * (a - 1) / 2).negOnePow = a.negOnePow * (a * (n' + 1) + a * (a - 1) / 2).negOnePow
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
J : Type u_1
inst✝ : Category.{v_1, u_1} J
A B : J ⥤ Triangle C
iso₁ : A ⋙ π₁ ≅ B ⋙ π₁
iso₂ : A ⋙ π₂ ≅ B ⋙ π₂
iso₃ : A ⋙ π₃ ≅ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ iso₂.hom = iso₁.hom ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ iso₃.hom = iso₂.hom ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight iso₁.hom (shiftFunctor C 1) = iso₃.hom ≫ B.whiskerLeft π₃Toπ₁
⊢ B.whiskerLeft π₁Toπ₂ ≫ iso₂.inv = iso₁.inv ≫ A.whiskerLeft π₁Toπ₂

Tactic:
by simp only [← cancel_epi iso₁.hom, ← reassoc_of% comm₁,
          Iso.hom_inv_id, comp_id, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a m : ℤ
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ m.negOnePow • a.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯ =
    a.negOnePow • m.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯

Tactic:
smul_comm

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a m : ℤ
hnm : n + 1 = m
p q : ℤ
hpq : p + m = q
⊢ a.negOnePow • m.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯ =
    a.negOnePow • m.negOnePow • K.d (p + a) (p + 1 + a) ≫ γ.v (p + 1 + a) (q + a) ⋯