fix(data/mv_polynomial): add missing decidable_eq arguments to lemmas (#18848)

This does not change the type of any definitions; the effect of this PR is to make the *statement* of the lemmas syntactically more general.

To ensure this catches them all, this removes `open_locale classical` from the beginning of every file in `data/mv_polynomial` and `ring_theory/mv_polynomial`.

For definitions which bake in a `classical.dec_eq` assumption, this adds a lemma proven by `convert rfl` that unfolds them to a version with an arbitrary `decidable_eq` instance, following a pattern established elsewhere.

Unlike previous refactors of this style this doesn't seemed to have helped any downstream proofs much.

Author: eric-wieser

src/data/mv_polynomial/basic.lean

@@ -72,7 +72,7 @@ polynomial, multivariate polynomial, multivariable polynomial
 
 noncomputable theory
 
-open_locale classical big_operators
+open_locale big_operators
 
 open set function finsupp add_monoid_algebra
 open_locale big_operators
@@ -417,22 +417,22 @@ by convert rfl
 lemma support_monomial_subset : (monomial s a).support ⊆ {s} :=
 support_single_subset
 
-lemma support_add : (p + q).support ⊆ p.support ∪ q.support := finsupp.support_add
+lemma support_add [decidable_eq σ] : (p + q).support ⊆ p.support ∪ q.support := finsupp.support_add
 
 lemma support_X [nontrivial R] : (X n : mv_polynomial σ R).support = {single n 1} :=
-by rw [X, support_monomial, if_neg]; exact one_ne_zero
+by classical; rw [X, support_monomial, if_neg]; exact one_ne_zero
 
 lemma support_X_pow [nontrivial R] (s : σ) (n : ℕ) :
   (X s ^ n : mv_polynomial σ R).support = {finsupp.single s n} :=
-by rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]
+by classical; rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]
 
 @[simp] lemma support_zero : (0 : mv_polynomial σ R).support = ∅ := rfl
 
 lemma support_smul {S₁ : Type*} [smul_zero_class S₁ R] {a : S₁} {f : mv_polynomial σ R} :
   (a • f).support ⊆ f.support :=
 finsupp.support_smul
 
-lemma support_sum {α : Type*} {s : finset α} {f : α → mv_polynomial σ R} :
+lemma support_sum {α : Type*} [decidable_eq σ] {s : finset α} {f : α → mv_polynomial σ R} :
   (∑ x in s, f x).support ⊆ s.bUnion (λ x, (f x).support) := finsupp.support_finset_sum
 
 end support
@@ -455,7 +455,7 @@ lemma sum_def {A} [add_comm_monoid A] {p : mv_polynomial σ R} {b : (σ →₀ 
   p.sum b = ∑ m in p.support, b m (p.coeff m) :=
 by simp [support, finsupp.sum, coeff]
 
-lemma support_mul (p q : mv_polynomial σ R) :
+lemma support_mul [decidable_eq σ] (p q : mv_polynomial σ R) :
   (p * q).support ⊆ p.support.bUnion (λ a, q.support.bUnion $ λ b, {a + b}) :=
 by convert add_monoid_algebra.support_mul p q; ext; convert iff.rfl
 
@@ -525,11 +525,12 @@ by rw [← coeff_X_pow, pow_one]
 
 @[simp] lemma coeff_X (i : σ) :
   coeff (single i 1) (X i : mv_polynomial σ R) = 1 :=
-by rw [coeff_X', if_pos rfl]
+by classical; rw [coeff_X', if_pos rfl]
 
 @[simp] lemma coeff_C_mul (m) (a : R) (p : mv_polynomial σ R) :
   coeff m (C a * p) = a * coeff m p :=
 begin
+  classical,
   rw [mul_def, sum_C],
   { simp [sum_def, coeff_sum] {contextual := tt} },
   simp
@@ -589,6 +590,7 @@ end
 lemma coeff_mul_monomial' (m) (s : σ →₀ ℕ) (r : R) (p : mv_polynomial σ R) :
   coeff m (p * monomial s r) = if s ≤ m then coeff (m - s) p * r else 0 :=
 begin
+  classical,
   obtain rfl | hr := eq_or_ne r 0,
   { simp only [monomial_zero, coeff_zero, mul_zero, if_t_t], },
   haveI : nontrivial R := nontrivial_of_ne _ _ hr,
@@ -742,9 +744,12 @@ finsupp.sum_zero_index
 section
 
 @[simp] lemma eval₂_add : (p + q).eval₂ f g = p.eval₂ f g + q.eval₂ f g :=
-finsupp.sum_add_index
-  (by simp [f.map_zero])
-  (by simp [add_mul, f.map_add])
+begin
+  classical,
+  exact finsupp.sum_add_index
+    (by simp [f.map_zero])
+    (by simp [add_mul, f.map_add])
+end
 
 @[simp] lemma eval₂_monomial : (monomial s a).eval₂ f g = f a * s.prod (λn e, g n ^ e) :=
 finsupp.sum_single_index (by simp [f.map_zero])
@@ -761,6 +766,7 @@ by simp [eval₂_monomial, f.map_one, X, prod_single_index, pow_one]
 lemma eval₂_mul_monomial :
   ∀{s a}, (p * monomial s a).eval₂ f g = p.eval₂ f g * f a * s.prod (λn e, g n ^ e) :=
 begin
+  classical,
   apply mv_polynomial.induction_on p,
   { assume a' s a,
     simp [C_mul_monomial, eval₂_monomial, f.map_mul] },
@@ -994,6 +1000,7 @@ end
 
 lemma coeff_map (p : mv_polynomial σ R) : ∀ (m : σ →₀ ℕ), coeff m (map f p) = f (coeff m p) :=
 begin
+  classical,
   apply mv_polynomial.induction_on p; clear p,
   { intros r m, rw [map_C], simp only [coeff_C], split_ifs, {refl}, rw f.map_zero },
   { intros p q hp hq m, simp only [hp, hq, (map f).map_add, coeff_add], rw f.map_add },

src/data/mv_polynomial/comm_ring.lean

@@ -38,8 +38,6 @@ This will give rise to a monomial in `mv_polynomial σ R` which mathematicians m
 
 noncomputable theory
 
-open_locale classical big_operators
-
 open set function finsupp add_monoid_algebra
 open_locale big_operators
 
@@ -70,7 +68,8 @@ variables (σ a a')
 @[simp] lemma support_neg : (- p).support = p.support :=
 finsupp.support_neg p
 
-lemma support_sub (p q : mv_polynomial σ R) : (p - q).support ⊆ p.support ∪ q.support :=
+lemma support_sub [decidable_eq σ] (p q : mv_polynomial σ R) :
+  (p - q).support ⊆ p.support ∪ q.support :=
 finsupp.support_sub
 
 variables {σ} (p)
@@ -80,9 +79,9 @@ section degrees
 lemma degrees_neg (p : mv_polynomial σ R) : (- p).degrees = p.degrees :=
 by rw [degrees, support_neg]; refl
 
-lemma degrees_sub (p q : mv_polynomial σ R) :
+lemma degrees_sub [decidable_eq σ] (p q : mv_polynomial σ R) :
   (p - q).degrees ≤ p.degrees ⊔ q.degrees :=
-by simpa only [sub_eq_add_neg] using le_trans (degrees_add p (-q)) (by rw degrees_neg)
+by classical; simpa only [sub_eq_add_neg, degrees_neg] using degrees_add p (-q)
 
 end degrees
 
@@ -93,13 +92,14 @@ variables (p q)
 @[simp] lemma vars_neg : (-p).vars = p.vars :=
 by simp [vars, degrees_neg]
 
-lemma vars_sub_subset : (p - q).vars ⊆ p.vars ∪ q.vars :=
+lemma vars_sub_subset [decidable_eq σ] : (p - q).vars ⊆ p.vars ∪ q.vars :=
 by convert vars_add_subset p (-q) using 2; simp [sub_eq_add_neg]
 
 variables {p q}
 
 @[simp]
-lemma vars_sub_of_disjoint (hpq : disjoint p.vars q.vars) : (p - q).vars = p.vars ∪ q.vars :=
+lemma vars_sub_of_disjoint [decidable_eq σ] (hpq : disjoint p.vars q.vars) :
+  (p - q).vars = p.vars ∪ q.vars :=
 begin
   rw ←vars_neg q at hpq,
   convert vars_add_of_disjoint hpq using 2;
@@ -148,6 +148,7 @@ lemma degree_of_sub_lt {x : σ} {f g : mv_polynomial σ R} {k : ℕ} (h : 0 < k)
   (hg : ∀ (m : σ →₀ ℕ), m ∈ g.support → (k ≤ m x) → coeff m f = coeff m g) :
   degree_of x (f - g) < k :=
 begin
+  classical,
   rw degree_of_lt_iff h,
   intros m hm,
   by_contra hc,
@@ -169,9 +170,12 @@ by simp only [total_degree, support_neg]
 
 lemma total_degree_sub (a b : mv_polynomial σ R) :
   (a - b).total_degree ≤ max a.total_degree b.total_degree :=
-calc (a - b).total_degree = (a + -b).total_degree                : by rw sub_eq_add_neg
-                      ... ≤ max a.total_degree (-b).total_degree : total_degree_add a (-b)
-                      ... = max a.total_degree b.total_degree    : by rw total_degree_neg
+begin
+  classical,
+  calc (a - b).total_degree = (a + -b).total_degree                : by rw sub_eq_add_neg
+                        ... ≤ max a.total_degree (-b).total_degree : total_degree_add a (-b)
+                        ... = max a.total_degree b.total_degree    : by rw total_degree_neg
+end
 
 end total_degree
 

src/data/mv_polynomial/equiv.lean

@@ -46,7 +46,7 @@ equivalence, isomorphism, morphism, ring hom, hom
 
 noncomputable theory
 
-open_locale classical big_operators polynomial
+open_locale big_operators polynomial
 
 open set function finsupp add_monoid_algebra
 

src/data/mv_polynomial/monad.lean

@@ -288,9 +288,8 @@ lemma bind₂_monomial_one (f : R →+* mv_polynomial σ S) (d : σ →₀ ℕ)
 by rw [bind₂_monomial, f.map_one, one_mul]
 
 section
-open_locale classical
 
-lemma vars_bind₁ (f : σ → mv_polynomial τ R) (φ : mv_polynomial σ R) :
+lemma vars_bind₁ [decidable_eq τ] (f : σ → mv_polynomial τ R) (φ : mv_polynomial σ R) :
   (bind₁ f φ).vars ⊆ φ.vars.bUnion (λ i, (f i).vars) :=
 begin
   calc (bind₁ f φ).vars
@@ -323,7 +322,8 @@ end
 lemma mem_vars_bind₁ (f : σ → mv_polynomial τ R) (φ : mv_polynomial σ R) {j : τ}
   (h : j ∈ (bind₁ f φ).vars) :
   ∃ (i : σ), i ∈ φ.vars ∧ j ∈ (f i).vars :=
-by simpa only [exists_prop, finset.mem_bUnion, mem_support_iff, ne.def] using vars_bind₁ f φ h
+by classical; simpa only [exists_prop, finset.mem_bUnion, mem_support_iff, ne.def]
+                using vars_bind₁ f φ h
 
 instance monad : monad (λ σ, mv_polynomial σ R) :=
 { map := λ α β f p, rename f p,

src/data/mv_polynomial/pderiv.lean

@@ -47,7 +47,7 @@ namespace mv_polynomial
 
 
 open set function finsupp add_monoid_algebra
-open_locale classical big_operators
+open_locale big_operators
 
 variables {R : Type u} {σ : Type v} {a a' a₁ a₂ : R} {s : σ →₀ ℕ}
 
@@ -57,12 +57,16 @@ variables {R} [comm_semiring R]
 
 /-- `pderiv i p` is the partial derivative of `p` with respect to `i` -/
 def pderiv (i : σ) : derivation R (mv_polynomial σ R) (mv_polynomial σ R) :=
-mk_derivation R $ pi.single i 1
+by letI := classical.dec_eq σ; exact (mk_derivation R $ pi.single i 1)
+
+lemma pderiv_def [decidable_eq σ] (i : σ) : pderiv i = mk_derivation R (pi.single i 1) :=
+by convert rfl
 
 @[simp] lemma pderiv_monomial {i : σ} :
   pderiv i (monomial s a) = monomial (s - single i 1) (a * (s i)) :=
 begin
-  simp only [pderiv, mk_derivation_monomial, finsupp.smul_sum, smul_eq_mul,
+  classical,
+  simp only [pderiv_def, mk_derivation_monomial, finsupp.smul_sum, smul_eq_mul,
     ← smul_mul_assoc, ← (monomial _).map_smul],
   refine (finset.sum_eq_single i (λ j hj hne, _) (λ hi, _)).trans _,
   { simp [pi.single_eq_of_ne hne] },
@@ -74,14 +78,15 @@ lemma pderiv_C {i : σ} : pderiv i (C a) = 0 := derivation_C _ _
 
 lemma pderiv_one {i : σ} : pderiv i (1 : mv_polynomial σ R) = 0 := pderiv_C
 
-@[simp] lemma pderiv_X [d : decidable_eq σ] (i j : σ) :
-  pderiv i (X j : mv_polynomial σ R) = @pi.single σ _ d _ i 1 j :=
-(mk_derivation_X _ _ _).trans (by congr)
+@[simp] lemma pderiv_X [decidable_eq σ] (i j : σ) :
+  pderiv i (X j : mv_polynomial σ R) = @pi.single _ _ _ _ i 1 j :=
+by rw [pderiv_def, mk_derivation_X]
 
-@[simp] lemma pderiv_X_self (i : σ) : pderiv i (X i : mv_polynomial σ R) = 1 := by simp
+@[simp] lemma pderiv_X_self (i : σ) : pderiv i (X i : mv_polynomial σ R) = 1 :=
+by classical; simp
 
 @[simp] lemma pderiv_X_of_ne {i j : σ} (h : j ≠ i) : pderiv i (X j : mv_polynomial σ R) = 0 :=
-by simp [h]
+by classical; simp [h]
 
 lemma pderiv_eq_zero_of_not_mem_vars {i : σ} {f : mv_polynomial σ R} (h : i ∉ f.vars) :
   pderiv i f = 0 :=

src/data/mv_polynomial/rename.lean

@@ -41,7 +41,7 @@ This will give rise to a monomial in `mv_polynomial σ R` which mathematicians m
 
 noncomputable theory
 
-open_locale classical big_operators
+open_locale big_operators
 
 open set function finsupp add_monoid_algebra
 open_locale big_operators
@@ -185,6 +185,7 @@ end
 theorem exists_finset_rename (p : mv_polynomial σ R) :
   ∃ (s : finset σ) (q : mv_polynomial {x // x ∈ s} R), p = rename coe q :=
 begin
+  classical,
   apply induction_on p,
   { intro r, exact ⟨∅, C r, by rw rename_C⟩ },
   { rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩,
@@ -241,6 +242,7 @@ section coeff
 lemma coeff_rename_map_domain (f : σ → τ) (hf : injective f) (φ : mv_polynomial σ R) (d : σ →₀ ℕ) :
   (rename f φ).coeff (d.map_domain f) = φ.coeff d :=
 begin
+  classical,
   apply induction_on' φ,
   { intros u r,
     rw [rename_monomial, coeff_monomial, coeff_monomial],
@@ -252,6 +254,7 @@ lemma coeff_rename_eq_zero (f : σ → τ) (φ : mv_polynomial σ R) (d : τ →
   (h : ∀ u : σ →₀ ℕ, u.map_domain f = d → φ.coeff u = 0) :
   (rename f φ).coeff d = 0 :=
 begin
+  classical,
   rw [rename_eq, ← not_mem_support_iff],
   intro H,
   replace H := map_domain_support H,
@@ -280,7 +283,8 @@ end coeff
 
 section support
 
-lemma support_rename_of_injective {p : mv_polynomial σ R} {f : σ → τ} (h : function.injective f) :
+lemma support_rename_of_injective {p : mv_polynomial σ R} {f : σ → τ} [decidable_eq τ]
+  (h : function.injective f) :
   (rename f p).support = finset.image (map_domain f) p.support :=
 begin
   rw rename_eq,

src/data/mv_polynomial/supported.lean

@@ -38,7 +38,6 @@ algebra.adjoin R (X '' s)
 
 variables {σ R}
 
-open_locale classical
 open algebra
 
 lemma supported_eq_range_rename (s : set σ) :
@@ -67,6 +66,7 @@ variables {s t : set σ}
 
 lemma mem_supported : p ∈ (supported R s) ↔ ↑p.vars ⊆ s :=
 begin
+  classical,
   rw [supported_eq_range_rename, alg_hom.mem_range],
   split,
   { rintros ⟨p, rfl⟩,