-- Module: Mathlib.RepresentationTheory.Homological.FiniteCyclic
Goal:
k G : Type u
inst : CommRing k
inst_1 : CommGroup G
inst_2 : Fintype G
g : G
hg : ∀ (x : G), Membership.mem (γ := Subgroup G) (Subgroup.zpowers g) x
x :
  (↑(ShortComplex.X₂
        (Functor.obj (HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0)
          (Functor.obj (ChainComplex.single₀ (Rep k G)) (trivial k G k)))) :
    Type u)
h :
  (Hom.hom
          (ShortComplex.Hom.τ₂
            (CategoryTheory.Functor.map (HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0)
              ((Equiv.symm
                    (ChainComplex.toSingle₀Equiv (Functor.obj (chainComplexFunctor k g) (leftRegular k G))
                      (trivial k G k)) :
                  (a :
                      { f : ((chainComplexFunctor k g).obj (leftRegular k G)).X 0 ⟶ trivial k G k //
                        ((chainComplexFunctor k g).obj (leftRegular k G)).d 1 0 ≫ f = 0 }) →
                    (chainComplexFunctor k g).obj (leftRegular k G) ⟶
                      (ChainComplex.single₀ (Rep k G)).obj (trivial k G k))
                (Subtype.mk (p :=
                    fun
                      (f :
                        Quiver.Hom (V := Rep k G)
                          (HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 0)
                          (trivial k G k)) ↦
                    Eq (α :=
                      Quiver.Hom (V := Rep k G)
                        (HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1)
                        (trivial k G k))
                      (HomologicalComplex.d (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1 0 ≫ f) 0)
                    (leftRegularHom (trivial k G k) 1) ⋯ :
                  { f :
                    Quiver.Hom (V := Rep k G)
                      (HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 0)
                      (trivial k G k) //
                    Eq (α :=
                      Quiver.Hom (V := Rep k G)
                        (HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1)
                        (trivial k G k))
                      (HomologicalComplex.d (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1 0 ≫ f) 0 })))) :
        (a :
            (↑((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
                    ((chainComplexFunctor k g).obj (leftRegular k G))).X₂ :
              Type u)) →
          (↑((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
                  ((ChainComplex.single₀ (Rep k G)).obj (trivial k G k))).X₂ :
            Type u))
      (single 1 x) =
    x
⊢ ∃ (a :
    (↑(ShortComplex.X₂
          (Functor.obj (HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0)
            (Functor.obj (chainComplexFunctor k g) (leftRegular k G)))) :
      Type u)),
    (Hom.hom
            (ShortComplex.Hom.τ₂
              (CategoryTheory.Functor.map
                (HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0)
                ((Equiv.symm
                      (ChainComplex.toSingle₀Equiv (Functor.obj (chainComplexFunctor k g) (leftRegular k G))
                        (trivial k G k)) :
                    (a :
                        { f : ((chainComplexFunctor k g).obj (leftRegular k G)).X 0 ⟶ trivial k G k //
                          ((chainComplexFunctor k g).obj (leftRegular k G)).d 1 0 ≫ f = 0 }) →
                      (chainComplexFunctor k g).obj (leftRegular k G) ⟶
                        (ChainComplex.single₀ (Rep k G)).obj (trivial k G k))
                  (Subtype.mk (p :=
                      fun
                        (f :
                          Quiver.Hom (V := Rep k G)
                            (HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 0)
                            (trivial k G k)) ↦
                      Eq (α :=
                        Quiver.Hom (V := Rep k G)
                          (HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1)
                          (trivial k G k))
                        (HomologicalComplex.d (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1 0 ≫ f) 0)
                      (leftRegularHom (trivial k G k) 1) ⋯ :
                    { f :
                      Quiver.Hom (V := Rep k G)
                        (HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 0)
                        (trivial k G k) //
                      Eq (α :=
                        Quiver.Hom (V := Rep k G)
                          (HomologicalComplex.X (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1)
                          (trivial k G k))
                        (HomologicalComplex.d (Functor.obj (chainComplexFunctor k g) (leftRegular k G)) 1 0 ≫ f)
                        0 })))) :
          (a :
              (↑((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
                      ((chainComplexFunctor k g).obj (leftRegular k G))).X₂ :
                Type u)) →
            (↑((HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0).obj
                    ((ChainComplex.single₀ (Rep k G)).obj (trivial k G k))).X₂ :
              Type u))
        a =
      x

Tactic:
use single 1 x

Premises used: OfNat.ofNat, Finsupp.single