-- Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean
theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0

Proof state:
case h.mk.e_a.H
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (i, j).2 ≤ (i, j).1.castSucc

Tactic:
simpa [S] using hij

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (∑ i : Fin (n + 1 + 2), (-1) ^ ↑i • X.δ i) ≫ ∑ i : Fin (n + 2), (-1) ^ ↑i • X.δ i = 0

Tactic:
simp only [comp_sum, sum_comp, ← Finset.sum_product']

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ ∑ x ∈ Finset.univ ×ˢ Finset.univ, ((-1) ^ ↑x.2 • X.δ x.2) ≫ ((-1) ^ ↑x.1 • X.δ x.1) = 0

Proof state:
case i_surj
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
⊢ ∀ b ∈ Sᶜ, ∃ a, ∃ (ha : a ∈ S), φ a ha = b

Tactic:
rintro ⟨i', j'⟩ hij'

Result:
case i_surj.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ Sᶜ
⊢ ∃ a, ∃ (ha : a ∈ S), φ a ha = (i', j')

Proof state:
case h.mk.e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (-1) ^ ↑i * (-1) ^ ↑j = (-1) ^ ↑(j.castLT ⋯) * (-1) ^ ↑i

Tactic:
apply mul_comm

Result:
no goals

Proof state:
case hi
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
ij : P
hij : ↑ij.2 ≤ ↑ij.1
⊢ ¬↑ij.1 + 1 ≤ ↑ij.2

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
⊢ ∑ i ∈ S, ((-1) ^ ↑i.2 • X.δ i.2) ≫ ((-1) ^ ↑i.1 • X.δ i.1) =
    ∑ x ∈ Sᶜ, -((-1) ^ ↑x.2 • X.δ x.2) ≫ ((-1) ^ ↑x.1 • X.δ x.1)

Tactic:
apply Finset.sum_bij φ

Result:
case hi
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
⊢ ∀ (a : P) (ha : a ∈ S), φ a ha ∈ Sᶜ

case i_inj
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
⊢ ∀ (a₁ : P) (ha₁ : a₁ ∈ S) (a₂ : P) (ha₂ : a₂ ∈ S), φ a₁ ha₁ = φ a₂ ha₂ → a₁ = a₂

case i_surj
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
⊢ ∀ b ∈ Sᶜ, ∃ a, ∃ (ha : a ∈ S), φ a ha = b

case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
⊢ ∀ (a : P) (ha : a ∈ S),
    ((-1) ^ ↑a.2 • X.δ a.2) ≫ ((-1) ^ ↑a.1 • X.δ a.1) =
      -((-1) ^ ↑(φ a ha).2 • X.δ (φ a ha).2) ≫ ((-1) ^ ↑(φ a ha).1 • X.δ (φ a ha).1)

Proof state:
case i_inj.mk.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ (i, j) = (i', j')

Tactic:
rw [Prod.mk.inj_iff]

Result:
case i_inj.mk.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ i = i' ∧ j = j'

Proof state:
case i_inj.mk.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ i = i' ∧ j = j'

Tactic:
exact ⟨by simpa [φ] using congr_arg Prod.snd h,
  by simpa [φ, Fin.castSucc_castLT] using congr_arg Fin.castSucc (congr_arg Prod.fst h)⟩

Result:
no goals

Proof state:
case h.mk
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ ((-1) ^ ↑i * (-1) ^ ↑j) • X.δ j ≫ X.δ i =
    -((-1) ^ ↑(φ (i, j) hij).1 * (-1) ^ ↑(φ (i, j) hij).2) • X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1

Tactic:
congr 1

Result:
case h.mk.e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (-1) ^ ↑i * (-1) ^ ↑j = -((-1) ^ ↑(φ (i, j) hij).1 * (-1) ^ ↑(φ (i, j) hij).2)

case h.mk.e_a
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.2 ≤ ↑ij.1) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (ij.2.castLT ⋯, ij.1.succ)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ X.δ j ≫ X.δ i = X.δ (φ (i, j) hij).2 ≫ X.δ (φ (i, j) hij).1