awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
hom : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
n : ι
h :
  (C.dFrom n ≫ hom (c.next n) n + hom n (c.prev n) ≫ D.dTo n) ≫ g.f n =
    C.dFrom n ≫ hom (c.next n) n ≫ g.f n + (hom n (c.prev n) ≫ g.f (c.prev n)) ≫ E.dTo n
⊢ (nullHomotopicMap hom ≫ g).f n = Hom.f (nullHomotopicMap fun (i j : ι) ↦ hom i j ≫ g.f j) n

Tactic:
dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]

Premises used: fromNext, toPrev, AddMonoidHom.mk'_apply, Homotopy.nullHomotopicMap
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
hom : (i j : ι) → C.X i ⟶ D.X j
g : D ⟶ E
n : ι
⊢ (C.dFrom n ≫ hom (c.next n) n + hom n (c.prev n) ≫ D.dTo n) ≫ g.f n =
    C.dFrom n ≫ hom (c.next n) n ≫ g.f n + (hom n (c.prev n) ≫ g.f (c.prev n)) ≫ E.dTo n

Tactic:
simp only [Preadditive.add_comp, assoc, g.comm]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Preadditive.add_comp, HomologicalComplex.Hom.comm
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
rw :
  Eq (α := C ⟶ E) (nullHomotopicMap fun (i j : ι) ↦ (dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0) ≫ g.f j)
    (nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦ hom i j hij ≫ g.f j)
⊢ nullHomotopicMap' hom ≫ g = nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦ hom i j hij ≫ g.f j

Tactic:
rw [nullHomotopicMap', nullHomotopicMap_comp]

Premises used: Homotopy.nullHomotopicMap_comp, Homotopy.nullHomotopicMap'
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
e_hom :
  Eq (α := (i j : ι) → C.X i ⟶ E.X j) (fun (i j : ι) ↦ (dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0) ≫ g.f j)
    fun (i j : ι) ↦
    dite (c.Rel j i) ((fun (i j : ι) (hij : c.Rel j i) ↦ hom i j hij ≫ g.f j) i j) fun (x : ¬c.Rel j i) ↦ 0
⊢ Eq (α := C ⟶ E) (nullHomotopicMap fun (i j : ι) ↦ (dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0) ≫ g.f j)
    (nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦ hom i j hij ≫ g.f j)

Tactic:
congr
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
e_hom :
  ∀ (i j : ι),
    (dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0) ≫ g.f j =
      dite (c.Rel j i) ((fun (i j : ι) (hij : c.Rel j i) ↦ hom i j hij ≫ g.f j) i j) fun (x : ¬c.Rel j i) ↦ 0
⊢ Eq (α := (i j : ι) → C.X i ⟶ E.X j) (fun (i j : ι) ↦ (dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0) ≫ g.f j)
    fun (i j : ι) ↦
    dite (c.Rel j i) ((fun (i j : ι) (hij : c.Rel j i) ↦ hom i j hij ≫ g.f j) i j) fun (x : ¬c.Rel j i) ↦ 0

Tactic:
ext i j
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
i j : ι
pos : ∀ (h : c.Rel j i), hom i j h ≫ g.f j = (fun (i j : ι) (hij : c.Rel j i) ↦ hom i j hij ≫ g.f j) i j h
neg : ¬c.Rel j i → Eq (α := C.X i ⟶ E.X j) (0 ≫ g.f j) 0
⊢ (dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0) ≫ g.f j =
    dite (c.Rel j i) ((fun (i j : ι) (hij : c.Rel j i) ↦ hom i j hij ≫ g.f j) i j) fun (x : ¬c.Rel j i) ↦ 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
i j : ι
h : c.Rel j i
⊢ hom i j h ≫ g.f j = (fun (i j : ι) (hij : c.Rel j i) ↦ hom i j hij ≫ g.f j) i j h

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
g : D ⟶ E
i j : ι
h : ¬c.Rel j i
neg neg₁ : Eq.{v + 1} (α := C.X i ⟶ E.X j) 0 0
⊢ Eq (α := C.X i ⟶ E.X j) (0 ≫ g.f j) 0

Tactic:
rw [zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
hom : (i j : ι) → D.X i ⟶ E.X j
h : ∀ (n : ι), (f ≫ nullHomotopicMap hom).f n = Hom.f (nullHomotopicMap fun (i j : ι) ↦ f.f i ≫ hom i j) n
⊢ f ≫ nullHomotopicMap hom = nullHomotopicMap fun (i j : ι) ↦ f.f i ≫ hom i j

Tactic:
ext n
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
hom : (i j : ι) → D.X i ⟶ E.X j
n : ι
h :
  f.f n ≫ (D.dFrom n ≫ hom (c.next n) n + hom n (c.prev n) ≫ E.dTo n) =
    C.dFrom n ≫ f.f (c.next n) ≫ hom (c.next n) n + (f.f n ≫ hom n (c.prev n)) ≫ E.dTo n
⊢ (f ≫ nullHomotopicMap hom).f n = Hom.f (nullHomotopicMap fun (i j : ι) ↦ f.f i ≫ hom i j) n

Tactic:
dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]

Premises used: fromNext, toPrev, AddMonoidHom.mk'_apply, Homotopy.nullHomotopicMap
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
hom : (i j : ι) → D.X i ⟶ E.X j
n : ι
⊢ f.f n ≫ (D.dFrom n ≫ hom (c.next n) n + hom n (c.prev n) ≫ E.dTo n) =
    C.dFrom n ≫ f.f (c.next n) ≫ hom (c.next n) n + (f.f n ≫ hom n (c.prev n)) ≫ E.dTo n

Tactic:
simp only [Preadditive.comp_add, assoc, f.comm_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Preadditive.comp_add, HomologicalComplex.Hom.comm_assoc
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)
rw :
  Eq (α := C ⟶ E) (nullHomotopicMap fun (i j : ι) ↦ f.f i ≫ dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0)
    (nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦ f.f i ≫ hom i j hij)
⊢ f ≫ nullHomotopicMap' hom = nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦ f.f i ≫ hom i j hij

Tactic:
rw [nullHomotopicMap', comp_nullHomotopicMap]

Premises used: Homotopy.comp_nullHomotopicMap, Homotopy.nullHomotopicMap'
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)
e_hom :
  Eq (α := (i j : ι) → C.X i ⟶ E.X j) (fun (i j : ι) ↦ f.f i ≫ dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0)
    fun (i j : ι) ↦
    dite (c.Rel j i) ((fun (i j : ι) (hij : c.Rel j i) ↦ f.f i ≫ hom i j hij) i j) fun (x : ¬c.Rel j i) ↦ 0
⊢ Eq (α := C ⟶ E) (nullHomotopicMap fun (i j : ι) ↦ f.f i ≫ dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0)
    (nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦ f.f i ≫ hom i j hij)

Tactic:
congr
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)
e_hom :
  ∀ (i j : ι),
    (f.f i ≫ dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0) =
      dite (c.Rel j i) ((fun (i j : ι) (hij : c.Rel j i) ↦ f.f i ≫ hom i j hij) i j) fun (x : ¬c.Rel j i) ↦ 0
⊢ Eq (α := (i j : ι) → C.X i ⟶ E.X j) (fun (i j : ι) ↦ f.f i ≫ dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0)
    fun (i j : ι) ↦
    dite (c.Rel j i) ((fun (i j : ι) (hij : c.Rel j i) ↦ f.f i ≫ hom i j hij) i j) fun (x : ¬c.Rel j i) ↦ 0

Tactic:
ext i j
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)
i j : ι
pos : ∀ (h : c.Rel j i), f.f i ≫ hom i j h = (fun (i j : ι) (hij : c.Rel j i) ↦ f.f i ≫ hom i j hij) i j h
neg : ¬c.Rel j i → Eq (α := C.X i ⟶ E.X j) (f.f i ≫ 0) 0
⊢ (f.f i ≫ dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0) =
    dite (c.Rel j i) ((fun (i j : ι) (hij : c.Rel j i) ↦ f.f i ≫ hom i j hij) i j) fun (x : ¬c.Rel j i) ↦ 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)
i j : ι
h : c.Rel j i
⊢ f.f i ≫ hom i j h = (fun (i j : ι) (hij : c.Rel j i) ↦ f.f i ≫ hom i j hij) i j h

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f : C ⟶ D
hom : (i j : ι) → c.Rel j i → (D.X i ⟶ E.X j)
i j : ι
h : ¬c.Rel j i
neg neg₁ : Eq.{v + 1} (α := C.X i ⟶ E.X j) 0 0
⊢ Eq (α := C.X i ⟶ E.X j) (f.f i ≫ 0) 0

Tactic:
rw [comp_zero]

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h k : D ⟶ E
i_1 : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
G : CategoryTheory.Functor.{v, v_1, u, u_2} V W
inst_4 : G.Additive
hom : (i j : ι) → C.X i ⟶ D.X j
i j : ι
⊢ X (Functor.obj (G.mapHomologicalComplex c) C) i ⟶ X (Functor.obj (G.mapHomologicalComplex c) D) j

Tactic:
exact G.map (hom i j)

Premises used: CategoryTheory.Functor.map
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
G : CategoryTheory.Functor.{v, v_1, u, u_2} V W
inst_4 : G.Additive
hom : (i j : ι) → C.X i ⟶ D.X j
h :
  ∀ (i : ι),
    Eq (α := X (Functor.obj (G.mapHomologicalComplex c) C) i ⟶ X (Functor.obj (G.mapHomologicalComplex c) D) i)
      (Hom.f (CategoryTheory.Functor.map (G.mapHomologicalComplex c) (nullHomotopicMap hom)) i)
      (Hom.f (nullHomotopicMap fun (i j : ι) ↦ G.map (hom i j)) i)
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_1, u_2, u_1} W c) (Functor.obj (G.mapHomologicalComplex c) C)
      (Functor.obj (G.mapHomologicalComplex c) D))
    (CategoryTheory.Functor.map (G.mapHomologicalComplex c) (nullHomotopicMap hom))
    (nullHomotopicMap fun (i j : ι) ↦ G.map (hom i j))

Tactic:
ext i
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
G : CategoryTheory.Functor.{v, v_1, u, u_2} V W
inst_4 : G.Additive
hom : (i j : ι) → C.X i ⟶ D.X j
i : ι
h :
  G.map
      (CategoryStruct.comp (Y := C.X (c.next i)) (C.d i (c.next i)) (hom (c.next i) i) +
        CategoryStruct.comp (Y := D.X (c.prev i)) (hom i (c.prev i)) (D.d (c.prev i) i)) =
    CategoryStruct.comp (Y := G.obj (C.X (c.next i))) (G.map (C.d i (c.next i))) (G.map (hom (c.next i) i)) +
      CategoryStruct.comp (Y := G.obj (D.X (c.prev i))) (G.map (hom i (c.prev i))) (G.map (D.d (c.prev i) i))
⊢ Eq (α := X (Functor.obj (G.mapHomologicalComplex c) C) i ⟶ X (Functor.obj (G.mapHomologicalComplex c) D) i)
    (Hom.f (CategoryTheory.Functor.map (G.mapHomologicalComplex c) (nullHomotopicMap hom)) i)
    (Hom.f (nullHomotopicMap fun (i j : ι) ↦ G.map (hom i j)) i)

Tactic:
dsimp [nullHomotopicMap, dNext, prevD]

Premises used: dNext, Homotopy.nullHomotopicMap, prevD
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
G : CategoryTheory.Functor.{v, v_1, u, u_2} V W
inst_4 : G.Additive
hom : (i j : ι) → C.X i ⟶ D.X j
i : ι
⊢ G.map
      (CategoryStruct.comp (Y := C.X (c.next i)) (C.d i (c.next i)) (hom (c.next i) i) +
        CategoryStruct.comp (Y := D.X (c.prev i)) (hom i (c.prev i)) (D.d (c.prev i) i)) =
    CategoryStruct.comp (Y := G.obj (C.X (c.next i))) (G.map (C.d i (c.next i))) (G.map (hom (c.next i) i)) +
      CategoryStruct.comp (Y := G.obj (D.X (c.prev i))) (G.map (hom i (c.prev i))) (G.map (D.d (c.prev i) i))

Tactic:
simp only [G.map_comp, Functor.map_add]

Premises used: CategoryTheory.Functor.map_add, CategoryTheory.Functor.map_comp
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h k : D ⟶ E
i_1 : ι
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
G : CategoryTheory.Functor.{v, v_1, u, u_2} V W
inst_4 : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
i j : ι
hij : c.Rel j i
⊢ X (Functor.obj (G.mapHomologicalComplex c) C) i ⟶ X (Functor.obj (G.mapHomologicalComplex c) D) j

Tactic:
exact G.map (hom i j hij)

Premises used: CategoryTheory.Functor.map
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
G : CategoryTheory.Functor.{v, v_1, u, u_2} V W
inst_4 : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
rw :
  Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_1, u_2, u_1} W c) (Functor.obj (G.mapHomologicalComplex c) C)
      (Functor.obj (G.mapHomologicalComplex c) D))
    (nullHomotopicMap fun (i j : ι) ↦ G.map (dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0))
    (nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦ G.map (hom i j hij))
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_1, u_2, u_1} W c) (Functor.obj (G.mapHomologicalComplex c) C)
      (Functor.obj (G.mapHomologicalComplex c) D))
    (CategoryTheory.Functor.map (G.mapHomologicalComplex c) (nullHomotopicMap' hom))
    (nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦ G.map (hom i j hij))

Tactic:
rw [nullHomotopicMap', map_nullHomotopicMap]

Premises used: Homotopy.map_nullHomotopicMap, Homotopy.nullHomotopicMap'
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
G : CategoryTheory.Functor.{v, v_1, u, u_2} V W
inst_4 : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
e_hom :
  Eq (α :=
    (i j : ι) → X (Functor.obj (G.mapHomologicalComplex c) C) i ⟶ X (Functor.obj (G.mapHomologicalComplex c) D) j)
    (fun (i j : ι) ↦ G.map (dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0)) fun (i j : ι) ↦
    dite (c.Rel j i) ((fun (i j : ι) (hij : c.Rel j i) ↦ G.map (hom i j hij)) i j) fun (x : ¬c.Rel j i) ↦ 0
⊢ Eq (α :=
    Quiver.Hom (V := HomologicalComplex.{v_1, u_2, u_1} W c) (Functor.obj (G.mapHomologicalComplex c) C)
      (Functor.obj (G.mapHomologicalComplex c) D))
    (nullHomotopicMap fun (i j : ι) ↦ G.map (dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0))
    (nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦ G.map (hom i j hij))

Tactic:
congr
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
G : CategoryTheory.Functor.{v, v_1, u, u_2} V W
inst_4 : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
e_hom :
  ∀ (i j : ι),
    G.map (dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0) =
      dite (c.Rel j i) ((fun (i j : ι) (hij : c.Rel j i) ↦ G.map (hom i j hij)) i j) fun (x : ¬c.Rel j i) ↦ 0
⊢ Eq (α :=
    (i j : ι) → X (Functor.obj (G.mapHomologicalComplex c) C) i ⟶ X (Functor.obj (G.mapHomologicalComplex c) D) j)
    (fun (i j : ι) ↦ G.map (dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0)) fun (i j : ι) ↦
    dite (c.Rel j i) ((fun (i j : ι) (hij : c.Rel j i) ↦ G.map (hom i j hij)) i j) fun (x : ¬c.Rel j i) ↦ 0

Tactic:
ext i j
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
G : CategoryTheory.Functor.{v, v_1, u, u_2} V W
inst_4 : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
i j : ι
pos : ∀ (h : c.Rel j i), G.map (hom i j h) = (fun (i j : ι) (hij : c.Rel j i) ↦ G.map (hom i j hij)) i j h
neg : ¬c.Rel j i → Eq (α := G.obj (C.X i) ⟶ G.obj (D.X j)) (G.map 0) 0
⊢ G.map (dite (c.Rel j i) (hom i j) fun (x : ¬c.Rel j i) ↦ 0) =
    dite (c.Rel j i) ((fun (i j : ι) (hij : c.Rel j i) ↦ G.map (hom i j hij)) i j) fun (x : ¬c.Rel j i) ↦ 0

Tactic:
split_ifs
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
G : CategoryTheory.Functor.{v, v_1, u, u_2} V W
inst_4 : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
i j : ι
h : c.Rel j i
⊢ G.map (hom i j h) = (fun (i j : ι) (hij : c.Rel j i) ↦ G.map (hom i j hij)) i j h

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
W : Type u_2
inst_2 : Category.{v_1, u_2} W
inst_3 : Preadditive.{v_1, u_2} W
G : CategoryTheory.Functor.{v, v_1, u, u_2} V W
inst_4 : G.Additive
hom : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
i j : ι
h : ¬c.Rel j i
neg neg₁ : Eq.{v_1 + 1} (α := G.obj (C.X i) ⟶ G.obj (D.X j)) 0 0
⊢ Eq (α := G.obj (C.X i) ⟶ G.obj (D.X j)) (G.map 0) 0

Tactic:
rw [G.map_zero]

Premises used: CategoryTheory.Functor.map_zero
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h k : D ⟶ E
i_1 : ι
hom : (i j : ι) → C.X i ⟶ D.X j
zero : ∀ (i j : ι), ¬c.Rel j i → hom i j = 0
i : ι
rw :
  (nullHomotopicMap hom).f i =
    HAdd.hAdd (α := C.X i ⟶ D.X i) (β := C.X i ⟶ D.X i)
      ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom : C.X i ⟶ D.X i)
      ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom : C.X i ⟶ D.X i)
⊢ (nullHomotopicMap hom).f i =
    HAdd.hAdd (α := C.X i ⟶ D.X i) (β := C.X i ⟶ D.X i)
        ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom : C.X i ⟶ D.X i)
        ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom : C.X i ⟶ D.X i) +
      Hom.f 0 i

Tactic:
rw [HomologicalComplex.zero_f_apply, add_zero]

Premises used: HomologicalComplex.zero_f_apply, add_zero
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h k : D ⟶ E
i_1 : ι
hom : (i j : ι) → C.X i ⟶ D.X j
zero : ∀ (i j : ι), ¬c.Rel j i → hom i j = 0
i : ι
⊢ (nullHomotopicMap hom).f i =
    HAdd.hAdd (α := C.X i ⟶ D.X i) (β := C.X i ⟶ D.X i)
      ((dNext i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom : C.X i ⟶ D.X i)
      ((prevD i : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X i ⟶ D.X i) hom : C.X i ⟶ D.X i)

Tactic:
rfl
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h_1 k : D ⟶ E
i : ι
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
apply : ∀ (i j : ι), ¬c.Rel j i → (dite (c.Rel j i) (h i j) fun (x : ¬c.Rel j i) ↦ 0) = 0
⊢ Homotopy (nullHomotopicMap' h) 0

Tactic:
apply nullHomotopy fun i j => dite (c.Rel j i) (h i j) fun _ => 0

Premises used: dite, Homotopy.nullHomotopy, OfNat.ofNat, ComplexShape.Rel
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D E : HomologicalComplex.{v, u, u_1} V c
f g : C ⟶ D
h_1 k : D ⟶ E
i : ι
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ ∀ (i j : ι), ¬c.Rel j i → (dite (c.Rel j i) (h i j) fun (x : ¬c.Rel j i) ↦ 0) = 0

Tactic:
grind
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
hom : (i j : ι) → C.X i ⟶ D.X j
dsimp :
  HAdd.hAdd (α := C.X k₁ ⟶ D.X k₁) (β := C.X k₁ ⟶ D.X k₁)
      ((dNext k₁ : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X k₁ ⟶ D.X k₁) hom : C.X k₁ ⟶ D.X k₁)
      ((prevD k₁ : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X k₁ ⟶ D.X k₁) hom : C.X k₁ ⟶ D.X k₁) =
    C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁
⊢ (nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁

Tactic:
dsimp only [nullHomotopicMap]

Premises used: Homotopy.nullHomotopicMap
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
hom : (i j : ι) → C.X i ⟶ D.X j
rw :
  HAdd.hAdd (β := C.X k₁ ⟶ D.X k₁) (C.d k₁ k₀ ≫ hom k₀ k₁)
      ((prevD k₁ : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X k₁ ⟶ D.X k₁) hom : C.X k₁ ⟶ D.X k₁) =
    C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁
rw₁ rw₂ : C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁ = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁
⊢ HAdd.hAdd (α := C.X k₁ ⟶ D.X k₁) (β := C.X k₁ ⟶ D.X k₁)
      ((dNext k₁ : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X k₁ ⟶ D.X k₁) hom : C.X k₁ ⟶ D.X k₁)
      ((prevD k₁ : (a : (i j : ι) → C.X i ⟶ D.X j) → C.X k₁ ⟶ D.X k₁) hom : C.X k₁ ⟶ D.X k₁) =
    C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁

Tactic:
rw [dNext_eq hom r₁₀, prevD_eq hom r₂₁]

Premises used: prevD_eq, dNext_eq
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
c : ComplexShape ι
C D : HomologicalComplex.{v, u, u_1} V c
k₂ k₁ k₀ : ι
r₂₁ : c.Rel k₂ k₁
r₁₀ : c.Rel k₁ k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
rw :
  (C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun (x : ¬c.Rel k₁ k₀) ↦ 0) +
      (dite (c.Rel k₂ k₁) (h k₁ k₂) fun (x : ¬c.Rel k₂ k₁) ↦ 0) ≫ D.d k₂ k₁ =
    C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁
⊢ Hom.f (nullHomotopicMap fun (i j : ι) ↦ dite (c.Rel j i) (h i j) fun (x : ¬c.Rel j i) ↦ 0) k₁ =
    C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁

Tactic:
rw [nullHomotopicMap_f r₂₁ r₁₀]

Premises used: Homotopy.nullHomotopicMap_f