case h
α : Type u_1
β : Type u_2
γ : Type ?u.226928
ι : Type ?u.226931
M : Type u_3
M' : Type ?u.226937
N : Type ?u.226940
P : Type ?u.226943
G : Type ?u.226946
H : Type ?u.226949
R : Type ?u.226952
S : Type ?u.226955
inst✝ : AddCommMonoid M
v✝ v₁ v₂ : α →₀ M
f : α ↪ β
v : α →₀ M
a : β
⊢ ↑(embDomain f v) a = ↑(mapDomain (↑f) v) a
α : Type u_1
β : Type u_2
γ : Type ?u.226928
ι : Type ?u.226931
M : Type u_3
M' : Type ?u.226937
N : Type ?u.226940
P : Type ?u.226943
G : Type ?u.226946
H : Type ?u.226949
R : Type ?u.226952
S : Type ?u.226955
inst✝ : AddCommMonoid M
v✝ v₁ v₂ : α →₀ M
f : α ↪ β
v : α →₀ M
⊢ embDomain f v = mapDomain (↑f) v
ext a
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.226928
ι : Type ?u.226931
M : Type u_3
M' : Type ?u.226937
N : Type ?u.226940
P : Type ?u.226943
G : Type ?u.226946
H : Type ?u.226949
R : Type ?u.226952
S : Type ?u.226955
inst✝ : AddCommMonoid M
v✝ v₁ v₂ : α →₀ M
f : α ↪ β
v : α →₀ M
a : β
h : a ∈ Set.range ↑f
⊢ ↑(embDomain f v) a = ↑(mapDomain (↑f) v) a

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.226928
ι : Type ?u.226931
M : Type u_3
M' : Type ?u.226937
N : Type ?u.226940
P : Type ?u.226943
G : Type ?u.226946
H : Type ?u.226949
R : Type ?u.226952
S : Type ?u.226955
inst✝ : AddCommMonoid M
v✝ v₁ v₂ : α →₀ M
f : α ↪ β
v : α →₀ M
a : β
h : ¬a ∈ Set.range ↑f
⊢ ↑(embDomain f v) a = ↑(mapDomain (↑f) v) a
case h
α : Type u_1
β : Type u_2
γ : Type ?u.226928
ι : Type ?u.226931
M : Type u_3
M' : Type ?u.226937
N : Type ?u.226940
P : Type ?u.226943
G : Type ?u.226946
H : Type ?u.226949
R : Type ?u.226952
S : Type ?u.226955
inst✝ : AddCommMonoid M
v✝ v₁ v₂ : α →₀ M
f : α ↪ β
v : α →₀ M
a : β
⊢ ↑(embDomain f v) a = ↑(mapDomain (↑f) v) a
by_cases h : a ∈ Set.range f
case pos.intro
α : Type u_1
β : Type u_2
γ : Type ?u.226928
ι : Type ?u.226931
M : Type u_3
M' : Type ?u.226937
N : Type ?u.226940
P : Type ?u.226943
G : Type ?u.226946
H : Type ?u.226949
R : Type ?u.226952
S : Type ?u.226955
inst✝ : AddCommMonoid M
v✝ v₁ v₂ : α →₀ M
f : α ↪ β
v : α →₀ M
a : α
⊢ ↑(embDomain f v) (↑f a) = ↑(mapDomain (↑f) v) (↑f a)
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.226928
ι : Type ?u.226931
M : Type u_3
M' : Type ?u.226937
N : Type ?u.226940
P : Type ?u.226943
G : Type ?u.226946
H : Type ?u.226949
R : Type ?u.226952
S : Type ?u.226955
inst✝ : AddCommMonoid M
v✝ v₁ v₂ : α →₀ M
f : α ↪ β
v : α →₀ M
a : β
h : a ∈ Set.range ↑f
⊢ ↑(embDomain f v) a = ↑(mapDomain (↑f) v) a
rcases h with ⟨a, rfl⟩
no goals
case pos.intro
α : Type u_1
β : Type u_2
γ : Type ?u.226928
ι : Type ?u.226931
M : Type u_3
M' : Type ?u.226937
N : Type ?u.226940
P : Type ?u.226943
G : Type ?u.226946
H : Type ?u.226949
R : Type ?u.226952
S : Type ?u.226955
inst✝ : AddCommMonoid M
v✝ v₁ v₂ : α →₀ M
f : α ↪ β
v : α →₀ M
a : α
⊢ ↑(embDomain f v) (↑f a) = ↑(mapDomain (↑f) v) (↑f a)
rw [mapDomain_apply f.injective, embDomain_apply]
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.226928
ι : Type ?u.226931
M : Type u_3
M' : Type ?u.226937
N : Type ?u.226940
P : Type ?u.226943
G : Type ?u.226946
H : Type ?u.226949
R : Type ?u.226952
S : Type ?u.226955
inst✝ : AddCommMonoid M
v✝ v₁ v₂ : α →₀ M
f : α ↪ β
v : α →₀ M
a : β
h : ¬a ∈ Set.range ↑f
⊢ ↑(embDomain f v) a = ↑(mapDomain (↑f) v) a
rw [mapDomain_notin_range, embDomain_notin_range] <;> assumption