R✝ : Type ?u.225297
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
r : R
f g : R[X]
h : ↑(taylor r) f = ↑(taylor r) g
⊢ f = g
R✝ : Type ?u.225297
inst✝¹ : Semiring R✝
r✝ : R✝
f : R✝[X]
R : Type u_1
inst✝ : CommRing R
r : R
⊢ Function.Injective ↑(taylor r)
intro f g h
R✝ : Type ?u.225297
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
r : R
f g : R[X]
h : ↑(taylor (-r)) (↑(taylor r) f) = ↑(taylor (-r)) (↑(taylor r) g)
⊢ f = g
R✝ : Type ?u.225297
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
r : R
f g : R[X]
h : ↑(taylor r) f = ↑(taylor r) g
⊢ f = g
apply_fun taylor (-r) at h
no goals
R✝ : Type ?u.225297
inst✝¹ : Semiring R✝
r✝ : R✝
f✝ : R✝[X]
R : Type u_1
inst✝ : CommRing R
r : R
f g : R[X]
h : ↑(taylor (-r)) (↑(taylor r) f) = ↑(taylor (-r)) (↑(taylor r) g)
⊢ f = g
simpa only [taylor_apply, comp_assoc, add_comp, X_comp, C_comp, C_neg, neg_add_cancel_right,
  comp_X] using h