[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ Linear k (Rep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ AddCommGroup (CoeSort.coe V)
[PROOFSTEP]
change AddCommGroup ((forget₂ (Rep k G) (ModuleCat k)).obj V)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ AddCommGroup ↑((forget₂ (Rep k G) (ModuleCat k)).obj V)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ Module k (CoeSort.coe V)
[PROOFSTEP]
change Module k ((forget₂ (Rep k G) (ModuleCat k)).obj V)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ Module k ↑((forget₂ (Rep k G) (ModuleCat k)).obj V)
[PROOFSTEP]
infer_instance
[GOAL]
k G✝ : Type u
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Group G
A : Rep k G
g : G
x : CoeSort.coe A
⊢ ↑(↑(ρ A) g⁻¹ * ↑(ρ A) g) x = x
[PROOFSTEP]
rw [← map_mul, inv_mul_self, map_one, LinearMap.one_apply]
[GOAL]
k G✝ : Type u
inst✝² : CommRing k
inst✝¹ : Monoid G✝
G : Type u
inst✝ : Group G
A : Rep k G
g : G
x : CoeSort.coe A
⊢ ↑(↑(ρ A) g * ↑(ρ A) g⁻¹) x = x
[PROOFSTEP]
rw [← map_mul, mul_inv_self, map_one, LinearMap.one_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X : Action (Type u) (MonCat.of G)
g : G
x : X.V
⊢ ↑(↑(ρ ((linearization k G).toLaxMonoidalFunctor.toFunctor.obj X)) g) (Finsupp.single x 1) =
    Finsupp.single (↑X.ρ g x) 1
[PROOFSTEP]
rw [linearization_obj_ρ, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X : Action (Type u) (MonCat.of G)
g : G
x : X.V
r : k
⊢ ↑(↑(ρ ((linearization k G).toLaxMonoidalFunctor.toFunctor.obj X)) g) (Finsupp.single x r) =
    Finsupp.single (↑X.ρ g x) r
[PROOFSTEP]
rw [linearization_obj_ρ, Finsupp.lmapDomain_apply, Finsupp.mapDomain_single]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Action (Type u) (MonCat.of G)
f : X✝ ⟶ Y✝
X Y : Action (Type u) (MonCat.of G)
⊢ (inv (LaxMonoidalFunctor.μ (linearization k G).toLaxMonoidalFunctor X Y)).hom =
    ↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V))
[PROOFSTEP]
rw [← Action.forget_map, Functor.map_inv]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Action (Type u) (MonCat.of G)
f : X✝ ⟶ Y✝
X Y : Action (Type u) (MonCat.of G)
⊢ inv
      ((Action.forget (ModuleCat k) (MonCat.of G)).map
        (LaxMonoidalFunctor.μ (linearization k G).toLaxMonoidalFunctor X Y)) =
    ↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V))
[PROOFSTEP]
apply IsIso.inv_eq_of_hom_inv_id
[GOAL]
case hom_inv_id
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Action (Type u) (MonCat.of G)
f : X✝ ⟶ Y✝
X Y : Action (Type u) (MonCat.of G)
⊢ (Action.forget (ModuleCat k) (MonCat.of G)).map (LaxMonoidalFunctor.μ (linearization k G).toLaxMonoidalFunctor X Y) ≫
      ↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) =
    𝟙
      ((Action.forget (ModuleCat k) (MonCat.of G)).obj
        (MonoidalCategory.tensorObj ((linearization k G).toLaxMonoidalFunctor.toFunctor.obj X)
          ((linearization k G).toLaxMonoidalFunctor.toFunctor.obj Y)))
[PROOFSTEP]
exact LinearMap.ext fun x => LinearEquiv.symm_apply_apply (finsuppTensorFinsupp' k X.V Y.V) x
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : ↑(MonCat.of G)
⊢ (↑(ofMulAction k G G).ρ g ≫ ↑(Finsupp.lift ((fun x => CoeSort.coe A) x) k G) fun g => ↑(↑(ρ A) g) x) =
    (↑(Finsupp.lift ((fun x => CoeSort.coe A) x) k G) fun g => ↑(↑(ρ A) g) x) ≫ ↑A.ρ g
[PROOFSTEP]
refine'
  Finsupp.lhom_ext' fun y =>
    LinearMap.ext_ring
      _
        /- Porting note: rest of broken proof was
            simpa only [LinearMap.comp_apply, ModuleCat.comp_def, Finsupp.lsingle_apply, Finsupp.lift_apply,
              Action_ρ_eq_ρ, of_ρ_apply, Representation.ofMulAction_single, Finsupp.sum_single_index,
              zero_smul, one_smul, smul_eq_mul, A.ρ.map_mul] -/
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : ↑(MonCat.of G)
y : G
⊢ ↑(LinearMap.comp (↑(ofMulAction k G G).ρ g ≫ ↑(Finsupp.lift ((fun x => CoeSort.coe A) x) k G) fun g => ↑(↑(ρ A) g) x)
          (Finsupp.lsingle y))
      1 =
    ↑(LinearMap.comp ((↑(Finsupp.lift ((fun x => CoeSort.coe A) x) k G) fun g => ↑(↑(ρ A) g) x) ≫ ↑A.ρ g)
          (Finsupp.lsingle y))
      1
[PROOFSTEP]
simp only [LinearMap.comp_apply, ModuleCat.comp_def, Finsupp.lsingle_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : ↑(MonCat.of G)
y : G
⊢ ↑(↑(Finsupp.lift (CoeSort.coe A) k G) fun g => ↑(↑(ρ A) g) x) (↑(↑(ofMulAction k G G).ρ g) (Finsupp.single y 1)) =
    ↑(↑A.ρ g) (↑(↑(Finsupp.lift (CoeSort.coe A) k G) fun g => ↑(↑(ρ A) g) x) (Finsupp.single y 1))
[PROOFSTEP]
erw [Finsupp.lift_apply, Finsupp.lift_apply, Representation.ofMulAction_single (G := G)]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : ↑(MonCat.of G)
y : G
⊢ (Finsupp.sum (Finsupp.single (g • y) 1) fun x_1 r => r • ↑(↑(ρ A) x_1) x) =
    ↑(↑A.ρ g) (Finsupp.sum (Finsupp.single y 1) fun x_1 r => r • ↑(↑(ρ A) x_1) x)
[PROOFSTEP]
simp only [Finsupp.sum_single_index, zero_smul, one_smul, smul_eq_mul, A.ρ.map_mul, of_ρ]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : ↑(MonCat.of G)
y : G
⊢ ↑(↑(ρ A) g * ↑(ρ A) y) x = ↑(↑A.ρ g) (↑(↑(ρ A) y) x)
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
⊢ ↑(leftRegularHom A x).hom (Finsupp.single 1 1) = x
[PROOFSTEP]
rw [leftRegularHom_hom, Finsupp.lift_apply, Finsupp.sum_single_index, one_smul, A.ρ.map_one, LinearMap.one_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
⊢ 0 • ↑(↑(ρ A) 1) x = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
⊢ (fun x => leftRegularHom A x)
      (AddHom.toFun
        {
            toAddHom :=
              { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                map_add' :=
                  (_ :
                    ∀ (x y : ofMulAction k G G ⟶ A),
                      (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                        (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) },
            map_smul' :=
              (_ :
                ∀ (r : k) (x : ofMulAction k G G ⟶ A),
                  AddHom.toFun
                      { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                        map_add' :=
                          (_ :
                            ∀ (x y : ofMulAction k G G ⟶ A),
                              (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) }
                      (r • x) =
                    AddHom.toFun
                      { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                        map_add' :=
                          (_ :
                            ∀ (x y : ofMulAction k G G ⟶ A),
                              (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) }
                      (r • x)) }.toAddHom
        f) =
    f
[PROOFSTEP]
refine' Action.Hom.ext _ _ (Finsupp.lhom_ext' fun x : G => LinearMap.ext_ring _)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
⊢ ↑(LinearMap.comp
          ((fun x => leftRegularHom A x)
              (AddHom.toFun
                {
                    toAddHom :=
                      { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                        map_add' :=
                          (_ :
                            ∀ (x y : ofMulAction k G G ⟶ A),
                              (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) },
                    map_smul' :=
                      (_ :
                        ∀ (r : k) (x : ofMulAction k G G ⟶ A),
                          AddHom.toFun
                              { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ofMulAction k G G ⟶ A),
                                      (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                        (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) }
                              (r • x) =
                            AddHom.toFun
                              { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ofMulAction k G G ⟶ A),
                                      (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                        (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) }
                              (r • x)) }.toAddHom
                f)).hom
          (Finsupp.lsingle x))
      1 =
    ↑(LinearMap.comp f.hom (Finsupp.lsingle x)) 1
[PROOFSTEP]
have :
  f.hom ((ofMulAction k G G).ρ x (Finsupp.single (1 : G) (1 : k))) = A.ρ x (f.hom (Finsupp.single (1 : G) (1 : k))) :=
  LinearMap.ext_iff.1 (f.comm x)
    (Finsupp.single 1 1)
      /- Porting note: rest of broken proof was
          simp only [LinearMap.comp_apply, Finsupp.lsingle_apply, left_regular_hom_hom,
            Finsupp.lift_apply, Finsupp.sum_single_index, one_smul, ← this, zero_smul, of_ρ_apply,
            Representation.ofMulAction_single x (1 : G) (1 : k), smul_eq_mul, mul_one] -/
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ ↑(LinearMap.comp
          ((fun x => leftRegularHom A x)
              (AddHom.toFun
                {
                    toAddHom :=
                      { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                        map_add' :=
                          (_ :
                            ∀ (x y : ofMulAction k G G ⟶ A),
                              (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) },
                    map_smul' :=
                      (_ :
                        ∀ (r : k) (x : ofMulAction k G G ⟶ A),
                          AddHom.toFun
                              { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ofMulAction k G G ⟶ A),
                                      (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                        (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) }
                              (r • x) =
                            AddHom.toFun
                              { toFun := fun f => ↑f.hom (Finsupp.single 1 1),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : ofMulAction k G G ⟶ A),
                                      (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y) =
                                        (fun f => ↑f.hom (Finsupp.single 1 1)) (x + y)) }
                              (r • x)) }.toAddHom
                f)).hom
          (Finsupp.lsingle x))
      1 =
    ↑(LinearMap.comp f.hom (Finsupp.lsingle x)) 1
[PROOFSTEP]
simp only [LinearMap.comp_apply, Finsupp.lsingle_apply, leftRegularHom_hom]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ ↑(↑(Finsupp.lift (CoeSort.coe A) k G) fun g => ↑(↑(ρ A) g) (↑f.hom (Finsupp.single 1 1))) (Finsupp.single x 1) =
    ↑f.hom (Finsupp.single x 1)
[PROOFSTEP]
erw [Finsupp.lift_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ (Finsupp.sum (Finsupp.single x 1) fun x r => r • ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))) =
    ↑f.hom (Finsupp.single x 1)
[PROOFSTEP]
rw [Finsupp.sum_single_index, ← this, of_ρ_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ 1 • ↑f.hom (↑(↑(Representation.ofMulAction k G G) x) (Finsupp.single 1 1)) = ↑f.hom (Finsupp.single x 1)
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ 0 • ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1)) = 0
[PROOFSTEP]
erw [Representation.ofMulAction_single x (1 : G) (1 : k)]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ 1 • ↑f.hom (Finsupp.single (x • 1) 1) = ↑f.hom (Finsupp.single x 1)
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ 0 • ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1)) = 0
[PROOFSTEP]
simp only [one_smul, smul_eq_mul, mul_one]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f✝ : X ⟶ Y
A : Rep k G
f : ofMulAction k G G ⟶ A
x : G
this : ↑f.hom (↑(↑(ρ (ofMulAction k G G)) x) (Finsupp.single 1 1)) = ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1))
⊢ 0 • ↑(↑(ρ A) x) (↑f.hom (Finsupp.single 1 1)) = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : G
⊢ ↑(↑(LinearEquiv.symm (leftRegularHomEquiv A)) x).hom (Finsupp.single g 1) = ↑(↑(ρ A) g) x
[PROOFSTEP]
rw [leftRegularHomEquiv_symm_apply, leftRegularHom_hom, Finsupp.lift_apply, Finsupp.sum_single_index, one_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X Y : Action (Type u) (MonCat.of G)
f : X ⟶ Y
A : Rep k G
x : CoeSort.coe A
g : G
⊢ 0 • ↑(↑(ρ A) g) x = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A X Y : Rep k G
f : X ⟶ Y
g : ↑(MonCat.of G)
x : ↑((fun B => of (Representation.linHom (ρ A) (ρ B))) X).V
y : CoeSort.coe A
⊢ ↑(↑(↑((fun B => of (Representation.linHom (ρ A) (ρ B))) X).ρ g ≫
              ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom))
          x)
      y =
    ↑(↑(ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom) ≫
              ↑((fun B => of (Representation.linHom (ρ A) (ρ B))) Y).ρ g)
          x)
      y
[PROOFSTEP]
show f.hom (X.ρ g _) = _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A X Y : Rep k G
f : X ⟶ Y
g : ↑(MonCat.of G)
x : ↑((fun B => of (Representation.linHom (ρ A) (ρ B))) X).V
y : CoeSort.coe A
⊢ ↑f.hom (↑(↑(ρ X) g) (↑(LinearMap.comp x (↑(ρ A) g⁻¹)) y)) =
    ↑(↑(ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom) ≫
              ↑((fun B => of (Representation.linHom (ρ A) (ρ B))) Y).ρ g)
          x)
      y
[PROOFSTEP]
simp only [hom_comm_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A X Y : Rep k G
f : X ⟶ Y
g : ↑(MonCat.of G)
x : ↑((fun B => of (Representation.linHom (ρ A) (ρ B))) X).V
y : CoeSort.coe A
⊢ ↑(↑(ρ Y) g) (↑f.hom (↑(LinearMap.comp x (↑(ρ A) g⁻¹)) y)) =
    ↑(↑(ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom) ≫
              ↑(of (Representation.linHom (ρ A) (ρ Y))).ρ g)
          x)
      y
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A x✝ : Rep k G
⊢ { obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
          map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
      (𝟙 x✝) =
    𝟙
      ({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
            map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.obj
        x✝)
[PROOFSTEP]
ext
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A x✝¹ : Rep k G
x✝ :
  ↑({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
            map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.obj
        x✝¹).V
⊢ ↑({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
                map := fun {X Y} f =>
                  Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
            (𝟙 x✝¹)).hom
      x✝ =
    ↑(𝟙
            ({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
                  map := fun {X Y} f =>
                    Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.obj
              x✝¹)).hom
      x✝
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A X✝ Y✝ Z✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ { obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
          map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
      (x✝¹ ≫ x✝) =
    { obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
            map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
        x✝¹ ≫
      { obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
            map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
        x✝
[PROOFSTEP]
ext
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B C A X✝ Y✝ Z✝ : Rep k G
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ :
  ↑({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
            map := fun {X Y} f => Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.obj
        X✝).V
⊢ ↑({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
                map := fun {X Y} f =>
                  Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
            (x✝² ≫ x✝¹)).hom
      x✝ =
    ↑({ obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
                  map := fun {X Y} f =>
                    Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
              x✝² ≫
            { obj := fun B => of (Representation.linHom (ρ A) (ρ B)),
                  map := fun {X Y} f =>
                    Hom.mk (ModuleCat.ofHom (↑(LinearMap.llcomp k (CoeSort.coe A) ↑X.V ↑Y.V) f.hom)) }.map
              x✝¹).hom
      x✝
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : A ⊗ B ⟶ C
g : ↑(MonCat.of G)
⊢ ↑B.ρ g ≫ LinearMap.flip (TensorProduct.curry f.hom) =
    LinearMap.flip (TensorProduct.curry f.hom) ≫ ↑((Rep.ihom A).obj C).ρ g
[PROOFSTEP]
refine' LinearMap.ext fun x => LinearMap.ext fun y => _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : A ⊗ B ⟶ C
g : ↑(MonCat.of G)
x : ↑B.V
y : CoeSort.coe A
⊢ ↑(↑(↑B.ρ g ≫ LinearMap.flip (TensorProduct.curry f.hom)) x) y =
    ↑(↑(LinearMap.flip (TensorProduct.curry f.hom) ≫ ↑((Rep.ihom A).obj C).ρ g) x) y
[PROOFSTEP]
change f.hom (_ ⊗ₜ[k] _) = C.ρ g (f.hom (_ ⊗ₜ[k] _))
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : A ⊗ B ⟶ C
g : ↑(MonCat.of G)
x : ↑B.V
y : CoeSort.coe A
⊢ ↑f.hom (y ⊗ₜ[k] ↑(↑B.ρ g) x) = ↑(↑(ρ C) g) (↑f.hom (↑(↑(ρ A) g⁻¹) y ⊗ₜ[k] x))
[PROOFSTEP]
rw [← hom_comm_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : A ⊗ B ⟶ C
g : ↑(MonCat.of G)
x : ↑B.V
y : CoeSort.coe A
⊢ ↑f.hom (y ⊗ₜ[k] ↑(↑B.ρ g) x) = ↑f.hom (↑(↑(ρ (A ⊗ B)) g) (↑(↑(ρ A) g⁻¹) y ⊗ₜ[k] x))
[PROOFSTEP]
change _ = f.hom ((A.ρ g * A.ρ g⁻¹) y ⊗ₜ[k] _)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : A ⊗ B ⟶ C
g : ↑(MonCat.of G)
x : ↑B.V
y : CoeSort.coe A
⊢ ↑f.hom (y ⊗ₜ[k] ↑(↑B.ρ g) x) =
    ↑f.hom
      (↑(↑(ρ A) g * ↑(ρ A) g⁻¹) y ⊗ₜ[k]
        ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj B).map
              g)
          (↑(↑(ρ A) g⁻¹) y, x).snd)
[PROOFSTEP]
simp only [← map_mul, mul_inv_self, map_one]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : A ⊗ B ⟶ C
g : ↑(MonCat.of G)
x : ↑B.V
y : CoeSort.coe A
⊢ ↑f.hom (y ⊗ₜ[k] ↑(↑B.ρ g) x) =
    ↑f.hom
      (↑1 y ⊗ₜ[k]
        ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj B).map
              g)
          x)
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : B ⟶ (Rep.ihom A).obj C
g : ↑(MonCat.of G)
x :
  ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj A).obj
      PUnit.unit)
y :
  ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj B).obj
      PUnit.unit)
⊢ ↑(↑(A ⊗ B).ρ g ≫ ↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom))
      (x ⊗ₜ[k] y) =
    ↑(↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom) ≫ ↑C.ρ g) (x ⊗ₜ[k] y)
[PROOFSTEP]
change
  TensorProduct.uncurry k _ _ _ f.hom.flip (A.ρ g x ⊗ₜ[k] B.ρ g y) =
    C.ρ g (TensorProduct.uncurry k _ _ _ f.hom.flip (x ⊗ₜ[k] y))
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : B ⟶ (Rep.ihom A).obj C
g : ↑(MonCat.of G)
x :
  ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj A).obj
      PUnit.unit)
y :
  ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj B).obj
      PUnit.unit)
⊢ ↑(↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom))
      (↑(↑(ρ A) g) x ⊗ₜ[k] ↑(↑(ρ B) g) y) =
    ↑(↑(ρ C) g)
      (↑(↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom)) (x ⊗ₜ[k] y))
[PROOFSTEP]
rw [TensorProduct.uncurry_apply, LinearMap.flip_apply, hom_comm_apply, Rep.ihom_obj_ρ_apply, LinearMap.comp_apply,
  LinearMap.comp_apply, ρ_inv_self_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : B ⟶ (Rep.ihom A).obj C
g : ↑(MonCat.of G)
x :
  ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj A).obj
      PUnit.unit)
y :
  ↑(((CategoryTheory.Equivalence.symm (functorCategoryEquivalence (ModuleCat k) (MonCat.of G))).inverse.obj B).obj
      PUnit.unit)
⊢ ↑(↑(ρ C) g) (↑(↑f.hom y) x) =
    ↑(↑(ρ C) g)
      (↑(↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom)) (x ⊗ₜ[k] y))
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : B ⟶ (Rep.ihom A).obj C
⊢ (fun f => Hom.mk (LinearMap.flip (TensorProduct.curry f.hom)))
      ((fun f => Hom.mk (↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom))) f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h.h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C✝ A B C : Rep k G
f : B ⟶ (Rep.ihom A).obj C
x✝ : ↑B.V
⊢ ↑((fun f => Hom.mk (LinearMap.flip (TensorProduct.curry f.hom)))
            ((fun f =>
                Hom.mk (↑(TensorProduct.uncurry k (CoeSort.coe A) (↑B.V) (CoeSort.coe C)) (LinearMap.flip f.hom)))
              f)).hom
      x✝ =
    ↑f.hom x✝
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C A B : Rep k G
⊢ (NatTrans.app (ihom.ev A) B).hom =
    ↑(TensorProduct.uncurry k (CoeSort.coe A) (CoeSort.coe A →ₗ[k] CoeSort.coe B) (CoeSort.coe B))
      (LinearMap.flip LinearMap.id)
[PROOFSTEP]
ext
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A✝ B✝ C A B : Rep k G
x✝ : ↑((ihom A ⋙ tensorLeft A).obj B).V
⊢ ↑(NatTrans.app (ihom.ev A) B).hom x✝ =
    ↑(↑(TensorProduct.uncurry k (CoeSort.coe A) (CoeSort.coe A →ₗ[k] CoeSort.coe B) (CoeSort.coe B))
          (LinearMap.flip LinearMap.id))
      x✝
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ SymmetricCategory (Rep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ MonoidalPreadditive (Rep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ MonoidalLinear k (Rep k G)
[PROOFSTEP]
infer_instance
[GOAL]
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
⊢ ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) r) x) = ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) r) (↑f x)
[PROOFSTEP]
apply MonoidAlgebra.induction_on r
[GOAL]
case hM
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
⊢ ∀ (g : G),
    ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (↑(MonoidAlgebra.of k G) g)) x) =
      ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (↑(MonoidAlgebra.of k G) g)) (↑f x)
[PROOFSTEP]
intro g
[GOAL]
case hM
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
g : G
⊢ ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (↑(MonoidAlgebra.of k G) g)) x) =
    ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (↑(MonoidAlgebra.of k G) g)) (↑f x)
[PROOFSTEP]
simp only [one_smul, MonoidAlgebra.lift_single, MonoidAlgebra.of_apply]
[GOAL]
case hM
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
g : G
⊢ ↑f (↑(↑ρ g) x) = ↑(↑σ g) (↑f x)
[PROOFSTEP]
exact LinearMap.congr_fun (w g) x
[GOAL]
case hadd
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
⊢ ∀ (f_1 g : MonoidAlgebra k G),
    ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) f_1) x) =
        ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) f_1) (↑f x) →
      ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) g) x) = ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) g) (↑f x) →
        ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (f_1 + g)) x) =
          ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (f_1 + g)) (↑f x)
[PROOFSTEP]
intro g h gw hw
[GOAL]
case hadd
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
g h : MonoidAlgebra k G
gw : ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) g) x) = ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) g) (↑f x)
hw : ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) h) x) = ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) h) (↑f x)
⊢ ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (g + h)) x) =
    ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (g + h)) (↑f x)
[PROOFSTEP]
simp only [map_add, add_left_inj, LinearMap.add_apply, hw, gw]
[GOAL]
case hsmul
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r : MonoidAlgebra k G
x : V
⊢ ∀ (r : k) (f_1 : MonoidAlgebra k G),
    ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) f_1) x) =
        ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) f_1) (↑f x) →
      ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (r • f_1)) x) =
        ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (r • f_1)) (↑f x)
[PROOFSTEP]
intro r g w
[GOAL]
case hsmul
k✝ G✝ : Type u
inst✝⁷ : CommRing k✝
inst✝⁶ : Monoid G✝
k : Type u_1
G : Type u_2
inst✝⁵ : CommRing k
inst✝⁴ : Monoid G
V : Type u_3
W : Type u_4
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup W
inst✝¹ : Module k V
inst✝ : Module k W
ρ : G →* V →ₗ[k] V
σ : G →* W →ₗ[k] W
f : V →ₗ[k] W
w✝ : ∀ (g : G), LinearMap.comp f (↑ρ g) = LinearMap.comp (↑σ g) f
r✝ : MonoidAlgebra k G
x : V
r : k
g : MonoidAlgebra k G
w : ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) g) x) = ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) g) (↑f x)
⊢ ↑f (↑(↑(↑(MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ) (r • g)) x) =
    ↑(↑(↑(MonoidAlgebra.lift k G (W →ₗ[k] W)) σ) (r • g)) (↑f x)
[PROOFSTEP]
simp only [AlgHom.map_smul, w, RingHom.id_apply, LinearMap.smul_apply, LinearMap.map_smulₛₗ]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : ModuleCat (MonoidAlgebra k G)
f : X✝ ⟶ Y✝
g : ↑(MonCat.of G)
⊢ ↑((fun M => of (Representation.ofModule ↑M)) X✝).ρ g ≫
      { toAddHom := f.toAddHom,
        map_smul' :=
          (_ :
            ∀ (r : k) (x : ↑((fun M => of (Representation.ofModule ↑M)) X✝).V),
              ↑f (↑(algebraMap k (MonoidAlgebra k G)) r • x) = ↑(algebraMap k (MonoidAlgebra k G)) r • ↑f x) } =
    { toAddHom := f.toAddHom,
        map_smul' :=
          (_ :
            ∀ (r : k) (x : ↑((fun M => of (Representation.ofModule ↑M)) X✝).V),
              ↑f (↑(algebraMap k (MonoidAlgebra k G)) r • x) = ↑(algebraMap k (MonoidAlgebra k G)) r • ↑f x) } ≫
      ↑((fun M => of (Representation.ofModule ↑M)) Y✝).ρ g
[PROOFSTEP]
ext
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : ModuleCat (MonoidAlgebra k G)
f : X✝ ⟶ Y✝
g : ↑(MonCat.of G)
x✝ : ↑((fun M => of (Representation.ofModule ↑M)) X✝).V
⊢ ↑(↑((fun M => of (Representation.ofModule ↑M)) X✝).ρ g ≫
          { toAddHom := f.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : k) (x : ↑((fun M => of (Representation.ofModule ↑M)) X✝).V),
                  ↑f (↑(algebraMap k (MonoidAlgebra k G)) r • x) = ↑(algebraMap k (MonoidAlgebra k G)) r • ↑f x) })
      x✝ =
    ↑({ toAddHom := f.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : k) (x : ↑((fun M => of (Representation.ofModule ↑M)) X✝).V),
                  ↑f (↑(algebraMap k (MonoidAlgebra k G)) r • x) = ↑(algebraMap k (MonoidAlgebra k G)) r • ↑f x) } ≫
          ↑((fun M => of (Representation.ofModule ↑M)) Y✝).ρ g)
      x✝
[PROOFSTEP]
apply f.map_smul
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat (MonoidAlgebra k G)
⊢ ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M) ≃+ ↑M
[PROOFSTEP]
dsimp [ofModuleMonoidAlgebra, toModuleMonoidAlgebra]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat (MonoidAlgebra k G)
⊢ ↑(ModuleCat.of (MonoidAlgebra k G) (Representation.asModule (Representation.ofModule ↑M))) ≃+ ↑M
[PROOFSTEP]
refine' (Representation.ofModule M).asModuleEquiv.trans (RestrictScalars.addEquiv k (MonoidAlgebra k G) _)
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ CoeSort.coe V ≃+ CoeSort.coe ((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V)
[PROOFSTEP]
dsimp [ofModuleMonoidAlgebra, toModuleMonoidAlgebra]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ CoeSort.coe V ≃+
    RestrictScalars k (MonoidAlgebra k G) ↑(ModuleCat.of (MonoidAlgebra k G) (Representation.asModule (ρ V)))
[PROOFSTEP]
refine' V.ρ.asModuleEquiv.symm.trans _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
⊢ Representation.asModule (ρ V) ≃+
    RestrictScalars k (MonoidAlgebra k G) ↑(ModuleCat.of (MonoidAlgebra k G) (Representation.asModule (ρ V)))
[PROOFSTEP]
exact (RestrictScalars.addEquiv _ _ _).symm
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat (MonoidAlgebra k G)
src✝ : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M) ≃+ ↑M := counitIsoAddEquiv
r : MonoidAlgebra k G
x : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M)
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M)),
              Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (r • x) =
    ↑(RingHom.id (MonoidAlgebra k G)) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M)),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        x
[PROOFSTEP]
dsimp [counitIsoAddEquiv]
  /- Porting note: rest of broken proof was `simp`. -/
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat (MonoidAlgebra k G)
src✝ : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M) ≃+ ↑M := counitIsoAddEquiv
r : MonoidAlgebra k G
x : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M)
⊢ ↑↑(AddEquiv.trans (Representation.asModuleEquiv (Representation.ofModule ↑M))
            (RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M))
      (r • x) =
    r •
      ↑↑(AddEquiv.trans (Representation.asModuleEquiv (Representation.ofModule ↑M))
              (RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M))
        x
[PROOFSTEP]
rw [AddEquiv.coe_toEquiv, AddEquiv.trans_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat (MonoidAlgebra k G)
src✝ : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M) ≃+ ↑M := counitIsoAddEquiv
r : MonoidAlgebra k G
x : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M)
⊢ ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M)
      (↑(Representation.asModuleEquiv (Representation.ofModule ↑M)) (r • x)) =
    r •
      ↑(AddEquiv.trans (Representation.asModuleEquiv (Representation.ofModule ↑M))
            (RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M))
        x
[PROOFSTEP]
erw [Representation.ofModule_asAlgebraHom_apply_apply]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
M : ModuleCat (MonoidAlgebra k G)
src✝ : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M) ≃+ ↑M := counitIsoAddEquiv
r : MonoidAlgebra k G
x : ↑((ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).obj M)
⊢ ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) ((fun x => ↑M) x)))
      (r • ↑(RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M) x) =
    r •
      ↑(AddEquiv.trans (Representation.asModuleEquiv (Representation.ofModule ↑M))
            (RestrictScalars.addEquiv k (MonoidAlgebra k G) ↑M))
        x
[PROOFSTEP]
exact AddEquiv.symm_apply_apply _ _
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : G
x : CoeSort.coe V
⊢ ↑unitIsoAddEquiv (AddHom.toFun (↑(ρ V) g).toAddHom x) =
    AddHom.toFun (↑(ρ (ofModuleMonoidAlgebra.obj (toModuleMonoidAlgebra.obj V))) g).toAddHom (↑unitIsoAddEquiv x)
[PROOFSTEP]
dsimp [unitIsoAddEquiv, ofModuleMonoidAlgebra, toModuleMonoidAlgebra]
  /- Porting note: rest of broken proof was
    simp only [AddEquiv.apply_eq_iff_eq, AddEquiv.apply_symm_apply,
      Representation.asModuleEquiv_symm_map_rho, Representation.ofModule_asModule_act] -/
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : G
x : CoeSort.coe V
⊢ ↑(AddEquiv.trans (AddEquiv.symm (Representation.asModuleEquiv (ρ V)))
          (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V)))))
      (↑(↑(ρ V) g) x) =
    AddHom.toFun
      (↑(Representation.ofModule ↑(ModuleCat.of (MonoidAlgebra k G) (Representation.asModule (ρ V)))) g).toAddHom
      (↑(AddEquiv.trans (AddEquiv.symm (Representation.asModuleEquiv (ρ V)))
            (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V)))))
        x)
[PROOFSTEP]
erw [Representation.asModuleEquiv_symm_map_rho]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : G
x : CoeSort.coe V
⊢ ↑(MonoidAlgebra.of k G) g • ↑(AddEquiv.symm (Representation.asModuleEquiv (ρ V))) x =
    AddHom.toFun
      (↑(Representation.ofModule ↑(ModuleCat.of (MonoidAlgebra k G) (Representation.asModule (ρ V)))) g).toAddHom
      (↑(AddEquiv.trans (AddEquiv.symm (Representation.asModuleEquiv (ρ V)))
            (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V)))))
        x)
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
src✝ : CoeSort.coe V ≃+ CoeSort.coe ((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V) := unitIsoAddEquiv
r : k
x : ↑V.V
⊢ AddHom.toFun
      { toFun := src✝.toFun,
        map_add' :=
          (_ :
            ∀ (x y : CoeSort.coe V),
              Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
      (r • x) =
    ↑(RingHom.id k) r •
      AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : CoeSort.coe V),
                Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
        x
[PROOFSTEP]
dsimp [unitIsoAddEquiv]
  /- Porting note: rest of broken proof was
            simp only [Representation.asModuleEquiv_symm_map_smul,
              RestrictScalars.addEquiv_symm_map_algebraMap_smul] -/
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
src✝ : CoeSort.coe V ≃+ CoeSort.coe ((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V) := unitIsoAddEquiv
r : k
x : ↑V.V
⊢ ↑↑(AddEquiv.trans (AddEquiv.symm (Representation.asModuleEquiv (ρ V)))
            (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V)))))
      (r • x) =
    r •
      ↑↑(AddEquiv.trans (AddEquiv.symm (Representation.asModuleEquiv (ρ V)))
              (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V)))))
        x
[PROOFSTEP]
rw [AddEquiv.coe_toEquiv, AddEquiv.trans_apply, Representation.asModuleEquiv_symm_map_smul,
  RestrictScalars.addEquiv_symm_map_algebraMap_smul]
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
src✝ : CoeSort.coe V ≃+ CoeSort.coe ((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V) := unitIsoAddEquiv
r : k
x : ↑V.V
⊢ r •
      ↑(AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V))))
        (↑(AddEquiv.symm (Representation.asModuleEquiv (ρ V))) x) =
    r •
      ↑(AddEquiv.trans (AddEquiv.symm (Representation.asModuleEquiv (ρ V)))
            (AddEquiv.symm (RestrictScalars.addEquiv k (MonoidAlgebra k G) (Representation.asModule (ρ V)))))
        x
[PROOFSTEP]
rfl
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : ↑(MonCat.of G)
⊢ ↑V.ρ g ≫
      (LinearEquiv.toModuleIso'
          (let src := unitIsoAddEquiv;
          {
            toLinearMap :=
              {
                toAddHom :=
                  { toFun := src.toFun,
                    map_add' :=
                      (_ :
                        ∀ (x y : CoeSort.coe V),
                          Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) },
                map_smul' :=
                  (_ :
                    ∀ (r : k) (x : ↑V.V),
                      AddHom.toFun
                          { toFun := src.toFun,
                            map_add' :=
                              (_ :
                                ∀ (x y : CoeSort.coe V),
                                  Equiv.toFun src.toEquiv (x + y) =
                                    Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                          (r • x) =
                        ↑(RingHom.id k) r •
                          AddHom.toFun
                            { toFun := src.toFun,
                              map_add' :=
                                (_ :
                                  ∀ (x y : CoeSort.coe V),
                                    Equiv.toFun src.toEquiv (x + y) =
                                      Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                            x) },
            invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
            right_inv := (_ : Function.RightInverse src.invFun src.toFun) })).hom =
    (LinearEquiv.toModuleIso'
          (let src := unitIsoAddEquiv;
          {
            toLinearMap :=
              {
                toAddHom :=
                  { toFun := src.toFun,
                    map_add' :=
                      (_ :
                        ∀ (x y : CoeSort.coe V),
                          Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) },
                map_smul' :=
                  (_ :
                    ∀ (r : k) (x : ↑V.V),
                      AddHom.toFun
                          { toFun := src.toFun,
                            map_add' :=
                              (_ :
                                ∀ (x y : CoeSort.coe V),
                                  Equiv.toFun src.toEquiv (x + y) =
                                    Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                          (r • x) =
                        ↑(RingHom.id k) r •
                          AddHom.toFun
                            { toFun := src.toFun,
                              map_add' :=
                                (_ :
                                  ∀ (x y : CoeSort.coe V),
                                    Equiv.toFun src.toEquiv (x + y) =
                                      Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                            x) },
            invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
            right_inv := (_ : Function.RightInverse src.invFun src.toFun) })).hom ≫
      ↑((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V).ρ g
[PROOFSTEP]
ext
[GOAL]
case h
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
V : Rep k G
g : ↑(MonCat.of G)
x✝ : ↑V.V
⊢ ↑(↑V.ρ g ≫
          (LinearEquiv.toModuleIso'
              (let src := unitIsoAddEquiv;
              {
                toLinearMap :=
                  {
                    toAddHom :=
                      { toFun := src.toFun,
                        map_add' :=
                          (_ :
                            ∀ (x y : CoeSort.coe V),
                              Equiv.toFun src.toEquiv (x + y) =
                                Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) },
                    map_smul' :=
                      (_ :
                        ∀ (r : k) (x : ↑V.V),
                          AddHom.toFun
                              { toFun := src.toFun,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : CoeSort.coe V),
                                      Equiv.toFun src.toEquiv (x + y) =
                                        Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                              (r • x) =
                            ↑(RingHom.id k) r •
                              AddHom.toFun
                                { toFun := src.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : CoeSort.coe V),
                                        Equiv.toFun src.toEquiv (x + y) =
                                          Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                                x) },
                invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
                right_inv := (_ : Function.RightInverse src.invFun src.toFun) })).hom)
      x✝ =
    ↑((LinearEquiv.toModuleIso'
              (let src := unitIsoAddEquiv;
              {
                toLinearMap :=
                  {
                    toAddHom :=
                      { toFun := src.toFun,
                        map_add' :=
                          (_ :
                            ∀ (x y : CoeSort.coe V),
                              Equiv.toFun src.toEquiv (x + y) =
                                Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) },
                    map_smul' :=
                      (_ :
                        ∀ (r : k) (x : ↑V.V),
                          AddHom.toFun
                              { toFun := src.toFun,
                                map_add' :=
                                  (_ :
                                    ∀ (x y : CoeSort.coe V),
                                      Equiv.toFun src.toEquiv (x + y) =
                                        Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                              (r • x) =
                            ↑(RingHom.id k) r •
                              AddHom.toFun
                                { toFun := src.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : CoeSort.coe V),
                                        Equiv.toFun src.toEquiv (x + y) =
                                          Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }
                                x) },
                invFun := src.invFun, left_inv := (_ : Function.LeftInverse src.invFun src.toFun),
                right_inv := (_ : Function.RightInverse src.invFun src.toFun) })).hom ≫
          ↑((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V).ρ g)
      x✝
[PROOFSTEP]
apply unit_iso_comm
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ∀ {X Y : Rep k G} (f : X ⟶ Y),
    (𝟭 (Rep k G)).map f ≫ ((fun V => unitIso V) Y).hom =
      ((fun V => unitIso V) X).hom ≫ (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).map f
[PROOFSTEP]
aesop_cat
[GOAL]
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ ∀ {X Y : ModuleCat (MonoidAlgebra k G)} (f : X ⟶ Y),
    (ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra).map f ≫ ((fun M => counitIso M) Y).hom =
      ((fun M => counitIso M) X).hom ≫ (𝟭 (ModuleCat (MonoidAlgebra k G))).map f
[PROOFSTEP]
aesop_cat
