-- 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
η : 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)
⊢ Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)
have 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)
Tactic: rwa [← one_mul (α_inv 1), map_mul_toRightFDRepComp, h, mul_one] at this
Cleared hypotheses: this, h