awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
h₁₀ :
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) 0 ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) 0)
    (HomologicalComplex.Hom.f PInfty 0 ≫
      f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0)
    (HomologicalComplex.Hom.f PInfty 0)
⊢ f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 = 𝟙 (X _⦋0⦌) ∧
    Eq (α := Y _⦋0⦌ ⟶ Y _⦋0⦌)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫ f.app (op ⦋0⦌) :
        Y _⦋0⦌ ⟶ Y _⦋0⦌)
      (𝟙 (Y _⦋0⦌) : Y _⦋0⦌ ⟶ Y _⦋0⦌)
have h₂₀ : Eq (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) 0 ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) 0)
  (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫
    HomologicalComplex.Hom.f PInfty 0 ≫ f.app (op ⦋0⦌))
  (HomologicalComplex.Hom.f PInfty 0)
Tactic: have h₂₀ := h₂ 0
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
h₁₀ :
  𝟙 (X _⦋0⦌) ≫ f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 =
    𝟙 (X _⦋0⦌)
h₂₀ :
  Eq (α := Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫ 𝟙 (X _⦋0⦌) ≫ f.app (op ⦋0⦌) :
      Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (𝟙 (Y _⦋0⦌) : Y _⦋0⦌ ⟶ Y _⦋0⦌)
⊢ f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 = 𝟙 (X _⦋0⦌) ∧
    Eq (α := Y _⦋0⦌ ⟶ Y _⦋0⦌)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫ f.app (op ⦋0⦌) :
        Y _⦋0⦌ ⟶ Y _⦋0⦌)
      (𝟙 (Y _⦋0⦌) : Y _⦋0⦌ ⟶ Y _⦋0⦌)
have h₁₁ : f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 = 𝟙 (X _⦋0⦌)
Tactic: simp only [id_comp] at h₁₀ h₂₀
Cleared hypotheses: h₁₀, h₂₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (hypothesis)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
h₁₀ :
  𝟙 (X _⦋0⦌) ≫ f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 =
    𝟙 (X _⦋0⦌)
h₂₀ :
  Eq (α := Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫ 𝟙 (X _⦋0⦌) ≫ f.app (op ⦋0⦌) :
      Y _⦋0⦌ ⟶ Y _⦋0⦌)
    (𝟙 (Y _⦋0⦌) : Y _⦋0⦌ ⟶ Y _⦋0⦌)
h₁₁ : f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 = 𝟙 (X _⦋0⦌)
⊢ f.app (op ⦋0⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 = 𝟙 (X _⦋0⦌) ∧
    Eq (α := Y _⦋0⦌ ⟶ Y _⦋0⦌)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫ f.app (op ⦋0⦌) :
        Y _⦋0⦌ ⟶ Y _⦋0⦌)
      (𝟙 (Y _⦋0⦌) : Y _⦋0⦌ ⟶ Y _⦋0⦌)
have h₂₁ : Eq (α := Y _⦋0⦌ ⟶ Y _⦋0⦌)
  (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) 0 ≫ f.app (op ⦋0⦌) :
    Y _⦋0⦌ ⟶ Y _⦋0⦌)
  (𝟙 (Y _⦋0⦌) : Y _⦋0⦌ ⟶ Y _⦋0⦌)
Tactic: simp only [id_comp] at h₁₀ h₂₀
Cleared hypotheses: h₁₀, h₂₀
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
n : ℕ
hn : IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
⊢ IsIso (X := X _⦋n + 1⦌) (f.app (op ⦋n + 1⦌))
have h : f.app (op ⦋n + 1⦌) ≫
      φ
        {
          a :=
            CategoryStruct.comp (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj Y) (n + 1))
              (HomologicalComplex.Hom.f PInfty (n + 1))
              (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) (n + 1)),
          b := fun (i : Fin (n + 1)) ↦ inv (f.app (op ⦋n⦌)) ≫ X.σ i } =
    𝟙 (X _⦋n + 1⦌) ∧
  φ
        {
          a :=
            CategoryStruct.comp (Y := HomologicalComplex.X (AlternatingFaceMapComplex.obj Y) (n + 1))
              (HomologicalComplex.Hom.f PInfty (n + 1))
              (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) (n + 1)),
          b := fun (i : Fin (n + 1)) ↦ inv (f.app (op ⦋n⦌)) ≫ X.σ i } ≫
      f.app (op ⦋n + 1⦌) =
    𝟙 (Y _⦋n + 1⦌)
Tactic: use φ { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1)
              b := fun i => inv (f.app (op ⦋n⦌)) ≫ X.σ i }
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
n : ℕ
⊢ IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
have zero : IsIso (X := X _⦋0⦌) (f.app (op ⦋0⦌))
Tactic: induction n with
    -- degree 0
    | zero =>
      use (inv (N₁.map f)).f.f 0
      have h₁₀ := h₁ 0
      have h₂₀ := h₂ 0
      dsimp at h₁₀ h₂₀
      simp only [id_comp] at h₁₀ h₂₀
      tauto
    | succ n hn =>
      use φ { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1)
              b := fun i => inv (f.app (op ⦋n⦌)) ≫ X.σ i }
      simp only [MorphComponents.id, ← id_φ, ← preComp_φ, preComp, ← postComp_φ, postComp,
        PInfty_f_naturality_assoc, IsIso.hom_inv_id_assoc, assoc, IsIso.inv_hom_id_assoc,
        SimplicialObject.σ_naturality, h₁, h₂, h₃, and_self]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
X Y : SimplicialObject.{v_1, u_1} C
f : X ⟶ Y
inst_2 : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X := Functor.obj N₁ X) (CategoryTheory.Functor.map N₁ f)
h₂ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i ≫
        HomologicalComplex.Hom.f PInfty i ≫ f.app (op ⦋i⦌))
      (HomologicalComplex.Hom.f PInfty i)
h₃ :
  ∀ (n : ℕ),
    Eq.{v_1 + 1} (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f PInfty n ≫
        HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫ f.app (op ⦋n⦌))
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) n ≫
        HomologicalComplex.Hom.f PInfty n ≫ f.app (op ⦋n⦌))
h₁ :
  ∀ (i : ℕ),
    Eq (α :=
      HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f PInfty i ≫
        f.app (op ⦋i⦌) ≫ HomologicalComplex.Hom.f (Karoubi.Hom.f (inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f PInfty i)
n : ℕ
zero : IsIso (X := X _⦋0⦌) (f.app (op ⦋0⦌))
⊢ IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
have succ : ∀ (n : ℕ) (hn : IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))), IsIso (X := X _⦋n + 1⦌) (f.app (op ⦋n + 1⦌))
Tactic: induction n with
    -- degree 0
    | zero =>
      use (inv (N₁.map f)).f.f 0
      have h₁₀ := h₁ 0
      have h₂₀ := h₂ 0
      dsimp at h₁₀ h₂₀
      simp only [id_comp] at h₁₀ h₂₀
      tauto
    | succ n hn =>
      use φ { a := PInfty.f (n + 1) ≫ (inv (N₁.map f)).f.f (n + 1)
              b := fun i => inv (f.app (op ⦋n⦌)) ≫ X.σ i }
      simp only [MorphComponents.id, ← id_φ, ← preComp_φ, preComp, ← postComp_φ, postComp,
        PInfty_f_naturality_assoc, IsIso.hom_inv_id_assoc, assoc, IsIso.inv_hom_id_assoc,
        SimplicialObject.σ_naturality, h₁, h₂, h₃, and_self]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
⊢ Eq (α := Karoubi (SimplicialObject.{v_1, u_1} C) ⥤ ChainComplex (Karoubi.{v_1, u_1} C) ℕ)
    (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ))
    (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
      Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
        (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
          Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
have refine_1 : ∀ (P : Karoubi (SimplicialObject.{v_1, u_1} C)),
  Eq (α := ChainComplex (Karoubi.{v_1, u_1} C) ℕ)
    (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P)
    (Functor.obj
      (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
        Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
          (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
            Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
      P)
Tactic: refine CategoryTheory.Functor.ext (fun P => ?_) fun P Q f => ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
refine_1 :
  ∀ (P : Karoubi (SimplicialObject.{v_1, u_1} C)),
    Eq (α := ChainComplex (Karoubi.{v_1, u_1} C) ℕ)
      (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P)
      (Functor.obj
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
            (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
              Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
        P)
⊢ Eq (α := Karoubi (SimplicialObject.{v_1, u_1} C) ⥤ ChainComplex (Karoubi.{v_1, u_1} C) ℕ)
    (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ))
    (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
      Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
        (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
          Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
have refine_2 : ∀ (P Q : Karoubi (SimplicialObject.{v_1, u_1} C)) (f : P ⟶ Q),
  Eq (α :=
    Quiver.Hom (V := ChainComplex (Karoubi.{v_1, u_1} C) ℕ)
      (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P)
      (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) Q))
    (CategoryTheory.Functor.map (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) f)
    (CategoryStruct.comp (Y :=
      Functor.obj
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
            (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
              Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
        P)
      (eqToHom sorry)
      (CategoryTheory.Functor.map
          (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
              (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                  (ComplexShape.down ℕ)))
          f ≫
        eqToHom sorry))
Tactic: refine CategoryTheory.Functor.ext (fun P => ?_) fun P Q f => ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
⊢ Eq (α := ChainComplex (Karoubi.{v_1, u_1} C) ℕ)
    (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P)
    (Functor.obj
      (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
        Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
          (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
            Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
      P)
have refine_1 : HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) =
  HomologicalComplex.X
    (Functor.obj
      (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
        Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
          (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
            Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
      P)
Tactic: refine HomologicalComplex.ext ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
refine_1 :
  HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) =
    HomologicalComplex.X
      (Functor.obj
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
            (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
              Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
        P)
⊢ Eq (α := ChainComplex (Karoubi.{v_1, u_1} C) ℕ)
    (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P)
    (Functor.obj
      (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
        Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
          (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
            Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
      P)
have refine_1₁ : ∀ (i j : ℕ),
  (ComplexShape.down ℕ).Rel i j →
    Eq (α :=
      HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) i ⟶
        HomologicalComplex.X
          (Functor.obj
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
                (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                  Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                    (ComplexShape.down ℕ)))
            P)
          j)
      (HomologicalComplex.d (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) i j ≫
        eqToHom sorry)
      (eqToHom sorry ≫
        HomologicalComplex.d
          (Functor.obj
            (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
              Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
                (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                  Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                    (ComplexShape.down ℕ)))
            P)
          i j)
Tactic: refine HomologicalComplex.ext ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NReflectsIso (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
P : Karoubi (SimplicialObject.{v_1, u_1} C)
⊢ HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) =
    HomologicalComplex.X
      (Functor.obj
        (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
          Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
            (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
              Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C)) (ComplexShape.down ℕ)))
        P)
have refine_1 : ∀ (n : ℕ),
  (HomologicalComplex.X (Functor.obj (N₂ ⋙ Equivalence.functor (karoubiChainComplexEquivalence C ℕ)) P) n).X =
    (HomologicalComplex.X
        (Functor.obj
          (karoubiFunctorCategoryEmbedding SimplexCategoryᵒᵖ C ⋙
            Functor.comp (D := Karoubi (ChainComplex (Karoubi.{v_1, u_1} C) ℕ)) N₁
              (Equivalence.functor (karoubiChainComplexEquivalence (Karoubi.{v_1, u_1} C) ℕ) ⋙
                Functor.mapHomologicalComplex (Equivalence.inverse (KaroubiKaroubi.equivalence C))
                  (ComplexShape.down ℕ)))
          P)
        n).X
Tactic: ext n