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
F G : CochainComplex C ℤ
n : ℤ
z₁ z₂ : Cochain F G n
h : ∀ (p q : ℤ) (hpq : p + n = q), z₁.v p q hpq = z₂.v p q hpq
⊢ z₁ = z₂

Tactic:
funext ⟨p, q, hpq⟩
  apply h

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ inlX φ j i hij ≫ d φ i j = -F.d j k ≫ inlX φ k j hjk + φ.f j ≫ inrX φ j

Tactic:
apply ext_to_X φ j k hjk
  · simp [d_fstX φ _ _ _ hij hjk]
  · simp [d_sndX φ _ _ hij]

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 : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
k : R
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ (k • z₁).comp z₂ h = k • z₁.comp z₂ h

Tactic:
ext p q hpq
  simp only [comp_v _ _ h p _ q rfl (by lia), smul_v, Linear.smul_comp]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
j : ι
hj : ¬c.Rel j (c.next j)
⊢ (desc φ α hα).f j = sndX φ j ≫ α.f j

Tactic:
apply dif_neg hj

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ φ ≫ inr φ ≫ f = (φ ≫ inr φ) ≫ f

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
α : G ⟶ K
hα : Homotopy (φ ≫ α) 0
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ 0 ≫ f = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K✝ : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
K : HomologicalComplex C c
hc : ∀ (j : ι), ∃ i, c.Rel i j
f : homotopyCofiber φ ⟶ K
⊢ φ ≫ inr φ ≫ f = (φ ≫ inr φ) ≫ f

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K✝ : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
K : HomologicalComplex C c
hc : ∀ (j : ι), ∃ i, c.Rel i j
f : homotopyCofiber φ ⟶ K
⊢ 0 ≫ f = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
φ : F ⟶ G
⊢ δ 0 1 (Cochain.ofHom φ) = 0

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G 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 φ'
⊢ Arrow.Hom.left α ≫ 0 = 0

Tactic:
by simp

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

Tactic:
rw [← h₂₃, ← h₁₂, ← h, add_comm m, add_assoc, neg_add_cancel_left]

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 : ℤ
⊢ ↑0 = 0

Tactic:
by simp

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 : ℤ
⊢ ∀ (x y : Cocycle K L n), ↑(x + y) = ↑x + ↑y

Tactic:
by simp

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 : CochainComplex C ℤ
f₁ f₂ : mappingCone φ ⟶ K
γ₁ : Cochain F K (-2)
γ₂ : Cochain G K (-1)
h₁ :
  (inl φ).comp (Cochain.ofHom f₁) ⋯ = δ (-2) (-1) γ₁ + (Cochain.ofHom φ).comp γ₂ ⋯ + (inl φ).comp (Cochain.ofHom f₂) ⋯
h₂ : Cochain.ofHom (inr φ ≫ f₁) = δ (-1) 0 γ₂ + Cochain.ofHom (inr φ ≫ f₂)
⊢ -2 + 1 = -1

Tactic:
by simp

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 n : ℤ
z : Cocycle G K n
f : F ⟶ G
⊢ δ n (n + 1) ((Cochain.ofHom f).comp ↑z ⋯) = 0

Tactic:
by simp

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 n : ℤ
z : Cocycle F G n
f : G ⟶ K
⊢ δ n (n + 1) ((↑z).comp (Cochain.ofHom f) ⋯) = 0

Tactic:
by simp

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

Tactic:
simp only [δ_liftCochain φ α β h (m + 1) rfl, eq,
      Cocycle.δ_eq_zero, Cochain.zero_comp, neg_zero, add_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 φ
K : CochainComplex C ℤ
α : Cocycle K F 1
β : Cochain K G 0
eq : δ 0 1 β + (↑α).comp (Cochain.ofHom φ) ⋯ = 0
⊢ (Cochain.ofHom (lift φ α β eq)).comp ↑(fst φ) ⋯ = ↑α

Tactic:
by simp

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

Tactic:
by simp

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 φ
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
⊢ (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (descCochain φ α' β' h').v p₂ p₃ h₂₃ =
    α.v p₁ q hq ≫ α'.v q p₃ ⋯ + β.v p₁ p₂ h₁₂ ≫ β'.v p₂ p₃ h₂₃

Tactic:
by
  have eq := Cochain.congr_v (liftCochain_descCochain φ α β α' β' h h' p hp) p₁ p₃ (by lia)
  simpa only [Cochain.comp_v _ _ hp p₁ p₂ p₃ h₁₂ h₂₃, Cochain.add_v,
    Cochain.comp_v _ _ _ _ _ _ hq (show q + m' = p₃ by lia)] using eq

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 ι
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 : ι
⊢ biprod.lift (𝟙 K) (-𝟙 K) ≫ biprod.fst = (biprod.inl - biprod.inr) ≫ biprod.fst

Tactic:
by simp

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 m : ℤ
hnm : n + 1 = m
⊢ ((↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n m ⋯ ≫ H.map ((inl φ).v m n ⋯) +
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯ ≫ H.map ((inr φ).f n)) ≫
      (H.map ((↑(fst φ)).v n m ⋯) ≫ (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v m n ⋯ +
        H.map ((snd φ).v n n ⋯) ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n) =
    𝟙 ((mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).X n)

Tactic:
by
    simp only [Functor.mapHomologicalComplex_obj_X, comp_add, add_comp, assoc,
      ← H.map_comp_assoc, inl_v_fst_v, CategoryTheory.Functor.map_id, id_comp, inr_f_fst_v,
      inl_v_snd_v, inr_f_snd_v]
    simp [ext_from_iff _ _ _ hnm]

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 ι
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 : ι
⊢ biprod.lift (𝟙 K) (-𝟙 K) ≫ biprod.snd = (biprod.inl - biprod.inr) ≫ biprod.snd

Tactic:
by simp

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 : ι
C D E : HomologicalComplex V c
⊢ 𝟙 C ≫ 𝟙 C = 𝟙 C

Tactic:
by simp

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
g : C ⟶ D
e : HomotopyEquiv C D
hfg : Homotopy e.hom g
⊢ (e.copy hfg).hom = g

Tactic:
by simp

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
X✝ Y✝ : Quotient r
f : Hom r X✝ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as),
    comp r (Quot.mk (HomRel.CompClosure r) (𝟙 X✝.as)) (Quot.mk (HomRel.CompClosure r) a) =
      Quot.mk (HomRel.CompClosure r) a

Tactic:
by simp

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
X✝ Y✝ : Quotient r
f : Hom r X✝ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as),
    comp r (Quot.mk (HomRel.CompClosure r) a) (Quot.mk (HomRel.CompClosure r) (𝟙 Y✝.as)) =
      Quot.mk (HomRel.CompClosure r) a

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ ι₀ K ≫ π K = 𝟙 K

Tactic:
by simp

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
W✝ X✝ Y✝ Z✝ : Quotient r
f : Hom r W✝ X✝
g : Hom r X✝ Y✝
h : Hom r Y✝ Z✝
⊢ ∀ (a : Y✝.as ⟶ Z✝.as) (a_1 : X✝.as ⟶ Y✝.as) (a_2 : W✝.as ⟶ X✝.as),
    comp r (comp r (Quot.mk (HomRel.CompClosure r) a_2) (Quot.mk (HomRel.CompClosure r) a_1))
        (Quot.mk (HomRel.CompClosure r) a) =
      comp r (Quot.mk (HomRel.CompClosure r) a_2)
        (comp r (Quot.mk (HomRel.CompClosure r) a_1) (Quot.mk (HomRel.CompClosure r) a))

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ ι₀ K = ι₁ K ≫ π K ≫ ι₀ K

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝³ : HasHomotopyCofiber φ
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ ι₁ K ≫ 𝟙 K.cylinder = ι₁ K

Tactic:
by simp

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
L : C ⥤ D
inst✝ : L.Full
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
by simp

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
L : C ⥤ D
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
by simp

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
L : C ⥤ D
inst✝ : L.EssSurj
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
by simp

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
L : C ⥤ D
inst✝¹ : L.Full
inst✝ : L.EssSurj
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), L.homRel f₁ f₂ → L.map f₁ = L.map f₂

Tactic:
by simp

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

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D E : HomotopyCategory V c
f : C ⟶ D
g : D ⟶ E
⊢ (quotient V c).map (Quot.out f ≫ Quot.out g) = f ≫ g

Tactic:
by simp

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

Goal state before:
pp: C : Type u_3
D : Type u_1
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_2
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
X : C
h :
  F.whiskerLeft (zero F s i).hom =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom
⊢ (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).hom.app X =
    (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)

Tactic:
by simp

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

Goal state before:
pp: C : Type u_2
D : Type u_1
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_3
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
X : C
h :
  F.whiskerLeft (zero F s i).inv =
    (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv
⊢ (i 0 ≪≫ isoWhiskerRight (shiftFunctorZero C A) F ≪≫ F.leftUnitor ≪≫ F.rightUnitor.symm).inv.app X =
    F.map ((shiftFunctorZero C A).inv.app X) ≫ (i 0).inv.app X

Tactic:
by simp

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

Goal state before:
pp: C : Type u_3
D : Type u_1
inst✝⁵ : Category.{v_1, u_3} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_2
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
a b : A
X : C
h :
  F.whiskerLeft (add F s i a b).hom =
    (i (a + b) ≪≫
        isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
          (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫
            (shiftFunctor C a).isoWhiskerLeft (i b).symm ≪≫
              ((shiftFunctor C a).associator F (s b)).symm ≪≫
                isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).hom
⊢ (i (a + b) ≪≫
            isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
              (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫
                (shiftFunctor C a).isoWhiskerLeft (i b).symm ≪≫
                  ((shiftFunctor C a).associator F (s b)).symm ≪≫
                    isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).hom.app
      X =
    (i (a + b)).hom.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)

Tactic:
by simp

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

Goal state before:
pp: C : Type u_2
D : Type u_1
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Category.{v_2, u_1} D
F : C ⥤ D
A : Type u_3
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
a b : A
X : C
h :
  F.whiskerLeft (add F s i a b).inv =
    (i (a + b) ≪≫
        isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
          (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫
            (shiftFunctor C a).isoWhiskerLeft (i b).symm ≪≫
              ((shiftFunctor C a).associator F (s b)).symm ≪≫
                isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).inv
⊢ (i (a + b) ≪≫
            isoWhiskerRight (shiftFunctorAdd C a b) F ≪≫
              (shiftFunctor C a).associator (shiftFunctor C b) F ≪≫
                (shiftFunctor C a).isoWhiskerLeft (i b).symm ≪≫
                  ((shiftFunctor C a).associator F (s b)).symm ≪≫
                    isoWhiskerRight (i a).symm (s b) ≪≫ F.associator (s a) (s b)).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

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
n i i' : ℤ
hi : n + i = i'
⊢ ∀ {X Y : CochainComplex C ℤ} (f : X ⟶ Y),
    (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n ⋙ eval C (ComplexShape.up ℤ) i).map f ≫ (XIsoOfEq Y ⋯).hom =
      (XIsoOfEq X ⋯).hom ≫ (eval C (ComplexShape.up ℤ) i').map f

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
n : ℤ
K : HomologicalComplex C (ComplexShape.up ℤ)
⊢ ∀ (i j : ℤ),
    (ComplexShape.up ℤ).Rel i j →
      (Iso.refl
              (((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙
                        F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                    K).X
                i)).hom ≫
          ((F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ shiftFunctor (HomologicalComplex D (ComplexShape.up ℤ)) n).obj
                K).d
            i j =
        ((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙ F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                K).d
            i j ≫
          (Iso.refl
              (((shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) n ⋙
                        F.mapHomologicalComplex (ComplexShape.up ℤ)).obj
                    K).X
                j)).hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ A.mor₁ ≫ (asIso f.hom₂).hom = (asIso f.hom₁).hom ≫ B.mor₁

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ A.mor₂ ≫ (asIso f.hom₃).hom = (asIso f.hom₂).hom ≫ B.mor₂

Tactic:
by simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
f : A ⟶ B
h₁ : IsIso f.hom₁
h₂ : IsIso f.hom₂
h₃ : IsIso f.hom₃
⊢ A.mor₃ ≫ (shiftFunctor C 1).map (asIso f.hom₁).hom = (asIso f.hom₃).hom ≫ B.mor₃

Tactic:
by simp

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 M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = ((a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯).v p q hpq

Tactic:
have h' : n' + m = t' := by lia

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
m t t' : ℤ
γ' : Cochain L M m
h : n + m = t
ht' : t + a = t'
p q : ℤ
hpq : p + t' = q
h' : n' + m = t'
⊢ ((γ.comp γ' h).leftShift a t' ht').v p q hpq = ((a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯).v p q hpq
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
a b : A
ha : CommShiftCore τ a
hb : CommShiftCore τ b
⊢ (Functor.commShiftIso F₁ (a + b)).hom ≫ Functor.whiskerRight τ (shiftFunctor D (a + b)) =
    (shiftFunctor C (a + b)).whiskerLeft τ ≫ (Functor.commShiftIso F₂ (a + b)).hom

Tactic:
ext X
    have := (shiftFunctorAdd D a b).inv.naturality (τ.app X)
    dsimp at this ⊢
    simp only [Functor.commShiftIso_add, Functor.CommShift.isoAdd_hom_app,
      ← NatTrans.naturality_2 τ ((shiftFunctorAdd C a b).app X),
      Functor.comp_obj, hb.app_shift_assoc, ha.app_shift, assoc,
      (shiftFunctor D b).map_comp_assoc]
    simp [← Functor.map_comp_assoc, this]

Goal state after: