awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ 𝟙 (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1)) ≫ K.d (n + 1) n =
    CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
          Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
          (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
        (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) :
          Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)
              (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
              Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
              (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
        (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ K (op ⦋n⦌))
            (HomologicalComplex.d (AlternatingFaceMapComplex.obj (Γ₀.obj K)) (n + 1) n)
            (Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
              Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
              (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) ⟶
            Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n) ≫
      𝟙 (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
have simp : Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
  (∑ j : Fin (n + 2),
    CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
        (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
      ((HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • (Γ₀.obj K).δ j) ≫
        Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))
Tactic: simp only [id_comp, comp_id, AlternatingFaceMapComplex.obj_d_eq, Preadditive.sum_comp,
        Preadditive.comp_sum]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (∑ j : Fin (n + 2),
      CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
          Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
          (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
        (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
        ((HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • (Γ₀.obj K).δ j) ≫
          Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))
have rw : Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
  (CategoryStruct.comp (Y :=
    Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
      Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
      (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
    (HSMul.hSMul (β := Γ₀.obj K _⦋n + 1⦌ ⟶ Γ₀.obj K _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) ((Γ₀.obj K).δ 0) ≫
      Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))
Tactic: rw [Fintype.sum_eq_single (0 : Fin (n + 2))]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
rw :
  Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
        (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
      (HSMul.hSMul (β := Γ₀.obj K _⦋n + 1⦌ ⟶ Γ₀.obj K _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) ((Γ₀.obj K).δ 0) ≫
        Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (∑ j : Fin (n + 2),
      CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
          Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
          (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
        (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
        ((HPow.hPow (α := ℤ) (-1) (↑j : ℕ) • (Γ₀.obj K).δ j) ≫
          Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))
have rw₁ : ∀ (x : Fin (n + 2)),
  x ≠ 0 →
    Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
      (CategoryStruct.comp (Y :=
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
            Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
            (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
          (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
          ((HPow.hPow (α := ℤ) (-1) (↑x : ℕ) • (Γ₀.obj K).δ x) ≫
            Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
        Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
      (0 : Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
Tactic: rw [Fintype.sum_eq_single (0 : Fin (n + 2))]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
        (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
      (HSMul.hSMul (β := Γ₀.obj K _⦋n + 1⦌ ⟶ Γ₀.obj K _⦋n⦌) (HPow.hPow (α := ℤ) (-1) (↑0 : ℕ)) ((Γ₀.obj K).δ 0) ≫
        Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))
have simp : Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
  (CategoryStruct.comp (Y :=
    Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
      Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
      (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
    ((Γ₀.obj K).δ 0 ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))
Tactic: simp only [Fin.val_zero, pow_zero, one_zsmul]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
        (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
      ((Γ₀.obj K).δ 0 ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))))
have rw : Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
  (K.d (n + 1) n ≫
    𝟙 (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌))))
Tactic: rw [δ, Γ₀.Obj.mapMono_on_summand_id_assoc, Γ₀.Obj.Termwise.mapMono_δ₀,
          Splitting.cofan_inj_πSummand_eq_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ K.X n) (K.d (n + 1) n)
    (K.d (n + 1) n ≫
      𝟙 (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌))))
have dsimp : Eq (α := K.X (n + 1) ⟶ K.X n) (K.d (n + 1) n) (K.d (n + 1) n ≫ 𝟙 (K.X n))
Tactic: dsimp only [Γ₀.splitting, Splitting.summand.eq_1, Splitting.IndexSet.id_fst]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α := K.X (n + 1) ⟶ K.X n) (K.d (n + 1) n) (K.d (n + 1) n ≫ 𝟙 (K.X n))
have rw : Eq (α := K.X (n + 1) ⟶ K.X n) (K.d (n + 1) n) (K.d (n + 1) n)
Tactic: rw [comp_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
    (CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
          Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
          (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
        (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
        ((HPow.hPow (α := ℤ) (-1) (↑i : ℕ) • (Γ₀.obj K).δ i) ≫
          Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
      Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
    (0 : Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
have simp : HSMul.hSMul (β := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
    (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
    (CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
          Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
          (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
        (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
        ((Γ₀.obj K).δ i ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
      Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n) =
  0
Tactic: simp only [Preadditive.zsmul_comp, Preadditive.comp_zsmul]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
⊢ HSMul.hSMul (β :=
      Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
      (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
      (CategoryStruct.comp (Y :=
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
            Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
            (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
          (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
          ((Γ₀.obj K).δ i ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
        Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n) =
    0
have h₁ : ⦋n + 1⦌ ≠ ⦋n⦌
Tactic: rw [δ, Γ₀.Obj.mapMono_on_summand_id_assoc, Γ₀.Obj.Termwise.mapMono_eq_zero, zero_comp,
          zsmul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h₁ : ⦋n + 1⦌ ≠ ⦋n⦌
⊢ HSMul.hSMul (β :=
      Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n)
      (HPow.hPow (α := ℤ) (-1) (↑i : ℕ))
      (CategoryStruct.comp (Y :=
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n + 1⦌))) (F :=
            Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)))
            (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)))
          (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
          ((Γ₀.obj K).δ i ≫ Splitting.πSummand (Γ₀.splitting K) (Splitting.IndexSet.id (op ⦋n⦌))) :
        Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) (n + 1) ⟶ Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n) =
    0
have h₂ : ¬Isδ₀ (SimplexCategory.δ i)
Tactic: rw [δ, Γ₀.Obj.mapMono_on_summand_id_assoc, Γ₀.Obj.Termwise.mapMono_eq_zero, zero_comp,
          zsmul_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : ⦋n + 1⦌ = ⦋n⦌
⊢ False
have h₁ : ⦋n + 1⦌.len = ⦋n⦌.len
Tactic: replace h := congr_arg SimplexCategory.len h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
i : Fin (n + 2)
hi : i ≠ 0
h : ⦋n + 1⦌.len = ⦋n⦌.len
⊢ False
have h₁ : n + 1 = n
Tactic: change n + 1 = n at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
⊢ Eq (α := obj (Γ₀ ⋙ N₁) K ≅ obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K) (Iso.app N₁Γ₀ K)
    (Iso.symm (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≪≫
      mapIso (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₀NondegComplexIso K))
have w : ∀ (i : ℕ),
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) K)) i ⟶
      (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)).X i)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.hom (Iso.app N₁Γ₀ K))) i)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (Iso.hom
          (Iso.symm (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≪≫
            mapIso (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₀NondegComplexIso K))))
      i)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
⊢ Eq (α := obj (Γ₀ ⋙ N₁) K ⟶ obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K) (Iso.hom (Iso.app N₁Γ₀ K))
    (Iso.inv (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≫
      map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.hom (Γ₀NondegComplexIso K)))
have simp : Eq (α := obj (Γ₀ ⋙ N₁) K ⟶ obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)
  (Iso.hom
    (Iso.symm (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≪≫
      mapIso (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₀NondegComplexIso K)))
  (Iso.inv (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≫
    map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.hom (Γ₀NondegComplexIso K)))
Tactic: simp only [N₁Γ₀_app]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
⊢ Eq (α := obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K ⟶ obj (Γ₀ ⋙ N₁) K) (Iso.inv (Iso.app N₁Γ₀ K))
    (map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.inv (Γ₀NondegComplexIso K)) ≫
      Iso.hom (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))
have simp : Eq (α := obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K ⟶ obj (Γ₀ ⋙ N₁) K)
  (Iso.inv
    (Iso.symm (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≪≫
      mapIso (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₀NondegComplexIso K)))
  (map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.inv (Γ₀NondegComplexIso K)) ≫
    Iso.hom (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))
Tactic: simp only [N₁Γ₀_app]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) K)) n ⟶
      (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)).X n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.hom N₁Γ₀) K)) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.inv (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))) n)
have rw : Eq (α :=
  HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) K)) n ⟶
    (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)).X n)
  (HomologicalComplex.Hom.f
    (Karoubi.Hom.f
      (Iso.inv (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)) ≫
        map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.hom (Γ₀NondegComplexIso K))))
    n)
  (HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.inv (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))) n)
Tactic: rw [N₁Γ₀_hom_app]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α :=
    (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)).X n ⟶
      HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) K)) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₁Γ₀) K)) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.hom (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))) n)
have rw : Eq (α :=
  (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) K)).X n ⟶
    HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) K)) n)
  (HomologicalComplex.Hom.f
    (Karoubi.Hom.f
      (map (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Iso.inv (Γ₀NondegComplexIso K)) ≫
        Iso.hom (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K))))
    n)
  (HomologicalComplex.Hom.f (Karoubi.Hom.f (Iso.hom (Splitting.toKaroubiNondegComplexIsoN₁ (Γ₀.splitting K)))) n)
Tactic: rw [N₁Γ₀_inv_app]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : ChainComplex.{v_1, u_1, 0} C ℕ
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) (Karoubi.X (obj (Γ₀ ⋙ N₁) X))
      (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ Γ₂ ⋙ N₂) X)))
    (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂ToKaroubiIso) X)) PInfty
have h : ∀ (n : ℕ),
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) X)) n ⟶
      HomologicalComplex.X (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ Γ₂ ⋙ N₂) X)) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂ToKaroubiIso) X)) n)
    (HomologicalComplex.Hom.f PInfty n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.GammaCompN (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (obj (Γ₀ ⋙ N₁) X)) n ⟶
      HomologicalComplex.X (Karoubi.X (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ) ⋙ Γ₂ ⋙ N₂) X)) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂ToKaroubiIso) X)) n)
    (HomologicalComplex.Hom.f PInfty n)
have h : Eq.{v_1 + 1} (α := Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
  (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
      (HomologicalComplex.Hom.f PInfty n :
        HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n ⟶
          HomologicalComplex.X (Karoubi.X (obj N₂ (obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) (obj Γ₀ X)))) n)
      (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
        (HomologicalComplex.Hom.f PInfty n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
          Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
        (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
            (HomologicalComplex.Hom.f PInfty n ≫ 𝟙 (Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
              Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
            (CategoryStruct.comp (Y := Γ₀.Obj.obj₂ X (op ⦋n⦌))
                (HomologicalComplex.Hom.f PInfty n :
                  HomologicalComplex.X
                      (AlternatingFaceMapComplex.obj (obj Γ₂ (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)).X)
                      n ⟶
                    HomologicalComplex.X
                      (AlternatingFaceMapComplex.obj (obj Γ₂ (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)).X) n)
                (Splitting.desc (Γ₀.splitting X) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
                    𝟙 (X.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len) ≫
                      Cofan.inj (Splitting.cofan (Γ₀.splitting X) (op ⦋n⦌)) A :
                  Γ₀.obj X _⦋n⦌ ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
              Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌)) :
          Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))) :
    Γ₀.Obj.obj₂ X (op ⦋n⦌) ⟶ Γ₀.Obj.obj₂ X (op ⦋n⦌))
  (HomologicalComplex.Hom.f PInfty n :
    HomologicalComplex.X (AlternatingFaceMapComplex.obj (obj Γ₀ X)) n ⟶
      HomologicalComplex.X (Karoubi.X (obj N₂ (obj Γ₂ (obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) X)))) n)
Tactic: dsimp [N₂Γ₂ToKaroubiIso]