awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
⊢ Eq (α := Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Functor.obj N₁ X) (Functor.obj N₁ X))
    ({
        f :=
          { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ :
            HomologicalComplex.Hom (Karoubi.X (Functor.obj N₁ X))
              (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) },
        comm := ⋯ :
        Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj N₁ X)
          (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex) } ≫
      {
        f :=
          { f := fun (n : ℕ) ↦ Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
            comm' := ⋯ },
        comm := ⋯ })
    (𝟙 (Functor.obj N₁ X))
have h : ∀ (n : ℕ),
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) n ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        ({
            f :=
              { f := fun (n : ℕ) ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := sorry :
                HomologicalComplex.Hom (Karoubi.X (Functor.obj N₁ X))
                  (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) },
            comm := sorry :
            Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} C ℕ) (Functor.obj N₁ X)
              (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex) } ≫
          {
            f :=
              {
                f := fun (n : ℕ) ↦
                  Cofan.inj (s.cofan (op ⦋n⦌)) (IndexSet.id (op ⦋n⦌)) ≫ HomologicalComplex.Hom.f PInfty n,
                comm' := sorry },
            comm := sorry }))
      n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ X))) n)
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
s : X.Splitting
inst_1 : Preadditive.{v_1, u_1} C
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) s.nondegComplex s.nondegComplex)
    (Karoubi.Hom.f (Iso.hom s.toKaroubiNondegComplexIsoN₁) ≫ Karoubi.Hom.f (Iso.inv s.toKaroubiNondegComplexIsoN₁))
    (𝟙 s.nondegComplex)
have rw : Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ) s.nondegComplex s.nondegComplex)
  (Karoubi.Hom.f (𝟙 (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)) :
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
      (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex))
      (Karoubi.X (Functor.obj (toKaroubi (ChainComplex.{v_1, u_1, 0} C ℕ)) s.nondegComplex)))
  (𝟙 s.nondegComplex)
Tactic: rw [← dsimp% [-Karoubi.comp_f] Karoubi.comp_f s.toKaroubiNondegComplexIsoN₁.hom
    s.toKaroubiNondegComplexIsoN₁.inv, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (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
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
⊢ Eq (α := HomologicalComplex.X S₁.s.nondegComplex i ⟶ HomologicalComplex.X S₂.s.nondegComplex j)
    (Φ.f i ≫ HomologicalComplex.d S₂.s.nondegComplex i j) (HomologicalComplex.d S₁.s.nondegComplex i j ≫ Φ.f j)
have dsimp : Eq (α := S₁.s.N i ⟶ S₂.s.N j)
  (Φ.f i ≫
    CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₂.s.cofan (op ⦋i⦌)))
      (Cofan.inj (S₂.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)) :
        Splitting.summand S₂.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₂.s.cofan (op ⦋i⦌)))
      (CategoryStruct.comp (Y := S₂.X _⦋j⦌) (HomologicalComplex.d K[S₂.X] i j)
          (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₂.s.cofan (op ⦋i⦌)) ⟶ S₂.s.N j))
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)) :
        Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
      (CategoryStruct.comp (Y := S₁.X _⦋j⦌) (HomologicalComplex.d K[S₁.X] i j)
          (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)) ⟶ S₁.s.N j) ≫
    Φ.f j)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (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
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
⊢ Eq (α := S₁.s.N i ⟶ S₂.s.N j)
    (Φ.f i ≫
      CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₂.s.cofan (op ⦋i⦌)))
        (Cofan.inj (S₂.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)) :
          Splitting.summand S₂.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₂.s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := S₂.X _⦋j⦌) (HomologicalComplex.d K[S₂.X] i j)
            (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₂.s.cofan (op ⦋i⦌)) ⟶ S₂.s.N j))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
        (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)) :
          Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := S₁.X _⦋j⦌) (HomologicalComplex.d K[S₁.X] i j)
            (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)) ⟶ S₁.s.N j) ≫
      Φ.f j)
have erw : Eq (α := S₁.s.N i ⟶ S₂.s.N j)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)))
      (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) S₁.X) i j ≫
        HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
          S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
    Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶ S₂.s.N j)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)) :
        Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
      (CategoryStruct.comp (Y := S₁.X _⦋j⦌) (HomologicalComplex.d K[S₁.X] i j)
          (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)) ⟶ S₁.s.N j) ≫
    Φ.f j)
Tactic: erw [← cofan_inj_naturality_symm_assoc Φ (Splitting.IndexSet.id (op ⦋i⦌)),
          ((alternatingFaceMapComplex C).map Φ.F).comm_assoc i j]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (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
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
⊢ Eq (α := S₁.s.N i ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
        (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)))
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) S₁.X) i j ≫
          HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
            S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
      Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
        (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)) :
          Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
        (CategoryStruct.comp (Y := S₁.X _⦋j⦌) (HomologicalComplex.d K[S₁.X] i j)
            (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)) ⟶ S₁.s.N j) ≫
      Φ.f j)
have simp : Eq (α := S₁.s.N i ⟶ S₂.s.N j)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)))
      (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) S₁.X) i j ≫
        HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
          S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
    Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶ S₂.s.N j)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
    (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)) :
      Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
    (CategoryStruct.comp (Y := S₁.X _⦋j⦌) (HomologicalComplex.d K[S₁.X] i j)
        (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j) :
      Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)) ⟶ S₂.s.N j))
Tactic: simp only [assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (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
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
⊢ Eq (α := S₁.s.N i ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
        (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)))
        (HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex C) S₁.X) i j ≫
          HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
            S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))) :
      Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋i⦌)) (Splitting.IndexSet.id (op ⦋i⦌)) :
        Splitting.summand S₁.s.N (op ⦋i⦌) (Splitting.IndexSet.id (op ⦋i⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)))
      (CategoryStruct.comp (Y := S₁.X _⦋j⦌) (HomologicalComplex.d K[S₁.X] i j)
          (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j) :
        Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋i⦌))) (S₁.s.cofan (op ⦋i⦌)) ⟶ S₂.s.N j))
have e_a : Eq (α := HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) S₁.X) j ⟶ S₂.s.N j)
  (HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
    S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)))
  (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (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
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
⊢ Eq (α := HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex C) S₁.X) j ⟶ S₂.s.N j)
    (HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
      S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)))
    (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j)
have e_a : ∀ (A : Splitting.IndexSet (op ⦋j⦌)),
  Eq (α := Splitting.summand S₁.s.N (op ⦋j⦌) A ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A)
      (HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
        S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
Tactic: apply S₁.s.hom_ext'
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (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
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
⊢ Eq (α := Splitting.summand S₁.s.N (op ⦋j⦌) A ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A)
      (HomologicalComplex.Hom.f (Functor.map (alternatingFaceMapComplex C) Φ.F) j ≫
        S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
have e_a : Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
    (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (Φ.F.app (op ⦋j⦌) ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
    (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
Tactic: dsimp [alternatingFaceMapComplex]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (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
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
⊢ Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (Φ.F.app (op ⦋j⦌) ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
have e_a : Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
  (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
    CategoryStruct.comp (Y := S₂.X _⦋j⦌)
      (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
        Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
      (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
    (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
Tactic: rw [cofan_inj_naturality_symm_assoc Φ A]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (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
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
⊢ Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
have pos : ∀ (h : A.EqId),
  Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
Tactic: by_cases h : A.EqId
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (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
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
pos :
  ∀ (h : A.EqId),
    Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
      (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
        CategoryStruct.comp (Y := S₂.X _⦋j⦌)
          (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
            Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
              Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
          (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
      (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
        (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
⊢ Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
have neg : ∀ (h : ¬A.EqId),
  Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
Tactic: by_cases h : A.EqId
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject (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
S₁ S₂ : Split.{v_1, u_1} C
Φ : S₁ ⟶ S₂
i j : ℕ
h_1 : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
h : A = Splitting.IndexSet.id (op ⦋j⦌)
⊢ Eq (α := S₁.s.N (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α }))).len ⟶ S₂.s.N j)
    (Φ.f (unop (A.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α }))).len ≫
      CategoryStruct.comp (Y := S₂.X _⦋j⦌)
        (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) A :
          Splitting.summand S₂.s.N (op ⦋j⦌) A ⟶
            Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
        (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
    (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
      (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) A) (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
have pos : Eq (α :=
  S₁.s.N
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : ⦋j⦌ ⟶ unop Δ' // Epi α })
            (Splitting.IndexSet.id (op ⦋j⦌)))).len ⟶
    S₂.s.N j)
  (Φ.f
      (unop
          (Sigma.fst (β := fun (Δ' : SimplexCategoryᵒᵖ) ↦ { α : unop (op ⦋j⦌) ⟶ unop Δ' // Epi α })
            (Splitting.IndexSet.id (op ⦋j⦌)))).len ≫
    CategoryStruct.comp (Y := S₂.X _⦋j⦌)
      (Cofan.inj (S₂.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)) :
        Splitting.summand S₂.s.N (op ⦋j⦌) (Splitting.IndexSet.id (op ⦋j⦌)) ⟶
          Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₂.s.cofan (op ⦋j⦌)))
      (S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌))))
  (CategoryStruct.comp (Y := Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋j⦌))) (S₁.s.cofan (op ⦋j⦌)))
    (Cofan.inj (S₁.s.cofan (op ⦋j⦌)) (Splitting.IndexSet.id (op ⦋j⦌)))
    (S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j))
Tactic: subst h
Cleared hypotheses: A, h