Theorem: Polynomial.irreducible_taylor_iff (FltRegular/NumberTheory/AuxLemmas.lean)

State before:
R : Type u_1
inst✝ : CommRing R
r : R
p : R[X]
⊢ Irreducible ((taylor r) p) ↔ Irreducible p
Tactic:
refine ⟨fun H ↦ of_irreducible_map (taylorAlgEquiv r).toRingEquiv H, fun H ↦ ?_⟩
State after:
R : Type u_1
inst✝ : CommRing R
r : R
p : R[X]
H : Irreducible p
⊢ Irreducible ((taylor r) p)

State before:
R : Type u_1
inst✝ : CommRing R
r : R
p : R[X]
H : Irreducible p
⊢ Irreducible ((taylor r) p)
Tactic:
apply of_irreducible_map ((taylorAlgEquiv r).symm.toRingEquiv : R[X] →+* R[X])
State after:
R : Type u_1
inst✝ : CommRing R
r : R
p : R[X]
H : Irreducible p
⊢ Irreducible (↑(taylorAlgEquiv r).symm.toRingEquiv ((taylor r) p))

State before:
R : Type u_1
inst✝ : CommRing R
r : R
p : R[X]
H : Irreducible p
⊢ Irreducible (↑(taylorAlgEquiv r).symm.toRingEquiv ((taylor r) p))
Tactic:
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]
State after:
no goals