awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ 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)
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ 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
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
⊢ (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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ (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
have neg : ¬c.Rel j i → Eq (α := C.X i ⟶ E.X j) (0 ≫ g.f j) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ Eq (α := C.X i ⟶ E.X j) (0 ≫ g.f j) 0
have neg : Eq.{v + 1} (α := C.X i ⟶ E.X j) 0 0
Tactic: rw [zero_comp]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ f ≫ nullHomotopicMap hom = nullHomotopicMap fun (i j : ι) ↦ f.f i ≫ hom i j
have h : ∀ (n : ι), (f ≫ nullHomotopicMap hom).f n = Hom.f (nullHomotopicMap fun (i j : ι) ↦ f.f i ≫ hom i j) n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 ≫ nullHomotopicMap hom).f n = Hom.f (nullHomotopicMap fun (i j : ι) ↦ f.f i ≫ hom i j) n
have 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
Tactic: dsimp [nullHomotopicMap, fromNext, toPrev, AddMonoidHom.mk'_apply]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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)
⊢ f ≫ nullHomotopicMap' hom = nullHomotopicMap' fun (i j : ι) (hij : c.Rel j i) ↦ f.f i ≫ hom i j hij
have 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)
Tactic: rw [nullHomotopicMap', comp_nullHomotopicMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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)
⊢ 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)
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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)
⊢ 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
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
⊢ (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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ (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
have neg : ¬c.Rel j i → Eq (α := C.X i ⟶ E.X j) (f.f i ≫ 0) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ Eq (α := C.X i ⟶ E.X j) (f.f i ≫ 0) 0
have neg : Eq.{v + 1} (α := C.X i ⟶ E.X j) 0 0
Tactic: rw [comp_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ 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))
have 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)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
⊢ 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)
have 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))
Tactic: dsimp [nullHomotopicMap, dNext, prevD]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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)
⊢ 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))
have 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))
Tactic: rw [nullHomotopicMap', map_nullHomotopicMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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)
⊢ 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))
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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)
⊢ 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
have 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
Tactic: ext i j
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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 : ι
⊢ 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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ 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
have neg : ¬c.Rel j i → Eq (α := G.obj (C.X i) ⟶ G.obj (D.X j)) (G.map 0) 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ Eq (α := G.obj (C.X i) ⟶ G.obj (D.X j)) (G.map 0) 0
have neg : Eq.{v_1 + 1} (α := G.obj (C.X i) ⟶ G.obj (D.X j)) 0 0
Tactic: rw [G.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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) +
      Hom.f 0 i
have 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)
Tactic: rw [HomologicalComplex.zero_f_apply, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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)
⊢ Homotopy (nullHomotopicMap' h) 0
have apply : ∀ (i j : ι), ¬c.Rel j i → (dite (c.Rel j i) (h i j) fun (x : ¬c.Rel j i) ↦ 0) = 0
Tactic: apply nullHomotopy fun i j => dite (c.Rel j i) (h i j) fun _ => 0
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ (nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁ + hom k₁ k₂ ≫ D.d k₂ k₁
have 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₁
Tactic: dsimp only [nullHomotopicMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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
⊢ 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₁
have 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₁
Tactic: rw [dNext_eq hom r₁₀, prevD_eq hom r₂₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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₁
⊢ 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₁
have 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₁
Tactic: rw [dNext_eq hom r₁₀, prevD_eq hom r₂₁]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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)
⊢ 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₁
have 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₁
Tactic: rw [nullHomotopicMap_f r₂₁ r₁₀]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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)
⊢ (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₁
have split_ifs : C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₀ = hom k₀ k₁ ≫ D.d k₁ k₀
have 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₀) =
  hom k₀ k₁ ≫ D.d k₁ k₀
Tactic: dsimp only [nullHomotopicMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ 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₀) =
    hom k₀ k₁ ≫ D.d k₁ k₀
have a : ¬c.Rel k₀ (c.next k₀)
Tactic: rw [prevD_eq hom r₁₀, dNext, AddMonoidHom.mk'_apply, C.shape, zero_comp, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ Hom.f (nullHomotopicMap fun (i j : ι) ↦ dite (c.Rel j i) (h i j) fun (x : ¬c.Rel j i) ↦ 0) k₀ =
    h k₀ k₁ r₁₀ ≫ D.d k₁ k₀
have rw : (dite (c.Rel k₁ k₀) (h k₀ k₁) fun (x : ¬c.Rel k₁ k₀) ↦ 0) ≫ D.d k₁ k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀
Tactic: rw [nullHomotopicMap_f_of_not_rel_left r₁₀ hk₀]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ (dite (c.Rel k₁ k₀) (h k₀ k₁) fun (x : ¬c.Rel k₁ k₀) ↦ 0) ≫ D.d k₁ k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀
have split_ifs : h k₀ k₁ r₁₀ ≫ D.d k₁ k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom k₀ k₁
have 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₁
Tactic: dsimp only [nullHomotopicMap]
-- Lean 4 proof step from Mathlib.Algebra.Homology.Homotopy (goal)
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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ 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₁
have a : ¬c.Rel (c.prev k₁) k₁
Tactic: rw [dNext_eq hom r₁₀, prevD, AddMonoidHom.mk'_apply, D.shape, comp_zero, add_zero]