feat(NNRat): More basic lemmas (#15047)

From LeanAPAP

Author: YaelDillies

Mathlib/Algebra/Algebra/Rat.lean

@@ -3,18 +3,19 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
-import Mathlib.Data.Rat.Cast.CharZero
 import Mathlib.Algebra.Algebra.Defs
+import Mathlib.Algebra.GroupWithZero.Action.Basic
+import Mathlib.Data.Rat.Cast.CharZero
 
 /-!
 # Further basic results about `Algebra`'s over `ℚ`.
 
 This file could usefully be split further.
 -/
 
-namespace RingHom
+variable {F R S : Type*}
 
-variable {R S : Type*}
+namespace RingHom
 
 -- Porting note: changed `[Ring R] [Ring S]` to `[Semiring R] [Semiring S]`
 -- otherwise, Lean failed to find a `Subsingleton (ℚ →+* S)` instance
@@ -25,26 +26,89 @@ theorem map_rat_algebraMap [Semiring R] [Semiring S] [Algebra ℚ R] [Algebra 
 
 end RingHom
 
-section Rat
+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]
+
+instance _root_.DivisionSemiring.toNNRatAlgebra : Algebra ℚ≥0 R where
+  smul_def' := smul_def
+  toRingHom := castHom _
+  commutes' := cast_commute
+
+instance _root_.RingHomClass.toLinearMapClassNNRat [FunLike F R S] [RingHomClass F R S] :
+    LinearMapClass F ℚ≥0 R S where
+  map_smulₛₗ f q a := by simp [smul_def, cast_id]
+
+variable [SMul R S]
+
+instance instSMulCommClass [SMulCommClass R S S] : SMulCommClass ℚ≥0 R S where
+  smul_comm q a b := by simp [smul_def, mul_smul_comm]
+
+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
+/-- `nnqsmul` 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]
+
+instance _root_.DivisionRing.toRatAlgebra : Algebra ℚ R where
+  smul_def' := smul_def
+  toRingHom := castHom _
+  commutes' := cast_commute
+
+instance _root_.RingHomClass.toLinearMapClassRat [FunLike F R S] [RingHomClass F R S] :
+    LinearMapClass F ℚ R S where
+  map_smulₛₗ f q a := by simp [smul_def, cast_id]
+
+variable [SMul R S]
 
-/-- Every division ring of characteristic zero is an algebra over the rationals. -/
-instance DivisionRing.toRatAlgebra {α} [DivisionRing α] [CharZero α] : Algebra ℚ α where
-  smul := (· • ·)
-  smul_def' := Rat.smul_def
-  toRingHom := Rat.castHom α
-  commutes' := Rat.cast_commute
+instance instSMulCommClass [SMulCommClass R S S] : SMulCommClass ℚ R S where
+  smul_comm q a b := by simp [smul_def, mul_smul_comm]
 
-/-- The rational numbers are an algebra over the non-negative rationals. -/
-instance : Algebra NNRat ℚ :=
-  NNRat.coeHom.toAlgebra
+instance instSMulCommClass' [SMulCommClass S R S] : SMulCommClass R ℚ S :=
+  have := SMulCommClass.symm S R S; SMulCommClass.symm _ _ _
 
-/-- The two `Algebra ℚ ℚ` instances should coincide. -/
-example : DivisionRing.toRatAlgebra = Algebra.id ℚ :=
-  rfl
+end DivisionRing
 
-@[simp] theorem algebraMap_rat_rat : algebraMap ℚ ℚ = RingHom.id ℚ := rfl
+@[deprecated Algebra.id.map_eq_id (since := "2024-07-30")]
+lemma _root_.algebraMap_rat_rat : algebraMap ℚ ℚ = RingHom.id ℚ := rfl
 
-instance algebra_rat_subsingleton {α} [Semiring α] : Subsingleton (Algebra ℚ α) :=
+instance algebra_rat_subsingleton {R} [Semiring R] : Subsingleton (Algebra ℚ R) :=
   ⟨fun x y => Algebra.algebra_ext x y <| RingHom.congr_fun <| Subsingleton.elim _ _⟩
 
 end Rat

Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

@@ -6,6 +6,7 @@ Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne
 import Mathlib.Analysis.SpecialFunctions.Exp
 import Mathlib.Data.Nat.Factorization.Defs
 import Mathlib.Analysis.NormedSpace.Real
+import Mathlib.Data.Rat.Cast.CharZero
 
 /-!
 # Real logarithm

Mathlib/Data/NNRat/Defs.lean

@@ -30,6 +30,17 @@ Whenever you state a lemma about the coercion `ℚ≥0 → ℚ`, check that Lean
 `Subtype.val`. Else your lemma will never apply.
 -/
 
+library_note "specialised high priority simp lemma" /--
+It sometimes happens that a `@[simp]` lemma declared early in the library can be proved by `simp`
+using later, more general simp lemmas. In that case, the following reasons might be arguments for
+the early lemma to be tagged `@[simp high]` (rather than `@[simp, nolint simpNF]` or
+un``@[simp]``ed):
+1. There is a significant portion of the library which needs the early lemma to be available via
+  `simp` and which doesn't have access to the more general lemmas.
+2. The more general lemmas have more complicated typeclass assumptions, causing rewrites with them
+  to be slower.
+-/
+
 open Function
 
 deriving instance CanonicallyOrderedCommSemiring for NNRat
@@ -56,7 +67,8 @@ theorem ext : (p : ℚ) = (q : ℚ) → p = q :=
 protected theorem coe_injective : Injective ((↑) : ℚ≥0 → ℚ) :=
   Subtype.coe_injective
 
-@[simp, norm_cast]
+-- See note [specialised high priority simp lemma]
+@[simp high, norm_cast]
 theorem coe_inj : (p : ℚ) = q ↔ p = q :=
   Subtype.coe_inj
 
@@ -109,7 +121,8 @@ theorem coe_mul (p q : ℚ≥0) : ((p * q : ℚ≥0) : ℚ) = p * q :=
 theorem coe_sub (h : q ≤ p) : ((p - q : ℚ≥0) : ℚ) = p - q :=
   max_eq_left <| le_sub_comm.2 <| by rwa [sub_zero]
 
-@[simp]
+-- See note [specialised high priority simp lemma]
+@[simp high]
 theorem coe_eq_zero : (q : ℚ) = 0 ↔ q = 0 := by norm_cast
 
 theorem coe_ne_zero : (q : ℚ) ≠ 0 ↔ q ≠ 0 :=

Mathlib/Data/Rat/Cast/CharZero.lean

@@ -10,21 +10,15 @@ import Mathlib.Data.Rat.Cast.Defs
 # Casts of rational numbers into characteristic zero fields (or division rings).
 -/
 
+open Function
 
 variable {F ι α β : Type*}
 
 namespace Rat
+variable [DivisionRing α] [CharZero α] {p q : ℚ}
 
-open Rat
-
-section WithDivRing
-
-variable [DivisionRing α]
-
-@[simp, norm_cast]
-theorem cast_inj [CharZero α] : ∀ {m n : ℚ}, (m : α) = n ↔ m = n
-  | ⟨n₁, d₁, d₁0, c₁⟩, ⟨n₂, d₂, d₂0, c₂⟩ => by
-    refine ⟨fun h => ?_, congr_arg _⟩
+lemma cast_injective : Injective ((↑) : ℚ → α)
+  | ⟨n₁, d₁, d₁0, c₁⟩, ⟨n₂, d₂, d₂0, c₂⟩, h => by
     have d₁a : (d₁ : α) ≠ 0 := Nat.cast_ne_zero.2 d₁0
     have d₂a : (d₂ : α) ≠ 0 := Nat.cast_ne_zero.2 d₂0
     rw [mk'_eq_divInt, mk'_eq_divInt] at h ⊢
@@ -34,30 +28,21 @@ theorem cast_inj [CharZero α] : ∀ {m n : ℚ}, (m : α) = n ↔ m = n
       Int.cast_mul, ← Int.cast_natCast d₂, ← Int.cast_mul, Int.cast_inj, ← mkRat_eq_iff d₁0 d₂0]
       at h
 
-theorem cast_injective [CharZero α] : Function.Injective ((↑) : ℚ → α)
-  | _, _ => cast_inj.1
+@[simp, norm_cast] lemma cast_inj : (p : α) = q ↔ p = q := cast_injective.eq_iff
 
-@[simp]
-theorem cast_eq_zero [CharZero α] {n : ℚ} : (n : α) = 0 ↔ n = 0 := by rw [← cast_zero, cast_inj]
-
-theorem cast_ne_zero [CharZero α] {n : ℚ} : (n : α) ≠ 0 ↔ n ≠ 0 :=
-  not_congr cast_eq_zero
-
-@[simp, norm_cast]
-theorem cast_add [CharZero α] (m n) : ((m + n : ℚ) : α) = m + n :=
-  cast_add_of_ne_zero (Nat.cast_ne_zero.2 <| ne_of_gt m.pos) (Nat.cast_ne_zero.2 <| ne_of_gt n.pos)
+@[simp, norm_cast] lemma cast_eq_zero : (p : α) = 0 ↔ p = 0 := cast_injective.eq_iff' cast_zero
+lemma cast_ne_zero : (p : α) ≠ 0 ↔ p ≠ 0 := cast_eq_zero.ne
 
-@[simp, norm_cast]
-theorem cast_sub [CharZero α] (m n) : ((m - n : ℚ) : α) = m - n :=
-  cast_sub_of_ne_zero (Nat.cast_ne_zero.2 <| ne_of_gt m.pos) (Nat.cast_ne_zero.2 <| ne_of_gt n.pos)
+@[simp, norm_cast] lemma cast_add (p q : ℚ) : ↑(p + q) = (p + q : α) :=
+  cast_add_of_ne_zero (Nat.cast_ne_zero.2 p.pos.ne') (Nat.cast_ne_zero.2 q.pos.ne')
 
-@[simp, norm_cast]
-theorem cast_mul [CharZero α] (m n) : ((m * n : ℚ) : α) = m * n :=
-  cast_mul_of_ne_zero (Nat.cast_ne_zero.2 <| ne_of_gt m.pos) (Nat.cast_ne_zero.2 <| ne_of_gt n.pos)
+@[simp, norm_cast] lemma cast_sub (p q : ℚ) : ↑(p - q) = (p - q : α) :=
+  cast_sub_of_ne_zero (Nat.cast_ne_zero.2 p.pos.ne') (Nat.cast_ne_zero.2 q.pos.ne')
 
-variable (α)
-variable [CharZero α]
+@[simp, norm_cast] lemma cast_mul (p q : ℚ) : ↑(p * q) = (p * q : α) :=
+  cast_mul_of_ne_zero (Nat.cast_ne_zero.2 p.pos.ne') (Nat.cast_ne_zero.2 q.pos.ne')
 
+variable (α) in
 /-- Coercion `ℚ → α` as a `RingHom`. -/
 def castHom : ℚ →+* α where
   toFun := (↑)
@@ -66,32 +51,67 @@ def castHom : ℚ →+* α where
   map_zero' := cast_zero
   map_add' := cast_add
 
-variable {α}
-
-@[simp]
-theorem coe_cast_hom : ⇑(castHom α) = ((↑) : ℚ → α) :=
-  rfl
+@[simp] lemma coe_castHom : ⇑(castHom α) = ((↑) : ℚ → α) := rfl
 
-@[simp, norm_cast]
-theorem cast_inv (n) : ((n⁻¹ : ℚ) : α) = (n : α)⁻¹ :=
-  map_inv₀ (castHom α) _
+@[deprecated (since := "2024-07-22")] alias coe_cast_hom := coe_castHom
 
-@[simp, norm_cast]
-theorem cast_div (m n) : ((m / n : ℚ) : α) = m / n :=
-  map_div₀ (castHom α) _ _
+@[simp, norm_cast] lemma cast_inv (p : ℚ) : ↑(p⁻¹) = (p⁻¹ : α) := map_inv₀ (castHom α) _
+@[simp, norm_cast] lemma cast_div (p q : ℚ) : ↑(p / q) = (p / q : α) := map_div₀ (castHom α) ..
 
 @[simp, norm_cast]
-theorem cast_zpow (q : ℚ) (n : ℤ) : ((q ^ n : ℚ) : α) = (q : α) ^ n :=
-  map_zpow₀ (castHom α) q n
+lemma cast_zpow (p : ℚ) (n : ℤ) : ↑(p ^ n) = (p ^ n : α) := map_zpow₀ (castHom α) ..
 
 @[norm_cast]
 theorem cast_mk (a b : ℤ) : (a /. b : α) = a / b := by
   simp only [divInt_eq_div, cast_div, cast_intCast]
 
+end Rat
+
+namespace NNRat
+variable [DivisionSemiring α] [CharZero α] {p q : ℚ≥0}
+
+lemma cast_injective : Injective ((↑) : ℚ≥0 → α) := by
+  rintro p q hpq
+  rw [NNRat.cast_def, NNRat.cast_def, Commute.div_eq_div_iff] at hpq
+  rw [← p.num_div_den, ← q.num_div_den, div_eq_div_iff]
+  norm_cast at hpq ⊢
+  any_goals norm_cast
+  any_goals apply den_ne_zero
+  exact Nat.cast_commute ..
+
+@[simp, norm_cast] lemma cast_inj : (p : α) = q ↔ p = q := cast_injective.eq_iff
+
+@[simp, norm_cast] lemma cast_eq_zero : (q : α) = 0 ↔ q = 0 := by rw [← cast_zero, cast_inj]
+lemma cast_ne_zero : (q : α) ≠ 0 ↔ q ≠ 0 := cast_eq_zero.not
+
+@[simp, norm_cast] lemma cast_add (p q : ℚ≥0) : ↑(p + q) = (p + q : α) :=
+  cast_add_of_ne_zero (Nat.cast_ne_zero.2 p.den_pos.ne') (Nat.cast_ne_zero.2 q.den_pos.ne')
+
+@[simp, norm_cast] lemma cast_mul (p q) : (p * q : ℚ≥0) = (p * q : α) :=
+  cast_mul_of_ne_zero (Nat.cast_ne_zero.2 p.den_pos.ne') (Nat.cast_ne_zero.2 q.den_pos.ne')
+
+variable (α) in
+/-- Coercion `ℚ≥0 → α` as a `RingHom`. -/
+def castHom : ℚ≥0 →+* α where
+  toFun := (↑)
+  map_one' := cast_one
+  map_mul' := cast_mul
+  map_zero' := cast_zero
+  map_add' := cast_add
+
+@[simp, norm_cast] lemma coe_castHom : ⇑(castHom α) = (↑) := rfl
+
+@[simp, norm_cast] lemma cast_inv (p) : (p⁻¹ : ℚ≥0) = (p : α)⁻¹ := map_inv₀ (castHom α) _
+@[simp, norm_cast] lemma cast_div (p q) : (p / q : ℚ≥0) = (p / q : α) := map_div₀ (castHom α) ..
+
 @[simp, norm_cast]
-theorem cast_pow (q : ℚ) (k : ℕ) : ↑(q ^ k) = (q : α) ^ k :=
-  (castHom α).map_pow q k
+lemma cast_zpow (q : ℚ≥0) (p : ℤ) : ↑(q ^ p) = ((q : α) ^ p : α) := map_zpow₀ (castHom α) ..
 
-end WithDivRing
+@[simp]
+lemma cast_divNat (a b : ℕ) : (divNat a b : α) = a / b := by
+  rw [← cast_natCast, ← cast_natCast b, ← cast_div]
+  congr
+  ext
+  apply Rat.mkRat_eq_div
 
-end Rat
+end NNRat