awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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
P : Karoubi (SimplicialObject.{v_1, u_1} C)
n : ℕ
eq₁ :
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))) n ⟶
      HomologicalComplex.X
        (Karoubi.X (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))) n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))) n)
    (HomologicalComplex.Hom.f PInfty n ≫
      P.p.app (op ⦋n⦌) ≫
        Cofan.inj (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌))
          (Splitting.IndexSet.id (op ⦋n⦌)))
⊢ Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))) n ⟶
      HomologicalComplex.X (Karoubi.X (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))) n)
    (HomologicalComplex.Hom.f
      (Karoubi.Hom.f
        (CategoryStruct.comp (Y :=
          Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))
          (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))
          (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))))
      n)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₂ P))) n)
have eq₂ : Eq (α :=
  Splitting.summand
      (Splitting.N (X := Γ₀.obj (Karoubi.X (Functor.obj N₂ P))) (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P)))) (op ⦋n⦌)
      (Splitting.IndexSet.id (op ⦋n⦌)) ⟶
    HomologicalComplex.X (Karoubi.X (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))) n)
  (CategoryStruct.comp (Y :=
    Cocone.pt (J := Discrete (Splitting.IndexSet (op ⦋n⦌))) (F :=
      Discrete.functor
        (Splitting.summand
          (Splitting.N (X := Γ₀.obj (Karoubi.X (Functor.obj N₂ P))) (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))))
          (op ⦋n⦌)))
      (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌)))
    (Cofan.inj (Splitting.cofan (Γ₀.splitting (Karoubi.X (Functor.obj N₂ P))) (op ⦋n⦌))
      (Splitting.IndexSet.id (op ⦋n⦌)))
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))) n))
  (HomologicalComplex.Hom.f PInfty n ≫ P.p.app (op ⦋n⦌))
Tactic: have eq₂ : ((Γ₀.splitting (N₂.obj P).X).cofan _).inj (Splitting.IndexSet.id (op ⦋n⦌)) ≫
      (N₂.map (Γ₂N₂.natTrans.app P)).f.f n = PInfty.f n ≫ P.p.app (op ⦋n⦌) := by
    dsimp
    rw [PInfty_on_Γ₀_splitting_summand_eq_self_assoc, Γ₂N₂.natTrans_app_f_app]
    dsimp
    rw [Γ₂N₂ToKaroubiIso_hom_app, assoc, Splitting.ι_desc_assoc, assoc, assoc]
    dsimp [toKaroubi]
    rw [Splitting.ι_desc_assoc]
    simp [Splitting.IndexSet.e]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (SimplicialObject.{v_1, u_1} C) ⥤ Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (N₂ ⋙ 𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C)) ⋙ N₂))
    (CategoryStruct.comp (Y := Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ (Γ₂ ⋙ N₂))
      (𝟙 N₂ ◫ Iso.inv N₂Γ₂) (Iso.inv (Functor.associator N₂ Γ₂ N₂) ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂))
    (𝟙 N₂)
have w : ∀ (P : Karoubi (SimplicialObject.{v_1, u_1} C)),
  Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (N₂ ⋙ 𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) P)
      (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C)) ⋙ N₂) P))
    (NatTrans.app
      (CategoryStruct.comp (Y := Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ (Γ₂ ⋙ N₂))
        (𝟙 N₂ ◫ Iso.inv N₂Γ₂) (Iso.inv (Functor.associator N₂ Γ₂ N₂) ≫ Γ₂N₂.natTrans ◫ 𝟙 N₂))
      P)
    (NatTrans.app (𝟙 N₂) P)
Tactic: ext P : 2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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
P : Karoubi (SimplicialObject.{v_1, u_1} C)
⊢ Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
      (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (CategoryStruct.comp (Y :=
        Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
        (CategoryStruct.comp (Y :=
          Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
          (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))
          (CategoryTheory.Functor.map N₂ (CategoryTheory.Functor.map Γ₂ (𝟙 (Functor.obj N₂ P)))))
        (𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))) ≫
          𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))) ≫
            CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)) :
      Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
        (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
        (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
    (𝟙 (Functor.obj N₂ P) :
      Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Functor.obj N₂ P) (Functor.obj N₂ P))
have w : Eq (α :=
  Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
    (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
    (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
  (CategoryStruct.comp (Y :=
      Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
      (CategoryStruct.comp (Y :=
        Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
        (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P))
        (CategoryTheory.Functor.map N₂
          (𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))))
      (𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))) ≫
        𝟙 (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P))) ≫
          CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)) :
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
      (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
  (𝟙 (Functor.obj N₂ P) :
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Functor.obj N₂ P) (Functor.obj N₂ P))
Tactic: rw [Γ₂.map_id, N₂.map_id, comp_id, id_comp, id_comp, identity_N₂_objectwise P]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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
P : Karoubi (SimplicialObject.{v_1, u_1} C)
⊢ IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X :=
    Functor.obj N₂ (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P))
    (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))
have h : Eq (α :=
  Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
    (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N₂ P))
    (Functor.obj N₂ (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)))
  (CategoryStruct.comp (Y := Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N₂ P))
    (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)) (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)))
  (𝟙 (Functor.obj N₂ P))
Tactic: have h := identity_N₂_objectwise P
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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
P : Karoubi (SimplicialObject.{v_1, u_1} C)
h :
  Eq (α := Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Functor.obj N₂ P) (Functor.obj N₂ P))
    (CategoryStruct.comp (Y :=
      Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
      (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)) (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)))
    (𝟙 (Functor.obj N₂ P))
⊢ IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X :=
    Functor.obj N₂ (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P))
    (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))
have h₁ : Eq (α :=
  Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
    (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
    (Functor.obj N₂ P))
  (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P)) (inv (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)))
Tactic: rw [hom_comp_eq_id] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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
P : Karoubi (SimplicialObject.{v_1, u_1} C)
h :
  Eq (α :=
    Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
      (Functor.obj N₂ (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₂ P)))
      (Functor.obj N₂ P))
    (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))
    (inv (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)))
⊢ IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X :=
    Functor.obj N₂ (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P))
    (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))
have rw : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X :=
  Functor.obj N₂ (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P))
  (inv (NatTrans.app (Iso.inv N₂Γ₂) (Functor.obj N₂ P)))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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
P : Karoubi (SimplicialObject.{v_1, u_1} C)
⊢ IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)
    (NatTrans.app Γ₂N₂.natTrans P)
have this : IsIso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (X :=
  Functor.obj N₂ (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P))
  (CategoryTheory.Functor.map N₂ (NatTrans.app Γ₂N₂.natTrans P))
Tactic: have : IsIso (N₂.map (Γ₂N₂.natTrans.app P)) := by
      have h := identity_N₂_objectwise P
      dsimp only [Functor.id_obj, Functor.comp_obj] at h
      rw [hom_comp_eq_id] at h
      rw [h]
      infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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
⊢ IsIso (C := Karoubi (SimplicialObject.{v_1, u_1} C) ⥤ Karoubi (SimplicialObject.{v_1, u_1} C)) (X :=
    Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) Γ₂N₂.natTrans
have this : ∀ (P : Karoubi (SimplicialObject.{v_1, u_1} C)),
  IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)
    (NatTrans.app Γ₂N₂.natTrans P)
Tactic: have : ∀ P : Karoubi (SimplicialObject C), IsIso (Γ₂N₂.natTrans.app P) := by
    intro P
    have : IsIso (N₂.map (Γ₂N₂.natTrans.app P)) := by
      have h := identity_N₂_objectwise P
      dsimp only [Functor.id_obj, Functor.comp_obj] at h
      rw [hom_comp_eq_id] at h
      rw [h]
      infer_instance
    exact isIso_of_reflects_iso _ N₂
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X)
    (NatTrans.app Γ₂N₁.natTrans X)
have rw : IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X)
  (Iso.inv (Iso.app Γ₂N₂ToKaroubiIso X) ≫
    NatTrans.app Γ₂N₂.natTrans (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
Tactic: rw [compatibility_Γ₂N₁_Γ₂N₂_natTrans]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.NCompGamma (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
⊢ IsIso (C := SimplicialObject.{v_1, u_1} C ⥤ Karoubi (SimplicialObject.{v_1, u_1} C)) (X :=
    Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) Γ₂N₁.natTrans
have this : ∀ (X : SimplicialObject.{v_1, u_1} C),
  IsIso (X := Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X)
    (NatTrans.app Γ₂N₁.natTrans X)
Tactic: have : ∀ X : SimplicialObject C, IsIso (Γ₂N₁.natTrans.app X) := by
    intro X
    rw [compatibility_Γ₂N₁_Γ₂N₂_natTrans]
    infer_instance
-- 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)
this : ∀ (n : ℕ), IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
⊢ IsIso f
have this₁ : ∀ (Δ : SimplexCategoryᵒᵖ), IsIso (f.app Δ)
Tactic: haveI : ∀ Δ : SimplexCategoryᵒᵖ, IsIso (f.app Δ) := fun Δ => this Δ.unop.len
-- 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)
⊢ IsIso f
have suffices : ∀ (n : ℕ), IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
Tactic: suffices ∀ n : ℕ, IsIso (f.app (op ⦋n⦌)) by
      haveI : ∀ Δ : SimplexCategoryᵒᵖ, IsIso (f.app Δ) := fun Δ => this Δ.unop.len
      apply NatIso.isIso_of_isIso_app
-- 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)
⊢ ∀ (n : ℕ), IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
have h₁ : ∀ (i : ℕ),
  Eq (α :=
    HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (CategoryTheory.Functor.map N₁ f ≫ inv (CategoryTheory.Functor.map N₁ f)))
      i)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ X))) i)
Tactic: have h₁ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.hom_inv_id (N₁.map f)))
-- 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₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f (CategoryTheory.Functor.map N₁ f ≫ inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ X))) i)
⊢ ∀ (n : ℕ), IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
have 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) ≫ CategoryTheory.Functor.map N₁ f))
      i)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ Y))) i)
Tactic: have h₂ := HomologicalComplex.congr_hom (Karoubi.hom_ext_iff.mp (IsIso.inv_hom_id (N₁.map f)))
-- 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₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f (CategoryTheory.Functor.map N₁ f ≫ inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ X))) i)
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) ≫ CategoryTheory.Functor.map N₁ f)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ Y))) i)
⊢ ∀ (n : ℕ), IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
have h₃ : ∀ (n : ℕ),
  Eq (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
    (HomologicalComplex.Hom.f (Karoubi.p (Functor.obj N₁ Y)) 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 (Karoubi.p (Functor.obj N₁ X)) n ≫ f.app (op ⦋n⦌))
Tactic: have h₃ := fun n =>
      Karoubi.HomologicalComplex.p_comm_f_assoc (inv (N₁.map f)) n (f.app (op ⦋n⦌))
-- 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₁ X)) i ⟶ HomologicalComplex.X (Karoubi.X (Functor.obj N₁ X)) i)
      (HomologicalComplex.Hom.f
        (Karoubi.Hom.f (CategoryTheory.Functor.map N₁ f ≫ inv (CategoryTheory.Functor.map N₁ f))) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ X))) i)
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) ≫ CategoryTheory.Functor.map N₁ f)) i)
      (HomologicalComplex.Hom.f (Karoubi.Hom.f (𝟙 (Functor.obj N₁ Y))) i)
h₃ :
  ∀ (n : ℕ),
    Eq (α := HomologicalComplex.X (Karoubi.X (Functor.obj N₁ Y)) n ⟶ Y _⦋n⦌)
      (HomologicalComplex.Hom.f (Karoubi.p (Functor.obj N₁ Y)) 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 (Karoubi.p (Functor.obj N₁ X)) n ≫ f.app (op ⦋n⦌))
⊢ ∀ (n : ℕ), IsIso (X := X _⦋n⦌) (f.app (op ⦋n⦌))
have 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)
Tactic: simp only [N₁_map_f, Karoubi.comp_f, HomologicalComplex.comp_f,
      AlternatingFaceMapComplex.map_f, N₁_obj_p, Karoubi.id_f, assoc] at h₁ h₂ h₃
Cleared hypotheses: 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)
⊢ IsIso (X := X _⦋0⦌) (f.app (op ⦋0⦌))
have h : 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⦌)
Tactic: use (inv (N₁.map f)).f.f 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)
⊢ 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₁ 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)
Tactic: have h₁₀ := h₁ 0