-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
α : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep))
α_inv : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.inv.hom.app rightFDRep))
this h : Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)
rwa :
  ∀
    (this :
      Eq (α := G → k)
        ((α : (a : G → k) → G → k)
            (HMul.hMul (α := G → k) (β := G → k) (1 : G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k)) :
          G → k)
        (1 : G → k))
    (h : Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)),
    Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)
rwa₁ :
  ∀
    (this :
      HMul.hMul (α := G → k) (β := G → k)
          (((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) → G → k)
              1 :
            G → k)
          (((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) → G → k)
              ((α_inv : (a : G → k) → G → k) 1 : G → k) :
            G → k) =
        1)
    (h : Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)),
    Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)
rwa₂ :
  ∀
    (this :
      HMul.hMul (α := G → k) (β := G → k)
          (((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) → G → k)
              1 :
            G → k)
          (1 : G → k) =
        1)
    (h : Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)),
    Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)
rwa₃ rwa₄ rwa₅ rwa₆ :
  ∀
    (this :
      Eq (α := G → k)
        (((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) → G → k)
            1 :
          G → k)
        (1 : G → k))
    (h : Eq (α := G → k) ((α : (a : G → k) → G → k) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)),
    Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)
⊢ Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)

Tactic:
rwa [← one_mul (α_inv 1), map_mul_toRightFDRepComp, h, mul_one] at this

Premises used: mul_one, OfNat.ofNat, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp, DFunLike.coe, one_mul