α : Type u_1
β : Type ?u.593102
γ : Type ?u.593105
ι : Type ?u.593108
M : Type u_2
M' : Type ?u.593114
N : Type ?u.593117
P : Type ?u.593120
G : Type u_3
H : Type ?u.593126
R : Type ?u.593129
S : Type ?u.593132
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f : α →₀ M
a : α
⊢ ↑(g • f) (g • g⁻¹ • a) = ↑f (g⁻¹ • a)
α : Type u_1
β : Type ?u.593102
γ : Type ?u.593105
ι : Type ?u.593108
M : Type u_2
M' : Type ?u.593114
N : Type ?u.593117
P : Type ?u.593120
G : Type u_3
H : Type ?u.593126
R : Type ?u.593129
S : Type ?u.593132
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f : α →₀ M
a : α
⊢ ↑(g • f) a = ↑f (g⁻¹ • a)
conv_lhs => rw [← smul_inv_smul g a]
no goals
α : Type u_1
β : Type ?u.593102
γ : Type ?u.593105
ι : Type ?u.593108
M : Type u_2
M' : Type ?u.593114
N : Type ?u.593117
P : Type ?u.593120
G : Type u_3
H : Type ?u.593126
R : Type ?u.593129
S : Type ?u.593132
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : AddCommMonoid M
g : G
f : α →₀ M
a : α
⊢ ↑(g • f) (g • g⁻¹ • a) = ↑f (g⁻¹ • a)
exact mapDomain_apply (MulAction.injective g) _ (g⁻¹ • a)