α : Type u_1
β : Type u_2
γ : Type ?u.172677
ι : Type ?u.172680
M : Type u_3
M' : Type ?u.172686
N : Type ?u.172689
P : Type ?u.172692
G : Type ?u.172695
H : Type ?u.172698
R : Type ?u.172701
S : Type ?u.172704
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α ≃ β
x : α →₀ M
a : β
⊢ ↑(mapDomain (↑f) x) (↑f (↑f.symm a)) = ↑x (↑f.symm a)
α : Type u_1
β : Type u_2
γ : Type ?u.172677
ι : Type ?u.172680
M : Type u_3
M' : Type ?u.172686
N : Type ?u.172689
P : Type ?u.172692
G : Type ?u.172695
H : Type ?u.172698
R : Type ?u.172701
S : Type ?u.172704
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α ≃ β
x : α →₀ M
a : β
⊢ ↑(mapDomain (↑f) x) a = ↑x (↑f.symm a)
conv_lhs => rw [← f.apply_symm_apply a]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.172677
ι : Type ?u.172680
M : Type u_3
M' : Type ?u.172686
N : Type ?u.172689
P : Type ?u.172692
G : Type ?u.172695
H : Type ?u.172698
R : Type ?u.172701
S : Type ?u.172704
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α ≃ β
x : α →₀ M
a : β
⊢ ↑(mapDomain (↑f) x) (↑f (↑f.symm a)) = ↑x (↑f.symm a)
exact mapDomain_apply f.injective _ _