awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : Membership.mem (γ := Submodule A W) { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ } w
x : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
h :
  Membership.mem (α := W) N
    ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) ((ρ.asModuleEquiv : (a : ρ.asModule) → W) w : W) : W)
⊢ Membership.mem (α := W) (γ := Submodule A W) { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
    ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) w : W)

Tactic:
h

Premises used: Set.Mem
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
N : Submodule A[G] ρ.asModule
g : G
w : W
hw : Membership.mem (γ := Submodule A W) { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ } w
x : Module A[G] W := ρ.instModuleMonoidAlgebraAsModule
h :
  Membership.mem (α := W) N
    ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) ((ρ.asModuleEquiv : (a : ρ.asModule) → W) w : W) : W)
⊢ Membership.mem (α := W) (γ := Submodule A W) { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
    ((((ρ : (a : G) → W →ₗ[A] W) g : W →ₗ[A] W) : (a : W) → W) w : W)

Tactic:
exact h
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
N : Submodule A[G] ρ.asModule
w : W
⊢ w ∈ ofSubmodule' N ↔ w ∈ N

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
⊢ ∀ {a b : Subrepresentation ρ},
    LE.le (α := Submodule A[G] ρ.asModule)
        (({ toFun := asSubmodule, invFun := ofSubmodule', left_inv := ⋯, right_inv := ⋯ } :
              (a : Subrepresentation ρ) → Submodule A[G] ρ.asModule)
            a :
          Submodule A[G] ρ.asModule)
        (({ toFun := asSubmodule, invFun := ofSubmodule', left_inv := ⋯, right_inv := ⋯ } :
              (a : Subrepresentation ρ) → Submodule A[G] ρ.asModule)
            b :
          Submodule A[G] ρ.asModule) ↔
      a ≤ b

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Subrepresentation
Goal:
A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst : CommSemiring A
inst_1 : Monoid G
inst_2 : AddCommMonoid W
inst_3 : Module A W
ρ : Representation A G W
inst_4 : AddCommMonoid M
inst_5 : Module A[G] M
⊢ ∀ {a b : Submodule A[G] M},
    LE.le (α :=
        Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M) (Representation.ofModule M))
        (({ toFun := ofSubmodule, invFun := asSubmodule', left_inv := ⋯, right_inv := ⋯ } :
              (a : Submodule A[G] M) → Subrepresentation (Representation.ofModule M))
            a :
          Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M)
            (Representation.ofModule M))
        (({ toFun := ofSubmodule, invFun := asSubmodule', left_inv := ⋯, right_inv := ⋯ } :
              (a : Submodule A[G] M) → Subrepresentation (Representation.ofModule M))
            b :
          Subrepresentation.{u_1, u_2, u_4} (A := A) (G := G) (W := RestrictScalars A A[G] M)
            (Representation.ofModule M)) ↔
      a ≤ b

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X : FDRep k G
⊢ Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X = X.V

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
X Y : FDRep k G
f : X ⟶ Y
⊢ CategoryTheory.Functor.map (LaxMonoidalFunctor.toFunctor (forget k G)) f = f.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
g : G
X : FDRep k G
h :
  ∀ (x : (↑(X.V.obj (P := isFG k)) : Type u)),
    Eq (α := (↑(X.V.obj (P := isFG k)) : Type u))
      ((Hom.hom
              (InducedCategory.Hom.hom
                (CategoryStruct.comp (Y := X.V)
                  (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g)))
                  (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g⁻¹))))) :
            (a : (↑X.V.obj : Type u)) → (↑X.V.obj : Type u))
          x :
        (↑(X.V.obj (P := isFG k)) : Type u))
      ((Hom.hom (InducedCategory.Hom.hom (𝟙 X.V)) : (a : (↑X.V.obj : Type u)) → (↑X.V.obj : Type u)) x :
        (↑(X.V.obj (P := isFG k)) : Type u))
⊢ CategoryStruct.comp (Y := X.V) (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g)))
      (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g⁻¹))) =
    𝟙 X.V

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
g : G
X : FDRep k G
x : (↑(X.V.obj (P := isFG k)) : Type u)
⊢ Eq (α := (↑(X.V.obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := X.V)
                (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g)))
                (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g⁻¹))))) :
          (a : (↑X.V.obj : Type u)) → (↑X.V.obj : Type u))
        x :
      (↑(X.V.obj (P := isFG k)) : Type u))
    ((Hom.hom (InducedCategory.Hom.hom (𝟙 X.V)) : (a : (↑X.V.obj : Type u)) → (↑X.V.obj : Type u)) x :
      (↑(X.V.obj (P := isFG k)) : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
g : G
X : FDRep k G
h :
  ∀ (x : (↑(X.V.obj (P := isFG k)) : Type u)),
    Eq (α := (↑(X.V.obj (P := isFG k)) : Type u))
      ((Hom.hom
              (InducedCategory.Hom.hom
                (CategoryStruct.comp (Y := X.V)
                  (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g⁻¹)))
                  (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g))))) :
            (a : (↑X.V.obj : Type u)) → (↑X.V.obj : Type u))
          x :
        (↑(X.V.obj (P := isFG k)) : Type u))
      ((Hom.hom (InducedCategory.Hom.hom (𝟙 X.V)) : (a : (↑X.V.obj : Type u)) → (↑X.V.obj : Type u)) x :
        (↑(X.V.obj (P := isFG k)) : Type u))
⊢ CategoryStruct.comp (Y := X.V)
      (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g⁻¹)))
      (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g))) =
    𝟙 X.V

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
g : G
X : FDRep k G
x : (↑(X.V.obj (P := isFG k)) : Type u)
⊢ Eq (α := (↑(X.V.obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := X.V)
                (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g⁻¹)))
                (InducedCategory.homMk (↟((X.ρ : (a : G) → (↑X.V : Type u) →ₗ[k] (↑X.V : Type u)) g))))) :
          (a : (↑X.V.obj : Type u)) → (↑X.V.obj : Type u))
        x :
      (↑(X.V.obj (P := isFG k)) : Type u))
    ((Hom.hom (InducedCategory.Hom.hom (𝟙 X.V)) : (a : (↑X.V.obj : Type u)) → (↑X.V.obj : Type u)) x :
      (↑(X.V.obj (P := isFG k)) : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
g : G
X Y : FDRep k G
⊢ Eq (α :=
    tensorObj (𝒞 := ObjectProperty.FullSubcategory.category (isFG k))
        (Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) X)
        (Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) Y) ⟶
      Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) (tensorObj (𝒞 := Action.instCategory) X Y))
    (Functor.LaxMonoidal.μ (LaxMonoidalFunctor.toFunctor (forget k G)) X Y ≫
      (equivApp g (tensorObj (𝒞 := Action.instCategory) X Y)).hom)
    (((equivApp g X).hom ⊗ₘ (equivApp g Y).hom) ≫ Functor.LaxMonoidal.μ (LaxMonoidalFunctor.toFunctor (forget k G)) X Y)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
h :
  ∀ (x : FDRep k G) (x_1 : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u)),
    Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u))
      ((Hom.hom
              (InducedCategory.Hom.hom
                (NatTrans.app
                  (LaxMonoidalFunctor.Hom.hom (Iso.hom (LaxMonoidalFunctor.isoOfComponents (equivApp 1) ⋯ ⋯ ⋯))) x)) :
            (a : (↑((forget k G).obj x).obj : Type u)) → (↑((forget k G).obj x).obj : Type u))
          x_1 :
        (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u))
      ((Hom.hom (InducedCategory.Hom.hom (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom 1)) x)) :
            (a : (↑((forget k G).obj x).obj : Type u)) → (↑((forget k G).obj x).obj : Type u))
          x_1 :
        (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u))
⊢ Eq.{u + 2} (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
    (LaxMonoidalFunctor.isoOfComponents (equivApp 1) ⋯ ⋯ ⋯) 1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x : FDRep k G
x_1 : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u)
h :
  Eq (α := (↑x.V : Type u)) ((1 : (a : (↑x.V : Type u)) → (↑x.V : Type u)) x_1 : (↑x.V : Type u))
    ((Hom.hom (InducedCategory.Hom.hom (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom 1)) x)) :
          (a : (↑x.V : Type u)) → (↑x.V : Type u))
        x_1 :
      (↑x.V : Type u))
⊢ Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (NatTrans.app
                (LaxMonoidalFunctor.Hom.hom (Iso.hom (LaxMonoidalFunctor.isoOfComponents (equivApp 1) ⋯ ⋯ ⋯))) x)) :
          (a : (↑((forget k G).obj x).obj : Type u)) → (↑((forget k G).obj x).obj : Type u))
        x_1 :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u))
    ((Hom.hom (InducedCategory.Hom.hom (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom 1)) x)) :
          (a : (↑((forget k G).obj x).obj : Type u)) → (↑((forget k G).obj x).obj : Type u))
        x_1 :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x : FDRep k G
x_1 : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x).obj (P := isFG k)) : Type u)
⊢ Eq (α := (↑x.V : Type u)) ((1 : (a : (↑x.V : Type u)) → (↑x.V : Type u)) x_1 : (↑x.V : Type u))
    ((Hom.hom (InducedCategory.Hom.hom (NatTrans.app (LaxMonoidalFunctor.Hom.hom (Iso.hom 1)) x)) :
          (a : (↑x.V : Type u)) → (↑x.V : Type u))
        x_1 :
      (↑x.V : Type u))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x x_1 : G
h :
  ∀ (x_2 : FDRep k G)
    (x_3 : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u)),
    Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u))
      ((Hom.hom
              (InducedCategory.Hom.hom
                (NatTrans.app
                  (LaxMonoidalFunctor.Hom.hom (Iso.hom (LaxMonoidalFunctor.isoOfComponents (equivApp (x * x_1)) ⋯ ⋯ ⋯)))
                  x_2)) :
            (a : (↑((forget k G).obj x_2).obj : Type u)) → (↑((forget k G).obj x_2).obj : Type u))
          x_3 :
        (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u))
      ((Hom.hom
              ((HMul.hMul (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
                          (LaxMonoidalFunctor.isoOfComponents (equivApp x) ⋯ ⋯ ⋯)
                          (LaxMonoidalFunctor.isoOfComponents (equivApp x_1) ⋯ ⋯ ⋯)).hom.hom.app
                  x_2).hom :
            (a : (↑((forget k G).obj x_2).obj : Type u)) → (↑((forget k G).obj x_2).obj : Type u))
          x_3 :
        (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u))
⊢ LaxMonoidalFunctor.isoOfComponents (equivApp (x * x_1)) ⋯ ⋯ ⋯ =
    HMul.hMul (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
      (LaxMonoidalFunctor.isoOfComponents (equivApp x) ⋯ ⋯ ⋯) (LaxMonoidalFunctor.isoOfComponents (equivApp x_1) ⋯ ⋯ ⋯)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x x_1 : G
x_2 : FDRep k G
x_3 : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u)
h :
  Eq (α := (↑x_2.V : Type u))
    ((HMul.hMul (α := (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u)) (β := (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u))
            ((x_2.ρ : (a : G) → (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u)) x :
              (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u))
            ((x_2.ρ : (a : G) → (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u)) x_1 :
              (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u)) :
          (a : (↑x_2.V : Type u)) → (↑x_2.V : Type u))
        x_3 :
      (↑x_2.V : Type u))
    ((Hom.hom
            ((HMul.hMul (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
                        (LaxMonoidalFunctor.isoOfComponents (equivApp x) ⋯ ⋯ ⋯)
                        (LaxMonoidalFunctor.isoOfComponents (equivApp x_1) ⋯ ⋯ ⋯)).hom.hom.app
                x_2).hom :
          (a : (↑x_2.V : Type u)) → (↑x_2.V : Type u))
        x_3 :
      (↑x_2.V : Type u))
⊢ Eq (α := (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (NatTrans.app
                (LaxMonoidalFunctor.Hom.hom (Iso.hom (LaxMonoidalFunctor.isoOfComponents (equivApp (x * x_1)) ⋯ ⋯ ⋯)))
                x_2)) :
          (a : (↑((forget k G).obj x_2).obj : Type u)) → (↑((forget k G).obj x_2).obj : Type u))
        x_3 :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u))
    ((Hom.hom
            ((HMul.hMul (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
                        (LaxMonoidalFunctor.isoOfComponents (equivApp x) ⋯ ⋯ ⋯)
                        (LaxMonoidalFunctor.isoOfComponents (equivApp x_1) ⋯ ⋯ ⋯)).hom.hom.app
                x_2).hom :
          (a : (↑((forget k G).obj x_2).obj : Type u)) → (↑((forget k G).obj x_2).obj : Type u))
        x_3 :
      (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x x_1 : G
x_2 : FDRep k G
x_3 : (↑((Functor.obj (LaxMonoidalFunctor.toFunctor (forget k G)) x_2).obj (P := isFG k)) : Type u)
⊢ Eq (α := (↑x_2.V : Type u))
    ((HMul.hMul (α := (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u)) (β := (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u))
            ((x_2.ρ : (a : G) → (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u)) x :
              (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u))
            ((x_2.ρ : (a : G) → (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u)) x_1 :
              (↑x_2.V : Type u) →ₗ[k] (↑x_2.V : Type u)) :
          (a : (↑x_2.V : Type u)) → (↑x_2.V : Type u))
        x_3 :
      (↑x_2.V : Type u))
    ((Hom.hom
            ((HMul.hMul (α := Aut (C := LaxMonoidalFunctor (FDRep k G) (FGModuleCat k)) (forget k G))
                        (LaxMonoidalFunctor.isoOfComponents (equivApp x) ⋯ ⋯ ⋯)
                        (LaxMonoidalFunctor.isoOfComponents (equivApp x_1) ⋯ ⋯ ⋯)).hom.hom.app
                x_2).hom :
          (a : (↑x_2.V : Type u)) → (↑x_2.V : Type u))
        x_3 :
      (↑x_2.V : Type u))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
h :
  ∀ (x : G → k) (x_1 : G),
    Eq (α := k)
      (({ toFun := fun (f : G → k) (t : G) ↦ f (t * 1), map_add' := ⋯, map_smul' := ⋯ } : (a : G → k) → G → k) x x_1 :
        k)
      ((1 : (a : G → k) → G → k) x x_1 : k)
⊢ Eq.{u + 1} (α := (G → k) →ₗ[k] G → k) { toFun := fun (f : G → k) (t : G) ↦ f (t * 1), map_add' := ⋯, map_smul' := ⋯ }
    1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x : G → k
x_1 : G
⊢ Eq (α := k)
    (({ toFun := fun (f : G → k) (t : G) ↦ f (t * 1), map_add' := ⋯, map_smul' := ⋯ } : (a : G → k) → G → k) x x_1 : k)
    ((1 : (a : G → k) → G → k) x x_1 : k)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x x_1 : G
h :
  ∀ (x_2 : G → k) (x_3 : G),
    Eq (α := k)
      (({ toFun := fun (f : G → k) (t : G) ↦ f (t * (x * x_1)), map_add' := ⋯, map_smul' := ⋯ } : (a : G → k) → G → k)
          x_2 x_3 :
        k)
      ((HMul.hMul (α := (G → k) →ₗ[k] G → k)
              { toFun := fun (f : G → k) (t : G) ↦ f (t * x), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k }
              { toFun := fun (f : G → k) (t : G) ↦ f (t * x_1), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k } :
            (a : G → k) → G → k)
          x_2 x_3 :
        k)
⊢ { toFun := fun (f : G → k) (t : G) ↦ f (t * (x * x_1)), map_add' := ⋯, map_smul' := ⋯ } =
    HMul.hMul (α := (G → k) →ₗ[k] G → k)
      { toFun := fun (f : G → k) (t : G) ↦ f (t * x), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k }
      { toFun := fun (f : G → k) (t : G) ↦ f (t * x_1), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k }

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x x_1 : G
x_2 : G → k
x_3 : G
⊢ Eq (α := k)
    (({ toFun := fun (f : G → k) (t : G) ↦ f (t * (x * x_1)), map_add' := ⋯, map_smul' := ⋯ } : (a : G → k) → G → k) x_2
        x_3 :
      k)
    ((HMul.hMul (α := (G → k) →ₗ[k] G → k)
            { toFun := fun (f : G → k) (t : G) ↦ f (t * x), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k }
            { toFun := fun (f : G → k) (t : G) ↦ f (t * x_1), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k } :
          (a : G → k) → G → k)
        x_2 x_3 :
      k)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
s t : G
f : G → k
⊢ (((rightRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k) f t = f (t * s)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
h :
  ∀ (x : G → k) (x_1 : G),
    Eq (α := k)
      (({ toFun := fun (f : G → k) (t : G) ↦ f (1⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } : (a : G → k) → G → k) x x_1 :
        k)
      ((1 : (a : G → k) → G → k) x x_1 : k)
⊢ Eq.{u + 1} (α := (G → k) →ₗ[k] G → k)
    { toFun := fun (f : G → k) (t : G) ↦ f (1⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } 1

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x : G → k
x_1 : G
⊢ Eq (α := k)
    (({ toFun := fun (f : G → k) (t : G) ↦ f (1⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } : (a : G → k) → G → k) x x_1 :
      k)
    ((1 : (a : G → k) → G → k) x x_1 : k)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x x_1 : G
h :
  ∀ (x_2 : G → k) (x_3 : G),
    Eq (α := k)
      (({ toFun := fun (f : G → k) (t : G) ↦ f ((x * x_1)⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } : (a : G → k) → G → k)
          x_2 x_3 :
        k)
      ((HMul.hMul (α := (G → k) →ₗ[k] G → k)
              { toFun := fun (f : G → k) (t : G) ↦ f (x⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k }
              { toFun := fun (f : G → k) (t : G) ↦ f (x_1⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ :
                (G → k) →ₗ[k] G → k } :
            (a : G → k) → G → k)
          x_2 x_3 :
        k)
⊢ { toFun := fun (f : G → k) (t : G) ↦ f ((x * x_1)⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } =
    HMul.hMul (α := (G → k) →ₗ[k] G → k)
      { toFun := fun (f : G → k) (t : G) ↦ f (x⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k }
      { toFun := fun (f : G → k) (t : G) ↦ f (x_1⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k }

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
x x_1 : G
x_2 : G → k
x_3 : G
⊢ Eq (α := k)
    (({ toFun := fun (f : G → k) (t : G) ↦ f ((x * x_1)⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ } : (a : G → k) → G → k)
        x_2 x_3 :
      k)
    ((HMul.hMul (α := (G → k) →ₗ[k] G → k)
            { toFun := fun (f : G → k) (t : G) ↦ f (x⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k }
            { toFun := fun (f : G → k) (t : G) ↦ f (x_1⁻¹ * t), map_add' := ⋯, map_smul' := ⋯ : (G → k) →ₗ[k] G → k } :
          (a : G → k) → G → k)
        x_2 x_3 :
      k)

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
s t : G
f : G → k
⊢ (((leftRegular : (a : G) → (G → k) →ₗ[k] G → k) s : (G → k) →ₗ[k] G → k) : (a : G → k) → G → k) f t = f (s⁻¹ * t)

Tactic:
rfl

Premises used: rfl