Theorem: Polynomial.separable_map' (FltRegular/NumberTheory/AuxLemmas.lean)

State before:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
⊢ (map f p).Separable ↔ p.Separable
Tactic:
refine ⟨fun H ↦ ?_, fun H ↦ H.map⟩
State after:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
H : (map f p).Separable
⊢ p.Separable

State before:
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
H : (map f p).Separable
⊢ p.Separable
Tactic:
obtain ⟨m, hm⟩ := Ideal.exists_maximal S
State after:
case intro
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
⊢ p.Separable

State before:
case intro
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
⊢ p.Separable
Tactic:
have := Separable.map H (f := Ideal.Quotient.mk m)
State after:
case intro
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : (map (Ideal.Quotient.mk m) (map f p)).Separable
⊢ p.Separable

State before:
case intro
R : Type u_1
S : Type u_2
inst✝² : Field R
inst✝¹ : CommRing S
inst✝ : Nontrivial S
f : R →+* S
p : R[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : (map (Ideal.Quotient.mk m) (map f p)).Separable
⊢ p.Separable
Tactic:
rwa [map_map, separable_map] at this
State after:
no goals