awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
i j : ℕ
h : i + 1 = j
subst :
  (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : xNext P i ⟶ Q.X i) ↦
            (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i).fst
        (β := fun (f' : P.X i ⟶ xPrev Q i) ↦
        e.f i =
          dFrom P i ≫
              (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : xNext P i ⟶ Q.X i) ↦
                (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i) +
            f' ≫ dTo Q i) ≫
      (xPrevIso Q ⋯).hom =
    (xNextIso P ⋯).inv ≫
      PSigma.fst (β := fun (f : xNext P (i + 1) ⟶ Q.X (i + 1)) ↦
        (f' : P.X (i + 1) ⟶ xPrev Q (i + 1)) ×' e.f (i + 1) = dFrom P (i + 1) ≫ f + f' ≫ dTo Q (i + 1))
        (mkInductiveAux₂ e zero comm_zero one comm_one succ (i + 1))
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : xNext P i ⟶ Q.X i) ↦
            (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i).fst
        (β := fun (f' : P.X i ⟶ xPrev Q i) ↦
        e.f i =
          dFrom P i ≫
              (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : xNext P i ⟶ Q.X i) ↦
                (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i) +
            f' ≫ dTo Q i) ≫
      (xPrevIso Q h).hom =
    (xNextIso P h).inv ≫
      (mkInductiveAux₂ e zero comm_zero one comm_one succ j).fst (β := fun (f : xNext P j ⟶ Q.X j) ↦
        (f' : P.X j ⟶ xPrev Q j) ×' e.f j = dFrom P j ≫ f + f' ≫ dTo Q j)

Tactic:
subst 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 ℕ
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)
⊢ PSigma.fst (β := fun (f' : P.X 0 ⟶ xPrev Q 0) ↦
        e.f 0 =
          dFrom P 0 ≫
              PSigma.fst (β := 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)
                (mkInductiveAux₂ e zero comm_zero one comm_one succ 0) +
            f' ≫ dTo Q 0)
        (PSigma.snd (β := 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)
          (mkInductiveAux₂ e zero comm_zero one comm_one succ 0)) ≫
      (xPrevIso Q ⋯).hom =
    (xNextIso P ⋯).inv ≫
      PSigma.fst (β := fun (f : xNext P (HAdd.hAdd (α := ℕ) 0 1) ⟶ Q.X (HAdd.hAdd (α := ℕ) 0 1)) ↦
        (f' : P.X (HAdd.hAdd (α := ℕ) 0 1) ⟶ xPrev Q (HAdd.hAdd (α := ℕ) 0 1)) ×'
          e.f (HAdd.hAdd (α := ℕ) 0 1) = dFrom P (HAdd.hAdd (α := ℕ) 0 1) ≫ f + f' ≫ dTo Q (HAdd.hAdd (α := ℕ) 0 1))
        (mkInductiveAux₂ e zero comm_zero one comm_one succ (HAdd.hAdd (α := ℕ) 0 1))

Tactic:
simp [mkInductiveAux₂]

Premises used: Homotopy.mkInductiveAux₂
-- 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)
⊢ PSigma.fst (β := fun (f' : P.X (HAdd.hAdd (α := ℕ) 0 1) ⟶ xPrev Q (HAdd.hAdd (α := ℕ) 0 1)) ↦
        e.f (HAdd.hAdd (α := ℕ) 0 1) =
          dFrom P (HAdd.hAdd (α := ℕ) 0 1) ≫
              PSigma.fst (β := fun (f : xNext P (HAdd.hAdd (α := ℕ) 0 1) ⟶ Q.X (HAdd.hAdd (α := ℕ) 0 1)) ↦
                (f' : P.X (HAdd.hAdd (α := ℕ) 0 1) ⟶ xPrev Q (HAdd.hAdd (α := ℕ) 0 1)) ×'
                  e.f (HAdd.hAdd (α := ℕ) 0 1) =
                    dFrom P (HAdd.hAdd (α := ℕ) 0 1) ≫ f + f' ≫ dTo Q (HAdd.hAdd (α := ℕ) 0 1))
                (mkInductiveAux₂ e zero comm_zero one comm_one succ (HAdd.hAdd (α := ℕ) 0 1)) +
            f' ≫ dTo Q (HAdd.hAdd (α := ℕ) 0 1))
        (PSigma.snd (β := fun (f : xNext P (HAdd.hAdd (α := ℕ) 0 1) ⟶ Q.X (HAdd.hAdd (α := ℕ) 0 1)) ↦
          (f' : P.X (HAdd.hAdd (α := ℕ) 0 1) ⟶ xPrev Q (HAdd.hAdd (α := ℕ) 0 1)) ×'
            e.f (HAdd.hAdd (α := ℕ) 0 1) = dFrom P (HAdd.hAdd (α := ℕ) 0 1) ≫ f + f' ≫ dTo Q (HAdd.hAdd (α := ℕ) 0 1))
          (mkInductiveAux₂ e zero comm_zero one comm_one succ (HAdd.hAdd (α := ℕ) 0 1))) ≫
      (xPrevIso Q ⋯).hom =
    (xNextIso P ⋯).inv ≫
      PSigma.fst (β := fun (f : xNext P (HAdd.hAdd (α := ℕ) 0 1 + 1) ⟶ Q.X (HAdd.hAdd (α := ℕ) 0 1 + 1)) ↦
        (f' : P.X (HAdd.hAdd (α := ℕ) 0 1 + 1) ⟶ xPrev Q (HAdd.hAdd (α := ℕ) 0 1 + 1)) ×'
          e.f (HAdd.hAdd (α := ℕ) 0 1 + 1) =
            dFrom P (HAdd.hAdd (α := ℕ) 0 1 + 1) ≫ f + f' ≫ dTo Q (HAdd.hAdd (α := ℕ) 0 1 + 1))
        (mkInductiveAux₂ e zero comm_zero one comm_one succ (HAdd.hAdd (α := ℕ) 0 1 + 1))

Tactic:
simp [mkInductiveAux₂]

Premises used: Homotopy.mkInductiveAux₂
-- 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)
i : ℕ
⊢ PSigma.fst (β := fun (f' : P.X (i + 1 + 1) ⟶ xPrev Q (i + 1 + 1)) ↦
        e.f (i + 1 + 1) =
          dFrom P (i + 1 + 1) ≫
              PSigma.fst (β := fun (f : xNext P (i + 1 + 1) ⟶ Q.X (i + 1 + 1)) ↦
                (f' : P.X (i + 1 + 1) ⟶ xPrev Q (i + 1 + 1)) ×'
                  e.f (i + 1 + 1) = dFrom P (i + 1 + 1) ≫ f + f' ≫ dTo Q (i + 1 + 1))
                (mkInductiveAux₂ e zero comm_zero one comm_one succ (i + 1 + 1)) +
            f' ≫ dTo Q (i + 1 + 1))
        (PSigma.snd (β := fun (f : xNext P (i + 1 + 1) ⟶ Q.X (i + 1 + 1)) ↦
          (f' : P.X (i + 1 + 1) ⟶ xPrev Q (i + 1 + 1)) ×'
            e.f (i + 1 + 1) = dFrom P (i + 1 + 1) ≫ f + f' ≫ dTo Q (i + 1 + 1))
          (mkInductiveAux₂ e zero comm_zero one comm_one succ (i + 1 + 1))) ≫
      (xPrevIso Q ⋯).hom =
    (xNextIso P ⋯).inv ≫
      PSigma.fst (β := fun (f : xNext P (i + 1 + 1 + 1) ⟶ Q.X (i + 1 + 1 + 1)) ↦
        (f' : P.X (i + 1 + 1 + 1) ⟶ xPrev Q (i + 1 + 1 + 1)) ×'
          e.f (i + 1 + 1 + 1) = dFrom P (i + 1 + 1 + 1) ≫ f + f' ≫ dTo Q (i + 1 + 1 + 1))
        (mkInductiveAux₂ e zero comm_zero one comm_one succ (i + 1 + 1 + 1))

Tactic:
simp [mkInductiveAux₂]

Premises used: Homotopy.mkInductiveAux₂
-- 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 : ι
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)
i j : ℕ
w : ¬(ComplexShape.down ℕ).Rel j i
hnc : ¬i + 1 = j
⊢ Eq.{v + 1} (α := P.X i ⟶ Q.X j)
    (if h : i + 1 = j then
      (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : xNext P i ⟶ Q.X i) ↦
              (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i).fst
          (β := fun (f' : P.X i ⟶ xPrev Q i) ↦
          e.f i =
            dFrom P i ≫
                (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : xNext P i ⟶ Q.X i) ↦
                  (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i) +
              f' ≫ dTo Q i) ≫
        (xPrevIso Q h).hom
    else 0)
    0

Tactic:
rw [dif_neg]

Premises used: dif_neg
-- 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 : ι
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)
i j : ℕ
w : ¬(ComplexShape.down ℕ).Rel j i
⊢ ¬i + 1 = j

Tactic:
w
-- 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 : ι
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)
i j : ℕ
w : ¬(ComplexShape.down ℕ).Rel j i
⊢ ¬i + 1 = j

Tactic:
exact w
-- 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 : ι
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)
i : ℕ
⊢ e.f i =
    HAdd.hAdd (α := P.X i ⟶ Q.X i) (β := P.X i ⟶ Q.X i)
      (dFrom P i ≫
        (fromNext i : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → xNext P i ⟶ Q.X i) fun (i j : ℕ) ↦
          if h : i + 1 = j then
            (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : xNext P i ⟶ Q.X i) ↦
                    (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i).fst
                (β := fun (f' : P.X i ⟶ xPrev Q i) ↦
                e.f i =
                  dFrom P i ≫
                      (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : xNext P i ⟶ Q.X i) ↦
                        (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i) +
                    f' ≫ dTo Q i) ≫
              (xPrevIso Q h).hom
          else 0)
      (((toPrev i : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → P.X i ⟶ xPrev Q i) fun (i j : ℕ) ↦
            if h : i + 1 = j then
              (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : xNext P i ⟶ Q.X i) ↦
                      (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i).fst
                  (β := fun (f' : P.X i ⟶ xPrev Q i) ↦
                  e.f i =
                    dFrom P i ≫
                        (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : xNext P i ⟶ Q.X i) ↦
                          (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i) +
                      f' ≫ dTo Q i) ≫
                (xPrevIso Q h).hom
            else 0) ≫
          dTo Q i :
        P.X i ⟶ Q.X i)

Tactic:
(mkInductiveAux₂ e zero comm_zero one comm_one succ i).2.2.trans ?_

Premises used: PSigma.snd, Homotopy.mkInductiveAux₂, Eq.trans
-- 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)
⊢ Eq (α := xNext P 0 ⟶ Q.X 0)
    (PSigma.fst (β := 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)
      (mkInductiveAux₂ e zero comm_zero one comm_one succ 0))
    ((fromNext 0 : (a : (i j : ℕ) → P.X i ⟶ Q.X j) → xNext P 0 ⟶ Q.X 0) fun (i j : ℕ) ↦
      if h : i + 1 = j then
        (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd (β := fun (f : xNext P i ⟶ Q.X i) ↦
                (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i).fst
            (β := fun (f' : P.X i ⟶ xPrev Q i) ↦
            e.f i =
              dFrom P i ≫
                  (mkInductiveAux₂ e zero comm_zero one comm_one succ i).fst (β := fun (f : xNext P i ⟶ Q.X i) ↦
                    (f' : P.X i ⟶ xPrev Q i) ×' e.f i = dFrom P i ≫ f + f' ≫ dTo Q i) +
                f' ≫ dTo Q i) ≫
          (xPrevIso Q h).hom
      else 0)

Tactic:
dsimp [fromNext, mkInductiveAux₂]

Premises used: fromNext, Homotopy.mkInductiveAux₂
-- 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 : ℕ
e_a :
  eqToHom ⋯ ≫
      (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)) =
    𝟙 (xNext P (n + 1)) ≫
      eqToHom ⋯ ≫
        (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))
⊢ 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)) =
    (xNextIso P ⋯).inv ≫
      PSigma.fst (β := 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))
        (mkInductiveAux₂ e zero comm_zero one comm_one succ (n + 1))

Tactic:
dsimp [xNextIso]

Premises used: HomologicalComplex.xNextIso
-- 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 : ℕ
e_a e_a₁ :
  eqToHom ⋯ ≫
      (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)) =
    eqToHom ⋯ ≫
      (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))
⊢ eqToHom ⋯ ≫
      (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)) =
    𝟙 (xNext P (n + 1)) ≫
      eqToHom ⋯ ≫
        (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))

Tactic:
rw [id_comp]

Premises used: CategoryTheory.Category.id_comp