fix: restore the NonUnitalCommRing (Fin n) instance (#25531)

`#synth NonUnitalCommRing (Fin n)` was made to fail uncecessarily in #25476;
it doesn't imply `NatCast` so is not relevant to the goal of that PR.

Also restores the `CommMonoid` and `HasDistribNeg` and `NeZero 1` instances.

Author: eric-wieser

Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean

@@ -398,7 +398,6 @@ lemma mk_XYIdeal'_mul_mk_XYIdeal' {x₁ x₂ y₁ y₂ : F} (h₁ : W.Nonsingula
 
 /-! ## Norms on the affine coordinate ring -/
 
-open Fin.CommRing in -- TODO: should this be refactored to avoid needing the coercion?
 lemma norm_smul_basis (p q : R[X]) : Algebra.norm R[X] (p • (1 : W'.CoordinateRing) + q • mk W' Y) =
     p ^ 2 - p * q * (C W'.a₁ * X + C W'.a₃) -
       q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆) := by

Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian/Basic.lean

@@ -296,7 +296,6 @@ associated to a Weierstrass curve `W` in Jacobian coordinates. -/
 noncomputable def polynomialX : MvPolynomial (Fin 3) R :=
   pderiv x W'.polynomial
 
-open Fin.CommRing in
 lemma polynomialX_eq : W'.polynomialX =
     C W'.a₁ * X 1 * X 2 - (C 3 * X 0 ^ 2 + C (2 * W'.a₂) * X 0 * X 2 ^ 2 + C W'.a₄ * X 2 ^ 4) := by
   rw [polynomialX, polynomial]
@@ -321,7 +320,6 @@ associated to a Weierstrass curve `W` in Jacobian coordinates. -/
 noncomputable def polynomialY : MvPolynomial (Fin 3) R :=
   pderiv y W'.polynomial
 
-open Fin.CommRing in
 lemma polynomialY_eq : W'.polynomialY = C 2 * X 1 + C W'.a₁ * X 0 * X 2 + C W'.a₃ * X 2 ^ 3 := by
   rw [polynomialY, polynomial]
   pderiv_simp

Mathlib/AlgebraicGeometry/EllipticCurve/Projective/Basic.lean

@@ -287,7 +287,6 @@ associated to a Weierstrass curve `W` in projective coordinates. -/
 noncomputable def polynomialX : MvPolynomial (Fin 3) R :=
   pderiv x W'.polynomial
 
-open Fin.CommRing in
 lemma polynomialX_eq : W'.polynomialX =
     C W'.a₁ * X 1 * X 2 - (C 3 * X 0 ^ 2 + C (2 * W'.a₂) * X 0 * X 2 + C W'.a₄ * X 2 ^ 2) := by
   rw [polynomialX, polynomial]
@@ -311,7 +310,6 @@ associated to a Weierstrass curve `W` in projective coordinates. -/
 noncomputable def polynomialY : MvPolynomial (Fin 3) R :=
   pderiv y W'.polynomial
 
-open Fin.CommRing in
 lemma polynomialY_eq : W'.polynomialY =
     C 2 * X 1 * X 2 + C W'.a₁ * X 0 * X 2 + C W'.a₃ * X 2 ^ 2 := by
   rw [polynomialY, polynomial]

Mathlib/Combinatorics/Extremal/RuzsaSzemeredi.lean

@@ -173,12 +173,12 @@ lemma addRothNumber_le_ruzsaSzemerediNumber :
   rw [← hscard, ← card_triangleIndices, ← card_triangles]
   exact (locallyLinear hs).le_ruzsaSzemerediNumber
 
-open Fin.CommRing in -- TODO: can this be refactored to avoid using the ring structure in the proof?
 lemma rothNumberNat_le_ruzsaSzemerediNumberNat (n : ℕ) :
     (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3) := by
   let α := Fin (2 * n + 1)
   have : Nat.Coprime 2 (2 * n + 1) := by simp
   haveI : Fact (IsUnit (2 : Fin (2 * n + 1))) := ⟨by simpa using (ZMod.unitOfCoprime 2 this).isUnit⟩
+  open scoped Fin.CommRing in
   calc
     (2 * n + 1) * rothNumberNat n
     _ = Fintype.card α * addRothNumber (Iio (n : α)) := by

Mathlib/Data/BitVec.lean

@@ -51,13 +51,11 @@ lemma toFin_pow (x : BitVec w) (n : ℕ)    : toFin (x ^ n) = x.toFin ^ n := by
 ## Ring
 -/
 
-open Fin.CommRing
-
 -- Verify that the `HPow` instance from Lean agrees definitionally with the instance via `Monoid`.
 example : @instHPow (Fin (2 ^ w)) ℕ Monoid.toNatPow = Lean.Grind.Fin.instHPowFinNatOfNeZero := rfl
 
-open Fin.CommRing in
 instance : CommSemiring (BitVec w) :=
+  open Fin.CommRing in
   toFin_injective.commSemiring _
     rfl /- toFin_zero -/
     rfl /- toFin_one -/
@@ -76,6 +74,7 @@ theorem _root_.Fin.intCast_def' {n : Nat} [NeZero n] (x : Int) :
   dsimp [Int.cast, IntCast.intCast, Int.castDef]
   split <;> (simp [Fin.intCast]; omega)
 
+open Fin.CommRing in
 @[simp] theorem _root_.Fin.val_intCast {n : Nat} [NeZero n] (x : Int) :
     (x : Fin n).val = (x % n).toNat := by
   rw [Fin.intCast_def']
@@ -90,6 +89,7 @@ theorem _root_.Fin.intCast_def' {n : Nat} [NeZero n] (x : Int) :
       omega
 
 -- TODO: move to the Lean4 repository.
+open Fin.CommRing in
 theorem ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = ↑z := by
   cases w
   case zero =>
@@ -108,8 +108,8 @@ open Fin.CommRing in
 theorem toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z := by
   apply toFin_inj.mpr <| (ofFin_intCast z).symm
 
-open Fin.CommRing in
 instance : CommRing (BitVec w) :=
+  open Fin.CommRing in
   toFin_injective.commRing _
     toFin_zero toFin_one toFin_add toFin_mul toFin_neg toFin_sub
     toFin_nsmul toFin_zsmul toFin_pow toFin_natCast toFin_intCast

Mathlib/Data/ZMod/Defs.lean

@@ -69,6 +69,23 @@ instance instDistrib (n : ℕ) : Distrib (Fin n) :=
     right_distrib := fun a b c => by
       rw [mul_comm, left_distrib_aux, mul_comm _ b, mul_comm] }
 
+instance instNonUnitalCommRing (n : ℕ) [NeZero n] : NonUnitalCommRing (Fin n) where
+  __ := Fin.addCommGroup n
+  __ := Fin.instCommSemigroup n
+  __ := Fin.instDistrib n
+  zero_mul := Fin.zero_mul'
+  mul_zero := Fin.mul_zero'
+
+instance instCommMonoid (n : ℕ) [NeZero n] : CommMonoid (Fin n) where
+  one_mul := Fin.one_mul'
+  mul_one := Fin.mul_one'
+
+/-- Note this is more general than `Fin.instCommRing` as it applies (vacuously) to `Fin 0` too. -/
+instance instHasDistribNeg (n : ℕ) : HasDistribNeg (Fin n) where
+  toInvolutiveNeg := Fin.instInvolutiveNeg n
+  mul_neg := Nat.casesOn n finZeroElim fun _i => mul_neg
+  neg_mul := Nat.casesOn n finZeroElim fun _i => neg_mul
+
 /--
 Commutative ring structure on `Fin n`.
 
@@ -83,27 +100,22 @@ For example, for `x : Fin k` and `n : Nat`,
 it causes `x < n` to be elaborated as `x < ↑n` rather than `↑x < n`,
 silently introducing wraparound arithmetic.
 -/
-def instCommRing (n : ℕ) [NeZero n] : CommRing (Fin n) :=
-  { Fin.instAddMonoidWithOne n, Fin.addCommGroup n, Fin.instCommSemigroup n,
-      Fin.instDistrib n with
-    intCast n := Fin.intCast n
-    one_mul := Fin.one_mul'
-    mul_one := Fin.mul_one',
-    zero_mul := Fin.zero_mul'
-    mul_zero := Fin.mul_zero' }
+def instCommRing (n : ℕ) [NeZero n] : CommRing (Fin n) where
+  __ := Fin.instAddMonoidWithOne n
+  __ := Fin.addCommGroup n
+  __ := Fin.instCommSemigroup n
+  __ := Fin.instNonUnitalCommRing n
+  __ := Fin.instCommMonoid n
+  intCast n := Fin.intCast n
 
 namespace CommRing
 
 attribute [scoped instance] Fin.instCommRing
 
 end CommRing
 
-open Fin.CommRing in
-/-- Note this is more general than `Fin.instCommRing` as it applies (vacuously) to `Fin 0` too. -/
-def instHasDistribNeg (n : ℕ) : HasDistribNeg (Fin n) :=
-  { toInvolutiveNeg := Fin.instInvolutiveNeg n
-    mul_neg := Nat.casesOn n finZeroElim fun _i => mul_neg
-    neg_mul := Nat.casesOn n finZeroElim fun _i => neg_mul }
+instance (n : ℕ) [NeZero n] : NeZero (1 : Fin (n + 1)) :=
+  open Fin.CommRing in inferInstance
 
 end Fin
 

Mathlib/FieldTheory/AxGrothendieck.lean

@@ -140,7 +140,6 @@ noncomputable def genericPolyMapSurjOnOfInjOn [Finite ι]
             (fun i => (Equiv.sumAssoc _ _ _).symm (Sum.inr i)))))
   Formula.iAlls (α ⊕ Σ i : ι, mons i) ((mapsTo.imp <| injOn.imp <| surjOn).relabel Sum.inr)
 
-open Fin.CommRing in -- TODO: can this be refactored to avoid using the ring structure in the proof?
 theorem realize_genericPolyMapSurjOnOfInjOn
     [Finite ι] (φ : ring.Formula (α ⊕ ι)) (mons : ι → Finset (ι →₀ ℕ)) :
     (K ⊨ genericPolyMapSurjOnOfInjOn φ mons) ↔

Mathlib/LinearAlgebra/LinearDisjoint.lean

@@ -483,7 +483,6 @@ section
 
 variable [Nontrivial R]
 
-open Fin.CommRing in -- TODO: can this be refactored to avoid using the ring structure in the proof?
 /-- If `M` and `N` are linearly disjoint, if `M` is flat, then any two commutative
 elements of `↥(M ⊓ N)` are not `R`-linearly independent (namely, their span is not `R ^ 2`). -/
 theorem not_linearIndependent_pair_of_commute_of_flat_left [Module.Flat R M]
@@ -500,7 +499,6 @@ theorem not_linearIndependent_pair_of_commute_of_flat_left [Module.Flat R M]
   repeat rw [AddSubmonoid.mk_eq_zero, ZeroMemClass.coe_eq_zero] at hm
   exact h.ne_zero 0 hm.2
 
-open Fin.CommRing in
 /-- If `M` and `N` are linearly disjoint, if `N` is flat, then any two commutative
 elements of `↥(M ⊓ N)` are not `R`-linearly independent (namely, their span is not `R ^ 2`). -/
 theorem not_linearIndependent_pair_of_commute_of_flat_right [Module.Flat R N]

Mathlib/MeasureTheory/Integral/RieszMarkovKakutani/Basic.lean

@@ -154,7 +154,6 @@ section PartitionOfUnity
 
 variable [T2Space X] [LocallyCompactSpace X]
 
-open Fin.CommRing in -- TODO: can this be refactored to avoid using the ring structure in the proof?
 lemma exists_continuous_add_one_of_isCompact_nnreal
     {s₀ s₁ : Set X} {t : Set X} (s₀_compact : IsCompact s₀) (s₁_compact : IsCompact s₁)
     (t_compact : IsCompact t) (disj : Disjoint s₀ s₁) (hst : s₀ ∪ s₁ ⊆ t) :

Mathlib/SetTheory/Cardinal/Free.lean

@@ -105,7 +105,6 @@ end Cardinal
 
 section Nonempty
 
-open Fin.CommRing in
 /-- A commutative ring can be constructed on any non-empty type.
 
 See also `Infinite.nonempty_field`. -/
@@ -115,7 +114,7 @@ instance nonempty_commRing [Nonempty α] : Nonempty (CommRing α) := by
     have : NeZero (Fintype.card α) := ⟨by inhabit α; simp⟩
     classical
     obtain ⟨e⟩ := Fintype.truncEquivFin α
-    exact ⟨e.commRing⟩
+    exact ⟨open scoped Fin.CommRing in e.commRing⟩
   · have ⟨e⟩ : Nonempty (α ≃ FreeCommRing α) := by simp [← Cardinal.eq]
     exact ⟨e.commRing⟩