awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Monoid G
V : Type u_3
W : Type u_4
inst_2 : AddCommGroup V
inst_3 : AddCommGroup W
inst_4 : Module k V
inst_5 : Module k W
ρ : MonoidHom.{u_2, u_3} G (V →ₗ[k] V)
σ : MonoidHom.{u_2, u_4} G (W →ₗ[k] W)
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g = (σ : (a : G) → W →ₗ[k] W) g ∘ₗ f
r : k[G]
x : V
g : G
hM :
  Eq (α := W) ((f : (a : V) → W) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) : W)
    ((((σ : (a : G) → W →ₗ[k] W) g : W →ₗ[k] W) : (a : W) → W) ((f : (a : V) → W) x : W) : W)
⊢ Eq (α := W)
    ((f : (a : V) → W)
        ((((((lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ : k[G] →ₐ[k] V →ₗ[k] V) :
                    (a : k[G]) → V →ₗ[k] V)
                  ((MonoidAlgebra.of k G : (a : G) → k[G]) g) :
                V →ₗ[k] V) :
              (a : V) → V)
            x :
          V) :
      W)
    ((((((lift k (W →ₗ[k] W) G : (a : G →* W →ₗ[k] W) → k[G] →ₐ[k] W →ₗ[k] W) σ : k[G] →ₐ[k] W →ₗ[k] W) :
                (a : k[G]) → W →ₗ[k] W)
              ((MonoidAlgebra.of k G : (a : G) → k[G]) g) :
            W →ₗ[k] W) :
          (a : W) → W)
        ((f : (a : V) → W) x : W) :
      W)

Tactic:
simp only [one_smul, MonoidAlgebra.lift_single, MonoidAlgebra.of_apply]

Premises used: one_smul, MonoidAlgebra.lift_single, MonoidAlgebra.of_apply
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Monoid G
V : Type u_3
W : Type u_4
inst_2 : AddCommGroup V
inst_3 : AddCommGroup W
inst_4 : Module k V
inst_5 : Module k W
ρ : MonoidHom.{u_2, u_3} G (V →ₗ[k] V)
σ : MonoidHom.{u_2, u_4} G (W →ₗ[k] W)
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g = (σ : (a : G) → W →ₗ[k] W) g ∘ₗ f
r : k[G]
x : V
g : G
⊢ Eq (α := W) ((f : (a : V) → W) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) : W)
    ((((σ : (a : G) → W →ₗ[k] W) g : W →ₗ[k] W) : (a : W) → W) ((f : (a : V) → W) x : W) : W)

Tactic:
LinearMap.congr_fun (w g) x

Premises used: LinearMap.congr_fun
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Monoid G
V : Type u_3
W : Type u_4
inst_2 : AddCommGroup V
inst_3 : AddCommGroup W
inst_4 : Module k V
inst_5 : Module k W
ρ : MonoidHom.{u_2, u_3} G (V →ₗ[k] V)
σ : MonoidHom.{u_2, u_4} G (W →ₗ[k] W)
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g = (σ : (a : G) → W →ₗ[k] W) g ∘ₗ f
r : k[G]
x : V
g : G
⊢ Eq (α := W) ((f : (a : V) → W) ((((ρ : (a : G) → V →ₗ[k] V) g : V →ₗ[k] V) : (a : V) → V) x : V) : W)
    ((((σ : (a : G) → W →ₗ[k] W) g : W →ₗ[k] W) : (a : W) → W) ((f : (a : V) → W) x : W) : W)

Tactic:
exact LinearMap.congr_fun (w g) x

Premises used: LinearMap.congr_fun
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Monoid G
V : Type u_3
W : Type u_4
inst_2 : AddCommGroup V
inst_3 : AddCommGroup W
inst_4 : Module k V
inst_5 : Module k W
ρ : MonoidHom.{u_2, u_3} G (V →ₗ[k] V)
σ : MonoidHom.{u_2, u_4} G (W →ₗ[k] W)
f : V →ₗ[k] W
w : ∀ (g : G), f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g = (σ : (a : G) → W →ₗ[k] W) g ∘ₗ f
r : k[G]
x : V
g h : k[G]
gw :
  Eq (α := W)
    ((f : (a : V) → W)
        ((((((lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ : k[G] →ₐ[k] V →ₗ[k] V) :
                    (a : k[G]) → V →ₗ[k] V)
                  g :
                V →ₗ[k] V) :
              (a : V) → V)
            x :
          V) :
      W)
    ((((((lift k (W →ₗ[k] W) G : (a : G →* W →ₗ[k] W) → k[G] →ₐ[k] W →ₗ[k] W) σ : k[G] →ₐ[k] W →ₗ[k] W) :
                (a : k[G]) → W →ₗ[k] W)
              g :
            W →ₗ[k] W) :
          (a : W) → W)
        ((f : (a : V) → W) x : W) :
      W)
hw :
  Eq (α := W)
    ((f : (a : V) → W)
        ((((((lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ : k[G] →ₐ[k] V →ₗ[k] V) :
                    (a : k[G]) → V →ₗ[k] V)
                  h :
                V →ₗ[k] V) :
              (a : V) → V)
            x :
          V) :
      W)
    ((((((lift k (W →ₗ[k] W) G : (a : G →* W →ₗ[k] W) → k[G] →ₐ[k] W →ₗ[k] W) σ : k[G] →ₐ[k] W →ₗ[k] W) :
                (a : k[G]) → W →ₗ[k] W)
              h :
            W →ₗ[k] W) :
          (a : W) → W)
        ((f : (a : V) → W) x : W) :
      W)
⊢ Eq (α := W)
    ((f : (a : V) → W)
        ((((((lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ : k[G] →ₐ[k] V →ₗ[k] V) :
                    (a : k[G]) → V →ₗ[k] V)
                  (g + h) :
                V →ₗ[k] V) :
              (a : V) → V)
            x :
          V) :
      W)
    ((((((lift k (W →ₗ[k] W) G : (a : G →* W →ₗ[k] W) → k[G] →ₐ[k] W →ₗ[k] W) σ : k[G] →ₐ[k] W →ₗ[k] W) :
                (a : k[G]) → W →ₗ[k] W)
              (g + h) :
            W →ₗ[k] W) :
          (a : W) → W)
        ((f : (a : V) → W) x : W) :
      W)

Tactic:
simp only [map_add, LinearMap.add_apply, hw, gw]

Premises used: LinearMap.add_apply, map_add
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u_1
G : Type u_2
inst : CommRing k
inst_1 : Monoid G
V : Type u_3
W : Type u_4
inst_2 : AddCommGroup V
inst_3 : AddCommGroup W
inst_4 : Module k V
inst_5 : Module k W
ρ : MonoidHom.{u_2, u_3} G (V →ₗ[k] V)
σ : MonoidHom.{u_2, u_4} G (W →ₗ[k] W)
f : V →ₗ[k] W
w_1 : ∀ (g : G), f ∘ₗ (ρ : (a : G) → V →ₗ[k] V) g = (σ : (a : G) → W →ₗ[k] W) g ∘ₗ f
r_1 : k[G]
x : V
r : k
g : k[G]
w :
  Eq (α := W)
    ((f : (a : V) → W)
        ((((((lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ : k[G] →ₐ[k] V →ₗ[k] V) :
                    (a : k[G]) → V →ₗ[k] V)
                  g :
                V →ₗ[k] V) :
              (a : V) → V)
            x :
          V) :
      W)
    ((((((lift k (W →ₗ[k] W) G : (a : G →* W →ₗ[k] W) → k[G] →ₐ[k] W →ₗ[k] W) σ : k[G] →ₐ[k] W →ₗ[k] W) :
                (a : k[G]) → W →ₗ[k] W)
              g :
            W →ₗ[k] W) :
          (a : W) → W)
        ((f : (a : V) → W) x : W) :
      W)
⊢ Eq (α := W)
    ((f : (a : V) → W)
        ((((((lift k (V →ₗ[k] V) G : (a : G →* V →ₗ[k] V) → k[G] →ₐ[k] V →ₗ[k] V) ρ : k[G] →ₐ[k] V →ₗ[k] V) :
                    (a : k[G]) → V →ₗ[k] V)
                  (r • g) :
                V →ₗ[k] V) :
              (a : V) → V)
            x :
          V) :
      W)
    ((((((lift k (W →ₗ[k] W) G : (a : G →* W →ₗ[k] W) → k[G] →ₐ[k] W →ₗ[k] W) σ : k[G] →ₐ[k] W →ₗ[k] W) :
                (a : k[G]) → W →ₗ[k] W)
              (r • g) :
            W →ₗ[k] W) :
          (a : W) → W)
        ((f : (a : V) → W) x : W) :
      W)

Tactic:
simp only [map_smul, w, LinearMap.smul_apply]

Premises used: LinearMap.smul_apply, map_smul
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : ModuleCat k[G]
f : X ⟶ Y
g : G
h :
  ∀ (x : RestrictScalars k k[G] (↑X : Type w)),
    Eq (α := RestrictScalars k k[G] (↑Y : Type w))
      (({ toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ } ∘ₗ
              (Representation.ofModule (↑X : Type w) :
                  (a : G) → RestrictScalars k k[G] (↑X : Type w) →ₗ[k] RestrictScalars k k[G] (↑X : Type w))
                g :
            (a : RestrictScalars k k[G] (↑X : Type w)) → RestrictScalars k k[G] (↑Y : Type w))
          x :
        RestrictScalars k k[G] (↑Y : Type w))
      (((Representation.ofModule (↑Y : Type w) :
                  (a : G) → RestrictScalars k k[G] (↑Y : Type w) →ₗ[k] RestrictScalars k k[G] (↑Y : Type w))
                g ∘ₗ
              { toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ } :
            (a : RestrictScalars k k[G] (↑X : Type w)) → RestrictScalars k k[G] (↑Y : Type w))
          x :
        RestrictScalars k k[G] (↑Y : Type w))
⊢ Eq (α := RestrictScalars k k[G] (↑X : Type w) →ₗ[k] RestrictScalars k k[G] (↑Y : Type w))
    ({ toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ } ∘ₗ
      (Representation.ofModule (↑X : Type w) :
          (a : G) → RestrictScalars k k[G] (↑X : Type w) →ₗ[k] RestrictScalars k k[G] (↑X : Type w))
        g)
    ((Representation.ofModule (↑Y : Type w) :
          (a : G) → RestrictScalars k k[G] (↑Y : Type w) →ₗ[k] RestrictScalars k k[G] (↑Y : Type w))
        g ∘ₗ
      { toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ })

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : ModuleCat k[G]
f : X ⟶ Y
g : G
x : RestrictScalars k k[G] (↑X : Type w)
⊢ Eq (α := RestrictScalars k k[G] (↑Y : Type w))
    (({ toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ } ∘ₗ
            (Representation.ofModule (↑X : Type w) :
                (a : G) → RestrictScalars k k[G] (↑X : Type w) →ₗ[k] RestrictScalars k k[G] (↑X : Type w))
              g :
          (a : RestrictScalars k k[G] (↑X : Type w)) → RestrictScalars k k[G] (↑Y : Type w))
        x :
      RestrictScalars k k[G] (↑Y : Type w))
    (((Representation.ofModule (↑Y : Type w) :
                (a : G) → RestrictScalars k k[G] (↑Y : Type w) →ₗ[k] RestrictScalars k k[G] (↑Y : Type w))
              g ∘ₗ
            { toAddHom := (ModuleCat.Hom.hom f).toAddHom, map_smul' := ⋯ } :
          (a : RestrictScalars k k[G] (↑X : Type w)) → RestrictScalars k k[G] (↑Y : Type w))
        x :
      RestrictScalars k k[G] (↑Y : Type w))

Tactic:
apply f.hom.map_smul

Premises used: LinearMap.map_smul, ModuleCat.Hom.hom
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
M : ModuleCat k[G]
⊢ (↑(Functor.obj ofModuleMonoidAlgebra M) : Type w) = RestrictScalars k k[G] (↑M : Type w)

Tactic:
rfl

Premises used: RestrictScalars, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
M : ModuleCat k[G]
⊢ (Functor.obj ofModuleMonoidAlgebra M).ρ = Representation.ofModule (↑M : Type w)

Tactic:
rfl

Premises used: Representation.ofModule, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
M : ModuleCat k[G]
dsimp :
  Representation.asModule.{u, v, w} (k := k) (G := G) (V := RestrictScalars k k[G] (↑M : Type w))
      (Representation.ofModule (↑M : Type w)) ≃+
    (↑M : Type w)
⊢ (↑(Functor.obj (ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra) M) : Type w) ≃+ (↑M : Type w)

Tactic:
dsimp [ofModuleMonoidAlgebra, toModuleMonoidAlgebra]

Premises used: Rep.ofModuleMonoidAlgebra, Rep.toModuleMonoidAlgebra
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
M : ModuleCat k[G]
⊢ Representation.asModule.{u, v, w} (k := k) (G := G) (V := RestrictScalars k k[G] (↑M : Type w))
      (Representation.ofModule (↑M : Type w)) ≃+
    (↑M : Type w)

Tactic:
exact (Representation.ofModule M).asModuleEquiv.toAddEquiv.trans
    (RestrictScalars.addEquiv k k[G] _)

Premises used: RestrictScalars.addEquiv, LinearEquiv.toAddEquiv, Representation.ofModule, AddEquiv.trans, MonoidAlgebra, ModuleCat.carrier, Representation.asModuleEquiv
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
V : Rep.{w, u, v} k G
dsimp : (↑V : Type w) ≃+ RestrictScalars k k[G] V.ρ.asModule
⊢ (↑V : Type w) ≃+ (↑(Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) V) : Type w)

Tactic:
dsimp [ofModuleMonoidAlgebra, toModuleMonoidAlgebra]

Premises used: Rep.ofModuleMonoidAlgebra, Rep.toModuleMonoidAlgebra
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
V : Rep.{w, u, v} k G
⊢ (↑V : Type w) ≃+ RestrictScalars k k[G] V.ρ.asModule

Tactic:
exact V.ρ.asModuleEquiv.symm.toAddEquiv.trans (RestrictScalars.addEquiv _ _ _).symm

Premises used: LinearEquiv.symm, RestrictScalars.addEquiv, LinearEquiv.toAddEquiv, AddEquiv.trans, Rep.ρ, Representation.asModuleEquiv, AddEquiv.symm
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
M : ModuleCat k[G]
r : k[G]
x : (Functor.obj ofModuleMonoidAlgebra M).ρ.asModule
⊢ Equiv.toFun (AddEquiv.toEquiv counitIsoAddEquiv) (r • x) =
    HSMul.hSMul (α := k[G]) ((RingHom.id k[G] : (a : k[G]) → k[G]) r : k[G])
      (Equiv.toFun (AddEquiv.toEquiv counitIsoAddEquiv) x)

Tactic:
simp [counitIsoAddEquiv]

Premises used: Rep.counitIsoAddEquiv
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
V : Rep.{w, u, v} k G
g : G
x : (↑V : Type w)
⊢ Eq (α := (↑(Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) V) : Type w))
    ((unitIsoAddEquiv : (a : (↑V : Type w)) → (↑((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V) : Type w))
        (AddHom.toFun
          (LinearMap.toAddHom.{u, u, w, w} (R := k) (S := k) (σ := RingHom.id k)
            ((V.ρ : (a : G) → (↑V : Type w) →ₗ[k] (↑V : Type w)) g))
          x) :
      (↑(Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) V) : Type w))
    (AddHom.toFun (M := (↑(Functor.obj ofModuleMonoidAlgebra (Functor.obj toModuleMonoidAlgebra V)) : Type w))
        (LinearMap.toAddHom.{u, u, w, w} (R := k) (S := k) (σ := RingHom.id k)
            (((Functor.obj ofModuleMonoidAlgebra (Functor.obj toModuleMonoidAlgebra V)).ρ :
                (a : G) →
                  (↑(ofModuleMonoidAlgebra.obj (toModuleMonoidAlgebra.obj V)) : Type w) →ₗ[k]
                    (↑(ofModuleMonoidAlgebra.obj (toModuleMonoidAlgebra.obj V)) : Type w))
              g) :
          (↑(Functor.obj ofModuleMonoidAlgebra (Functor.obj toModuleMonoidAlgebra V)) : Type w) →ₙ+
            (↑(Functor.obj ofModuleMonoidAlgebra (Functor.obj toModuleMonoidAlgebra V)) : Type w))
        ((unitIsoAddEquiv : (a : (↑V : Type w)) → (↑((toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra).obj V) : Type w))
            x :
          (↑(Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) V) : Type w)) :
      (↑(Functor.obj ofModuleMonoidAlgebra (Functor.obj toModuleMonoidAlgebra V)) : Type w))

Tactic:
simp [unitIsoAddEquiv, ofModuleMonoidAlgebra, toModuleMonoidAlgebra]

Premises used: Rep.ofModuleMonoidAlgebra, Rep.unitIsoAddEquiv, Rep.toModuleMonoidAlgebra
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
V : Rep.{w, u, v} k G
r : k
x : (↑V : Type w)
simp :
  (AddEquiv.symm (RestrictScalars.addEquiv k k[G] V.ρ.asModule) :
        (a : V.ρ.asModule) → RestrictScalars k k[G] V.ρ.asModule)
      (HSMul.hSMul (α := k[G]) (β := V.ρ.asModule) ((algebraMap k k[G] : (a : k) → k[G]) r : k[G])
        ((V.ρ.asModuleEquiv.symm : (a : (↑V : Type w)) → V.ρ.asModule) x : V.ρ.asModule)) =
    HSMul.hSMul (α := k) ((RingHom.id k : (a : k) → k) r : k) (Equiv.toFun (AddEquiv.toEquiv unitIsoAddEquiv) x)
⊢ (AddEquiv.symm (RestrictScalars.addEquiv k k[G] V.ρ.asModule) :
        (a : V.ρ.asModule) → RestrictScalars k k[G] V.ρ.asModule)
      ((V.ρ.asModuleEquiv.symm : (a : (↑V : Type w)) → V.ρ.asModule) (r • x) : V.ρ.asModule) =
    HSMul.hSMul (α := k) ((RingHom.id k : (a : k) → k) r : k) (Equiv.toFun (AddEquiv.toEquiv unitIsoAddEquiv) x)

Tactic:
simp only [Representation.asModuleEquiv_symm_map_smul]

Premises used: Representation.asModuleEquiv_symm_map_smul
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
V : Rep.{w, u, v} k G
r : k
x : (↑V : Type w)
⊢ (AddEquiv.symm (RestrictScalars.addEquiv k k[G] V.ρ.asModule) :
        (a : V.ρ.asModule) → RestrictScalars k k[G] V.ρ.asModule)
      (HSMul.hSMul (α := k[G]) (β := V.ρ.asModule) ((algebraMap k k[G] : (a : k) → k[G]) r : k[G])
        ((V.ρ.asModuleEquiv.symm : (a : (↑V : Type w)) → V.ρ.asModule) x : V.ρ.asModule)) =
    HSMul.hSMul (α := k) ((RingHom.id k : (a : k) → k) r : k) (Equiv.toFun (AddEquiv.toEquiv unitIsoAddEquiv) x)

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
V : Rep.{w, u, v} k G
g : G
h :
  ∀ (x : (↑V : Type w)),
    Eq (α := RestrictScalars k k[G] (↑(Functor.obj toModuleMonoidAlgebra V) : Type w))
      (((↑(let __src : (↑V : Type w) ≃+ (↑(Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) V) : Type w) :=
                    unitIsoAddEquiv;
                  { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
                    right_inv := ⋯ }) :
                (↑V : Type w) →ₗ[k] RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w)) ∘ₗ
              (V.ρ : (a : G) → (↑V : Type w) →ₗ[k] (↑V : Type w)) g :
            (a : (↑V : Type w)) → RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w))
          x :
        RestrictScalars k k[G] (↑(Functor.obj toModuleMonoidAlgebra V) : Type w))
      (((Representation.ofModule (↑(Functor.obj toModuleMonoidAlgebra V) : Type w) :
                  (a : G) →
                    RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w) →ₗ[k]
                      RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w))
                g ∘ₗ
              (↑(let __src :
                    (↑V : Type w) ≃+ (↑(Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) V) : Type w) :=
                    unitIsoAddEquiv;
                  { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
                    right_inv := ⋯ }) :
                (↑V : Type w) →ₗ[k] RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w)) :
            (a : (↑V : Type w)) → RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w))
          x :
        RestrictScalars k k[G] (↑(Functor.obj toModuleMonoidAlgebra V) : Type w))
⊢ Eq.{w + 1} (α := (↑V : Type w) →ₗ[k] RestrictScalars k k[G] (↑(Functor.obj toModuleMonoidAlgebra V) : Type w))
    ((↑(let __src : (↑V : Type w) ≃+ (↑(Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) V) : Type w) :=
            unitIsoAddEquiv;
          { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
            right_inv := ⋯ }) :
        (↑V : Type w) →ₗ[k] RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w)) ∘ₗ
      (V.ρ : (a : G) → (↑V : Type w) →ₗ[k] (↑V : Type w)) g)
    ((Representation.ofModule (↑(Functor.obj toModuleMonoidAlgebra V) : Type w) :
          (a : G) →
            RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w) →ₗ[k]
              RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w))
        g ∘ₗ
      (↑(let __src : (↑V : Type w) ≃+ (↑(Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) V) : Type w) :=
            unitIsoAddEquiv;
          { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
            right_inv := ⋯ }) :
        (↑V : Type w) →ₗ[k] RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w)))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
V : Rep.{w, u, v} k G
g : G
x : (↑V : Type w)
⊢ Eq (α := RestrictScalars k k[G] (↑(Functor.obj toModuleMonoidAlgebra V) : Type w))
    (((↑(let __src : (↑V : Type w) ≃+ (↑(Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) V) : Type w) :=
                  unitIsoAddEquiv;
                { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
                  right_inv := ⋯ }) :
              (↑V : Type w) →ₗ[k] RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w)) ∘ₗ
            (V.ρ : (a : G) → (↑V : Type w) →ₗ[k] (↑V : Type w)) g :
          (a : (↑V : Type w)) → RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w))
        x :
      RestrictScalars k k[G] (↑(Functor.obj toModuleMonoidAlgebra V) : Type w))
    (((Representation.ofModule (↑(Functor.obj toModuleMonoidAlgebra V) : Type w) :
                (a : G) →
                  RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w) →ₗ[k]
                    RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w))
              g ∘ₗ
            (↑(let __src :
                  (↑V : Type w) ≃+ (↑(Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) V) : Type w) :=
                  unitIsoAddEquiv;
                { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
                  right_inv := ⋯ }) :
              (↑V : Type w) →ₗ[k] RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w)) :
          (a : (↑V : Type w)) → RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w))
        x :
      RestrictScalars k k[G] (↑(Functor.obj toModuleMonoidAlgebra V) : Type w))

Tactic:
unit_iso_comm ..

Premises used: Representation.asModule, RestrictScalars, Rep.unit_iso_comm
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
V : Rep.{w, u, v} k G
g : G
x : (↑V : Type w)
⊢ Eq (α := RestrictScalars k k[G] (↑(Functor.obj toModuleMonoidAlgebra V) : Type w))
    (((↑(let __src : (↑V : Type w) ≃+ (↑(Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) V) : Type w) :=
                  unitIsoAddEquiv;
                { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
                  right_inv := ⋯ }) :
              (↑V : Type w) →ₗ[k] RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w)) ∘ₗ
            (V.ρ : (a : G) → (↑V : Type w) →ₗ[k] (↑V : Type w)) g :
          (a : (↑V : Type w)) → RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w))
        x :
      RestrictScalars k k[G] (↑(Functor.obj toModuleMonoidAlgebra V) : Type w))
    (((Representation.ofModule (↑(Functor.obj toModuleMonoidAlgebra V) : Type w) :
                (a : G) →
                  RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w) →ₗ[k]
                    RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w))
              g ∘ₗ
            (↑(let __src :
                  (↑V : Type w) ≃+ (↑(Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) V) : Type w) :=
                  unitIsoAddEquiv;
                { toFun := __src.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := __src.invFun, left_inv := ⋯,
                  right_inv := ⋯ }) :
              (↑V : Type w) →ₗ[k] RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w)) :
          (a : (↑V : Type w)) → RestrictScalars k k[G] (↑(toModuleMonoidAlgebra.obj V) : Type w))
        x :
      RestrictScalars k k[G] (↑(Functor.obj toModuleMonoidAlgebra V) : Type w))

Tactic:
exact unit_iso_comm ..

Premises used: Rep.unit_iso_comm
-- Module: Mathlib.RepresentationTheory.Rep.Iso
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  ∀ {X Y : Rep.{w, u, v} k G} (f : X ⟶ Y),
    Eq (α := Functor.obj (𝟭 (Rep.{w, u, v} k G)) X ⟶ Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) Y)
      (CategoryTheory.Functor.map (𝟭 (Rep.{w, u, v} k G)) f ≫ Iso.hom ((fun (V : Rep.{w, u, v} k G) ↦ V.unitIso) Y))
      (Iso.hom ((fun (V : Rep.{w, u, v} k G) ↦ V.unitIso) X) ≫
        CategoryTheory.Functor.map (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) f)
⊢ ∀ {X Y : Rep.{w, u, v} k G} (f : X ⟶ Y),
    Eq (α := Functor.obj (𝟭 (Rep.{w, u, v} k G)) X ⟶ Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) Y)
      (CategoryTheory.Functor.map (𝟭 (Rep.{w, u, v} k G)) f ≫ Iso.hom ((fun (V : Rep.{w, u, v} k G) ↦ V.unitIso) Y))
      (Iso.hom ((fun (V : Rep.{w, u, v} k G) ↦ V.unitIso) X) ≫
        CategoryTheory.Functor.map (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) f)

Tactic:
cat_disch