Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : ↑C r = ↑C s
⊢ r = s
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
⊢ Injective ↑C
intro r s rs
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : ∀ (a : Γ), coeff (↑C r) a = coeff (↑C s) a
⊢ r = s
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : ↑C r = ↑C s
⊢ r = s
rw [HahnSeries.ext_iff, Function.funext_iff] at rs
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : ∀ (a : Γ), coeff (↑C r) a = coeff (↑C s) a
h : coeff (↑C r) 0 = coeff (↑C s) 0
⊢ r = s
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : ∀ (a : Γ), coeff (↑C r) a = coeff (↑C s) a
⊢ r = s
have h := rs 0
no goals
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonAssocSemiring R
r s : R
rs : ∀ (a : Γ), coeff (↑C r) a = coeff (↑C s) a
h : coeff (↑C r) 0 = coeff (↑C s) 0
⊢ r = s
rwa [C_apply, single_coeff_same, C_apply, single_coeff_same] at h