awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
inst_3 : Nontrivial k
s t : G
h :
  Eq (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
    ((equivHom k G : (a : G) → Aut (forget k G)) s :
      Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
    ((equivHom k G : (a : G) → Aut (forget k G)) t :
      Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
⊢ Eq (α := k)
    ((@ConcreteCategory.hom _ (moduleCategory k) (fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u))
            carrier _ _
            (ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
            (ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
            (InducedCategory.Hom.hom
              (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom ((equivHom k G : (a : G) → Aut (forget k G)) s)))
                rightFDRep)) :
          (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
        (single (M := fun (a : G) ↦ k) t 1) 1 :
      k)
    ((@ConcreteCategory.hom _ (moduleCategory k) (fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u))
            carrier _ _
            (ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
            (ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
            (InducedCategory.Hom.hom
              (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom ((equivHom k G : (a : G) → Aut (forget k G)) t)))
                rightFDRep)) :
          (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
        (single (M := fun (a : G) ↦ k) t 1) 1 :
      k)

Tactic:
apply_fun (fun x ↦ (x.hom.hom.app rightFDRep).hom (single t 1) 1) at h
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
inst_3 : Nontrivial k
s t : G
h :
  Eq (α := k)
    ((@ConcreteCategory.hom _ (moduleCategory k) (fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u))
            carrier _ _
            (ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
            (ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
            (InducedCategory.Hom.hom
              (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom ((equivHom k G : (a : G) → Aut (forget k G)) s)))
                rightFDRep)) :
          (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
        (single (M := fun (a : G) ↦ k) t 1) 1 :
      k)
    ((@ConcreteCategory.hom _ (moduleCategory k) (fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u))
            carrier _ _
            (ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
            (ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
            (InducedCategory.Hom.hom
              (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom ((equivHom k G : (a : G) → Aut (forget k G)) t)))
                rightFDRep)) :
          (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
        (single (M := fun (a : G) ↦ k) t 1) 1 :
      k)
⊢ s = t

Tactic:
simp_all [single_apply]

Premises used: Pi.single_apply
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
inst_3 : Nontrivial k
s t : G
h :
  Eq (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
    ((equivHom k G : (a : G) → Aut (forget k G)) s :
      Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
    ((equivHom k G : (a : G) → Aut (forget k G)) t :
      Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
⊢ Eq (α := k)
    ((@ConcreteCategory.hom _ (moduleCategory k) (fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u))
            carrier _ _
            (ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
            (ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
            (InducedCategory.Hom.hom
              (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom ((equivHom k G : (a : G) → Aut (forget k G)) s)))
                rightFDRep)) :
          (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
        (single (M := fun (a : G) ↦ k) t 1) 1 :
      k)
    ((@ConcreteCategory.hom _ (moduleCategory k) (fun (x1 x2 : ModuleCat k) ↦ (↑x1 : Type u) →ₗ[k] (↑x2 : Type u))
            carrier _ _
            (ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
            (ObjectProperty.FullSubcategory.obj (P := isFG k)
              (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
            (InducedCategory.Hom.hom
              (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom ((equivHom k G : (a : G) → Aut (forget k G)) t)))
                rightFDRep)) :
          (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
        (single (M := fun (a : G) ↦ k) t 1) 1 :
      k)

Tactic:
classical
  apply_fun (fun x ↦ (x.hom.hom.app rightFDRep).hom (single t 1) 1) at h
  simp_all [single_apply]

Premises used: Pi.single_apply
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
g : G
h :
  ∀
    (u :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))) :
        Type u)),
    Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
      ((Hom.hom
              (InducedCategory.Hom.hom
                (CategoryStruct.comp (Y :=
                  Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
                  ((Action.ρ (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) :
                      (a : G) → End (rightFDRep ⊗ rightFDRep).V)
                    g)
                  (InducedCategory.homMk (↟(LinearMap.mul' k (G → k)))))) :
            (a : (↑(rightFDRep ⊗ rightFDRep).V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
          u :
        (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
      ((Hom.hom
              (InducedCategory.Hom.hom
                (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                  (InducedCategory.homMk (↟(LinearMap.mul' k (G → k))))
                  ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) g))) :
            (a : (↑(rightFDRep ⊗ rightFDRep).V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
          u :
        (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
⊢ Eq.{u + 1} (α :=
    Quiver.Hom (V := FGModuleCat k) (Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      (Action.V (G := G) rightFDRep))
    (CategoryStruct.comp (Y := Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      ((Action.ρ (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) :
          (a : G) → End (rightFDRep ⊗ rightFDRep).V)
        g)
      (InducedCategory.homMk (↟(LinearMap.mul' k (G → k)))))
    (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep) (InducedCategory.homMk (↟(LinearMap.mul' k (G → k))))
      ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) g))

Tactic:
ext u
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
g : G
u :
  (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
        (Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))) :
    Type u)
⊢ Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
                ((Action.ρ (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) :
                    (a : G) → End (rightFDRep ⊗ rightFDRep).V)
                  g)
                (InducedCategory.homMk (↟(LinearMap.mul' k (G → k)))))) :
          (a : (↑(rightFDRep ⊗ rightFDRep).V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        u :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                (InducedCategory.homMk (↟(LinearMap.mul' k (G → k))))
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) g))) :
          (a : (↑(rightFDRep ⊗ rightFDRep).V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        u :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))

Tactic:
TensorProduct.induction_on u rfl (fun _ _ ↦ rfl) (fun _ _ hx hy ↦ ?_)

Premises used: TensorProduct.induction_on
-- 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)
f g : G → k
⊢ Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G))
        (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom ≫ η.hom.hom.app rightFDRep)
    (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom)

Tactic:
have nat := η.hom.hom.naturality mulRepHom
-- 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)
f g : G → k
nat :
  Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G))
        (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom ≫ η.hom.hom.app rightFDRep)
    (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom)
⊢ ∀ (X Y : FDRep k G),
    Eq (α :=
      Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y) ⟶
        Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y))
      (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) X Y)) (η.hom.hom.app X ⊗ₘ η.hom.hom.app Y)

Tactic:
have tensor (X Y) : η.hom.hom.app (X ⊗ Y) = (η.hom.hom.app X ⊗ₘ η.hom.hom.app Y) :=
    η.hom.isMonoidal.tensor X Y
-- 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)
f g : G → k
nat :
  Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G))
        (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom ≫ η.hom.hom.app rightFDRep)
    (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom)
tensor :
  ∀ (X Y : FDRep k G),
    Eq (α :=
      Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y) ⟶
        Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y))
      (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) X Y)) (η.hom.hom.app X ⊗ₘ η.hom.hom.app Y)
⊢ Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G))
        (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom ≫ η.hom.hom.app rightFDRep)
    ((η.hom.hom.app rightFDRep ⊗ₘ η.hom.hom.app rightFDRep) ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom)

Tactic:
rw [tensor] at nat
-- 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)
f g : G → k
nat :
  Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G))
        (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom ≫ η.hom.hom.app rightFDRep)
    (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom)
tensor :
  ∀ (X Y : FDRep k G),
    Eq (α :=
      Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y) ⟶
        Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y))
      (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) X Y)) (η.hom.hom.app X ⊗ₘ η.hom.hom.app Y)
nat₁ :
  Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G))
        (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom ≫ η.hom.hom.app rightFDRep)
    ((η.hom.hom.app rightFDRep ⊗ₘ η.hom.hom.app rightFDRep) ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom)
⊢ ∀ (X Y : FDRep k G),
    Eq (α :=
      Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y) ⟶
        Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y))
      (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) X Y)) (η.hom.hom.app X ⊗ₘ η.hom.hom.app Y)

Tactic:
rw [tensor] at nat
-- 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)
f g : G → k
nat :
  Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G))
        (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom ≫ η.hom.hom.app rightFDRep)
    ((η.hom.hom.app rightFDRep ⊗ₘ η.hom.hom.app rightFDRep) ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom)
tensor :
  ∀ (X Y : FDRep k G),
    Eq (α :=
      Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y) ⟶
        Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y))
      (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) X Y)) (η.hom.hom.app X ⊗ₘ η.hom.hom.app Y)
⊢ let α : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep));
  (α : (a : G → k) → G → k) (f * g) =
    HMul.hMul (α := G → k) (β := G → k) ((α : (a : G → k) → G → k) f : G → k) ((α : (a : G → k) → G → k) g : G → k)

Tactic:
ConcreteCategory.congr_hom ((CategoryTheory.forget _).congr_map nat) (f ⊗ₜ[k] g)

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, CategoryTheory.forget, CategoryTheory.Functor.congr_map, CategoryTheory.ConcreteCategory.congr_hom, FreeAddMonoid.sumAux
-- 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)
f g : G → k
nat :
  Eq (α :=
    Quiver.Hom (V := FGModuleCat k)
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G))
        (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
      (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep))
    (CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom ≫ η.hom.hom.app rightFDRep)
    ((η.hom.hom.app rightFDRep ⊗ₘ η.hom.hom.app rightFDRep) ≫
      CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) mulRepHom)
tensor :
  ∀ (X Y : FDRep k G),
    Eq (α :=
      Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y) ⟶
        Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y))
      (η.hom.hom.app (tensorObj (𝒞 := Action.instCategory) X Y)) (η.hom.hom.app X ⊗ₘ η.hom.hom.app Y)
⊢ let α : (G → k) →ₗ[k] G → k := Hom.hom (InducedCategory.Hom.hom (η.hom.hom.app rightFDRep));
  (α : (a : G → k) → G → k) (f * g) =
    HMul.hMul (α := G → k) (β := G → k) ((α : (a : G → k) → G → k) f : G → k) ((α : (a : G → k) → G → k) g : G → k)

Tactic:
exact ConcreteCategory.congr_hom ((CategoryTheory.forget _).congr_map nat) (f ⊗ₜ[k] g)

Premises used: CategoryTheory.forget, CategoryTheory.Functor.congr_map, CategoryTheory.ConcreteCategory.congr_hom
-- 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))
refine : Eq (α := G → k) ((α : (a : G → k) → G → k) 1 : G → k) (1 : G → k)
⊢ (G → k) →ₐ[k] G → k

Tactic:
refine AlgHom.ofLinearMap α ?_ (map_mul_toRightFDRepComp η)

Premises used: AlgHom.ofLinearMap, TannakaDuality.FiniteGroup.map_mul_toRightFDRepComp
-- 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 : 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) ((α_inv : (a : G → k) → G → k) 1 : G → k) : G → k) (1 : G → k)

Tactic:
have h := this
-- 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))
suffices : 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:
suffices α (α_inv 1) = (1 : G → k) by
    have h := this
    rwa [← one_mul (α_inv 1), map_mul_toRightFDRepComp, h, mul_one] at this
-- 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))
⊢ η.inv ≫ η.hom = 𝟙 (forget k G)

Tactic:
have := η.inv_hom_id
-- 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 : η.inv ≫ η.hom = 𝟙 (forget k G)
⊢ Eq (α :=
    (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
          (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
      Type u))
    ((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 ((η.inv ≫ η.hom).hom.app rightFDRep)) :
          (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
        1 :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
        Type u))
    ((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 (NatTrans.app (LaxMonoidalFunctor.Hom.hom (𝟙 (forget k G))) rightFDRep)) :
          (a : (↑((forget k G).obj rightFDRep).obj : Type u)) → (↑((forget k G).obj rightFDRep).obj : Type u))
        1 :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
            (Functor.obj (C := FDRep k G) (LaxMonoidalFunctor.toFunctor (forget k G)) rightFDRep)) :
        Type u))

Tactic:
apply_fun (fun x ↦ (x.hom.app rightFDRep).hom (1 : G → k)) at this