simpa only [AlgEquiv.toRingEquiv_eq_coe, RingHom.coe_coe, AlgEquiv.coe_ringEquiv,
  taylorAlgEquiv_symm_apply, taylor_taylor, add_left_neg, taylor_zero', LinearMap.id_coe, id_eq]
R : Type u_1
inst✝ : CommRing R
r : R
p : R[X]
H : Irreducible p
⊢ Irreducible (↑(taylorAlgEquiv r).symm.toRingEquiv ((taylor r) p))
no goals