awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (hypothesis)
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
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf :
  Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
    (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
⊢ DegeneraciesVanish f
have this : HAdd.hAdd (α :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) ≫
    f =
  𝟙 (HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1)) ≫ f
Tactic: have := PInfty_f_add_QInfty_f (n + 1) =≫ f
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (hypothesis)
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
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf :
  Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
    (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
this :
  HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) ≫
      f =
    𝟙 (HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1)) ≫ f
⊢ DegeneraciesVanish f
have this₁ : HAdd.hAdd (α :=
      HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
      (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) ≫
    f =
  f
Tactic: rw [Category.id_comp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Degeneracies (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
T : C
n : ℕ
f : X _⦋n + 1⦌ ⟶ T
hf :
  Eq (α := HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶ T)
    (HomologicalComplex.Hom.f QInfty (n + 1) ≫ f) 0
this :
  HAdd.hAdd (α :=
        HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
        (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) ≫
      f =
    f
⊢ DegeneraciesVanish f
have succ : ∀ (i : Fin (n + 1)),
  X.σ i ≫
      HAdd.hAdd (α :=
          HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1) ⟶
            HomologicalComplex.X (AlternatingFaceMapComplex.obj X) (n + 1))
          (HomologicalComplex.Hom.f PInfty (n + 1)) (HomologicalComplex.Hom.f QInfty (n + 1)) ≫
        f =
    0
Tactic: rw [degeneraciesVanish_succ_iff, ← this]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive (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)
α : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj N (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))
  (Functor.obj N (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)) :=
  Functor.mapIso N (Iso.app Γ₂N₂ P)
β : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N P))
  (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N P)) :=
  Iso.app N₂Γ₂ (Functor.obj N P)
⊢ 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)))
      (Functor.map N (NatTrans.app (Iso.hom Γ₂N₂) P)) (NatTrans.app (Iso.hom N₂Γ₂) (Functor.obj N P)))
    (𝟙 (Functor.obj N P))
have symm : Eq (α := Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Functor.obj N P) (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)))
    (Functor.map N (NatTrans.app (Iso.hom Γ₂N₂) P)) (NatTrans.app (Iso.hom N₂Γ₂) (Functor.obj N P)))
Tactic: symm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive (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)
α : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj N (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))
  (Functor.obj N (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)) :=
  Functor.mapIso N (Iso.app Γ₂N₂ P)
β : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N P))
  (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N P)) :=
  Iso.app N₂Γ₂ (Functor.obj N P)
⊢ Eq (α := Quiver.Hom (V := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Functor.obj N P) (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)))
      (Functor.map N (NatTrans.app (Iso.hom Γ₂N₂) P)) (NatTrans.app (Iso.hom N₂Γ₂) (Functor.obj N P)))
have change : 𝟙 (Functor.obj N (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)) = α.hom ≫ β.hom
Tactic: change 𝟙 _ = α.hom ≫ β.hom
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive (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)
α : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj N (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P))
  (Functor.obj N (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂) P)) :=
  Functor.mapIso N (Iso.app Γ₂N₂ P)
β : Iso (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
  (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) (Γ₂ ⋙ N₂) (Functor.obj N P))
  (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N P)) :=
  Iso.app N₂Γ₂ (Functor.obj N P)
⊢ 𝟙 (Functor.obj N (Functor.obj (𝟭 (Karoubi (SimplicialObject.{v_1, u_1} C))) P)) = α.hom ≫ β.hom
have rw : β.inv ≫ α.inv = 𝟙 (Functor.obj (𝟭 (Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))) (Functor.obj N P))
Tactic: rw [← Iso.inv_comp_eq, comp_id, ← comp_id β.hom, ← Iso.inv_comp_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
X : ChainComplex.{v_1, u_1, 0} C ℕ
⊢ Eq (α :=
    Quiver.Hom (V := ChainComplex.{v_1, u_1, 0} C ℕ)
      (Karoubi.X
        (Functor.obj N₂
          (Functor.obj
            (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
              Equivalence.inverse Preadditive.DoldKan.equivalence)
            X)))
      (Karoubi.X
        (Functor.obj N₂
          (Functor.obj (Γ ⋙ Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C))) X))))
    (Karoubi.Hom.f (Functor.map N₂ (NatTrans.app (Iso.hom isoΓ₀) X))) PInfty
have h : ∀ (i : ℕ),
  Eq (α :=
    HomologicalComplex.X
        (Karoubi.X
          (Functor.obj N₂
            (Functor.obj
              (Equivalence.functor (toKaroubiEquivalence (ChainComplex.{v_1, u_1, 0} C ℕ)) ⋙
                Equivalence.inverse Preadditive.DoldKan.equivalence)
              X)))
        i ⟶
      HomologicalComplex.X
        (Karoubi.X
          (Functor.obj N₂
            (Functor.obj (Γ ⋙ Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C))) X)))
        i)
    (HomologicalComplex.Hom.f (Karoubi.Hom.f (Functor.map N₂ (NatTrans.app (Iso.hom isoΓ₀) X))) i)
    (HomologicalComplex.Hom.f PInfty i)
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
⊢ Eq (α :=
    Iso (C := SimplicialObject.{v_1, u_1} C ⥤ Karoubi (SimplicialObject.{v_1, u_1} C))
      (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C)))
      (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
        (Equivalence.inverse Preadditive.DoldKan.equivalence)))
    (Compatibility.υ toKaroubiCompN₂IsoN₁) Γ₂N₁
have w : Eq (α :=
  Quiver.Hom (V := SimplicialObject.{v_1, u_1} C ⥤ Karoubi (SimplicialObject.{v_1, u_1} C))
    (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C)))
    (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
      (Equivalence.inverse Preadditive.DoldKan.equivalence)))
  (Iso.hom (Compatibility.υ toKaroubiCompN₂IsoN₁)) (Iso.hom Γ₂N₁)
Tactic: ext1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
⊢ Eq (α :=
    Quiver.Hom (V := SimplicialObject.{v_1, u_1} C ⥤ Karoubi (SimplicialObject.{v_1, u_1} C))
      (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C)))
      (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
        (Equivalence.inverse Preadditive.DoldKan.equivalence)))
    (Iso.hom (Compatibility.υ toKaroubiCompN₂IsoN₁)) (Iso.hom Γ₂N₁)
have w : Eq (α :=
  Quiver.Hom (V := SimplicialObject.{v_1, u_1} C ⥤ Karoubi (SimplicialObject.{v_1, u_1} C))
    (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂)
    (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
      (Equivalence.inverse Preadditive.DoldKan.equivalence)))
  (Iso.inv Γ₂N₁ ≫ Iso.hom (Compatibility.υ toKaroubiCompN₂IsoN₁))
  (𝟙 (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂))
Tactic: rw [← cancel_epi Γ₂N₁.inv, Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
⊢ Eq (α :=
    Quiver.Hom (V := SimplicialObject.{v_1, u_1} C ⥤ Karoubi (SimplicialObject.{v_1, u_1} C))
      (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂)
      (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
        (Equivalence.inverse Preadditive.DoldKan.equivalence)))
    (Iso.inv Γ₂N₁ ≫ Iso.hom (Compatibility.υ toKaroubiCompN₂IsoN₁))
    (𝟙 (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂))
have w : ∀ (X : SimplicialObject.{v_1, u_1} C),
  Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      Functor.obj
        (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
          (Equivalence.inverse Preadditive.DoldKan.equivalence))
        X)
    (NatTrans.app (Iso.inv Γ₂N₁ ≫ Iso.hom (Compatibility.υ toKaroubiCompN₂IsoN₁)) X)
    (NatTrans.app (𝟙 (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂)) X)
Tactic: ext X : 2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ Eq (α :=
    Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
      Functor.obj
        (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
          (Equivalence.inverse Preadditive.DoldKan.equivalence))
        X)
    (NatTrans.app (Iso.inv Γ₂N₁ ≫ Iso.hom (Compatibility.υ toKaroubiCompN₂IsoN₁)) X)
    (NatTrans.app (𝟙 (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂)) X)
have w : Eq (α :=
  Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂) X ⟶
    Functor.obj
      (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁
        (Equivalence.inverse Preadditive.DoldKan.equivalence))
      X)
  (NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
    NatTrans.app Γ₂N₂.natTrans (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) ≫
      CategoryStruct.comp (Y :=
        Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
          (Equivalence.inverse Preadditive.DoldKan.equivalence)
          (Functor.obj (Equivalence.functor Preadditive.DoldKan.equivalence)
            (Functor.obj (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C))) X)))
        (NatTrans.app (Iso.hom Γ₂N₂)
          (Functor.obj (Equivalence.functor (toKaroubiEquivalence (SimplicialObject.{v_1, u_1} C))) X))
        (Functor.map (Equivalence.inverse Preadditive.DoldKan.equivalence)
          (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)))
  (NatTrans.app (𝟙 (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₁ Γ₂)) X)
Tactic: rw [NatTrans.comp_app, Γ₂N₁_inv, compatibility_Γ₂N₁_Γ₂N₂_natTrans X, Compatibility.υ_hom_app,
    Preadditive.DoldKan.equivalence_unitIso, Iso.app_inv, assoc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
⊢ NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      NatTrans.app Γ₂N₂.natTrans (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) ≫
        CategoryStruct.comp (Y :=
          Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
            (Functor.obj (Equivalence.functor Preadditive.DoldKan.equivalence)
              (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)))
          (NatTrans.app (Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
          (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
have w : NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
    CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
          (Equivalence.functor Preadditive.DoldKan.equivalence) Γ₂)
        (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
      (NatTrans.app (Γ₂N₂.natTrans ≫ Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
      (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
  𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
Tactic: rw [← NatTrans.comp_app_assoc, ← Γ₂N₂_inv, Iso.inv_hom_id, NatTrans.id_app, id_comp,
    Γ₂N₂ToKaroubiIso_inv_app, ← Γ₂.map_comp, Iso.inv_hom_id_app, Γ₂.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
w :
  NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
            (Equivalence.functor Preadditive.DoldKan.equivalence) Γ₂)
          (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (NatTrans.app (Γ₂N₂.natTrans ≫ Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
⊢ NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      NatTrans.app Γ₂N₂.natTrans (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) ≫
        CategoryStruct.comp (Y :=
          Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
            (Functor.obj (Equivalence.functor Preadditive.DoldKan.equivalence)
              (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)))
          (NatTrans.app (Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
          (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
have w₁ : NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
    CategoryStruct.comp (Y :=
      Functor.obj
        (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
          (Equivalence.functor Preadditive.DoldKan.equivalence) Γ₂)
        (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
      (NatTrans.app (Iso.inv Γ₂N₂ ≫ Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
      (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
  𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
Tactic: rw [← NatTrans.comp_app_assoc, ← Γ₂N₂_inv, Iso.inv_hom_id, NatTrans.id_app, id_comp,
    Γ₂N₂ToKaroubiIso_inv_app, ← Γ₂.map_comp, Iso.inv_hom_id_app, Γ₂.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
w :
  NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
            (Equivalence.functor Preadditive.DoldKan.equivalence) Γ₂)
          (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (NatTrans.app (Γ₂N₂.natTrans ≫ Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
w₁ :
  NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
            (Equivalence.functor Preadditive.DoldKan.equivalence) Γ₂)
          (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (NatTrans.app (Iso.inv Γ₂N₂ ≫ Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
⊢ NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      NatTrans.app Γ₂N₂.natTrans (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) ≫
        CategoryStruct.comp (Y :=
          Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
            (Functor.obj (Equivalence.functor Preadditive.DoldKan.equivalence)
              (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)))
          (NatTrans.app (Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
          (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
have w₂ : NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
    NatTrans.app (𝟙 (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂))
        (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) ≫
      Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X) =
  𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
Tactic: rw [← NatTrans.comp_app_assoc, ← Γ₂N₂_inv, Iso.inv_hom_id, NatTrans.id_app, id_comp,
    Γ₂N₂ToKaroubiIso_inv_app, ← Γ₂.map_comp, Iso.inv_hom_id_app, Γ₂.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian (goal)
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : IsIdempotentComplete.{v_1, u_1} C
inst_3 : HasFiniteCoproducts.{v_1, u_1} C
X : SimplicialObject.{v_1, u_1} C
w :
  NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
            (Equivalence.functor Preadditive.DoldKan.equivalence) Γ₂)
          (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (NatTrans.app (Γ₂N₂.natTrans ≫ Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
w₁ :
  NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      CategoryStruct.comp (Y :=
        Functor.obj
          (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ))
            (Equivalence.functor Preadditive.DoldKan.equivalence) Γ₂)
          (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (NatTrans.app (Iso.inv Γ₂N₂ ≫ Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
        (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
w₂ :
  NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      NatTrans.app (𝟙 (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂))
          (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) ≫
        Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
⊢ NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
      NatTrans.app Γ₂N₂.natTrans (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X) ≫
        CategoryStruct.comp (Y :=
          Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂
            (Functor.obj (Equivalence.functor Preadditive.DoldKan.equivalence)
              (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)))
          (NatTrans.app (Iso.hom Γ₂N₂) (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X))
          (Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X)) =
    𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
have w₃ : NatTrans.app (Iso.inv Γ₂N₂ToKaroubiIso) X ≫
    𝟙
        (Functor.obj (Functor.comp (D := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) N₂ Γ₂)
          (Functor.obj (toKaroubi (SimplicialObject.{v_1, u_1} C)) X)) ≫
      Functor.map Γ₂ (NatTrans.app (Iso.hom toKaroubiCompN₂IsoN₁) X) =
  𝟙 (Functor.obj (C := Karoubi (ChainComplex.{v_1, u_1, 0} C ℕ)) Γ₂ (Functor.obj N₁ X))
Tactic: rw [← NatTrans.comp_app_assoc, ← Γ₂N₂_inv, Iso.inv_hom_id, NatTrans.id_app, id_comp,
    Γ₂N₂ToKaroubiIso_inv_app, ← Γ₂.map_comp, Iso.inv_hom_id_app, Γ₂.map_id]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.DoldKan.Faces (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
Y : C
n q : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
j : Fin (n + 2)
hj₁ : j ≠ 0
hj₂ : n + 2 ≤ (↑j : ℕ) + q
⊢ φ ≫ X.δ j = 0
have obtain : ∀ (i : Fin (n + 1)) (hj₁ : i.succ ≠ 0) (hj₂ : n + 2 ≤ (↑i.succ : ℕ) + q), φ ≫ X.δ i.succ = 0
Tactic: obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero hj₁
Cleared hypotheses: j, hj₁, hj₂