awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
n : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
rw :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X.obj (Opposite.op { len := n : SimplexCategory }))
    (((kernelSubobject (X.δ j.succ)).factorThru
          (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
        (kernelSubobject (X.δ j.succ)).arrow) ≫
      X.δ j.succ)
    0
rw₁ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X.obj (Opposite.op { len := n : SimplexCategory }))
    ((kernelSubobject (X.δ j.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ j.succ)).arrow ≫ X.δ j.succ)
    0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X.obj (Opposite.op { len := n : SimplexCategory }))
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ j.succ) 0
have rw₂ : Eq (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    X.obj (Opposite.op { len := n : SimplexCategory }))
  ((kernelSubobject (X.δ j.succ)).factorThru
      (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) sorry ≫
    0)
  0
Tactic: rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j
    (by simp)), assoc, kernelSubobject_arrow_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
n : ℕ
j : Fin (n + 1)
h : n + 1 ≤ (↑j : ℕ) + (n + 1)
rw :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X.obj (Opposite.op { len := n : SimplexCategory }))
    (((kernelSubobject (X.δ j.succ)).factorThru
          (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
        (kernelSubobject (X.δ j.succ)).arrow) ≫
      X.δ j.succ)
    0
rw₁ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X.obj (Opposite.op { len := n : SimplexCategory }))
    ((kernelSubobject (X.δ j.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      (kernelSubobject (X.δ j.succ)).arrow ≫ X.δ j.succ)
    0
rw₂ :
  Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X.obj (Opposite.op { len := n : SimplexCategory }))
    ((kernelSubobject (X.δ j.succ)).factorThru
        (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ))) ⋯ ≫
      0)
    0
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
        (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
      X.obj (Opposite.op { len := n : SimplexCategory }))
    (arrow (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ≫ X.δ j.succ) 0
have rw₃ : Eq.{v_1 + 1} (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := n + 1 : SimplexCategory }))) underlying
      (Finset.inf Finset.univ fun (k : Fin (n + 1)) ↦ kernelSubobject (X.δ k.succ)) ⟶
    X.obj (Opposite.op { len := n : SimplexCategory }))
  0 0
Tactic: rw [← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ j
    (by simp)), assoc, kernelSubobject_arrow_comp, comp_zero]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
n : ℕ
⊢ (NormalizedMooreComplex.objX X n).Factors (X := HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f PInfty n)
have zero : Factors (X := HomologicalComplex.X K[X] 0) (NormalizedMooreComplex.objX X 0) (HomologicalComplex.Hom.f PInfty 0)
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
n : ℕ
zero : Factors (X := HomologicalComplex.X K[X] 0) (NormalizedMooreComplex.objX X 0) (HomologicalComplex.Hom.f PInfty 0)
⊢ (NormalizedMooreComplex.objX X n).Factors (X := HomologicalComplex.X K[X] n) (HomologicalComplex.Hom.f PInfty n)
have succ : ∀ (n : ℕ),
  Factors (X := HomologicalComplex.X K[X] (n + 1)) (NormalizedMooreComplex.objX X (n + 1))
    (HomologicalComplex.Hom.f PInfty (n + 1))
Tactic: rcases n with _ | n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
n : ℕ
⊢ Factors (X := HomologicalComplex.X K[X] (n + 1)) (NormalizedMooreComplex.objX X (n + 1))
    (HomologicalComplex.Hom.f PInfty (n + 1))
have succ : ∀ (i : Fin (n + 1)),
  Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i →
    (kernelSubobject (X.δ i.succ)).Factors (X := HomologicalComplex.X K[X] (n + 1))
      (HomologicalComplex.Hom.f (P (n + 1)) (n + 1))
Tactic: rw [PInfty_f, NormalizedMooreComplex.objX, finset_inf_factors]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
n : ℕ
i : Fin (n + 1)
h : Membership.mem (γ := Finset (Fin (n + 1))) Finset.univ i
⊢ (kernelSubobject (X.δ i.succ)).Factors (X := HomologicalComplex.X K[X] (n + 1))
    (HomologicalComplex.Hom.f (P (n + 1)) (n + 1))
have succ : Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ X.obj (Opposite.op { len := n }))
  (HomologicalComplex.Hom.f (P (n + 1)) (n + 1) ≫ X.δ i.succ) 0
Tactic: apply kernelSubobject_factors
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X_1 X : SimplicialObject.{v_1, u_1} A
n : ℕ
⊢ Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X N[X] n)
    (CategoryStruct.comp (Y := HomologicalComplex.X N[X] (n + 1))
      ((fun (n : ℕ) ↦ (NormalizedMooreComplex.objX X n).factorThru (HomologicalComplex.Hom.f PInfty n) ⋯) (n + 1))
      (HomologicalComplex.d N[X] (n + 1) n))
    (HomologicalComplex.d K[X] (n + 1) n ≫
      (fun (n : ℕ) ↦ (NormalizedMooreComplex.objX X n).factorThru (HomologicalComplex.Hom.f PInfty n) ⋯) n)
have rw : Eq (α := HomologicalComplex.X K[X] (n + 1) ⟶ X.obj (Opposite.op { len := n }))
  (HomologicalComplex.Hom.f PInfty (n + 1) ≫
    HomologicalComplex.d (Functor.obj (alternatingFaceMapComplex A) X) (n + 1) n)
  (HomologicalComplex.d K[X] (n + 1) n ≫ HomologicalComplex.Hom.f PInfty n)
Tactic: rw [← cancel_mono (NormalizedMooreComplex.objX X n).arrow, assoc, assoc, factorThru_arrow,
      ← inclusionOfMooreComplexMap_f, NormalizedMooreComplex.obj_d, ChainComplex.of_d,
      ← normalizedMooreComplex_objD, ← (inclusionOfMooreComplexMap X).comm (n + 1) n,
      inclusionOfMooreComplexMap_f, factorThru_arrow_assoc, alternatingFaceMapComplex_obj_d,
      ← alternatingFaceMapComplex_obj_d]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ) (Functor.obj (normalizedMooreComplex A) X) K[X])
    (inclusionOfMooreComplexMap X ≫ PInfty) (inclusionOfMooreComplexMap X)
have h : Eq (α := HomologicalComplex.X (Functor.obj (normalizedMooreComplex A) X) 0 ⟶ HomologicalComplex.X K[X] 0)
  (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) 0)
  (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0)
Tactic: ext (_ | n)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
h :
  Eq (α := HomologicalComplex.X (Functor.obj (normalizedMooreComplex A) X) 0 ⟶ HomologicalComplex.X K[X] 0)
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) 0)
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0)
⊢ Eq (α := Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ) (Functor.obj (normalizedMooreComplex A) X) K[X])
    (inclusionOfMooreComplexMap X ≫ PInfty) (inclusionOfMooreComplexMap X)
have h₁ : ∀ (n : ℕ),
  Eq (α := HomologicalComplex.X (Functor.obj (normalizedMooreComplex A) X) (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) (n + 1))
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) (n + 1))
Tactic: ext (_ | n)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
⊢ Eq (α := HomologicalComplex.X (Functor.obj (normalizedMooreComplex A) X) 0 ⟶ HomologicalComplex.X K[X] 0)
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X ≫ PInfty) 0)
    (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0)
have h : Eq (α :=
  Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := 0 : SimplexCategory }))) underlying ⊤ ⟶
    X.obj (Opposite.op { len := 0 : SimplexCategory }))
  (CategoryStruct.comp (Y := X.obj (Opposite.op { len := 0 }))
      (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0 :
        HomologicalComplex.X N[X] 0 ⟶ HomologicalComplex.X (Functor.obj (alternatingFaceMapComplex A) X) 0)
      (𝟙 (X.obj (Opposite.op { len := 0 : SimplexCategory }))) :
    Functor.obj (C := Subobject.{v_1, u_1} (X.obj (Opposite.op { len := 0 : SimplexCategory }))) underlying ⊤ ⟶
      X.obj (Opposite.op { len := 0 : SimplexCategory }))
  (HomologicalComplex.Hom.f (inclusionOfMooreComplexMap X) 0 :
    HomologicalComplex.X N[X] 0 ⟶ HomologicalComplex.X K[X] 0)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
Z : ChainComplex.{v_1, u_1, 0} A ℕ
x x_1 : Z ⟶ Functor.obj (normalizedMooreComplex A) X
hf : x ≫ inclusionOfMooreComplexMap X = x_1 ≫ inclusionOfMooreComplexMap X
⊢ x = x_1
have h : ∀ (n : ℕ), x.f n = x_1.f n
Tactic: ext n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
Z : ChainComplex.{v_1, u_1, 0} A ℕ
x x_1 : Z ⟶ Functor.obj (normalizedMooreComplex A) X
hf : x ≫ inclusionOfMooreComplexMap X = x_1 ≫ inclusionOfMooreComplexMap X
n : ℕ
⊢ x.f n = x_1.f n
have h : x.f n = x_1.f n
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
Z : ChainComplex.{v_1, u_1, 0} A ℕ
x x_1 : Z ⟶ Functor.obj (normalizedMooreComplex A) X
hf : x ≫ inclusionOfMooreComplexMap X = x_1 ≫ inclusionOfMooreComplexMap X
n : ℕ
⊢ x.f n = x_1.f n
have h : x.f n ≫ (NormalizedMooreComplex.objX X n).arrow = x_1.f n ≫ (NormalizedMooreComplex.objX X n).arrow
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
⊢ Eq (α := Quiver.Hom (V := SimplicialObject.{v_1, u_1} A ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁ N₁)
    ({
        app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
          { f := PInftyToNormalizedMooreComplex X, comm := ⋯ :
            Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ) (Functor.obj N₁ X)
              (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X) },
        naturality := ⋯ :
        NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁
          (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) } ≫
      { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := inclusionOfMooreComplexMap X, comm := ⋯ },
        naturality := ⋯ })
    (𝟙 N₁)
have w : ∀ (X : SimplicialObject.{v_1, u_1} A),
  Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ) (Karoubi.X (Functor.obj N₁ X)) (Karoubi.X (Functor.obj N₁ X)))
    (Karoubi.Hom.f
      (NatTrans.app
        ({
            app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
              { f := PInftyToNormalizedMooreComplex X, comm := sorry :
                Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ) (Functor.obj N₁ X)
                  (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X) },
            naturality := sorry :
            NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁
              (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) } ≫
          { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := inclusionOfMooreComplexMap X, comm := sorry },
            naturality := sorry })
        X))
    (Karoubi.Hom.f (NatTrans.app (𝟙 N₁) X))
Tactic: ext X : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X : SimplicialObject.{v_1, u_1} A
⊢ Eq (α :=
    Quiver.Hom (V := SimplicialObject.{v_1, u_1} A ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ))
      (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ))
      (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)))
    ({
        app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
          { f := inclusionOfMooreComplexMap X, comm := ⋯ :
            Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ)
              (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)
              (Functor.obj N₁ X) },
        naturality := ⋯ :
        NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ))
          (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁ } ≫
      { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ },
        naturality := ⋯ })
    (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)))
have w : ∀ (X : SimplicialObject.{v_1, u_1} A),
  Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
      (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
      (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)))
    (Karoubi.Hom.f
      (NatTrans.app
        ({
            app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
              { f := inclusionOfMooreComplexMap X, comm := sorry :
                Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ)
                  (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)
                  (Functor.obj N₁ X) },
            naturality := sorry :
            NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ))
              (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁ } ≫
          { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := PInftyToNormalizedMooreComplex X, comm := sorry },
            naturality := sorry })
        X))
    (Karoubi.Hom.f (NatTrans.app (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ))) X))
Tactic: ext X : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X_1 X : SimplicialObject.{v_1, u_1} A
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
      (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
      (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)))
    (Karoubi.Hom.f
      (NatTrans.app
        ({
            app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
              { f := inclusionOfMooreComplexMap X, comm := ⋯ :
                Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ)
                  (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)
                  (Functor.obj N₁ X) },
            naturality := ⋯ :
            NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ))
              (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁ } ≫
          { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ },
            naturality := ⋯ })
        X))
    (Karoubi.Hom.f (NatTrans.app (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ))) X))
have w : Eq (α :=
  Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
    (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
    (Functor.obj (alternatingFaceMapComplex A) X))
  (CategoryStruct.comp (Y := Functor.obj (normalizedMooreComplex A) X)
    (Karoubi.Hom.f
        (NatTrans.app
          ({
              app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
                { f := inclusionOfMooreComplexMap X, comm := sorry :
                  Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ)
                    (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)
                    (Functor.obj N₁ X) },
              naturality := sorry :
              NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ))
                (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁ } ≫
            { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := PInftyToNormalizedMooreComplex X, comm := sorry },
              naturality := sorry })
          X) :
      Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
        (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
        (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)))
    (inclusionOfMooreComplexMap X))
  (Karoubi.Hom.f (NatTrans.app (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ))) X) ≫
    inclusionOfMooreComplexMap X)
Tactic: rw [← cancel_mono (inclusionOfMooreComplexMap X)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X_1 X : SimplicialObject.{v_1, u_1} A
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
      (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
      (Functor.obj (alternatingFaceMapComplex A) X))
    (CategoryStruct.comp (Y := Functor.obj (normalizedMooreComplex A) X)
      (Karoubi.Hom.f
          (NatTrans.app
            ({
                app := fun (X : SimplicialObject.{v_1, u_1} A) ↦
                  { f := inclusionOfMooreComplexMap X, comm := ⋯ :
                    Karoubi.Hom (C := ChainComplex.{v_1, u_1, 0} A ℕ)
                      (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)
                      (Functor.obj N₁ X) },
                naturality := ⋯ :
                NatTrans (C := SimplicialObject.{v_1, u_1} A) (D := Karoubi (ChainComplex.{v_1, u_1, 0} A ℕ))
                  (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) N₁ } ≫
              { app := fun (X : SimplicialObject.{v_1, u_1} A) ↦ { f := PInftyToNormalizedMooreComplex X, comm := ⋯ },
                naturality := ⋯ })
            X) :
        Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
          (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
          (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X)))
      (inclusionOfMooreComplexMap X))
    (Karoubi.Hom.f (NatTrans.app (𝟙 (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ))) X) ≫
      inclusionOfMooreComplexMap X)
have w : Eq (α :=
  Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ)
    (Karoubi.X (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X))
    (Functor.obj (alternatingFaceMapComplex A) X))
  (inclusionOfMooreComplexMap X)
  (Karoubi.p (Functor.obj (normalizedMooreComplex A ⋙ toKaroubi (ChainComplex.{v_1, u_1, 0} A ℕ)) X) ≫
    inclusionOfMooreComplexMap X)
Tactic: simp only [NatTrans.comp_app, Karoubi.comp_f, assoc, NatTrans.id_app, Karoubi.id_f,
      PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,
      inclusionOfMooreComplexMap_comp_PInfty]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Normalized (goal)
Goal:
A : Type u_1
inst : Category.{v_1, u_1} A
inst_1 : Abelian.{v_1, u_1} A
X_1 X : SimplicialObject.{v_1, u_1} A
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ) (Functor.obj (normalizedMooreComplex A) X)
      (Functor.obj (alternatingFaceMapComplex A) X))
    (inclusionOfMooreComplexMap X) (𝟙 (Functor.obj (normalizedMooreComplex A) X) ≫ inclusionOfMooreComplexMap X)
have w : Eq (α :=
  Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} A ℕ) (Functor.obj (normalizedMooreComplex A) X)
    (Functor.obj (alternatingFaceMapComplex A) X))
  (inclusionOfMooreComplexMap X) (inclusionOfMooreComplexMap X)
Tactic: rw [id_comp]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.PInfty (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 : ℕ
hqn : n + 1 ≤ q
⊢ Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
    (HomologicalComplex.Hom.f (P (q + 1)) (n + 1)) (HomologicalComplex.Hom.f (P q) (n + 1))
have succ : Eq.{v_1 + 1} (α := HomologicalComplex.X K[X] (n + 1) ⟶ HomologicalComplex.X K[X] (n + 1))
  (HomologicalComplex.Hom.f (P q) (n + 1) ≫ HomologicalComplex.Hom.f (Hσ q) (n + 1)) 0
Tactic: simp only [P_succ, comp_add, comp_id, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
      add_eq_left]