chore(IsFractionRing): make argument explicit (#36655)

Makes the base ring an explicit argument in `IsFractionRing.div_surjective`. This argument cannot be inferred by typeclass inference, because the base ring is not an `outParam` or `semiOutParam` in the type of `IsFractionRing`. It is also rarely determined by the expected type, since this is typically used as the discriminant for an `obtain` or `rcases`.

Also update every usage of `IsFractionRing.div_surjective` to take advantage of this explicit argument.

Author: plp127

Mathlib/Algebra/Algebra/Epi.lean

@@ -62,7 +62,7 @@ end Semiring
 instance (R A : Type*) [CommRing R] [IsDomain R] [Field A] [Algebra R A] [IsFractionRing R A] :
     Algebra.IsEpi R A := by
   refine (isEpi_iff_forall_one_tmul_eq R A).mpr fun x ↦ ?_
-  obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective (A := R) x
+  obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective R x
   set f := algebraMap R A with hf
   replace hb : f b ≠ 0 := by aesop
   calc 1 ⊗ₜ[R] (f a / f b)

Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

@@ -124,13 +124,13 @@ theorem IsGaloisGroup.to_isFractionRing [Finite G] [hGAB : IsGaloisGroup G A B]
   refine ⟨⟨fun h ↦ ?_⟩, ⟨fun g x y ↦ ?_⟩, ⟨fun x h ↦ ?_⟩⟩
   · have := hGAB.faithful
     exact eq_of_smul_eq_smul fun y ↦ by simpa [← algebraMap.coe_smul'] using h (algebraMap B L y)
-  · obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective (A := A) x
-    obtain ⟨c, d, hd, rfl⟩ := IsFractionRing.div_surjective (A := B) y
+  · obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective A x
+    obtain ⟨c, d, hd, rfl⟩ := IsFractionRing.div_surjective B y
     simp [Algebra.smul_def, smul_mul', smul_div₀', hc, ← algebraMap.coe_smul']
   · have := hGAB.isInvariant.isIntegral
     have : Nontrivial A := (IsFractionRing.nontrivial_iff_nontrivial A K).mpr inferInstance
     have : Nontrivial B := (IsFractionRing.nontrivial_iff_nontrivial B L).mpr inferInstance
-    obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := B) x
+    obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective B x
     have hy' : algebraMap B L y ≠ 0 := by simpa using nonZeroDivisors.ne_zero hy
     obtain ⟨b, a, ha, hb⟩ := (Algebra.IsAlgebraic.isAlgebraic (R := A) y).exists_smul_eq_mul x hy
     rw [mul_comm, Algebra.smul_def, mul_comm] at hb
@@ -152,7 +152,7 @@ theorem IsGaloisGroup.of_isFractionRing [hGKL : IsGaloisGroup G K L]
   refine ⟨⟨fun h ↦ ?_⟩, ⟨fun g x y ↦ IsFractionRing.injective B L ?_⟩, ⟨fun x h ↦ ?_⟩⟩
   · have := hGKL.faithful
     refine eq_of_smul_eq_smul fun (y : L) ↦ ?_
-    obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective (A := B) y
+    obtain ⟨a, b, hb, rfl⟩ := IsFractionRing.div_surjective B y
     simp only [smul_div₀', ← algebraMap.coe_smul', h]
   · simp [Algebra.smul_def, algebraMap.coe_smul', ← hc]
   · obtain ⟨b, hb⟩ := hGKL.isInvariant.isInvariant (algebraMap B L x)

Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean

@@ -326,7 +326,7 @@ theorem hasFiniteMulSupport_int {x : 𝓞 K} (h_x_nezero : x ≠ 0) :
 @[fun_prop]
 theorem hasFiniteMulSupport {x : K} (h_x_nezero : x ≠ 0) :
     (fun w : FinitePlace K ↦ w x).HasFiniteMulSupport := by
-  rcases IsFractionRing.div_surjective (A := 𝓞 K) x with ⟨a, b, hb, rfl⟩
+  rcases IsFractionRing.div_surjective (𝓞 K) x with ⟨a, b, hb, rfl⟩
   simp_all only [ne_eq, div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff, not_or, map_div₀]
   obtain ⟨ha, hb⟩ := h_x_nezero
   simp_rw [← RingOfIntegers.coe_eq_algebraMap]

Mathlib/NumberTheory/NumberField/ProductFormula.lean

@@ -78,7 +78,7 @@ equal to the inverse of the absolute value of `Algebra.norm ℚ x`. -/
 theorem FinitePlace.prod_eq_inv_abs_norm {x : K} (h_x_nezero : x ≠ 0) :
     ∏ᶠ w : FinitePlace K, w x = |(Algebra.norm ℚ) x|⁻¹ := by
   --reduce to 𝓞 K
-  rcases IsFractionRing.div_surjective (A := 𝓞 K) x with ⟨a, b, hb, rfl⟩
+  rcases IsFractionRing.div_surjective (𝓞 K) x with ⟨a, b, hb, rfl⟩
   apply nonZeroDivisors.ne_zero at hb
   have ha : a ≠ 0 := by
     rintro rfl

Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean

@@ -82,7 +82,7 @@ theorem IsDecompositionField.of_isGaloisGroup [h : IsGaloisGroup (stabilizer G P
   · refine (stabilizerEquiv _ (IsGaloisGroup.mulEquivAlgEquiv G K L) fun _ _ ↦ ?_).symm
     apply FaithfulSMul.algebraMap_injective B L
     simp [algebraMap.smul']
-  · obtain ⟨y, z, _, rfl⟩ := IsFractionRing.div_surjective (A := B) x
+  · obtain ⟨y, z, _, rfl⟩ := IsFractionRing.div_surjective B x
     simp_rw [smul_div₀', subgroup_smul_def, ← algebraMap.smul', ← subgroup_smul_def,
       stabilizerEquiv_symm_apply_smul]
 
@@ -92,7 +92,7 @@ theorem IsInertiaField.of_isGaloisGroup [h : IsGaloisGroup (inertia G P) D L] :
   · refine (inertiaEquiv _ (IsGaloisGroup.mulEquivAlgEquiv G K L) fun _ _ ↦ ?_).symm
     apply FaithfulSMul.algebraMap_injective B L
     simp [algebraMap.smul']
-  · obtain ⟨y, z, _, rfl⟩ := IsFractionRing.div_surjective (A := B) x
+  · obtain ⟨y, z, _, rfl⟩ := IsFractionRing.div_surjective B x
     simp_rw [smul_div₀', subgroup_smul_def, ← algebraMap.smul', ← subgroup_smul_def,
       inertiaEquiv_symm_apply_smul]
 

Mathlib/RingTheory/Invariant/Basic.lean

@@ -360,7 +360,7 @@ private theorem fixed_of_fixed2 (f : Gal(L/K)) (x : L)
   obtain ⟨_⟩ := nonempty_fintype G
   have : P.IsPrime := Ideal.over_def Q P ▸ Ideal.IsPrime.under A Q
   have : Algebra.IsIntegral A B := Algebra.IsInvariant.isIntegral A B G
-  obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := B ⧸ Q) x
+  obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (B ⧸ Q) x
   obtain ⟨b, a, ha, h⟩ := (Algebra.IsAlgebraic.isAlgebraic (R := A ⧸ P) y).exists_smul_eq_mul x hy
   replace ha : algebraMap (A ⧸ P) L a ≠ 0 := by
     rwa [Ne, algebraMap_apply (A ⧸ P) K L, algebraMap_eq_zero_iff, algebraMap_eq_zero_iff]

Mathlib/RingTheory/Localization/AsSubring.lean

@@ -140,7 +140,7 @@ instance isLocalization_ofField : IsLocalization S (ofField K S hS) := by
 
 instance (S : Subalgebra A K) : IsFractionRing S K := by
   refine IsFractionRing.of_field S K fun z ↦ ?_
-  rcases IsFractionRing.div_surjective (A := A) z with ⟨x, y, _, eq⟩
+  rcases IsFractionRing.div_surjective A z with ⟨x, y, _, eq⟩
   exact ⟨algebraMap A S x, algebraMap A S y, eq.symm⟩
 
 instance isFractionRing_ofField : IsFractionRing (ofField K S hS) K :=

Mathlib/RingTheory/Localization/FractionRing.lean

@@ -250,6 +250,7 @@ theorem mk'_mk_eq_div {r s} (hs : s ∈ nonZeroDivisors A) :
 theorem mk'_eq_div {r} (s : nonZeroDivisors A) : mk' K r s = algebraMap A K r / algebraMap A K s :=
   mk'_mk_eq_div s.2
 
+variable (A) in
 theorem div_surjective (z : K) :
     ∃ x y : A, y ∈ nonZeroDivisors A ∧ algebraMap _ _ x / algebraMap _ _ y = z :=
   let ⟨x, ⟨y, hy⟩, h⟩ := exists_mk'_eq (nonZeroDivisors A) z
@@ -286,7 +287,7 @@ omit [IsDomain B]
 
 theorem algHom_commutes (e : K₁ →ₐ[A] K₂) (f : L₁ →ₐ[B] L₂) (x : K₁) :
     algebraMap K₂ L₂ (e x) = f (algebraMap K₁ L₁ x) := by
-  obtain ⟨r, s, hs, rfl⟩ := IsFractionRing.div_surjective (A := A) x
+  obtain ⟨r, s, hs, rfl⟩ := IsFractionRing.div_surjective A x
   simp_rw [map_div₀, AlgHom.commutes, ← IsScalarTower.algebraMap_apply,
     IsScalarTower.algebraMap_apply A B L₁, AlgHom.commutes, ← IsScalarTower.algebraMap_apply]
 
@@ -303,7 +304,7 @@ variable (A K) in
 the image of `algebraMap A K` is equal to the whole field `K`. -/
 theorem closure_range_algebraMap : Subfield.closure (Set.range (algebraMap A K)) = ⊤ :=
   top_unique fun z _ ↦ by
-    obtain ⟨_, _, -, rfl⟩ := div_surjective (A := A) z
+    obtain ⟨_, _, -, rfl⟩ := div_surjective A z
     apply div_mem <;> exact Subfield.subset_closure ⟨_, rfl⟩
 
 variable {L : Type*} [Field L] {g : A →+* L} {f : K →+* L}
@@ -343,7 +344,7 @@ theorem lift_unique (hg : Function.Injective g) {f : K →+* L}
 theorem ringHom_ext {f1 f2 : K →+* L}
     (hf : ∀ x : A, f1 (algebraMap A K x) = f2 (algebraMap A K x)) : f1 = f2 := by
   ext z
-  obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective (A := A) z
+  obtain ⟨x, y, hy, rfl⟩ := IsFractionRing.div_surjective A z
   rw [map_div₀, map_div₀, hf, hf]
 
 theorem injective_comp_algebraMap :
@@ -474,7 +475,7 @@ variable {A B C D : Type*}
 noncomputable def fieldEquivOfAlgEquiv (f : B ≃ₐ[A] C) : FB ≃ₐ[FA] FC where
   __ := IsFractionRing.ringEquivOfRingEquiv f.toRingEquiv
   commutes' x := by
-    obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective (A := A) x
+    obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective A x
     simp_rw [map_div₀, ← IsScalarTower.algebraMap_apply, IsScalarTower.algebraMap_apply A B FB]
     simp [← IsScalarTower.algebraMap_apply A C FC]
 
@@ -494,14 +495,14 @@ variable (A B) in
 lemma fieldEquivOfAlgEquiv_refl :
     fieldEquivOfAlgEquiv FA FB FB (AlgEquiv.refl : B ≃ₐ[A] B) = AlgEquiv.refl := by
   ext x
-  obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective (A := B) x
+  obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective B x
   simp
 
 lemma fieldEquivOfAlgEquiv_trans (f : B ≃ₐ[A] C) (g : C ≃ₐ[A] D) :
     fieldEquivOfAlgEquiv FA FB FD (f.trans g) =
       (fieldEquivOfAlgEquiv FA FB FC f).trans (fieldEquivOfAlgEquiv FA FC FD g) := by
   ext x
-  obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective (A := B) x
+  obtain ⟨x, y, -, rfl⟩ := IsFractionRing.div_surjective B x
   simp
 
 end fieldEquivOfAlgEquiv

Mathlib/RingTheory/Localization/Integral.lean

@@ -491,7 +491,7 @@ theorem isAlgebraic_iff' [Field K] [IsDomain R] [Algebra R K] [Algebra S K]
     letI := FractionRing.liftAlgebra R K
     have := FractionRing.isScalarTower_liftAlgebra R K
     rw [IsFractionRing.isAlgebraic_iff R (FractionRing R) K, isAlgebraic_iff_isIntegral]
-    obtain ⟨a : S, b, ha, rfl⟩ := div_surjective (A := S) x
+    obtain ⟨a : S, b, ha, rfl⟩ := div_surjective S x
     obtain ⟨f, hf₁, hf₂⟩ := h b
     rw [div_eq_mul_inv]
     refine .mul ?_ (.inv ?_) <;> exact isAlgebraic_iff_isIntegral.mp <|

Mathlib/RingTheory/Valuation/Discrete/Basic.lean

@@ -466,7 +466,7 @@ open scoped WithZero
 theorem exists_lift_of_le_one {x : K} (H : ((maximalIdeal A).valuation K) x ≤ (1 : ℤᵐ⁰)) :
     ∃ a : A, algebraMap A K a = x := by
   obtain ⟨π, hπ⟩ := exists_irreducible A
-  obtain ⟨a, b, hb, h_frac⟩ := IsFractionRing.div_surjective (A := A) x
+  obtain ⟨a, b, hb, h_frac⟩ := IsFractionRing.div_surjective A x
   by_cases ha : a = 0
   · rw [← h_frac]
     use 0