case h
α : Type u_2
β : Type u_3
γ : Type ?u.296865
ι : Type ?u.296868
M✝ : Type ?u.296871
M' : Type ?u.296874
N : Type ?u.296877
P : Type ?u.296880
G : Type ?u.296883
H : Type ?u.296886
R : Type ?u.296889
S : Type ?u.296892
inst✝¹ : AddCommMonoid M✝
v v₁ v₂ : α →₀ M✝
M : Type u_1
inst✝ : AddCommMonoid M
f : α ≃ β
l : α →₀ M
x : β
⊢ ↑(equivMapDomain f l) x = ↑(mapDomain (↑f) l) x
α : Type u_2
β : Type u_3
γ : Type ?u.296865
ι : Type ?u.296868
M✝ : Type ?u.296871
M' : Type ?u.296874
N : Type ?u.296877
P : Type ?u.296880
G : Type ?u.296883
H : Type ?u.296886
R : Type ?u.296889
S : Type ?u.296892
inst✝¹ : AddCommMonoid M✝
v v₁ v₂ : α →₀ M✝
M : Type u_1
inst✝ : AddCommMonoid M
f : α ≃ β
l : α →₀ M
⊢ equivMapDomain f l = mapDomain (↑f) l
ext x
no goals
case h
α : Type u_2
β : Type u_3
γ : Type ?u.296865
ι : Type ?u.296868
M✝ : Type ?u.296871
M' : Type ?u.296874
N : Type ?u.296877
P : Type ?u.296880
G : Type ?u.296883
H : Type ?u.296886
R : Type ?u.296889
S : Type ?u.296892
inst✝¹ : AddCommMonoid M✝
v v₁ v₂ : α →₀ M✝
M : Type u_1
inst✝ : AddCommMonoid M
f : α ≃ β
l : α →₀ M
x : β
⊢ ↑(equivMapDomain f l) x = ↑(mapDomain (↑f) l) x
simp [mapDomain_equiv_apply]