awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
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))
    (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:
comp_zero

Premises used: CategoryTheory.Limits.comp_zero, ite
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
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))
    (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:
exact comp_zero

Premises used: CategoryTheory.Limits.comp_zero
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
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

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
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
x : (↑(HomologicalComplex.X (standardComplex k G) 1) : Type u)
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
⊢ 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:
LinearMap.ext_iff.1 (ModuleCat.hom_ext_iff.mp this) _

Premises used: LinearMap.ext_iff, ModuleCat.hom_ext_iff, Iff.mp
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
x : (↑(HomologicalComplex.X (standardComplex k G) 1) : Type u)
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
⊢ 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:
exact LinearMap.ext_iff.1 (ModuleCat.hom_ext_iff.mp this) _

Premises used: LinearMap.ext_iff, ModuleCat.hom_ext_iff, Iff.mp
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
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)
⊢ 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
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
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)
⊢ 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:
ext1
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
⊢ 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:
simpa using (forget₂ToModuleCatHomotopyEquiv_f_0_eq k G).symm

Premises used: Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, Eq.symm
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
⊢ 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
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
h : QuasiIso (C := ModuleCat k) (K := forget₂ToModuleCat k G) (HomotopyEquiv.hom (forget₂ToModuleCatHomotopyEquiv k G))
⊢ QuasiIso (K := forget₂ToModuleCat k G) (L :=
    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)))
    (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))

Tactic:
rw [← εToSingle₀_comp_eq k G] at h

Premises used: Rep.standardComplex.εToSingle₀_comp_eq
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
h :
  QuasiIso (K := forget₂ToModuleCat k G) (L :=
    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)))
    (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))
⊢ 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))

Tactic:
quasiIso_of_comp_right (hφφ' := h)

Premises used: quasiIso_of_comp_right
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Monoid G
h :
  QuasiIso (K := forget₂ToModuleCat k G) (L :=
    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)))
    (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))
⊢ 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))

Tactic:
exact quasiIso_of_comp_right (hφφ' := h)

Premises used: quasiIso_of_comp_right
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Monoid G
rw :
  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))
⊢ QuasiIso (C := Rep k G) (εToSingle₀ k G)

Tactic:
rw [← HomologicalComplex.quasiIso_map_iff_of_preservesHomology _ (forget₂ _ (ModuleCat.{u} k))]
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
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))

Tactic:
apply quasiIso_forget₂_εToSingle₀

Premises used: Rep.standardComplex.quasiIso_forget₂_εToSingle₀
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
x : Fin (n + 1) → G
⊢ (Hom.hom (d k G n) : (a : (↑(free k G (Fin (n + 1) → G)) : Type u)) → (↑(free k G (Fin n → G)) : Type u))
      (single x (single 1 1)) =
    HAdd.hAdd (α := ((i : Fin n) → G) →₀ G →₀ k) (single (fun (i : Fin n) ↦ x i.succ) (single (x 0) 1))
      (∑ j : Fin (n + 1),
        single (j.contractNth (fun (x1 x2 : G) ↦ x1 * x2) x) (single 1 (HPow.hPow (α := k) (-1) ((↑j : ℕ) + 1))))

Tactic:
simp [d, ← Representation.IntertwiningMap.toLinearMap_apply]

Premises used: Representation.IntertwiningMap.toLinearMap_apply, Rep.barComplex.d
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
m : ℕ
g : G
r s : k
f : Fin m → G
⊢ Eq (α := MonoidalCategoryStruct.tensorObj (𝒞 := types) (Action.V (Action.leftRegular G)) (Fin m → G) →₀ k)
    ((Representation.LinearizeMonoidal.μ (Action.leftRegular G) (Action.trivial G (Fin m → G)) :
          (a : TensorProduct k ((Action.leftRegular G).V →₀ k) ((Fin m → G) →₀ k)) →
            (Action.leftRegular G).V ⊗ (Fin m → G) →₀ k)
        (single g r ⊗ₜ[k] single f s) :
      MonoidalCategoryStruct.tensorObj (𝒞 := types) (Action.V (Action.leftRegular G)) (Fin m → G) →₀ k)
    (single (g, f) (r * s) : G × (Fin m → G) →₀ k)

Tactic:
Representation.LinearizeMonoidal.μ_apply_single_single
    (X := Action.leftRegular G) (Y := Action.trivial G (Fin m → G)) g f r s

Premises used: Representation.LinearizeMonoidal.μ_apply_single_single
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
m : ℕ
g : G
f : Fin m → G
r : k
⊢ Eq (α := Action.V (Action.diagonal G (m + 1)) →₀ k)
    ((Representation.linearizeMap (Iso.inv (Action.diagonalSuccIsoTensorTrivial G m)) :
          (a : (Action.leftRegular G).V ⊗ (Fin m → G) →₀ k) → (Action.diagonal G (m + 1)).V →₀ k)
        (single (g, f) r) :
      Action.V (Action.diagonal G (m + 1)) →₀ k)
    (single
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (Action.Hom.hom (Iso.inv (Action.diagonalSuccIsoTensorTrivial G m))) :
            (a : (fun (X : Type u) ↦ X) (Action.leftRegular G ⊗ Action.trivial G (Fin m → G)).V) →
              (fun (X : Type u) ↦ X) (Action.diagonal G (m + 1)).V)
          (g, f))
        r :
      (fun (X : Type u) ↦ X) (Action.V (Action.diagonal G (m + 1))) →₀ k)

Tactic:
Representation.linearizeMap_single (Action.diagonalSuccIsoTensorTrivial G m).inv (g, f) r

Premises used: Action.diagonalSuccIsoTensorTrivial, Prod.mk, Representation.linearizeMap_single, CategoryTheory.Iso.inv
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
i : Fin (n + 1) → G
e_a :
  HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ) =
    Fin.partialProd i ∘ Fin.succ
⊢ Eq (α := ((i : Fin (n + 1)) → G) →₀ k)
    (single (HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ)) 1)
    (single (Fin.partialProd i ∘ Fin.succ) 1)

Tactic:
congr
-- Module: Mathlib.RepresentationTheory.Homological.Resolution
Goal:
k G : Type u
inst : CommRing k
n : ℕ
inst_1 : Group G
i : Fin (n + 1) → G
⊢ HSMul.hSMul (β := (i : Fin (n + 1)) → G) (i 0) (Fin.partialProd fun (i_1 : Fin n) ↦ i i_1.succ) =
    Fin.partialProd i ∘ Fin.succ

Tactic:
funext fun j ↦ Fin.partialProd_succ' i j |>.symm

Premises used: funext, Fin.partialProd_succ', Eq.symm