mathlib-initiative/mathlib-tactics huggingface dataset:
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 ℤ
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₃
⊢ (inl φ).v p₁ p₂ h₁₂ ≫ (descCochain φ α β h).v p₂ p₃ h₂₃ = α.v p₁ p₃ ⋯

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
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₃
⊢ (inl φ).v p₁ p₂ h₁₂ ≫ (descCochain φ α β h).v p₂ p₃ h₂₃ = α.v p₁ p₃ ⋯
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 ℤ
n m : ℤ
α : Cochain F K m
β : Cochain G K n
h : m + 1 = n
p₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ (inr φ).f p₁ ≫ (descCochain φ α β h).v p₁ p₂ h₁₂ = β.v p₁ p₂ h₁₂

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
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₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ (inr φ).f p₁ ≫ (descCochain φ α β h).v p₁ p₂ h₁₂ = β.v p₁ p₂ h₁₂
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.up ℕ).Rel ((ComplexShape.up ℕ).prev 0) 0

Tactic:
rw [CochainComplex.prev_nat_zero]

Goal state after:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.up ℕ).Rel 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 : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
⊢ e.f 0 = 0 ≫ dTo Q 0 + dFrom P 0 ≫ (xNextIso P ⋯).hom ≫ zero

Tactic:
simpa using

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 : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
⊢ e.f 0 = P.d 0 1 ≫ zero
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 ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + 1 = p₃
⊢ (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (↑(fst φ)).v p₂ p₃ h₂₃ = α.v p₁ p₃ ⋯

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
p₁ p₂ p₃ : ℤ
h₁₂ : p₁ + n = p₂
h₂₃ : p₂ + 1 = p₃
⊢ (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (↑(fst φ)).v p₂ p₃ h₂₃ = α.v p₁ p₃ ⋯
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 ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
p₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (snd φ).v p₂ p₂ ⋯ = β.v p₁ p₂ h₁₂

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
p₁ p₂ : ℤ
h₁₂ : p₁ + n = p₂
⊢ (liftCochain φ α β h).v p₁ p₂ h₁₂ ≫ (snd φ).v p₂ p₂ ⋯ = β.v p₁ p₂ h₁₂
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
eq : ((liftCochain φ α β h).comp (descCochain φ α' β' h') hp).v p₁ p₃ ⋯ = (α.comp α' ⋯ + β.comp β' ⋯).v p₁ p₃ ⋯
⊢ (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:
simpa using

Goal state after:
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
eq : ((liftCochain φ α β h).comp (descCochain φ α' β' h') hp).v p₁ p₃ ⋯ = (α.comp α' ⋯ + β.comp β' ⋯).v p₁ p₃ ⋯
⊢ (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₂₃
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case e_a.e_a.succ
ι : 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 : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
n✝ : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ (xPrevIso Q ⋯).inv =
    (xNextIso P ⋯).inv ≫
      (mkCoinductiveAux₂ e zero comm_zero one comm_one succ ((ComplexShape.up ℕ).prev (n✝ + 1))).snd.fst

Tactic:
rw [mkCoinductiveAux₃ e zero comm_zero one comm_one succ]

Goal state after:
case e_a.e_a.succ
ι : 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 : ι
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
n✝ : ℕ
⊢ (mkCoinductiveAux₁ e zero one comm_one succ n✝).fst ≫ (xPrevIso Q ⋯).inv =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (n✝ + 1)).fst ≫ (xPrevIso Q ⋯).hom
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
f : HomotopyEquiv C D
g : HomotopyEquiv D E
⊢ Homotopy ((f.hom ≫ g.hom) ≫ g.inv ≫ f.inv) (𝟙 C)

Tactic:
simpa using

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 : ι
C D E : HomologicalComplex V c
f : HomotopyEquiv C D
g : HomotopyEquiv D E
⊢ Homotopy (f.hom ≫ g.hom ≫ g.inv ≫ f.inv) (𝟙 C)
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
f : HomotopyEquiv C D
g : HomotopyEquiv D E
⊢ Homotopy ((g.inv ≫ f.inv) ≫ f.hom ≫ g.hom) (𝟙 E)

Tactic:
simpa using

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 : ι
C D E : HomologicalComplex V c
f : HomotopyEquiv C D
g : HomotopyEquiv D E
⊢ Homotopy (g.inv ≫ f.inv ≫ f.hom ≫ g.hom) (𝟙 E)
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
a b : C
m₁ m₂ : a ⟶ b
h : r m₁ m₂
⊢ CompClosure r m₁ m₂

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
a b : C
m₁ m₂ : a ⟶ b
h : r m₁ m₂
⊢ CompClosure r m₁ m₂
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
a b e : C
f : a ⟶ b
X Y c d : C
h₁ h₂ : c ⟶ d
h : r h₁ h₂
g : b ⟶ c
i : d ⟶ e
⊢ CompClosure r (f ≫ g ≫ h₁ ≫ i) (f ≫ g ≫ h₂ ≫ i)

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
a b e : C
f : a ⟶ b
X Y c d : C
h₁ h₂ : c ⟶ d
h : r h₁ h₂
g : b ⟶ c
i : d ⟶ e
⊢ CompClosure r (f ≫ g ≫ h₁ ≫ i) (f ≫ g ≫ h₂ ≫ i)
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
a d e : C
g : d ⟶ e
X Y b c : C
g₁ g₂ : b ⟶ c
h : r g₁ g₂
f : a ⟶ b
i : c ⟶ d
⊢ CompClosure r ((f ≫ g₁ ≫ i) ≫ g) ((f ≫ g₂ ≫ i) ≫ g)

Tactic:
simpa using

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
a d e : C
g : d ⟶ e
X Y b c : C
g₁ g₂ : b ⟶ c
h : r g₁ g₂
f : a ⟶ b
i : c ⟶ d
⊢ CompClosure r (f ≫ g₁ ≫ i ≫ g) (f ≫ g₂ ≫ i ≫ g)
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ _root_.Equivalence (HomRel.CompClosure r)

Tactic:
simpa using

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ _root_.Equivalence r
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:
by ext1 ⟨X⟩; exact NatTrans.congr_app h X

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 : HomologicalComplex V c
f : C ⟶ D
h : (quotient V c).map f = 0
⊢ (quotient V c).map f = (quotient V c).map 0

Tactic:
simpa using

Goal state after:
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
h : (quotient V c).map f = 0
⊢ (quotient V c).map f = 0
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 : HomologicalComplex V c
f : C ⟶ D
x✝ : Nonempty (Homotopy f 0)
h : Homotopy f 0
⊢ (quotient V c).map f = 0

Tactic:
simpa using

Goal state after:
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
x✝ : Nonempty (Homotopy f 0)
h : Homotopy f 0
⊢ (quotient V c).map f = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: case mpr
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
h : Homotopy (𝟙 C) 0
⊢ 𝟙 ((quotient V c).obj C) = 0

Tactic:
simpa using

Goal state after:
case mpr
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
h : Homotopy (𝟙 C) 0
⊢ 𝟙 ((quotient V c).obj C) = 0
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
m₁ m₂ m₃ : A
this :
  (Induced.add F s i (m₁ + m₂) m₃).hom ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
    eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom
X : D
⊢ (Induced.add F s i (m₁ + m₂) m₃).hom.app X ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app X) =
    eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom.app X ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj X)

Tactic:
simpa using

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
m₁ m₂ m₃ : A
this :
  (Induced.add F s i (m₁ + m₂) m₃).hom ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
    eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom
X : D
⊢ (Induced.add F s i (m₁ + m₂) m₃).hom.app X ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app X) =
    eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom.app X ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj X)
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
K L : CochainComplex C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
⊢ φ₁.f (i + n) =
    (n.negOnePow • K.d (i + n) (i + 1 + n)) ≫ (n.negOnePow • h.hom (i + 1 + n) (i + n)) +
        (n.negOnePow • h.hom (i + n) (i - 1 + n)) ≫ (n.negOnePow • L.d (i - 1 + n) (i + n)) +
      φ₂.f (i + n)

Tactic:
simpa using

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K L : CochainComplex C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i : ℤ
⊢ φ₁.f (i + n) =
    K.d (i + n) (i + 1 + n) ≫ h.hom (i + 1 + n) (i + n) + h.hom (i + n) (i - 1 + n) ≫ L.d (i - 1 + n) (i + n) +
      φ₂.f (i + n)
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
this : (Induced.add F s i 0 n).hom = eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n)
X : D
⊢ (Induced.add F s i 0 n).hom.app X = eqToHom ⋯ ≫ (s n).map ((Induced.zero F s i).inv.app X)

Tactic:
simpa using

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
this : (Induced.add F s i 0 n).hom = eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n)
X : D
⊢ (Induced.add F s i 0 n).hom.app X = eqToHom ⋯ ≫ (s n).map ((Induced.zero F s i).inv.app X)
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
this : (Induced.add F s i n 0).hom = eqToHom ⋯ ≫ (s n).whiskerLeft (Induced.zero F s i).inv
X : D
⊢ (Induced.add F s i n 0).hom.app X = eqToHom ⋯ ≫ (Induced.zero F s i).inv.app ((s n).obj X)

Tactic:
simpa using

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
this : (Induced.add F s i n 0).hom = eqToHom ⋯ ≫ (s n).whiskerLeft (Induced.zero F s i).inv
X : D
⊢ (Induced.add F s i n 0).hom.app X = eqToHom ⋯ ≫ (Induced.zero F s i).inv.app ((s n).obj X)
Module: Mathlib.CategoryTheory.Shift.CommShift

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
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a : A
X : C
h :
  ((whiskeringRight C D E).obj G).map (iso e a).hom =
    ((shiftFunctor C a).associator F G ≪≫
        (shiftFunctor C a).isoWhiskerLeft e ≪≫
          commShiftIso H a ≪≫
            isoWhiskerRight e.symm (shiftFunctor E a) ≪≫
              F.associator G (shiftFunctor E a) ≪≫
                F.isoWhiskerLeft (commShiftIso G a).symm ≪≫ (F.associator (shiftFunctor D a) G).symm).hom
⊢ G.map ((iso e a).hom.app X) =
    e.hom.app ((shiftFunctor C a).obj X) ≫
      (commShiftIso H a).hom.app X ≫ (shiftFunctor E a).map (e.inv.app X) ≫ (commShiftIso G a).inv.app (F.obj X)

Tactic:
simpa using

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a : A
X : C
h :
  ((whiskeringRight C D E).obj G).map (iso e a).hom =
    ((shiftFunctor C a).associator F G ≪≫
        (shiftFunctor C a).isoWhiskerLeft e ≪≫
          commShiftIso H a ≪≫
            isoWhiskerRight e.symm (shiftFunctor E a) ≪≫
              F.associator G (shiftFunctor E a) ≪≫
                F.isoWhiskerLeft (commShiftIso G a).symm ≪≫ (F.associator (shiftFunctor D a) G).symm).hom
⊢ G.map ((iso e a).hom.app X) =
    e.hom.app ((shiftFunctor C a).obj X) ≫
      (commShiftIso H a).hom.app X ≫ (shiftFunctor E a).map (e.inv.app X) ≫ (commShiftIso G a).inv.app (F.obj X)
Module: Mathlib.CategoryTheory.Shift.CommShift

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
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a : A
X : C
h :
  ((whiskeringRight C D E).obj G).map (iso e a).inv =
    ((shiftFunctor C a).associator F G ≪≫
        (shiftFunctor C a).isoWhiskerLeft e ≪≫
          commShiftIso H a ≪≫
            isoWhiskerRight e.symm (shiftFunctor E a) ≪≫
              F.associator G (shiftFunctor E a) ≪≫
                F.isoWhiskerLeft (commShiftIso G a).symm ≪≫ (F.associator (shiftFunctor D a) G).symm).inv
⊢ G.map ((iso e a).inv.app X) =
    (commShiftIso G a).hom.app (F.obj X) ≫
      (shiftFunctor E a).map (e.hom.app X) ≫ (commShiftIso H a).inv.app X ≫ e.inv.app ((shiftFunctor C a).obj X)

Tactic:
simpa using

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁷ : G.Full
inst✝⁶ : G.Faithful
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : G.CommShift A
inst✝ : H.CommShift A
a : A
X : C
h :
  ((whiskeringRight C D E).obj G).map (iso e a).inv =
    ((shiftFunctor C a).associator F G ≪≫
        (shiftFunctor C a).isoWhiskerLeft e ≪≫
          commShiftIso H a ≪≫
            isoWhiskerRight e.symm (shiftFunctor E a) ≪≫
              F.associator G (shiftFunctor E a) ≪≫
                F.isoWhiskerLeft (commShiftIso G a).symm ≪≫ (F.associator (shiftFunctor D a) G).symm).inv
⊢ G.map ((iso e a).inv.app X) =
    (commShiftIso G a).hom.app (F.obj X) ≫
      (shiftFunctor E a).map (e.hom.app X) ≫ (commShiftIso H a).inv.app X ≫ e.inv.app ((shiftFunctor C a).obj X)
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
c : (contractibleTriangle T.obj₁).obj₃ ⟶ T.obj₃
hc :
  (contractibleTriangle T.obj₁).mor₂ ≫ c = T.mor₁ ≫ T.mor₂ ∧
    (contractibleTriangle T.obj₁).mor₃ ≫ (shiftFunctor C 1).map (𝟙 T.obj₁) = c ≫ T.mor₃
⊢ T.mor₁ ≫ T.mor₂ = 0

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
c : (contractibleTriangle T.obj₁).obj₃ ⟶ T.obj₃
hc :
  (contractibleTriangle T.obj₁).mor₂ ≫ c = T.mor₁ ≫ T.mor₂ ∧
    (contractibleTriangle T.obj₁).mor₃ ≫ (shiftFunctor C 1).map (𝟙 T.obj₁) = c ≫ T.mor₃
⊢ T.mor₁ ≫ T.mor₂ = 0
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
H : T ∈ distinguishedTriangles
H₂ : T.rotate.rotate ∈ distinguishedTriangles
⊢ T.mor₃ ≫ (shiftFunctor C 1).map T.mor₁ = 0

Tactic:
simpa using

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
H : T ∈ distinguishedTriangles
H₂ : T.rotate.rotate ∈ distinguishedTriangles
⊢ T.mor₃ ≫ (shiftFunctor C 1).map T.mor₁ = 0