diff --git a/Mathlib/Algebra/Field/Basic.lean b/Mathlib/Algebra/Field/Basic.lean index 0287961cb7a7d..19af168e9ced1 100644 --- a/Mathlib/Algebra/Field/Basic.lean +++ b/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 diff --git a/Mathlib/Algebra/Field/Defs.lean b/Mathlib/Algebra/Field/Defs.lean index 31e8d3d372f9b..4e0b3cf067b19 100644 --- a/Mathlib/Algebra/Field/Defs.lean +++ b/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' diff --git a/Mathlib/Data/Rat/Basic.lean b/Mathlib/Data/Rat/Basic.lean index 631a510ed6737..18a2a0c477060 100644 --- a/Mathlib/Data/Rat/Basic.lean +++ b/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 := (· * ·) } diff --git a/Mathlib/Data/Rat/Cast.lean b/Mathlib/Data/Rat/Cast.lean index 75ef138561c9f..1379c8c442931 100644 --- a/Mathlib/Data/Rat/Cast.lean +++ b/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] diff --git a/Mathlib/LinearAlgebra/TensorProduct.lean b/Mathlib/LinearAlgebra/TensorProduct.lean index 67f910828c8d6..e4b1f3bd4f331 100644 --- a/Mathlib/LinearAlgebra/TensorProduct.lean +++ b/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 diff --git a/Mathlib/Tactic/IrreducibleDef.lean b/Mathlib/Tactic/IrreducibleDef.lean index 119d9e70c880a..e95e5b36d6656 100644 --- a/Mathlib/Tactic/IrreducibleDef.lean +++ b/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) diff --git a/lake-manifest.json b/lake-manifest.json index 9700f467ec68c..af7698835e095 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -16,6 +16,6 @@ {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "ac39f359c64f54e833e358cf0a6b3ca9f00aa490", + "rev": "44a92d84c31a88b9af9329a441890ad449d8cd5f", "name": "std", "inputRev?": "main"}}]} diff --git a/lean-toolchain b/lean-toolchain index 2526786a65af2..7f0fd437b945f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-03-07 +leanprover/lean4:nightly-2023-03-09