awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : n < q
⊢ φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
have pos : φ ≫ X.δ j.succ + 0 ≫ X.δ j.succ = 0
Tactic: rw [v.comp_Hσ_eq_zero hqn, zero_comp, add_zero, v j (by lia)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : n < q
pos : φ ≫ X.δ j.succ + 0 ≫ X.δ j.succ = 0
⊢ φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
have pos₁ : φ ≫ X.δ j.succ + 0 = 0
Tactic: rw [v.comp_Hσ_eq_zero hqn, zero_comp, add_zero, v j (by lia)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : n < q
pos : φ ≫ X.δ j.succ + 0 ≫ X.δ j.succ = 0
pos₁ : φ ≫ X.δ j.succ + 0 = 0
⊢ φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
have pos₂ : φ ≫ X.δ j.succ = 0
Tactic: rw [v.comp_Hσ_eq_zero hqn, zero_comp, add_zero, v j (by lia)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : n < q
pos : φ ≫ X.δ j.succ + 0 ≫ X.δ j.succ = 0
pos₁ : φ ≫ X.δ j.succ + 0 = 0
pos₂ : φ ≫ X.δ j.succ = 0
⊢ φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
have pos₃ : Eq.{v_1 + 1} (α := Y ⟶ X _⦋n⦌) 0 0
Tactic: rw [v.comp_Hσ_eq_zero hqn, zero_comp, add_zero, v j (by lia)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ n
⊢ φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
have neg : ∀ (a : ℕ) (ha : q + a = n), φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
Tactic: obtain ⟨a, ha⟩ := Nat.le.dest hqn
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ φ ≫ X.δ j.succ + (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) ≫ X.δ j.succ = 0
have neg : φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, sorry⟩ ≫ X.σ (⟨a, sorry⟩ : Fin (n + 1)) ≫ X.δ j.succ
Tactic: rw [v.comp_Hσ_eq (show n = a + q by lia), neg_comp, add_neg_eq_zero, assoc, assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) ≫ X.δ j.succ
have neg : ∀ {φ : Y ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌} (v : HigherFacesVanish q φ) (j : Fin (HAdd.hAdd (α := ℕ) 0 1))
  (hj₁ : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑j : ℕ) + (q + 1)) (hqn : q ≤ 0) (ha : q + a = 0),
  φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, sorry⟩ ≫ X.σ (⟨a, sorry⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) ≫ X.δ j.succ
Tactic: rcases n with - | m
Cleared hypotheses: n, φ, v, j, hj₁, hqn, ha
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ n
a : ℕ
ha : q + a = n
neg :
  ∀ {φ : Y ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌} (v : HigherFacesVanish q φ) (j : Fin (HAdd.hAdd (α := ℕ) 0 1))
    (hj₁ : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑j : ℕ) + (q + 1)) (hqn : q ≤ 0) (ha : q + a = 0),
    φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) ≫ X.δ j.succ
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) ≫ X.δ j.succ
have neg₁ : ∀ (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),
  φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, sorry⟩ ≫ X.σ (⟨a, sorry⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
Tactic: rcases n with - | m
Cleared hypotheses: n, φ, v, j, hj₁, hqn, ha
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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 : ℕ
φ : Y ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌
v : HigherFacesVanish q φ
j : Fin (HAdd.hAdd (α := ℕ) 0 1)
hj₁ : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑j : ℕ) + (q + 1)
hqn : q ≤ 0
ha : q + a = 0
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (HAdd.hAdd (α := ℕ) 0 1)) ≫ X.δ j.succ
have neg : φ ≫ X.δ (Fin.succ 0) = φ ≫ X.δ ⟨HAdd.hAdd (α := ℕ) 0 1, sorry⟩
Tactic: simp only [Nat.eq_zero_of_add_eq_zero_left ha, Fin.eq_zero j, Fin.mk_zero,
      δ_comp_σ_succ, comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
have pos : ∀ (hj₂ : a = (↑j : ℕ)), φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, sorry⟩ ≫ X.σ (⟨a, sorry⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
Tactic: by_cases hj₂ : a = (j : ℕ)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
pos : ∀ (hj₂ : a = (↑j : ℕ)), φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
have neg : ∀ (hj₂ : ¬a = (↑j : ℕ)), φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, sorry⟩ ≫ X.σ (⟨a, sorry⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
Tactic: by_cases hj₂ : a = (j : ℕ)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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 : ℕ)
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
have pos : φ ≫ X.δ j.succ = φ ≫ X.δ ⟨(↑j : ℕ) + 1, sorry⟩
Tactic: simp only [hj₂, Fin.eta, δ_comp_σ_succ, comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (hypothesis)
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 : ℕ)
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
have haj : a < (↑j : ℕ)
Tactic: have haj : a < j := (Ne.le_iff_lt hj₂).mp (by lia)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (hypothesis)
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 : ℕ)
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
have ham : a ≤ m
Tactic: have ham : a ≤ m := by grind
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
have neg : φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, sorry⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, sorry⟩ : Fin (m + 1 + 1)) sorry)
Tactic: rw [X.δ_comp_σ_of_gt', j.pred_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
neg : φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.σ (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ≫ X.δ j.succ
have neg₁ : Fin.succ ⟨a, sorry⟩ < j.succ
Tactic: rw [X.δ_comp_σ_of_gt', j.pred_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)
have neg : a < m → φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, sorry⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, sorry⟩ : Fin (m + 1 + 1)) sorry)
Tactic: obtain _ | ham'' := ham.lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
neg : a < m → φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)
have neg₁ : ∀ (ham'' : a = m),
  φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, sorry⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, sorry⟩ : Fin (m + 1 + 1)) sorry)
Tactic: obtain _ | ham'' := ham.lt_or_eq
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
h : a < m
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)
have neg : φ ≫ X.δ j.succ =
  φ ≫ X.δ j.succ ≫ X.δ (Fin.castLT (⟨a + 1, sorry⟩ : Fin (m + 1 + 2)) sorry) ≫ X.σ (Fin.castLT (m := m + 2) ⟨a, sorry⟩ sorry)
Tactic: rw [← X.δ_comp_δ''_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
h : a < m
neg :
  φ ≫ X.δ j.succ =
    φ ≫ X.δ j.succ ≫ X.δ (Fin.castLT (⟨a + 1, ⋯⟩ : Fin (m + 1 + 2)) ⋯) ≫ X.σ (Fin.castLT (m := m + 2) ⟨a, ⋯⟩ ⋯)
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)
have neg₁ : ⟨a + 1, sorry⟩ ≤ j.castSucc
Tactic: rw [← X.δ_comp_δ''_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
h : a < m
⊢ (↑(⟨a + 1, ⋯⟩ : Fin (m + 1 + 2)) : ℕ) ≤ (↑j.castSucc : ℕ)
have neg : a + 1 ≤ (↑j : ℕ)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)
have neg : φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) ⟨a, sorry⟩ sorry)
Tactic: rw [X.δ_comp_δ_self'_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
neg : φ ≫ X.δ j.succ = φ ≫ X.δ j.succ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) ⟨a, ⋯⟩ ⋯)
⊢ φ ≫ X.δ j.succ = φ ≫ X.δ ⟨a + 1, ⋯⟩ ≫ X.δ j ≫ X.σ (Fin.castLT (m := m + 2) (⟨a, ⋯⟩ : Fin (m + 1 + 1)) ⋯)
have neg₁ : ⟨a + 1, sorry⟩ = j.castSucc
Tactic: rw [X.δ_comp_δ_self'_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ ⟨a + 1, ⋯⟩ = j.castSucc
have neg : (↑(⟨a + 1, sorry⟩ : Fin (m + 1 + 2)) : ℕ) = (↑j.castSucc : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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
⊢ (↑(⟨a + 1, ⋯⟩ : Fin (m + 1 + 2)) : ℕ) = (↑j.castSucc : ℕ)
have neg : ∀ (val : ℕ) (isLt : val < m + 1 + 1) (hj₁ : m + 1 + 1 ≤ (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)) : ℕ) + (q + 1))
  (hj₂ : ¬a = (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)) : ℕ)) (haj : a < (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)) : ℕ)),
  (↑(⟨a + 1, sorry⟩ : Fin (m + 1 + 2)) : ℕ) = (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)).castSucc : ℕ)
Tactic: cases j
Cleared hypotheses: j, hj₁, hj₂, haj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (goal)
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, isLt⟩ : Fin (m + 1 + 1)) : ℕ) + (q + 1)
hj₂ : ¬a = (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)) : ℕ)
haj : a < (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)) : ℕ)
⊢ (↑(⟨a + 1, ⋯⟩ : Fin (m + 1 + 2)) : ℕ) = (↑(⟨val, isLt⟩ : Fin (m + 1 + 1)).castSucc : ℕ)
have neg : a + 1 = val
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
j : ℕ
i : Fin (j + 2)
⊢ Isδ₀ (SimplexCategory.δ i) ↔ i = 0
have mp : Isδ₀ (SimplexCategory.δ i) → i = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
j : ℕ
i : Fin (j + 2)
mp : Isδ₀ (SimplexCategory.δ i) → i = 0
⊢ Isδ₀ (SimplexCategory.δ i) ↔ i = 0
have mpr : i = 0 → Isδ₀ (SimplexCategory.δ i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
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
⊢ i = 0
have mp : ∀ (h : ¬i = 0), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
n : ℕ
i : ⦋n⦌ ⟶ ⦋n + 1⦌
inst : Mono i
hi : Isδ₀ i
⊢ i = SimplexCategory.δ 0
have obtain : ∀ (j : Fin (n + 2)) [inst : Mono (SimplexCategory.δ j)] (hi : Isδ₀ (SimplexCategory.δ j)),
  SimplexCategory.δ j = SimplexCategory.δ 0
Tactic: obtain ⟨j, rfl⟩ := SimplexCategory.eq_δ_of_mono i
Cleared hypotheses: i, inst, hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (hypothesis)
Goal:
n : ℕ
j : Fin (n + 2)
inst : Mono (SimplexCategory.δ j)
hi : Isδ₀ (SimplexCategory.δ j)
⊢ SimplexCategory.δ j = SimplexCategory.δ 0
have hi₁ : j = 0
Tactic: rw [iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
Goal:
n : ℕ
j : Fin (n + 2)
inst : Mono (SimplexCategory.δ j)
hi : j = 0
⊢ SimplexCategory.δ j = SimplexCategory.δ 0
have rw : Eq (α := ⦋n⦌ ⟶ ⦋n + 1⦌) (SimplexCategory.δ 0) (SimplexCategory.δ 0)
Tactic: rw [hi]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
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
⊢ K.X Δ.len ⟶ K.X Δ'.len
have pos : Δ = Δ' → (K.X Δ.len ⟶ K.X Δ'.len)
Tactic: by_cases Δ = Δ'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
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)
⊢ K.X Δ.len ⟶ K.X Δ'.len
have neg : ¬Δ = Δ' → (K.X Δ.len ⟶ K.X Δ'.len)
Tactic: by_cases Δ = Δ'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
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
have pos : Isδ₀ i → (K.X Δ.len ⟶ K.X Δ'.len)
Tactic: by_cases Isδ₀ i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
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)
⊢ K.X Δ.len ⟶ K.X Δ'.len
have neg : ¬Isδ₀ i → (K.X Δ.len ⟶ K.X Δ'.len)
Tactic: by_cases Isδ₀ i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
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
⊢ 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)
have suffices : Δ ≠ Δ'
Tactic: suffices Δ ≠ Δ' by
    simp only [dif_neg this, dif_pos hi]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
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 : ℕ
⊢ Isδ₀ (Δ := ⦋n + 1⦌) (SimplexCategory.δ 0)
have rw : Eq (α := Fin (n + 2)) 0 0
Tactic: rw [Isδ₀.iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (hypothesis)
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)
    (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) 0
have h₃ : ¬Δ = Δ'
Tactic: rw [Ne] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
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)
    (if h : Δ = Δ' then eqToHom ⋯ else if h : Isδ₀ i then K.d Δ.len Δ'.len else 0) 0
have split_ifs : Eq.{v_1 + 1} (α := K.X Δ.len ⟶ K.X Δ'.len) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
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
⊢ mapMono K i ≫ f.f Δ.len = f.f Δ'.len ≫ mapMono K' i
have unfold : Eq (α := K.X Δ'.len ⟶ K'.X Δ.len)
  ((if h : Δ' = Δ then eqToHom sorry else if h : Isδ₀ i then K.d Δ'.len Δ.len else 0) ≫ f.f Δ.len)
  (f.f Δ'.len ≫ if h : Δ' = Δ then eqToHom sorry else if h : Isδ₀ i then K'.d Δ'.len Δ.len else 0)
Tactic: unfold mapMono
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
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
⊢ 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)
have pos : ∀ (h : Δ' = Δ), eqToHom sorry ≫ f.f Δ.len = f.f Δ'.len ≫ eqToHom sorry
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.FunctorGamma (goal)
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 ⋯
⊢ 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)
have 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)
Tactic: split_ifs with h