-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
inst_3 : IsDomain k
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
obtain :
  ∀ (s : G)
    (hs : AlgHom.comp (evalAlgHom k (fun (a : G) ↦ k) 1) (algHomOfRightFDRepComp η) = evalAlgHom k (fun (i : G) ↦ k) s),
    ∃ (s : G),
      Eq (α :=
        (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
                (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
            Type u) →ₗ[k]
          (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
                (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
            Type u))
        (Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep)))
        ((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s)
obtain₁ :
  ∀ (s : G)
    (hs : AlgHom.comp (evalAlgHom k (fun (a : G) ↦ k) 1) (algHomOfRightFDRepComp η) = evalAlgHom k (fun (i : G) ↦ k) s)
    (u : G),
    Eq (α :=
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
        Type u))
      (((Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep)) :
              (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
                      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
                  Type u) →ₗ[k]
                (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
                      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
                  Type u)) :
            (a : G → k) → (↑((forget k G).obj rightFDRep).obj : Type u))
          ((basisFun k G : (a : G) → G → k) u : G → k) :
        (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
          Type u))
      ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) :
            (a : G → k) → (↑((forget k G).obj rightFDRep).obj : Type u))
          ((basisFun k G : (a : G) → G → k) u : G → k) :
        (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
          Type u))
obtain₂ :
  ∀ (s : G)
    (hs : AlgHom.comp (evalAlgHom k (fun (a : G) ↦ k) 1) (algHomOfRightFDRepComp η) = evalAlgHom k (fun (i : G) ↦ k) s)
    (u : G),
    Eq (α := G → k)
      (((Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app (FDRep.of (V := G → k) rightRegular))) :
              (↑(of k (G → k)) : Type u) →ₗ[k] (↑(of k (G → k)) : Type u)) :
            (a : G → k) → G → k)
          ((basisFun k G : (a : G) → G → k) u : G → k) :
        G → k)
      ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
          ((basisFun k G : (a : G) → G → k) u : G → k) :
        G → k)
h :
  ∀ (s : G)
    (hs : AlgHom.comp (evalAlgHom k (fun (a : G) ↦ k) 1) (algHomOfRightFDRepComp η) = evalAlgHom k (fun (i : G) ↦ k) s)
    (u t : G),
    Eq (α := k)
      (((Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app (FDRep.of (V := G → k) rightRegular))) :
              (↑(of k (G → k)) : Type u) →ₗ[k] (↑(of k (G → k)) : Type u)) :
            (a : G → k) → G → k)
          ((basisFun k G : (a : G) → G → k) u : G → k) t :
        k)
      ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
          ((basisFun k G : (a : G) → G → k) u : G → k) t :
        k)
h₁ :
  ∀ (s : G)
    (hs : AlgHom.comp (evalAlgHom k (fun (a : G) ↦ k) 1) (algHomOfRightFDRepComp η) = evalAlgHom k (fun (i : G) ↦ k) s)
    (u t : G)
    (nat :
      Eq (α :=
        Quiver.Hom (V := FGModuleCat k)
          (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)
          (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
        (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (leftRegularFDRepHom t⁻¹) ≫
          η.hom.hom.app rightFDRep)
        (η.hom.hom.app rightFDRep ≫
          CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) (leftRegularFDRepHom t⁻¹))),
    Eq (α := k)
      (((Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app (FDRep.of (V := G → k) rightRegular))) :
              (↑(of k (G → k)) : Type u) →ₗ[k] (↑(of k (G → k)) : Type u)) :
            (a : G → k) → G → k)
          ((basisFun k G : (a : G) → G → k) u : G → k) t :
        k)
      ((((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
          ((basisFun k G : (a : G) → G → k) u : G → k) t :
        k)
⊢ ∃ (s : G),
    Eq (α :=
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
          Type u) →ₗ[k]
        (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
          Type u))
      (Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep))) ((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s)

Tactic:
classical
  obtain ⟨s, hs⟩ := ((evalAlgHom _ _ 1).comp (algHomOfRightFDRepComp η)).eq_piEvalAlgHom
  refine ⟨s, (basisFun k G).ext fun u ↦ ?_⟩
  simp only [rightFDRep, forget_obj]
  ext t
  have nat := η.hom.hom.naturality (leftRegularFDRepHom t⁻¹)
  calc
    _ = leftRegular t⁻¹ ((η.hom.hom.app rightFDRep).hom (single u 1)) 1 := by simp
    _ = (η.hom.hom.app rightFDRep).hom (leftRegular t⁻¹ (single u 1)) 1 :=
      congrFun congr(($nat.symm).hom (single u 1)) 1
    _ = evalAlgHom _ _ s (leftRegular t⁻¹ (single u 1)) :=
      congr($hs (leftRegular t⁻¹ (single u 1)))
    _ = _ := by by_cases u = t * s <;> simp_all [single_apply]

Premises used: TannakaDuality.FiniteGroup.forget_obj, Pi.evalAlgHom, TannakaDuality.FiniteGroup.algHomOfRightFDRepComp, AlgHom.comp, OfNat.ofNat, AlgHom.eq_piEvalAlgHom, TannakaDuality.FiniteGroup.rightFDRep