awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m : ℕ
i : ⦋m⦌ ⟶ ⦋m + 1⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ m + 1
h₂ : ¬Isδ₀ i
mk :
  ∀ (j : Fin (m + 2)) [hi : Mono (SimplexCategory.δ j)] (h₂ : ¬Isδ₀ (SimplexCategory.δ j)),
    Eq (α := HomologicalComplex.X K[X] (m + 1) ⟶ X _⦋m⦌)
      (HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op) 0
⊢ Eq (α := HomologicalComplex.X K[X] (m + 1) ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map i.op) 0

Tactic:
obtain ⟨j, rfl⟩ := eq_δ_of_mono i

Premises used: SimplexCategory.eq_δ_of_mono, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬Isδ₀ (SimplexCategory.δ j)
⊢ ¬j = 0

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

Premises used: AlgebraicTopology.DoldKan.Isδ₀.iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
by_contra : ∀ (h : ¬1 ≤ (↑j : ℕ)), False
⊢ 1 ≤ (↑j : ℕ)

Tactic:
by_contra h
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h : ¬1 ≤ (↑j : ℕ)
⊢ j = 0

Tactic:
simpa only [Fin.ext_iff, not_le, Nat.lt_one_iff] using h

Premises used: not_le, Fin.ext_iff, Nat.lt_one_iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} 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)
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
⊢ 1 ≤ (↑j : ℕ)

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)
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h₃ : 1 ≤ (↑j : ℕ)
⊢ m + 2 ≤ (↑j : ℕ) + (m + 1)

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m : ℕ
h₁ : ⦋m⦌.len ≠ m + 1
j : Fin (m + 2)
hi : Mono (SimplexCategory.δ j)
h₂ : ¬j = 0
h₃ : 1 ≤ (↑j : ℕ)
⊢ Eq (α := HomologicalComplex.X K[X] (m + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + 1) ≫ X.map (SimplexCategory.δ j).op) 0

Tactic:
exact (HigherFacesVanish.of_P (m + 1) m).comp_δ_eq_zero j h₂ (by lia)

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
k : ℕ
hk : ⦋n⦌.len = ⦋m⦌.len + (k + 1) + 1
⊢ n = m + k + 1 + 1

Tactic:
simp only [← add_assoc] at hk

Premises used: add_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
h₁ : ⦋m⦌.len ≠ n
k : ℕ
hk : n = m + k + 1 + 1
mk :
  ∀ (i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌) (h₁ : ⦋m⦌.len ≠ m + k + 1 + 1),
    Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
      (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map i.op) 0
⊢ Eq (α := HomologicalComplex.X K[X] n ⟶ X _⦋m⦌) (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op) 0

Tactic:
subst hk
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
h :
  Function.Surjective (α := Fin (⦋m⦌.len + 1)) (β := Fin (⦋m + k + 1 + 1⦌.len + 1))
    (⇑(Hom.toOrderHom i) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m + k + 1 + 1⦌.len + 1))
⊢ Epi i

Tactic:
rw [← SimplexCategory.epi_iff_surjective] at h

Premises used: SimplexCategory.epi_iff_surjective
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
h : Epi i
⊢ False

Tactic:
grind [→ le_of_epi]

Premises used: SimplexCategory.le_of_epi
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
i : ⦋m⦌ ⟶ ⦋m + k + 1 + 1⦌
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
mk :
  ∀ (j₁ : Fin (m + k + 2 + 1)) (i : ⦋m⦌ ⟶ ⦋m + k + 1⦌),
    Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
      (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map (i ≫ SimplexCategory.δ j₁).op) 0
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map i.op) 0

Tactic:
obtain ⟨j₁ : Fin (_ + 1), i, rfl⟩ :=
      eq_comp_δ_of_not_surjective i fun h => by
        rw [← SimplexCategory.epi_iff_surjective] at h
        grind [→ le_of_epi]

Premises used: HAdd.hAdd, OfNat.ofNat, Fin, SimplexCategory.eq_comp_δ_of_not_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : ⦋m⦌ ⟶ ⦋m + k + 1⦌
h :
  Function.Surjective (α := Fin (⦋m⦌.len + 1)) (β := Fin (⦋m + k + 1⦌.len + 1))
    (⇑(Hom.toOrderHom i) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋m + k + 1⦌.len + 1))
⊢ Epi i

Tactic:
rw [← SimplexCategory.epi_iff_surjective] at h

Premises used: SimplexCategory.epi_iff_surjective
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : ⦋m⦌ ⟶ ⦋m + k + 1⦌
h : Epi i
⊢ False

Tactic:
grind [→ le_of_epi]

Premises used: SimplexCategory.le_of_epi
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₁ : Fin (m + k + 2 + 1)
i : ⦋m⦌ ⟶ ⦋m + k + 1⦌
mk :
  ∀ (j₂ : Fin (m + k + 2)) (i : ⦋m⦌ ⟶ ⦋m + k⦌),
    Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
      (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map (i ≫ SimplexCategory.δ j₁).op) 0

Tactic:
obtain ⟨j₂, i, rfl⟩ :=
      eq_comp_δ_of_not_surjective i fun h => by
        rw [← SimplexCategory.epi_iff_surjective] at h
        grind [→ le_of_epi]

Premises used: SimplexCategory.eq_comp_δ_of_not_surjective, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} 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⦌
pos :
  ∀ (hj₁ : j₁ = 0),
    Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
      (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0
neg :
  ∀ (hj₁ : ¬j₁ = 0),
    Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
      (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0

Tactic:
by_cases hj₁ : j₁ = 0
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} 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
pos :
  Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ 0).op) 0
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0

Tactic:
subst hj₁
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
pos :
  Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫
      X.map (i ≫ SimplexCategory.δ (Fin.castLT 0 ⋯) ≫ SimplexCategory.δ j₂.succ).op)
    0
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ 0).op) 0

Tactic:
rw [assoc, ← SimplexCategory.δ_comp_δ'' (Fin.zero_le _)]

Premises used: CategoryTheory.Category.assoc, SimplexCategory.δ_comp_δ'', Fin.zero_le
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
pos :
  Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f (P (m + k + 1 + 1)) (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ j₂.succ).op ≫ X.map (SimplexCategory.δ (Fin.castLT 0 ⋯)).op ≫ X.map i.op)
    0
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (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]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, AlgebraicTopology.DoldKan.PInfty_f, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
pos : m + k + 1 + 2 ≤ (↑j₂.succ : ℕ) + (m + k + 1 + 1)
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f (P (m + k + 1 + 1)) (m + k + 1 + 1) ≫
      X.map (SimplexCategory.δ j₂.succ).op ≫ X.map (SimplexCategory.δ (Fin.castLT 0 ⋯)).op ≫ X.map i.op)
    0

Tactic:
erw [(HigherFacesVanish.of_P _ _).comp_δ_eq_zero_assoc _ j₂.succ_ne_zero, zero_comp]

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero_assoc, Fin.succ_ne_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
pos : m + k + 1 + 2 ≤ (↑j₂ : ℕ) + 1 + (m + k + 1 + 1)
⊢ m + k + 1 + 2 ≤ (↑j₂.succ : ℕ) + (m + k + 1 + 1)

Tactic:
simp only [Fin.succ]

Premises used: Fin.succ
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ m + k + 1 + 2 ≤ (↑j₂ : ℕ) + 1 + (m + k + 1 + 1)

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} 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
neg :
  Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (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
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (HomologicalComplex.Hom.f PInfty (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ j₁).op) 0

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

Premises used: CategoryTheory.Category.assoc, CategoryTheory.op_comp, AlgebraicTopology.DoldKan.PInfty_f, CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} 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
neg : m + k + 1 + 2 ≤ (↑j₁ : ℕ) + (m + k + 1 + 1)
⊢ Eq (α := HomologicalComplex.X K[X] (m + k + 1 + 1) ⟶ X _⦋m⦌)
    (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

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

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_δ_eq_zero_assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} 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
neg : ∀ (this : ¬m + k + 1 + 2 ≤ (↑j₁ : ℕ) + (m + k + 1 + 1)), False
⊢ m + k + 1 + 2 ≤ (↑j₁ : ℕ) + (m + k + 1 + 1)

Tactic:
by_contra
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} 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
this : ¬m + k + 1 + 2 ≤ (↑j₁ : ℕ) + (m + k + 1 + 1)
simp : (↑j₁ : ℕ) = 0
⊢ j₁ = 0

Tactic:
simp only [Fin.ext_iff, Fin.val_zero]

Premises used: Fin.ext_iff, Fin.val_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} 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
this : ¬m + k + 1 + 2 ≤ (↑j₁ : ℕ) + (m + k + 1 + 1)
⊢ (↑j₁ : ℕ) = 0

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} 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
this : ¬m + k + 1 + 2 ≤ (↑j₁ : ℕ) + (m + k + 1 + 1)
⊢ False

Tactic:
exact hj₁ (by simp only [Fin.ext_iff, Fin.val_zero]; lia)
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst_2 : Mono i
mk :
  ∀ (n : ℕ) (i : ⦋n⦌ ⟶ Δ') [inst_3 : Mono i],
    Eq (α := HomologicalComplex.X K[X] Δ'.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
      (Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty ⦋n⦌.len)
      (HomologicalComplex.Hom.f PInfty Δ'.len ≫ X.map i.op)
⊢ Eq (α := HomologicalComplex.X K[X] Δ'.len ⟶ HomologicalComplex.X K[X] Δ.len)
    (Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty Δ.len)
    (HomologicalComplex.Hom.f PInfty Δ'.len ≫ X.map i.op)

Tactic:
induction Δ using SimplexCategory.rec with | _ n
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
Δ' : SimplexCategory
n : ℕ
i : ⦋n⦌ ⟶ Δ'
inst_2 : Mono i
mk :
  ∀ (n' : ℕ) (i : ⦋n⦌ ⟶ ⦋n'⦌) [inst_3 : Mono i],
    Eq (α := HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
      (Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty ⦋n⦌.len)
      (HomologicalComplex.Hom.f PInfty ⦋n'⦌.len ≫ X.map i.op)
⊢ Eq (α := HomologicalComplex.X K[X] Δ'.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
    (Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty ⦋n⦌.len)
    (HomologicalComplex.Hom.f PInfty Δ'.len ≫ X.map i.op)

Tactic:
induction Δ' using SimplexCategory.rec with | _ n'
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
mk :
  Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
⊢ Eq (α := HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
    (Γ₀.Obj.Termwise.mapMono K[X] i ≫ HomologicalComplex.Hom.f PInfty ⦋n⦌.len)
    (HomologicalComplex.Hom.f PInfty ⦋n'⦌.len ≫ X.map i.op)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
pos :
  ∀ (h : n = n'),
    Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
      (CategoryStruct.comp (Y := X _⦋n⦌)
          (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
          (HomologicalComplex.Hom.f PInfty n) :
        X _⦋n'⦌ ⟶ X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
neg :
  ∀ (h : ¬n = n'),
    Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
      (CategoryStruct.comp (Y := X _⦋n⦌)
          (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
          (HomologicalComplex.Hom.f PInfty n) :
        X _⦋n'⦌ ⟶ X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)

Tactic:
by_cases h : n = n'
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : n = n'
pos :
  ∀ (i : ⦋n⦌ ⟶ ⦋n⦌) [inst_3 : Mono i],
    Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
      (CategoryStruct.comp (Y := X _⦋n⦌)
          (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
          (HomologicalComplex.Hom.f PInfty n) :
        X _⦋n⦌ ⟶ X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op : X _⦋n⦌ ⟶ X _⦋n⦌)
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)

Tactic:
subst h
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n⦌
inst_2 : Mono i
pos :
  𝟙 (HomologicalComplex.X K[X] n) ≫ HomologicalComplex.Hom.f PInfty n =
    CategoryStruct.comp (Y := X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (𝟙 (X _⦋n⦌))
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n ≫ X.map i.op : X _⦋n⦌ ⟶ X _⦋n⦌)

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

Premises used: CategoryTheory.Functor.map_id, SimplexCategory.eq_id_of_mono, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id, CategoryTheory.op_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n⦌
inst_2 : Mono i
pos :
  Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n : X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (𝟙 (X _⦋n⦌)) :
      X _⦋n⦌ ⟶ X _⦋n⦌)
⊢ 𝟙 (HomologicalComplex.X K[X] n) ≫ HomologicalComplex.Hom.f PInfty n =
    CategoryStruct.comp (Y := X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (𝟙 (X _⦋n⦌))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n : ℕ
i : ⦋n⦌ ⟶ ⦋n⦌
inst_2 : Mono i
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n⦌) (𝟙 (X _⦋n⦌) ≫ HomologicalComplex.Hom.f PInfty n : X _⦋n⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (HomologicalComplex.Hom.f PInfty n : HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (𝟙 (X _⦋n⦌)) :
      X _⦋n⦌ ⟶ X _⦋n⦌)

Tactic:
simp only [id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
n n' : ℕ
i : ⦋n⦌ ⟶ ⦋n'⦌
inst_2 : Mono i
h : ¬n = n'
pos :
  ∀ (hi : Isδ₀ i),
    Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
      (CategoryStruct.comp (Y := X _⦋n⦌)
          (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
          (HomologicalComplex.Hom.f PInfty n) :
        X _⦋n'⦌ ⟶ X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
neg :
  ∀ (hi : ¬Isδ₀ i),
    Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
      (CategoryStruct.comp (Y := X _⦋n⦌)
          (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
          (HomologicalComplex.Hom.f PInfty n) :
        X _⦋n'⦌ ⟶ X _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)
⊢ Eq (α := X _⦋n'⦌ ⟶ X _⦋n⦌)
    (CategoryStruct.comp (Y := X _⦋n⦌)
        (Γ₀.Obj.Termwise.mapMono K[X] i : HomologicalComplex.X K[X] ⦋n'⦌.len ⟶ HomologicalComplex.X K[X] ⦋n⦌.len)
        (HomologicalComplex.Hom.f PInfty n) :
      X _⦋n'⦌ ⟶ X _⦋n⦌)
    (HomologicalComplex.Hom.f PInfty n' ≫ X.map i.op : X _⦋n'⦌ ⟶ X _⦋n⦌)

Tactic:
by_cases hi : Isδ₀ i

Premises used: AlgebraicTopology.DoldKan.Isδ₀