awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A_1 B_1 C_1 : Rep.{w, u, v} k G
A B C : Rep k G
f : tensorObj (𝒞 := instCategory) A B ⟶ C
g : G
x : (↑B : Type u)
y : (↑A : Type u)
⊢ Eq (α := (↑C : Type u))
    (((((TensorProduct.curry (Hom.hom f).toLinearMap).flip ∘ₗ (B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g :
                (a : (↑B : Type u)) → (↑A : Type u) →ₗ[k] (↑C : Type u))
              x :
            (↑A : Type u) →ₗ[k] (↑C : Type u)) :
          (a : (↑A : Type u)) → (↑C : Type u))
        y :
      (↑C : Type u))
    (((((A.ρ.linHom C.ρ : (a : G) → ((↑A : Type u) →ₗ[k] (↑C : Type u)) →ₗ[k] (↑A : Type u) →ₗ[k] (↑C : Type u)) g ∘ₗ
                  (TensorProduct.curry (Hom.hom f).toLinearMap).flip :
                (a : (↑B : Type u)) → (↑A : Type u) →ₗ[k] (↑C : Type u))
              x :
            (↑A : Type u) →ₗ[k] (↑C : Type u)) :
          (a : (↑A : Type u)) → (↑C : Type u))
        y :
      (↑C : Type u))
have h : Eq (α := (↑C : Type u))
  ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
      (y ⊗ₜ[k]
          (((B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g : (↑B : Type u) →ₗ[k] (↑B : Type u)) :
              (a : (↑B : Type u)) → (↑B : Type u))
            x :
        TensorProduct k (↑A : Type u) (↑B : Type u)) :
    (↑C : Type u))
  ((((C.ρ : (a : G) → (↑C : Type u) →ₗ[k] (↑C : Type u)) g : (↑C : Type u) →ₗ[k] (↑C : Type u)) :
        (a : (↑C : Type u)) → (↑C : Type u))
      ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                y ⊗ₜ[k]
              x :
            TensorProduct k (↑A : Type u) (↑B : Type u)) :
        (↑C : Type u)) :
    (↑C : Type u))
Tactic: simp only [tensor_V, tensor_ρ, LinearMap.coe_comp, Function.comp_apply, LinearMap.flip_apply,
      TensorProduct.curry_apply, Representation.IntertwiningMap.toLinearMap_apply,
      Representation.linHom_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (hypothesis)
Goal:
k : Type u
G_1 : Type v
inst : CommRing k
inst_1 : Monoid G_1
G : Type v
inst_2 : Group G
A_1 B_1 C_1 : Rep.{w, u, v} k G
A B C : Rep k G
f : tensorObj (𝒞 := instCategory) A B ⟶ C
g : G
x : (↑B : Type u)
y : (↑A : Type u)
⊢ Eq (α := (↑C : Type u))
    ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
        (y ⊗ₜ[k]
            (((B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g : (↑B : Type u) →ₗ[k] (↑B : Type u)) :
                (a : (↑B : Type u)) → (↑B : Type u))
              x :
          TensorProduct k (↑A : Type u) (↑B : Type u)) :
      (↑C : Type u))
    ((((C.ρ : (a : G) → (↑C : Type u) →ₗ[k] (↑C : Type u)) g : (↑C : Type u) →ₗ[k] (↑C : Type u)) :
          (a : (↑C : Type u)) → (↑C : Type u))
        ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
            ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                    (a : (↑A : Type u)) → (↑A : Type u))
                  y ⊗ₜ[k]
                x :
              TensorProduct k (↑A : Type u) (↑B : Type u)) :
          (↑C : Type u)) :
      (↑C : Type u))
have this : Eq (α := (↑C : Type u))
  ((((C.ρ : (a : G) → (↑C : Type u) →ₗ[k] (↑C : Type u)) g : (↑C : Type u) →ₗ[k] (↑C : Type u)) :
        (a : (↑C : Type u)) → (↑C : Type u))
      ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
          ((((A.ρ : (a : G) → (↑A : Type u) →ₗ[k] (↑A : Type u)) g⁻¹ : (↑A : Type u) →ₗ[k] (↑A : Type u)) :
                  (a : (↑A : Type u)) → (↑A : Type u))
                y ⊗ₜ[k]
              x :
            TensorProduct k (↑A : Type u) (↑B : Type u)) :
        (↑C : Type u)) :
    (↑C : Type u))
  ((Hom.hom f : (a : TensorProduct k (↑A : Type u) (↑B : Type u)) → (↑C : Type u))
      (y ⊗ₜ[k]
          (((B.ρ : (a : G) → (↑B : Type u) →ₗ[k] (↑B : Type u)) g : (↑B : Type u) →ₗ[k] (↑B : Type u)) :
              (a : (↑B : Type u)) → (↑B : Type u))
            x :
        TensorProduct k (↑A : Type u) (↑B : Type u)) :
    (↑C : Type u))
Tactic: have := by simpa using (hom_comm_apply f g (A.ρ g⁻¹ y ⊗ₜ[k] x)).symm
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
A B : Rep k G
⊢ Eq (α := (↑(Functor.obj (ihom A ⋙ tensorLeft A) B) : Type u) →ₗ[k] (↑(Functor.obj (𝟭 (Rep k G)) B) : Type u))
    (Representation.IntertwiningMap.toLinearMap (Hom.hom (NatTrans.app (ihom.ev A) B)))
    ((TensorProduct.uncurry (RingHom.id k) (↑A : Type u) ((↑A : Type u) →ₗ[k] (↑B : Type u)) (↑B : Type u) :
        (a : (↑A : Type u) →ₗ[k] ((↑A : Type u) →ₗ[k] (↑B : Type u)) →ₗ[k] (↑B : Type u)) →
          TensorProduct k (↑A : Type u) ((↑A : Type u) →ₗ[k] (↑B : Type u)) →ₗ[k] (↑B : Type u))
      (LinearMap.flip LinearMap.id))
have h : ∀ (x : (↑(Functor.obj (ihom A ⋙ tensorLeft A) B) : Type u)),
  Eq (α := (↑(Functor.obj (𝟭 (Rep k G)) B) : Type u))
    ((Representation.IntertwiningMap.toLinearMap (Hom.hom (NatTrans.app (ihom.ev A) B)) :
          (a : (↑((ihom A ⋙ tensorLeft A).obj B) : Type u)) → (↑((𝟭 (Rep k G)).obj B) : Type u))
        x :
      (↑(Functor.obj (𝟭 (Rep k G)) B) : Type u))
    ((((TensorProduct.uncurry (RingHom.id k) (↑A : Type u) ((↑A : Type u) →ₗ[k] (↑B : Type u)) (↑B : Type u) :
                (a : (↑A : Type u) →ₗ[k] ((↑A : Type u) →ₗ[k] (↑B : Type u)) →ₗ[k] (↑B : Type u)) →
                  TensorProduct k (↑A : Type u) ((↑A : Type u) →ₗ[k] (↑B : Type u)) →ₗ[k] (↑B : Type u))
              (LinearMap.flip LinearMap.id) :
            TensorProduct k (↑A : Type u) ((↑A : Type u) →ₗ[k] (↑B : Type u)) →ₗ[k] (↑B : Type u)) :
          (a : (↑((ihom A ⋙ tensorLeft A).obj B) : Type u)) → (↑((𝟭 (Rep k G)).obj B) : Type u))
        x :
      (↑(Functor.obj (𝟭 (Rep k G)) B) : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
A B C : Rep k G
f : B ⟶ Functor.obj (ihom A) C
⊢ Eq.{u + 1} (α := (↑(tensorObj (𝒞 := instCategory) A B) : Type u) →ₗ[k] (↑C : Type u))
    (Representation.IntertwiningMap.toLinearMap
      (Hom.hom (((linearHomEquiv A B C).symm : (a : B ⟶ (ihom A).obj C) → A ⊗ B ⟶ C) f)))
    ((TensorProduct.uncurry (RingHom.id k) (↑A : Type u) (↑B : Type u) (↑C : Type u) :
        (a : (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] (↑C : Type u)) →
          TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
      (Hom.hom f).flip)
have simp : Eq.{u + 1} (α := TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
  (Representation.IntertwiningMap.toLinearMap.{u, v, u, u} (G := G) (ρ := A.ρ.tprod B.ρ) (σ := C.ρ)
      (Hom.hom (((A.tensorHomEquiv B C).symm : (a : B ⟶ (ihom A).obj C) → A ⊗ B ⟶ C) f)) :
    TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
  ((TensorProduct.uncurry (RingHom.id k) (↑A : Type u) (↑B : Type u) (↑C : Type u) :
        (a : (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] (↑C : Type u)) →
          TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
      (Hom.hom f).flip :
    TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
Tactic: simp [linearHomEquiv]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k_1 : Type u
G_1 : Type v
inst : CommRing k_1
inst_1 : Monoid G_1
k : Type u
inst_2 : Semiring k
G : Type v
inst_3 : Group G
inst_4 : Fintype G
A : Rep.{w, u, v} k G
g : G
⊢ A.ρ.norm ∘ₗ (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g =
    (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g ∘ₗ A.ρ.norm
have h : ∀ (x : (↑A : Type w)),
  Eq (α := (↑A : Type w))
    ((A.ρ.norm ∘ₗ (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g : (a : (↑A : Type w)) → (↑A : Type w)) x :
      (↑A : Type w))
    (((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g ∘ₗ A.ρ.norm : (a : (↑A : Type w)) → (↑A : Type w)) x :
      (↑A : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
A B : Rep.{u_1, u, v} k G
f : A ⟶ B
⊢ f ≫ B.norm = A.norm ≫ f
have hf : ∀ (x : (↑A : Type u_1)),
  Eq (α := (↑B : Type u_1))
    (((Hom.hom (f ≫ B.norm)).toLinearMap : (a : (↑A : Type u_1)) → (↑B : Type u_1)) x : (↑B : Type u_1))
    (((Hom.hom (A.norm ≫ f)).toLinearMap : (a : (↑A : Type u_1)) → (↑B : Type u_1)) x : (↑B : Type u_1))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Action (Type u) G
f : X ⟶ Y
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G)
      (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X))
      (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)))
    (Functor.obj (linearization k G) Z ◁ CategoryTheory.Functor.map (linearization k G) f ≫ ofHom (μ Z Y) :
      Quiver.Hom (V := Rep k G)
        (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X))
        (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)))
    (ofHom (μ Z X) ≫ CategoryTheory.Functor.map (linearization k G) (Z ◁ f) :
      Quiver.Hom (V := Rep k G)
        (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X))
        (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)))
have hf : Eq (α :=
  Representation.IntertwiningMap (V :=
    (↑(tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)) : Type u))
    (W := (↑(Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)) : Type u))
    (ρ (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)))
    (ρ (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y))))
  (Hom.hom (Functor.obj (linearization k G) Z ◁ CategoryTheory.Functor.map (linearization k G) f ≫ ofHom (μ Z Y)) :
    Representation.IntertwiningMap (V :=
      (↑(tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)) :
        Type u))
      (W := (↑(Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)) : Type u))
      (ρ (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)))
      (ρ (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y))))
  (Hom.hom (ofHom (μ Z X) ≫ CategoryTheory.Functor.map (linearization k G) (Z ◁ f)) :
    Representation.IntertwiningMap (V :=
      (↑(tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)) :
        Type u))
      (W := (↑(Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)) : Type u))
      (ρ (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)))
      (ρ (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y))))
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Basic (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Action (Type u) G
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G)
      (tensorObj (𝒞 := instCategory)
        (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y))
        (Functor.obj (linearization k G) Z))
      (Functor.obj (linearization k G)
        (tensorObj (𝒞 := Action.instCategory) X (tensorObj (𝒞 := Action.instCategory) Y Z))))
    (CategoryStruct.comp (Y :=
      tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) X Y))
        (Functor.obj (linearization k G) Z))
      (ofHom (μ X Y) ▷ Functor.obj (linearization k G) Z)
      (ofHom (μ (tensorObj (𝒞 := Action.instCategory) X Y) Z) ≫
        CategoryTheory.Functor.map (linearization k G) (Iso.hom (α_ X Y Z))))
    (Iso.hom
        (α_ (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y)
          (Functor.obj (linearization k G) Z)) ≫
      CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X)
          (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Y Z)))
        (Functor.obj (linearization k G) X ◁ ofHom (μ Y Z)) (ofHom (μ X (tensorObj (𝒞 := Action.instCategory) Y Z))))
have hf : Eq (α :=
  Representation.IntertwiningMap (V :=
    (↑(tensorObj (𝒞 := instCategory)
          (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y))
          (Functor.obj (linearization k G) Z)) :
      Type u))
    (W :=
    (↑(Functor.obj (linearization k G)
          (tensorObj (𝒞 := Action.instCategory) X (tensorObj (𝒞 := Action.instCategory) Y Z))) :
      Type u))
    (ρ
      (tensorObj (𝒞 := instCategory)
        (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y))
        (Functor.obj (linearization k G) Z)))
    (ρ
      (Functor.obj (linearization k G)
        (tensorObj (𝒞 := Action.instCategory) X (tensorObj (𝒞 := Action.instCategory) Y Z)))))
  (Hom.hom
    (CategoryStruct.comp (Y :=
      tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) X Y))
        (Functor.obj (linearization k G) Z))
      (ofHom (μ X Y) ▷ Functor.obj (linearization k G) Z)
      (ofHom (μ (tensorObj (𝒞 := Action.instCategory) X Y) Z) ≫
        CategoryTheory.Functor.map (linearization k G) (Iso.hom (α_ X Y Z)))))
  (Hom.hom
    (Iso.hom
        (α_ (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y)
          (Functor.obj (linearization k G) Z)) ≫
      CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X)
          (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Y Z)))
        (Functor.obj (linearization k G) X ◁ ofHom (μ Y Z)) (ofHom (μ X (tensorObj (𝒞 := Action.instCategory) Y Z)))))
Tactic: ext1
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
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
⊢ 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 :
                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 :
            W →ₗ[k] W) :
          (a : W) → W)
        ((f : (a : V) → W) x : W) :
      W)
have hM : ∀ (m : G),
  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]) m) :
                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]) m) :
            W →ₗ[k] W) :
          (a : W) → W)
        ((f : (a : V) → W) x : W) :
      W)
Tactic: apply MonoidAlgebra.induction_on r
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
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)
        ((((((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)
have 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)
Tactic: simp only [one_smul, MonoidAlgebra.lift_single, MonoidAlgebra.of_apply]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : ModuleCat k[G]
f : X ⟶ Y
g : G
⊢ 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' := ⋯ })
have 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' := sorry } ∘ₗ
            (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' := sorry } :
          (a : RestrictScalars k k[G] (↑X : Type w)) → RestrictScalars k k[G] (↑Y : Type w))
        x :
      RestrictScalars k k[G] (↑Y : Type w))
Tactic: ext
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
M : ModuleCat k[G]
⊢ (↑(Functor.obj (ofModuleMonoidAlgebra ⋙ toModuleMonoidAlgebra) M) : Type w) ≃+ (↑M : Type w)
have 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)
Tactic: dsimp [ofModuleMonoidAlgebra, toModuleMonoidAlgebra]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
V : Rep.{w, u, v} k G
⊢ (↑V : Type w) ≃+ (↑(Functor.obj (toModuleMonoidAlgebra ⋙ ofModuleMonoidAlgebra) V) : Type w)
have dsimp : (↑V : Type w) ≃+ RestrictScalars k k[G] V.ρ.asModule
Tactic: dsimp [ofModuleMonoidAlgebra, toModuleMonoidAlgebra]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
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)
      ((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)
have 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)
Tactic: simp only [Representation.asModuleEquiv_symm_map_smul]
-- Lean 4 proof step from Mathlib.RepresentationTheory.Rep.Iso (goal)
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
V : Rep.{w, u, v} k G
g : G
⊢ 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)))
have 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' := sorry, map_smul' := sorry, invFun := __src.invFun, left_inv := sorry,
                  right_inv := sorry }) :
              (↑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' := sorry, map_smul' := sorry, invFun := __src.invFun, left_inv := sorry,
                  right_inv := sorry }) :
              (↑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: ext