case h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i : Δ' ⟶ [n]
hi : Mono i
h₁ : len Δ' ≠ n
h₂ : ¬Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
induction' Δ' using SimplexCategory.rec with m
case h.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : len [n] = len [m] + k + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
case h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i fun h => by
      rw [← h] at h₁
      exact h₁ rfl)
case h.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : n = m + k + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
case h.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : len [n] = len [m] + k + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
simp only [len_mk] at hk
case h.intro.zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
hk : n = m + Nat.zero + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0

case h.intro.succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : n = m + Nat.succ k + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
case h.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : n = m + k + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
rcases k with _|k
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [n] ≠ n
h₂ : ¬Isδ₀ i
h : [n] = [m]
⊢ False
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
h : [n] = [m]
⊢ False
rw [← h] at h₁
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [n] ≠ n
h₂ : ¬Isδ₀ i
h : [n] = [m]
⊢ False
exact h₁ rfl
case h.intro.zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
hk : n = m + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
case h.intro.zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
hk : n = m + Nat.zero + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
change n = m + 1 at hk
case h.intro.zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i✝ : Δ' ⟶ [m + 1]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i✝
i : [m] ⟶ [m + 1]
hi : Mono i
h₁ : len [m] ≠ m + 1
h₂ : ¬Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map i.op = 0
case h.intro.zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
hk : n = m + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
subst hk
case h.intro.zero.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬Isδ₀ (SimplexCategory.δ j)
⊢ HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0
case h.intro.zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i✝ : Δ' ⟶ [m + 1]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i✝
i : [m] ⟶ [m + 1]
hi : Mono i
h₁ : len [m] ≠ m + 1
h₂ : ¬Isδ₀ i
⊢ HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map i.op = 0
obtain ⟨j, rfl⟩ := eq_δ_of_mono i
case h.intro.zero.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
⊢ HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0
case h.intro.zero.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬Isδ₀ (SimplexCategory.δ j)
⊢ HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0
rw [Isδ₀.iff] at h₂
case h.intro.zero.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h₃ : 1 ≤ ↑j
⊢ HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0
case h.intro.zero.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
⊢ HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0
have h₃ : 1 ≤ (j : ℕ) := by
  by_contra h
  exact h₂ (by simpa only [Fin.ext_iff, not_le, Nat.lt_one_iff] using h)
no goals
case h.intro.zero.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h₃ : 1 ≤ ↑j
⊢ HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0
exact (HigherFacesVanish.of_P (m + 1) m).comp_δ_eq_zero j h₂ (by linarith)
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h : ¬1 ≤ ↑j
⊢ False
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
⊢ 1 ≤ ↑j
by_contra h
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h : ¬1 ≤ ↑j
⊢ False
exact h₂ (by simpa only [Fin.ext_iff, not_le, Nat.lt_one_iff] using h)
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h : ¬1 ≤ ↑j
⊢ j = 0
simpa only [Fin.ext_iff, not_le, Nat.lt_one_iff] using h
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m : ℕ
i : Δ' ⟶ [m + 1]
hi✝ : Mono i
h₁✝ : len Δ' ≠ m + 1
h₂✝ : ¬Isδ₀ i
h₁ : len [m] ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h₃ : 1 ≤ ↑j
⊢ m + 2 ≤ ↑j + (m + 1)
linarith
case h.intro.succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : n = m + k + 1 + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
case h.intro.succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : n = m + Nat.succ k + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
simp only [Nat.succ_eq_add_one, ← add_assoc] at hk
case h.intro.succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi : Mono i✝
h₁✝ : len Δ' ≠ n
h₂ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
h₁ : len [m] ≠ n
k : ℕ
hk : n = m + k + 1 + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
case h.intro.succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi✝ : Mono i✝
h₁✝ : len Δ' ≠ n
h₂✝ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
hi : Mono i
h₁ : len [m] ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : n = m + k + 1 + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
clear h₂ hi
case h.intro.succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
i : [m] ⟶ [m + k + 1 + 1]
h₁ : len [m] ≠ m + k + 1 + 1
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map i.op = 0
case h.intro.succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
i✝ : Δ' ⟶ [n]
hi : Mono i✝
h₁✝ : len Δ' ≠ n
h₂ : ¬Isδ₀ i✝
m : ℕ
i : [m] ⟶ [n]
h₁ : len [m] ≠ n
k : ℕ
hk : n = m + k + 1 + 1
⊢ HomologicalComplex.Hom.f PInfty n ≫ X.map i.op = 0
subst hk
case h.intro.succ.intro.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : [m] ⟶ [m + k + 1]
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map (i ≫ SimplexCategory.δ j₁).op = 0
case h.intro.succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
i : [m] ⟶ [m + k + 1 + 1]
h₁ : len [m] ≠ m + k + 1 + 1
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map i.op = 0
obtain ⟨j₁ : Fin (_ + 1), i, rfl⟩ :=
  eq_comp_δ_of_not_surjective i fun h => by
    have h' := len_le_of_epi (SimplexCategory.epi_iff_surjective.2 h)
    dsimp at h'
    linarith
case h.intro.succ.intro.intro.intro.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0
case h.intro.succ.intro.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : [m] ⟶ [m + k + 1]
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map (i ≫ SimplexCategory.δ j₁).op = 0
obtain ⟨j₂, i, rfl⟩ :=
  eq_comp_δ_of_not_surjective i fun h => by
    have h' := len_le_of_epi (SimplexCategory.epi_iff_surjective.2 h)
    dsimp at h'
    linarith
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : j₁ = 0
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0

case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0
case h.intro.succ.intro.intro.intro.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0
by_cases hj₁ : j₁ = 0
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : j₁ = 0
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0

case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0
. subst hj₁
  rw [assoc, ← SimplexCategory.δ_comp_δ'' (Fin.zero_le _)]
  simp only [op_comp, X.map_comp, assoc, PInfty_f]
  erw [(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ j₂.succ_ne_zero, zero_comp]
  simp only [Nat.succ_eq_add_one, Nat.add, Fin.succ]
  linarith
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
i : [m] ⟶ [m + k + 1 + 1]
h₁ : len [m] ≠ m + k + 1 + 1
h : Function.Surjective ↑(Hom.toOrderHom i)
h' : len [m + k + 1 + 1] ≤ len [m]
⊢ False
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
i : [m] ⟶ [m + k + 1 + 1]
h₁ : len [m] ≠ m + k + 1 + 1
h : Function.Surjective ↑(Hom.toOrderHom i)
⊢ False
have h' := len_le_of_epi (SimplexCategory.epi_iff_surjective.2 h)
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
i : [m] ⟶ [m + k + 1 + 1]
h₁ : len [m] ≠ m + k + 1 + 1
h : Function.Surjective ↑(Hom.toOrderHom i)
h' : m + k + 1 + 1 ≤ m
⊢ False
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
i : [m] ⟶ [m + k + 1 + 1]
h₁ : len [m] ≠ m + k + 1 + 1
h : Function.Surjective ↑(Hom.toOrderHom i)
h' : len [m + k + 1 + 1] ≤ len [m]
⊢ False
dsimp at h'
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
i : [m] ⟶ [m + k + 1 + 1]
h₁ : len [m] ≠ m + k + 1 + 1
h : Function.Surjective ↑(Hom.toOrderHom i)
h' : m + k + 1 + 1 ≤ m
⊢ False
linarith
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : [m] ⟶ [m + k + 1]
h : Function.Surjective ↑(Hom.toOrderHom i)
h' : len [m + k + 1] ≤ len [m]
⊢ False
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : [m] ⟶ [m + k + 1]
h : Function.Surjective ↑(Hom.toOrderHom i)
⊢ False
have h' := len_le_of_epi (SimplexCategory.epi_iff_surjective.2 h)
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : [m] ⟶ [m + k + 1]
h : Function.Surjective ↑(Hom.toOrderHom i)
h' : m + k + 1 ≤ m
⊢ False
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : [m] ⟶ [m + k + 1]
h : Function.Surjective ↑(Hom.toOrderHom i)
h' : len [m + k + 1] ≤ len [m]
⊢ False
dsimp at h'
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : [m] ⟶ [m + k + 1]
h : Function.Surjective ↑(Hom.toOrderHom i)
h' : m + k + 1 ≤ m
⊢ False
linarith
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ 0).op = 0
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : j₁ = 0
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0
subst hj₁
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫
      X.map (i ≫ SimplexCategory.δ (Fin.castLT 0 (_ : ↑0 < m + k + 2)) ≫ SimplexCategory.δ (Fin.succ j₂)).op =
    0
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ 0).op = 0
rw [assoc, ← SimplexCategory.δ_comp_δ'' (Fin.zero_le _)]
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ HomologicalComplex.Hom.f (P (m + k + 1 + 1)) (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ (Fin.succ j₂)).op ≫
        X.map (SimplexCategory.δ (Fin.castLT 0 (_ : ↑0 < m + k + 2))).op ≫ X.map i.op =
    0
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫
      X.map (i ≫ SimplexCategory.δ (Fin.castLT 0 (_ : ↑0 < m + k + 2)) ≫ SimplexCategory.δ (Fin.succ j₂)).op =
    0
simp only [op_comp, X.map_comp, assoc, PInfty_f]
case pos.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ m + k + 1 + 2 ≤ ↑(Fin.succ j₂) + (m + k + 1 + 1)
case pos
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ HomologicalComplex.Hom.f (P (m + k + 1 + 1)) (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ (Fin.succ j₂)).op ≫
        X.map (SimplexCategory.δ (Fin.castLT 0 (_ : ↑0 < m + k + 2))).op ≫ X.map i.op =
    0
erw [(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ j₂.succ_ne_zero, zero_comp]
case pos.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ m + k + 1 + 2 ≤ ↑j₂ + 1 + (m + k + 1 + 1)
case pos.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ m + k + 1 + 2 ≤ ↑(Fin.succ j₂) + (m + k + 1 + 1)
simp only [Nat.succ_eq_add_one, Nat.add, Fin.succ]
no goals
case pos.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
⊢ m + k + 1 + 2 ≤ ↑j₂ + 1 + (m + k + 1 + 1)
linarith
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
⊢ HomologicalComplex.Hom.f (P (m + k + 1 + 1)) (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ j₁).op ≫ X.map (SimplexCategory.δ j₂).op ≫ X.map i.op =
    0
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
⊢ HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0
simp only [op_comp, X.map_comp, assoc, PInfty_f]
case neg.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
⊢ m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
case neg
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
⊢ HomologicalComplex.Hom.f (P (m + k + 1 + 1)) (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ j₁).op ≫ X.map (SimplexCategory.δ j₂).op ≫ X.map i.op =
    0
erw [(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ hj₁, zero_comp]
case neg.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
x✝ : ¬m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
⊢ False
case neg.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
⊢ m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
by_contra
no goals
case neg.hj₂
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
x✝ : ¬m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
⊢ False
exact hj₁ (by simp only [Fin.ext_iff, Fin.val_zero] ; linarith)
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
x✝ : ¬m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
⊢ ↑j₁ = 0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
x✝ : ¬m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
⊢ j₁ = 0
simp only [Fin.ext_iff, Fin.val_zero]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
m k : ℕ
i✝ : Δ' ⟶ [m + k + 1 + 1]
hi : Mono i✝
h₁✝ : len Δ' ≠ m + k + 1 + 1
h₂ : ¬Isδ₀ i✝
h₁ : len [m] ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : [m] ⟶ [m + k]
hj₁ : ¬j₁ = 0
x✝ : ¬m + k + 1 + 2 ≤ ↑j₁ + (m + k + 1 + 1)
⊢ ↑j₁ = 0
linarith