From 756c4dbee24fd005fb4920970d06d43751c65065 Mon Sep 17 00:00:00 2001
From: Eric <ericrboidi@gmail.com>
Date: Mon, 15 Nov 2021 14:45:38 +0000
Subject: [PATCH 01/12] chore(field_theory/separable): generalize theorems

---
 src/field_theory/finite/basic.lean     |  11 +-
 src/field_theory/separable.lean        | 227 ++++++++++++++-----------
 src/field_theory/separable_degree.lean |  12 +-
 3 files changed, 137 insertions(+), 113 deletions(-)

diff --git a/src/field_theory/finite/basic.lean b/src/field_theory/finite/basic.lean
index 023113b782a9a..5cf1f66506e0a 100644
--- a/src/field_theory/finite/basic.lean
+++ b/src/field_theory/finite/basic.lean
@@ -304,11 +304,12 @@ open polynomial
 lemma expand_card (f : polynomial K) :
   expand K q f = f ^ q :=
 begin
-  cases char_p.exists K with p hp, letI := hp,
-  rcases finite_field.card K p with ⟨⟨n, npos⟩, ⟨hp, hn⟩⟩, haveI : fact p.prime := ⟨hp⟩,
-  dsimp at hn, rw hn at *,
-  rw ← map_expand_pow_char,
-  rw [frobenius_pow hn, ring_hom.one_def, map_id],
+  cases char_p.exists K with p hp,
+  letI := hp,
+  rcases finite_field.card K p with ⟨⟨n, npos⟩, ⟨hp, hn⟩⟩,
+  haveI : fact p.prime := ⟨hp⟩,
+  dsimp at hn,
+  rw [hn, ← map_expand_pow_char, frobenius_pow hn, ring_hom.one_def, map_id]
 end
 
 end finite_field
diff --git a/src/field_theory/separable.lean b/src/field_theory/separable.lean
index 106c98bc912cc..8dd974e746c36 100644
--- a/src/field_theory/separable.lean
+++ b/src/field_theory/separable.lean
@@ -137,6 +137,9 @@ polynomial.induction_on f (λ r, by simp_rw expand_C)
 theorem expand_mul (f : polynomial R) : expand R (p * q) f = expand R p (expand R q f) :=
 (expand_expand p q f).symm
 
+@[simp] theorem expand_zero (f : polynomial R) : expand R 0 f = C (eval 1 f) :=
+by simp [expand]
+
 @[simp] theorem expand_one (f : polynomial R) : expand R 1 f = f :=
 polynomial.induction_on f
   (λ r, by rw expand_C)
@@ -221,6 +224,34 @@ lemma expand_injective {n : ℕ} (hn : 0 < n) :
   exact h',
 end
 
+lemma is_unit_of_self_mul_dvd_separable {p q : polynomial R}
+  (hp : p.separable) (hq : q * q ∣ p) : is_unit q :=
+begin
+  obtain ⟨p, rfl⟩ := hq,
+  apply is_coprime_self.mp,
+  have : is_coprime (q * (q * p)) (q * (q.derivative * p + q.derivative * p + q * p.derivative)),
+  { simp only [← mul_assoc, mul_add],
+    convert hp,
+    rw [derivative_mul, derivative_mul],
+    ring },
+  exact is_coprime.of_mul_right_left (is_coprime.of_mul_left_left this)
+end
+/-- The opposite of `expand`: sends `∑ aₙ xⁿᵖ` to `∑ aₙ xⁿ`. -/
+noncomputable def contract (p : ℕ) (f : polynomial R) : polynomial R :=
+∑ n in range (f.nat_degree + 1), monomial n (f.coeff (n * p))
+
+theorem coeff_contract {p : ℕ} (hp : p ≠ 0) (f : polynomial R) (n : ℕ) :
+  (contract p f).coeff n = f.coeff (n * p) :=
+begin
+  simp only [contract, coeff_monomial, sum_ite_eq', finset_sum_coeff, mem_range, not_lt,
+    ite_eq_left_iff],
+  assume hn,
+  apply (coeff_eq_zero_of_nat_degree_lt _).symm,
+  calc f.nat_degree < f.nat_degree + 1 : nat.lt_succ_self _
+    ... ≤ n * 1 : by simpa only [mul_one] using hn
+    ... ≤ n * p : mul_le_mul_of_nonneg_left (show 1 ≤ p, from hp.bot_lt) (zero_le n)
+end
+
 end comm_semiring
 
 section comm_ring
@@ -263,19 +294,32 @@ lemma separable.injective_of_prod_X_sub_C [nontrivial R] {ι : Sort*} [fintype 
   (hfs : (∏ i, (X - C (f i))).separable) : function.injective f :=
 λ x y hfxy, hfs.inj_of_prod_X_sub_C (mem_univ _) (mem_univ _) hfxy
 
-lemma is_unit_of_self_mul_dvd_separable {p q : polynomial R}
-  (hp : p.separable) (hq : q * q ∣ p) : is_unit q :=
+section char_p
+
+variables (p : ℕ) [hp : fact p.prime] [HF : char_p R p]
+include hp HF
+
+theorem expand_char (f : polynomial R) : map (frobenius R p) (expand R p f) = f ^ p :=
 begin
-  obtain ⟨p, rfl⟩ := hq,
-  apply is_coprime_self.mp,
-  have : is_coprime (q * (q * p)) (q * (q.derivative * p + q.derivative * p + q * p.derivative)),
-  { simp only [← mul_assoc, mul_add],
-    convert hp,
-    rw [derivative_mul, derivative_mul],
-    ring },
-  exact is_coprime.of_mul_right_left (is_coprime.of_mul_left_left this)
+  refine f.induction_on' (λ a b ha hb, _) (λ n a, _),
+  { rw [alg_hom.map_add, map_add, ha, hb, add_pow_char], },
+  { rw [expand_monomial, map_monomial, monomial_eq_C_mul_X, monomial_eq_C_mul_X,
+        mul_pow, ← C.map_pow, frobenius_def],
+    ring_exp }
 end
 
+theorem map_expand_pow_char (f : polynomial R) (n : ℕ) :
+   map ((frobenius R p) ^ n) (expand R (p ^ n) f) = f ^ (p ^ n) :=
+begin
+  induction n,
+  { simp [ring_hom.one_def] },
+  symmetry,
+  rw [pow_succ', pow_mul, ← n_ih, ← expand_char, pow_succ, ring_hom.mul_def,
+      ← map_map, mul_comm, expand_mul, ← map_expand (nat.prime.pos hp.1)]
+end
+
+end char_p
+
 end comm_ring
 
 section is_domain
@@ -291,6 +335,32 @@ begin
   rw [hf2, is_unit_C] at hf1, rw expand_eq_C hp at hf2, rwa [hf2, is_unit_C]
 end
 
+theorem of_irreducible_expand {p : ℕ} (hp : p ≠ 0) {f : polynomial R}
+  (hf : irreducible (expand R p f)) : irreducible f :=
+@@of_irreducible_map _ _ _ (is_local_ring_hom_expand R hp.bot_lt) hf
+
+theorem of_irreducible_expand_pow {p : ℕ} (hp : p ≠ 0) {f : polynomial R} {n : ℕ} :
+  irreducible (expand R (p ^ n) f) → irreducible f :=
+nat.rec_on n (λ hf, by rwa [pow_zero, expand_one] at hf) $ λ n ih hf,
+ih $ of_irreducible_expand R hp $ by { rw pow_succ at hf, rwa [expand_expand] }
+
+theorem expand_contract (p : ℕ) [char_p R p] {f : polynomial R} (hf : f.derivative = 0)
+  (hp : p ≠ 0) : expand R p (contract p f) = f :=
+begin
+  ext n,
+  rw [coeff_expand hp.bot_lt, coeff_contract hp],
+  split_ifs with h,
+  { rw nat.div_mul_cancel h },
+  { cases n,
+    { exact absurd (dvd_zero p) h },
+    have := coeff_derivative f n,
+    rw [hf, coeff_zero, zero_eq_mul] at this,
+    cases this,
+    { rw this },
+    rw [← nat.cast_succ, char_p.cast_eq_zero_iff R p] at this,
+    exact absurd this h }
+end
+
 end is_domain
 
 section field
@@ -308,81 +378,45 @@ not_lt_of_le (nat_degree_le_of_dvd this h) $ nat_degree_derivative_lt h⟩
 theorem separable_map (f : F →+* K) {p : polynomial F} : (p.map f).separable ↔ p.separable :=
 by simp_rw [separable_def, derivative_map, is_coprime_map]
 
-section char_p
-
-/-- The opposite of `expand`: sends `∑ aₙ xⁿᵖ` to `∑ aₙ xⁿ`. -/
-noncomputable def contract (p : ℕ) (f : polynomial F) : polynomial F :=
-∑ n in range (f.nat_degree + 1), monomial n (f.coeff (n * p))
-
-variables (p : ℕ) [hp : fact p.prime]
-include hp
-
-theorem coeff_contract (f : polynomial F) (n : ℕ) : (contract p f).coeff n = f.coeff (n * p) :=
-begin
-  simp only [contract, coeff_monomial, sum_ite_eq', finset_sum_coeff, mem_range, not_lt,
-    ite_eq_left_iff],
-  assume hn,
-  apply (coeff_eq_zero_of_nat_degree_lt _).symm,
-  calc f.nat_degree < f.nat_degree + 1 : nat.lt_succ_self _
-    ... ≤ n * 1 : by simpa only [mul_one] using hn
-    ... ≤ n * p : mul_le_mul_of_nonneg_left (@nat.prime.one_lt p (fact.out _)).le (zero_le n)
-end
+lemma separable_prod_X_sub_C_iff' {ι : Sort*} {f : ι → F} {s : finset ι} :
+  (∏ i in s, (X - C (f i))).separable ↔ (∀ (x ∈ s) (y ∈ s), f x = f y → x = y) :=
+⟨λ hfs x hx y hy hfxy, hfs.inj_of_prod_X_sub_C hx hy hfxy,
+λ H, by { rw ← prod_attach, exact separable_prod' (λ x hx y hy hxy,
+    @pairwise_coprime_X_sub _ _ { x // x ∈ s } (λ x, f x)
+      (λ x y hxy, subtype.eq $ H x.1 x.2 y.1 y.2 hxy) _ _ hxy)
+  (λ _ _, separable_X_sub_C) }⟩
 
-theorem of_irreducible_expand {f : polynomial F} (hf : irreducible (expand F p f)) :
-  irreducible f :=
-@@of_irreducible_map _ _ _ (is_local_ring_hom_expand F hp.1.pos) hf
+lemma separable_prod_X_sub_C_iff {ι : Sort*} [fintype ι] {f : ι → F} :
+  (∏ i, (X - C (f i))).separable ↔ function.injective f :=
+separable_prod_X_sub_C_iff'.trans $ by simp_rw [mem_univ, true_implies_iff, function.injective]
 
-theorem of_irreducible_expand_pow {f : polynomial F} {n : ℕ} :
-  irreducible (expand F (p ^ n) f) → irreducible f :=
-nat.rec_on n (λ hf, by rwa [pow_zero, expand_one] at hf) $ λ n ih hf,
-ih $ of_irreducible_expand p $ by { rw pow_succ at hf, rwa [expand_expand] }
+section char_p
 
-variables [HF : char_p F p]
+variables (p : ℕ) [HF : char_p F p]
 include HF
 
-theorem expand_char (f : polynomial F) :
-  map (frobenius F p) (expand F p f) = f ^ p :=
-begin
-  refine f.induction_on' (λ a b ha hb, _) (λ n a, _),
-  { rw [alg_hom.map_add, map_add, ha, hb, add_pow_char], },
-  { rw [expand_monomial, map_monomial, monomial_eq_C_mul_X, monomial_eq_C_mul_X,
-        mul_pow, ← C.map_pow, frobenius_def],
-    ring_exp }
-end
-
-theorem map_expand_pow_char (f : polynomial F) (n : ℕ) :
-   map ((frobenius F p) ^ n) (expand F (p ^ n) f) = f ^ (p ^ n) :=
-begin
-  induction n, { simp [ring_hom.one_def] },
-  symmetry,
-  rw [pow_succ', pow_mul, ← n_ih, ← expand_char, pow_succ, ring_hom.mul_def, ← map_map, mul_comm,
-      expand_mul, ← map_expand (nat.prime.pos hp.1)],
-end
-
-theorem expand_contract {f : polynomial F} (hf : f.derivative = 0) :
-  expand F p (contract p f) = f :=
-begin
-  ext n, rw [coeff_expand hp.1.pos, coeff_contract], split_ifs with h,
-  { rw nat.div_mul_cancel h },
-  { cases n, { exact absurd (dvd_zero p) h },
-    have := coeff_derivative f n, rw [hf, coeff_zero, zero_eq_mul] at this, cases this, { rw this },
-    rw [← nat.cast_succ, char_p.cast_eq_zero_iff F p] at this,
-    exact absurd this h }
-end
-
 theorem separable_or {f : polynomial F} (hf : irreducible f) : f.separable ∨
   ¬f.separable ∧ ∃ g : polynomial F, irreducible g ∧ expand F p g = f :=
-if H : f.derivative = 0 then or.inr
-  ⟨by rw [separable_iff_derivative_ne_zero hf, not_not, H],
-  contract p f,
-  by haveI := is_local_ring_hom_expand F hp.1.pos; exact
-    of_irreducible_map ↑(expand F p) (by rwa ← expand_contract p H at hf),
-  expand_contract p H⟩
+if H : f.derivative = 0 then
+begin
+  unfreezingI { rcases p.eq_zero_or_pos with rfl | hp },
+  { haveI := char_p.char_p_to_char_zero F,
+    have := nat_degree_eq_zero_of_derivative_eq_zero H,
+    have := (nat_degree_pos_iff_degree_pos.mpr $ degree_pos_of_irreducible hf).ne',
+    contradiction },
+  haveI := is_local_ring_hom_expand F hp,
+  exact or.inr
+        ⟨by rw [separable_iff_derivative_ne_zero hf, not_not, H],
+        contract p f,
+        of_irreducible_map ↑(expand F p) (by rwa ← expand_contract F p H hp.ne' at hf),
+        expand_contract F p H hp.ne'⟩
+end
 else or.inl $ (separable_iff_derivative_ne_zero hf).2 H
 
-theorem exists_separable_of_irreducible {f : polynomial F} (hf : irreducible f) (hf0 : f ≠ 0) :
+theorem exists_separable_of_irreducible {f : polynomial F} (hf : irreducible f) (hp : p ≠ 0) :
   ∃ (n : ℕ) (g : polynomial F), g.separable ∧ expand F (p ^ n) g = f :=
 begin
+  replace hp : p.prime := (char_p.char_is_prime_or_zero F p).resolve_right hp,
   unfreezingI {
     induction hn : f.nat_degree using nat.strong_induction_on with N ih generalizing f },
   rcases separable_or p hf with h | ⟨h1, g, hg, hgf⟩,
@@ -390,6 +424,7 @@ begin
   { cases N with N,
     { rw [nat_degree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hn,
       rw [hn, separable_C, is_unit_iff_ne_zero, not_not] at h1,
+      have hf0 : f ≠ 0 := by unfreezingI { rintro rfl, exact not_irreducible_zero hf },
       rw [h1, C_0] at hn, exact absurd hn hf0 },
     have hg1 : g.nat_degree * p = N.succ,
     { rwa [← nat_degree_expand, hgf] },
@@ -397,56 +432,46 @@ begin
     { intro this, rw [this, zero_mul] at hg1, cases hg1 },
     have hg3 : g.nat_degree < N.succ,
     { rw [← mul_one g.nat_degree, ← hg1],
-      exact nat.mul_lt_mul_of_pos_left hp.1.one_lt (nat.pos_of_ne_zero hg2) },
-    have hg4 : g ≠ 0,
-    { rintro rfl, exact hg2 nat_degree_zero },
-    rcases ih _ hg3 hg hg4 rfl with ⟨n, g, hg5, rfl⟩, refine ⟨n+1, g, hg5, _⟩,
+      exact nat.mul_lt_mul_of_pos_left hp.one_lt hg2.bot_lt },
+    rcases ih _ hg3 hg rfl with ⟨n, g, hg4, rfl⟩, refine ⟨n+1, g, hg4, _⟩,
     rw [← hgf, expand_expand, pow_succ] }
 end
 
-theorem is_unit_or_eq_zero_of_separable_expand {f : polynomial F} (n : ℕ)
+theorem is_unit_or_eq_zero_of_separable_expand {f : polynomial F} (n : ℕ) (hp : 0 < p)
   (hf : (expand F (p ^ n) f).separable) : is_unit f ∨ n = 0 :=
 begin
-  rw or_iff_not_imp_right, intro hn,
+  rw or_iff_not_imp_right,
+  rintro hn : n ≠ 0,
   have hf2 : (expand F (p ^ n) f).derivative = 0,
   { by rw [derivative_expand, nat.cast_pow, char_p.cast_eq_zero,
-      zero_pow (nat.pos_of_ne_zero hn), zero_mul, mul_zero] },
-  rw [separable_def, hf2, is_coprime_zero_right, is_unit_iff] at hf, rcases hf with ⟨r, hr, hrf⟩,
-  rw [eq_comm, expand_eq_C (pow_pos hp.1.pos _)] at hrf,
+      zero_pow hn.bot_lt, zero_mul, mul_zero] },
+  rw [separable_def, hf2, is_coprime_zero_right, is_unit_iff] at hf,
+  rcases hf with ⟨r, hr, hrf⟩,
+  rw [eq_comm, expand_eq_C (pow_pos hp _)] at hrf,
   rwa [hrf, is_unit_C]
 end
 
-theorem unique_separable_of_irreducible {f : polynomial F} (hf : irreducible f) (hf0 : f ≠ 0)
+theorem unique_separable_of_irreducible {f : polynomial F} (hf : irreducible f) (hp : 0 < p)
   (n₁ : ℕ) (g₁ : polynomial F) (hg₁ : g₁.separable) (hgf₁ : expand F (p ^ n₁) g₁ = f)
   (n₂ : ℕ) (g₂ : polynomial F) (hg₂ : g₂.separable) (hgf₂ : expand F (p ^ n₂) g₂ = f) :
   n₁ = n₂ ∧ g₁ = g₂ :=
 begin
-  revert g₁ g₂, wlog hn : n₁ ≤ n₂ := le_total n₁ n₂ using [n₁ n₂, n₂ n₁] tactic.skip,
+  revert g₁ g₂,
+  wlog hn : n₁ ≤ n₂ := le_total n₁ n₂ using [n₁ n₂, n₂ n₁],
+  have hf0 : f ≠ 0 := by unfreezingI { rintro rfl, exact not_irreducible_zero hf },
   unfreezingI { intros, rw le_iff_exists_add at hn, rcases hn with ⟨k, rfl⟩,
-    rw [← hgf₁, pow_add, expand_mul, expand_inj (pow_pos hp.1.pos n₁)] at hgf₂, subst hgf₂,
+    rw [← hgf₁, pow_add, expand_mul, expand_inj (pow_pos hp n₁)] at hgf₂, subst hgf₂,
     subst hgf₁,
-    rcases is_unit_or_eq_zero_of_separable_expand p k hg₁ with h | rfl,
+    rcases is_unit_or_eq_zero_of_separable_expand p k hp hg₁ with h | rfl,
     { rw is_unit_iff at h, rcases h with ⟨r, hr, rfl⟩,
       simp_rw expand_C at hf, exact absurd (is_unit_C.2 hr) hf.1 },
     { rw [add_zero, pow_zero, expand_one], split; refl } },
-  exact λ g₁ g₂ hg₁ hgf₁ hg₂ hgf₂, let ⟨hn, hg⟩ :=
-    this g₂ g₁ hg₂ hgf₂ hg₁ hgf₁ in ⟨hn.symm, hg.symm⟩
+  obtain ⟨hn, hg⟩ := this g₂ g₁ hg₂ hgf₂ hg₁ hgf₁,
+  exact ⟨hn.symm, hg.symm⟩
 end
 
 end char_p
 
-lemma separable_prod_X_sub_C_iff' {ι : Sort*} {f : ι → F} {s : finset ι} :
-  (∏ i in s, (X - C (f i))).separable ↔ (∀ (x ∈ s) (y ∈ s), f x = f y → x = y) :=
-⟨λ hfs x hx y hy hfxy, hfs.inj_of_prod_X_sub_C hx hy hfxy,
-λ H, by { rw ← prod_attach, exact separable_prod' (λ x hx y hy hxy,
-    @pairwise_coprime_X_sub _ _ { x // x ∈ s } (λ x, f x)
-      (λ x y hxy, subtype.eq $ H x.1 x.2 y.1 y.2 hxy) _ _ hxy)
-  (λ _ _, separable_X_sub_C) }⟩
-
-lemma separable_prod_X_sub_C_iff {ι : Sort*} [fintype ι] {f : ι → F} :
-  (∏ i, (X - C (f i))).separable ↔ function.injective f :=
-separable_prod_X_sub_C_iff'.trans $ by simp_rw [mem_univ, true_implies_iff, function.injective]
-
 section splits
 
 open_locale big_operators
diff --git a/src/field_theory/separable_degree.lean b/src/field_theory/separable_degree.lean
index 62efddcfb5452..051af38e119da 100644
--- a/src/field_theory/separable_degree.lean
+++ b/src/field_theory/separable_degree.lean
@@ -20,7 +20,7 @@ This file contains basics about the separable degree of a polynomial.
 - `has_separable_contraction`: the condition of having a separable contraction
 - `has_separable_contraction.degree`: the separable degree, defined as the degree of some
   separable contraction
-- `irreducible_has_separable_contraction`: any nonzero irreducible polynomial can be contracted
+- `irreducible_has_separable_contraction`: any irreducible polynomial can be contracted
   to a separable polynomial
 - `has_separable_contraction.dvd_degree'`: the degree of a separable contraction divides the degree,
   in function of the exponential characteristic of the field
@@ -92,13 +92,11 @@ variables (q : ℕ) {f : polynomial F} (hf : has_separable_contraction q f)
 /-- Every irreducible polynomial can be contracted to a separable polynomial.
 https://stacks.math.columbia.edu/tag/09H0 -/
 lemma irreducible_has_separable_contraction (q : ℕ) [hF : exp_char F q]
-  (f : polynomial F) [irred : irreducible f] (fn : f ≠ 0) : has_separable_contraction q f :=
+  (f : polynomial F) [irred : irreducible f] : has_separable_contraction q f :=
 begin
   casesI hF,
-  { use f,
-    exact ⟨irreducible.separable irred, ⟨0, by rw [pow_zero, expand_one]⟩⟩ },
-  { haveI qp : fact (nat.prime q) := ⟨hF_hprime⟩,
-    rcases exists_separable_of_irreducible q irred fn with ⟨n, g, hgs, hge⟩,
+  { exact ⟨f, irreducible.separable irred, ⟨0, by rw [pow_zero, expand_one]⟩⟩ },
+  { rcases exists_separable_of_irreducible q irred ‹q.prime›.ne_zero with ⟨n, g, hgs, hge⟩,
     exact ⟨g, hgs, n, hge⟩, }
 end
 
@@ -114,7 +112,7 @@ begin
   rw [add_assoc, pow_add, expand_mul] at h_expand,
   let aux := expand_injective (pow_pos hq.1.pos m) h_expand,
   rw aux at hg,
-  have := (is_unit_or_eq_zero_of_separable_expand q (s + 1) hg).resolve_right
+  have := (is_unit_or_eq_zero_of_separable_expand q (s + 1) hq.out.pos hg).resolve_right
     s.succ_ne_zero,
   rw [aux, nat_degree_expand,
     nat_degree_eq_of_degree_eq_some (degree_eq_zero_of_is_unit this),

From c5afa4634d5a28e79a360ab7b9383c60a81a9e15 Mon Sep 17 00:00:00 2001
From: Eric <ericrboidi@gmail.com>
Date: Mon, 15 Nov 2021 18:52:09 +0000
Subject: [PATCH 02/12] finish

---
 src/data/polynomial/algebra_map.lean       |   2 +-
 src/field_theory/primitive_element.lean    |   2 +-
 src/field_theory/separable.lean            | 258 ++++++++++-----------
 src/ring_theory/polynomial/cyclotomic.lean |   2 +-
 src/ring_theory/roots_of_unity.lean        |   5 +-
 5 files changed, 134 insertions(+), 135 deletions(-)

diff --git a/src/data/polynomial/algebra_map.lean b/src/data/polynomial/algebra_map.lean
index 645d70cf9e050..1a2d3b38d5a3c 100644
--- a/src/data/polynomial/algebra_map.lean
+++ b/src/data/polynomial/algebra_map.lean
@@ -376,7 +376,7 @@ begin
   simp [sum_range_sub', coeff_monomial],
 end
 
-theorem not_is_unit_X_sub_C [nontrivial R] {r : R} : ¬ is_unit (X - C r) :=
+theorem not_is_unit_X_sub_C [nontrivial R] (r : R) : ¬ is_unit (X - C r) :=
 λ ⟨⟨_, g, hfg, hgf⟩, rfl⟩, @zero_ne_one R _ _ $ by erw [← eval_mul_X_sub_C, hgf, eval_one]
 
 end ring
diff --git a/src/field_theory/primitive_element.lean b/src/field_theory/primitive_element.lean
index 243145268a411..e3fa8b23e1e98 100644
--- a/src/field_theory/primitive_element.lean
+++ b/src/field_theory/primitive_element.lean
@@ -154,7 +154,7 @@ begin
     apply (div_eq_iff (sub_ne_zero.mpr a)).mpr,
     simp only [algebra.smul_def, ring_hom.map_add, ring_hom.map_mul, ring_hom.comp_apply],
     ring },
-  rw ← eq_X_sub_C_of_separable_of_root_eq h_ne_zero h_sep h_root h_splits h_roots,
+  rw ← eq_X_sub_C_of_separable_of_root_eq h_sep h_root h_splits h_roots,
   transitivity euclidean_domain.gcd (_ : polynomial E) (_ : polynomial E),
   { dsimp only [p],
     convert (gcd_map (algebra_map F⟮γ⟯ E)).symm },
diff --git a/src/field_theory/separable.lean b/src/field_theory/separable.lean
index 8dd974e746c36..5d26c46210778 100644
--- a/src/field_theory/separable.lean
+++ b/src/field_theory/separable.lean
@@ -57,6 +57,9 @@ end
 lemma separable_one : (1 : polynomial R).separable :=
 is_coprime_one_left
 
+@[nontriviality] lemma separable_subsingleton [subsingleton R] (f : polynomial R) : f.separable :=
+by simp [separable]
+
 lemma separable_X_add_C (a : R) : (X + C a).separable :=
 by { rw [separable_def, derivative_add, derivative_X, derivative_C, add_zero],
   exact is_coprime_one_right }
@@ -252,6 +255,71 @@ begin
     ... ≤ n * p : mul_le_mul_of_nonneg_left (show 1 ≤ p, from hp.bot_lt) (zero_le n)
 end
 
+section char_p
+
+variable [HF : char_p R p]
+include HF
+
+theorem expand_contract [no_zero_divisors R] {f : polynomial R} (hf : f.derivative = 0)
+  (hp : p ≠ 0) : expand R p (contract p f) = f :=
+begin
+  ext n,
+  rw [coeff_expand hp.bot_lt, coeff_contract hp],
+  split_ifs with h,
+  { rw nat.div_mul_cancel h },
+  { cases n,
+    { exact absurd (dvd_zero p) h },
+    have := coeff_derivative f n,
+    rw [hf, coeff_zero, zero_eq_mul] at this,
+    cases this,
+    { rw this },
+    rw [← nat.cast_succ, char_p.cast_eq_zero_iff R p] at this,
+    exact absurd this h }
+end
+
+variable [hp : fact p.prime]
+include hp
+
+theorem expand_char (f : polynomial R) : map (frobenius R p) (expand R p f) = f ^ p :=
+begin
+  refine f.induction_on' (λ a b ha hb, _) (λ n a, _),
+  { rw [alg_hom.map_add, map_add, ha, hb, add_pow_char], },
+  { rw [expand_monomial, map_monomial, monomial_eq_C_mul_X, monomial_eq_C_mul_X,
+        mul_pow, ← C.map_pow, frobenius_def],
+    ring_exp }
+end
+
+theorem map_expand_pow_char (f : polynomial R) (n : ℕ) :
+   map ((frobenius R p) ^ n) (expand R (p ^ n) f) = f ^ (p ^ n) :=
+begin
+  induction n,
+  { simp [ring_hom.one_def] },
+  symmetry,
+  rw [pow_succ', pow_mul, ← n_ih, ← expand_char, pow_succ, ring_hom.mul_def,
+      ← map_map, mul_comm, expand_mul, ← map_expand (nat.prime.pos hp.1)]
+end
+
+end char_p
+
+lemma multiplicity_le_one_of_separable {p q : polynomial R} (hq : ¬ is_unit q)
+  (hsep : separable p) : multiplicity q p ≤ 1 :=
+begin
+  contrapose! hq,
+  apply is_unit_of_self_mul_dvd_separable hsep,
+  rw ← sq,
+  apply multiplicity.pow_dvd_of_le_multiplicity,
+  simpa only [nat.cast_one, nat.cast_bit0] using enat.add_one_le_of_lt hq
+end
+
+lemma separable.squarefree {p : polynomial R} (hsep : separable p) : squarefree p :=
+begin
+  rw multiplicity.squarefree_iff_multiplicity_le_one p,
+  intro f,
+  by_cases hunit : is_unit f,
+  { exact or.inr hunit },
+  exact or.inl (multiplicity_le_one_of_separable hunit hsep)
+end
+
 end comm_semiring
 
 section comm_ring
@@ -287,46 +355,52 @@ begin
   rw [← insert_erase hx, prod_insert (not_mem_erase _ _),
       ← insert_erase (mem_erase_of_ne_of_mem (ne.symm hxy) hy),
       prod_insert (not_mem_erase _ _), ← mul_assoc, hfxy, ← sq] at hfs,
-  cases (hfs.of_mul_left.of_pow (by exact not_is_unit_X_sub_C) two_ne_zero).2
+  cases (hfs.of_mul_left.of_pow (by exact not_is_unit_X_sub_C _) two_ne_zero).2
 end
 
 lemma separable.injective_of_prod_X_sub_C [nontrivial R] {ι : Sort*} [fintype ι] {f : ι → R}
   (hfs : (∏ i, (X - C (f i))).separable) : function.injective f :=
 λ x y hfxy, hfs.inj_of_prod_X_sub_C (mem_univ _) (mem_univ _) hfxy
 
-section char_p
-
-variables (p : ℕ) [hp : fact p.prime] [HF : char_p R p]
-include hp HF
-
-theorem expand_char (f : polynomial R) : map (frobenius R p) (expand R p f) = f ^ p :=
+lemma nodup_of_separable_prod [nontrivial R] {s : multiset R}
+  (hs : separable (multiset.map (λ a, X - C a) s).prod) : s.nodup :=
 begin
-  refine f.induction_on' (λ a b ha hb, _) (λ n a, _),
-  { rw [alg_hom.map_add, map_add, ha, hb, add_pow_char], },
-  { rw [expand_monomial, map_monomial, monomial_eq_C_mul_X, monomial_eq_C_mul_X,
-        mul_pow, ← C.map_pow, frobenius_def],
-    ring_exp }
+  rw multiset.nodup_iff_ne_cons_cons,
+  rintros a t rfl,
+  refine not_is_unit_X_sub_C a (is_unit_of_self_mul_dvd_separable hs _),
+  simpa only [multiset.map_cons, multiset.prod_cons] using mul_dvd_mul_left _ (dvd_mul_right _ _)
 end
 
-theorem map_expand_pow_char (f : polynomial R) (n : ℕ) :
-   map ((frobenius R p) ^ n) (expand R (p ^ n) f) = f ^ (p ^ n) :=
+/--If `is_unit n` in a `comm_ring R`, then `X ^ n - u` is separable for any unit `u`. -/
+lemma separable_X_pow_sub_C_unit {n : ℕ} (u : units R) (hn : is_unit (n : R)) :
+  separable (X ^ n - C (u : R)) :=
 begin
-  induction n,
-  { simp [ring_hom.one_def] },
-  symmetry,
-  rw [pow_succ', pow_mul, ← n_ih, ← expand_char, pow_succ, ring_hom.mul_def,
-      ← map_map, mul_comm, expand_mul, ← map_expand (nat.prime.pos hp.1)]
+  nontriviality R,
+  rcases n.eq_zero_or_pos with rfl | hpos,
+  { simpa using hn },
+  apply (separable_def' (X ^ n - C (u : R))).2,
+  obtain ⟨n', hn'⟩ := hn.exists_left_inv,
+  refine ⟨-C ↑u⁻¹, C ↑u⁻¹ * C n' * X, _⟩,
+  rw [derivative_sub, derivative_C, sub_zero, derivative_pow X n, derivative_X, mul_one],
+  calc  - C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (↑n * X ^ (n - 1))
+      = C (↑u⁻¹ * ↑ u) - C ↑u⁻¹ * X^n + C ↑ u ⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1)) :
+    by { simp only [C.map_mul, C_eq_nat_cast], ring }
+  ... = 1 : by simp only [units.inv_mul, hn', C.map_one, mul_one, ← pow_succ,
+              nat.sub_add_cancel (show 1 ≤ n, from hpos), sub_add_cancel]
 end
 
-end char_p
+lemma root_multiplicity_le_one_of_separable [nontrivial R] {p : polynomial R} (hp : p ≠ 0)
+  (hsep : separable p) (x : R) : root_multiplicity x p ≤ 1 :=
+begin
+  rw [root_multiplicity_eq_multiplicity, dif_neg hp, ← enat.coe_le_coe, enat.coe_get, nat.cast_one],
+  exact multiplicity_le_one_of_separable (not_is_unit_X_sub_C _) hsep
+end
 
 end comm_ring
 
 section is_domain
 
-variables (R : Type u) [comm_ring R] [is_domain R]
-
-theorem is_local_ring_hom_expand {p : ℕ} (hp : 0 < p) :
+theorem is_local_ring_hom_expand (R : Type u) [comm_ring R] [is_domain R] {p : ℕ} (hp : 0 < p) :
   is_local_ring_hom (↑(expand R p) : polynomial R →+* polynomial R) :=
 begin
   refine ⟨λ f hf1, _⟩, rw ← coe_fn_coe_base at hf1,
@@ -335,6 +409,8 @@ begin
   rw [hf2, is_unit_C] at hf1, rw expand_eq_C hp at hf2, rwa [hf2, is_unit_C]
 end
 
+variables {R : Type u} [comm_ring R] [is_domain R]
+
 theorem of_irreducible_expand {p : ℕ} (hp : p ≠ 0) {f : polynomial R}
   (hf : irreducible (expand R p f)) : irreducible f :=
 @@of_irreducible_map _ _ _ (is_local_ring_hom_expand R hp.bot_lt) hf
@@ -342,25 +418,20 @@ theorem of_irreducible_expand {p : ℕ} (hp : p ≠ 0) {f : polynomial R}
 theorem of_irreducible_expand_pow {p : ℕ} (hp : p ≠ 0) {f : polynomial R} {n : ℕ} :
   irreducible (expand R (p ^ n) f) → irreducible f :=
 nat.rec_on n (λ hf, by rwa [pow_zero, expand_one] at hf) $ λ n ih hf,
-ih $ of_irreducible_expand R hp $ by { rw pow_succ at hf, rwa [expand_expand] }
+ih $ of_irreducible_expand hp $ by { rw pow_succ at hf, rwa [expand_expand] }
 
-theorem expand_contract (p : ℕ) [char_p R p] {f : polynomial R} (hf : f.derivative = 0)
-  (hp : p ≠ 0) : expand R p (contract p f) = f :=
+lemma count_roots_le_one {p : polynomial R} (hsep : separable p) (x : R) :
+  p.roots.count x ≤ 1 :=
 begin
-  ext n,
-  rw [coeff_expand hp.bot_lt, coeff_contract hp],
-  split_ifs with h,
-  { rw nat.div_mul_cancel h },
-  { cases n,
-    { exact absurd (dvd_zero p) h },
-    have := coeff_derivative f n,
-    rw [hf, coeff_zero, zero_eq_mul] at this,
-    cases this,
-    { rw this },
-    rw [← nat.cast_succ, char_p.cast_eq_zero_iff R p] at this,
-    exact absurd this h }
+  rcases eq_or_ne p 0 with rfl | hp,
+  { simp },
+  rw count_roots hp,
+  exact root_multiplicity_le_one_of_separable hp hsep x
 end
 
+lemma nodup_roots {p : polynomial R} (hsep : separable p) : p.roots.nodup :=
+multiset.nodup_iff_count_le_one.mpr (count_roots_le_one hsep)
+
 end is_domain
 
 section field
@@ -408,8 +479,8 @@ begin
   exact or.inr
         ⟨by rw [separable_iff_derivative_ne_zero hf, not_not, H],
         contract p f,
-        of_irreducible_map ↑(expand F p) (by rwa ← expand_contract F p H hp.ne' at hf),
-        expand_contract F p H hp.ne'⟩
+        of_irreducible_map ↑(expand F p) (by rwa ← expand_contract p H hp.ne' at hf),
+        expand_contract p H hp.ne'⟩
 end
 else or.inl $ (separable_iff_derivative_ne_zero hf).2 H
 
@@ -472,61 +543,6 @@ end
 
 end char_p
 
-section splits
-
-open_locale big_operators
-
-variables {i : F →+* K}
-
-lemma not_unit_X_sub_C (a : F) : ¬ is_unit (X - C a) :=
-λ h, have one_eq_zero : (1 : with_bot ℕ) = 0, by simpa using degree_eq_zero_of_is_unit h,
-one_ne_zero (option.some_injective _ one_eq_zero)
-
-lemma nodup_of_separable_prod {s : multiset F}
-  (hs : separable (multiset.map (λ a, X - C a) s).prod) : s.nodup :=
-begin
-  rw multiset.nodup_iff_ne_cons_cons,
-  rintros a t rfl,
-  refine not_unit_X_sub_C a (is_unit_of_self_mul_dvd_separable hs _),
-  simpa only [multiset.map_cons, multiset.prod_cons] using mul_dvd_mul_left _ (dvd_mul_right _ _)
-end
-
-lemma multiplicity_le_one_of_separable {p q : polynomial F} (hq : ¬ is_unit q)
-  (hsep : separable p) : multiplicity q p ≤ 1 :=
-begin
-  contrapose! hq,
-  apply is_unit_of_self_mul_dvd_separable hsep,
-  rw ← sq,
-  apply multiplicity.pow_dvd_of_le_multiplicity,
-  simpa only [nat.cast_one, nat.cast_bit0] using enat.add_one_le_of_lt hq
-end
-
-lemma separable.squarefree {p : polynomial F}  (hsep : separable p) : squarefree p :=
-begin
-  rw multiplicity.squarefree_iff_multiplicity_le_one p,
-  intro f,
-  by_cases hunit : is_unit f,
-  { exact or.inr hunit },
-  exact or.inl (multiplicity_le_one_of_separable hunit hsep)
-end
-
-/--If `is_unit n` in a nontrivial `comm_ring R`, then `X ^ n - u` is separable for any unit `u`. -/
-lemma separable_X_pow_sub_C_unit {R : Type*} [comm_ring R] [nontrivial R] {n : ℕ}
-  (u : units R) (hn : is_unit (n : R)) : separable (X ^ n - C (u : R)) :=
-begin
-  rcases n.eq_zero_or_pos with rfl | hpos,
-  { simpa using hn },
-  apply (separable_def' (X ^ n - C (u : R))).2,
-  obtain ⟨n', hn'⟩ := hn.exists_left_inv,
-  refine ⟨-C ↑u⁻¹, C ↑u⁻¹ * C n' * X, _⟩,
-  rw [derivative_sub, derivative_C, sub_zero, derivative_pow X n, derivative_X, mul_one],
-  calc  - C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (↑n * X ^ (n - 1))
-      = C (↑u⁻¹ * ↑ u) - C ↑u⁻¹ * X^n + C ↑ u ⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1)) :
-    by { simp only [C.map_mul, C_eq_nat_cast], ring }
-  ... = 1 : by simp only [units.inv_mul, hn', C.map_one, mul_one, ← pow_succ,
-              nat.sub_add_cancel (show 1 ≤ n, from hpos), sub_add_cancel]
-end
-
 /--If `n ≠ 0` in `F`, then ` X ^ n - a` is separable for any `a ≠ 0`. -/
 lemma separable_X_pow_sub_C {n : ℕ} (a : F) (hn : (n : F) ≠ 0) (ha : a ≠ 0) :
   separable (X ^ n - C a) :=
@@ -547,30 +563,7 @@ begin
   contradiction
 end
 
-/--If `n ≠ 0` in `F`, then ` X ^ n - a` is squarefree for any `a ≠ 0`. -/
-lemma squarefree_X_pow_sub_C {n : ℕ} (a : F) (hn : (n : F) ≠ 0) (ha : a ≠ 0) :
-  squarefree (X ^ n - C a) :=
-(separable_X_pow_sub_C a hn ha).squarefree
-
-lemma root_multiplicity_le_one_of_separable {p : polynomial F} (hp : p ≠ 0)
-  (hsep : separable p) (x : F) : root_multiplicity x p ≤ 1 :=
-begin
-  rw [root_multiplicity_eq_multiplicity, dif_neg hp, ← enat.coe_le_coe, enat.coe_get, nat.cast_one],
-  exact multiplicity_le_one_of_separable (not_unit_X_sub_C _) hsep
-end
-
-lemma count_roots_le_one {p : polynomial F} (hsep : separable p) (x : F) :
-  p.roots.count x ≤ 1 :=
-begin
-  by_cases hp : p = 0,
-  { simp [hp] },
-  rw count_roots hp,
-  exact root_multiplicity_le_one_of_separable hp hsep x
-end
-
-lemma nodup_roots {p : polynomial F} (hsep : separable p) :
-  p.roots.nodup :=
-multiset.nodup_iff_count_le_one.mpr (count_roots_le_one hsep)
+section splits
 
 lemma card_root_set_eq_nat_degree [algebra F K] {p : polynomial F} (hsep : p.separable)
   (hsplit : splits (algebra_map F K) p) : fintype.card (p.root_set K) = p.nat_degree :=
@@ -580,10 +573,13 @@ begin
   exact nodup_roots hsep.map,
 end
 
-lemma eq_X_sub_C_of_separable_of_root_eq {x : F} {h : polynomial F} (h_ne_zero : h ≠ 0)
+variable {i : F →+* K}
+
+lemma eq_X_sub_C_of_separable_of_root_eq {x : F} {h : polynomial F}
   (h_sep : h.separable) (h_root : h.eval x = 0) (h_splits : splits i h)
   (h_roots : ∀ y ∈ (h.map i).roots, y = i x) : h = (C (leading_coeff h)) * (X - C x) :=
 begin
+  have h_ne_zero : h ≠ 0 := by { rintro rfl, exact not_separable_zero h_sep },
   apply polynomial.eq_X_sub_C_of_splits_of_single_root i h_splits,
   apply finset.mk.inj,
   { change _ = {i x},
@@ -614,21 +610,25 @@ end
 
 end splits
 
+theorem _root_.irreducible.separable [char_zero F] {f : polynomial F}
+  (hf : irreducible f) : f.separable :=
+begin
+  rw [separable_iff_derivative_ne_zero hf, ne, ← degree_eq_bot, degree_derivative_eq],
+  { rintro ⟨⟩ },
+  rw [pos_iff_ne_zero, ne, nat_degree_eq_zero_iff_degree_le_zero, degree_le_zero_iff],
+  refine λ hf1, hf.not_unit _,
+  rw [hf1, is_unit_C, is_unit_iff_ne_zero],
+  intro hf2,
+  rw [hf2, C_0] at hf1,
+  exact absurd hf1 hf.ne_zero
+end
+
 end field
 
 end polynomial
 
 open polynomial
 
-theorem irreducible.separable {F : Type u} [field F] [char_zero F] {f : polynomial F}
-  (hf : irreducible f) : f.separable :=
-begin
-  rw [separable_iff_derivative_ne_zero hf, ne, ← degree_eq_bot, degree_derivative_eq], rintro ⟨⟩,
-  rw [pos_iff_ne_zero, ne, nat_degree_eq_zero_iff_degree_le_zero, degree_le_zero_iff],
-  refine λ hf1, hf.not_unit _, rw [hf1, is_unit_C, is_unit_iff_ne_zero],
-  intro hf2, rw [hf2, C_0] at hf1, exact absurd hf1 hf.ne_zero
-end
-
 section comm_ring
 
 variables (F K : Type*) [comm_ring F] [ring K] [algebra F K]
diff --git a/src/ring_theory/polynomial/cyclotomic.lean b/src/ring_theory/polynomial/cyclotomic.lean
index 6d9216a4ed37b..2a7eb6e542885 100644
--- a/src/ring_theory/polynomial/cyclotomic.lean
+++ b/src/ring_theory/polynomial/cyclotomic.lean
@@ -650,7 +650,7 @@ begin
   { intro ha,
     exact hn (int.coe_nat_dvd.1 ((zmod.int_coe_zmod_eq_zero_iff_dvd n p).1 ha)) },
   rw [sq] at habs,
-  replace habs := squarefree_X_pow_sub_C (1 : (zmod p)) hnzero one_ne_zero
+  replace habs := (separable_X_pow_sub_C (1 : (zmod p)) hnzero one_ne_zero).squarefree
     (map (int.cast_ring_hom (zmod p)) (X - a)) habs,
   simp only [map_nat_cast, map_X, map_sub] at habs,
   replace habs := degree_eq_zero_of_is_unit habs,
diff --git a/src/ring_theory/roots_of_unity.lean b/src/ring_theory/roots_of_unity.lean
index 9837b26626875..072ebda8c8f8d 100644
--- a/src/ring_theory/roots_of_unity.lean
+++ b/src/ring_theory/roots_of_unity.lean
@@ -907,9 +907,8 @@ begin
   replace habs := lt_of_lt_of_le (enat.coe_lt_coe.2 one_lt_two)
     (multiplicity.le_multiplicity_of_pow_dvd (dvd_trans habs prod)),
   have hfree : squarefree (X ^ n - 1 : polynomial (zmod p)),
-  { refine squarefree_X_pow_sub_C 1 _ one_ne_zero,
-    by_contra hzero,
-    exact hdiv ((zmod.nat_coe_zmod_eq_zero_iff_dvd n p).1 hzero) },
+  { exact (separable_X_pow_sub_C 1
+          (λ h, hdiv $ (zmod.nat_coe_zmod_eq_zero_iff_dvd n p).1 h) one_ne_zero).squarefree },
   cases (multiplicity.squarefree_iff_multiplicity_le_one (X ^ n - 1)).1 hfree
     (map (int.cast_ring_hom (zmod p)) P) with hle hunit,
   { rw nat.cast_one at habs, exact hle.not_lt habs },

From 43e78051d5dc104a4263ac78e890507599c68ff7 Mon Sep 17 00:00:00 2001
From: Eric <ericrboidi@gmail.com>
Date: Mon, 15 Nov 2021 19:23:26 +0000
Subject: [PATCH 03/12] fix

---
 src/data/polynomial/ring_division.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean
index dd5b4ea9c1ac2..015b90d3380e6 100644
--- a/src/data/polynomial/ring_division.lean
+++ b/src/data/polynomial/ring_division.lean
@@ -171,7 +171,7 @@ by rw [nat_degree_one, nat_degree_mul hp0 hq0, eq_comm,
 degree_eq_zero_of_is_unit ⟨u, rfl⟩
 
 theorem prime_X_sub_C (r : R) : prime (X - C r) :=
-⟨X_sub_C_ne_zero r, not_is_unit_X_sub_C,
+⟨X_sub_C_ne_zero r, not_is_unit_X_sub_C r,
  λ _ _, by { simp_rw [dvd_iff_is_root, is_root.def, eval_mul, mul_eq_zero], exact id }⟩
 
 theorem prime_X : prime (X : polynomial R) :=

From b909013a8759ccadf4a80dca8979984cc7a81608 Mon Sep 17 00:00:00 2001
From: Eric <ericrboidi@gmail.com>
Date: Mon, 15 Nov 2021 20:34:25 +0000
Subject: [PATCH 04/12] fix

---
 src/ring_theory/norm.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/ring_theory/norm.lean b/src/ring_theory/norm.lean
index 1ca1325c694ea..a64491644c1cf 100644
--- a/src/ring_theory/norm.lean
+++ b/src/ring_theory/norm.lean
@@ -195,7 +195,8 @@ begin
   letI := classical.dec_eq E,
   rw [norm_gen_eq_prod_roots pb hE, fintype.prod_equiv pb.lift_equiv', finset.prod_mem_multiset,
     finset.prod_eq_multiset_prod, multiset.to_finset_val,
-    multiset.erase_dup_eq_self.mpr (nodup_roots ((separable_map _).mpr hfx)), multiset.map_id],
+    multiset.erase_dup_eq_self.mpr, multiset.map_id],
+  { exact nodup_roots ((separable_map _).mpr hfx) },
   { intro x, refl },
   { intro σ, rw [power_basis.lift_equiv'_apply_coe, id.def] }
 end

From d81c6f10b7472ae83834bc5c8d2aa7303b8010c0 Mon Sep 17 00:00:00 2001
From: Eric <ericrboidi@gmail.com>
Date: Mon, 15 Nov 2021 21:05:55 +0000
Subject: [PATCH 05/12] not sure why this breaks nodup roots...

---
 src/ring_theory/trace.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/ring_theory/trace.lean b/src/ring_theory/trace.lean
index d7f15da50986e..490292ac0a5c3 100644
--- a/src/ring_theory/trace.lean
+++ b/src/ring_theory/trace.lean
@@ -295,7 +295,8 @@ begin
   letI := classical.dec_eq E,
   rw [pb.trace_gen_eq_sum_roots hE, fintype.sum_equiv pb.lift_equiv', finset.sum_mem_multiset,
       finset.sum_eq_multiset_sum, multiset.to_finset_val,
-      multiset.erase_dup_eq_self.mpr (nodup_roots ((separable_map _).mpr hfx)), multiset.map_id],
+      multiset.erase_dup_eq_self.mpr _, multiset.map_id],
+  { exact nodup_roots ((separable_map _).mpr hfx) },
   { intro x, refl },
   { intro σ, rw [power_basis.lift_equiv'_apply_coe, id.def] }
 end

From 67a108f9f3fb6df8eb739dee6bdbe035851739c3 Mon Sep 17 00:00:00 2001
From: Eric <ericrboidi@gmail.com>
Date: Tue, 16 Nov 2021 00:14:55 +0000
Subject: [PATCH 06/12] turns out magical lemma I wanted exists

---
 src/field_theory/separable.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/field_theory/separable.lean b/src/field_theory/separable.lean
index 5d26c46210778..6408d988c73d2 100644
--- a/src/field_theory/separable.lean
+++ b/src/field_theory/separable.lean
@@ -495,7 +495,7 @@ begin
   { cases N with N,
     { rw [nat_degree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hn,
       rw [hn, separable_C, is_unit_iff_ne_zero, not_not] at h1,
-      have hf0 : f ≠ 0 := by unfreezingI { rintro rfl, exact not_irreducible_zero hf },
+      have hf0 : f ≠ 0 := hf.ne_zero,
       rw [h1, C_0] at hn, exact absurd hn hf0 },
     have hg1 : g.nat_degree * p = N.succ,
     { rwa [← nat_degree_expand, hgf] },
@@ -529,7 +529,7 @@ theorem unique_separable_of_irreducible {f : polynomial F} (hf : irreducible f)
 begin
   revert g₁ g₂,
   wlog hn : n₁ ≤ n₂ := le_total n₁ n₂ using [n₁ n₂, n₂ n₁],
-  have hf0 : f ≠ 0 := by unfreezingI { rintro rfl, exact not_irreducible_zero hf },
+  have hf0 : f ≠ 0 := hf.ne_zero,
   unfreezingI { intros, rw le_iff_exists_add at hn, rcases hn with ⟨k, rfl⟩,
     rw [← hgf₁, pow_add, expand_mul, expand_inj (pow_pos hp n₁)] at hgf₂, subst hgf₂,
     subst hgf₁,

From 59a07b02497829d34e0534c5d66993eb04b92c0c Mon Sep 17 00:00:00 2001
From: Eric <ericrboidi@gmail.com>
Date: Tue, 16 Nov 2021 09:29:14 +0000
Subject: [PATCH 07/12] contract_expand

---
 src/field_theory/separable.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/field_theory/separable.lean b/src/field_theory/separable.lean
index 6408d988c73d2..82b71f91d672b 100644
--- a/src/field_theory/separable.lean
+++ b/src/field_theory/separable.lean
@@ -255,6 +255,15 @@ begin
     ... ≤ n * p : mul_le_mul_of_nonneg_left (show 1 ≤ p, from hp.bot_lt) (zero_le n)
 end
 
+theorem contract_expand {f : polynomial R} (hp : p ≠ 0) : contract p (expand R p f) = f :=
+begin
+  ext,
+  rw [coeff_contract hp, coeff_expand hp.bot_lt],
+  split_ifs with h,
+  { rw nat.mul_div_cancel _ hp.bot_lt },
+  { simpa using h }
+end
+
 section char_p
 
 variable [HF : char_p R p]

From 3891dbb604fe5257811fedb1db2d37bf75303608 Mon Sep 17 00:00:00 2001
From: Eric <37984851+ericrbg@users.noreply.github.com>
Date: Tue, 16 Nov 2021 09:30:33 +0000
Subject: [PATCH 08/12] Apply suggestions from code review

Co-authored-by: Johan Commelin <johan@commelin.net>
---
 src/field_theory/separable.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/field_theory/separable.lean b/src/field_theory/separable.lean
index 82b71f91d672b..485dcf791b67c 100644
--- a/src/field_theory/separable.lean
+++ b/src/field_theory/separable.lean
@@ -57,7 +57,7 @@ end
 lemma separable_one : (1 : polynomial R).separable :=
 is_coprime_one_left
 
-@[nontriviality] lemma separable_subsingleton [subsingleton R] (f : polynomial R) : f.separable :=
+@[nontriviality] lemma separable_of_subsingleton [subsingleton R] (f : polynomial R) : f.separable :=
 by simp [separable]
 
 lemma separable_X_add_C (a : R) : (X + C a).separable :=
@@ -239,6 +239,7 @@ begin
     ring },
   exact is_coprime.of_mul_right_left (is_coprime.of_mul_left_left this)
 end
+
 /-- The opposite of `expand`: sends `∑ aₙ xⁿᵖ` to `∑ aₙ xⁿ`. -/
 noncomputable def contract (p : ℕ) (f : polynomial R) : polynomial R :=
 ∑ n in range (f.nat_degree + 1), monomial n (f.coeff (n * p))
@@ -266,8 +267,7 @@ end
 
 section char_p
 
-variable [HF : char_p R p]
-include HF
+variable [char_p R p]
 
 theorem expand_contract [no_zero_divisors R] {f : polynomial R} (hf : f.derivative = 0)
   (hp : p ≠ 0) : expand R p (contract p f) = f :=

From c211dd1f3e7131d5b32dbe76b91a09e71a50b7e3 Mon Sep 17 00:00:00 2001
From: Eric <ericrboidi@gmail.com>
Date: Tue, 16 Nov 2021 09:34:00 +0000
Subject: [PATCH 09/12] 100char, simplify proof

---
 src/field_theory/separable.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/field_theory/separable.lean b/src/field_theory/separable.lean
index 485dcf791b67c..4ecbbad012331 100644
--- a/src/field_theory/separable.lean
+++ b/src/field_theory/separable.lean
@@ -57,8 +57,8 @@ end
 lemma separable_one : (1 : polynomial R).separable :=
 is_coprime_one_left
 
-@[nontriviality] lemma separable_of_subsingleton [subsingleton R] (f : polynomial R) : f.separable :=
-by simp [separable]
+@[nontriviality] lemma separable_of_subsingleton [subsingleton R] (f : polynomial R) :
+  f.separable := by simp [separable]
 
 lemma separable_X_add_C (a : R) : (X + C a).separable :=
 by { rw [separable_def, derivative_add, derivative_X, derivative_C, add_zero],
@@ -259,10 +259,7 @@ end
 theorem contract_expand {f : polynomial R} (hp : p ≠ 0) : contract p (expand R p f) = f :=
 begin
   ext,
-  rw [coeff_contract hp, coeff_expand hp.bot_lt],
-  split_ifs with h,
-  { rw nat.mul_div_cancel _ hp.bot_lt },
-  { simpa using h }
+  simp [coeff_contract hp, coeff_expand hp.bot_lt, nat.mul_div_cancel _ hp.bot_lt]
 end
 
 section char_p

From 556a9bb8c780f749b408d1735d7b919a3ac187a2 Mon Sep 17 00:00:00 2001
From: Eric <ericrboidi@gmail.com>
Date: Wed, 17 Nov 2021 10:28:18 +0000
Subject: [PATCH 10/12] fix new linter

---
 src/field_theory/separable.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/field_theory/separable.lean b/src/field_theory/separable.lean
index 4ecbbad012331..b9304dfb7817e 100644
--- a/src/field_theory/separable.lean
+++ b/src/field_theory/separable.lean
@@ -494,8 +494,8 @@ theorem exists_separable_of_irreducible {f : polynomial F} (hf : irreducible f)
   ∃ (n : ℕ) (g : polynomial F), g.separable ∧ expand F (p ^ n) g = f :=
 begin
   replace hp : p.prime := (char_p.char_is_prime_or_zero F p).resolve_right hp,
-  unfreezingI {
-    induction hn : f.nat_degree using nat.strong_induction_on with N ih generalizing f },
+  unfreezingI
+  { induction hn : f.nat_degree using nat.strong_induction_on with N ih generalizing f },
   rcases separable_or p hf with h | ⟨h1, g, hg, hgf⟩,
   { refine ⟨0, f, h, _⟩, rw [pow_zero, expand_one] },
   { cases N with N,

From 0c620c8b6f1587d5e48ac3000fdd989a127d77b8 Mon Sep 17 00:00:00 2001
From: Eric <ericrboidi@gmail.com>
Date: Thu, 18 Nov 2021 17:04:19 +0000
Subject: [PATCH 11/12] change variables line

---
 src/field_theory/separable.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/field_theory/separable.lean b/src/field_theory/separable.lean
index b9304dfb7817e..6eb392feb8ff6 100644
--- a/src/field_theory/separable.lean
+++ b/src/field_theory/separable.lean
@@ -406,7 +406,9 @@ end comm_ring
 
 section is_domain
 
-theorem is_local_ring_hom_expand (R : Type u) [comm_ring R] [is_domain R] {p : ℕ} (hp : 0 < p) :
+variables (R : Type u) [comm_ring R] [is_domain R]
+
+theorem is_local_ring_hom_expand {p : ℕ} (hp : 0 < p) :
   is_local_ring_hom (↑(expand R p) : polynomial R →+* polynomial R) :=
 begin
   refine ⟨λ f hf1, _⟩, rw ← coe_fn_coe_base at hf1,
@@ -415,7 +417,7 @@ begin
   rw [hf2, is_unit_C] at hf1, rw expand_eq_C hp at hf2, rwa [hf2, is_unit_C]
 end
 
-variables {R : Type u} [comm_ring R] [is_domain R]
+variable {R}
 
 theorem of_irreducible_expand {p : ℕ} (hp : p ≠ 0) {f : polynomial R}
   (hf : irreducible (expand R p f)) : irreducible f :=

From 22feceeda012cf3470809fde93addc04d1cfb441 Mon Sep 17 00:00:00 2001
From: Eric <ericrboidi@gmail.com>
Date: Thu, 18 Nov 2021 17:10:23 +0000
Subject: [PATCH 12/12] tiny golf

---
 src/field_theory/separable_degree.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/field_theory/separable_degree.lean b/src/field_theory/separable_degree.lean
index 051af38e119da..a585b8f233c19 100644
--- a/src/field_theory/separable_degree.lean
+++ b/src/field_theory/separable_degree.lean
@@ -95,7 +95,7 @@ lemma irreducible_has_separable_contraction (q : ℕ) [hF : exp_char F q]
   (f : polynomial F) [irred : irreducible f] : has_separable_contraction q f :=
 begin
   casesI hF,
-  { exact ⟨f, irreducible.separable irred, ⟨0, by rw [pow_zero, expand_one]⟩⟩ },
+  { exact ⟨f, irred.separable, ⟨0, by rw [pow_zero, expand_one]⟩⟩ },
   { rcases exists_separable_of_irreducible q irred ‹q.prime›.ne_zero with ⟨n, g, hgs, hge⟩,
     exact ⟨g, hgs, n, hge⟩, }
 end