awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ LE.le (α := Fin 2) 0 (Fin.castSucc 0)
have rw : LE.le (α := Fin 2) 0 0
Tactic: rw [Fin.castSucc_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q : ℕ
hq :
  ∀ (i : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi : HAdd.hAdd (α := ℕ) 0 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (HAdd.hAdd (α := ℕ) 0 1) : X _⦋0⦌ ⟶ X _⦋HAdd.hAdd (α := ℕ) 0 1⦌)
      (0 : X _⦋0⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (HAdd.hAdd (α := ℕ) 0 1))
h : ¬1 ≤ 0 + q
hi : 0 = 0 + q
⊢ X.σ 0 +
      (HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋1⦌) (X.σ 0 ≫ X.δ 0 ≫ X.σ 0) (-X.σ 0 ≫ X.δ 1 ≫ X.σ 0) +
        (-X.σ 0 ≫ X.σ 1 ≫ X.δ 0 +
          HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋1⦌) (X.σ 0 ≫ X.σ 1 ≫ X.δ 1) (-X.σ 0 ≫ X.σ 1 ≫ X.δ (Fin.succ 1)))) =
    0
have neg : X.σ 0 +
    (HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋1⦌) (X.σ 0) (-X.σ 0) + (-X.σ 0 + HAdd.hAdd (α := X _⦋0⦌ ⟶ X _⦋1⦌) (X.σ 0) (-X.σ 0))) =
  0
Tactic: rw [← Fin.castSucc_one, SimplicialObject.δ_comp_σ_self, ← Fin.castSucc_zero (n := 1),
          SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ, comp_id, ← Fin.castSucc_zero (n := 2),
          ← Fin.succ_zero_eq_one,
          SimplicialObject.δ_comp_σ_of_le X
            (show (0 : Fin 2) ≤ Fin.castSucc 0 by rw [Fin.castSucc_zero]),
          ← Fin.castSucc_zero (n := 1), SimplicialObject.δ_comp_σ_self_assoc,
          SimplicialObject.δ_comp_σ_succ_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
⊢ Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (X.σ i ≫ HomologicalComplex.Hom.f (P (q + 1)) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
have neg : HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    ((HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i) ≫
        (P q ≫
              HAdd.hAdd (α :=
                Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (AlternatingFaceMapComplex.obj X)
                  (AlternatingFaceMapComplex.obj X))
                (𝟙 (AlternatingFaceMapComplex.obj X)) (Hσ q)).f
          (n + 1 + 1) :
      X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    ((HomologicalComplex.Hom.f (Q q) n.succ ≫ X.σ i) ≫
        (P q ≫
              HAdd.hAdd (α :=
                Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (AlternatingFaceMapComplex.obj X)
                  (AlternatingFaceMapComplex.obj X))
                (𝟙 (AlternatingFaceMapComplex.obj X)) (Hσ q)).f
          (n + 1 + 1) :
      X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) =
  0
Tactic: rw [← id_comp (X.σ i), ← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)), add_comp, add_comp,
          P_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
⊢ HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i) ≫
          (P q ≫
                HAdd.hAdd (α :=
                  Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (AlternatingFaceMapComplex.obj X)
                    (AlternatingFaceMapComplex.obj X))
                  (𝟙 (AlternatingFaceMapComplex.obj X)) (Hσ q)).f
            (n + 1 + 1) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (Q q) n.succ ≫ X.σ i) ≫
          (P q ≫
                HAdd.hAdd (α :=
                  Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (AlternatingFaceMapComplex.obj X)
                    (AlternatingFaceMapComplex.obj X))
                  (𝟙 (AlternatingFaceMapComplex.obj X)) (Hσ q)).f
            (n + 1 + 1) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) =
    0
have v : HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
  (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
Tactic: have v : HigherFacesVanish q ((P q).f n.succ ≫ X.σ i) :=
          (HigherFacesVanish.of_P q n).comp_σ hi
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
⊢ HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i) ≫
          (P q ≫
                HAdd.hAdd (α :=
                  Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (AlternatingFaceMapComplex.obj X)
                    (AlternatingFaceMapComplex.obj X))
                  (𝟙 (AlternatingFaceMapComplex.obj X)) (Hσ q)).f
            (n + 1 + 1) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (Q q) n.succ ≫ X.σ i) ≫
          (P q ≫
                HAdd.hAdd (α :=
                  Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (AlternatingFaceMapComplex.obj X)
                    (AlternatingFaceMapComplex.obj X))
                  (𝟙 (AlternatingFaceMapComplex.obj X)) (Hσ q)).f
            (n + 1 + 1) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) =
    0
have neg : HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    ((HomologicalComplex.Hom.f (P q) (n + 1) ≫ X.σ i) ≫
        HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
          HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
            (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) :
      X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    ((HomologicalComplex.Hom.f (Q q) (n + 1) ≫ X.σ i) ≫
        HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
          HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
            (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) :
      X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) =
  0
Tactic: dsimp only [AlternatingFaceMapComplex.obj_X, Nat.succ_eq_add_one, HomologicalComplex.comp_f,
          HomologicalComplex.add_f_apply, HomologicalComplex.id_f]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
⊢ HAdd.hAdd (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (β := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (P q) (n + 1) ≫ X.σ i) ≫
          HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
            HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
              (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      ((HomologicalComplex.Hom.f (Q q) (n + 1) ≫ X.σ i) ≫
          HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
            HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
              (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) :
        X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌) =
    0
have neg : ∀ (x : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q} x →
    ((HomologicalComplex.Hom.f (P (↑x : ℕ)) (n + 1) ≫ X.δ x.rev.succ ≫ X.σ x.rev) ≫ X.σ i) ≫
        HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
          HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
            (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) =
      0
Tactic: rw [← assoc, v.comp_P_eq_self, Preadditive.comp_add,
          comp_id, v.comp_Hσ_eq hi, assoc, ← Fin.succ_mk _ _ i.2,
          SimplicialObject.δ_comp_σ_succ_assoc,
          Fin.eta, decomposition_Q n q, sum_comp, sum_comp, Finset.sum_eq_zero, add_zero,
          add_neg_eq_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : Membership.mem (γ := Finset (Fin (n + 1))) {i : Fin (n + 1) | (↑i : ℕ) < q} j
⊢ ((HomologicalComplex.Hom.f (P (↑j : ℕ)) (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
      HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
        HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
          (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) =
    0
have hj₁ : True ∧ (↑j : ℕ) < q
Tactic: simp only [Finset.mem_univ, Finset.mem_filter] at hj
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
⊢ ((HomologicalComplex.Hom.f (P (↑j : ℕ)) (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
      HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
        HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
          (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) =
    0
have neg : ∀ (k : ℕ) (hk : (↑j : ℕ) + k = n),
  ((HomologicalComplex.Hom.f (P (↑j : ℕ)) (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
      HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
        HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
          (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) =
    0
Tactic: obtain ⟨k, hk⟩ := Nat.le.dest (Nat.lt_succ_iff.mp (Fin.is_lt j))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : (↑j : ℕ) + k = n
⊢ ((HomologicalComplex.Hom.f (P (↑j : ℕ)) (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
      HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
        HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
          (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) =
    0
have hk₁ : k + (↑j : ℕ) = n
Tactic: rw [add_comm] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
⊢ i = ⟨(↑i : ℕ), ⋯⟩.castSucc
have h₁ : (↑i : ℕ) = (↑(⟨(↑i : ℕ), sorry⟩ : Fin (n + 1)).castSucc : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
⊢ ((HomologicalComplex.Hom.f (P (↑j : ℕ)) (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
      HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
        HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
          (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) =
    0
have hi' : i = ⟨(↑i : ℕ), sorry⟩.castSucc
Tactic: have hi' : i = Fin.castSucc ⟨i, by lia⟩ := by
          ext
          simp only [Fin.castSucc_mk, Fin.eta]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
hi' : i = ⟨(↑i : ℕ), ⋯⟩.castSucc
⊢ n + 1 + 1 ≤ (↑j.rev.succ : ℕ) + q
have simp : k + (↑j : ℕ) + 1 + 1 ≤ k + 1 + q
Tactic: simp only [← hk, Fin.rev_eq j hk.symm, Fin.succ_mk, Fin.val_mk]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
hi' : i = ⟨(↑i : ℕ), ⋯⟩.castSucc
⊢ ((HomologicalComplex.Hom.f (P (↑j : ℕ)) (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
      HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
        HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
          (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) =
    0
have eq : Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
  (X.σ j.rev.succ ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
  (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
Tactic: have eq := hq j.rev.succ (by
          simp only [← hk, Fin.rev_eq j hk.symm, Fin.succ_mk, Fin.val_mk]
          lia)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
hi' : i = ⟨(↑i : ℕ), ⋯⟩.castSucc
eq :
  Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (X.σ j.rev.succ ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
⊢ ((HomologicalComplex.Hom.f (P (↑j : ℕ)) (n + 1) ≫ X.δ j.rev.succ ≫ X.σ j.rev) ≫ X.σ i) ≫
      HomologicalComplex.Hom.f (P q) (n + 1 + 1) ≫
        HAdd.hAdd (β := X _⦋n + 1 + 1⦌ ⟶ X _⦋n + 1 + 1⦌) (𝟙 (X _⦋n + 1 + 1⦌))
          (HomologicalComplex.Hom.f (Hσ q) (n + 1 + 1)) =
    0
have neg : (⟨(↑i : ℕ), sorry⟩ : Fin (n + 1)) ≤ j.rev
Tactic: rw [assoc, assoc, assoc, hi',
          SimplicialObject.σ_comp_σ_assoc, reassoc_of% eq, zero_comp, comp_zero, comp_zero,
          comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
q n : ℕ
hq :
  ∀ (i : Fin (n + 1 + 1)) (hi : n + 1 + 1 ≤ (↑i : ℕ) + q),
    Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (X.σ i ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
      (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
i : Fin (n + 1 + 1)
h : ¬n + 1 + 1 ≤ (↑i : ℕ) + q
hi : n + 1 = (↑i : ℕ) + q
v :
  HigherFacesVanish (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n.succ) q
    (HomologicalComplex.Hom.f (P q) n.succ ≫ X.σ i)
j : Fin (n + 1)
hj : True ∧ (↑j : ℕ) < q
k : ℕ
hk : k + (↑j : ℕ) = n
hi' : i = ⟨(↑i : ℕ), ⋯⟩.castSucc
eq :
  Eq (α := X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (X.σ j.rev.succ ≫ HomologicalComplex.Hom.f (P q) (n + 1 + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1 + 1⦌)
    (0 : X _⦋n + 1⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1 + 1))
⊢ (⟨(↑i : ℕ), ⋯⟩ : Fin (n + 1)) ≤ j.rev
have neg : (↑i : ℕ) ≤ k
Tactic: simp only [Fin.rev_eq j hk.symm, Fin.le_iff_val_le_val]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
n : ℕ
i : Fin (n + 1)
⊢ Eq (α := X _⦋n⦌ ⟶ X _⦋n + 1⦌) (X.σ i ≫ HomologicalComplex.Hom.f PInfty (n + 1) : X _⦋n⦌ ⟶ X _⦋n + 1⦌)
    (0 : X _⦋n⦌ ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
have rw : n + 1 ≤ (↑i : ℕ) + (n + 1)
Tactic: rw [PInfty_f, σ_comp_P_eq_zero X i]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
n : ℕ
Δ' : SimplexCategory
θ : ⦋n⦌ ⟶ Δ'
hθ : ¬Mono θ
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty n : X.obj (Opposite.op Δ') ⟶ X _⦋n⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n)
have hθ₁ : ¬Function.Injective (α := Fin (⦋n⦌.len + 1)) (β := Fin (Δ'.len + 1))
    (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ'.len + 1))
Tactic: rw [SimplexCategory.mono_iff_injective] at hθ
Cleared hypotheses: hθ
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
n : ℕ
Δ' : SimplexCategory
θ : ⦋n⦌ ⟶ Δ'
hθ :
  ¬Function.Injective (α := Fin (⦋n⦌.len + 1)) (β := Fin (Δ'.len + 1))
      (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ'.len + 1))
⊢ Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋n⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty n : X.obj (Opposite.op Δ') ⟶ X _⦋n⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) n)
have zero : ∀ (θ : ⦋0⦌ ⟶ Δ')
  (hθ :
    ¬Function.Injective (α := Fin (⦋0⦌.len + 1)) (β := Fin (Δ'.len + 1))
        (⇑(SimplexCategory.Hom.toOrderHom θ) : (a : Fin (⦋0⦌.len + 1)) → Fin (Δ'.len + 1))),
  Eq (α := X.obj (Opposite.op Δ') ⟶ X _⦋0⦌)
    (X.map θ.op ≫ HomologicalComplex.Hom.f PInfty 0 : X.obj (Opposite.op Δ') ⟶ X _⦋0⦌)
    (0 : X.obj (Opposite.op Δ') ⟶ HomologicalComplex.X (AlternatingFaceMapComplex.obj X) 0)
Tactic: cases n
Cleared hypotheses: n, θ, hθ