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
s x : G
f : (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u)
h :
  ∀ (x_1 : G),
    Eq (α := k)
      ((Hom.hom
              (InducedCategory.Hom.hom
                (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                  ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x)
                  (InducedCategory.homMk (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s))))) :
            (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
          f x_1 :
        k)
      ((Hom.hom
              (InducedCategory.Hom.hom
                (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                  (InducedCategory.homMk (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s)))
                  ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x))) :
            (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
          f x_1 :
        k)
⊢ 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) rightFDRep)
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x)
                (InducedCategory.homMk (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s))))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        f :
      (↑(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 (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s)))
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        f :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))

Tactic:
funext _
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
s x : G
f : (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u)
x_1 : G
h : s⁻¹ * x_1 * x = s⁻¹ * (x_1 * x)
⊢ Eq (α := k)
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x)
                (InducedCategory.homMk (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s))))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        f x_1 :
      k)
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                (InducedCategory.homMk (↟((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s)))
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) x))) :
          (a : (↑rightFDRep.V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        f x_1 :
      k)

Tactic:
apply congrArg f

Premises used: congrArg
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
s x : G
f : (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u)
x_1 : G
⊢ s⁻¹ * x_1 * x = s⁻¹ * (x_1 * x)

Tactic:
mul_assoc ..

Premises used: mul_assoc
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
s x : G
f : (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u)
x_1 : G
⊢ s⁻¹ * x_1 * x = s⁻¹ * (x_1 * x)

Tactic:
exact mul_assoc ..

Premises used: mul_assoc
-- 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
⊢ ∃ (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)

Tactic:
⟨s, (basisFun k G).ext fun u ↦ ?_⟩

Premises used: Exists.intro, Pi.basisFun, Module.Basis.ext
-- 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
refine :
  ∀ (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)

Tactic:
refine ⟨s, (basisFun k G).ext fun u ↦ ?_⟩
-- 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 : G
simp :
  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)
⊢ 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))

Tactic:
simp only [rightFDRep, forget_obj]

Premises used: TannakaDuality.FiniteGroup.forget_obj, TannakaDuality.FiniteGroup.rightFDRep
-- 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 : G
h :
  ∀ (t : G),
    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)
⊢ 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:
ext t
-- 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
⊢ 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⁻¹))

Tactic:
have nat := η.hom.hom.naturality (leftRegularFDRepHom t⁻¹)
-- 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)

Tactic:
simp
-- 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)
    ((((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)
    ((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))
        ((((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)
        1 :
      k)

Tactic:
congrFun congr(($nat.symm).hom (single u 1)) 1

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, Pi.single, congrFun, CategoryTheory.InducedCategory.Hom.hom, OfNat.ofNat, Eq.symm, DFunLike.coe
-- 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)
    ((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))
        ((((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)
        1 :
      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)

Tactic:
congr($hs (leftRegular t⁻¹ (single u 1)))

Premises used: congrArg, id, Pi.single, TannakaDuality.FiniteGroup.leftRegular, Inv.inv, OfNat.ofNat, DFunLike.coe
-- 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⁻¹))
pos :
  u = t * s →
    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)
neg :
  ¬u = t * s →
    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)
    ((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)

Tactic:
by_cases u = t * s
-- 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⁻¹))
h : u = t * s
⊢ 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)

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 : 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⁻¹))
h : ¬u = t * s
⊢ 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)

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 : IsDomain k
η : Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G)
obtain :
  ∀ (s : G)
    (h :
      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)),
    ∃ (a : G), (equivHom k G : (a : G) → Aut (forget k G)) a = η
⊢ ∃ (a : G), (equivHom k G : (a : G) → Aut (forget k G)) a = η

Tactic:
obtain ⟨s, h⟩ := toRightFDRepComp_in_rightRegular η

Premises used: TannakaDuality.FiniteGroup.toRightFDRepComp_in_rightRegular