awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
⊢ Eq (α := (↑(H2 A) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H2π A) :
            (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
          x :
        (↑(H2 A) : Type u))
      (0 : (↑(H2 A) : Type u)) ↔
    (↑x : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A
have h : Eq (α := (shortComplexH2 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousChains A) 2).homology)
  ((shortComplexH2 A).moduleCatLeftHomologyData.π ≫
    leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
      Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso)
  (cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
      (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
    (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData.π ≫
      Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso)
Tactic: have h := leftHomologyπ_naturality'_assoc (isoShortComplexH2 A).inv
    (shortComplexH2 A).moduleCatLeftHomologyData (leftHomologyData _)
    ((inhomogeneousChains A).sc 2).leftHomologyIso.hom
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x : ↥(cycles₂ A)
h :
  Eq (α := (shortComplexH2 A).moduleCatLeftHomologyData.K ⟶ (HomologicalComplex.sc (inhomogeneousChains A) 2).homology)
    ((shortComplexH2 A).moduleCatLeftHomologyData.π ≫
      leftHomologyMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
          (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso)
    (cyclesMap' (isoShortComplexH2 A).inv (shortComplexH2 A).moduleCatLeftHomologyData
        (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData ≫
      (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyData.π ≫
        Iso.hom (HomologicalComplex.sc (inhomogeneousChains A) 2).leftHomologyIso)
⊢ Eq (α := (↑(H2 A) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H2π A) :
            (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
          x :
        (↑(H2 A) : Type u))
      (0 : (↑(H2 A) : Type u)) ↔
    (↑x : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A
have simp : Eq (α := (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
    ((ModuleCat.Hom.hom (shortComplexH2 A).moduleCatLeftHomologyData.π :
          (a : ↥(cycles₂ A)) → (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
        x :
      (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u))
    (0 : (↑(shortComplexH2 A).moduleCatLeftHomologyData.H : Type u)) ↔
  (↑x : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A
Tactic: simp only [H2π, isoCycles₂, π, HomologicalComplex.homologyπ, homologyπ,
    cyclesMapIso'_inv, leftHomologyπ, ← h, ← leftHomologyMapIso'_inv, ModuleCat.hom_comp,
    LinearMap.coe_comp, Function.comp_apply, map_eq_zero_iff _
    ((ModuleCat.mono_iff_injective <| _).1 inferInstance)]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
A : Rep k G
x y : ↥(cycles₂ A)
⊢ Eq (α := (↑(H2 A) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H2π A) :
            (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
          x :
        (↑(H2 A) : Type u))
      ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC :=
              ModuleCat.carrier) (H2π A) :
            (a : (↑(ModuleCat.of k ↥(cycles₂ A)) : Type u)) → (↑(H2 A) : Type u))
          y :
        (↑(H2 A) : Type u)) ↔
    (↑x : G × G →₀ (↑A : Type u)) - (↑y : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A
have rw : (↑(x - y) : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A ↔
  (↑x : G × G →₀ (↑A : Type u)) - (↑y : G × G →₀ (↑A : Type u)) ∈ boundaries₂ A
Tactic: rw [← sub_eq_zero, ← map_sub, H2π_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
⊢ cechNerveTerminalFrom G ≅
    classifyingSpaceUniversalCover G ⋙
      forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
        fun (X : Action (Type u) G) ↦ X.V)
have refine : ∀ {X Y : SimplexCategoryᵒᵖ} (x : X ⟶ Y),
  Eq (α :=
    Functor.obj (cechNerveTerminalFrom G) X ⟶
      (classifyingSpaceUniversalCover G ⋙
            forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
              fun (X : Action (Type u) G) ↦ X.V)).obj
        Y)
    (CategoryTheory.Functor.map (cechNerveTerminalFrom G) x ≫
      Iso.hom
        ((fun (x : SimplexCategoryᵒᵖ) ↦
            (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
              Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                ((j : Fin ((Opposite.unop x).len + 1)) → G)))
          Y))
    (Iso.hom
        ((fun (x : SimplexCategoryᵒᵖ) ↦
            (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
              Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                ((j : Fin ((Opposite.unop x).len + 1)) → G)))
          X) ≫
      (classifyingSpaceUniversalCover G ⋙
            forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
              fun (X : Action (Type u) G) ↦ X.V)).map
        x)
Tactic: refine NatIso.ofComponents (fun _ => Types.productIso _) fun _ => ?_
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
X Y : SimplexCategoryᵒᵖ
x : X ⟶ Y
⊢ Eq (α :=
    Functor.obj (cechNerveTerminalFrom G) X ⟶
      (classifyingSpaceUniversalCover G ⋙
            forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
              fun (X : Action (Type u) G) ↦ X.V)).obj
        Y)
    (CategoryTheory.Functor.map (cechNerveTerminalFrom G) x ≫
      Iso.hom
        ((fun (x : SimplexCategoryᵒᵖ) ↦
            (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
              Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                ((j : Fin ((Opposite.unop x).len + 1)) → G)))
          Y))
    (Iso.hom
        ((fun (x : SimplexCategoryᵒᵖ) ↦
            (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
              Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                ((j : Fin ((Opposite.unop x).len + 1)) → G)))
          X) ≫
      (classifyingSpaceUniversalCover G ⋙
            forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
              fun (X : Action (Type u) G) ↦ X.V)).map
        x)
have h : Eq (α :=
  Functor.obj (cechNerveTerminalFrom G) X →
    (classifyingSpaceUniversalCover G ⋙
          forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
            fun (X : Action (Type u) G) ↦ X.V)).obj
      Y)
  (TypeCat.Fun.toFun
    (ConcreteCategory.hom (FC := TypeCat.Fun)
      (CategoryTheory.Functor.map (cechNerveTerminalFrom G) x ≫
        Iso.hom
          ((fun (x : SimplexCategoryᵒᵖ) ↦
              (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
                Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                  ((j : Fin ((Opposite.unop x).len + 1)) → G)))
            Y))))
  (TypeCat.Fun.toFun
    (ConcreteCategory.hom (FC := TypeCat.Fun)
      (Iso.hom
          ((fun (x : SimplexCategoryᵒᵖ) ↦
              (Types.productIso fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G :
                Iso (C := Type u) (∏ᶜ fun (x : Fin ((Opposite.unop x).len + 1)) ↦ G)
                  ((j : Fin ((Opposite.unop x).len + 1)) → G)))
            X) ≫
        (classifyingSpaceUniversalCover G ⋙
              forget (Action (Type u) G) (FC := Action.HomSubtype (Type u) G (FV := TypeCat.Fun)) (CC :=
                fun (X : Action (Type u) G) ↦ X.V)).map
          x)))
Tactic: ext : 2
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
⊢ (compForgetAugmented G).ExtraDegeneracy
have this : (Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve ≅ compForgetAugmented G
Tactic: refine
    ExtraDegeneracy.ofIso (?_ : (Arrow.mk <| terminal.from G).augmentedCechNerve ≅ _)
      (extraDegeneracyAugmentedCechNerve G)
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
⊢ CategoryTheory.Functor.map (𝟭 (SimplicialObject (Type u)))
        (Iso.hom (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G)) ≫
      (compForgetAugmented G).hom =
    (Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve.hom ≫
      CategoryTheory.Functor.map (SimplicialObject.const (Type u))
        (Iso.hom (Iso.refl (Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve.right))
have w : ∀ (n : SimplexCategoryᵒᵖ),
  NatTrans.app
      (CategoryTheory.Functor.map (𝟭 (SimplicialObject (Type u)))
          (Iso.hom (CechNerveTerminalFrom.iso G ≪≫ cechNerveTerminalFromIsoCompForget G)) ≫
        (compForgetAugmented G).hom)
      n =
    ((Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve.hom ≫
          CategoryTheory.Functor.map (SimplicialObject.const (Type u))
            (Iso.hom (Iso.refl (Arrow.mk (Y := ⊤_ Type u) (terminal.from G)).augmentedCechNerve.right))).app
      n
Tactic: ext : 1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
n : ℕ
c : Fin (n + 1) → G
r : k
⊢ Eq (α := (Fin n → G) →₀ k)
    ((d k G n : (a : (Fin (n + 1) → G) →₀ k) → (Fin n → G) →₀ k) (single c r) : (Fin n → G) →₀ k)
    (∑ p : Fin (n + 1), single (c ∘ p.succAbove) (r * HPow.hPow (α := k) (-1) (↑p : ℕ)) : (Fin n → G) →₀ k)
have rw : HSMul.hSMul (β := (Fin n → G) →₀ k) r (∑ p : Fin (n + 1), single (c ∘ p.succAbove) (HPow.hPow (α := k) (-1) (↑p : ℕ))) =
  ∑ p : Fin (n + 1), single (c ∘ p.succAbove) (HSMul.hSMul (β := k) r 1 * HPow.hPow (α := k) (-1) (↑p : ℕ))
Tactic: rw [← mul_one r, ← smul_eq_mul, ← smul_single, map_smul, d_of]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
n : ℕ
⊢ Eq (α :=
    (↑(HomologicalComplex.X (standardComplex k G) (n + 1)) : Type u) →ₗ[k]
      (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
    (Representation.IntertwiningMap.toLinearMap (Hom.hom (HomologicalComplex.d (standardComplex k G) (n + 1) n)))
    (d k G (n + 1))
have refine : ∀ (x : Fin (n + 2) → G),
  Eq (α := (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom (HomologicalComplex.d (standardComplex k G) (n + 1) n)) ∘ₗ
          lsingle x :
        (a : k) → (↑((standardComplex k G).X n) : Type u))
      1)
    ((d k G (n + 1) ∘ₗ lsingle x : (a : k) → (↑((standardComplex k G).X n) : Type u)) 1)
Tactic: refine Finsupp.lhom_ext' fun (x : Fin (n + 2) → G) => LinearMap.ext_ring ?_
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
n : ℕ
f : (Fin (n + 1 + 1) → G) →₀ k
⊢ Eq (α := (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
    ((Hom.hom (HomologicalComplex.d (standardComplex k G) (n + 1) n) :
          (a : (↑((standardComplex k G).X (n + 1)) : Type u)) → (↑((standardComplex k G).X n) : Type u))
        f :
      (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
    ((d k G (n + 1) : (a : (Fin (n + 1 + 1) → G) →₀ k) → (Fin (n + 1) → G) →₀ k) f : (Fin (n + 1) → G) →₀ k)
have rw : Eq (α := (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
  ((d k G (n + 1) : (a : (↑((standardComplex k G).X (n + 1)) : Type u)) → (↑((standardComplex k G).X n) : Type u)) f :
    (↑(HomologicalComplex.X (standardComplex k G) n) : Type u))
  ((d k G (n + 1) : (a : (Fin (n + 1 + 1) → G) →₀ k) → (Fin (n + 1) → G) →₀ k) f : (Fin (n + 1) → G) →₀ k)
Tactic: rw [← Representation.IntertwiningMap.toLinearMap_apply, d_eq]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
⊢ Eq (α := Quiver.Hom (V := Rep k G) (HomologicalComplex.X (standardComplex k G) 1) (trivial k G k))
    (HomologicalComplex.d (standardComplex k G) 1 0 ≫ ε k G) 0
have hf : ∀ (x : (↑(HomologicalComplex.X (standardComplex k G) 1) : Type u)),
  Eq (α := (↑(trivial k G k) : Type u))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom (HomologicalComplex.d (standardComplex k G) 1 0 ≫ ε k G)) :
          (a : (↑((standardComplex k G).X 1) : Type u)) → (↑(trivial k G k) : Type u))
        x :
      (↑(trivial k G k) : Type u))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom 0) :
          (a : (↑((standardComplex k G).X 1) : Type u)) → (↑(trivial k G k) : Type u))
        x :
      (↑(trivial k G k) : Type u))
Tactic: ext : 3
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
x : (↑(HomologicalComplex.X (standardComplex k G) 1) : Type u)
⊢ Eq (α :=
    HomologicalComplex.X (forget₂ToModuleCat k G) 1 ⟶
      Functor.obj
        (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
          fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
        (trivial k G k))
    (CategoryStruct.comp (Y := HomologicalComplex.X (forget₂ToModuleCat k G) 0)
      (HomologicalComplex.d (forget₂ToModuleCat k G) 1 0)
      (CategoryTheory.Functor.map
        (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
          fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
        (ε k G)))
    0
have rw : Eq (α :=
  HomologicalComplex.X (forget₂ToModuleCat k G) 1 ⟶
    Functor.obj
      (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
        fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
      (trivial k G k))
  (HomologicalComplex.Hom.f (HomotopyEquiv.hom (forget₂ToModuleCatHomotopyEquiv k G)) 1 ≫
      HomologicalComplex.d
        (Functor.obj (ChainComplex.single₀ (ModuleCat k))
          (Functor.obj
            (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
              fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
            (trivial k G k)))
        1 0 :
    HomologicalComplex.X (forget₂ToModuleCat k G) 1 ⟶
      HomologicalComplex.X
        (Functor.obj (ChainComplex.single₀ (ModuleCat k))
          (Functor.obj
            (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
              fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
            (trivial k G k)))
        0)
  0
Tactic: rw [← forget₂ToModuleCatHomotopyEquiv_f_0_eq,
      ← (forget₂ToModuleCatHomotopyEquiv k G).1.2 1 0 rfl]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
x : (↑(HomologicalComplex.X (standardComplex k G) 1) : Type u)
⊢ Eq (α := (↑(trivial k G k) : Type u))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom (HomologicalComplex.d (standardComplex k G) 1 0 ≫ ε k G)) :
          (a : (↑((standardComplex k G).X 1) : Type u)) → (↑(trivial k G k) : Type u))
        x :
      (↑(trivial k G k) : Type u))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom 0) :
          (a : (↑((standardComplex k G).X 1) : Type u)) → (↑(trivial k G k) : Type u))
        x :
      (↑(trivial k G k) : Type u))
have this : Eq (α :=
  HomologicalComplex.X (forget₂ToModuleCat k G) 1 ⟶
    Functor.obj
      (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
        fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
      (trivial k G k))
  (CategoryStruct.comp (Y := HomologicalComplex.X (forget₂ToModuleCat k G) 0)
    (HomologicalComplex.d (forget₂ToModuleCat k G) 1 0)
    (CategoryTheory.Functor.map
      (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
        fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
      (ε k G)))
  0
Tactic: have : (forget₂ToModuleCat k G).d 1 0
      ≫ (forget₂ (Rep k G) (ModuleCat.{u} k)).map (ε k G) = 0 := by
    rw [← forget₂ToModuleCatHomotopyEquiv_f_0_eq,
      ← (forget₂ToModuleCatHomotopyEquiv k G).1.2 1 0 rfl]
    exact comp_zero
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
⊢ CategoryTheory.Functor.map
        (Functor.mapHomologicalComplex
          (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
            fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
          (ComplexShape.down ℕ))
        (εToSingle₀ k G) ≫
      NatTrans.app
        (Iso.hom
          (HomologicalComplex.singleMapHomologicalComplex
            (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
              fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
            (ComplexShape.down ℕ) 0))
        (trivial k G k) =
    HomotopyEquiv.hom (forget₂ToModuleCatHomotopyEquiv k G)
have dsimp : CategoryTheory.Functor.map
      (Functor.mapHomologicalComplex
        (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
          fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
        (ComplexShape.down ℕ))
      (εToSingle₀ k G) ≫
    NatTrans.app
      (Iso.hom
        (HomologicalComplex.singleMapHomologicalComplex
          (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
            fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
          (ComplexShape.down ℕ) 0))
      (trivial k G k) =
  HomotopyEquiv.hom (forget₂ToModuleCatHomotopyEquiv k G)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (goal)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
⊢ CategoryTheory.Functor.map
        (Functor.mapHomologicalComplex
          (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
            fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
          (ComplexShape.down ℕ))
        (εToSingle₀ k G) ≫
      NatTrans.app
        (Iso.hom
          (HomologicalComplex.singleMapHomologicalComplex
            (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
              fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
            (ComplexShape.down ℕ) 0))
        (trivial k G k) =
    HomotopyEquiv.hom (forget₂ToModuleCatHomotopyEquiv k G)
have hfg : Eq (α :=
  HomologicalComplex.X
      (Functor.obj
        (Functor.mapHomologicalComplex
          (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
            fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
          (ComplexShape.down ℕ))
        (standardComplex k G))
      0 ⟶
    HomologicalComplex.X
      (Functor.obj (HomologicalComplex.single (ModuleCat k) (ComplexShape.down ℕ) 0) (ModuleCat.of k k)) 0)
  (HomologicalComplex.Hom.f
    (CategoryTheory.Functor.map
        (Functor.mapHomologicalComplex
          (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
            fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
          (ComplexShape.down ℕ))
        (εToSingle₀ k G) ≫
      NatTrans.app
        (Iso.hom
          (HomologicalComplex.singleMapHomologicalComplex
            (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
              fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
            (ComplexShape.down ℕ) 0))
        (trivial k G k))
    0)
  (HomologicalComplex.Hom.f (HomotopyEquiv.hom (forget₂ToModuleCatHomotopyEquiv k G)) 0)
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.Resolution (hypothesis)
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
⊢ QuasiIso (K :=
    Functor.obj
      (Functor.mapHomologicalComplex
        (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
          fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
        (ComplexShape.down ℕ))
      (standardComplex k G))
    (CategoryTheory.Functor.map
      (Functor.mapHomologicalComplex
        (forget₂ (Rep k G) (FC := fun (A B : Rep k G) ↦ A.ρ.IntertwiningMap B.ρ) (CC := V) (ModuleCat k) (FD :=
          fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CD := ModuleCat.carrier))
        (ComplexShape.down ℕ))
      (εToSingle₀ k G))
have h : QuasiIso (C := ModuleCat k) (K := forget₂ToModuleCat k G) (HomotopyEquiv.hom (forget₂ToModuleCatHomotopyEquiv k G))
Tactic: have h : QuasiIso (forget₂ToModuleCatHomotopyEquiv k G).hom := inferInstance