case h
α : Type u_1
β : Type u_2
γ : Type ?u.236087
ι : Type ?u.236090
M : Type u_3
M' : Type ?u.236096
N : Type u_4
P : Type ?u.236102
G : Type ?u.236105
H : Type ?u.236108
R : Type ?u.236111
S : Type ?u.236114
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
⊢ ↑(embDomain f (mapRange g hg p)) a = ↑(mapRange g hg (embDomain f p)) a
α : Type u_1
β : Type u_2
γ : Type ?u.236087
ι : Type ?u.236090
M : Type u_3
M' : Type ?u.236096
N : Type u_4
P : Type ?u.236102
G : Type ?u.236105
H : Type ?u.236108
R : Type ?u.236111
S : Type ?u.236114
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
⊢ embDomain f (mapRange g hg p) = mapRange g hg (embDomain f p)
ext a
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.236087
ι : Type ?u.236090
M : Type u_3
M' : Type ?u.236096
N : Type u_4
P : Type ?u.236102
G : Type ?u.236105
H : Type ?u.236108
R : Type ?u.236111
S : Type ?u.236114
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
h : a ∈ Set.range ↑f
⊢ ↑(embDomain f (mapRange g hg p)) a = ↑(mapRange g hg (embDomain f p)) a

case neg
α : Type u_1
β : Type u_2
γ : Type ?u.236087
ι : Type ?u.236090
M : Type u_3
M' : Type ?u.236096
N : Type u_4
P : Type ?u.236102
G : Type ?u.236105
H : Type ?u.236108
R : Type ?u.236111
S : Type ?u.236114
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
h : ¬a ∈ Set.range ↑f
⊢ ↑(embDomain f (mapRange g hg p)) a = ↑(mapRange g hg (embDomain f p)) a
case h
α : Type u_1
β : Type u_2
γ : Type ?u.236087
ι : Type ?u.236090
M : Type u_3
M' : Type ?u.236096
N : Type u_4
P : Type ?u.236102
G : Type ?u.236105
H : Type ?u.236108
R : Type ?u.236111
S : Type ?u.236114
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
⊢ ↑(embDomain f (mapRange g hg p)) a = ↑(mapRange g hg (embDomain f p)) a
by_cases h : a ∈ Set.range f
case pos.intro
α : Type u_1
β : Type u_2
γ : Type ?u.236087
ι : Type ?u.236090
M : Type u_3
M' : Type ?u.236096
N : Type u_4
P : Type ?u.236102
G : Type ?u.236105
H : Type ?u.236108
R : Type ?u.236111
S : Type ?u.236114
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a' : α
⊢ ↑(embDomain f (mapRange g hg p)) (↑f a') = ↑(mapRange g hg (embDomain f p)) (↑f a')
case pos
α : Type u_1
β : Type u_2
γ : Type ?u.236087
ι : Type ?u.236090
M : Type u_3
M' : Type ?u.236096
N : Type u_4
P : Type ?u.236102
G : Type ?u.236105
H : Type ?u.236108
R : Type ?u.236111
S : Type ?u.236114
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
h : a ∈ Set.range ↑f
⊢ ↑(embDomain f (mapRange g hg p)) a = ↑(mapRange g hg (embDomain f p)) a
rcases h with ⟨a', rfl⟩
no goals
case pos.intro
α : Type u_1
β : Type u_2
γ : Type ?u.236087
ι : Type ?u.236090
M : Type u_3
M' : Type ?u.236096
N : Type u_4
P : Type ?u.236102
G : Type ?u.236105
H : Type ?u.236108
R : Type ?u.236111
S : Type ?u.236114
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a' : α
⊢ ↑(embDomain f (mapRange g hg p)) (↑f a') = ↑(mapRange g hg (embDomain f p)) (↑f a')
rw [mapRange_apply, embDomain_apply, embDomain_apply, mapRange_apply]
no goals
case neg
α : Type u_1
β : Type u_2
γ : Type ?u.236087
ι : Type ?u.236090
M : Type u_3
M' : Type ?u.236096
N : Type u_4
P : Type ?u.236102
G : Type ?u.236105
H : Type ?u.236108
R : Type ?u.236111
S : Type ?u.236114
inst✝¹ : Zero M
inst✝ : Zero N
f : α ↪ β
g : M → N
p : α →₀ M
hg : g 0 = 0
a : β
h : ¬a ∈ Set.range ↑f
⊢ ↑(embDomain f (mapRange g hg p)) a = ↑(mapRange g hg (embDomain f p)) a
rw [mapRange_apply, embDomain_notin_range, embDomain_notin_range, ← hg] <;> assumption