C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
⊢ (∑ i : Fin (n + 1 + 2), (-1) ^ ↑i • SimplicialObject.δ X i) ≫ ∑ i : Fin (n + 2), (-1) ^ ↑i • SimplicialObject.δ X i =
    0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
⊢ objD X (n + 1) ≫ objD X n = 0
dsimp
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
⊢ ∑ x in Finset.univ ×ˢ Finset.univ,
      ((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst) =
    0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
⊢ (∑ i : Fin (n + 1 + 2), (-1) ^ ↑i • SimplicialObject.δ X i) ≫ ∑ i : Fin (n + 2), (-1) ^ ↑i • SimplicialObject.δ X i =
    0
simp only [comp_sum, sum_comp, ← Finset.sum_product']
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
⊢ ∑ x in Finset.univ ×ˢ Finset.univ,
      ((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst) =
    0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
⊢ ∑ x in Finset.univ ×ˢ Finset.univ,
      ((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst) =
    0
let P := Fin (n + 2) × Fin (n + 3)
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
⊢ ∑ x in Finset.univ ×ˢ Finset.univ,
      ((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst) =
    0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
⊢ ∑ x in Finset.univ ×ˢ Finset.univ,
      ((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst) =
    0
let S := Finset.univ.filter fun ij : P => (ij.2 : ℕ) ≤ (ij.1 : ℕ)
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
⊢ ∑ i in S, ((-1) ^ ↑i.snd • SimplicialObject.δ X i.snd) ≫ ((-1) ^ ↑i.fst • SimplicialObject.δ X i.fst) =
    ∑ x in Sᶜ, -((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst)
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
⊢ ∑ x in Finset.univ ×ˢ Finset.univ,
      ((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst) =
    0
erw [← Finset.sum_add_sum_compl S, ← eq_neg_iff_add_eq_zero, ← Finset.sum_neg_distrib]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
⊢ ∑ i in S, ((-1) ^ ↑i.snd • SimplicialObject.δ X i.snd) ≫ ((-1) ^ ↑i.fst • SimplicialObject.δ X i.fst) =
    ∑ x in Sᶜ, -((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst)
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
⊢ ∑ i in S, ((-1) ^ ↑i.snd • SimplicialObject.δ X i.snd) ≫ ((-1) ^ ↑i.fst • SimplicialObject.δ X i.fst) =
    ∑ x in Sᶜ, -((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst)
let φ : ∀ ij : P, ij ∈ S → P := fun ij hij =>
  (Fin.castLT ij.2 (lt_of_le_of_lt (Finset.mem_filter.mp hij).right (Fin.is_lt ij.1)), ij.1.succ)
case hi
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
⊢ ∀ (a : P) (ha : a ∈ S), φ a ha ∈ Sᶜ

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

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

case i_surj
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
⊢ ∀ (b : P), b ∈ Sᶜ → ∃ a ha, b = φ a ha
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
⊢ ∑ i in S, ((-1) ^ ↑i.snd • SimplicialObject.δ X i.snd) ≫ ((-1) ^ ↑i.fst • SimplicialObject.δ X i.fst) =
    ∑ x in Sᶜ, -((-1) ^ ↑x.snd • SimplicialObject.δ X x.snd) ≫ ((-1) ^ ↑x.fst • SimplicialObject.δ X x.fst)
apply Finset.sum_bij φ
case hi
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
ij : P
hij : ij ∈ S
⊢ φ ij hij ∈ Sᶜ
case hi
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
⊢ ∀ (a : P) (ha : a ∈ S), φ a ha ∈ Sᶜ
intro ij hij
case hi
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
ij : P
hij : ↑ij.snd ≤ ↑ij.fst
⊢ ¬↑ij.fst + 1 ≤ ↑ij.snd
case hi
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
ij : P
hij : ij ∈ S
⊢ φ ij hij ∈ Sᶜ
simp only [Finset.mem_univ, Finset.compl_filter, Finset.mem_filter, true_and_iff, Fin.val_succ,
  Fin.coe_castLT] at hij ⊢
no goals
case hi
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
ij : P
hij : ↑ij.snd ≤ ↑ij.fst
⊢ ¬↑ij.fst + 1 ≤ ↑ij.snd
linarith
case h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ ((-1) ^ ↑(i, j).snd • SimplicialObject.δ X (i, j).snd) ≫ ((-1) ^ ↑(i, j).fst • SimplicialObject.δ X (i, j).fst) =
    -((-1) ^ ↑(φ (i, j) hij).snd • SimplicialObject.δ X (φ (i, j) hij).snd) ≫
        ((-1) ^ ↑(φ (i, j) hij).fst • SimplicialObject.δ X (φ (i, j) hij).fst)
case h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
⊢ ∀ (a : P) (ha : a ∈ S),
    ((-1) ^ ↑a.snd • SimplicialObject.δ X a.snd) ≫ ((-1) ^ ↑a.fst • SimplicialObject.δ X a.fst) =
      -((-1) ^ ↑(φ a ha).snd • SimplicialObject.δ X (φ a ha).snd) ≫
          ((-1) ^ ↑(φ a ha).fst • SimplicialObject.δ X (φ a ha).fst)
rintro ⟨i, j⟩ hij
case h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ ((-1) ^ ↑j • SimplicialObject.δ X j) ≫ ((-1) ^ ↑i • SimplicialObject.δ X i) =
    -((-1) ^ ↑(Fin.succ i) • SimplicialObject.δ X (Fin.succ i)) ≫
        ((-1) ^ ↑j • SimplicialObject.δ X (Fin.castLT j (_ : ↑j < n + 2)))
case h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ ((-1) ^ ↑(i, j).snd • SimplicialObject.δ X (i, j).snd) ≫ ((-1) ^ ↑(i, j).fst • SimplicialObject.δ X (i, j).fst) =
    -((-1) ^ ↑(φ (i, j) hij).snd • SimplicialObject.δ X (φ (i, j) hij).snd) ≫
        ((-1) ^ ↑(φ (i, j) hij).fst • SimplicialObject.δ X (φ (i, j) hij).fst)
dsimp
case h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ ((-1) ^ ↑i * (-1) ^ ↑j) • SimplicialObject.δ X j ≫ SimplicialObject.δ X i =
    -((-1) ^ ↑j * (-1) ^ ↑(Fin.succ i)) •
      SimplicialObject.δ X (Fin.succ i) ≫ SimplicialObject.δ X (Fin.castLT j (_ : ↑j < n + 2))
case h.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ ((-1) ^ ↑j • SimplicialObject.δ X j) ≫ ((-1) ^ ↑i • SimplicialObject.δ X i) =
    -((-1) ^ ↑(Fin.succ i) • SimplicialObject.δ X (Fin.succ i)) ≫
        ((-1) ^ ↑j • SimplicialObject.δ X (Fin.castLT j (_ : ↑j < n + 2)))
simp only [zsmul_comp, comp_zsmul, smul_smul, ← neg_smul]
case h.mk.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (-1) ^ ↑i * (-1) ^ ↑j = -((-1) ^ ↑j * (-1) ^ ↑(Fin.succ i))

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

case h.mk.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ SimplicialObject.δ X j ≫ SimplicialObject.δ X i =
    SimplicialObject.δ X (Fin.succ i) ≫ SimplicialObject.δ X (Fin.castLT j (_ : ↑j < n + 2))
. simp only [Fin.val_succ, pow_add, pow_one, mul_neg, neg_neg, mul_one]
  apply mul_comm
no goals
case h.mk.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ SimplicialObject.δ X j ≫ SimplicialObject.δ X i =
    SimplicialObject.δ X (Fin.succ i) ≫ SimplicialObject.δ X (Fin.castLT j (_ : ↑j < n + 2))
. rw [CategoryTheory.SimplicialObject.δ_comp_δ'']
  simpa using hij
case h.mk.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (-1) ^ ↑i * (-1) ^ ↑j = (-1) ^ ↑j * (-1) ^ ↑i
case h.mk.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (-1) ^ ↑i * (-1) ^ ↑j = -((-1) ^ ↑j * (-1) ^ ↑(Fin.succ i))
simp only [Fin.val_succ, pow_add, pow_one, mul_neg, neg_neg, mul_one]
no goals
case h.mk.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ (-1) ^ ↑i * (-1) ^ ↑j = (-1) ^ ↑j * (-1) ^ ↑i
apply mul_comm
case h.mk.e_a.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ j ≤ ↑Fin.castSucc i
case h.mk.e_a
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ SimplicialObject.δ X j ≫ SimplicialObject.δ X i =
    SimplicialObject.δ X (Fin.succ i) ≫ SimplicialObject.δ X (Fin.castLT j (_ : ↑j < n + 2))
rw [CategoryTheory.SimplicialObject.δ_comp_δ'']
no goals
case h.mk.e_a.H
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
hij : (i, j) ∈ S
⊢ j ≤ ↑Fin.castSucc i
simpa using hij
case i_inj.mk.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij : (i, j) ∈ S
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ (i, j) = (i', j')
case i_inj
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
⊢ ∀ (a₁ a₂ : P) (ha₁ : a₁ ∈ S) (ha₂ : a₂ ∈ S), φ a₁ ha₁ = φ a₂ ha₂ → a₁ = a₂
rintro ⟨i, j⟩ ⟨i', j'⟩ hij hij' h
case i_inj.mk.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij : (i, j) ∈ S
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ i = i' ∧ j = j'
case i_inj.mk.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij : (i, j) ∈ S
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ (i, j) = (i', j')
rw [Prod.mk.inj_iff]
no goals
case i_inj.mk.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij : (i, j) ∈ S
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ i = i' ∧ j = j'
exact ⟨by simpa using congr_arg Prod.snd h,
  by simpa [Fin.castSucc_castLT] using congr_arg Fin.castSucc (congr_arg Prod.fst h)⟩
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij : (i, j) ∈ S
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ i = i'
simpa using congr_arg Prod.snd h
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i : Fin (n + 2)
j : Fin (n + 3)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij : (i, j) ∈ S
hij' : (i', j') ∈ S
h : φ (i, j) hij = φ (i', j') hij'
⊢ j = j'
simpa [Fin.castSucc_castLT] using congr_arg Fin.castSucc (congr_arg Prod.fst h)
case i_surj.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ Sᶜ
⊢ ∃ a ha, (i', j') = φ a ha
case i_surj
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
⊢ ∀ (b : P), b ∈ Sᶜ → ∃ a ha, b = φ a ha
rintro ⟨i', j'⟩ hij'
case i_surj.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ ∃ a ha, (i', j') = φ a ha
case i_surj.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : (i', j') ∈ Sᶜ
⊢ ∃ a ha, (i', j') = φ a ha
simp only [Finset.mem_univ, forall_true_left, Prod.forall, ge_iff_le, Finset.compl_filter,
  not_le, Finset.mem_filter, true_and] at hij'
case i_surj.mk.refine'_1
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ j' ≠ 0

case i_surj.mk.refine'_2
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (Fin.pred j' ?i_surj.mk.refine'_1, ↑Fin.castSucc i') ∈ S

case i_surj.mk.refine'_3
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (i', j') = φ (Fin.pred j' ?i_surj.mk.refine'_1, ↑Fin.castSucc i') ?i_surj.mk.refine'_2
case i_surj.mk
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ ∃ a ha, (i', j') = φ a ha
refine' ⟨(j'.pred _, Fin.castSucc i'), _, _⟩
case i_surj.mk.refine'_2
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (Fin.pred j' (_ : j' = 0 → False), ↑Fin.castSucc i') ∈ S

case i_surj.mk.refine'_3
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (i', j') = φ (Fin.pred j' (_ : j' = 0 → False), ↑Fin.castSucc i') ?i_surj.mk.refine'_2
case i_surj.mk.refine'_1
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ j' ≠ 0

case i_surj.mk.refine'_2
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (Fin.pred j' ?i_surj.mk.refine'_1, ↑Fin.castSucc i') ∈ S

case i_surj.mk.refine'_3
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (i', j') = φ (Fin.pred j' ?i_surj.mk.refine'_1, ↑Fin.castSucc i') ?i_surj.mk.refine'_2
. rintro rfl
  simp only [Fin.val_zero, not_lt_zero'] at hij'
case i_surj.mk.refine'_3
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (i', j') =
    φ (Fin.pred j' (_ : j' = 0 → False), ↑Fin.castSucc i')
      (_ : (Fin.pred j' (_ : j' = 0 → False), ↑Fin.castSucc i') ∈ S)
case i_surj.mk.refine'_2
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (Fin.pred j' (_ : j' = 0 → False), ↑Fin.castSucc i') ∈ S

case i_surj.mk.refine'_3
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (i', j') = φ (Fin.pred j' (_ : j' = 0 → False), ↑Fin.castSucc i') ?i_surj.mk.refine'_2
. simpa only [Finset.mem_univ, forall_true_left, Prod.forall, ge_iff_le, Finset.mem_filter,
    Fin.coe_castSucc, Fin.coe_pred, true_and] using Nat.le_pred_of_lt hij'
no goals
case i_surj.mk.refine'_3
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (i', j') =
    φ (Fin.pred j' (_ : j' = 0 → False), ↑Fin.castSucc i')
      (_ : (Fin.pred j' (_ : j' = 0 → False), ↑Fin.castSucc i') ∈ S)
. simp only [Fin.castLT_castSucc, Fin.succ_pred]
case i_surj.mk.refine'_1
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
hij' : ↑i' < ↑0
⊢ False
case i_surj.mk.refine'_1
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ j' ≠ 0
rintro rfl
no goals
case i_surj.mk.refine'_1
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
hij' : ↑i' < ↑0
⊢ False
simp only [Fin.val_zero, not_lt_zero'] at hij'
no goals
case i_surj.mk.refine'_2
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (Fin.pred j' (_ : j' = 0 → False), ↑Fin.castSucc i') ∈ S
simpa only [Finset.mem_univ, forall_true_left, Prod.forall, ge_iff_le, Finset.mem_filter,
  Fin.coe_castSucc, Fin.coe_pred, true_and] using Nat.le_pred_of_lt hij'
no goals
case i_surj.mk.refine'_3
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X Y : SimplicialObject C
n : ℕ
P : Type := Fin (n + 2) × Fin (n + 3)
S : Finset P := Finset.filter (fun ij => ↑ij.snd ≤ ↑ij.fst) Finset.univ
φ : (ij : P) → ij ∈ S → P := fun ij hij => (Fin.castLT ij.snd (_ : ↑ij.snd < n + 2), Fin.succ ij.fst)
i' : Fin (n + 2)
j' : Fin (n + 3)
hij' : ↑i' < ↑j'
⊢ (i', j') =
    φ (Fin.pred j' (_ : j' = 0 → False), ↑Fin.castSucc i')
      (_ : (Fin.pred j' (_ : j' = 0 → False), ↑Fin.castSucc i') ∈ S)
simp only [Fin.castLT_castSucc, Fin.succ_pred]