case coeff.h
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : embDomain f x = embDomain f y
g : Γ
⊢ coeff x g = coeff y g
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : embDomain f x = embDomain f y
⊢ x = y
ext g
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : ∀ (a : Γ'), coeff (embDomain f x) a = coeff (embDomain f y) a
g : Γ
⊢ coeff x g = coeff y g
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : embDomain f x = embDomain f y
g : Γ
⊢ coeff x g = coeff y g
rw [HahnSeries.ext_iff, Function.funext_iff] at xy
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : ∀ (a : Γ'), coeff (embDomain f x) a = coeff (embDomain f y) a
g : Γ
xyg : coeff (embDomain f x) (↑f g) = coeff (embDomain f y) (↑f g)
⊢ coeff x g = coeff y g
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : ∀ (a : Γ'), coeff (embDomain f x) a = coeff (embDomain f y) a
g : Γ
⊢ coeff x g = coeff y g
have xyg := xy (f g)
no goals
case coeff.h
Γ : Type u_1
R : Type u_3
inst✝² : PartialOrder Γ
inst✝¹ : Zero R
a b : Γ
r : R
Γ' : Type u_2
inst✝ : PartialOrder Γ'
f : Γ ↪o Γ'
x y : HahnSeries Γ R
xy : ∀ (a : Γ'), coeff (embDomain f x) a = coeff (embDomain f y) a
g : Γ
xyg : coeff (embDomain f x) (↑f g) = coeff (embDomain f y) (↑f g)
⊢ coeff x g = coeff y g
rwa [embDomain_coeff, embDomain_coeff] at xyg