feat(ring_theory/polynomial): refactor of is_integral_domain_fin (#2119)

* chore(ring_theory/polynomial): refactor proof of is_noetherian_ring_fin

* not there yet

* feat(ring_theory/polynomial): refactor of is_integral_domain_fin

* fix

* refactor

* fix

* fix

* suggestion from linter

* Update src/data/mv_polynomial.lean

Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

src/data/mv_polynomial.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 -/
 
 import algebra.ring
-import data.finsupp data.polynomial data.equiv.algebra
+import data.finsupp data.polynomial data.equiv.algebra data.equiv.fin
 
 /-!
 # Multivariate polynomials
@@ -1263,6 +1263,15 @@ def option_equiv_right : mv_polynomial (option β) α ≃+* mv_polynomial β (po
 (sum_ring_equiv α β unit).trans $
 ring_equiv_congr (mv_polynomial unit α) (punit_ring_equiv α)
 
+/--
+The ring isomorphism between multivariable polynomials in `fin (n + 1)` and
+polynomials over multivariable polynomials in `fin n`.
+-/
+def fin_succ_equiv (n : ℕ) :
+  mv_polynomial (fin (n + 1)) α ≃+* polynomial (mv_polynomial (fin n) α) :=
+(ring_equiv_of_equiv α (fin_succ_equiv n)).trans
+  (option_equiv_left α (fin n))
+
 end
 
 end equiv

src/data/polynomial.lean

@@ -2461,3 +2461,13 @@ end
 end identities
 
 end polynomial
+
+namespace is_integral_domain
+
+variables {α : Type*} [comm_ring α]
+
+/-- Lift evidence that `is_integral_domain α` to `is_integral_domain (polynomial α)`. -/
+lemma polynomial (h : is_integral_domain α) : is_integral_domain (polynomial α) :=
+@integral_domain.to_is_integral_domain _ (@polynomial.integral_domain _ (h.to_integral_domain _))
+
+end is_integral_domain

src/ring_theory/polynomial.lean

@@ -299,8 +299,7 @@ theorem is_noetherian_ring_fin [is_noetherian_ring R] :
 | 0 := is_noetherian_ring_fin_0
 | (n+1) :=
   @is_noetherian_ring_of_ring_equiv (polynomial (mv_polynomial (fin n) R)) _ _ _
-    ((mv_polynomial.option_equiv_left R (fin n)).symm.trans (mv_polynomial.ring_equiv_of_equiv R
-      (fin_succ_equiv n).symm))
+    (mv_polynomial.fin_succ_equiv _ n).symm
     (@polynomial.is_noetherian_ring (mv_polynomial (fin n) R) _ (is_noetherian_ring_fin))
 
 /-- The multivariate polynomial ring in finitely many variables over a noetherian ring
@@ -311,26 +310,25 @@ trunc.induction_on (fintype.equiv_fin σ) $ λ e,
 @is_noetherian_ring_of_ring_equiv (mv_polynomial (fin (fintype.card σ)) R) _ _ _
   (mv_polynomial.ring_equiv_of_equiv _ e.symm) is_noetherian_ring_fin
 
+lemma is_integral_domain_fin_zero (R : Type u) [comm_ring R] (hR : is_integral_domain R) :
+  is_integral_domain (mv_polynomial (fin 0) R) :=
+ring_equiv.is_integral_domain R hR
+  ((ring_equiv_of_equiv R fin_zero_equiv').trans (mv_polynomial.pempty_ring_equiv R))
+
 /-- Auxilliary lemma:
 Multivariate polynomials over an integral domain
 with variables indexed by `fin n` form an integral domain.
 This fact is proven inductively,
 and then used to prove the general case without any finiteness hypotheses.
 See `mv_polynomial.integral_domain` for the general case. -/
-lemma is_integral_domain_fin (R : Type u) [comm_ring R] (hR : is_integral_domain R) (n : ℕ) :
-  is_integral_domain (mv_polynomial (fin n) R) :=
-begin
-  induction n with n ih,
-  { let e : mv_polynomial (fin 0) R ≃+* R :=
-      (ring_equiv_of_equiv R fin_zero_equiv').trans (mv_polynomial.pempty_ring_equiv R),
-    exact ring_equiv.is_integral_domain R hR e },
-  let e : mv_polynomial (fin (n.succ)) R ≃+* polynomial (mv_polynomial (fin n) R) :=
-    (ring_equiv_of_equiv R $ fin_succ_equiv n).trans (option_equiv_left R (fin n)),
-  refine ring_equiv.is_integral_domain (polynomial (mv_polynomial (fin n) R)) _ e,
-  letI _ih := @is_integral_domain.to_integral_domain (mv_polynomial (fin n) R) _ ih,
-  letI _id := @polynomial.integral_domain _ _ih,
-  exact @integral_domain.to_is_integral_domain _ _id,
-end
+lemma is_integral_domain_fin (R : Type u) [comm_ring R] (hR : is_integral_domain R) :
+  ∀ (n : ℕ), is_integral_domain (mv_polynomial (fin n) R)
+| 0 := is_integral_domain_fin_zero R hR
+| (n+1) :=
+  ring_equiv.is_integral_domain
+    (polynomial (mv_polynomial (fin n) R))
+    (is_integral_domain_fin n).polynomial
+    (mv_polynomial.fin_succ_equiv _ n)
 
 lemma is_integral_domain_fintype (R : Type u) (σ : Type v) [comm_ring R] [fintype σ]
   (hR : is_integral_domain R) : is_integral_domain (mv_polynomial σ R) :=