[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
r : k
⊢ ↑(asAlgebraHom ρ) (Finsupp.single g r) = r • ↑ρ g
[PROOFSTEP]
simp only [asAlgebraHom_def, MonoidAlgebra.lift_single]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
⊢ ↑(asAlgebraHom ρ) (Finsupp.single g 1) = ↑ρ g
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
⊢ ↑(asAlgebraHom ρ) (↑(of k G) g) = ↑ρ g
[PROOFSTEP]
simp only [MonoidAlgebra.of_apply, asAlgebraHom_single, one_smul]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
r : k
x : V
⊢ ↑(AddEquiv.symm (asModuleEquiv ρ)) (r • x) =
    ↑(algebraMap k (MonoidAlgebra k G)) r • ↑(AddEquiv.symm (asModuleEquiv ρ)) x
[PROOFSTEP]
apply_fun ρ.asModuleEquiv
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
r : k
x : V
⊢ ↑(asModuleEquiv ρ) (↑(AddEquiv.symm (asModuleEquiv ρ)) (r • x)) =
    ↑(asModuleEquiv ρ) (↑(algebraMap k (MonoidAlgebra k G)) r • ↑(AddEquiv.symm (asModuleEquiv ρ)) x)
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
⊢ ↑(AddEquiv.symm (asModuleEquiv ρ)) (↑(↑ρ g) x) = ↑(of k G) g • ↑(AddEquiv.symm (asModuleEquiv ρ)) x
[PROOFSTEP]
apply_fun ρ.asModuleEquiv
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
x : V
⊢ ↑(asModuleEquiv ρ) (↑(AddEquiv.symm (asModuleEquiv ρ)) (↑(↑ρ g) x)) =
    ↑(asModuleEquiv ρ) (↑(of k G) g • ↑(AddEquiv.symm (asModuleEquiv ρ)) x)
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
⊢ ↑(↑(asAlgebraHom (ofModule M)) r) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (r • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
[PROOFSTEP]
apply MonoidAlgebra.induction_on r
[GOAL]
case hM
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (g : G),
    ↑(↑(asAlgebraHom (ofModule M)) (↑(of k G) g)) m =
      ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
        (↑(of k G) g • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
[PROOFSTEP]
intro g
[GOAL]
case hM
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
g : G
⊢ ↑(↑(asAlgebraHom (ofModule M)) (↑(of k G) g)) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (↑(of k G) g • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
[PROOFSTEP]
simp only [one_smul, MonoidAlgebra.lift_symm_apply, MonoidAlgebra.of_apply, Representation.asAlgebraHom_single,
  Representation.ofModule, AddEquiv.apply_eq_iff_eq, RestrictScalars.lsmul_apply_apply]
[GOAL]
case hadd
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (f g : MonoidAlgebra k G),
    ↑(↑(asAlgebraHom (ofModule M)) f) m =
        ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
          (f • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
      ↑(↑(asAlgebraHom (ofModule M)) g) m =
          ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
            (g • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
        ↑(↑(asAlgebraHom (ofModule M)) (f + g)) m =
          ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
            ((f + g) • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
[PROOFSTEP]
intro f g fw gw
[GOAL]
case hadd
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
f g : MonoidAlgebra k G
fw :
  ↑(↑(asAlgebraHom (ofModule M)) f) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (f • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
gw :
  ↑(↑(asAlgebraHom (ofModule M)) g) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (g • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
⊢ ↑(↑(asAlgebraHom (ofModule M)) (f + g)) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      ((f + g) • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
[PROOFSTEP]
simp only [fw, gw, map_add, add_smul, LinearMap.add_apply]
[GOAL]
case hsmul
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
⊢ ∀ (r : k) (f : MonoidAlgebra k G),
    ↑(↑(asAlgebraHom (ofModule M)) f) m =
        ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
          (f • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m) →
      ↑(↑(asAlgebraHom (ofModule M)) (r • f)) m =
        ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
          ((r • f) • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
[PROOFSTEP]
intro r f w
[GOAL]
case hsmul
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r✝ : MonoidAlgebra k G
m : RestrictScalars k (MonoidAlgebra k G) M
r : k
f : MonoidAlgebra k G
w :
  ↑(↑(asAlgebraHom (ofModule M)) f) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      (f • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
⊢ ↑(↑(asAlgebraHom (ofModule M)) (r • f)) m =
    ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => M) m)))
      ((r • f) • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
[PROOFSTEP]
simp only [w, AlgHom.map_smul, LinearMap.smul_apply, RestrictScalars.addEquiv_symm_map_smul_smul]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
g : G
x : RestrictScalars k (MonoidAlgebra k G) (asModule ρ)
⊢ ↑(↑(ofModule (asModule ρ)) g) x =
    ↑(AddEquiv.symm
          (RestrictScalars.addEquiv k (MonoidAlgebra k G)
            ((fun x => asModule ρ)
              (↑(↑ρ g) (↑(asModuleEquiv ρ) (↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x))))))
      (↑(AddEquiv.symm (asModuleEquiv ρ))
        (↑(↑ρ g) (↑(asModuleEquiv ρ) (↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x))))
[PROOFSTEP]
apply_fun RestrictScalars.addEquiv _ _ ρ.asModule using (RestrictScalars.addEquiv _ _ ρ.asModule).injective
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
g : G
x : RestrictScalars k (MonoidAlgebra k G) (asModule ρ)
⊢ ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) (↑(↑(ofModule (asModule ρ)) g) x) =
    ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ))
      (↑(AddEquiv.symm
            (RestrictScalars.addEquiv k (MonoidAlgebra k G)
              ((fun x => asModule ρ)
                (↑(↑ρ g) (↑(asModuleEquiv ρ) (↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x))))))
        (↑(AddEquiv.symm (asModuleEquiv ρ))
          (↑(↑ρ g) (↑(asModuleEquiv ρ) (↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x)))))
[PROOFSTEP]
dsimp [ofModule, RestrictScalars.lsmul_apply_apply]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
g : G
x : RestrictScalars k (MonoidAlgebra k G) (asModule ρ)
⊢ ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ))
      (↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)))
        (MonoidAlgebra.single g 1 • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x)) =
    ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ))
      (↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)))
        (↑(AddEquiv.symm (asModuleEquiv ρ))
          (↑(↑ρ g) (↑(asModuleEquiv ρ) (↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) (asModule ρ)) x)))))
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : asModule (ofModule M)
⊢ ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) (↑(asModuleEquiv (ofModule M)) (r • m)) =
    r • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) (↑(asModuleEquiv (ofModule M)) m)
[PROOFSTEP]
dsimp
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
ρ : Representation k G V
M : Type u_4
inst✝¹ : AddCommMonoid M
inst✝ : Module (MonoidAlgebra k G) M
r : MonoidAlgebra k G
m : asModule (ofModule M)
⊢ ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M)
      (↑(↑(asAlgebraHom (ofModule M)) r) (↑(asModuleEquiv (ofModule M)) m)) =
    r • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) M) (↑(asModuleEquiv (ofModule M)) m)
[PROOFSTEP]
simp only [AddEquiv.apply_symm_apply, ofModule_asAlgebraHom_apply_apply]
[GOAL]
k : Type u_1
inst✝² : CommSemiring k
G : Type u_2
inst✝¹ : Monoid G
H : Type u_3
inst✝ : MulAction G H
⊢ (fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g)) 1 = 1
[PROOFSTEP]
ext x y
[GOAL]
case h.h.h
k : Type u_1
inst✝² : CommSemiring k
G : Type u_2
inst✝¹ : Monoid G
H : Type u_3
inst✝ : MulAction G H
x y : H
⊢ ↑(↑(comp ((fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g)) 1) (Finsupp.lsingle x)) 1) y =
    ↑(↑(comp 1 (Finsupp.lsingle x)) 1) y
[PROOFSTEP]
dsimp
[GOAL]
case h.h.h
k : Type u_1
inst✝² : CommSemiring k
G : Type u_2
inst✝¹ : Monoid G
H : Type u_3
inst✝ : MulAction G H
x y : H
⊢ ↑(Finsupp.mapDomain (fun x => 1 • x) (Finsupp.single x 1)) y = ↑(Finsupp.single x 1) y
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
inst✝² : CommSemiring k
G : Type u_2
inst✝¹ : Monoid G
H : Type u_3
inst✝ : MulAction G H
x y : G
⊢ OneHom.toFun
      { toFun := fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g),
        map_one' := (_ : (fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g)) 1 = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g),
          map_one' := (_ : (fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g)) 1 = 1) }
        x *
      OneHom.toFun
        { toFun := fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g),
          map_one' := (_ : (fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g)) 1 = 1) }
        y
[PROOFSTEP]
ext z w
[GOAL]
case h.h.h
k : Type u_1
inst✝² : CommSemiring k
G : Type u_2
inst✝¹ : Monoid G
H : Type u_3
inst✝ : MulAction G H
x y : G
z w : H
⊢ ↑(↑(comp
              (OneHom.toFun
                { toFun := fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g),
                  map_one' := (_ : (fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g)) 1 = 1) }
                (x * y))
              (Finsupp.lsingle z))
          1)
      w =
    ↑(↑(comp
              (OneHom.toFun
                  { toFun := fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g),
                    map_one' := (_ : (fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g)) 1 = 1) }
                  x *
                OneHom.toFun
                  { toFun := fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g),
                    map_one' := (_ : (fun g => Finsupp.lmapDomain k k ((fun x x_1 => x • x_1) g)) 1 = 1) }
                  y)
              (Finsupp.lsingle z))
          1)
      w
[PROOFSTEP]
simp [mul_smul]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
⊢ ↑(↑(↑(ofMulAction k G H) g) f) h = ↑f (g⁻¹ • h)
[PROOFSTEP]
conv_lhs => rw [← smul_inv_smul g h]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
| ↑(↑(↑(ofMulAction k G H) g) f) h
[PROOFSTEP]
rw [← smul_inv_smul g h]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
| ↑(↑(↑(ofMulAction k G H) g) f) h
[PROOFSTEP]
rw [← smul_inv_smul g h]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
| ↑(↑(↑(ofMulAction k G H) g) f) h
[PROOFSTEP]
rw [← smul_inv_smul g h]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
⊢ ↑(↑(↑(ofMulAction k G H) g) f) (g • g⁻¹ • h) = ↑f (g⁻¹ • h)
[PROOFSTEP]
let h' := g⁻¹ • h
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
⊢ ↑(↑(↑(ofMulAction k G H) g) f) (g • g⁻¹ • h) = ↑f (g⁻¹ • h)
[PROOFSTEP]
change ofMulAction k G H g f (g • h') = f h'
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
⊢ ↑(↑(↑(ofMulAction k G H) g) f) (g • h') = ↑f h'
[PROOFSTEP]
have hg : Function.Injective ((· • ·) g : H → H) := by
  intro h₁ h₂
  simp
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
⊢ Function.Injective ((fun x x_1 => x • x_1) g)
[PROOFSTEP]
intro h₁ h₂
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
h₁ h₂ : H
⊢ (fun x x_1 => x • x_1) g h₁ = (fun x x_1 => x • x_1) g h₂ → h₁ = h₂
[PROOFSTEP]
simp
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁴ : CommSemiring k
inst✝³ : Group G
inst✝² : AddCommMonoid V
inst✝¹ : Module k V
ρ : Representation k G V
H : Type u_4
inst✝ : MulAction G H
g : G
f : H →₀ k
h : H
h' : H := g⁻¹ • h
hg : Function.Injective ((fun x x_1 => x • x_1) g)
⊢ ↑(↑(↑(ofMulAction k G H) g) f) (g • h') = ↑f h'
[PROOFSTEP]
simp only [ofMulAction_def, Finsupp.lmapDomain_apply, Finsupp.mapDomain_apply, hg]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
g : G
⊢ (fun z => z • y = z * y) (↑(of k G) g)
[PROOFSTEP]
show asAlgebraHom (ofMulAction k G G) _ _ = _
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
g : G
⊢ ↑(↑(asAlgebraHom (ofMulAction k G G)) (↑(of k G) g)) y = ↑(of k G) g * y
[PROOFSTEP]
ext
[GOAL]
case h
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
g a✝ : G
⊢ ↑(↑(↑(asAlgebraHom (ofMulAction k G G)) (↑(of k G) g)) y) a✝ = ↑(↑(of k G) g * y) a✝
[PROOFSTEP]
simp only [MonoidAlgebra.of_apply, asAlgebraHom_single, one_smul, ofMulAction_apply, smul_eq_mul]
  -- Porting note : single_mul_apply not firing in simp
[GOAL]
case h
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
g a✝ : G
⊢ ↑y (g⁻¹ * a✝) = ↑(MonoidAlgebra.single g 1 * y) a✝
[PROOFSTEP]
rw [MonoidAlgebra.single_mul_apply, one_mul]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : MonoidAlgebra k G
y✝ : asModule (ofMulAction k G G)
x y : MonoidAlgebra k G
hx : (fun z => z • y✝ = z * y✝) x
hy : (fun z => z • y✝ = z * y✝) y
⊢ (fun z => z • y✝ = z * y✝) (x + y)
[PROOFSTEP]
simp only [hx, hy, add_mul, add_smul]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ (fun z => z • y = z * y) (r • x)
[PROOFSTEP]
show
  asAlgebraHom (ofMulAction k G G) _ _ =
    _
      -- Porting note: was simpa [← hx]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ ↑(↑(asAlgebraHom (ofMulAction k G G)) (r • x)) y = r • x * y
[PROOFSTEP]
simp only [map_smul, smul_apply, Algebra.smul_mul_assoc]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ r • ↑(↑(asAlgebraHom (ofMulAction k G G)) x) y = r • (x * y)
[PROOFSTEP]
rw [← hx]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
x✝ : MonoidAlgebra k G
y : asModule (ofMulAction k G G)
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ r • ↑(↑(asAlgebraHom (ofMulAction k G G)) x) y = r • x • y
[PROOFSTEP]
rfl
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
⊢ ↑(↑(asGroupHom ρ) g) = ↑ρ g
[PROOFSTEP]
simp only [asGroupHom, MonoidHom.coe_toHomUnits]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
⊢ (fun g => map (↑ρV g) (↑ρW g)) 1 = 1
[PROOFSTEP]
simp only [_root_.map_one, TensorProduct.map_one]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
⊢ OneHom.toFun { toFun := fun g => map (↑ρV g) (↑ρW g), map_one' := (_ : map (↑ρV 1) (↑ρW 1) = 1) } (g * h) =
    OneHom.toFun { toFun := fun g => map (↑ρV g) (↑ρW g), map_one' := (_ : map (↑ρV 1) (↑ρW 1) = 1) } g *
      OneHom.toFun { toFun := fun g => map (↑ρV g) (↑ρW g), map_one' := (_ : map (↑ρV 1) (↑ρW 1) = 1) } h
[PROOFSTEP]
simp only [_root_.map_mul, TensorProduct.map_mul]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ let x' := x;
  let z := x ⊗ₜ[k] y;
  r • z = (r • x') ⊗ₜ[k] y
[PROOFSTEP]
show asAlgebraHom (ρV ⊗ 1) _ _ = asAlgebraHom ρV _ _ ⊗ₜ _
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ ↑(↑(asAlgebraHom (ρV ⊗ 1)) r) (x ⊗ₜ[k] y) = ↑(↑(asAlgebraHom ρV) r) x ⊗ₜ[k] y
[PROOFSTEP]
simp only [asAlgebraHom_def, MonoidAlgebra.lift_apply, tprod_apply, MonoidHom.one_apply, LinearMap.finsupp_sum_apply,
  LinearMap.smul_apply, TensorProduct.map_tmul, LinearMap.one_apply]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ (Finsupp.sum r fun i d => d • ↑(↑ρV i) x ⊗ₜ[k] y) = (Finsupp.sum r fun i d => d • ↑(↑ρV i) x) ⊗ₜ[k] y
[PROOFSTEP]
simp only [Finsupp.sum, TensorProduct.sum_tmul]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ (Finset.sum r.support fun x_1 => ↑r x_1 • ↑(↑ρV x_1) x ⊗ₜ[k] y) =
    Finset.sum r.support fun a => (↑r a • ↑(↑ρV a) x) ⊗ₜ[k] y
[PROOFSTEP]
rfl
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ let y' := y;
  let z := x ⊗ₜ[k] y;
  r • z = x ⊗ₜ[k] (r • y')
[PROOFSTEP]
show asAlgebraHom (1 ⊗ ρW) _ _ = _ ⊗ₜ asAlgebraHom ρW _ _
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ ↑(↑(asAlgebraHom (1 ⊗ ρW)) r) (x ⊗ₜ[k] y) = x ⊗ₜ[k] ↑(↑(asAlgebraHom ρW) r) y
[PROOFSTEP]
simp only [asAlgebraHom_def, MonoidAlgebra.lift_apply, tprod_apply, MonoidHom.one_apply, LinearMap.finsupp_sum_apply,
  LinearMap.smul_apply, TensorProduct.map_tmul, LinearMap.one_apply]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
r : MonoidAlgebra k G
x : V
y : W
⊢ (Finsupp.sum r fun i d => d • x ⊗ₜ[k] ↑(↑ρW i) y) = x ⊗ₜ[k] Finsupp.sum r fun i d => d • ↑(↑ρW i) y
[PROOFSTEP]
simp only [Finsupp.sum, TensorProduct.tmul_sum, TensorProduct.tmul_smul]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
f₁ f₂ : V →ₗ[k] W
⊢ (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
    (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ + (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂
[PROOFSTEP]
simp_rw [add_comp, comp_add]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
r : k
f : V →ₗ[k] W
⊢ AddHom.toFun
      { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
        map_add' :=
          (_ :
            ∀ (f₁ f₂ : V →ₗ[k] W),
              (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ + (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
      (r • f) =
    ↑(RingHom.id k) r •
      AddHom.toFun
        { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
          map_add' :=
            (_ :
              ∀ (f₁ f₂ : V →ₗ[k] W),
                (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                  (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ + (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
        f
[PROOFSTEP]
simp_rw [RingHom.id_apply, smul_comp, comp_smul]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
x : V →ₗ[k] W
⊢ ↑((fun g =>
            {
              toAddHom :=
                { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                  map_add' :=
                    (_ :
                      ∀ (f₁ f₂ : V →ₗ[k] W),
                        (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                          (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                            (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) },
              map_smul' :=
                (_ :
                  ∀ (r : k) (f : V →ₗ[k] W),
                    AddHom.toFun
                        { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                          map_add' :=
                            (_ :
                              ∀ (f₁ f₂ : V →ₗ[k] W),
                                (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                  (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                    (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                        (r • f) =
                      ↑(RingHom.id k) r •
                        AddHom.toFun
                          { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                            map_add' :=
                              (_ :
                                ∀ (f₁ f₂ : V →ₗ[k] W),
                                  (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                    (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                      (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                          f) })
          1)
      x =
    ↑1 x
[PROOFSTEP]
dsimp
  -- Porting note: now needed
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
x : V →ₗ[k] W
⊢ comp (↑ρW 1) (comp x (↑ρV 1⁻¹)) = x
[PROOFSTEP]
simp_rw [inv_one, map_one, one_eq_id, comp_id, id_comp]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
x : V →ₗ[k] W
⊢ ↑(OneHom.toFun
          {
            toFun := fun g =>
              {
                toAddHom :=
                  { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                    map_add' :=
                      (_ :
                        ∀ (f₁ f₂ : V →ₗ[k] W),
                          (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                            (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                              (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) },
                map_smul' :=
                  (_ :
                    ∀ (r : k) (f : V →ₗ[k] W),
                      AddHom.toFun
                          { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                            map_add' :=
                              (_ :
                                ∀ (f₁ f₂ : V →ₗ[k] W),
                                  (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                    (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                      (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                          (r • f) =
                        ↑(RingHom.id k) r •
                          AddHom.toFun
                            { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                              map_add' :=
                                (_ :
                                  ∀ (f₁ f₂ : V →ₗ[k] W),
                                    (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                      (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                        (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                            f) },
            map_one' :=
              (_ :
                (fun g =>
                      {
                        toAddHom :=
                          { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                            map_add' :=
                              (_ :
                                ∀ (f₁ f₂ : V →ₗ[k] W),
                                  (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                    (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                      (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) },
                        map_smul' :=
                          (_ :
                            ∀ (r : k) (f : V →ₗ[k] W),
                              AddHom.toFun
                                  { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                                    map_add' :=
                                      (_ :
                                        ∀ (f₁ f₂ : V →ₗ[k] W),
                                          (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                            (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                              (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                                  (r • f) =
                                ↑(RingHom.id k) r •
                                  AddHom.toFun
                                    { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                                      map_add' :=
                                        (_ :
                                          ∀ (f₁ f₂ : V →ₗ[k] W),
                                            (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                              (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                                (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                                    f) })
                    1 =
                  1) }
          (g * h))
      x =
    ↑(OneHom.toFun
            {
              toFun := fun g =>
                {
                  toAddHom :=
                    { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                      map_add' :=
                        (_ :
                          ∀ (f₁ f₂ : V →ₗ[k] W),
                            (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                              (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) },
                  map_smul' :=
                    (_ :
                      ∀ (r : k) (f : V →ₗ[k] W),
                        AddHom.toFun
                            { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                              map_add' :=
                                (_ :
                                  ∀ (f₁ f₂ : V →ₗ[k] W),
                                    (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                      (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                        (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                            (r • f) =
                          ↑(RingHom.id k) r •
                            AddHom.toFun
                              { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                                map_add' :=
                                  (_ :
                                    ∀ (f₁ f₂ : V →ₗ[k] W),
                                      (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                        (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                          (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                              f) },
              map_one' :=
                (_ :
                  (fun g =>
                        {
                          toAddHom :=
                            { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                              map_add' :=
                                (_ :
                                  ∀ (f₁ f₂ : V →ₗ[k] W),
                                    (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                      (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                        (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) },
                          map_smul' :=
                            (_ :
                              ∀ (r : k) (f : V →ₗ[k] W),
                                AddHom.toFun
                                    { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                                      map_add' :=
                                        (_ :
                                          ∀ (f₁ f₂ : V →ₗ[k] W),
                                            (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                              (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                                (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                                    (r • f) =
                                  ↑(RingHom.id k) r •
                                    AddHom.toFun
                                      { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                                        map_add' :=
                                          (_ :
                                            ∀ (f₁ f₂ : V →ₗ[k] W),
                                              (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                                (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                                  (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                                      f) })
                      1 =
                    1) }
            g *
          OneHom.toFun
            {
              toFun := fun g =>
                {
                  toAddHom :=
                    { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                      map_add' :=
                        (_ :
                          ∀ (f₁ f₂ : V →ₗ[k] W),
                            (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                              (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) },
                  map_smul' :=
                    (_ :
                      ∀ (r : k) (f : V →ₗ[k] W),
                        AddHom.toFun
                            { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                              map_add' :=
                                (_ :
                                  ∀ (f₁ f₂ : V →ₗ[k] W),
                                    (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                      (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                        (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                            (r • f) =
                          ↑(RingHom.id k) r •
                            AddHom.toFun
                              { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                                map_add' :=
                                  (_ :
                                    ∀ (f₁ f₂ : V →ₗ[k] W),
                                      (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                        (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                          (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                              f) },
              map_one' :=
                (_ :
                  (fun g =>
                        {
                          toAddHom :=
                            { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                              map_add' :=
                                (_ :
                                  ∀ (f₁ f₂ : V →ₗ[k] W),
                                    (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                      (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                        (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) },
                          map_smul' :=
                            (_ :
                              ∀ (r : k) (f : V →ₗ[k] W),
                                AddHom.toFun
                                    { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                                      map_add' :=
                                        (_ :
                                          ∀ (f₁ f₂ : V →ₗ[k] W),
                                            (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                              (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                                (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                                    (r • f) =
                                  ↑(RingHom.id k) r •
                                    AddHom.toFun
                                      { toFun := fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹)),
                                        map_add' :=
                                          (_ :
                                            ∀ (f₁ f₂ : V →ₗ[k] W),
                                              (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) (f₁ + f₂) =
                                                (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₁ +
                                                  (fun f => comp (↑ρW g) (comp f (↑ρV g⁻¹))) f₂) }
                                      f) })
                      1 =
                    1) }
            h)
      x
[PROOFSTEP]
dsimp
  -- Porting note: now needed
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
x : V →ₗ[k] W
⊢ comp (↑ρW (g * h)) (comp x (↑ρV (g * h)⁻¹)) = comp (↑ρW g) (comp (comp (↑ρW h) (comp x (↑ρV h⁻¹))) (↑ρV g⁻¹))
[PROOFSTEP]
simp_rw [mul_inv_rev, map_mul, mul_eq_comp, comp_assoc]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
f₁ f₂ : Module.Dual k V
⊢ (fun f => comp f (↑ρV g⁻¹)) (f₁ + f₂) = (fun f => comp f (↑ρV g⁻¹)) f₁ + (fun f => comp f (↑ρV g⁻¹)) f₂
[PROOFSTEP]
simp only [add_comp]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
r : k
f : Module.Dual k V
⊢ AddHom.toFun
      { toFun := fun f => comp f (↑ρV g⁻¹),
        map_add' :=
          (_ :
            ∀ (f₁ f₂ : Module.Dual k V),
              comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
      (r • f) =
    ↑(RingHom.id k) r •
      AddHom.toFun
        { toFun := fun f => comp f (↑ρV g⁻¹),
          map_add' :=
            (_ :
              ∀ (f₁ f₂ : Module.Dual k V),
                comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
        f
[PROOFSTEP]
ext
[GOAL]
case h
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
r : k
f : Module.Dual k V
x✝ : V
⊢ ↑(AddHom.toFun
          { toFun := fun f => comp f (↑ρV g⁻¹),
            map_add' :=
              (_ :
                ∀ (f₁ f₂ : Module.Dual k V),
                  comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
          (r • f))
      x✝ =
    ↑(↑(RingHom.id k) r •
          AddHom.toFun
            { toFun := fun f => comp f (↑ρV g⁻¹),
              map_add' :=
                (_ :
                  ∀ (f₁ f₂ : Module.Dual k V),
                    comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
            f)
      x✝
[PROOFSTEP]
simp only [coe_comp, Function.comp_apply, smul_apply, RingHom.id_apply]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
⊢ (fun g =>
        {
          toAddHom :=
            { toFun := fun f => comp f (↑ρV g⁻¹),
              map_add' :=
                (_ :
                  ∀ (f₁ f₂ : Module.Dual k V),
                    comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
          map_smul' :=
            (_ :
              ∀ (r : k) (f : Module.Dual k V),
                AddHom.toFun
                    { toFun := fun f => comp f (↑ρV g⁻¹),
                      map_add' :=
                        (_ :
                          ∀ (f₁ f₂ : Module.Dual k V),
                            comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                    (r • f) =
                  ↑(RingHom.id k) r •
                    AddHom.toFun
                      { toFun := fun f => comp f (↑ρV g⁻¹),
                        map_add' :=
                          (_ :
                            ∀ (f₁ f₂ : Module.Dual k V),
                              comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                      f) })
      1 =
    1
[PROOFSTEP]
ext
[GOAL]
case h.h
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
x✝¹ : Module.Dual k V
x✝ : V
⊢ ↑(↑((fun g =>
                {
                  toAddHom :=
                    { toFun := fun f => comp f (↑ρV g⁻¹),
                      map_add' :=
                        (_ :
                          ∀ (f₁ f₂ : Module.Dual k V),
                            comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
                  map_smul' :=
                    (_ :
                      ∀ (r : k) (f : Module.Dual k V),
                        AddHom.toFun
                            { toFun := fun f => comp f (↑ρV g⁻¹),
                              map_add' :=
                                (_ :
                                  ∀ (f₁ f₂ : Module.Dual k V),
                                    comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                            (r • f) =
                          ↑(RingHom.id k) r •
                            AddHom.toFun
                              { toFun := fun f => comp f (↑ρV g⁻¹),
                                map_add' :=
                                  (_ :
                                    ∀ (f₁ f₂ : Module.Dual k V),
                                      comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                              f) })
              1)
          x✝¹)
      x✝ =
    ↑(↑1 x✝¹) x✝
[PROOFSTEP]
dsimp
  -- Porting note: now needed
[GOAL]
case h.h
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
x✝¹ : Module.Dual k V
x✝ : V
⊢ ↑x✝¹ (↑(↑ρV 1⁻¹) x✝) = ↑x✝¹ x✝
[PROOFSTEP]
simp only [coe_comp, Function.comp_apply, map_one, inv_one, coe_mk, one_apply]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
⊢ OneHom.toFun
      {
        toFun := fun g =>
          {
            toAddHom :=
              { toFun := fun f => comp f (↑ρV g⁻¹),
                map_add' :=
                  (_ :
                    ∀ (f₁ f₂ : Module.Dual k V),
                      comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
            map_smul' :=
              (_ :
                ∀ (r : k) (f : Module.Dual k V),
                  AddHom.toFun
                      { toFun := fun f => comp f (↑ρV g⁻¹),
                        map_add' :=
                          (_ :
                            ∀ (f₁ f₂ : Module.Dual k V),
                              comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                      (r • f) =
                    ↑(RingHom.id k) r •
                      AddHom.toFun
                        { toFun := fun f => comp f (↑ρV g⁻¹),
                          map_add' :=
                            (_ :
                              ∀ (f₁ f₂ : Module.Dual k V),
                                comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                        f) },
        map_one' :=
          (_ :
            (fun g =>
                  {
                    toAddHom :=
                      { toFun := fun f => comp f (↑ρV g⁻¹),
                        map_add' :=
                          (_ :
                            ∀ (f₁ f₂ : Module.Dual k V),
                              comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
                    map_smul' :=
                      (_ :
                        ∀ (r : k) (f : Module.Dual k V),
                          AddHom.toFun
                              { toFun := fun f => comp f (↑ρV g⁻¹),
                                map_add' :=
                                  (_ :
                                    ∀ (f₁ f₂ : Module.Dual k V),
                                      comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                              (r • f) =
                            ↑(RingHom.id k) r •
                              AddHom.toFun
                                { toFun := fun f => comp f (↑ρV g⁻¹),
                                  map_add' :=
                                    (_ :
                                      ∀ (f₁ f₂ : Module.Dual k V),
                                        comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                f) })
                1 =
              1) }
      (g * h) =
    OneHom.toFun
        {
          toFun := fun g =>
            {
              toAddHom :=
                { toFun := fun f => comp f (↑ρV g⁻¹),
                  map_add' :=
                    (_ :
                      ∀ (f₁ f₂ : Module.Dual k V),
                        comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
              map_smul' :=
                (_ :
                  ∀ (r : k) (f : Module.Dual k V),
                    AddHom.toFun
                        { toFun := fun f => comp f (↑ρV g⁻¹),
                          map_add' :=
                            (_ :
                              ∀ (f₁ f₂ : Module.Dual k V),
                                comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                        (r • f) =
                      ↑(RingHom.id k) r •
                        AddHom.toFun
                          { toFun := fun f => comp f (↑ρV g⁻¹),
                            map_add' :=
                              (_ :
                                ∀ (f₁ f₂ : Module.Dual k V),
                                  comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                          f) },
          map_one' :=
            (_ :
              (fun g =>
                    {
                      toAddHom :=
                        { toFun := fun f => comp f (↑ρV g⁻¹),
                          map_add' :=
                            (_ :
                              ∀ (f₁ f₂ : Module.Dual k V),
                                comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
                      map_smul' :=
                        (_ :
                          ∀ (r : k) (f : Module.Dual k V),
                            AddHom.toFun
                                { toFun := fun f => comp f (↑ρV g⁻¹),
                                  map_add' :=
                                    (_ :
                                      ∀ (f₁ f₂ : Module.Dual k V),
                                        comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                (r • f) =
                              ↑(RingHom.id k) r •
                                AddHom.toFun
                                  { toFun := fun f => comp f (↑ρV g⁻¹),
                                    map_add' :=
                                      (_ :
                                        ∀ (f₁ f₂ : Module.Dual k V),
                                          comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) =
                                            comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                  f) })
                  1 =
                1) }
        g *
      OneHom.toFun
        {
          toFun := fun g =>
            {
              toAddHom :=
                { toFun := fun f => comp f (↑ρV g⁻¹),
                  map_add' :=
                    (_ :
                      ∀ (f₁ f₂ : Module.Dual k V),
                        comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
              map_smul' :=
                (_ :
                  ∀ (r : k) (f : Module.Dual k V),
                    AddHom.toFun
                        { toFun := fun f => comp f (↑ρV g⁻¹),
                          map_add' :=
                            (_ :
                              ∀ (f₁ f₂ : Module.Dual k V),
                                comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                        (r • f) =
                      ↑(RingHom.id k) r •
                        AddHom.toFun
                          { toFun := fun f => comp f (↑ρV g⁻¹),
                            map_add' :=
                              (_ :
                                ∀ (f₁ f₂ : Module.Dual k V),
                                  comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                          f) },
          map_one' :=
            (_ :
              (fun g =>
                    {
                      toAddHom :=
                        { toFun := fun f => comp f (↑ρV g⁻¹),
                          map_add' :=
                            (_ :
                              ∀ (f₁ f₂ : Module.Dual k V),
                                comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
                      map_smul' :=
                        (_ :
                          ∀ (r : k) (f : Module.Dual k V),
                            AddHom.toFun
                                { toFun := fun f => comp f (↑ρV g⁻¹),
                                  map_add' :=
                                    (_ :
                                      ∀ (f₁ f₂ : Module.Dual k V),
                                        comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                (r • f) =
                              ↑(RingHom.id k) r •
                                AddHom.toFun
                                  { toFun := fun f => comp f (↑ρV g⁻¹),
                                    map_add' :=
                                      (_ :
                                        ∀ (f₁ f₂ : Module.Dual k V),
                                          comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) =
                                            comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                  f) })
                  1 =
                1) }
        h
[PROOFSTEP]
ext
[GOAL]
case h.h
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
x✝¹ : Module.Dual k V
x✝ : V
⊢ ↑(↑(OneHom.toFun
              {
                toFun := fun g =>
                  {
                    toAddHom :=
                      { toFun := fun f => comp f (↑ρV g⁻¹),
                        map_add' :=
                          (_ :
                            ∀ (f₁ f₂ : Module.Dual k V),
                              comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
                    map_smul' :=
                      (_ :
                        ∀ (r : k) (f : Module.Dual k V),
                          AddHom.toFun
                              { toFun := fun f => comp f (↑ρV g⁻¹),
                                map_add' :=
                                  (_ :
                                    ∀ (f₁ f₂ : Module.Dual k V),
                                      comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                              (r • f) =
                            ↑(RingHom.id k) r •
                              AddHom.toFun
                                { toFun := fun f => comp f (↑ρV g⁻¹),
                                  map_add' :=
                                    (_ :
                                      ∀ (f₁ f₂ : Module.Dual k V),
                                        comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                f) },
                map_one' :=
                  (_ :
                    (fun g =>
                          {
                            toAddHom :=
                              { toFun := fun f => comp f (↑ρV g⁻¹),
                                map_add' :=
                                  (_ :
                                    ∀ (f₁ f₂ : Module.Dual k V),
                                      comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
                            map_smul' :=
                              (_ :
                                ∀ (r : k) (f : Module.Dual k V),
                                  AddHom.toFun
                                      { toFun := fun f => comp f (↑ρV g⁻¹),
                                        map_add' :=
                                          (_ :
                                            ∀ (f₁ f₂ : Module.Dual k V),
                                              comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) =
                                                comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                      (r • f) =
                                    ↑(RingHom.id k) r •
                                      AddHom.toFun
                                        { toFun := fun f => comp f (↑ρV g⁻¹),
                                          map_add' :=
                                            (_ :
                                              ∀ (f₁ f₂ : Module.Dual k V),
                                                comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) =
                                                  comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                        f) })
                        1 =
                      1) }
              (g * h))
          x✝¹)
      x✝ =
    ↑(↑(OneHom.toFun
                {
                  toFun := fun g =>
                    {
                      toAddHom :=
                        { toFun := fun f => comp f (↑ρV g⁻¹),
                          map_add' :=
                            (_ :
                              ∀ (f₁ f₂ : Module.Dual k V),
                                comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
                      map_smul' :=
                        (_ :
                          ∀ (r : k) (f : Module.Dual k V),
                            AddHom.toFun
                                { toFun := fun f => comp f (↑ρV g⁻¹),
                                  map_add' :=
                                    (_ :
                                      ∀ (f₁ f₂ : Module.Dual k V),
                                        comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                (r • f) =
                              ↑(RingHom.id k) r •
                                AddHom.toFun
                                  { toFun := fun f => comp f (↑ρV g⁻¹),
                                    map_add' :=
                                      (_ :
                                        ∀ (f₁ f₂ : Module.Dual k V),
                                          comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) =
                                            comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                  f) },
                  map_one' :=
                    (_ :
                      (fun g =>
                            {
                              toAddHom :=
                                { toFun := fun f => comp f (↑ρV g⁻¹),
                                  map_add' :=
                                    (_ :
                                      ∀ (f₁ f₂ : Module.Dual k V),
                                        comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) =
                                          comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
                              map_smul' :=
                                (_ :
                                  ∀ (r : k) (f : Module.Dual k V),
                                    AddHom.toFun
                                        { toFun := fun f => comp f (↑ρV g⁻¹),
                                          map_add' :=
                                            (_ :
                                              ∀ (f₁ f₂ : Module.Dual k V),
                                                comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) =
                                                  comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                        (r • f) =
                                      ↑(RingHom.id k) r •
                                        AddHom.toFun
                                          { toFun := fun f => comp f (↑ρV g⁻¹),
                                            map_add' :=
                                              (_ :
                                                ∀ (f₁ f₂ : Module.Dual k V),
                                                  comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) =
                                                    comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                          f) })
                          1 =
                        1) }
                g *
              OneHom.toFun
                {
                  toFun := fun g =>
                    {
                      toAddHom :=
                        { toFun := fun f => comp f (↑ρV g⁻¹),
                          map_add' :=
                            (_ :
                              ∀ (f₁ f₂ : Module.Dual k V),
                                comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
                      map_smul' :=
                        (_ :
                          ∀ (r : k) (f : Module.Dual k V),
                            AddHom.toFun
                                { toFun := fun f => comp f (↑ρV g⁻¹),
                                  map_add' :=
                                    (_ :
                                      ∀ (f₁ f₂ : Module.Dual k V),
                                        comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) = comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                (r • f) =
                              ↑(RingHom.id k) r •
                                AddHom.toFun
                                  { toFun := fun f => comp f (↑ρV g⁻¹),
                                    map_add' :=
                                      (_ :
                                        ∀ (f₁ f₂ : Module.Dual k V),
                                          comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) =
                                            comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                  f) },
                  map_one' :=
                    (_ :
                      (fun g =>
                            {
                              toAddHom :=
                                { toFun := fun f => comp f (↑ρV g⁻¹),
                                  map_add' :=
                                    (_ :
                                      ∀ (f₁ f₂ : Module.Dual k V),
                                        comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) =
                                          comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) },
                              map_smul' :=
                                (_ :
                                  ∀ (r : k) (f : Module.Dual k V),
                                    AddHom.toFun
                                        { toFun := fun f => comp f (↑ρV g⁻¹),
                                          map_add' :=
                                            (_ :
                                              ∀ (f₁ f₂ : Module.Dual k V),
                                                comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) =
                                                  comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                        (r • f) =
                                      ↑(RingHom.id k) r •
                                        AddHom.toFun
                                          { toFun := fun f => comp f (↑ρV g⁻¹),
                                            map_add' :=
                                              (_ :
                                                ∀ (f₁ f₂ : Module.Dual k V),
                                                  comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹) =
                                                    comp f₁ (↑ρV g⁻¹) + comp f₂ (↑ρV g⁻¹)) }
                                          f) })
                          1 =
                        1) }
                h)
          x✝¹)
      x✝
[PROOFSTEP]
dsimp
  -- Porting note: now needed
[GOAL]
case h.h
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g h : G
x✝¹ : Module.Dual k V
x✝ : V
⊢ ↑x✝¹ (↑(↑ρV (g * h)⁻¹) x✝) = ↑x✝¹ (↑(↑ρV h⁻¹) (↑(↑ρV g⁻¹) x✝))
[PROOFSTEP]
simp only [coe_comp, Function.comp_apply, mul_inv_rev, map_mul, coe_mk, mul_apply]
[GOAL]
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
⊢ comp (dualTensorHom k V W) (TensorProduct.map (↑(dual ρV) g) (↑ρW g)) = comp (↑(linHom ρV ρW) g) (dualTensorHom k V W)
[PROOFSTEP]
ext
[GOAL]
case a.h.h.h
k : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : CommSemiring k
inst✝⁴ : Group G
inst✝³ : AddCommMonoid V
inst✝² : Module k V
inst✝¹ : AddCommMonoid W
inst✝ : Module k W
ρV : Representation k G V
ρW : Representation k G W
g : G
x✝² : Module.Dual k V
x✝¹ : W
x✝ : V
⊢ ↑(↑(↑(TensorProduct.AlgebraTensorModule.curry (comp (dualTensorHom k V W) (TensorProduct.map (↑(dual ρV) g) (↑ρW g))))
              x✝²)
          x✝¹)
      x✝ =
    ↑(↑(↑(TensorProduct.AlgebraTensorModule.curry (comp (↑(linHom ρV ρW) g) (dualTensorHom k V W))) x✝²) x✝¹) x✝
[PROOFSTEP]
simp [Module.Dual.transpose_apply]
