chore: remove MulAction ℚ α → MulAction ℚ≥0 α instances (leanprover-community#30671)

This fixes the instances diamond in the `NNRat` action.

Author: astrainfinita

Mathlib/Algebra/Algebra/Rat.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import Mathlib.Algebra.Algebra.Defs
-import Mathlib.Algebra.GroupWithZero.Action.Basic
 import Mathlib.Algebra.Module.Equiv.Defs
 import Mathlib.Data.Rat.Cast.CharZero
 
@@ -28,24 +27,7 @@ theorem map_rat_algebraMap [Semiring R] [Semiring S] [Algebra ℚ R] [Algebra 
 end RingHom
 
 namespace NNRat
-variable [DivisionSemiring R] [CharZero R]
-
-section Semiring
-variable [Semiring S] [Module ℚ≥0 S]
-
-variable (R) in
-/-- `nnqsmul` is equal to any other module structure via a cast. -/
-lemma cast_smul_eq_nnqsmul [Module R S] (q : ℚ≥0) (a : S) : (q : R) • a = q • a := by
-  refine MulAction.injective₀ (G₀ := ℚ≥0) (Nat.cast_ne_zero.2 q.den_pos.ne') ?_
-  dsimp
-  rw [← mul_smul, den_mul_eq_num, Nat.cast_smul_eq_nsmul, Nat.cast_smul_eq_nsmul, ← smul_assoc,
-    nsmul_eq_mul q.den, ← cast_natCast, ← cast_mul, den_mul_eq_num, cast_natCast,
-    Nat.cast_smul_eq_nsmul]
-
-end Semiring
-
-section DivisionSemiring
-variable [DivisionSemiring S] [CharZero S]
+variable [DivisionSemiring R] [CharZero R] [DivisionSemiring S] [CharZero S]
 
 instance _root_.DivisionSemiring.toNNRatAlgebra : Algebra ℚ≥0 R where
   smul_def' := smul_def
@@ -64,28 +46,10 @@ instance instSMulCommClass [SMulCommClass R S S] : SMulCommClass ℚ≥0 R S whe
 instance instSMulCommClass' [SMulCommClass S R S] : SMulCommClass R ℚ≥0 S :=
   have := SMulCommClass.symm S R S; SMulCommClass.symm _ _ _
 
-end DivisionSemiring
 end NNRat
 
 namespace Rat
-variable [DivisionRing R] [CharZero R]
-
-section Ring
-variable [Ring S] [Module ℚ S]
-
-variable (R) in
-/-- `qsmul` is equal to any other module structure via a cast. -/
-lemma cast_smul_eq_qsmul [Module R S] (q : ℚ) (a : S) : (q : R) • a = q • a := by
-  refine MulAction.injective₀ (G₀ := ℚ) (Nat.cast_ne_zero.2 q.den_pos.ne') ?_
-  dsimp
-  rw [← mul_smul, den_mul_eq_num, Nat.cast_smul_eq_nsmul, Int.cast_smul_eq_zsmul, ← smul_assoc,
-    nsmul_eq_mul q.den, ← cast_natCast, ← cast_mul, den_mul_eq_num, cast_intCast,
-    Int.cast_smul_eq_zsmul]
-
-end Ring
-
-section DivisionRing
-variable [DivisionRing S] [CharZero S]
+variable [DivisionRing R] [CharZero R] [DivisionRing S] [CharZero S]
 
 instance _root_.DivisionRing.toRatAlgebra : Algebra ℚ R where
   smul_def' := smul_def
@@ -108,8 +72,6 @@ instance instSMulCommClass [SMulCommClass R S S] : SMulCommClass ℚ R S where
 instance instSMulCommClass' [SMulCommClass S R S] : SMulCommClass R ℚ S :=
   have := SMulCommClass.symm S R S; SMulCommClass.symm _ _ _
 
-end DivisionRing
-
 instance algebra_rat_subsingleton {R} [Semiring R] : Subsingleton (Algebra ℚ R) :=
   ⟨fun x y => Algebra.algebra_ext x y <| RingHom.congr_fun <| Subsingleton.elim _ _⟩
 

Mathlib/Algebra/Module/Rat.lean

@@ -71,6 +71,18 @@ instance IsScalarTower.rat {R : Type u} {M : Type v} [Ring R] [AddCommGroup M] [
     [Module ℚ R] [Module ℚ M] : IsScalarTower ℚ R M where
   smul_assoc r x y := map_rat_smul ((smulAddHom R M).flip y) r x
 
+/-- `nnqsmul` is equal to any other module structure via a cast. -/
+lemma NNRat.cast_smul_eq_nnqsmul (R : Type*) [DivisionSemiring R]
+    [MulAction R M] [MulAction ℚ≥0 M] [IsScalarTower ℚ≥0 R M]
+    (q : ℚ≥0) (x : M) : (q : R) • x = q • x := by
+  rw [← one_smul R x, ← smul_assoc, ← smul_assoc]; simp
+
+/-- `qsmul` is equal to any other module structure via a cast. -/
+lemma Rat.cast_smul_eq_qsmul (R : Type*) [DivisionRing R]
+    [MulAction R M] [MulAction ℚ M] [IsScalarTower ℚ R M]
+    (q : ℚ) (x : M) : (q : R) • x = q • x := by
+  rw [← one_smul R x, ← smul_assoc, ← smul_assoc]; simp
+
 section
 variable {α : Type u} {M : Type v}
 

Mathlib/Algebra/Order/Module/Rat.lean

@@ -3,8 +3,8 @@ Copyright (c) 2024 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import Mathlib.Algebra.Module.Rat
 import Mathlib.Algebra.Order.Module.Basic
-import Mathlib.Data.NNRat.Lemmas
 import Mathlib.Data.Rat.Cast.Order
 
 /-!
@@ -13,13 +13,19 @@ import Mathlib.Data.Rat.Cast.Order
 
 variable {α : Type*}
 
-instance PosSMulMono.nnrat_of_rat [Preorder α] [MulAction ℚ α] [PosSMulMono ℚ α] :
+instance PosSMulMono.nnrat_of_rat [Preorder α] [MulAction ℚ α] [MulAction ℚ≥0 α]
+    [IsScalarTower ℚ≥0 ℚ α] [PosSMulMono ℚ α] :
     PosSMulMono ℚ≥0 α where
-  smul_le_smul_of_nonneg_left _q hq _a₁ _a₂ ha := smul_le_smul_of_nonneg_left (α := ℚ) ha hq
+  smul_le_smul_of_nonneg_left _q hq _a₁ _a₂ ha := by
+    rw [← NNRat.cast_smul_eq_nnqsmul ℚ, ← NNRat.cast_smul_eq_nnqsmul ℚ]
+    exact smul_le_smul_of_nonneg_left (α := ℚ) ha hq
 
-instance PosSMulStrictMono.nnrat_of_rat [Preorder α] [MulAction ℚ α] [PosSMulStrictMono ℚ α] :
+instance PosSMulStrictMono.nnrat_of_rat [Preorder α] [MulAction ℚ≥0 α] [MulAction ℚ α]
+    [IsScalarTower ℚ≥0 ℚ α] [PosSMulStrictMono ℚ α] :
     PosSMulStrictMono ℚ≥0 α where
-  smul_lt_smul_of_pos_left _q hq _a₁ _a₂ ha := smul_lt_smul_of_pos_left (α := ℚ) ha hq
+  smul_lt_smul_of_pos_left _q hq _a₁ _a₂ ha := by
+    rw [← NNRat.cast_smul_eq_nnqsmul ℚ, ← NNRat.cast_smul_eq_nnqsmul ℚ]
+    exact smul_lt_smul_of_pos_left (α := ℚ) ha hq
 
 section LinearOrderedAddCommGroup
 variable [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α]

Mathlib/Data/NNRat/Lemmas.lean

@@ -5,7 +5,6 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Algebra.Field.Rat
 import Mathlib.Algebra.Group.Indicator
-import Mathlib.Algebra.GroupWithZero.Action.End
 import Mathlib.Algebra.Order.Field.Rat
 import Mathlib.Data.Rat.Lemmas
 import Mathlib.Tactic.Zify
@@ -23,14 +22,6 @@ open scoped NNRat
 namespace NNRat
 variable {α : Type*} {q : ℚ≥0}
 
-/-- A `MulAction` over `ℚ` restricts to a `MulAction` over `ℚ≥0`. -/
-instance [MulAction ℚ α] : MulAction ℚ≥0 α :=
-  MulAction.compHom α coeHom.toMonoidHom
-
-/-- A `DistribMulAction` over `ℚ` restricts to a `DistribMulAction` over `ℚ≥0`. -/
-instance [AddCommMonoid α] [DistribMulAction ℚ α] : DistribMulAction ℚ≥0 α :=
-  DistribMulAction.compHom α coeHom.toMonoidHom
-
 @[simp, norm_cast]
 lemma coe_indicator (s : Set α) (f : α → ℚ≥0) (a : α) :
     ((s.indicator f a : ℚ≥0) : ℚ) = s.indicator (fun x ↦ ↑(f x)) a :=