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

Goal state before:
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 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
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 ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : n + 1 = m
⊢ δ n m (z.map Φ) = (δ n m z).map Φ

pp: case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : ¬n + 1 = m
⊢ δ n m (z.map Φ) = (δ n m z).map Φ

Tactic:
·

Goal state after:
case pos
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : n + 1 = m
⊢ δ n m (z.map Φ) = (δ n m z).map Φ
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 ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : ¬n + 1 = m
⊢ δ n m (z.map Φ) = (δ n m z).map Φ

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
K L : CochainComplex C ℤ
n m : ℤ
D : Type u_2
inst✝² : Category.{v_1, u_2} D
inst✝¹ : Preadditive D
z : Cochain K L n
Φ : C ⥤ D
inst✝ : Φ.Additive
hnm : ¬n + 1 = m
⊢ δ n m (z.map Φ) = (δ n m z).map Φ
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 i (c.next i)
⊢ ((shortComplexFunctor C c i).obj K).g ≫ K.d (c.next i) (c.next (c.next i)) ≫ ho.hom (c.next (c.next i)) (c.next i) = 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 i (c.next i)
⊢ ((shortComplexFunctor C c i).obj K).g ≫ (f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i)) = 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 i (c.next i)
⊢ ((shortComplexFunctor C c i).obj K).g ≫ K.d (c.next i) (c.next (c.next i)) ≫ ho.hom (c.next (c.next i)) (c.next i) = 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
i : ι
hi : c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

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
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

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
i : ι
hi : c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
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 i (c.next i)
⊢ ((shortComplexFunctor C c i).obj K).g ≫ (f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i)) = 0

Tactic:
·

Goal state after:
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 i (c.next i)
⊢ ((shortComplexFunctor C c i).obj K).g ≫ (f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i)) = 0
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
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i

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
i : ι
hi : ¬c.Rel i (c.next i)
⊢ (nullHomotopicMap K).f i = (π K ≫ ι₀ K - 𝟙 K.cylinder).f i
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
⊢ f.f (c.prev i) =
    K.d (c.prev i) i ≫ ho.hom i (c.prev i) +
        ho.hom (c.prev i) (c.prev (c.prev i)) ≫ L.d (c.prev (c.prev i)) (c.prev i) +
      g.f (c.prev i)

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) =
    K.d (c.prev i) i ≫ ho.hom i (c.prev i) +
        (f.f (c.prev i) - g.f (c.prev i) - K.d (c.prev i) i ≫ ho.hom i (c.prev i)) +
      g.f (c.prev i)

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
⊢ f.f (c.prev i) =
    K.d (c.prev i) i ≫ ho.hom i (c.prev i) +
        ho.hom (c.prev i) (c.prev (c.prev i)) ≫ L.d (c.prev (c.prev i)) (c.prev i) +
      g.f (c.prev i)
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
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) =
    K.d (c.prev i) i ≫ ho.hom i (c.prev i) +
        (f.f (c.prev i) - g.f (c.prev i) - K.d (c.prev i) i ≫ ho.hom i (c.prev i)) +
      g.f (c.prev i)

Tactic:
·

Goal state after:
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) =
    K.d (c.prev i) i ≫ ho.hom i (c.prev i) +
        (f.f (c.prev i) - g.f (c.prev i) - K.d (c.prev i) i ≫ ho.hom i (c.prev i)) +
      g.f (c.prev i)
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: case h_obj
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
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ ∀ (X : Quotient r), Φ.obj X = (lift r (functor r ⋙ Φ) H).obj X

pp: case h_map
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
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ ∀ (X Y : Quotient r) (f : X ⟶ Y), Φ.map f ≍ (lift r (functor r ⋙ Φ) H).map f

Tactic:
·

Goal state after:
case h_obj
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
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ ∀ (X : Quotient r), Φ.obj X = (lift r (functor r ⋙ Φ) H).obj X
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: case h_map
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
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ ∀ (X Y : Quotient r) (f : X ⟶ Y), Φ.map f ≍ (lift r (functor r ⋙ Φ) H).map f

Tactic:
·

Goal state after:
case h_map
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
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ ∀ (X Y : Quotient r) (f : X ⟶ Y), Φ.map f ≍ (lift r (functor r ⋙ Φ) H).map f
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 i (c.next i)
⊢ f.f (c.next i) =
    K.d (c.next i) (c.next (c.next i)) ≫ ho.hom (c.next (c.next i)) (c.next i) +
        ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)

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 i (c.next i)
⊢ f.f (c.next i) =
    f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i) + ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)

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 i (c.next i)
⊢ f.f (c.next i) =
    K.d (c.next i) (c.next (c.next i)) ≫ ho.hom (c.next (c.next i)) (c.next i) +
        ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)
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₁ F₂ : Quotient r ⥤ D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ F₂).map f₁ = (functor r ⋙ F₂).map f₂

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₁ F₂ : Quotient r ⥤ D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ F₁ = lift r (functor r ⋙ F₂) ?m.62

Tactic:
·

Goal state after:
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₁ F₂ : Quotient r ⥤ D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ F₂).map f₁ = (functor r ⋙ F₂).map f₂
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
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 i (c.next i)
⊢ f.f (c.next i) =
    f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i) + ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)

Tactic:
·

Goal state after:
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 i (c.next i)
⊢ f.f (c.next i) =
    f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i) + ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)
Module: Mathlib.Algebra.Homology.HomotopyCategory

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

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

Tactic:
·

Goal state after:
case mp
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ 𝟙 ((quotient V c).obj C) = 0 → Nonempty (Homotopy (𝟙 C) 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
⊢ Nonempty (Homotopy (𝟙 C) 0) → 𝟙 ((quotient V c).obj C) = 0

Tactic:
·

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
⊢ Nonempty (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
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
⊢ (Induced.add F s i (m₁ + m₂) m₃).hom.app (F.obj X) ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X)) =
    (eqToHom ⋯).app (F.obj X) ≫
      (Induced.add F s i m₁ (m₂ + m₃)).hom.app (F.obj X) ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))

Tactic:
← cancel_mono ((s m₃).map ((s m₂).map ((i m₁).hom.app X)))

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
X : C
eq :
  F.map ((shiftFunctorAdd C (m₁ + m₂) m₃).hom.app X) ≫
      F.map ((shiftFunctor C m₃).map ((shiftFunctorAdd C m₁ m₂).hom.app X)) =
    F.map (eqToHom ⋯) ≫
      F.map ((shiftFunctorAdd C m₁ (m₂ + m₃)).hom.app X) ≫
        F.map ((shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X))
⊢ ((Induced.add F s i (m₁ + m₂) m₃).hom.app (F.obj X) ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app (F.obj X))) ≫
      (s m₃).map ((s m₂).map ((i m₁).hom.app X)) =
    ((eqToHom ⋯).app (F.obj X) ≫
        (Induced.add F s i m₁ (m₂ + m₃)).hom.app (F.obj X) ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj (F.obj X))) ≫
      (s m₃).map ((s m₂).map ((i m₁).hom.app 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
n : ℤ
h : n = 0
K : CochainComplex C ℤ
i : ℤ
⊢ i = i + n

Tactic:
by lia

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₁ n₂ n₁₂ : ℤ
h : n₁ + n₂ = n₁₂
K : CochainComplex C ℤ
i : ℤ
⊢ i + n₂ + n₁ = i + n₁₂

Tactic:
by lia

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ ((shiftFunctorComm (CochainComplex C ℤ) a b).hom.app K).f p = (XIsoOfEq K ⋯).hom

Tactic:
shiftFunctorComm_eq _ _ _ _ rfl

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b p : ℤ
⊢ (((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b (a + b) ⋯).symm ≪≫
                CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) b a (a + b) ⋯).hom.app
          K).f
      p =
    (XIsoOfEq K ⋯).hom
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

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
K L M : CochainComplex C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n' + a = n
p q : ℤ
hpq : p + n' = q
⊢ p + n = q + a

Tactic:
by lia

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

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
K L M : CochainComplex C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
⊢ p + a + n = q

Tactic:
by lia

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 : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n' = q
p' : ℤ
hp' : p' + n = q
⊢ p' = p + a

Tactic:
by lia

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

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

Tactic:
by lia

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

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

Tactic:
by lia

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

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

Tactic:
by lia

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

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

Tactic:
by lia

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'
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p' + n' = q
⊢ p' = p - a

Tactic:
by lia

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

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
K L M : CochainComplex C ℤ
n : ℤ
γ γ₁ γ₂ : Cochain K L n
a p q : ℤ
hpq : p + n = q
⊢ p + a + n = q + a

Tactic:
by lia

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 : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
p q : ℤ
hpq : p + n = q
⊢ q - n' + n' = q

Tactic:
by lia

Goal state after: