no goals
k : Type u
inst✝⁹ : CommRing k
G : Type u
inst✝⁸ : Group G
V : Type v
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module (MonoidAlgebra k G) V
inst✝⁴ : IsScalarTower k (MonoidAlgebra k G) V
W : Type w
inst✝³ : AddCommGroup W
inst✝² : Module k W
inst✝¹ : Module (MonoidAlgebra k G) W
inst✝ : IsScalarTower k (MonoidAlgebra k G) W
π : W →ₗ[k] V
i : V →ₗ[MonoidAlgebra k G] W
h : ∀ (v : V), ↑π (↑i v) = v
g : G
v : V
⊢ ↑(conjugate π g) (↑i v) = v
rw [conjugate_apply, ← i.map_smul, h, ← mul_smul, single_mul_single, mul_one, mul_left_inv,
  ← one_def, one_smul]