-- 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)
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)
    ((((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) t⁻¹ : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
        ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u)) (CC := carrier)
                (X :=
                ObjectProperty.FullSubcategory.obj (P := isFG k)
                  (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
                (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep)) :
              (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
            (single (M := fun (a : G) ↦ k) u 1) :
          (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
                (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
            Type u))
        1 :
      k)
_₁ :
  Eq (α := k)
    ((evalAlgHom k (fun (a : G) ↦ k) s : (a : (i : G) → k) → k)
        ((((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) t⁻¹ : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k)
            (single (M := fun (a : G) ↦ k) u 1) :
          G → k) :
      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)
⊢ 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)

Tactic:
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: congrArg, CategoryTheory.ConcreteCategory.hom, CategoryTheory.LaxMonoidalFunctor.Hom.hom, id, Pi.single, TannakaDuality.FiniteGroup.leftRegular, Inv.inv, Pi.evalAlgHom, congrFun, CategoryTheory.InducedCategory.Hom.hom, OfNat.ofNat, Eq.symm, CategoryTheory.Iso.hom, DFunLike.coe, CategoryTheory.NatTrans.app, TannakaDuality.FiniteGroup.rightFDRep