C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
θ : [n] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty n = 0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
θ : [n] ⟶ Δ'
hθ : ¬Mono θ
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty n = 0
rw [SimplexCategory.mono_iff_injective] at hθ
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty Nat.zero = 0

case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : [Nat.succ n✝] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n✝) = 0
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
Δ' : SimplexCategory
θ : [n] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty n = 0
cases n
case zero.h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ False
case zero
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty Nat.zero = 0
exfalso
case zero.h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
case zero.h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ False
apply hθ
case zero.h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
x y : Fin (SimplexCategory.len [Nat.zero] + 1)
h : ↑(SimplexCategory.Hom.toOrderHom θ) x = ↑(SimplexCategory.Hom.toOrderHom θ) y
⊢ x = y
case zero.h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
intro x y h
case zero.h.head
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
y : Fin (SimplexCategory.len [Nat.zero] + 1)
h :
  ↑(SimplexCategory.Hom.toOrderHom θ) { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } =
    ↑(SimplexCategory.Hom.toOrderHom θ) y
⊢ { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } = y
case zero.h
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
x y : Fin (SimplexCategory.len [Nat.zero] + 1)
h : ↑(SimplexCategory.Hom.toOrderHom θ) x = ↑(SimplexCategory.Hom.toOrderHom θ) y
⊢ x = y
fin_cases x
case zero.h.head.head
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
h :
  ↑(SimplexCategory.Hom.toOrderHom θ) { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } =
    ↑(SimplexCategory.Hom.toOrderHom θ) { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) }
⊢ { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } =
    { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) }
case zero.h.head
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
y : Fin (SimplexCategory.len [Nat.zero] + 1)
h :
  ↑(SimplexCategory.Hom.toOrderHom θ) { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } =
    ↑(SimplexCategory.Hom.toOrderHom θ) y
⊢ { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } = y
fin_cases y
no goals
case zero.h.head.head
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
θ : [Nat.zero] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
h :
  ↑(SimplexCategory.Hom.toOrderHom θ) { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } =
    ↑(SimplexCategory.Hom.toOrderHom θ) { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) }
⊢ { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) } =
    { val := 0, isLt := (_ : 0 < SimplexCategory.len [Nat.zero] + 1) }
rfl
case succ.intro.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : [Nat.succ n✝] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
i : Fin (n✝ + 1)
α : [n✝] ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n✝) = 0
case succ
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : [Nat.succ n✝] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n✝) = 0
obtain ⟨i, α, h⟩ := SimplexCategory.eq_σ_comp_of_not_injective θ hθ
no goals
case succ.intro.intro
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : [Nat.succ n✝] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
i : Fin (n✝ + 1)
α : [n✝] ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
⊢ X.map θ.op ≫ HomologicalComplex.Hom.f PInfty (Nat.succ n✝) = 0
rw [h, op_comp, X.map_comp, assoc, show X.map (SimplexCategory.σ i).op = X.σ i by rfl,
  σ_comp_PInfty, comp_zero]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n✝ : ℕ
θ : [Nat.succ n✝] ⟶ Δ'
hθ : ¬Function.Injective ↑(SimplexCategory.Hom.toOrderHom θ)
i : Fin (n✝ + 1)
α : [n✝] ⟶ Δ'
h : θ = SimplexCategory.σ i ≫ α
⊢ X.map (SimplexCategory.σ i).op = SimplicialObject.σ X i
rfl