awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
Δ'' : SimplexCategory
e : unop Δ' ⟶ Δ''
i : Δ'' ⟶ unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))
inst_3 : Epi e
inst_4 : Mono i
fac : e ≫ i = θ.unop ≫ A.e
⊢ Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
    (Termwise.mapMono K i ≫
      Sigma.ι (summand K Δ')
        (Sigma.mk (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }) (op Δ'')
          (Subtype.mk (p := fun (α : unop Δ' ⟶ Δ'') ↦ Epi α) e ⋯)))
    (Termwise.mapMono K i ≫ 𝟙 (K.X Δ''.len) ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
have rw : Eq (α := K.X (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ⟶ obj₂ K Δ')
  (Termwise.mapMono K i ≫
    Sigma.ι (summand K Δ')
      (Sigma.mk (β := fun (Δ'_1 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_1 // Epi α }) (op Δ'')
        (Subtype.mk (p := fun (α : unop Δ' ⟶ Δ'') ↦ Epi α) e sorry)))
  (Termwise.mapMono K i ≫ Sigma.ι (summand K Δ') (Splitting.IndexSet.mk e))
Tactic: rw [id_comp]
-- 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 ℕ
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
Δ Δ' : SimplexCategoryᵒᵖ
A : Splitting.IndexSet Δ
θ : Δ ⟶ Δ'
⊢ Eq (α := Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ A ⟶ (obj K).obj Δ')
    (Cofan.inj (Splitting.cofan (splitting K) Δ) A ≫ (obj K).map θ)
    (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
      (Cofan.inj (Splitting.cofan (splitting K) Δ') (A.pull θ)))
have fac : CategoryStruct.comp (Y := image (θ.unop ≫ A.e)) (factorThruImage (θ.unop ≫ A.e)) (image.ι (θ.unop ≫ A.e)) = θ.unop ≫ A.e
Tactic: apply Obj.map_on_summand
-- 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'_1 : ChainComplex.{v_1, u_1, 0} C ℕ
f_1 : K_1 ⟶ K'_1
Δ_1 Δ'_1 Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
⊢ ((obj K).map θ ≫
      Splitting.desc (splitting K) Δ fun (A : Splitting.IndexSet Δ) ↦
        f.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
          Cofan.inj (Splitting.cofan (splitting K') Δ) A) =
    (Splitting.desc (splitting K) Δ' fun (A : Splitting.IndexSet Δ') ↦
        f.f (unop (A.fst (β := fun (Δ'_2 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_2 // Epi α }))).len ≫
          Cofan.inj (Splitting.cofan (splitting K') Δ') A) ≫
      (obj K').map θ
have h : ∀ (A : Splitting.IndexSet Δ'),
  Eq (α := Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ' A ⟶ (obj K').obj Δ)
    (Cofan.inj (Splitting.cofan (splitting K) Δ') A ≫
      (obj K).map θ ≫
        Splitting.desc (splitting K) Δ fun (A : Splitting.IndexSet Δ) ↦
          f.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
            Cofan.inj (Splitting.cofan (splitting K') Δ) A)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ'))
        (Splitting.cofan (splitting K) Δ'))
      (Cofan.inj (Splitting.cofan (splitting K) Δ') A :
        Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ' A ⟶
          Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ'))
            (Splitting.cofan (splitting K) Δ'))
      ((Splitting.desc (splitting K) Δ' fun (A : Splitting.IndexSet Δ') ↦
            f.f (unop (A.fst (β := fun (Δ'_2 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_2 // Epi α }))).len ≫
              Cofan.inj (Splitting.cofan (splitting K') Δ') A) ≫
          (obj K').map θ :
        (obj K).obj Δ' ⟶ (obj K').obj Δ))
Tactic: apply (Γ₀.splitting K).hom_ext'
-- 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'_1 : ChainComplex.{v_1, u_1, 0} C ℕ
f_1 : K_1 ⟶ K'_1
Δ_1 Δ'_1 Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
Δ' Δ : SimplexCategoryᵒᵖ
θ : Δ' ⟶ Δ
A : Splitting.IndexSet Δ'
⊢ Eq (α := Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ' A ⟶ (obj K').obj Δ)
    (Cofan.inj (Splitting.cofan (splitting K) Δ') A ≫
      (obj K).map θ ≫
        Splitting.desc (splitting K) Δ fun (A : Splitting.IndexSet Δ) ↦
          f.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
            Cofan.inj (Splitting.cofan (splitting K') Δ) A)
    (CategoryStruct.comp (Y :=
      Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ'))
        (Splitting.cofan (splitting K) Δ'))
      (Cofan.inj (Splitting.cofan (splitting K) Δ') A :
        Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ' A ⟶
          Cocone.pt (F := Discrete.functor (Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ'))
            (Splitting.cofan (splitting K) Δ'))
      ((Splitting.desc (splitting K) Δ' fun (A : Splitting.IndexSet Δ') ↦
            f.f (unop (A.fst (β := fun (Δ'_2 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_2 // Epi α }))).len ≫
              Cofan.inj (Splitting.cofan (splitting K') Δ') A) ≫
          (obj K').map θ :
        (obj K).obj Δ' ⟶ (obj K').obj Δ))
have h : Eq (α := Splitting.summand (Splitting.N (X := obj K) (splitting K)) Δ' A ⟶ (obj K').obj Δ)
  (CategoryStruct.comp (Y := K.X (image (θ.unop ≫ A.e)).len) (Obj.Termwise.mapMono K (image.ι (θ.unop ≫ A.e)))
    (f.f (unop ((A.pull θ).fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop Δ ⟶ unop Δ' // Epi α }))).len ≫
      Cofan.inj (Splitting.cofan (splitting K') Δ) (A.pull θ)))
  (f.f (unop (A.fst (β := fun (Δ'_2 : SimplexCategoryᵒᵖ) ↦ { α : unop Δ' ⟶ unop Δ'_2 // Epi α }))).len ≫
    CategoryStruct.comp (Y := K'.X (image (θ.unop ≫ A.e)).len) (Obj.Termwise.mapMono K' (image.ι (θ.unop ≫ A.e)))
      (Cofan.inj (Splitting.cofan (splitting K') Δ) (A.pull θ)))
Tactic: simp only [(splitting K).ι_desc_assoc, Obj.map_on_summand'_assoc K _ θ, (splitting K).ι_desc,
      assoc, Obj.map_on_summand' K' _ θ]
-- 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'_1 : ChainComplex.{v_1, u_1, 0} C ℕ
f_1 : K_1 ⟶ K'_1
Δ Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
n : ℕ
⊢ (Split.mk' (X := Γ₀.obj K) (Γ₀.splitting K)).s.ι n ≫ NatTrans.app (Γ₀.map f) (op ⦋n⦌) =
    f.f n ≫ (Split.mk' (X := Γ₀.obj K') (Γ₀.splitting K')).s.ι n
have dsimp : Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n ⟶ Γ₀.Obj.obj₂ K' (op ⦋n⦌))
  (Splitting.ι (Γ₀.splitting K) n ≫
    Splitting.desc (Γ₀.splitting K) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
      f.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
        Cofan.inj (Splitting.cofan (Γ₀.splitting K') (op ⦋n⦌)) A)
  (f.f n ≫ Splitting.ι (Γ₀.splitting K') n)
Tactic: dsimp
-- 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'_1 : ChainComplex.{v_1, u_1, 0} C ℕ
f_1 : K_1 ⟶ K'_1
Δ Δ' Δ'' : SimplexCategory
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K K' : ChainComplex.{v_1, u_1, 0} C ℕ
f : K ⟶ K'
n : ℕ
⊢ Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n ⟶ Γ₀.Obj.obj₂ K' (op ⦋n⦌))
    (Splitting.ι (Γ₀.splitting K) n ≫
      Splitting.desc (Γ₀.splitting K) (op ⦋n⦌) fun (A : Splitting.IndexSet (op ⦋n⦌)) ↦
        f.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α }))).len ≫
          Cofan.inj (Splitting.cofan (Γ₀.splitting K') (op ⦋n⦌)) A)
    (f.f n ≫ Splitting.ι (Γ₀.splitting K') n)
have simp : Eq (α := Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K) n ⟶ Γ₀.Obj.obj₂ K' (op ⦋n⦌))
  (f.f
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋n⦌ ⟶ unop Δ' // Epi α })
            (Splitting.IndexSet.id (op ⦋n⦌)))).len ≫
    Cofan.inj (Splitting.cofan (Γ₀.splitting K') (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
  (f.f n ≫ Cofan.inj (Splitting.cofan (Γ₀.splitting K') (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
Tactic: simp only [← Splitting.cofan_inj_id, (Γ₀.splitting K).ι_desc]
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).δ j.succ)
    0
have eq : Eq (α :=
  Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
    Γ₀.obj K _⦋n⦌)
  (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
    (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
  (Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
    Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
Tactic: have eq := Γ₀.Obj.mapMono_on_summand_id K (SimplexCategory.δ j.succ)
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
eq :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
    (Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).δ j.succ)
    0
have rw : ∀
  (eq :
    Eq (α :=
      Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)
          (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
        Γ₀.obj K _⦋n⦌)
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
        (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
      0),
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).δ j.succ)
    0
Tactic: rw [Γ₀.Obj.Termwise.mapMono_eq_zero K, zero_comp] at eq
Cleared hypotheses: eq
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
eq :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
    (Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
rw :
  ∀
    (eq :
      Eq (α :=
        Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)
            (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
          Γ₀.obj K _⦋n⦌)
        (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
          (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
        0),
    Eq (α :=
      Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)
          (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
        Γ₀.obj K _⦋n⦌)
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
        (Γ₀.obj K).δ j.succ)
      0
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).δ j.succ)
    0
have h₁ : ⦋n + 1⦌ ≠ ⦋n⦌
Tactic: rw [Γ₀.Obj.Termwise.mapMono_eq_zero K, zero_comp] at eq
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
eq :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
    (Γ₀.Obj.Termwise.mapMono K (SimplexCategory.δ j.succ) ≫
      Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
rw :
  ∀
    (eq :
      Eq (α :=
        Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)
            (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
          Γ₀.obj K _⦋n⦌)
        (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
          (Γ₀.obj K).map (SimplexCategory.δ j.succ).op)
        0),
    Eq (α :=
      Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌)
          (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
        Γ₀.obj K _⦋n⦌)
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
        (Γ₀.obj K).δ j.succ)
      0
h₁ : ⦋n + 1⦌ ≠ ⦋n⦌
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      Γ₀.obj K _⦋n⦌)
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ≫
      (Γ₀.obj K).δ j.succ)
    0
have h₂ : ¬Isδ₀ (SimplexCategory.δ j.succ)
Tactic: rw [Γ₀.Obj.Termwise.mapMono_eq_zero K, zero_comp] at eq
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
      HomologicalComplex.X K[Γ₀.obj K] n)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌)))
        (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f PInfty n))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
have rw : Eq (α :=
  Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
    HomologicalComplex.X K[Γ₀.obj K] n)
  (CategoryStruct.comp (Y :=
    Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
      Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌)))
      (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
    (HomologicalComplex.Hom.f (P n) n))
  (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
Tactic: rw [PInfty_f]
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
      HomologicalComplex.X K[Γ₀.obj K] n)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌)))
        (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f (P n) n))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
have zero : Eq (α :=
  Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋0⦌) (Splitting.IndexSet.id (op ⦋0⦌)) ⟶
    HomologicalComplex.X K[Γ₀.obj K] 0)
  (CategoryStruct.comp (Y :=
    Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋0⦌))) (F :=
      Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋0⦌)))
      (Splitting.cofan (Γ₀.splitting K) (op ⦋0⦌)))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋0⦌)) (Splitting.IndexSet.id (op ⦋0⦌)))
    (HomologicalComplex.Hom.f (P 0) 0))
  (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋0⦌)) (Splitting.IndexSet.id (op ⦋0⦌)))
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- 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
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
zero :
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋0⦌) (Splitting.IndexSet.id (op ⦋0⦌)) ⟶
      HomologicalComplex.X K[Γ₀.obj K] 0)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋0⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋0⦌)))
        (Splitting.cofan (Γ₀.splitting K) (op ⦋0⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋0⦌)) (Splitting.IndexSet.id (op ⦋0⦌)))
      (HomologicalComplex.Hom.f (P 0) 0))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋0⦌)) (Splitting.IndexSet.id (op ⦋0⦌)))
⊢ Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌) (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
      HomologicalComplex.X K[Γ₀.obj K] n)
    (CategoryStruct.comp (Y :=
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
        Discrete.functor (Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n⦌)))
        (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)))
      (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
      (HomologicalComplex.Hom.f (P n) n))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n⦌)) (Splitting.IndexSet.id (op ⦋n⦌)))
have succ : ∀ (n : ℕ),
  Eq (α :=
    Splitting.summand (Splitting.N (X := Γ₀.obj K) (Γ₀.splitting K)) (op ⦋n + 1⦌) (Splitting.IndexSet.id (op ⦋n + 1⦌)) ⟶
      HomologicalComplex.X K[Γ₀.obj K] (n + 1))
    (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⦌)))
      (HomologicalComplex.Hom.f (P (n + 1)) (n + 1)))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting K) (op ⦋n + 1⦌)) (Splitting.IndexSet.id (op ⦋n + 1⦌)))
Tactic: rcases n with _ | n
Cleared hypotheses: 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
K : ChainComplex.{v_1, u_1, 0} C ℕ
n : ℕ
⊢ Eq (α := HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) (n + 1) ⟶ K.X n)
    (CategoryStruct.comp (Y := K.X (n + 1))
      (Iso.hom
        ((fun (x : ℕ) ↦
            (Iso.refl (HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) x) :
              HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) x ≅
                HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) x))
          (n + 1)))
      (K.d (n + 1) n))
    (HomologicalComplex.d (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) (n + 1) n ≫
      Iso.hom
        ((fun (x : ℕ) ↦
            (Iso.refl (HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) x) :
              HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) x ≅
                HomologicalComplex.X (Splitting.nondegComplex (X := Γ₀.obj K) (Γ₀.splitting K)) x))
          n))
have dsimp : 𝟙 (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)
Tactic: dsimp