-- 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 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⦌

Tactic:
swap

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
⊢ ⦋n'⦌ ≠ ⦋n⦌

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

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) ≫ X.δ 0 = PInfty.f (n + 1) ≫ X.map (SimplexCategory.δ 0).op

Tactic:
rfl

Result:
no goals

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

Tactic:
simp only [hi.eq_δ₀, Fin.val_zero, pow_zero, one_zsmul]

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) ≫ X.δ 0 = PInfty.f (n + 1) ≫ X.map (SimplexCategory.δ 0).op

Proof state:
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

Tactic:
intro b _ hb

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 : Fin (n + 2)
a✝ : b ∈ Finset.univ
hb : b ≠ 0
⊢ PInfty.f (n + 1) ≫ ((-1) ^ ↑b • X.δ b) = 0

Proof state:
case pos
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'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n' ≫ X.map i.op

Tactic:
subst h

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
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n ≫ X.map i.op

Proof state:
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 = PInfty.f n' ≫ X.map i.op

Tactic:
by_cases h : n = n'

Result:
case pos
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'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n' ≫ X.map i.op

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'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n' ≫ 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⦌
inst✝ : Mono i
⊢ 𝟙 (X _⦋n⦌) ≫ PInfty.f n = PInfty.f n ≫ 𝟙 (X _⦋n⦌)

Tactic:
simp only [id_comp, comp_id]

Result:
no goals

Proof state:
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

Tactic:
dsimp

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 = PInfty.f n' ≫ 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⦌.len ⦋n⦌.len ≫ PInfty.f n = PInfty.f (n + 1) ≫ X.map i.op

Tactic:
dsimp

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
⊢ K[X].d (n + 1) n ≫ PInfty.f n = 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'
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n' ≫ X.map i.op

Tactic:
by_cases hi : Isδ₀ i

Result:
case pos
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

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

Proof state:
case pos
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:
have h' : n' = n + 1 := hi.left

Result:
case pos
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 + 1
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f n' ≫ 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
⊢ Γ₀.Obj.Termwise.mapMono K[X] i ≫ PInfty.f n = PInfty.f (n + 1) ≫ X.map i.op

Tactic:
simp only [Γ₀.Obj.Termwise.mapMono_δ₀' _ i hi]

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
⊢ K[X].d ⦋n + 1⦌.len ⦋n⦌.len ≫ PInfty.f n = PInfty.f (n + 1) ≫ X.map i.op

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
⊢ ⦋n⦌.len ≠ n'

Tactic:
exact h

Result:
no goals

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
⊢ 𝟙 (K[X].X ⦋n⦌.len) ≫ PInfty.f n = PInfty.f n ≫ 𝟙 (X _⦋n⦌)

Tactic:
dsimp

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
⊢ 𝟙 (X _⦋n⦌) ≫ PInfty.f n = PInfty.f n ≫ 𝟙 (X _⦋n⦌)