[Merged by Bors] - chore: bump to nightly-2023-03-09

Mathlib/Algebra/Field/Basic.lean

@@ -289,7 +289,7 @@ protected def Function.Injective.divisionRing [DivisionRing K] {K'} [Zero K'] [O
     DivisionRing K' :=
   { hf.groupWithZero f zero one mul inv div npow zpow,
     hf.ring f zero one add mul neg sub nsmul zsmul npow nat_cast int_cast with
-    ratCast := RatCast.ratCast,
+    ratCast := Rat.cast,
     ratCast_mk := fun a b h1 h2 ↦
       hf
         (by
@@ -327,7 +327,7 @@ protected def Function.Injective.field [Field K] {K'} [Zero K'] [Mul K'] [Add K'
     Field K' :=
   { hf.commGroupWithZero f zero one mul inv div npow zpow,
     hf.commRing f zero one add mul neg sub nsmul zsmul npow nat_cast int_cast with
-    ratCast := RatCast.ratCast,
+    ratCast := Rat.cast,
     ratCast_mk := fun a b h1 h2 ↦
       hf
         (by

Mathlib/Algebra/Field/Defs.lean

@@ -66,15 +66,6 @@ def Rat.castRec [NatCast K] [IntCast K] [Mul K] [Inv K] : ℚ → K
   | ⟨a, b, _, _⟩ => ↑a * (↑b)⁻¹
 #align rat.cast_rec Rat.castRec
 
-/-- Type class for the canonical homomorphism `ℚ → K`.
--/
-class RatCast (K : Type u) where
-  /-- The canonical homomorphism `ℚ → K`. -/
-  protected ratCast : ℚ → K
-#align has_rat_cast RatCast
-
-attribute [coe] RatCast.ratCast
-
 /-- The default definition of the scalar multiplication `(a : ℚ) • (x : K)` for a division ring `K`
 is given by `a • x = (↑ a) * x`.
 Use `(a : ℚ) • (x : K)` instead of `qsmulRec` for better definitional behaviour.
@@ -104,14 +95,14 @@ class DivisionRing (K : Type u) extends Ring K, DivInvMonoid K, Nontrivial K, Ra
   protected inv_zero : (0 : K)⁻¹ = 0
   protected ratCast := Rat.castRec
   /-- However `ratCast` is defined, propositionally it must be equal to `a * b⁻¹`. -/
-  protected ratCast_mk : ∀ (a : ℤ) (b : ℕ) (h1 h2), ratCast ⟨a, b, h1, h2⟩ = a * (b : K)⁻¹ := by
+  protected ratCast_mk : ∀ (a : ℤ) (b : ℕ) (h1 h2), Rat.cast ⟨a, b, h1, h2⟩ = a * (b : K)⁻¹ := by
     intros
     rfl
   /-- Multiplication by a rational number. -/
-  protected qsmul : ℚ → K → K := qsmulRec ratCast
+  protected qsmul : ℚ → K → K := qsmulRec Rat.cast
   /-- However `qsmul` is defined,
   propositionally it must be equal to multiplication by `ratCast`. -/
-  protected qsmul_eq_mul' : ∀ (a : ℚ) (x : K), qsmul a x = ratCast a * x := by
+  protected qsmul_eq_mul' : ∀ (a : ℚ) (x : K), qsmul a x = Rat.cast a * x := by
     intros
     rfl
 #align division_ring DivisionRing
@@ -145,15 +136,6 @@ variable [DivisionRing K] {a b : K}
 
 namespace Rat
 
--- see Note [coercion into rings]
-/-- Construct the canonical injection from `ℚ` into an arbitrary
-  division ring. If the field has positive characteristic `p`,
-  we define `1 / p = 1 / 0 = 0` for consistency with our
-  division by zero convention. -/
-instance (priority := 900) castCoe {K : Type _} [RatCast K] : CoeTC ℚ K :=
-  ⟨RatCast.ratCast⟩
-#align rat.cast_coe Rat.castCoe
-
 theorem cast_mk' (a b h1 h2) : ((⟨a, b, h1, h2⟩ : ℚ) : K) = a * (b : K)⁻¹ :=
   DivisionRing.ratCast_mk _ _ _ _
 #align rat.cast_mk' Rat.cast_mk'

Mathlib/Data/Rat/Basic.lean

@@ -46,7 +46,7 @@ instance field : Field ℚ :=
     one := 1
     mul := (· * ·)
     inv := Inv.inv
-    ratCast := id
+    ratCast := Rat.cast
     ratCast_mk := fun a b h1 h2 => (num_div_den _).symm
     qsmul := (· * ·) }
 

Mathlib/Data/Rat/Cast.lean

@@ -425,7 +425,7 @@ end LinearOrderedField
 
 -- Porting note: statement made more explicit
 @[norm_cast]
-theorem cast_id (n : ℚ) : (RatCast.ratCast n ) = n := by rfl
+theorem cast_id (n : ℚ) : Rat.cast n = n := rfl
 #align rat.cast_id Rat.cast_id
 
 @[simp]

Mathlib/LinearAlgebra/TensorProduct.lean

@@ -629,9 +629,7 @@ protected def lid : R ⊗[R] M ≃ₗ[R] M :=
 end
 
 @[simp]
-theorem lid_tmul (m : M) (r : R) : (TensorProduct.lid R M : R ⊗ M → M) (r ⊗ₜ m) = r • m := by
-  dsimp [TensorProduct.lid]
-  simp
+theorem lid_tmul (m : M) (r : R) : (TensorProduct.lid R M : R ⊗ M → M) (r ⊗ₜ m) = r • m :=
   rfl
 #align tensor_product.lid_tmul TensorProduct.lid_tmul
 
@@ -676,9 +674,7 @@ protected def rid : M ⊗[R] R ≃ₗ[R] M :=
 end
 
 @[simp]
-theorem rid_tmul (m : M) (r : R) : (TensorProduct.rid R M) (m ⊗ₜ r) = r • m := by
-  dsimp [TensorProduct.rid, TensorProduct.comm, TensorProduct.lid]
-  simp
+theorem rid_tmul (m : M) (r : R) : (TensorProduct.rid R M) (m ⊗ₜ r) = r • m :=
   rfl
 #align tensor_product.rid_tmul TensorProduct.rid_tmul
 

Mathlib/Tactic/IrreducibleDef.lean

@@ -82,6 +82,7 @@ macro mods:declModifiers "irreducible_def" n_id:declId declSig:optDeclSig val:de
     { scopes with name := scopes.name.appendAfter "_def" }
   `(stop_at_first_error
     def definition$[.{$us,*}]? $declSig:optDeclSig $val
+    set_option genInjectivity false in -- generates awful simp lemmas
     structure Wrapper$[.{$us,*}]? where
       value : type_of% @definition.{$us',*}
       prop : Eq @value @(delta% @definition)

lake-manifest.json

@@ -16,6 +16,6 @@
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "ac39f359c64f54e833e358cf0a6b3ca9f00aa490",
+    "rev": "44a92d84c31a88b9af9329a441890ad449d8cd5f",
     "name": "std",
     "inputRev?": "main"}}]}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-03-07
+leanprover/lean4:nightly-2023-03-09