awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
hqn : q ≤ m + 1
ha : q + a = m + 1
ham : a ≤ m
ham'' : a = m
val : ℕ
isLt : val < m + 1 + 1
hj₁ : m + 1 + 1 ≤ val + (q + 1)
hj₂ : ¬a = val
haj : a < val
⊢ a + 1 = val

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
ham : a ≤ m
ham'' : a = m
⊢ m + 1 + 1 ≤ (↑j : ℕ) + q

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Faces
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
Y : C
q a m : ℕ
φ : Y ⟶ X _⦋m + 1 + 1⦌
v : HigherFacesVanish q φ
j : Fin (m + 1 + 1)
hj₁ : m + 1 + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ m + 1
ha : q + a = m + 1
hj₂ : ¬a = (↑j : ℕ)
haj : a < (↑j : ℕ)
ham : a ≤ m
ham'' : a = m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) ⟨a, ⋯⟩ ⋯)

Tactic:
simp only [← assoc, v j (by lia), zero_comp]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
j : ℕ
i : Fin (j + 2)
mp : Isδ₀ (SimplexCategory.δ i) → i = 0
mpr : i = 0 → Isδ₀ (SimplexCategory.δ i)
⊢ Isδ₀ (SimplexCategory.δ i) ↔ i = 0

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
j : ℕ
i : Fin (j + 2)
left : ⦋j + 1⦌.len = ⦋j⦌.len + 1
h₂ :
  Ne (α := Fin (⦋j + 1⦌.len + 1))
    ((Hom.toOrderHom (SimplexCategory.δ i) : (a : Fin (⦋j⦌.len + 1)) → Fin (⦋j + 1⦌.len + 1)) 0) 0
mp : ∀ (h : ¬i = 0), False
⊢ i = 0

Tactic:
by_contra h
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
j : ℕ
i : Fin (j + 2)
left : ⦋j + 1⦌.len = ⦋j⦌.len + 1
h₂ :
  Ne (α := Fin (⦋j + 1⦌.len + 1))
    ((Hom.toOrderHom (SimplexCategory.δ i) : (a : Fin (⦋j⦌.len + 1)) → Fin (⦋j + 1⦌.len + 1)) 0) 0
h : ¬i = 0
⊢ False

Tactic:
h₂ (Fin.succAbove_ne_zero_zero h)

Premises used: Fin.succAbove_ne_zero_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
j : ℕ
i : Fin (j + 2)
left : ⦋j + 1⦌.len = ⦋j⦌.len + 1
h₂ :
  Ne (α := Fin (⦋j + 1⦌.len + 1))
    ((Hom.toOrderHom (SimplexCategory.δ i) : (a : Fin (⦋j⦌.len + 1)) → Fin (⦋j + 1⦌.len + 1)) 0) 0
h : ¬i = 0
⊢ False

Tactic:
exact h₂ (Fin.succAbove_ne_zero_zero h)

Premises used: Fin.succAbove_ne_zero_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
j : ℕ
⊢ ¬Eq (α := Fin (j + 1 + 1)) ((Hom.toOrderHom (SimplexCategory.δ 0) : (a : Fin (j + 1)) → Fin (j + 1 + 1)) 0) 0

Tactic:
Fin.succ_ne_zero (0 : Fin (j + 1))

Premises used: Fin.succAbove, Fin.succ, Fin.succ_ne_zero, OfNat.ofNat, ite
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
j : ℕ
⊢ ¬Eq (α := Fin (j + 1 + 1)) ((Hom.toOrderHom (SimplexCategory.δ 0) : (a : Fin (j + 1)) → Fin (j + 1 + 1)) 0) 0

Tactic:
exact Fin.succ_ne_zero (0 : Fin (j + 1))

Premises used: Fin.succ_ne_zero, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
j : ℕ
⊢ Isδ₀ (Δ := ⦋j + 1⦌) (SimplexCategory.δ 0)

Tactic:
exact ⟨rfl, by dsimp; exact Fin.succ_ne_zero (0 : Fin (j + 1))⟩
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono i
hi : Isδ₀ i
obtain :
  ∀ (j : Fin (n + 2)) [inst : Mono (SimplexCategory.δ j)] (hi : Isδ₀ (SimplexCategory.δ j)),
    SimplexCategory.δ j = SimplexCategory.δ 0
⊢ i = SimplexCategory.δ 0

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

Premises used: SimplexCategory.eq_δ_of_mono, rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
n : ℕ
j : Fin (n + 2)
inst : Mono (SimplexCategory.δ j)
hi : Isδ₀ (SimplexCategory.δ j)
⊢ j = 0

Tactic:
rw [iff] at hi

Premises used: AlgebraicTopology.DoldKan.Isδ₀.iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
n : ℕ
j : Fin (n + 2)
inst : Mono (SimplexCategory.δ j)
hi : j = 0
rw rw₁ : Eq (α := ⦋n⦌ ⟶ ⦋n + 1⦌) (SimplexCategory.δ 0) (SimplexCategory.δ 0)
⊢ SimplexCategory.δ j = SimplexCategory.δ 0

Tactic:
rw [hi]
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ'_1 Δ'' : SimplexCategory
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst_2 : Mono i
pos : Δ = Δ' → (K.X Δ.len ⟶ K.X Δ'.len)
neg : ¬Δ = Δ' → (K.X Δ.len ⟶ K.X Δ'.len)
⊢ K.X Δ.len ⟶ K.X Δ'.len

Tactic:
by_cases Δ = Δ'
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ'_1 Δ'' : SimplexCategory
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst_2 : Mono i
h : Δ = Δ'
⊢ K.X Δ.len = K.X Δ'.len

Tactic:
congr
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ'_1 Δ'' : SimplexCategory
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst_2 : Mono i
h : Δ = Δ'
⊢ K.X Δ.len ⟶ K.X Δ'.len

Tactic:
exact eqToHom (by congr)

Premises used: CategoryTheory.eqToHom
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ'_1 Δ'' : SimplexCategory
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst_2 : Mono i
h : ¬Δ = Δ'
pos : Isδ₀ i → (K.X Δ.len ⟶ K.X Δ'.len)
neg : ¬Isδ₀ i → (K.X Δ.len ⟶ K.X Δ'.len)
⊢ K.X Δ.len ⟶ K.X Δ'.len

Tactic:
by_cases Isδ₀ i

Premises used: AlgebraicTopology.DoldKan.Isδ₀
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ'_1 Δ'' : SimplexCategory
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst_2 : Mono i
h : ¬Δ = Δ'
h_1 : Isδ₀ i
⊢ K.X Δ.len ⟶ K.X Δ'.len

Tactic:
exact K.d Δ.len Δ'.len

Premises used: SimplexCategory.len, HomologicalComplex.d
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K_1 K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K_1 ⟶ K'
Δ_1 Δ'_1 Δ'' : SimplexCategory
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ' Δ : SimplexCategory
i : Δ' ⟶ Δ
inst_2 : Mono i
h : ¬Δ = Δ'
h_1 : ¬Isδ₀ i
⊢ K.X Δ.len ⟶ K.X Δ'.len

Tactic:
exact 0
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategory
⊢ Eq.{v_1 + 1} (α := K.X Δ.len ⟶ K.X Δ.len)
    (if h : Δ = Δ then eqToHom ⋯ else if h : Isδ₀ (𝟙 Δ) then K.d Δ.len Δ.len else 0) (𝟙 (K.X Δ.len))

Tactic:
simp only [eqToHom_refl, dite_eq_ite, if_true]

Premises used: if_true, CategoryTheory.eqToHom_refl, dite_eq_ite
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst_2 : Mono i
hi : Isδ₀ i
this : Δ ≠ Δ'
⊢ Eq (α := K.X Δ.len ⟶ K.X Δ'.len) (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0)
    (K.d Δ.len Δ'.len)

Tactic:
simp only [dif_neg this, dif_pos hi]

Premises used: dif_pos, dif_neg
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst_2 : Mono i
hi : Isδ₀ i
suffices : Δ ≠ Δ'
⊢ Eq (α := K.X Δ.len ⟶ K.X Δ'.len) (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0)
    (K.d Δ.len Δ'.len)

Tactic:
suffices Δ ≠ Δ' by
    simp only [dif_neg this, dif_pos hi]
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ : SimplexCategory
i : Δ ⟶ Δ
inst_2 : Mono i
hi : Isδ₀ i
⊢ False

Tactic:
simpa only [left_eq_add, Nat.one_ne_zero] using hi.1

Premises used: left_eq_add, Nat.one_ne_zero, And.left
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
rw rw₁ : Eq (α := Fin (n + 2)) 0 0
⊢ Isδ₀ (Δ := ⦋n + 1⦌) (SimplexCategory.δ 0)

Tactic:
rw [Isδ₀.iff]

Premises used: AlgebraicTopology.DoldKan.Isδ₀.iff
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst_2 : Mono i
h₁ : Δ ≠ Δ'
h₂ : ¬Isδ₀ i
⊢ ¬Δ = Δ'

Tactic:
rw [Ne] at h₁

Premises used: Ne
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst_2 : Mono i
h₁ : Δ ≠ Δ'
h₂ : ¬Isδ₀ i
h₃ : ¬Δ = Δ'
⊢ ¬Isδ₀ i

Tactic:
rw [Ne] at h₁

Premises used: Ne
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst_2 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
split_ifs : Eq.{v_1 + 1} (α := K.X Δ.len ⟶ K.X Δ'.len) 0 0
⊢ Eq.{v_1 + 1} (α := K.X Δ.len ⟶ K.X Δ'.len)
    (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) 0

Tactic:
split_ifs
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst_2 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Isδ₀ i
⊢ Eq.{v_1 + 1} (α := K.X Δ.len ⟶ K.X Δ'.len) 0 0

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst_2 : Mono i
unfold :
  Eq (α := K.X Δ'.len ⟶ K'.X Δ.len)
    ((if h : Δ' = Δ then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ'.len Δ.len else 0) ≫ f.f Δ.len)
    (f.f Δ'.len ≫ if h : Δ' = Δ then eqToHom ⋯ else if h : Isδ₀ i then K'.d Δ'.len Δ.len else 0)
⊢ mapMono K i ≫ f.f Δ.len = f.f Δ'.len ≫ mapMono K' i

Tactic:
unfold mapMono

Premises used: AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst_2 : Mono i
pos : ∀ (h : Δ' = Δ), eqToHom ⋯ ≫ f.f Δ.len = f.f Δ'.len ≫ eqToHom ⋯
pos₁ :
  ∀ (h : ¬Δ' = Δ),
    Isδ₀ i → Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) (K.d Δ'.len Δ.len ≫ f.f Δ.len) (f.f Δ'.len ≫ K'.d Δ'.len Δ.len)
neg : ∀ (h : ¬Δ' = Δ), ¬Isδ₀ i → Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) (0 ≫ f.f Δ.len) (f.f Δ'.len ≫ 0)
⊢ Eq (α := K.X Δ'.len ⟶ K'.X Δ.len)
    ((if h : Δ' = Δ then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ'.len Δ.len else 0) ≫ f.f Δ.len)
    (f.f Δ'.len ≫ if h : Δ' = Δ then eqToHom ⋯ else if h : Isδ₀ i then K'.d Δ'.len Δ.len else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst_2 : Mono i
h : Δ' = Δ
pos : ∀ (i : Δ' ⟶ Δ') [Mono i], eqToHom ⋯ ≫ f.f Δ'.len = f.f Δ'.len ≫ eqToHom ⋯
⊢ eqToHom ⋯ ≫ f.f Δ.len = f.f Δ'.len ≫ eqToHom ⋯

Tactic:
subst h
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ' : SimplexCategory
i : Δ' ⟶ Δ'
inst_2 : Mono i
⊢ eqToHom ⋯ ≫ f.f Δ'.len = f.f Δ'.len ≫ eqToHom ⋯

Tactic:
simp only [id_comp, eqToHom_refl, comp_id]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst_2 : Mono i
h : ¬Δ' = Δ
h_1 : Isδ₀ i
pos pos₁ : Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) (K.d Δ'.len Δ.len ≫ f.f Δ.len) (K.d Δ'.len Δ.len ≫ f.f Δ.len)
⊢ Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) (K.d Δ'.len Δ.len ≫ f.f Δ.len) (f.f Δ'.len ≫ K'.d Δ'.len Δ.len)

Tactic:
rw [HomologicalComplex.Hom.comm]

Premises used: HomologicalComplex.Hom.comm
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ Δ' : SimplexCategory
i : Δ ⟶ Δ'
inst_2 : Mono i
h : ¬Δ' = Δ
h_1 : ¬Isδ₀ i
neg : Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) 0 (f.f Δ'.len ≫ 0)
neg₁ neg₂ : Eq.{v_1 + 1} (α := K.X Δ'.len ⟶ K'.X Δ.len) 0 0
⊢ Eq (α := K.X Δ'.len ⟶ K'.X Δ.len) (0 ≫ f.f Δ.len) (f.f Δ'.len ≫ 0)

Tactic:
rw [zero_comp, comp_zero]

Premises used: CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
pos : ∀ (h₁ : Δ = Δ'), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
neg : ∀ (h₁ : ¬Δ = Δ'), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
by_cases h₁ : Δ = Δ'
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : Δ = Δ'
pos : ∀ (i' : Δ'' ⟶ Δ) (i : Δ ⟶ Δ) [inst_4 : Mono i'] [inst_5 : Mono i], mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
subst h₁
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ
i : Δ ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
simp only [SimplexCategory.eq_id_of_mono i, comp_id, id_comp, mapMono_id K]

Premises used: CategoryTheory.Category.comp_id, SimplexCategory.eq_id_of_mono, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
pos : ∀ (h₂ : Δ' = Δ''), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
neg : ∀ (h₂ : ¬Δ' = Δ''), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
by_cases h₂ : Δ' = Δ''
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : Δ' = Δ''
pos : ∀ (i' : Δ' ⟶ Δ') [inst_4 : Mono i'], mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
subst h₂
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' : SimplexCategory
i : Δ' ⟶ Δ
inst_2 : Mono i
h₁ : ¬Δ = Δ'
i' : Δ' ⟶ Δ'
inst_3 : Mono i'
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
simp only [SimplexCategory.eq_id_of_mono i', comp_id, id_comp, mapMono_id K]

Premises used: CategoryTheory.Category.comp_id, SimplexCategory.eq_id_of_mono, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id, CategoryTheory.Category.id_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
neg : ∀ (k : ℕ) (hk : Δ.len = Δ'.len + k + 1), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i h₁)

Premises used: SimplexCategory.len_lt_of_mono, Nat.exists_eq_add_of_lt
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
neg : ∀ (k' : ℕ) (hk' : Δ'.len = Δ''.len + k' + 1), mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
obtain ⟨k', hk'⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i' h₂)

Premises used: SimplexCategory.len_lt_of_mono, Nat.exists_eq_add_of_lt
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
⊢ Δ.len = Δ''.len + (k + k' + 2)

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
⊢ Δ.len = Δ''.len + (k + k' + 2)

Tactic:
have eq : Δ.len = Δ''.len + (k + k' + 2) := by lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
neg : mapMono K i ≫ mapMono K i' = 0
rw : Δ ≠ Δ''
rw₁ : ¬Isδ₀ (i' ≫ i)
⊢ mapMono K i ≫ mapMono K i' = mapMono K (i' ≫ i)

Tactic:
rw [mapMono_eq_zero K (i' ≫ i) _ _]

Premises used: AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
by_contra : ∀ (h : Δ = Δ''), False
⊢ Δ ≠ Δ''

Tactic:
by_contra h
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h : Δ = Δ''
⊢ False

Tactic:
simp only [left_eq_add, h, add_eq_zero, and_false, reduceCtorEq] at eq

Premises used: reduceCtorEq, left_eq_add, and_false, add_eq_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
by_contra : ∀ (h : Isδ₀ (i' ≫ i)), False
⊢ ¬Isδ₀ (i' ≫ i)

Tactic:
by_contra h
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h : Isδ₀ (i' ≫ i)
⊢ 1 = k + k' + 2

Tactic:
simp only [h.1, add_right_inj] at eq

Premises used: And.left, add_right_inj
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
h : Isδ₀ (i' ≫ i)
eq : 1 = k + k' + 2
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
pos : ∀ (h₃ : Isδ₀ i), mapMono K i ≫ mapMono K i' = 0
neg : ∀ (h₃ : ¬Isδ₀ i), mapMono K i ≫ mapMono K i' = 0
⊢ mapMono K i ≫ mapMono K i' = 0

Tactic:
by_cases h₃ : Isδ₀ i

Premises used: AlgebraicTopology.DoldKan.Isδ₀
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
pos : ∀ (h₄ : Isδ₀ i'), mapMono K i ≫ mapMono K i' = 0
neg : ∀ (h₄ : ¬Isδ₀ i'), mapMono K i ≫ mapMono K i' = 0
⊢ mapMono K i ≫ mapMono K i' = 0

Tactic:
by_cases h₄ : Isδ₀ i'

Premises used: AlgebraicTopology.DoldKan.Isδ₀
-- Module: Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
Δ Δ' Δ'' : SimplexCategory
i' : Δ'' ⟶ Δ'
i : Δ' ⟶ Δ
inst_2 : Mono i'
inst_3 : Mono i
h₁ : ¬Δ = Δ'
h₂ : ¬Δ' = Δ''
k : ℕ
hk : Δ.len = Δ'.len + k + 1
k' : ℕ
hk' : Δ'.len = Δ''.len + k' + 1
eq : Δ.len = Δ''.len + (k + k' + 2)
h₃ : Isδ₀ i
h₄ : Isδ₀ i'
pos : Eq (α := K.X Δ.len ⟶ K.X Δ''.len) (K.d Δ.len Δ'.len ≫ mapMono K i') 0
pos₁ :
  Eq (α := K.X Δ.len ⟶ K.X Δ''.len) (CategoryStruct.comp (Y := K.X Δ'.len) (K.d Δ.len Δ'.len) (K.d Δ'.len Δ''.len)) 0
pos₂ pos₃ : Eq.{v_1 + 1} (α := K.X Δ.len ⟶ K.X Δ''.len) 0 0
⊢ mapMono K i ≫ mapMono K i' = 0

Tactic:
rw [mapMono_δ₀' K i h₃, mapMono_δ₀' K i' h₄, HomologicalComplex.d_comp_d]

Premises used: AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀', HomologicalComplex.d_comp_d