awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
⊢ Eq.{v_1 + 1} (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (Q 0) 0

Tactic:
sub_self _

Premises used: sub_self, AlgebraicTopology.DoldKan.Q
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q : ℕ
simp :
  𝟙 K[X] - HAdd.hAdd (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (P q) (P q ≫ Hσ q) =
    HSub.hSub (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) (P q) - P q ≫ Hσ q
⊢ Q (q + 1) = HSub.hSub (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (Q q) (P q ≫ Hσ q)

Tactic:
simp only [Q, P_succ, comp_add, comp_id]

Premises used: AlgebraicTopology.DoldKan.Q, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.P_succ, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q : ℕ
⊢ 𝟙 K[X] - HAdd.hAdd (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (P q) (P q ≫ Hσ q) =
    HSub.hSub (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) (P q) - P q ≫ Hσ q

Tactic:
abel
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (HomologicalComplex.Hom.f (Q q) 0) 0

Tactic:
simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, Q, P_f_0_eq, sub_self]

Premises used: AlgebraicTopology.DoldKan.P_f_0_eq, sub_self, HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, AlgebraicTopology.DoldKan.Q
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
j : Fin (n + 1)
hj₁ : n + 1 ≤ (↑j : ℕ) + 0
⊢ Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ X _⦋n⦌) (HomologicalComplex.Hom.f (P 0) (n + 1) ≫ X.δ j.succ) 0

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q n : ℕ
simp :
  HigherFacesVanish (Y := HomologicalComplex.X K[X] (n + 1)) (q + 1)
    ((P q ≫ HAdd.hAdd (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) (Hσ q)).f (n + 1))
⊢ HigherFacesVanish.{v_1, u_1} (C := C) (X := X) (Y := HomologicalComplex.X K[X] (n + 1)) (q + 1)
    (HomologicalComplex.Hom.f (P (q + 1)) (n + 1))

Tactic:
simp only [P_succ]

Premises used: AlgebraicTopology.DoldKan.P_succ
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q n : ℕ
⊢ HigherFacesVanish (Y := HomologicalComplex.X K[X] (n + 1)) (q + 1)
    ((P q ≫ HAdd.hAdd (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) (Hσ q)).f (n + 1))

Tactic:
(of_P q n).induction

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.induction
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q n : ℕ
⊢ HigherFacesVanish (Y := HomologicalComplex.X K[X] (n + 1)) (q + 1)
    ((P q ≫ HAdd.hAdd (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (𝟙 K[X]) (Hσ q)).f (n + 1))

Tactic:
exact (of_P q n).induction

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.induction
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish 0 φ
zero : φ ≫ HomologicalComplex.Hom.f (𝟙 K[X]) (n + 1) = φ
⊢ φ ≫ HomologicalComplex.Hom.f (P 0) (n + 1) = φ

Tactic:
simp only [P_zero]

Premises used: AlgebraicTopology.DoldKan.P_zero
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish 0 φ
⊢ φ ≫ HomologicalComplex.Hom.f (𝟙 K[X]) (n + 1) = φ

Tactic:
apply comp_id

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
succ : Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
⊢ φ ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) = φ

Tactic:
simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
      comp_id, ← assoc, hq v.of_succ, add_eq_left]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.add_f_apply, AlgebraicTopology.DoldKan.HigherFacesVanish.of_succ, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.P_succ, HomologicalComplex.comp_f, add_eq_left, CategoryTheory.Preadditive.comp_add
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
pos : ∀ (hqn : n < q), Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
neg : ∀ (hqn : q ≤ n), Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
⊢ Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0

Tactic:
by_cases! hqn : n < q
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : n < q
⊢ Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0

Tactic:
v.of_succ.comp_Hσ_eq_zero hqn

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, AlgebraicTopology.DoldKan.HigherFacesVanish.of_succ
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : n < q
⊢ Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0

Tactic:
exact v.of_succ.comp_Hσ_eq_zero hqn

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, AlgebraicTopology.DoldKan.HigherFacesVanish.of_succ
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
neg :
  ∀ (a : ℕ) (ha : q + a = n),
    Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
⊢ Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0

Tactic:
obtain ⟨a, ha⟩ := Nat.le.dest hqn

Premises used: Nat.le.dest
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ n = a + q

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
⊢ n = a + q

Tactic:
have hnaq : n = a + q := by lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
neg : (φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2))) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) = 0
⊢ Eq (α := Y ⟶ HomologicalComplex.X K[X] (n + 1)) (φ ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0

Tactic:
simp only [v.of_succ.comp_Hσ_eq hnaq, neg_eq_zero, ← assoc]

Premises used: CategoryTheory.Category.assoc, neg_eq_zero, AlgebraicTopology.DoldKan.HigherFacesVanish.of_succ, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ a < n + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
simp : a + (q + 1) ≤ a + (q + 1)
⊢ n + 1 ≤ (↑(⟨a, ⋯⟩ : Fin (n + 1)) : ℕ) + (q + 1)

Tactic:
simp only [hnaq, add_assoc]

Premises used: add_assoc
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ a + (q + 1) ≤ a + (q + 1)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
⊢ φ ≫ X.δ (⟨a, ⋯⟩ : Fin (n + 1)).succ = 0

Tactic:
have eq := v ⟨a, by lia⟩ (by
        simp only [hnaq, add_assoc]
        rfl)
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 : ℕ
φ : Y ⟶ X _⦋n + 1⦌
q : ℕ
hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
v : HigherFacesVanish (q + 1) φ
hqn : q ≤ n
a : ℕ
ha : q + a = n
hnaq : n = a + q
eq : φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 1 + 1)) = 0
⊢ (φ ≫ X.δ (⟨a + 1, ⋯⟩ : Fin (n + 2))) ≫ X.σ (⟨a, ⋯⟩ : Fin (n + 1)) = 0

Tactic:
simp only [eq, zero_comp]

Premises used: CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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 φ
zero : ∀ (v : HigherFacesVanish 0 φ), φ ≫ HomologicalComplex.Hom.f (P 0) (n + 1) = φ
succ :
  ∀ (q : ℕ) (hq : ∀ (v : HigherFacesVanish q φ), φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ)
    (v : HigherFacesVanish (q + 1) φ), φ ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1) = φ
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ

Tactic:
induction q with
  | zero =>
    simp only [P_zero]
    apply comp_id
  | succ q hq =>
    simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
      comp_id, ← assoc, hq v.of_succ, add_eq_left]
    by_cases! hqn : n < q
    · exact v.of_succ.comp_Hσ_eq_zero hqn
    · obtain ⟨a, ha⟩ := Nat.le.dest hqn
      have hnaq : n = a + q := by lia
      simp only [v.of_succ.comp_Hσ_eq hnaq, neg_eq_zero, ← assoc]
      have eq := v ⟨a, by lia⟩ (by
        simp only [hnaq, add_assoc]
        rfl)
      simp only [Fin.succ_mk] at eq
      simp only [eq, zero_comp]

Premises used: CategoryTheory.Category.assoc, HomologicalComplex.add_f_apply, neg_eq_zero, CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.P_succ, HomologicalComplex.comp_f, Fin.succ_mk, add_eq_left, CategoryTheory.Preadditive.comp_add, AlgebraicTopology.DoldKan.P_zero, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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⦌
mp : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ → HigherFacesVanish q φ
mpr : HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ ↔ HigherFacesVanish q φ

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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⦌
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
mp : HigherFacesVanish q (φ ≫ HomologicalComplex.Hom.f (P q) (n + 1))
⊢ HigherFacesVanish q φ

Tactic:
rw [← hφ]
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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⦌
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
mp :
  HigherFacesVanish.{v_1, u_1} (C := C) (X := X) (Y := X _⦋n + 1⦌) q
    (HomologicalComplex.Hom.f (P q) (n + 1) : HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
⊢ HigherFacesVanish q (φ ≫ HomologicalComplex.Hom.f (P q) (n + 1))

Tactic:
apply HigherFacesVanish.of_comp

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.of_comp
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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⦌
hφ : φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ
⊢ HigherFacesVanish.{v_1, u_1} (C := C) (X := X) (Y := X _⦋n + 1⦌) q
    (HomologicalComplex.Hom.f (P q) (n + 1) : HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))

Tactic:
apply HigherFacesVanish.of_P

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.of_P
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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⦌
⊢ HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ

Tactic:
HigherFacesVanish.comp_P_eq_self

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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⦌
⊢ HigherFacesVanish q φ → φ ≫ HomologicalComplex.Hom.f (P q) (n + 1) = φ

Tactic:
exact HigherFacesVanish.comp_P_eq_self

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q n : ℕ
zero :
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    (HomologicalComplex.Hom.f (P q) 0 ≫ HomologicalComplex.Hom.f (P q) 0) (HomologicalComplex.Hom.f (P q) 0)
succ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
      (HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (P q) (n + 1))
      (HomologicalComplex.Hom.f (P q) (n + 1))
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f (P q) n ≫ HomologicalComplex.Hom.f (P q) n) (HomologicalComplex.Hom.f (P q) n)

Tactic:
rcases n with (_ | n)
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q : ℕ
zero :
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    (𝟙 (HomologicalComplex.X K[X] 0) ≫ 𝟙 (HomologicalComplex.X K[X] 0)) (𝟙 (HomologicalComplex.X K[X] 0))
zero₁ zero₂ :
  Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0) (𝟙 (HomologicalComplex.X K[X] 0))
    (𝟙 (HomologicalComplex.X K[X] 0))
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] 0 ⟶ HomologicalComplex.X K[X] 0)
    (HomologicalComplex.Hom.f (P q) 0 ≫ HomologicalComplex.Hom.f (P q) 0) (HomologicalComplex.Hom.f (P q) 0)

Tactic:
rw [P_f_0_eq q, comp_id]

Premises used: AlgebraicTopology.DoldKan.P_f_0_eq, CategoryTheory.Category.comp_id
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q n : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
    (HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (P q) (n + 1))
    (HomologicalComplex.Hom.f (P q) (n + 1))

Tactic:
(HigherFacesVanish.of_P q n).comp_P_eq_self

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q n : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
    (HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (P q) (n + 1))
    (HomologicalComplex.Hom.f (P q) (n + 1))

Tactic:
exact (HigherFacesVanish.of_P q n).comp_P_eq_self

Premises used: AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q n : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
    (HomologicalComplex.Hom.f (Q q) n ≫ HomologicalComplex.Hom.f (Q q) n) (HomologicalComplex.Hom.f (Q q) n)

Tactic:
idem_of_id_sub_idem _ (P_f_idem q n)

Premises used: CategoryTheory.Idempotents.idem_of_id_sub_idem, AlgebraicTopology.DoldKan.P_f_idem
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q : ℕ
h :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
      (HomologicalComplex.Hom.f (P q ≫ P q) n) (HomologicalComplex.Hom.f (P q) n)
⊢ Eq.{v_1 + 1} (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (P q ≫ P q) (P q)

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q n : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f (P q ≫ P q) n)
    (HomologicalComplex.Hom.f (P q) n)

Tactic:
P_f_idem q n

Premises used: AlgebraicTopology.DoldKan.P_f_idem
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q n : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f (P q ≫ P q) n)
    (HomologicalComplex.Hom.f (P q) n)

Tactic:
exact P_f_idem q n

Premises used: AlgebraicTopology.DoldKan.P_f_idem
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q : ℕ
h :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n)
      (HomologicalComplex.Hom.f (Q q ≫ Q q) n) (HomologicalComplex.Hom.f (Q q) n)
⊢ Eq.{v_1 + 1} (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[X] K[X]) (Q q ≫ Q q) (Q q)

Tactic:
ext n
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q n : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f (Q q ≫ Q q) n)
    (HomologicalComplex.Hom.f (Q q) n)

Tactic:
Q_f_idem q n

Premises used: AlgebraicTopology.DoldKan.Q_f_idem
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
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
q n : ℕ
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] n ⟶ HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f (Q q ≫ Q q) n)
    (HomologicalComplex.Hom.f (Q q) n)

Tactic:
exact Q_f_idem q n

Premises used: AlgebraicTopology.DoldKan.Q_f_idem
-- Module: Mathlib.AlgebraicTopology.DoldKan.Projections
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X x x_1 : SimplicialObject.{v_1, u_1} C
f : x ⟶ x_1
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) K[x] K[x_1]) (AlternatingFaceMapComplex.map f ≫ P 0)
    (P 0 ≫ AlternatingFaceMapComplex.map f)

Tactic:
simp only [P_zero, id_comp, comp_id]

Premises used: CategoryTheory.Category.comp_id, AlgebraicTopology.DoldKan.P_zero, CategoryTheory.Category.id_comp