-- Lean 4 proof step from Mathlib.RepresentationTheory.Homological.FiniteCyclic (goal)
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
zero :
  ShortComplex.Exact (C := Rep k G)
    (ShortComplex.mk (X₁ :=
      ShortComplex.X₁
        (Functor.obj (HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0)
          (Functor.obj (chainComplexFunctor k g) (leftRegular k G))))
      (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))))
      (ShortComplex.f
        (Functor.obj (HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0)
          (Functor.obj (chainComplexFunctor k g) (leftRegular k G))))
      (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 }))))
      ⋯)
⊢ ShortComplex.Exact (C := Rep k G)
      (ShortComplex.mk (X₁ :=
        ShortComplex.X₁
          (Functor.obj (HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0)
            (Functor.obj (chainComplexFunctor k g) (leftRegular k G))))
        (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))))
        (ShortComplex.f
          (Functor.obj (HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0)
            (Functor.obj (chainComplexFunctor k g) (leftRegular k G))))
        (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 }))))
        ⋯) ∧
    Epi.{u, u + 1} (C := Rep k G) (X :=
      ShortComplex.X₂
        (Functor.obj (HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0)
          (Functor.obj (chainComplexFunctor k g) (leftRegular k G))))
      (Y :=
      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))))
      (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 }))))
have zero₁ : Epi.{u, u + 1} (C := Rep k G) (X :=
  ShortComplex.X₂
    (Functor.obj (HomologicalComplex.shortComplexFunctor' (Rep k G) (ComplexShape.down ℕ) 1 0 0)
      (Functor.obj (chainComplexFunctor k g) (leftRegular k G))))
  (Y :=
  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))))
  (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) sorry :
          { 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 }))))
Tactic: constructor