awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
        f'' ≫ Q.d (n + 2) (n + 1) =
          P.d (n + 2) (n + 1) ≫
            p.snd (β := fun (f : P.X n ⟶ Q.X n) ↦
                  (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f).fst
              (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
              f' ≫ Q.d (n + 1) n =
                P.d (n + 1) n ≫
                  p.fst (β := fun (f : P.X n ⟶ Q.X n) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f))
m : ℕ
⊢ Eq (α := P.X (m + 1) ⟶ Q.X m)
    (PSigma.fst (β := fun (f : P.X (m + 1) ⟶ Q.X (m + 1)) ↦
        (f' : P.X (m + 1 + 1) ⟶ Q.X (m + 1 + 1)) ×' f' ≫ Q.d (m + 1 + 1) (m + 1) = P.d (m + 1 + 1) (m + 1) ≫ f)
        (P.mkHomAux Q zero one one_zero_comm succ (m + 1)) ≫
      Q.d (m + 1) m)
    (P.d (m + 1) m ≫
      (P.mkHomAux Q zero one one_zero_comm succ m).fst (β := fun (f : P.X m ⟶ Q.X m) ↦
        (f' : P.X (m + 1) ⟶ Q.X (m + 1)) ×' f' ≫ Q.d (m + 1) m = P.d (m + 1) m ≫ f))

Tactic:
exact (mkHomAux P Q zero one one_zero_comm succ m).2.2

Premises used: PSigma.snd, ChainComplex.mkHomAux
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
        f'' ≫ Q.d (n + 2) (n + 1) =
          P.d (n + 2) (n + 1) ≫
            p.snd (β := fun (f : P.X n ⟶ Q.X n) ↦
                  (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f).fst
              (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
              f' ≫ Q.d (n + 1) n =
                P.d (n + 1) n ≫
                  p.fst (β := fun (f : P.X n ⟶ Q.X n) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f))
⊢ (P.mkHom Q zero one one_zero_comm succ).f 0 = zero

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
        f'' ≫ Q.d (n + 2) (n + 1) =
          P.d (n + 2) (n + 1) ≫
            p.snd (β := fun (f : P.X n ⟶ Q.X n) ↦
                  (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f).fst
              (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
              f' ≫ Q.d (n + 1) n =
                P.d (n + 1) n ≫
                  p.fst (β := fun (f : P.X n ⟶ Q.X n) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f))
⊢ (P.mkHom Q zero one one_zero_comm succ).f 1 = one

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
P Q : ChainComplex.{v, u, 0} V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : one ≫ Q.d 1 0 = P.d 1 0 ≫ zero
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
        f'' ≫ Q.d (n + 2) (n + 1) =
          P.d (n + 2) (n + 1) ≫
            p.snd (β := fun (f : P.X n ⟶ Q.X n) ↦
                  (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f).fst
              (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
              f' ≫ Q.d (n + 1) n =
                P.d (n + 1) n ≫
                  p.fst (β := fun (f : P.X n ⟶ Q.X n) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f))
n : ℕ
⊢ (P.mkHom Q zero one one_zero_comm succ).f (n + 2) =
    PSigma.fst (β := fun (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ↦
      Eq (α := P.X (n + 2) ⟶ Q.X (n + 1)) (f'' ≫ Q.d (n + 2) (n + 1))
        (CategoryStruct.comp (Y := P.X (n + 1)) (P.d (n + 2) (n + 1))
          (PSigma.fst (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
            f' ≫ Q.d (n + 1) n =
              P.d (n + 1) n ≫
                PSigma.fst (β := fun (f : P.X n ⟶ Q.X n) ↦
                  (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f)
                  (PSigma.mk (β := fun (f : P.X n ⟶ Q.X n) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f)
                    ((P.mkHom Q zero one one_zero_comm succ).f n)
                    (PSigma.mk (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
                      f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ (P.mkHom Q zero one one_zero_comm succ).f n)
                      ((P.mkHom Q zero one one_zero_comm succ).f (n + 1)) ⋯)))
            (PSigma.snd (β := fun (f : P.X n ⟶ Q.X n) ↦
              (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f)
              (PSigma.mk (β := fun (f : P.X n ⟶ Q.X n) ↦
                (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f)
                ((P.mkHom Q zero one one_zero_comm succ).f n)
                (PSigma.mk (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
                  f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ (P.mkHom Q zero one one_zero_comm succ).f n)
                  ((P.mkHom Q zero one one_zero_comm succ).f (n + 1)) ⋯))))))
      (succ n
        (PSigma.mk (β := fun (f : P.X n ⟶ Q.X n) ↦
          (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ f)
          ((P.mkHom Q zero one one_zero_comm succ).f n)
          (PSigma.mk (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
            f' ≫ Q.d (n + 1) n = P.d (n + 1) n ≫ (P.mkHom Q zero one one_zero_comm succ).f n)
            ((P.mkHom Q zero one one_zero_comm succ).f (n + 1)) ⋯)))

Tactic:
dsimp [mkHom, mkHomAux]

Premises used: ChainComplex.mkHom, ChainComplex.mkHomAux
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
i j : α
h : i + 1 = j
rw rw₁ : X j = X j
⊢ X (i + 1) = X j

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
dsimp :
  i + 1 = j →
    j + 1 = k →
      Eq.{v + 1} (α := X i ⟶ X k)
        (CategoryStruct.comp (Y := X j) (if h : i + 1 = j then d i ≫ eqToHom ⋯ else 0)
          (if h : j + 1 = k then d j ≫ eqToHom ⋯ else 0))
        0
⊢ (ComplexShape.up α).Rel i j → (ComplexShape.up α).Rel j k → of.d X d i j ≫ of.d X d j k = 0

Tactic:
dsimp [of.d]

Premises used: CochainComplex.of.d
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
pos : ∀ (h : i + 1 = j) (h' : j + 1 = k), i + 1 = j → j + 1 = k → (d i ≫ eqToHom ⋯) ≫ d j ≫ eqToHom ⋯ = 0
neg : ∀ (h : i + 1 = j) (h' : ¬j + 1 = k), i + 1 = j → j + 1 = k → Eq.{v + 1} (α := X i ⟶ X k) ((d i ≫ eqToHom ⋯) ≫ 0) 0
pos₁ : ∀ (h : ¬i + 1 = j) (h' : j + 1 = k), i + 1 = j → j + 1 = k → Eq.{v + 1} (α := X i ⟶ X k) (0 ≫ d j ≫ eqToHom ⋯) 0
neg₁ :
  ∀ (h : ¬i + 1 = j) (h' : ¬j + 1 = k),
    i + 1 = j → j + 1 = k → Eq.{v + 1} (α := X i ⟶ X k) (CategoryStruct.comp (Y := X j) 0 0) 0
⊢ i + 1 = j →
    j + 1 = k →
      Eq.{v + 1} (α := X i ⟶ X k)
        (CategoryStruct.comp (Y := X j) (if h : i + 1 = j then d i ≫ eqToHom ⋯ else 0)
          (if h : j + 1 = k then d j ≫ eqToHom ⋯ else 0))
        0

Tactic:
split_ifs with h h' h'
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : i + 1 = j
h' : j + 1 = k
pos : i + 1 = i + 1 → i + 1 + 1 = i + 1 + 1 → (d i ≫ eqToHom ⋯) ≫ d (i + 1) ≫ eqToHom ⋯ = 0
⊢ i + 1 = j → j + 1 = k → (d i ≫ eqToHom ⋯) ≫ d j ≫ eqToHom ⋯ = 0

Tactic:
substs h h'
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i : α
⊢ i + 1 = i + 1 → i + 1 + 1 = i + 1 + 1 → (d i ≫ eqToHom ⋯) ≫ d (i + 1) ≫ eqToHom ⋯ = 0

Tactic:
simp [sq]
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : i + 1 = j
h' : ¬j + 1 = k
⊢ i + 1 = j → j + 1 = k → Eq.{v + 1} (α := X i ⟶ X k) ((d i ≫ eqToHom ⋯) ≫ 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : ¬i + 1 = j
h' : j + 1 = k
⊢ i + 1 = j → j + 1 = k → Eq.{v + 1} (α := X i ⟶ X k) (0 ≫ d j ≫ eqToHom ⋯) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
i j k : α
h : ¬i + 1 = j
h' : ¬j + 1 = k
⊢ i + 1 = j → j + 1 = k → Eq.{v + 1} (α := X i ⟶ X k) (CategoryStruct.comp (Y := X j) 0 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
sq : ∀ (n : α), d n ≫ d (n + 1) = 0
⊢ (of X d sq).X = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
j : α
dsimp : (if j + 1 = j + 1 then d j ≫ 𝟙 (X (j + 1)) else 0) = d j
⊢ of.d X d j (j + 1) = d j

Tactic:
dsimp [of.d]

Premises used: CochainComplex.of.d
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
j : α
rw : d j ≫ 𝟙 (X (j + 1)) = d j
rw₁ rw₂ : d j = d j
⊢ (if j + 1 = j + 1 then d j ≫ 𝟙 (X (j + 1)) else 0) = d j

Tactic:
rw [if_pos rfl, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, if_pos, rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
i j : α
h : i + 1 ≠ j
⊢ of.d X d i j = 0

Tactic:
simp [of.d, dif_neg h]

Premises used: CochainComplex.of.d, dif_neg
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
α : Type u_2
inst_2 : AddRightCancelSemigroup α
inst_3 : One α
inst_4 : DecidableEq α
X_1 : α → V
d_X : (n : α) → X_1 n ⟶ X_1 (n + 1)
sq_X : ∀ (n : α), d_X n ≫ d_X (n + 1) = 0
Y_1 : α → V
d_Y : (n : α) → Y_1 n ⟶ Y_1 (n + 1)
sq_Y : ∀ (n : α), d_Y n ≫ d_Y (n + 1) = 0
X Y : CochainComplex.{v, u, u_2} V α
f : (i : α) → X.X i ⟶ Y.X i
comm : ∀ (i : α), Eq (α := X.X i ⟶ Y.X (i + 1)) (f i ≫ Y.d i (i + 1)) (X.d i (i + 1) ≫ f (i + 1))
n : α
⊢ Eq (α := X.X n ⟶ Y.X (n + 1)) (f n ≫ Y.d n (n + 1)) (X.d n (n + 1) ≫ f (n + 1))

Tactic:
simpa using comm n
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex.{v, u} V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).X 0 = X₀

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex.{v, u} V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).X 1 = X₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex.{v, u} V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).X 2 = X₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex.{v, u} V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
change : (if 1 = HAdd.hAdd (α := ℕ) 0 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 0 1 = d₀

Tactic:
change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀

Premises used: CategoryTheory.CategoryStruct.id, HAdd.hAdd, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, Eq, ite
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex.{v, u} V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
rw : d₀ ≫ 𝟙 X₁ = d₀
rw₁ rw₂ : d₀ = d₀
⊢ (if 1 = HAdd.hAdd (α := ℕ) 0 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀

Tactic:
rw [if_pos rfl, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, if_pos, rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex.{v, u} V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
change : (if 2 = HAdd.hAdd (α := ℕ) 1 1 then d₁ ≫ 𝟙 X₂ else 0) = d₁
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).d 1 2 = d₁

Tactic:
change ite (2 = 1 + 1) (d₁ ≫ 𝟙 X₂) 0 = d₁

Premises used: CategoryTheory.CategoryStruct.id, HAdd.hAdd, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, Eq, ite
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ X₂ : V
d₀ : X₀ ⟶ X₁
d₁ : X₁ ⟶ X₂
s : d₀ ≫ d₁ = 0
succ : (S : ShortComplex.{v, u} V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0
rw : d₁ ≫ 𝟙 X₂ = d₁
rw₁ rw₂ : d₁ = d₁
⊢ (if 2 = HAdd.hAdd (α := ℕ) 1 1 then d₁ ≫ 𝟙 X₂ else 0) = d₁

Tactic:
rw [if_pos rfl, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, if_pos, rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₀ ⟶ X₁
succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0
⊢ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 0 = X₀

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₀ ⟶ X₁
succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0
⊢ HomologicalComplex.X (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 1 = X₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₀ ⟶ X₁
succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0
change : (if 1 = HAdd.hAdd (α := ℕ) 0 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀
⊢ HomologicalComplex.d (mk' X₀ X₁ d₀ fun {X₀ X₁ : V} ↦ succ') 0 1 = d₀

Tactic:
change ite (1 = 0 + 1) (d₀ ≫ 𝟙 X₁) 0 = d₀

Premises used: CategoryTheory.CategoryStruct.id, HAdd.hAdd, CategoryTheory.CategoryStruct.comp, OfNat.ofNat, Eq, ite
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
X₀ X₁ : V
d₀ : X₀ ⟶ X₁
succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' f ≫ d = 0
rw : d₀ ≫ 𝟙 X₁ = d₀
rw₁ rw₂ : d₀ = d₀
⊢ (if 1 = HAdd.hAdd (α := ℕ) 0 1 then d₀ ≫ 𝟙 X₁ else 0) = d₀

Tactic:
rw [if_pos rfl, Category.comp_id]

Premises used: CategoryTheory.Category.comp_id, if_pos, rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
P Q : CochainComplex.{v, u, 0} V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
        p.snd (β := fun (f : P.X n ⟶ Q.X n) ↦
                  (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f').fst
              (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
              p.fst (β := fun (f : P.X n ⟶ Q.X n) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') ≫
                  Q.d n (n + 1) =
                P.d n (n + 1) ≫ f') ≫
            Q.d (n + 1) (n + 2) =
          P.d (n + 1) (n + 2) ≫ f''
n : ℕ
⊢ Eq (α := P.X n ⟶ Q.X (n + 1))
    ((P.mkHomAux Q zero one one_zero_comm succ n).fst (β := fun (f : P.X n ⟶ Q.X n) ↦
        (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') ≫
      Q.d n (n + 1))
    (P.d n (n + 1) ≫
      PSigma.fst (β := fun (f : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
        (f' : P.X (n + 1 + 1) ⟶ Q.X (n + 1 + 1)) ×' f ≫ Q.d (n + 1) (n + 1 + 1) = P.d (n + 1) (n + 1 + 1) ≫ f')
        (P.mkHomAux Q zero one one_zero_comm succ (n + 1)))

Tactic:
(mkHomAux P Q zero one one_zero_comm succ n).2.2

Premises used: PSigma.snd, CochainComplex.mkHomAux
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
ι : Type u_1
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
P Q : CochainComplex.{v, u, 0} V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
        p.snd (β := fun (f : P.X n ⟶ Q.X n) ↦
                  (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f').fst
              (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
              p.fst (β := fun (f : P.X n ⟶ Q.X n) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') ≫
                  Q.d n (n + 1) =
                P.d n (n + 1) ≫ f') ≫
            Q.d (n + 1) (n + 2) =
          P.d (n + 1) (n + 2) ≫ f''
n : ℕ
⊢ Eq (α := P.X n ⟶ Q.X (n + 1))
    ((P.mkHomAux Q zero one one_zero_comm succ n).fst (β := fun (f : P.X n ⟶ Q.X n) ↦
        (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') ≫
      Q.d n (n + 1))
    (P.d n (n + 1) ≫
      PSigma.fst (β := fun (f : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
        (f' : P.X (n + 1 + 1) ⟶ Q.X (n + 1 + 1)) ×' f ≫ Q.d (n + 1) (n + 1 + 1) = P.d (n + 1) (n + 1 + 1) ≫ f')
        (P.mkHomAux Q zero one one_zero_comm succ (n + 1)))

Tactic:
exact (mkHomAux P Q zero one one_zero_comm succ n).2.2

Premises used: PSigma.snd, CochainComplex.mkHomAux
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
P Q : CochainComplex.{v, u, 0} V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
        p.snd (β := fun (f : P.X n ⟶ Q.X n) ↦
                  (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f').fst
              (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
              p.fst (β := fun (f : P.X n ⟶ Q.X n) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') ≫
                  Q.d n (n + 1) =
                P.d n (n + 1) ≫ f') ≫
            Q.d (n + 1) (n + 2) =
          P.d (n + 1) (n + 2) ≫ f''
⊢ (P.mkHom Q zero one one_zero_comm succ).f 0 = zero

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Homology.HomologicalComplex
Goal:
V : Type u
inst : Category.{v, u} V
inst_1 : HasZeroMorphisms.{v, u} V
P Q : CochainComplex.{v, u, 0} V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
        p.snd (β := fun (f : P.X n ⟶ Q.X n) ↦
                  (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f').fst
              (β := fun (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ↦
              p.fst (β := fun (f : P.X n ⟶ Q.X n) ↦
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') ≫
                  Q.d n (n + 1) =
                P.d n (n + 1) ≫ f') ≫
            Q.d (n + 1) (n + 2) =
          P.d (n + 1) (n + 2) ≫ f''
⊢ (P.mkHom Q zero one one_zero_comm succ).f 1 = one

Tactic:
rfl

Premises used: rfl