case coeff.h
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
g : Γ'
⊢ coeff (embDomain f (x + y)) g = coeff (embDomain f x + embDomain f y) g
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
⊢ embDomain f (x + y) = embDomain f x + embDomain f y
ext g
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
g : Γ'
hg : g ∈ Set.range ↑f
⊢ coeff (embDomain f (x + y)) g = coeff (embDomain f x + embDomain f y) g

case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
g : Γ'
hg : ¬g ∈ Set.range ↑f
⊢ coeff (embDomain f (x + y)) g = coeff (embDomain f x + embDomain f y) g
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
g : Γ'
⊢ coeff (embDomain f (x + y)) g = coeff (embDomain f x + embDomain f y) g
by_cases hg : g ∈ Set.range f
case pos.intro
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
a : Γ
⊢ coeff (embDomain f (x + y)) (↑f a) = coeff (embDomain f x + embDomain f y) (↑f a)
case pos
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
g : Γ'
hg : g ∈ Set.range ↑f
⊢ coeff (embDomain f (x + y)) g = coeff (embDomain f x + embDomain f y) g
obtain ⟨a, rfl⟩ := hg
no goals
case pos.intro
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
a : Γ
⊢ coeff (embDomain f (x + y)) (↑f a) = coeff (embDomain f x + embDomain f y) (↑f a)
simp
no goals
case neg
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
g : Γ'
hg : ¬g ∈ Set.range ↑f
⊢ coeff (embDomain f (x + y)) g = coeff (embDomain f x + embDomain f y) g
simp [embDomain_notin_range hg]