Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
g : Γ'
hg : g ∈ support (embDomain f x)
⊢ g ∈ ↑f '' support x
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
⊢ support (embDomain f x) ⊆ ↑f '' support x
intro g hg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
g : Γ'
hg : ¬g ∈ (fun a => ↑f a) '' support x
⊢ ¬g ∈ support (embDomain f x)
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
g : Γ'
hg : g ∈ support (embDomain f x)
⊢ g ∈ ↑f '' support x
contrapose! hg
no goals
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x : HahnSeries Γ R
g : Γ'
hg : ¬g ∈ (fun a => ↑f a) '' support x
⊢ ¬g ∈ support (embDomain f x)
rw [mem_support, embDomain_notin_image_support hg, Classical.not_not]