mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℤ
⊢ n + 1 + 1 = n + 2

Tactic:
by lia

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

Goal state before:
pp: case e_a
ι : 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''
i : ℕ
⊢ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (fromNext i) fun i j ↦
      if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst else 0

Tactic:
·

Goal state after:
case e_a
ι : 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''
i : ℕ
⊢ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (fromNext i) fun i j ↦
      if h : j + 1 = i then (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).snd.fst else 0
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case pos
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∃ k, c.Rel j k
⊢ inrX K j ≫
      (Homotopy.nullHomotopicMap' fun i j hij ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ biprod.snd.f i ≫ inlX K i j hij).f
        j =
    inrX K j ≫ ((π K).f j ≫ (ι₀ K).f j - 𝟙 (homotopyCofiber.X (biprod.lift (𝟙 K) (-𝟙 K)) j))

pp: case neg
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ¬∃ k, c.Rel j k
⊢ inrX K j ≫
      (Homotopy.nullHomotopicMap' fun i j hij ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ biprod.snd.f i ≫ inlX K i j hij).f
        j =
    inrX K j ≫ ((π K).f j ≫ (ι₀ K).f j - 𝟙 (homotopyCofiber.X (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
·

Goal state after:
case pos
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∃ k, c.Rel j k
⊢ inrX K j ≫
      (Homotopy.nullHomotopicMap' fun i j hij ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ biprod.snd.f i ≫ inlX K i j hij).f
        j =
    inrX K j ≫ ((π K).f j ≫ (ι₀ K).f j - 𝟙 (homotopyCofiber.X (biprod.lift (𝟙 K) (-𝟙 K)) j))
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h : ¬p'' = p
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h : ¬p'' = p
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
⊢ m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    m.negOnePow • (single (K.d p' p ≫ f) m).v p'' q'' hpq''

Tactic:
·

Goal state after:
case e_a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
⊢ m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    m.negOnePow • (single (K.d p' p ≫ f) m).v p'' q'' hpq''
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case pos.h₀
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inl ≫ (K.biprodXIso K j).inv ≫ ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ (ι₀ K).f j - inrX K j)

pp: case h₁
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inr ≫ (K.biprodXIso K j).inv ≫ ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ (ι₀ K).f j - inrX K j)

Tactic:
·

Goal state after:
case pos.h₀
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inl ≫ (K.biprodXIso K j).inv ≫ ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ (ι₀ K).f j - inrX K j)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
h : q'' = q
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''

pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
h : ¬q'' = q
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''

Tactic:
·

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
h : q'' = q
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case h₁
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inr ≫ (K.biprodXIso K j).inv ≫ ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ (ι₀ K).f j - inrX K j)

Tactic:
·

Goal state after:
case h₁
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
k : ι
hjk : c.Rel j k
⊢ biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inr ≫ (K.biprodXIso K j).inv ≫ ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ (ι₀ K).f j - inrX K j)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
h : p'' = p'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''

pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
h : ¬p'' = p'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''

Tactic:
·

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
h : p'' = p'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p n q' p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
hp' : p'' + 1 = p
⊢ p = p'' + 1

Tactic:
by lia

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

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
h : ¬p'' = p'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
h : ¬p'' = p'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''
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 ι
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ¬∃ k, c.Rel j k
⊢ inrX K j ≫
      (Homotopy.nullHomotopicMap' fun i j hij ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ biprod.snd.f i ≫ inlX K i j hij).f
        j =
    inrX K j ≫ ((π K).f j ≫ (ι₀ K).f j - 𝟙 (homotopyCofiber.X (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
·

Goal state after:
case neg
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ¬∃ k, c.Rel j k
⊢ inrX K j ≫
      (Homotopy.nullHomotopicMap' fun i j hij ↦
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ biprod.snd.f i ≫ inlX K i j hij).f
        j =
    inrX K j ≫ ((π K).f j ≫ (ι₀ K).f j - 𝟙 (homotopyCofiber.X (biprod.lift (𝟙 K) (-𝟙 K)) j))
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
h : ¬q'' = q
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
h : ¬q'' = q
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
h : ¬q'' = q
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''

Tactic:
· simp [single_v_eq_zero' _ _ _ _ _ h]

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

Goal state before:
pp: case neg.h₀
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j)

pp: case h₁
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j)

Tactic:
·

Goal state after:
case neg.h₀
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j)
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case pos
ι✝ : 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 : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel (c.prev i) i
⊢ (ho.hom (c.prev i) (c.prev (c.prev i)) ≫ L.d (c.prev (c.prev i)) (c.prev i)) ≫ ((shortComplexFunctor C c i).obj L).f =
    0

pp: case neg
ι✝ : 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 : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : ¬c.Rel (c.prev i) i
⊢ (f.f (c.prev i) - g.f (c.prev i) - K.d (c.prev i) i ≫ ho.hom i (c.prev i)) ≫ ((shortComplexFunctor C c i).obj L).f = 0

Tactic:
·

Goal state after:
case pos
ι✝ : 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 : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel (c.prev i) i
⊢ (ho.hom (c.prev i) (c.prev (c.prev i)) ≫ L.d (c.prev (c.prev i)) (c.prev i)) ≫ ((shortComplexFunctor C c i).obj L).f =
    0
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: case right
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 : ℤ
⊢ (H.map ((↑(fst φ)).v n (n + 1) ⋯) ≫ (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) n ⋯ +
        H.map ((snd φ).v n n ⋯) ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n) ≫
      ((↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
          ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ).f (n + 1) +
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯ ≫
          ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj G).d n (n + 1)) =
    ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
      (H.map ((↑(fst φ)).v (n + 1) (n + 2) ⋯) ≫
            (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 2) (n + 1) ⋯ +
          H.map ((snd φ).v (n + 1) (n + 1) ⋯) ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f (n + 1)) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯

Tactic:
·

Goal state after:
case right
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 : ℤ
⊢ (H.map ((↑(fst φ)).v n (n + 1) ⋯) ≫ (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) n ⋯ +
        H.map ((snd φ).v n n ⋯) ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n) ≫
      ((↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
          ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ).f (n + 1) +
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v n n ⋯ ≫
          ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj G).d n (n + 1)) =
    ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
      (H.map ((↑(fst φ)).v (n + 1) (n + 2) ⋯) ≫
            (inl ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 2) (n + 1) ⋯ +
          H.map ((snd φ).v (n + 1) (n + 1) ⋯) ≫ (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f (n + 1)) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯
Module: Mathlib.Algebra.Homology.HomotopyCofiber

Goal state before:
pp: case h₁
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j)

Tactic:
·

Goal state after:
case h₁
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 : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
F G K : CochainComplex C ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
Φ : C ⥤ D
inst✝ : Φ.Additive
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
by lia

Goal state after: