-- Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean
theorem PInfty_comp_map_mono_eq_zero (X : SimplicialObject C) {n : ℕ} {Δ' : SimplexCategory}
    (i : Δ' ⟶ ⦋n⦌) [hi : Mono i] (h₁ : Δ'.len ≠ n) (h₂ : ¬Isδ₀ i) :
    PInfty.f n ≫ X.map i.op = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h : ¬1 ≤ ↑j
⊢ False

Tactic:
exact h₂ (by simpa only [Fin.ext_iff, not_le, Nat.lt_one_iff] using h)

Result:
no goals

Proof state:
case h.intro.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
hk : n = m + 0 + 1
⊢ PInfty.f n ≫ X.map i.op = 0

Tactic:
change n = m + 1 at hk

Result:
case h.intro.zero
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
hk : n = m + 1
⊢ PInfty.f n ≫ X.map i.op = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
h : Function.Surjective ⇑(Hom.toOrderHom i)
⊢ False

Tactic:
have h' := len_le_of_epi (SimplexCategory.epi_iff_surjective.2 h)

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
h : Function.Surjective ⇑(Hom.toOrderHom i)
h' : ⦋m + k + 1 + 1⦌.len ≤ ⦋m⦌.len
⊢ False

Proof state:
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
⊢ PInfty.f (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op = 0

Tactic:
simp only [op_comp, X.map_comp, assoc, PInfty_f]

Result:
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
⊢ (P (m + k + 1 + 1)).f (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ j₁).op ≫ X.map (SimplexCategory.δ j₂).op ≫ X.map i.op =
    0

Proof state:
case h.intro.zero.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
⊢ PInfty.f (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0

Tactic:
have h₃ : 1 ≤ (j : ℕ) := by
  by_contra h
  exact h₂ (by simpa only [Fin.ext_iff, not_le, Nat.lt_one_iff] using h)

Result:
case h.intro.zero.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h₃ : 1 ≤ ↑j
⊢ PInfty.f (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0

Proof state:
case neg
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
hj₁ : ¬j₁ = 0
⊢ (P (m + k + 1 + 1)).f (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ j₁).op ≫ X.map (SimplexCategory.δ j₂).op ≫ X.map i.op =
    0

Tactic:
erw [(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ hj₁, zero_comp]

Result:
case neg.hj₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ 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)

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

Tactic:
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i fun h => by
      rw [← h] at h₁
      exact h₁ rfl)

Result:
case h.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : ⦋n⦌.len = ⦋m⦌.len + k + 1
⊢ PInfty.f n ≫ X.map i.op = 0

Proof state:
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ PInfty.f (m + k + 1 + 1) ≫ X.map (i ≫ SimplexCategory.δ (Fin.castLT 0 ⋯) ≫ SimplexCategory.δ j₂.succ).op = 0

Tactic:
simp only [op_comp, X.map_comp, assoc, PInfty_f]

Result:
case pos
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ (P (m + k + 1 + 1)).f (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ j₂.succ).op ≫ X.map (SimplexCategory.δ (Fin.castLT 0 ⋯)).op ≫ X.map i.op =
    0

Proof state:
case h.intro.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
h₁ : ⦋m⦌.len ≠ n
k : ℕ
hk : n = m + k + 1 + 1
⊢ PInfty.f n ≫ X.map i.op = 0

Tactic:
subst hk

Result:
case h.intro.succ
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
⊢ PInfty.f (m + k + 1 + 1) ≫ X.map i.op = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
h : Function.Surjective ⇑(Hom.toOrderHom i)
h' : m + k + 1 + 1 ≤ m
⊢ False

Tactic:
omega

Result:
no goals

Proof state:
case h.intro.zero.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬Isδ₀ (SimplexCategory.δ j)
⊢ PInfty.f (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0

Tactic:
rw [Isδ₀.iff] at h₂

Result:
case h.intro.zero.intro
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
⊢ PInfty.f (m + 1) ≫ X.map (SimplexCategory.δ j).op = 0