-- Mathlib/RepresentationTheory/Basic.lean
theorem ofMulAction_self_smul_eq_mul (x : MonoidAlgebra k G) (y : (ofMulAction k G G).asModule) :
    x • y = (x * y : MonoidAlgebra k G) := -- by
  -- Porting note: trouble figuring out the motive
  x.induction_on (p := fun z => z • y = z * y)
    (fun g => by
      show asAlgebraHom (ofMulAction k G G) _ _ = _; ext
      simp only [MonoidAlgebra.of_apply, asAlgebraHom_single, one_smul,
        ofMulAction_apply, smul_eq_mul]
      -- Porting note: single_mul_apply not firing in simp
      rw [MonoidAlgebra.single_mul_apply, one_mul]
    )
    (fun x y hx hy => by simp only [hx, hy, add_mul, add_smul]) fun r x hx => by
    show asAlgebraHom (ofMulAction k G G) _ _ = _  -- Porting note: was simpa [← hx]
    simp only [map_smul, smul_apply, Algebra.smul_mul_assoc]
    rw [← hx]
    rfl

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
g : G
⊢ (fun z => z • y = z * y) ((of k G) g)

Tactic:
show asAlgebraHom (ofMulAction k G G) _ _ = _

Result:
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
g : G
⊢ ((ofMulAction k G G).asAlgebraHom ((of k G) g)) y = (of k G) g * y

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x✝ : MonoidAlgebra k G
y✝ : (ofMulAction k G G).asModule
x y : MonoidAlgebra k G
hx : (fun z => z • y✝ = z * y✝) x
hy : (fun z => z • y✝ = z * y✝) y
⊢ (fun z => z • y✝ = z * y✝) (x + y)

Tactic:
simp only [hx, hy, add_mul, add_smul]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x✝ : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ ((ofMulAction k G G).asAlgebraHom (r • x)) y = r • x * y

Tactic:
simp only [map_smul, smul_apply, Algebra.smul_mul_assoc]

Result:
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x✝ : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ r • ((ofMulAction k G G).asAlgebraHom x) y = r • (x * y)

Proof state:
case h
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
g a✝ : G
⊢ y (g⁻¹ * a✝) = (MonoidAlgebra.single g 1 * y) a✝

Tactic:
rw [MonoidAlgebra.single_mul_apply, one_mul]

Result:
no goals

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
g : G
⊢ ((ofMulAction k G G).asAlgebraHom ((of k G) g)) y = (of k G) g * y

Tactic:
ext

Result:
case h
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
g a✝ : G
⊢ (((ofMulAction k G G).asAlgebraHom ((of k G) g)) y) a✝ = ((of k G) g * y) a✝

Proof state:
case h
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
g a✝ : G
⊢ (((ofMulAction k G G).asAlgebraHom ((of k G) g)) y) a✝ = ((of k G) g * y) a✝

Tactic:
simp only [MonoidAlgebra.of_apply, asAlgebraHom_single, one_smul,
  ofMulAction_apply, smul_eq_mul]

Result:
case h
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
g a✝ : G
⊢ y (g⁻¹ * a✝) = (MonoidAlgebra.single g 1 * y) a✝

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x✝ : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ r • ((ofMulAction k G G).asAlgebraHom x) y = r • (x * y)

Tactic:
rw [← hx]

Result:
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x✝ : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ r • ((ofMulAction k G G).asAlgebraHom x) y = r • x • y

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x✝ : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ (fun z => z • y = z * y) (r • x)

Tactic:
show asAlgebraHom (ofMulAction k G G) _ _ = _

Result:
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x✝ : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ ((ofMulAction k G G).asAlgebraHom (r • x)) y = r • x * y

Proof state:
k : Type u_1
G : Type u_2
inst✝¹ : CommSemiring k
inst✝ : Group G
x✝ : MonoidAlgebra k G
y : (ofMulAction k G G).asModule
r : k
x : MonoidAlgebra k G
hx : (fun z => z • y = z * y) x
⊢ r • ((ofMulAction k G G).asAlgebraHom x) y = r • x • y

Tactic:
rfl

Result:
no goals