-- Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
theorem Γ₀_obj_termwise_mapMono_comp_PInfty (X : SimplicialObject C) {Δ Δ' : SimplexCategory}
    (i : Δ ⟶ Δ') [Mono i] :
    Γ₀.Obj.Termwise.mapMono (AlternatingFaceMapComplex.obj X) i ≫ PInfty.f Δ.len =
      PInfty.f Δ'.len ≫ X.map i.op

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ PInfty.f (n + 1) ≫ ((-1) ^ ↑0 • X.δ 0) = PInfty.f (n + 1) ≫ X.map i.op

case pos.h₀
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∀ b ∈ Finset.univ, b ≠ 0 → PInfty.f (n + 1) ≫ ((-1) ^ ↑b • X.δ b) = 0

case pos.h₁
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ 0 ∉ Finset.univ → PInfty.f (n + 1) ≫ ((-1) ^ ↑0 • X.δ 0) = 0

Tactic:
rotate_left

Result:
case pos.h₀
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∀ b ∈ Finset.univ, b ≠ 0 → PInfty.f (n + 1) ≫ ((-1) ^ ↑b • X.δ b) = 0

case pos.h₁
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ 0 ∉ Finset.univ → PInfty.f (n + 1) ≫ ((-1) ^ ↑0 • X.δ 0) = 0

case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ PInfty.f (n + 1) ≫ ((-1) ^ ↑0 • X.δ 0) = PInfty.f (n + 1) ≫ X.map i.op

Proof state:
case neg
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n' ≫ X.map i.op

Tactic:
rw [Γ₀.Obj.Termwise.mapMono_eq_zero _ i _ hi, zero_comp]

Result:
case neg
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ 0 = PInfty.f n' ≫ X.map i.op

C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ⦋n'⦌ ≠ ⦋n⦌

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n⦌
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n ≫ X.map i.op

Tactic:
simp only [SimplexCategory.eq_id_of_mono i, Γ₀.Obj.Termwise.mapMono_id, op_id, X.map_id]

Result:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n⦌
inst✝ : Mono i
⊢ 𝟙 (K[X].X ⦋n⦌.len) ≫ PInfty.f n = PInfty.f n ≫ 𝟙 (X _⦋n⦌)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ⦋n'⦌ ≠ ⦋n⦌

Tactic:
by_contra h'

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
h' : ⦋n'⦌ = ⦋n⦌
⊢ False

Proof state:
case neg
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ 0 = PInfty.f n' ≫ X.map i.op

Tactic:
rw [PInfty_comp_map_mono_eq_zero]

Result:
case neg.h₁
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ⦋n⦌.len ≠ n'

case neg.h₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ¬Isδ₀ i

Proof state:
case neg.h₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
⊢ ¬Isδ₀ i

Tactic:
by_contra h'

Result:
case neg.h₂
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
h : ¬n = n'
hi : ¬Isδ₀ i
h' : Isδ₀ i
⊢ False

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ PInfty.f (n + 1) ≫ ∑ i : Fin (n + 2), (-1) ^ ↑i • X.δ i = PInfty.f (n + 1) ≫ X.map i.op

Tactic:
simp only [eq_self_iff_true, id_comp, if_true, Preadditive.comp_sum]

Result:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∑ j : Fin (n + 2), PInfty.f (n + 1) ≫ ((-1) ^ ↑j • X.δ j) = PInfty.f (n + 1) ≫ X.map i.op

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ K[X].d (n + 1) n ≫ PInfty.f n = PInfty.f (n + 1) ≫ X.map i.op

Tactic:
rw [← PInfty.comm _ n, AlternatingFaceMapComplex.obj_d_eq]

Result:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ PInfty.f (n + 1) ≫ ∑ i : Fin (n + 2), (-1) ^ ↑i • X.δ i = PInfty.f (n + 1) ≫ X.map i.op

Proof state:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∑ j : Fin (n + 2), PInfty.f (n + 1) ≫ ((-1) ^ ↑j • X.δ j) = PInfty.f (n + 1) ≫ X.map i.op

Tactic:
rw [Finset.sum_eq_single (0 : Fin (n + 2))]

Result:
case pos
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ PInfty.f (n + 1) ≫ ((-1) ^ ↑0 • X.δ 0) = PInfty.f (n + 1) ≫ X.map i.op

case pos.h₀
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ ∀ b ∈ Finset.univ, b ≠ 0 → PInfty.f (n + 1) ≫ ((-1) ^ ↑b • X.δ b) = 0

case pos.h₁
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
⊢ 0 ∉ Finset.univ → PInfty.f (n + 1) ≫ ((-1) ^ ↑0 • X.δ 0) = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ ¬b = 0

Tactic:
exact hb

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ ¬Isδ₀ (SimplexCategory.δ b)

Tactic:
rw [Isδ₀.iff]

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono i
h : ¬n = n + 1
hi : Isδ₀ i
b : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ ¬b = 0

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
Δ' : SimplexCategory
n : ℕ
i : ⦋n⦌ ⟶ Δ'
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f ⦋n⦌.len = PInfty.f Δ'.len ≫ X.map i.op

Tactic:
induction' Δ' using SimplexCategory.rec with n'

Result:
case h.h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
X : SimplicialObject C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst✝ : Mono i
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f ⦋n⦌.len = PInfty.f ⦋n'⦌.len ≫ X.map i.op