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 : 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)
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₁
⊢ (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:
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
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₀ ≫ 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:
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
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
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₀) =
    hom k₀ k₁ ≫ D.d k₁ k₀
⊢ (nullHomotopicMap hom).f 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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
a : ¬c.Rel k₀ (c.next 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₀) =
    hom k₀ k₁ ≫ D.d k₁ k₀

Tactic:
rw [prevD_eq hom r₁₀, dNext, AddMonoidHom.mk'_apply, C.shape, zero_comp, zero_add]

Premises used: prevD_eq, zero_add, dNext, AddMonoidHom.mk'_apply, CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- 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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel k₀ (c.next k₀)

Tactic:
hk₀ _
-- 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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel k₀ (c.next k₀)

Tactic:
exact hk₀ _
-- 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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
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₀
⊢ 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₀

Tactic:
rw [nullHomotopicMap_f_of_not_rel_left r₁₀ hk₀]

Premises used: Homotopy.nullHomotopicMap_f_of_not_rel_left
-- 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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
split_ifs : h k₀ k₁ r₁₀ ≫ D.d k₁ k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀
⊢ (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:
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
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)
⊢ h k₀ k₁ r₁₀ ≫ D.d k₁ k₀ = h k₀ k₁ r₁₀ ≫ D.d k₁ k₀

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
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l 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₁
⊢ (nullHomotopicMap hom).f k₁ = C.d k₁ k₀ ≫ hom 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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
a : ¬c.Rel (c.prev 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₁

Tactic:
rw [dNext_eq hom r₁₀, prevD, AddMonoidHom.mk'_apply, D.shape, comp_zero, add_zero]

Premises used: CategoryTheory.Limits.comp_zero, dNext_eq, AddMonoidHom.mk'_apply, add_zero, HomologicalComplex.shape, 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
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel (c.prev k₁) k₁

Tactic:
hk₁ _
-- 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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel (c.prev k₁) k₁

Tactic:
exact hk₁ _
-- 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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l 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) = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀
⊢ 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₁₀

Tactic:
rw [nullHomotopicMap_f_of_not_rel_right r₁₀ hk₁]

Premises used: Homotopy.nullHomotopicMap_f_of_not_rel_right
-- 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₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
split_ifs : C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀
⊢ (C.d k₁ k₀ ≫ dite (c.Rel k₁ k₀) (h k₀ k₁) fun (x : ¬c.Rel k₁ k₀) ↦ 0) = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀

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
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀

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
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
dsimp :
  CategoryStruct.comp (Y := C.X (c.next k₀)) (C.d k₀ (c.next k₀)) (hom (c.next k₀) k₀) +
      CategoryStruct.comp (Y := D.X (c.prev k₀)) (hom k₀ (c.prev k₀)) (D.d (c.prev k₀) k₀) =
    0
⊢ (nullHomotopicMap hom).f k₀ = 0

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
k₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
a : ¬c.Rel (c.prev k₀) k₀
a₁ : ¬c.Rel k₀ (c.next k₀)
⊢ CategoryStruct.comp (Y := C.X (c.next k₀)) (C.d k₀ (c.next k₀)) (hom (c.next k₀) k₀) +
      CategoryStruct.comp (Y := D.X (c.prev k₀)) (hom k₀ (c.prev k₀)) (D.d (c.prev k₀) k₀) =
    0

Tactic:
rw [C.shape, D.shape, zero_comp, comp_zero, add_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp, add_zero, HomologicalComplex.shape
-- 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₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel (c.prev k₀) k₀

Tactic:
apply_assumption
-- 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₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel k₀ (c.next k₀)

Tactic:
apply_assumption
-- 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₀ : ι
hk₀ : ∀ (l : ι), ¬c.Rel k₀ l
hk₀' : ∀ (l : ι), ¬c.Rel l k₀
h : (i j : ι) → c.Rel j i → (C.X i ⟶ D.X j)
⊢ Eq.{v + 1} (α := C.X k₀ ⟶ D.X k₀)
    (Hom.f (nullHomotopicMap fun (i j : ι) ↦ dite (c.Rel j i) (h i j) fun (x : ¬c.Rel j i) ↦ 0) k₀) 0

Tactic:
apply nullHomotopicMap_f_eq_zero hk₀ hk₀'

Premises used: Homotopy.nullHomotopicMap_f_eq_zero
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
dsimp :
  CategoryStruct.comp (Y := Q.X ((ComplexShape.down ℕ).prev j)) (f j ((ComplexShape.down ℕ).prev j))
      (Q.d ((ComplexShape.down ℕ).prev j) j) =
    CategoryStruct.comp (Y := Q.X (j + 1)) (f j (j + 1)) (Q.d (j + 1) j)
⊢ (prevD j : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → P.X j ⟶ Q.X j) f =
    CategoryStruct.comp (Y := Q.X (j + 1)) (f j (j + 1)) (Q.d (j + 1) j)

Tactic:
dsimp [prevD]

Premises used: prevD
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
⊢ (ComplexShape.down ℕ).prev j = j + 1

Tactic:
have : (ComplexShape.down ℕ).prev j = j + 1 := ChainComplex.prev ℕ j
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
j : ℕ
this : (ComplexShape.down ℕ).prev j = j + 1
⊢ CategoryStruct.comp (Y := Q.X ((ComplexShape.down ℕ).prev j)) (f j ((ComplexShape.down ℕ).prev j))
      (Q.d ((ComplexShape.down ℕ).prev j) j) =
    CategoryStruct.comp (Y := Q.X (j + 1)) (f j (j + 1)) (Q.d (j + 1) j)

Tactic:
congr 2
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
dsimp :
  Eq (α := P.X (i + 1) ⟶ Q.X (i + 1))
    (CategoryStruct.comp (Y := P.X ((ComplexShape.down ℕ).next (i + 1)))
      (P.d (i + 1) ((ComplexShape.down ℕ).next (i + 1))) (f ((ComplexShape.down ℕ).next (i + 1)) (i + 1)))
    (P.d (i + 1) i ≫ f i (i + 1))
⊢ Eq (α := P.X (i + 1) ⟶ Q.X (i + 1))
    ((dNext (i + 1) : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → P.X (i + 1) ⟶ Q.X (i + 1)) f : P.X (i + 1) ⟶ Q.X (i + 1))
    (P.d (i + 1) i ≫ f i (i + 1) : P.X (i + 1) ⟶ Q.X (i + 1))

Tactic:
dsimp [dNext]

Premises used: dNext
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
⊢ (ComplexShape.down ℕ).next (i + 1) = i

Tactic:
have : (ComplexShape.down ℕ).next (i + 1) = i := ChainComplex.next_nat_succ _
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
i : ℕ
this : (ComplexShape.down ℕ).next (i + 1) = i
⊢ Eq (α := P.X (i + 1) ⟶ Q.X (i + 1))
    (CategoryStruct.comp (Y := P.X ((ComplexShape.down ℕ).next (i + 1)))
      (P.d (i + 1) ((ComplexShape.down ℕ).next (i + 1))) (f ((ComplexShape.down ℕ).next (i + 1)) (i + 1)))
    (P.d (i + 1) i ≫ f i (i + 1))

Tactic:
congr 2
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
dsimp :
  Eq (α := P.X 0 ⟶ Q.X 0)
    (CategoryStruct.comp (Y := P.X ((ComplexShape.down ℕ).next 0)) (P.d 0 ((ComplexShape.down ℕ).next 0))
      (f ((ComplexShape.down ℕ).next 0) 0))
    0
⊢ Eq (α := P.X 0 ⟶ Q.X 0) ((dNext 0 : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → P.X 0 ⟶ Q.X 0) f : P.X 0 ⟶ Q.X 0)
    (0 : P.X 0 ⟶ Q.X 0)

Tactic:
dsimp [dNext]

Premises used: dNext
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
a : ¬(ComplexShape.down ℕ).Rel 0 ((ComplexShape.down ℕ).next 0)
⊢ Eq (α := P.X 0 ⟶ Q.X 0)
    (CategoryStruct.comp (Y := P.X ((ComplexShape.down ℕ).next 0)) (P.d 0 ((ComplexShape.down ℕ).next 0))
      (f ((ComplexShape.down ℕ).next 0) 0))
    0

Tactic:
rw [P.shape, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp, HomologicalComplex.shape
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
a : ¬(ComplexShape.down ℕ).Rel 0 0
⊢ ¬(ComplexShape.down ℕ).Rel 0 ((ComplexShape.down ℕ).next 0)

Tactic:
rw [ChainComplex.next_nat_zero]

Premises used: ChainComplex.next_nat_zero
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬Eq (α := ℕ) 1 0

Tactic:
decide
-- 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 : ι
P Q : ChainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
        e.f (n + 2) =
          P.d (n + 2) (n + 1) ≫
              p.snd (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)).fst
                (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ↦
                e.f (n + 1) =
                  P.d (n + 1) n ≫
                      p.fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                          e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
                    f' ≫ Q.d (n + 2) (n + 1)) +
            f'' ≫ Q.d (n + 3) (n + 2)
⊢ e.f 0 = dFrom P 0 ≫ 0 + (zero ≫ Iso.inv (xPrevIso Q ⋯)) ≫ dTo Q 0

Tactic:
simpa using comm_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 : ι
P Q : ChainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
        e.f (n + 2) =
          P.d (n + 2) (n + 1) ≫
              p.snd (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)).fst
                (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ↦
                e.f (n + 1) =
                  P.d (n + 1) n ≫
                      p.fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                          e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
                    f' ≫ Q.d (n + 2) (n + 1)) +
            f'' ≫ Q.d (n + 3) (n + 2)
n : ℕ
I : (f : P.X n ⟶ Q.X (n + 1)) ×'
  (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1) :=
  mkInductiveAux₁ e zero one comm_one succ n
⊢ e.f (n + 1) =
    dFrom P (n + 1) ≫
        Iso.hom (xNextIso P ⋯) ≫
          I.fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
      (I.snd (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)).fst
            (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ↦
            e.f (n + 1) =
              P.d (n + 1) n ≫
                  I.fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
                f' ≫ Q.d (n + 2) (n + 1)) ≫
          Iso.inv (xPrevIso Q ⋯)) ≫
        dTo Q (n + 1)

Tactic:
simpa using I.2.2

Premises used: PSigma.snd
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
        e.f (n + 2) =
          P.d (n + 2) (n + 1) ≫
              p.snd (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)).fst
                (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ↦
                e.f (n + 1) =
                  P.d (n + 1) n ≫
                      p.fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                          e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
                    f' ≫ Q.d (n + 2) (n + 1)) +
            f'' ≫ Q.d (n + 3) (n + 2)
⊢ mkInductiveAux₂ e zero comm_zero one comm_one succ 0 =
    PSigma.mk (β := fun (f : xNext P 0 ⟶ Q.X 0) ↦ (f' : P.X 0 ⟶ xPrev Q 0) ×' e.f 0 = dFrom P 0 ≫ f + f' ≫ dTo Q 0) 0
      (PSigma.mk (β := fun (f' : P.X 0 ⟶ xPrev Q 0) ↦ e.f 0 = dFrom P 0 ≫ 0 + f' ≫ dTo Q 0)
        (zero ≫ Iso.inv (xPrevIso Q ⋯)) ⋯)

Tactic:
rfl

Premises used: Homotopy.mkInductiveAux₂, rfl
-- Module: Mathlib.Algebra.Homology.Homotopy
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : Preadditive.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
        e.f (n + 2) =
          P.d (n + 2) (n + 1) ≫
              p.snd (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)).fst
                (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ↦
                e.f (n + 1) =
                  P.d (n + 1) n ≫
                      p.fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                        (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
                          e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
                    f' ≫ Q.d (n + 2) (n + 1)) +
            f'' ≫ Q.d (n + 3) (n + 2)
n : ℕ
⊢ mkInductiveAux₂ e zero comm_zero one comm_one succ (n + 1) =
    PSigma.mk (β := fun (f : xNext P (n + 1) ⟶ Q.X (n + 1)) ↦
      (f' : P.X (n + 1) ⟶ xPrev Q (n + 1)) ×' e.f (n + 1) = dFrom P (n + 1) ≫ f + f' ≫ dTo Q (n + 1))
      (Iso.hom (xNextIso P ⋯) ≫
        (mkInductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)))
      (PSigma.mk (β := fun (f' : P.X (n + 1) ⟶ xPrev Q (n + 1)) ↦
        e.f (n + 1) =
          dFrom P (n + 1) ≫
              Iso.hom (xNextIso P ⋯) ≫
                (mkInductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                  (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
            f' ≫ dTo Q (n + 1))
        ((mkInductiveAux₁ e zero one comm_one succ n).snd (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)).fst
            (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ↦
            e.f (n + 1) =
              P.d (n + 1) n ≫
                  (mkInductiveAux₁ e zero one comm_one succ n).fst (β := fun (f : P.X n ⟶ Q.X (n + 1)) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) +
                f' ≫ Q.d (n + 2) (n + 1)) ≫
          Iso.inv (xPrevIso Q ⋯))
        ⋯)

Tactic:
rfl

Premises used: Homotopy.mkInductiveAux₂, rfl