chore: forward-port leanprover-community/mathlib#18848 (#4007)

I've been someone sloppy about forward-porting the exact mathport here; a lot of the `classical` additions result in the whole proof being indented, which IMO just adds noise to the diff.

What's important is that:
* `open Classical` is removed from all the same files
* `[DecidableEq _]` is added in the same position to all the same lemmas. In theory mathport will detect if we mess this up, so it's not essential to catch this in review. The linter will tell us if it is added unnecessarily, and the build will fail if is not added someewhere it is needed; so only the argument order is at risk of being wrong.
* The new `foo_def` lemmas are all added in `variables.lean`

Mathlib/Data/MvPolynomial/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.mv_polynomial.basic
-! leanprover-community/mathlib commit 4e529b03dd62b7b7d13806c3fb974d9d4848910e
+! leanprover-community/mathlib commit 2f5b500a507264de86d666a5f87ddb976e2d8de4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -74,7 +74,7 @@ polynomial, multivariate polynomial, multivariable polynomial
 
 noncomputable section
 
-open Classical BigOperators
+open BigOperators
 
 open Set Function Finsupp AddMonoidAlgebra
 
@@ -539,17 +539,18 @@ theorem support_monomial_subset : (monomial s a).support ⊆ {s} :=
   support_single_subset
 #align mv_polynomial.support_monomial_subset MvPolynomial.support_monomial_subset
 
-theorem support_add : (p + q).support ⊆ p.support ∪ q.support :=
+theorem support_add [DecidableEq σ] : (p + q).support ⊆ p.support ∪ q.support :=
   Finsupp.support_add
 #align mv_polynomial.support_add MvPolynomial.support_add
 
 theorem support_X [Nontrivial R] : (X n : MvPolynomial σ R).support = {Finsupp.single n 1} := by
-  rw [X, support_monomial, if_neg]; exact one_ne_zero
+  classical rw [X, support_monomial, if_neg]; exact one_ne_zero
 #align mv_polynomial.support_X MvPolynomial.support_X
 
 theorem support_X_pow [Nontrivial R] (s : σ) (n : ℕ) :
     (X s ^ n : MvPolynomial σ R).support = {Finsupp.single s n} := by
-  rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]
+  classical
+    rw [X_pow_eq_monomial, support_monomial, if_neg (one_ne_zero' R)]
 #align mv_polynomial.support_X_pow MvPolynomial.support_X_pow
 
 @[simp]
@@ -562,7 +563,7 @@ theorem support_smul {S₁ : Type _} [SMulZeroClass S₁ R] {a : S₁} {f : MvPo
   Finsupp.support_smul
 #align mv_polynomial.support_smul MvPolynomial.support_smul
 
-theorem support_sum {α : Type _} {s : Finset α} {f : α → MvPolynomial σ R} :
+theorem support_sum {α : Type _} [DecidableEq σ] {s : Finset α} {f : α → MvPolynomial σ R} :
     (∑ x in s, f x).support ⊆ s.biUnion fun x => (f x).support :=
   Finsupp.support_finset_sum
 #align mv_polynomial.support_sum MvPolynomial.support_sum
@@ -591,7 +592,7 @@ theorem sum_def {A} [AddCommMonoid A] {p : MvPolynomial σ R} {b : (σ →₀ 
     p.sum b = ∑ m in p.support, b m (p.coeff m) := by simp [support, Finsupp.sum, coeff]
 #align mv_polynomial.sum_def MvPolynomial.sum_def
 
-theorem support_mul (p q : MvPolynomial σ R) :
+theorem support_mul [DecidableEq σ] (p q : MvPolynomial σ R) :
     (p * q).support ⊆ p.support.biUnion fun a => q.support.biUnion fun b => {a + b} := by
   convert AddMonoidAlgebra.support_mul p q
 #align mv_polynomial.support_mul MvPolynomial.support_mul
@@ -685,11 +686,12 @@ theorem coeff_X' [DecidableEq σ] (i : σ) (m) :
 
 @[simp]
 theorem coeff_X (i : σ) : coeff (Finsupp.single i 1) (X i : MvPolynomial σ R) = 1 := by
-  rw [coeff_X', if_pos rfl]
+  classical rw [coeff_X', if_pos rfl]
 #align mv_polynomial.coeff_X MvPolynomial.coeff_X
 
 @[simp]
 theorem coeff_C_mul (m) (a : R) (p : MvPolynomial σ R) : coeff m (C a * p) = a * coeff m p := by
+  classical
   rw [mul_def, sum_C]
   · simp (config := { contextual := true }) [sum_def, coeff_sum]
   simp
@@ -760,6 +762,7 @@ theorem support_symmDiff_support_subset_support_add [DecidableEq σ] (p q : MvPo
 
 theorem coeff_mul_monomial' (m) (s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R) :
     coeff m (p * monomial s r) = if s ≤ m then coeff (m - s) p * r else 0 := by
+  classical
   obtain rfl | hr := eq_or_ne r 0
   · simp only [monomial_zero, coeff_zero, MulZeroClass.mul_zero, ite_self]
   haveI : Nontrivial R := nontrivial_of_ne _ _ hr
@@ -865,7 +868,7 @@ variable (σ)
 
 @[simp]
 theorem constantCoeff_C (r : R) : constantCoeff (C r : MvPolynomial σ R) = r := by
-  simp [constantCoeff_eq]
+  classical simp [constantCoeff_eq]
 #align mv_polynomial.constant_coeff_C MvPolynomial.constantCoeff_C
 
 variable {σ}
@@ -950,8 +953,8 @@ theorem eval₂_zero : (0 : MvPolynomial σ R).eval₂ f g = 0 :=
 section
 
 @[simp]
-theorem 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])
+theorem eval₂_add : (p + q).eval₂ f g = p.eval₂ f g + q.eval₂ f g := by
+  classical exact Finsupp.sum_add_index (by simp [f.map_zero]) (by simp [add_mul, f.map_add])
 #align mv_polynomial.eval₂_add MvPolynomial.eval₂_add
 
 @[simp]
@@ -976,6 +979,7 @@ theorem eval₂_X (n) : (X n).eval₂ f g = g n := by
 
 theorem eval₂_mul_monomial :
     ∀ {s a}, (p * monomial s a).eval₂ f g = p.eval₂ f g * f a * s.prod fun n e => g n ^ e := by
+  classical
   apply MvPolynomial.induction_on p
   · intro a' s a
     simp [C_mul_monomial, eval₂_monomial, f.map_mul]
@@ -1263,6 +1267,7 @@ theorem map_eval₂ (f : R →+* S₁) (g : S₂ → MvPolynomial S₃ R) (p : M
 #align mv_polynomial.map_eval₂ MvPolynomial.map_eval₂
 
 theorem coeff_map (p : MvPolynomial σ R) : ∀ m : σ →₀ ℕ, coeff m (map f p) = f (coeff m p) := by
+  classical
   apply MvPolynomial.induction_on p <;> clear p
   · intro r m
     rw [map_C]

Mathlib/Data/MvPolynomial/CommRing.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.mv_polynomial.comm_ring
-! leanprover-community/mathlib commit 972aa4234fa56ce119d19506045158a9d76881fd
+! leanprover-community/mathlib commit 2f5b500a507264de86d666a5f87ddb976e2d8de4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -40,7 +40,7 @@ This will give rise to a monomial in `MvPolynomial σ R` which mathematicians mi
 
 noncomputable section
 
-open Classical BigOperators Set Function Finsupp AddMonoidAlgebra
+open Set Function Finsupp AddMonoidAlgebra
 
 universe u v
 
@@ -88,7 +88,8 @@ theorem support_neg : (-p).support = p.support :=
   Finsupp.support_neg p
 #align mv_polynomial.support_neg MvPolynomial.support_neg
 
-theorem support_sub (p q : MvPolynomial σ R) : (p - q).support ⊆ p.support ∪ q.support :=
+theorem support_sub [DecidableEq σ] (p q : MvPolynomial σ R) :
+    (p - q).support ⊆ p.support ∪ q.support :=
   Finsupp.support_sub
 #align mv_polynomial.support_sub MvPolynomial.support_sub
 
@@ -100,7 +101,8 @@ theorem degrees_neg (p : MvPolynomial σ R) : (-p).degrees = p.degrees := by
   rw [degrees, support_neg]; rfl
 #align mv_polynomial.degrees_neg MvPolynomial.degrees_neg
 
-theorem degrees_sub (p q : MvPolynomial σ R) : (p - q).degrees ≤ p.degrees ⊔ q.degrees := by
+theorem degrees_sub [DecidableEq σ] (p q : MvPolynomial σ 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])
 #align mv_polynomial.degrees_sub MvPolynomial.degrees_sub
 
@@ -112,12 +114,13 @@ section Vars
 theorem vars_neg : (-p).vars = p.vars := by simp [vars, degrees_neg]
 #align mv_polynomial.vars_neg MvPolynomial.vars_neg
 
-theorem vars_sub_subset : (p - q).vars ⊆ p.vars ∪ q.vars := by
+theorem vars_sub_subset [DecidableEq σ] : (p - q).vars ⊆ p.vars ∪ q.vars := by
   convert vars_add_subset p (-q) using 2 <;> simp [sub_eq_add_neg]
 #align mv_polynomial.vars_sub_subset MvPolynomial.vars_sub_subset
 
 @[simp]
-theorem vars_sub_of_disjoint (hpq : Disjoint p.vars q.vars) : (p - q).vars = p.vars ∪ q.vars := by
+theorem vars_sub_of_disjoint [DecidableEq σ] (hpq : Disjoint p.vars q.vars) :
+    (p - q).vars = p.vars ∪ q.vars := by
   rw [← vars_neg q] at hpq
   convert vars_add_of_disjoint hpq using 2 <;> simp [sub_eq_add_neg]
 #align mv_polynomial.vars_sub_of_disjoint MvPolynomial.vars_sub_of_disjoint
@@ -180,6 +183,7 @@ theorem degreeOf_sub_lt {x : σ} {f g : MvPolynomial σ R} {k : ℕ} (h : 0 < k)
     (hf : ∀ m : σ →₀ ℕ, m ∈ f.support → k ≤ m x → coeff m f = coeff m g)
     (hg : ∀ m : σ →₀ ℕ, m ∈ g.support → k ≤ m x → coeff m f = coeff m g) :
     degreeOf x (f - g) < k := by
+  classical
   rw [degreeOf_lt_iff h]
   intro m hm
   by_contra' hc

Mathlib/Data/MvPolynomial/Equiv.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.mv_polynomial.equiv
-! leanprover-community/mathlib commit 70fd9563a21e7b963887c9360bd29b2393e6225a
+! leanprover-community/mathlib commit 2f5b500a507264de86d666a5f87ddb976e2d8de4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -47,7 +47,7 @@ equivalence, isomorphism, morphism, ring hom, hom
 
 noncomputable section
 
-open Classical BigOperators Polynomial Set Function Finsupp AddMonoidAlgebra
+open BigOperators Polynomial Set Function Finsupp AddMonoidAlgebra
 
 universe u v w x
 

Mathlib/Data/MvPolynomial/Monad.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Robert Y. Lewis
 
 ! This file was ported from Lean 3 source module data.mv_polynomial.monad
-! leanprover-community/mathlib commit 5120cf49cb659e2499edd7e4d336a04efd598f2f
+! leanprover-community/mathlib commit 2f5b500a507264de86d666a5f87ddb976e2d8de4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -357,9 +357,7 @@ theorem bind₂_monomial_one (f : R →+* MvPolynomial σ S) (d : σ →₀ ℕ)
 
 section
 
-open Classical
-
-theorem vars_bind₁ (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
+theorem vars_bind₁ [DecidableEq τ] (f : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
     (bind₁ f φ).vars ⊆ φ.vars.biUnion fun i => (f i).vars := by
   calc
     (bind₁ f φ).vars = (φ.support.sum fun x : σ →₀ ℕ => (bind₁ f) (monomial x (coeff x φ))).vars :=

Mathlib/Data/MvPolynomial/Rename.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 
 ! This file was ported from Lean 3 source module data.mv_polynomial.rename
-! leanprover-community/mathlib commit eabc6192c84ccce3936a8577a987b80b95ba75f6
+! leanprover-community/mathlib commit 2f5b500a507264de86d666a5f87ddb976e2d8de4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -43,7 +43,7 @@ This will give rise to a monomial in `MvPolynomial σ R` which mathematicians mi
 
 noncomputable section
 
-open Classical BigOperators
+open BigOperators
 
 open Set Function Finsupp AddMonoidAlgebra
 
@@ -230,6 +230,7 @@ end
 /-- Every polynomial is a polynomial in finitely many variables. -/
 theorem exists_finset_rename (p : MvPolynomial σ R) :
     ∃ (s : Finset σ)(q : MvPolynomial { x // x ∈ s } R), p = rename (↑) q := by
+  classical
   apply induction_on p
   · intro r
     exact ⟨∅, C r, by rw [rename_C]⟩
@@ -294,6 +295,7 @@ section Coeff
 @[simp]
 theorem coeff_rename_mapDomain (f : σ → τ) (hf : Injective f) (φ : MvPolynomial σ R) (d : σ →₀ ℕ) :
     (rename f φ).coeff (d.mapDomain f) = φ.coeff d := by
+  classical
   apply φ.induction_on' (P := fun ψ => coeff (Finsupp.mapDomain f d) ((rename f) ψ) = coeff d ψ)
   -- Lean could no longer infer the motive
   · intro u r
@@ -305,6 +307,7 @@ theorem coeff_rename_mapDomain (f : σ → τ) (hf : Injective f) (φ : MvPolyno
 
 theorem coeff_rename_eq_zero (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ)
     (h : ∀ u : σ →₀ ℕ, u.mapDomain f = d → φ.coeff u = 0) : (rename f φ).coeff d = 0 := by
+  classical
   rw [rename_eq, ← not_mem_support_iff]
   intro H
   replace H := mapDomain_support H
@@ -337,7 +340,8 @@ end Coeff
 
 section Support
 
-theorem support_rename_of_injective {p : MvPolynomial σ R} {f : σ → τ} (h : Function.Injective f) :
+theorem support_rename_of_injective {p : MvPolynomial σ R} {f : σ → τ} [DecidableEq τ]
+    (h : Function.Injective f) :
     (rename f p).support = Finset.image (Finsupp.mapDomain f) p.support := by
   rw [rename_eq]
   exact Finsupp.mapDomain_support_of_injective (mapDomain_injective h) _

Mathlib/Data/MvPolynomial/Supported.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 
 ! This file was ported from Lean 3 source module data.mv_polynomial.supported
-! leanprover-community/mathlib commit a26d17fcd679e43d380d0583b33c9eca5359d41e
+! leanprover-community/mathlib commit 2f5b500a507264de86d666a5f87ddb976e2d8de4
 ! Please do not edit these lines, except to modify the commit id
 ! if you have ported upstream changes.
 -/
@@ -45,8 +45,6 @@ noncomputable def supported (s : Set σ) : Subalgebra R (MvPolynomial σ R) :=
 
 variable {R}
 
-open Classical
-
 open Algebra
 
 theorem supported_eq_range_rename (s : Set σ) : supported R s = (rename ((↑) : s → σ)).range := by
@@ -78,6 +76,7 @@ set_option linter.uppercaseLean3 false in
 variable {s t : Set σ}
 
 theorem mem_supported : p ∈ supported R s ↔ ↑p.vars ⊆ s := by
+  classical
   rw [supported_eq_range_rename, AlgHom.mem_range]
   constructor
   · rintro ⟨p, rfl⟩