-- Lean 4 proof step from Mathlib.RepresentationTheory.Tannaka (goal)
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))
⊢ ∃ (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)
have 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)
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]