diff --git a/Archive/Imo/Imo2019Q4.lean b/Archive/Imo/Imo2019Q4.lean index 6672eed44cca7..b981091f29136 100644 --- a/Archive/Imo/Imo2019Q4.lean +++ b/Archive/Imo/Imo2019Q4.lean @@ -40,7 +40,7 @@ theorem upper_bound {k n : ℕ} (hk : k > 0) have h2 : ∑ i in range n, i < k := by suffices multiplicity 2 (k ! : ℤ) = ↑(∑ i in range n, i : ℕ) by rw [← PartENat.coe_lt_coe, ← this]; change multiplicity ((2 : ℕ) : ℤ) _ < _ - simp_rw [Int.coe_nat_multiplicity, multiplicity_two_factorial_lt hk.lt.ne.symm] + simp_rw [Int.natCast_multiplicity, multiplicity_two_factorial_lt hk.lt.ne.symm] rw [h, multiplicity.Finset.prod Int.prime_two, Nat.cast_sum] apply sum_congr rfl; intro i hi rw [multiplicity_sub_of_gt, multiplicity_pow_self_of_prime Int.prime_two] diff --git a/Archive/Wiedijk100Theorems/BallotProblem.lean b/Archive/Wiedijk100Theorems/BallotProblem.lean index 55e966b1c3b83..46c4eb20ffc67 100644 --- a/Archive/Wiedijk100Theorems/BallotProblem.lean +++ b/Archive/Wiedijk100Theorems/BallotProblem.lean @@ -403,13 +403,13 @@ theorem ballot_problem : rw [ballot_problem' q p qp] rw [ENNReal.toReal_div, ← Nat.cast_add, ← Nat.cast_add, ENNReal.toReal_nat, ENNReal.toReal_sub_of_le, ENNReal.toReal_nat, ENNReal.toReal_nat] - exacts [Nat.cast_le.2 qp.le, ENNReal.nat_ne_top _] + exacts [Nat.cast_le.2 qp.le, ENNReal.natCast_ne_top _] rwa [ENNReal.toReal_eq_toReal (measure_lt_top _ _).ne] at this · simp only [Ne, ENNReal.div_eq_top, tsub_eq_zero_iff_le, Nat.cast_le, not_le, - add_eq_zero_iff, Nat.cast_eq_zero, ENNReal.add_eq_top, ENNReal.nat_ne_top, or_self_iff, + add_eq_zero_iff, Nat.cast_eq_zero, ENNReal.add_eq_top, ENNReal.natCast_ne_top, or_self_iff, not_false_iff, and_true_iff] push_neg - exact ⟨fun _ _ => by linarith, (lt_of_le_of_lt tsub_le_self (ENNReal.nat_ne_top p).lt_top).ne⟩ + exact ⟨fun _ _ => by linarith, (tsub_le_self.trans_lt (ENNReal.natCast_ne_top p).lt_top).ne⟩ #align ballot.ballot_problem Ballot.ballot_problem end Ballot diff --git a/Counterexamples/SorgenfreyLine.lean b/Counterexamples/SorgenfreyLine.lean index 37121c6161c00..92ddffb42da4f 100644 --- a/Counterexamples/SorgenfreyLine.lean +++ b/Counterexamples/SorgenfreyLine.lean @@ -217,16 +217,16 @@ instance : T5Space ℝₗ := by _ ≤ x := (not_lt.1 fun hxy => (hYd y hy).le_bot ⟨⟨hle, hxy⟩, subset_closure hx⟩) _ ≤ max x y := le_max_left _ _ -theorem denseRange_coe_rat : DenseRange ((↑) : ℚ → ℝₗ) := by +theorem denseRange_ratCast : DenseRange ((↑) : ℚ → ℝₗ) := by refine' dense_iff_inter_open.2 _ rintro U Uo ⟨x, hx⟩ rcases isOpen_iff.1 Uo _ hx with ⟨y, hxy, hU⟩ rcases exists_rat_btwn hxy with ⟨z, hxz, hzy⟩ exact ⟨z, hU ⟨hxz.le, hzy⟩, mem_range_self _⟩ -#align counterexample.sorgenfrey_line.dense_range_coe_rat Counterexample.SorgenfreyLine.denseRange_coe_rat +#align counterexample.sorgenfrey_line.dense_range_coe_rat Counterexample.SorgenfreyLine.denseRange_ratCast instance : SeparableSpace ℝₗ := - ⟨⟨_, countable_range _, denseRange_coe_rat⟩⟩ + ⟨⟨_, countable_range _, denseRange_ratCast⟩⟩ theorem isClosed_antidiagonal (c : ℝₗ) : IsClosed {x : ℝₗ × ℝₗ | x.1 + x.2 = c} := isClosed_singleton.preimage continuous_add diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean index f390081d3ec26..5b5178e375b39 100644 --- a/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean +++ b/Mathlib/Algebra/Algebra/Subalgebra/Basic.lean @@ -151,9 +151,9 @@ protected theorem nsmul_mem {x : A} (hx : x ∈ S) (n : ℕ) : n • x ∈ S := nsmul_mem hx n #align subalgebra.nsmul_mem Subalgebra.nsmul_mem -protected theorem coe_nat_mem (n : ℕ) : (n : A) ∈ S := - coe_nat_mem S n -#align subalgebra.coe_nat_mem Subalgebra.coe_nat_mem +protected theorem natCast_mem (n : ℕ) : (n : A) ∈ S := + natCast_mem S n +#align subalgebra.coe_nat_mem Subalgebra.natCast_mem protected theorem list_prod_mem {L : List A} (h : ∀ x ∈ L, x ∈ S) : L.prod ∈ S := list_prod_mem h @@ -202,10 +202,14 @@ protected theorem zsmul_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Alg zsmul_mem hx n #align subalgebra.zsmul_mem Subalgebra.zsmul_mem -protected theorem coe_int_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] +protected theorem intCast_mem {R : Type u} {A : Type v} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R A) (n : ℤ) : (n : A) ∈ S := - coe_int_mem S n -#align subalgebra.coe_int_mem Subalgebra.coe_int_mem + intCast_mem S n +#align subalgebra.coe_int_mem Subalgebra.intCast_mem + +-- 2024-04-05 +@[deprecated natCast_mem] alias coe_nat_mem := Subalgebra.natCast_mem +@[deprecated intCast_mem] alias coe_int_mem := Subalgebra.intCast_mem /-- The projection from a subalgebra of `A` to an additive submonoid of `A`. -/ def toAddSubmonoid {R : Type u} {A : Type v} [CommSemiring R] [Semiring A] [Algebra R A] @@ -1431,7 +1435,7 @@ variable {R : Type*} [Semiring R] /-- A subsemiring is an `ℕ`-subalgebra. -/ def subalgebraOfSubsemiring (S : Subsemiring R) : Subalgebra ℕ R := - { S with algebraMap_mem' := fun i => coe_nat_mem S i } + { S with algebraMap_mem' := fun i => natCast_mem S i } #align subalgebra_of_subsemiring subalgebraOfSubsemiring @[simp] diff --git a/Mathlib/Algebra/CharZero/Lemmas.lean b/Mathlib/Algebra/CharZero/Lemmas.lean index f6fc80f4dc1f5..02193c0b3130b 100644 --- a/Mathlib/Algebra/CharZero/Lemmas.lean +++ b/Mathlib/Algebra/CharZero/Lemmas.lean @@ -189,7 +189,7 @@ namespace WithTop instance {R : Type*} [AddMonoidWithOne R] [CharZero R] : CharZero (WithTop R) where cast_injective m n h := by - rwa [← coe_nat, ← coe_nat n, coe_eq_coe, Nat.cast_inj] at h + rwa [← coe_natCast, ← coe_natCast n, coe_eq_coe, Nat.cast_inj] at h end WithTop @@ -198,7 +198,7 @@ namespace WithBot instance {R : Type*} [AddMonoidWithOne R] [CharZero R] : CharZero (WithBot R) where cast_injective m n h := by - rwa [← coe_nat, ← coe_nat n, coe_eq_coe, Nat.cast_inj] at h + rwa [← coe_natCast, ← coe_natCast n, coe_eq_coe, Nat.cast_inj] at h end WithBot diff --git a/Mathlib/Algebra/Module/CharacterModule.lean b/Mathlib/Algebra/Module/CharacterModule.lean index 42e0c798e313e..ff082ed5d2d40 100644 --- a/Mathlib/Algebra/Module/CharacterModule.lean +++ b/Mathlib/Algebra/Module/CharacterModule.lean @@ -186,7 +186,7 @@ lemma eq_zero_of_ofSpanSingleton_apply_self (a : A) AddCircle.coe_eq_zero_iff] at h rcases h with ⟨n, hn⟩ apply_fun Rat.den at hn - rw [zsmul_one, Rat.coe_int_den, Rat.inv_coe_nat_den_of_pos] at hn + rw [zsmul_one, Rat.coe_int_den, Rat.inv_natCast_den_of_pos] at hn · split_ifs at hn · cases hn · rwa [eq_comm, AddMonoid.addOrderOf_eq_one_iff] at hn diff --git a/Mathlib/Algebra/Module/Torsion.lean b/Mathlib/Algebra/Module/Torsion.lean index 67127aae98449..5c76113f8218c 100644 --- a/Mathlib/Algebra/Module/Torsion.lean +++ b/Mathlib/Algebra/Module/Torsion.lean @@ -865,7 +865,7 @@ theorem isTorsion_iff_isTorsion_int [AddCommGroup M] : refine' ⟨fun h x => _, fun h x => _⟩ · obtain ⟨n, h0, hn⟩ := (h x).exists_nsmul_eq_zero exact - ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt <| Int.coe_nat_pos.mpr h0⟩, + ⟨⟨n, mem_nonZeroDivisors_of_ne_zero <| ne_of_gt <| Int.natCast_pos.mpr h0⟩, (natCast_zsmul _ _).trans hn⟩ · rw [isOfFinAddOrder_iff_nsmul_eq_zero] obtain ⟨n, hn⟩ := @h x diff --git a/Mathlib/Algebra/Order/Module/OrderedSMul.lean b/Mathlib/Algebra/Order/Module/OrderedSMul.lean index 7db3f0f4e7da1..de1b37233ddcb 100644 --- a/Mathlib/Algebra/Order/Module/OrderedSMul.lean +++ b/Mathlib/Algebra/Order/Module/OrderedSMul.lean @@ -92,7 +92,7 @@ instance Nat.orderedSMul [LinearOrderedCancelAddCommMonoid M] : OrderedSMul ℕ instance Int.orderedSMul [LinearOrderedAddCommGroup M] : OrderedSMul ℤ M := OrderedSMul.mk'' fun n hn => by cases n - · simp only [Int.ofNat_eq_coe, Int.coe_nat_pos, natCast_zsmul] at hn ⊢ + · simp only [Int.ofNat_eq_coe, Int.natCast_pos, natCast_zsmul] at hn ⊢ exact strictMono_smul_left_of_pos hn · cases (Int.negSucc_not_pos _).1 hn #align int.ordered_smul Int.orderedSMul diff --git a/Mathlib/Algebra/Order/Monoid/WithTop.lean b/Mathlib/Algebra/Order/Monoid/WithTop.lean index 73a87dea118d4..c3eef054b327b 100644 --- a/Mathlib/Algebra/Order/Monoid/WithTop.lean +++ b/Mathlib/Algebra/Order/Monoid/WithTop.lean @@ -373,14 +373,19 @@ instance addMonoidWithOne : AddMonoidWithOne (WithTop α) := simp only -- Porting note: Had to add this...? rw [Nat.cast_add_one, WithTop.coe_add, WithTop.coe_one] } -@[simp, norm_cast] lemma coe_nat (n : ℕ) : ((n : α) : WithTop α) = n := rfl -#align with_top.coe_nat WithTop.coe_nat +@[simp, norm_cast] lemma coe_natCast (n : ℕ) : ((n : α) : WithTop α) = n := rfl +#align with_top.coe_nat WithTop.coe_natCast -@[simp] lemma nat_ne_top (n : ℕ) : (n : WithTop α) ≠ ⊤ := coe_ne_top -#align with_top.nat_ne_top WithTop.nat_ne_top +@[simp] lemma natCast_ne_top (n : ℕ) : (n : WithTop α) ≠ ⊤ := coe_ne_top +#align with_top.nat_ne_top WithTop.natCast_ne_top -@[simp] lemma top_ne_nat (n : ℕ) : (⊤ : WithTop α) ≠ n := top_ne_coe -#align with_top.top_ne_nat WithTop.top_ne_nat +@[simp] lemma top_ne_natCast (n : ℕ) : (⊤ : WithTop α) ≠ n := top_ne_coe +#align with_top.top_ne_nat WithTop.top_ne_natCast + +-- 2024-04-05 +@[deprecated] alias coe_nat := coe_natCast +@[deprecated] alias nat_ne_top := natCast_ne_top +@[deprecated] alias top_ne_nat := top_ne_natCast end AddMonoidWithOne @@ -569,14 +574,19 @@ variable [AddMonoidWithOne α] instance addMonoidWithOne : AddMonoidWithOne (WithBot α) := WithTop.addMonoidWithOne -@[norm_cast] lemma coe_nat (n : ℕ) : ((n : α) : WithBot α) = n := rfl -#align with_bot.coe_nat WithBot.coe_nat +@[norm_cast] lemma coe_natCast (n : ℕ) : ((n : α) : WithBot α) = n := rfl +#align with_bot.coe_nat WithBot.coe_natCast + +@[simp] lemma natCast_ne_bot (n : ℕ) : (n : WithBot α) ≠ ⊥ := coe_ne_bot +#align with_bot.nat_ne_bot WithBot.natCast_ne_bot -@[simp] lemma nat_ne_bot (n : ℕ) : (n : WithBot α) ≠ ⊥ := coe_ne_bot -#align with_bot.nat_ne_bot WithBot.nat_ne_bot +@[simp] lemma bot_ne_natCast (n : ℕ) : (⊥ : WithBot α) ≠ n := bot_ne_coe +#align with_bot.bot_ne_nat WithBot.bot_ne_natCast -@[simp] lemma bot_ne_nat (n : ℕ) : (⊥ : WithBot α) ≠ n := bot_ne_coe -#align with_bot.bot_ne_nat WithBot.bot_ne_nat +-- 2024-04-05 +@[deprecated] alias coe_nat := coe_natCast +@[deprecated] alias nat_ne_bot := natCast_ne_bot +@[deprecated] alias bot_ne_nat := bot_ne_natCast end AddMonoidWithOne diff --git a/Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean b/Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean index 80a85f478b4db..133868e83bc1d 100644 --- a/Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean +++ b/Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean @@ -42,7 +42,7 @@ open Polynomial noncomputable def cardPowDegree : AbsoluteValue Fq[X] ℤ := have card_pos : 0 < Fintype.card Fq := Fintype.card_pos_iff.mpr inferInstance have pow_pos : ∀ n, 0 < (Fintype.card Fq : ℤ) ^ n := fun n => - pow_pos (Int.coe_nat_pos.mpr card_pos) n + pow_pos (Int.natCast_pos.mpr card_pos) n letI := Classical.decEq Fq; { toFun := fun p => if p = 0 then 0 else (Fintype.card Fq : ℤ) ^ p.natDegree nonneg' := fun p => by @@ -95,7 +95,7 @@ theorem cardPowDegree_nonzero (p : Fq[X]) (hp : p ≠ 0) : theorem cardPowDegree_isEuclidean : IsEuclidean (cardPowDegree : AbsoluteValue Fq[X] ℤ) := have card_pos : 0 < Fintype.card Fq := Fintype.card_pos_iff.mpr inferInstance have pow_pos : ∀ n, 0 < (Fintype.card Fq : ℤ) ^ n := fun n => - pow_pos (Int.coe_nat_pos.mpr card_pos) n + pow_pos (Int.natCast_pos.mpr card_pos) n { map_lt_map_iff' := fun {p q} => by classical show cardPowDegree p < cardPowDegree q ↔ degree p < degree q diff --git a/Mathlib/Algebra/Squarefree/Basic.lean b/Mathlib/Algebra/Squarefree/Basic.lean index d1636dde2cd5a..49b4ffbcc7afb 100644 --- a/Mathlib/Algebra/Squarefree/Basic.lean +++ b/Mathlib/Algebra/Squarefree/Basic.lean @@ -315,8 +315,11 @@ theorem squarefree_natAbs {n : ℤ} : Squarefree n.natAbs ↔ Squarefree n := by #align int.squarefree_nat_abs Int.squarefree_natAbs @[simp] -theorem squarefree_coe_nat {n : ℕ} : Squarefree (n : ℤ) ↔ Squarefree n := by +theorem squarefree_natCast {n : ℕ} : Squarefree (n : ℤ) ↔ Squarefree n := by rw [← squarefree_natAbs, natAbs_ofNat] -#align int.squarefree_coe_nat Int.squarefree_coe_nat +#align int.squarefree_coe_nat Int.squarefree_natCast + +-- 2024-04-05 +@[deprecated] alias squarefree_coe_nat := squarefree_natCast end Int diff --git a/Mathlib/Analysis/Analytic/Constructions.lean b/Mathlib/Analysis/Analytic/Constructions.lean index 1263bf2f3be9b..d32a080a46a30 100644 --- a/Mathlib/Analysis/Analytic/Constructions.lean +++ b/Mathlib/Analysis/Analytic/Constructions.lean @@ -228,7 +228,7 @@ lemma formalMultilinearSeries_geometric_radius (𝕜) [NontriviallyNormedField Real.norm_of_nonneg (NNReal.coe_nonneg _), ← NNReal.coe_one, NNReal.coe_lt_coe] · refine le_of_forall_nnreal_lt (fun r hr ↦ ?_) - rw [← Nat.cast_one, ENNReal.coe_lt_coe_nat, Nat.cast_one] at hr + rw [← Nat.cast_one, ENNReal.coe_lt_natCast, Nat.cast_one] at hr apply FormalMultilinearSeries.le_radius_of_isBigO simp_rw [formalMultilinearSeries_geometric_apply_norm, one_mul] refine isBigO_of_le atTop (fun n ↦ ?_) diff --git a/Mathlib/Analysis/Analytic/Meromorphic.lean b/Mathlib/Analysis/Analytic/Meromorphic.lean index c9a7989e2e9e7..26b3b2934f637 100644 --- a/Mathlib/Analysis/Analytic/Meromorphic.lean +++ b/Mathlib/Analysis/Analytic/Meromorphic.lean @@ -150,7 +150,7 @@ lemma order_eq_top_iff {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) : hf.order = ⊤ ↔ ∀ᶠ z in 𝓝[≠] x, f z = 0 := by unfold order by_cases h : hf.choose_spec.order = ⊤ - · rw [h, WithTop.map_top, ← WithTop.coe_nat, + · rw [h, WithTop.map_top, ← WithTop.coe_natCast, WithTop.top_sub_coe, eq_self, true_iff, eventually_nhdsWithin_iff] rw [AnalyticAt.order_eq_top_iff] at h filter_upwards [h] with z hf hz @@ -170,7 +170,7 @@ lemma order_eq_int_iff {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (n : ∃ g : 𝕜 → E, AnalyticAt 𝕜 g x ∧ g x ≠ 0 ∧ ∀ᶠ z in 𝓝[≠] x, f z = (z - x) ^ n • g z := by unfold order by_cases h : hf.choose_spec.order = ⊤ - · rw [h, WithTop.map_top, ← WithTop.coe_nat, WithTop.top_sub_coe, + · rw [h, WithTop.map_top, ← WithTop.coe_natCast, WithTop.top_sub_coe, eq_false_intro WithTop.top_ne_coe, false_iff] rw [AnalyticAt.order_eq_top_iff] at h refine fun ⟨g, hg_an, hg_ne, hg_eq⟩ ↦ hg_ne ?_ @@ -182,7 +182,7 @@ lemma order_eq_int_iff {f : 𝕜 → E} {x : 𝕜} (hf : MeromorphicAt f x) (n : rwa [hfz_eq hz, ← mul_smul, smul_eq_zero_iff_right] at hfz exact mul_ne_zero (pow_ne_zero _ (sub_ne_zero.mpr hz)) (zpow_ne_zero _ (sub_ne_zero.mpr hz)) · obtain ⟨m, h⟩ := WithTop.ne_top_iff_exists.mp h - rw [← h, WithTop.map_coe, ← WithTop.coe_nat, ← WithTop.coe_sub, WithTop.coe_inj] + rw [← h, WithTop.map_coe, ← WithTop.coe_natCast, ← WithTop.coe_sub, WithTop.coe_inj] obtain ⟨g, hg_an, hg_ne, hg_eq⟩ := (AnalyticAt.order_eq_nat_iff _ _).mp h.symm replace hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] x, f z = (z - x) ^ (↑m - ↑hf.choose : ℤ) • g z := by rw [eventually_nhdsWithin_iff] diff --git a/Mathlib/Analysis/BoxIntegral/Integrability.lean b/Mathlib/Analysis/BoxIntegral/Integrability.lean index d1e2078afece0..6b4e6eea4351f 100644 --- a/Mathlib/Analysis/BoxIntegral/Integrability.lean +++ b/Mathlib/Analysis/BoxIntegral/Integrability.lean @@ -152,7 +152,7 @@ theorem HasIntegral.of_aeEq_zero {l : IntegrationParams} {I : Box ι} {f : (ι clear_value m lift m to ℝ≥0 using ne_top_of_lt this rw [ENNReal.coe_toReal, ← NNReal.coe_nat_cast, ← NNReal.coe_mul, NNReal.coe_le_coe, ← - ENNReal.coe_le_coe, ENNReal.coe_mul, ENNReal.coe_nat, mul_comm] + ENNReal.coe_le_coe, ENNReal.coe_mul, ENNReal.coe_natCast, mul_comm] exact (mul_le_mul_left' this.le _).trans ENNReal.mul_div_le #align box_integral.has_integral_zero_of_ae_eq_zero BoxIntegral.HasIntegral.of_aeEq_zero diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean index 9c1dd448f15fc..06383f860354c 100644 --- a/Mathlib/Analysis/Normed/Group/Basic.lean +++ b/Mathlib/Analysis/Normed/Group/Basic.lean @@ -1854,14 +1854,18 @@ theorem le_norm_self (r : ℝ) : r ≤ ‖r‖ := #align real.le_norm_self Real.le_norm_self -- Porting note (#10618): `simp` can prove this -theorem norm_coe_nat (n : ℕ) : ‖(n : ℝ)‖ = n := +theorem norm_natCast (n : ℕ) : ‖(n : ℝ)‖ = n := abs_of_nonneg n.cast_nonneg -#align real.norm_coe_nat Real.norm_coe_nat +#align real.norm_coe_nat Real.norm_natCast @[simp] -theorem nnnorm_coe_nat (n : ℕ) : ‖(n : ℝ)‖₊ = n := - NNReal.eq <| norm_coe_nat _ -#align real.nnnorm_coe_nat Real.nnnorm_coe_nat +theorem nnnorm_natCast (n : ℕ) : ‖(n : ℝ)‖₊ = n := + NNReal.eq <| norm_natCast _ +#align real.nnnorm_coe_nat Real.nnnorm_natCast + +-- 2024-04-05 +@[deprecated] alias norm_coe_nat := norm_natCast +@[deprecated] alias nnnorm_coe_nat := nnnorm_natCast -- Porting note (#10618): `simp` can prove this theorem norm_two : ‖(2 : ℝ)‖ = 2 := @@ -1922,8 +1926,11 @@ theorem norm_eq_abs (n : ℤ) : ‖n‖ = |(n : ℝ)| := #align int.norm_eq_abs Int.norm_eq_abs @[simp] -theorem norm_coe_nat (n : ℕ) : ‖(n : ℤ)‖ = n := by simp [Int.norm_eq_abs] -#align int.norm_coe_nat Int.norm_coe_nat +theorem norm_natCast (n : ℕ) : ‖(n : ℤ)‖ = n := by simp [Int.norm_eq_abs] +#align int.norm_coe_nat Int.norm_natCast + +-- 2024-04-05 +@[deprecated] alias norm_coe_nat := norm_natCast theorem _root_.NNReal.natCast_natAbs (n : ℤ) : (n.natAbs : ℝ≥0) = ‖n‖₊ := NNReal.eq <| diff --git a/Mathlib/Analysis/NormedSpace/Int.lean b/Mathlib/Analysis/NormedSpace/Int.lean index 8ffb8695855b5..71d31b453cb6e 100644 --- a/Mathlib/Analysis/NormedSpace/Int.lean +++ b/Mathlib/Analysis/NormedSpace/Int.lean @@ -31,9 +31,12 @@ theorem norm_coe_units (e : ℤˣ) : ‖(e : ℤ)‖ = 1 := by #align int.norm_coe_units Int.norm_coe_units @[simp] -theorem nnnorm_coe_nat (n : ℕ) : ‖(n : ℤ)‖₊ = n := - Real.nnnorm_coe_nat _ -#align int.nnnorm_coe_nat Int.nnnorm_coe_nat +theorem nnnorm_natCast (n : ℕ) : ‖(n : ℤ)‖₊ = n := + Real.nnnorm_natCast _ +#align int.nnnorm_coe_nat Int.nnnorm_natCast + +-- 2024-04-05 +@[deprecated] alias nnnorm_coe_nat := nnnorm_natCast @[simp] theorem toNat_add_toNat_neg_eq_nnnorm (n : ℤ) : ↑n.toNat + ↑(-n).toNat = ‖n‖₊ := by diff --git a/Mathlib/Analysis/NormedSpace/MatrixExponential.lean b/Mathlib/Analysis/NormedSpace/MatrixExponential.lean index dc17275dd33a7..ff3d3b3aba87a 100644 --- a/Mathlib/Analysis/NormedSpace/MatrixExponential.lean +++ b/Mathlib/Analysis/NormedSpace/MatrixExponential.lean @@ -189,9 +189,9 @@ theorem exp_neg (A : Matrix m m 𝔸) : exp 𝕂 (-A) = (exp 𝕂 A)⁻¹ := by theorem exp_zsmul (z : ℤ) (A : Matrix m m 𝔸) : exp 𝕂 (z • A) = exp 𝕂 A ^ z := by obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg - · rw [zpow_coe_nat, natCast_zsmul, exp_nsmul] + · rw [zpow_natCast, natCast_zsmul, exp_nsmul] · have : IsUnit (exp 𝕂 A).det := (Matrix.isUnit_iff_isUnit_det _).mp (isUnit_exp _ _) - rw [Matrix.zpow_neg this, zpow_coe_nat, neg_smul, exp_neg, natCast_zsmul, exp_nsmul] + rw [Matrix.zpow_neg this, zpow_natCast, neg_smul, exp_neg, natCast_zsmul, exp_nsmul] #align matrix.exp_zsmul Matrix.exp_zsmul theorem exp_conj (U : Matrix m m 𝔸) (A : Matrix m m 𝔸) (hy : IsUnit U) : diff --git a/Mathlib/Analysis/NormedSpace/PiLp.lean b/Mathlib/Analysis/NormedSpace/PiLp.lean index 6f36c72319558..0d4a1e295cafa 100644 --- a/Mathlib/Analysis/NormedSpace/PiLp.lean +++ b/Mathlib/Analysis/NormedSpace/PiLp.lean @@ -434,7 +434,7 @@ theorem antilipschitzWith_equiv_aux : simp only [nsmul_eq_mul, Finset.card_univ, ENNReal.rpow_one, Finset.sum_const, ENNReal.mul_rpow_of_nonneg _ _ nonneg, ← ENNReal.rpow_mul, cancel] have : (Fintype.card ι : ℝ≥0∞) = (Fintype.card ι : ℝ≥0) := - (ENNReal.coe_nat (Fintype.card ι)).symm + (ENNReal.coe_natCast (Fintype.card ι)).symm rw [this, ENNReal.coe_rpow_of_nonneg _ nonneg] #align pi_Lp.antilipschitz_with_equiv_aux PiLp.antilipschitzWith_equiv_aux @@ -609,7 +609,7 @@ end Linfty theorem norm_eq_of_nat {p : ℝ≥0∞} [Fact (1 ≤ p)] {β : ι → Type*} [∀ i, SeminormedAddCommGroup (β i)] (n : ℕ) (h : p = n) (f : PiLp p β) : ‖f‖ = (∑ i, ‖f i‖ ^ n) ^ (1 / (n : ℝ)) := by - have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.nat_ne_top n) + have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.natCast_ne_top n) simp only [one_div, h, Real.rpow_nat_cast, ENNReal.toReal_nat, eq_self_iff_true, Finset.sum_congr, norm_eq_sum this] #align pi_Lp.norm_eq_of_nat PiLp.norm_eq_of_nat diff --git a/Mathlib/Analysis/NormedSpace/ProdLp.lean b/Mathlib/Analysis/NormedSpace/ProdLp.lean index 8d06f03896e43..2662ba5f5a363 100644 --- a/Mathlib/Analysis/NormedSpace/ProdLp.lean +++ b/Mathlib/Analysis/NormedSpace/ProdLp.lean @@ -608,7 +608,7 @@ variable {p α β} theorem prod_norm_eq_of_nat [Norm α] [Norm β] (n : ℕ) (h : p = n) (f : WithLp p (α × β)) : ‖f‖ = (‖f.fst‖ ^ n + ‖f.snd‖ ^ n) ^ (1 / (n : ℝ)) := by - have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.nat_ne_top n) + have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.natCast_ne_top n) simp only [one_div, h, Real.rpow_nat_cast, ENNReal.toReal_nat, eq_self_iff_true, Finset.sum_congr, prod_norm_eq_add this] diff --git a/Mathlib/Analysis/NormedSpace/lpSpace.lean b/Mathlib/Analysis/NormedSpace/lpSpace.lean index 9b33c49bf7072..942db1988abe3 100644 --- a/Mathlib/Analysis/NormedSpace/lpSpace.lean +++ b/Mathlib/Analysis/NormedSpace/lpSpace.lean @@ -890,7 +890,7 @@ theorem _root_.nat_cast_memℓp_infty (n : ℕ) : Memℓp (n : ∀ i, B i) ∞ : #align nat_cast_mem_ℓp_infty nat_cast_memℓp_infty theorem _root_.int_cast_memℓp_infty (z : ℤ) : Memℓp (z : ∀ i, B i) ∞ := - coe_int_mem (lpInftySubring B) z + intCast_mem (lpInftySubring B) z #align int_cast_mem_ℓp_infty int_cast_memℓp_infty @[simp] diff --git a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean index 81549363ed376..1d9b0dc0ac350 100644 --- a/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean +++ b/Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean @@ -379,7 +379,7 @@ theorem GammaSeq_tendsto_Gamma (s : ℂ) : Tendsto (GammaSeq s) atTop (𝓝 <| G conv at this => arg 1; intro n; rw [mul_comm] rwa [← mul_one (GammaAux m (s + 1) / s), tendsto_mul_iff_of_ne_zero _ (one_ne_zero' ℂ)] at this simp_rw [add_assoc] - exact tendsto_coe_nat_div_add_atTop (1 + s) + exact tendsto_natCast_div_add_atTop (1 + s) #align complex.Gamma_seq_tendsto_Gamma Complex.GammaSeq_tendsto_Gamma end Complex @@ -436,7 +436,7 @@ theorem Gamma_mul_Gamma_one_sub (z : ℂ) : Gamma z * Gamma (1 - z) = π / sin ( have : ↑π / sin (↑π * z) = 1 * (π / sin (π * z)) := by rw [one_mul] convert Tendsto.congr' ((eventually_ne_atTop 0).mp (eventually_of_forall fun n hn => (GammaSeq_mul z hn).symm)) (Tendsto.mul _ _) - · convert tendsto_coe_nat_div_add_atTop (1 - z) using 1; ext1 n; rw [add_sub_assoc] + · convert tendsto_natCast_div_add_atTop (1 - z) using 1; ext1 n; rw [add_sub_assoc] · have : ↑π / sin (↑π * z) = 1 / (sin (π * z) / π) := by field_simp convert tendsto_const_nhds.div _ (div_ne_zero hs pi_ne) rw [← tendsto_mul_iff_of_ne_zero tendsto_const_nhds pi_ne, div_mul_cancel₀ _ pi_ne] diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean index 948aed8c826ab..4743f1ddaabc6 100644 --- a/Mathlib/Analysis/SpecificLimits/Basic.lean +++ b/Mathlib/Analysis/SpecificLimits/Basic.lean @@ -88,7 +88,7 @@ algebra over `ℝ`, e.g., `ℂ`). TODO: introduce a typeclass saying that `1 / n` tends to 0 at top, making it possible to get this statement simultaneously on `ℚ`, `ℝ` and `ℂ`. -/ -theorem tendsto_coe_nat_div_add_atTop {𝕜 : Type*} [DivisionRing 𝕜] [TopologicalSpace 𝕜] +theorem tendsto_natCast_div_add_atTop {𝕜 : Type*} [DivisionRing 𝕜] [TopologicalSpace 𝕜] [CharZero 𝕜] [Algebra ℝ 𝕜] [ContinuousSMul ℝ 𝕜] [TopologicalDivisionRing 𝕜] (x : 𝕜) : Tendsto (fun n : ℕ ↦ (n : 𝕜) / (n + x)) atTop (𝓝 1) := by refine' Tendsto.congr' ((eventually_ne_atTop 0).mp (eventually_of_forall fun n hn ↦ _)) _ @@ -105,7 +105,7 @@ theorem tendsto_coe_nat_div_add_atTop {𝕜 : Type*} [DivisionRing 𝕜] [Topolo refine' Iff.mpr tendsto_atTop' _ intros simp_all only [comp_apply, map_inv₀, map_natCast] -#align tendsto_coe_nat_div_add_at_top tendsto_coe_nat_div_add_atTop +#align tendsto_coe_nat_div_add_at_top tendsto_natCast_div_add_atTop /-! ### Powers -/ diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index 379a206bea98b..47003b2e25628 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/Mathlib/Analysis/SpecificLimits/Normed.lean @@ -61,7 +61,7 @@ theorem tendsto_norm_inverse_nhdsWithin_0_atTop {𝕜 : Type*} [NormedField 𝕜 theorem tendsto_norm_zpow_nhdsWithin_0_atTop {𝕜 : Type*} [NormedField 𝕜] {m : ℤ} (hm : m < 0) : Tendsto (fun x : 𝕜 ↦ ‖x ^ m‖) (𝓝[≠] 0) atTop := by rcases neg_surjective m with ⟨m, rfl⟩ - rw [neg_lt_zero] at hm; lift m to ℕ using hm.le; rw [Int.coe_nat_pos] at hm + rw [neg_lt_zero] at hm; lift m to ℕ using hm.le; rw [Int.natCast_pos] at hm simp only [norm_pow, zpow_neg, zpow_natCast, ← inv_pow] exact (tendsto_pow_atTop hm.ne').comp NormedField.tendsto_norm_inverse_nhdsWithin_0_atTop #align normed_field.tendsto_norm_zpow_nhds_within_0_at_top NormedField.tendsto_norm_zpow_nhdsWithin_0_atTop @@ -783,7 +783,7 @@ theorem Real.summable_pow_div_factorial (x : ℝ) : Summable (fun n ↦ x ^ n / calc ‖x ^ (n + 1) / (n + 1)!‖ = ‖x‖ / (n + 1) * ‖x ^ n / (n !)‖ := by rw [_root_.pow_succ', Nat.factorial_succ, Nat.cast_mul, ← _root_.div_mul_div_comm, norm_mul, - norm_div, Real.norm_coe_nat, Nat.cast_succ] + norm_div, Real.norm_natCast, Nat.cast_succ] _ ≤ ‖x‖ / (⌊‖x‖⌋₊ + 1) * ‖x ^ n / (n !)‖ := -- Porting note: this was `by mono* with 0 ≤ ‖x ^ n / (n !)‖, 0 ≤ ‖x‖ <;> apply norm_nonneg` -- but we can't wait on `mono`. diff --git a/Mathlib/Combinatorics/Additive/SalemSpencer.lean b/Mathlib/Combinatorics/Additive/SalemSpencer.lean index 9411ce55b7f64..7a762fd0f5ad2 100644 --- a/Mathlib/Combinatorics/Additive/SalemSpencer.lean +++ b/Mathlib/Combinatorics/Additive/SalemSpencer.lean @@ -511,7 +511,7 @@ open Asymptotics Filter theorem rothNumberNat_isBigOWith_id : IsBigOWith 1 atTop (fun N => (rothNumberNat N : ℝ)) fun N => (N : ℝ) := - isBigOWith_of_le _ <| by simpa only [Real.norm_coe_nat, Nat.cast_le] using rothNumberNat_le + isBigOWith_of_le _ <| by simpa only [Real.norm_natCast, Nat.cast_le] using rothNumberNat_le set_option linter.uppercaseLean3 false in #align roth_number_nat_is_O_with_id rothNumberNat_isBigOWith_id diff --git a/Mathlib/Data/DFinsupp/Interval.lean b/Mathlib/Data/DFinsupp/Interval.lean index 7e2cb1ff2f62e..4d8255283bb73 100644 --- a/Mathlib/Data/DFinsupp/Interval.lean +++ b/Mathlib/Data/DFinsupp/Interval.lean @@ -151,7 +151,7 @@ theorem mem_pi {f : Π₀ i, Finset (α i)} {g : Π₀ i, α i} : g ∈ f.pi ↔ @[simp] theorem card_pi (f : Π₀ i, Finset (α i)) : f.pi.card = f.prod fun i => (f i).card := by rw [pi, card_dfinsupp] - exact Finset.prod_congr rfl fun i _ => by simp only [Pi.nat_apply, Nat.cast_id] + exact Finset.prod_congr rfl fun i _ => by simp only [Pi.natCast_apply, Nat.cast_id] #align dfinsupp.card_pi DFinsupp.card_pi end Pi diff --git a/Mathlib/Data/ENNReal/Basic.lean b/Mathlib/Data/ENNReal/Basic.lean index 556f000e760cc..fdcdcb4acd987 100644 --- a/Mathlib/Data/ENNReal/Basic.lean +++ b/Mathlib/Data/ENNReal/Basic.lean @@ -558,34 +558,34 @@ theorem one_lt_coe_iff : 1 < (↑p : ℝ≥0∞) ↔ 1 < p := coe_lt_coe #align ennreal.one_lt_coe_iff ENNReal.one_lt_coe_iff @[simp, norm_cast] -theorem coe_nat (n : ℕ) : ((n : ℝ≥0) : ℝ≥0∞) = n := rfl -#align ennreal.coe_nat ENNReal.coe_nat +theorem coe_natCast (n : ℕ) : ((n : ℝ≥0) : ℝ≥0∞) = n := rfl +#align ennreal.coe_nat ENNReal.coe_natCast -@[simp, norm_cast] lemma ofReal_coe_nat (n : ℕ) : ENNReal.ofReal n = n := by simp [ENNReal.ofReal] -#align ennreal.of_real_coe_nat ENNReal.ofReal_coe_nat +@[simp, norm_cast] lemma ofReal_natCast (n : ℕ) : ENNReal.ofReal n = n := by simp [ENNReal.ofReal] +#align ennreal.of_real_coe_nat ENNReal.ofReal_natCast -- See note [no_index around OfNat.ofNat] @[simp] theorem ofReal_ofNat (n : ℕ) [n.AtLeastTwo] : ENNReal.ofReal (no_index (OfNat.ofNat n)) = OfNat.ofNat n := - ofReal_coe_nat n + ofReal_natCast n -@[simp] theorem nat_ne_top (n : ℕ) : (n : ℝ≥0∞) ≠ ∞ := WithTop.nat_ne_top n -#align ennreal.nat_ne_top ENNReal.nat_ne_top +@[simp] theorem natCast_ne_top (n : ℕ) : (n : ℝ≥0∞) ≠ ∞ := WithTop.natCast_ne_top n +#align ennreal.nat_ne_top ENNReal.natCast_ne_top -@[simp] theorem top_ne_nat (n : ℕ) : ∞ ≠ n := WithTop.top_ne_nat n -#align ennreal.top_ne_nat ENNReal.top_ne_nat +@[simp] theorem top_ne_natCast (n : ℕ) : ∞ ≠ n := WithTop.top_ne_natCast n +#align ennreal.top_ne_nat ENNReal.top_ne_natCast @[simp] theorem one_lt_top : 1 < ∞ := coe_lt_top #align ennreal.one_lt_top ENNReal.one_lt_top @[simp, norm_cast] theorem toNNReal_nat (n : ℕ) : (n : ℝ≥0∞).toNNReal = n := by - rw [← ENNReal.coe_nat n, ENNReal.toNNReal_coe] + rw [← ENNReal.coe_natCast n, ENNReal.toNNReal_coe] #align ennreal.to_nnreal_nat ENNReal.toNNReal_nat @[simp, norm_cast] theorem toReal_nat (n : ℕ) : (n : ℝ≥0∞).toReal = n := by - rw [← ENNReal.ofReal_coe_nat n, ENNReal.toReal_ofReal (Nat.cast_nonneg _)] + rw [← ENNReal.ofReal_natCast n, ENNReal.toReal_ofReal (Nat.cast_nonneg _)] #align ennreal.to_real_nat ENNReal.toReal_nat -- See note [no_index around OfNat.ofNat] @@ -667,18 +667,24 @@ theorem le_of_forall_pos_le_add (h : ∀ ε : ℝ≥0, 0 < ε → b < ∞ → a exact ⟨r, hr0, h.trans_le le_top, hr⟩ #align ennreal.le_of_forall_pos_le_add ENNReal.le_of_forall_pos_le_add -theorem coe_nat_lt_coe {n : ℕ} : (n : ℝ≥0∞) < r ↔ ↑n < r := - ENNReal.coe_nat n ▸ coe_lt_coe -#align ennreal.coe_nat_lt_coe ENNReal.coe_nat_lt_coe +theorem natCast_lt_coe {n : ℕ} : n < (r : ℝ≥0∞) ↔ n < r := ENNReal.coe_natCast n ▸ coe_lt_coe +#align ennreal.coe_nat_lt_coe ENNReal.natCast_lt_coe -theorem coe_lt_coe_nat {n : ℕ} : (r : ℝ≥0∞) < n ↔ r < n := - ENNReal.coe_nat n ▸ coe_lt_coe -#align ennreal.coe_lt_coe_nat ENNReal.coe_lt_coe_nat +theorem coe_lt_natCast {n : ℕ} : (r : ℝ≥0∞) < n ↔ r < n := ENNReal.coe_natCast n ▸ coe_lt_coe +#align ennreal.coe_lt_coe_nat ENNReal.coe_lt_natCast + +-- 2024-04-05 +@[deprecated] alias coe_nat := coe_natCast +@[deprecated] alias ofReal_coe_nat := ofReal_natCast +@[deprecated] alias nat_ne_top := natCast_ne_top +@[deprecated] alias top_ne_nat := top_ne_natCast +@[deprecated] alias coe_nat_lt_coe := natCast_lt_coe +@[deprecated] alias coe_lt_coe_nat := coe_lt_natCast protected theorem exists_nat_gt {r : ℝ≥0∞} (h : r ≠ ∞) : ∃ n : ℕ, r < n := by lift r to ℝ≥0 using h rcases exists_nat_gt r with ⟨n, hn⟩ - exact ⟨n, coe_lt_coe_nat.2 hn⟩ + exact ⟨n, coe_lt_natCast.2 hn⟩ #align ennreal.exists_nat_gt ENNReal.exists_nat_gt @[simp] @@ -690,7 +696,7 @@ theorem iUnion_Iio_coe_nat : ⋃ n : ℕ, Iio (n : ℝ≥0∞) = {∞}ᶜ := by @[simp] theorem iUnion_Iic_coe_nat : ⋃ n : ℕ, Iic (n : ℝ≥0∞) = {∞}ᶜ := - Subset.antisymm (iUnion_subset fun n _x hx => ne_top_of_le_ne_top (nat_ne_top n) hx) <| + Subset.antisymm (iUnion_subset fun n _x hx => ne_top_of_le_ne_top (natCast_ne_top n) hx) <| iUnion_Iio_coe_nat ▸ iUnion_mono fun _ => Iio_subset_Iic_self #align ennreal.Union_Iic_coe_nat ENNReal.iUnion_Iic_coe_nat diff --git a/Mathlib/Data/ENNReal/Operations.lean b/Mathlib/Data/ENNReal/Operations.lean index 01f59ef70b7d9..1de34a09de75c 100644 --- a/Mathlib/Data/ENNReal/Operations.lean +++ b/Mathlib/Data/ENNReal/Operations.lean @@ -380,7 +380,7 @@ theorem sub_ne_top (ha : a ≠ ∞) : a - b ≠ ∞ := mt sub_eq_top_iff.mp <| m @[simp, norm_cast] theorem nat_cast_sub (m n : ℕ) : ↑(m - n) = (m - n : ℝ≥0∞) := by - rw [← coe_nat, Nat.cast_tsub, coe_sub, coe_nat, coe_nat] + rw [← coe_natCast, Nat.cast_tsub, coe_sub, coe_natCast, coe_natCast] #align ennreal.nat_cast_sub ENNReal.nat_cast_sub protected theorem sub_eq_of_eq_add (hb : b ≠ ∞) : a = c + b → a - b = c := diff --git a/Mathlib/Data/ENNReal/Real.lean b/Mathlib/Data/ENNReal/Real.lean index bc9a0fdcda7f0..2ef13a9218a5f 100644 --- a/Mathlib/Data/ENNReal/Real.lean +++ b/Mathlib/Data/ENNReal/Real.lean @@ -351,7 +351,7 @@ theorem ofReal_pow {p : ℝ} (hp : 0 ≤ p) (n : ℕ) : ENNReal.ofReal (p ^ n) = #align ennreal.of_real_pow ENNReal.ofReal_pow theorem ofReal_nsmul {x : ℝ} {n : ℕ} : ENNReal.ofReal (n • x) = n • ENNReal.ofReal x := by - simp only [nsmul_eq_mul, ← ofReal_coe_nat n, ← ofReal_mul n.cast_nonneg] + simp only [nsmul_eq_mul, ← ofReal_natCast n, ← ofReal_mul n.cast_nonneg] #align ennreal.of_real_nsmul ENNReal.ofReal_nsmul theorem ofReal_inv_of_pos {x : ℝ} (hx : 0 < x) : ENNReal.ofReal x⁻¹ = (ENNReal.ofReal x)⁻¹ := by @@ -662,9 +662,12 @@ theorem sup_eq_zero {a b : ℝ≥0∞} : a ⊔ b = 0 ↔ a = 0 ∧ b = 0 := sup_eq_bot_iff #align ennreal.sup_eq_zero ENNReal.sup_eq_zero -theorem iSup_coe_nat : ⨆ n : ℕ, (n : ℝ≥0∞) = ∞ := +theorem iSup_natCast : ⨆ n : ℕ, (n : ℝ≥0∞) = ∞ := (iSup_eq_top _).2 fun _b hb => ENNReal.exists_nat_gt (lt_top_iff_ne_top.1 hb) -#align ennreal.supr_coe_nat ENNReal.iSup_coe_nat +#align ennreal.supr_coe_nat ENNReal.iSup_natCast + +-- 2024-04-05 +@[deprecated] alias iSup_coe_nat := iSup_natCast end iSup diff --git a/Mathlib/Data/Finset/Finsupp.lean b/Mathlib/Data/Finset/Finsupp.lean index 6c83a5fa4aa1b..59e83a6a37897 100644 --- a/Mathlib/Data/Finset/Finsupp.lean +++ b/Mathlib/Data/Finset/Finsupp.lean @@ -100,7 +100,7 @@ theorem mem_pi {f : ι →₀ Finset α} {g : ι →₀ α} : g ∈ f.pi ↔ ∀ @[simp] theorem card_pi (f : ι →₀ Finset α) : f.pi.card = f.prod fun i => (f i).card := by rw [pi, card_finsupp] - exact Finset.prod_congr rfl fun i _ => by simp only [Pi.nat_apply, Nat.cast_id] + exact Finset.prod_congr rfl fun i _ => by simp only [Pi.natCast_apply, Nat.cast_id] #align finsupp.card_pi Finsupp.card_pi end Finsupp diff --git a/Mathlib/Data/Int/Cast/Lemmas.lean b/Mathlib/Data/Int/Cast/Lemmas.lean index f04dc5f1f0030..d7712a9a951c3 100644 --- a/Mathlib/Data/Int/Cast/Lemmas.lean +++ b/Mathlib/Data/Int/Cast/Lemmas.lean @@ -38,20 +38,24 @@ def ofNatHom : ℕ →+* ℤ := -- Porting note: no need to be `@[simp]`, as `Nat.cast_pos` handles this. -- @[simp] -theorem coe_nat_pos {n : ℕ} : (0 : ℤ) < n ↔ 0 < n := +theorem natCast_pos {n : ℕ} : (0 : ℤ) < n ↔ 0 < n := Nat.cast_pos -#align int.coe_nat_pos Int.coe_nat_pos +#align int.coe_nat_pos Int.natCast_pos -theorem coe_nat_succ_pos (n : ℕ) : 0 < (n.succ : ℤ) := - Int.coe_nat_pos.2 (succ_pos n) -#align int.coe_nat_succ_pos Int.coe_nat_succ_pos +theorem natCast_succ_pos (n : ℕ) : 0 < (n.succ : ℤ) := + Int.natCast_pos.2 (succ_pos n) +#align int.coe_nat_succ_pos Int.natCast_succ_pos + +-- 2024-04-05 +@[deprecated] alias coe_nat_pos := natCast_pos +@[deprecated] alias coe_nat_succ_pos := natCast_succ_pos lemma toNat_lt' {a : ℤ} {b : ℕ} (hb : b ≠ 0) : a.toNat < b ↔ a < b := by - rw [← toNat_lt_toNat, toNat_natCast]; exact coe_nat_pos.2 hb.bot_lt + rw [← toNat_lt_toNat, toNat_natCast]; exact natCast_pos.2 hb.bot_lt #align int.to_nat_lt Int.toNat_lt' lemma natMod_lt {a : ℤ} {b : ℕ} (hb : b ≠ 0) : a.natMod b < b := - (toNat_lt' hb).2 <| emod_lt_of_pos _ <| coe_nat_pos.2 hb.bot_lt + (toNat_lt' hb).2 <| emod_lt_of_pos _ <| natCast_pos.2 hb.bot_lt #align int.nat_mod_lt Int.natMod_lt section cast @@ -517,14 +521,18 @@ variable {π : ι → Type*} [∀ i, IntCast (π i)] instance intCast : IntCast (∀ i, π i) := { intCast := fun n _ ↦ n } -theorem int_apply (n : ℤ) (i : ι) : (n : ∀ i, π i) i = n := +theorem intCast_apply (n : ℤ) (i : ι) : (n : ∀ i, π i) i = n := rfl -#align pi.int_apply Pi.int_apply +#align pi.int_apply Pi.intCast_apply @[simp] -theorem coe_int (n : ℤ) : (n : ∀ i, π i) = fun _ => ↑n := +theorem intCast_def (n : ℤ) : (n : ∀ i, π i) = fun _ => ↑n := rfl -#align pi.coe_int Pi.coe_int +#align pi.coe_int Pi.intCast_def + +-- 2024-04-05 +@[deprecated] alias int_apply := intCast_apply +@[deprecated] alias coe_int := intCast_def end Pi diff --git a/Mathlib/Data/NNRat/Defs.lean b/Mathlib/Data/NNRat/Defs.lean index 98cd99125cbc7..e986a33dc917d 100644 --- a/Mathlib/Data/NNRat/Defs.lean +++ b/Mathlib/Data/NNRat/Defs.lean @@ -201,9 +201,12 @@ theorem coe_natCast (n : ℕ) : (↑(↑n : ℚ≥0) : ℚ) = n := -- See note [no_index around OfNat.ofNat] @[simp] -theorem mk_coe_nat (n : ℕ) : @Eq ℚ≥0 (⟨(n : ℚ), n.cast_nonneg⟩ : ℚ≥0) n := +theorem mk_natCast (n : ℕ) : @Eq ℚ≥0 (⟨(n : ℚ), n.cast_nonneg⟩ : ℚ≥0) n := rfl -#align nnrat.mk_coe_nat NNRat.mk_coe_nat +#align nnrat.mk_coe_nat NNRat.mk_natCast + +-- 2024-04-05 +@[deprecated] alias mk_coe_nat := mk_natCast @[simp] theorem coe_coeHom : ⇑coeHom = ((↑) : ℚ≥0 → ℚ) := diff --git a/Mathlib/Data/Nat/Cast/Basic.lean b/Mathlib/Data/Nat/Cast/Basic.lean index 4eeba2554b724..11d9d88468ea7 100644 --- a/Mathlib/Data/Nat/Cast/Basic.lean +++ b/Mathlib/Data/Nat/Cast/Basic.lean @@ -313,14 +313,18 @@ variable {π : α → Type*} [∀ a, NatCast (π a)] Was `by refine_struct { .. } <;> pi_instance_derive_field` -/ instance natCast : NatCast (∀ a, π a) := { natCast := fun n _ ↦ n } -theorem nat_apply (n : ℕ) (a : α) : (n : ∀ a, π a) a = n := +theorem natCast_apply (n : ℕ) (a : α) : (n : ∀ a, π a) a = n := rfl -#align pi.nat_apply Pi.nat_apply +#align pi.nat_apply Pi.natCast_apply @[simp] -theorem coe_nat (n : ℕ) : (n : ∀ a, π a) = fun _ ↦ ↑n := +theorem natCast_def (n : ℕ) : (n : ∀ a, π a) = fun _ ↦ ↑n := rfl -#align pi.coe_nat Pi.coe_nat +#align pi.coe_nat Pi.natCast_def + +-- 2024-04-05 +@[deprecated] alias nat_apply := natCast_apply +@[deprecated] alias coe_nat := natCast_def @[simp] theorem ofNat_apply (n : ℕ) [n.AtLeastTwo] (a : α) : (OfNat.ofNat n : ∀ a, π a) a = n := rfl diff --git a/Mathlib/Data/Nat/ModEq.lean b/Mathlib/Data/Nat/ModEq.lean index 146852d209261..e66b40dedb68b 100644 --- a/Mathlib/Data/Nat/ModEq.lean +++ b/Mathlib/Data/Nat/ModEq.lean @@ -375,7 +375,7 @@ theorem chineseRemainder'_lt_lcm (h : a ≡ b [MOD gcd n m]) (hn : n ≠ 0) (hm ↑(chineseRemainder' h) < lcm n m := by dsimp only [chineseRemainder'] rw [dif_neg hn, dif_neg hm, Subtype.coe_mk, xgcd_val, ← Int.toNat_natCast (lcm n m)] - have lcm_pos := Int.coe_nat_pos.mpr (Nat.pos_of_ne_zero (lcm_ne_zero hn hm)) + have lcm_pos := Int.natCast_pos.mpr (Nat.pos_of_ne_zero (lcm_ne_zero hn hm)) exact (Int.toNat_lt_toNat lcm_pos).mpr (Int.emod_lt_of_pos _ lcm_pos) #align nat.chinese_remainder'_lt_lcm Nat.chineseRemainder'_lt_lcm diff --git a/Mathlib/Data/Rat/Cast/Defs.lean b/Mathlib/Data/Rat/Cast/Defs.lean index 9e0a0755125f8..5dd6dc52f3b40 100644 --- a/Mathlib/Data/Rat/Cast/Defs.lean +++ b/Mathlib/Data/Rat/Cast/Defs.lean @@ -94,7 +94,7 @@ theorem cast_mk_of_ne_zero (a b : ℤ) (b0 : (b : α) ≠ 0) : (a /. b : α) = a contradiction rw [num_den'] at e have := congr_arg ((↑) : ℤ → α) - ((divInt_eq_iff b0' <| ne_of_gt <| Int.coe_nat_pos.2 h.bot_lt).1 e) + ((divInt_eq_iff b0' <| ne_of_gt <| Int.natCast_pos.2 h.bot_lt).1 e) rw [Int.cast_mul, Int.cast_mul, Int.cast_natCast] at this -- Porting note: was `symm` apply Eq.symm diff --git a/Mathlib/Data/Rat/Cast/Lemmas.lean b/Mathlib/Data/Rat/Cast/Lemmas.lean index 50c3ba870776f..d6c093d075f26 100644 --- a/Mathlib/Data/Rat/Cast/Lemmas.lean +++ b/Mathlib/Data/Rat/Cast/Lemmas.lean @@ -28,7 +28,7 @@ variable {α : Type*} [DivisionRing α] theorem cast_inv_nat (n : ℕ) : ((n⁻¹ : ℚ) : α) = (n : α)⁻¹ := by cases' n with n · simp - rw [cast_def, inv_coe_nat_num, inv_coe_nat_den, if_neg n.succ_ne_zero, + rw [cast_def, inv_natCast_num, inv_natCast_den, if_neg n.succ_ne_zero, Int.sign_eq_one_of_pos (Nat.cast_pos.mpr n.succ_pos), Int.cast_one, one_div] #align rat.cast_inv_nat Rat.cast_inv_nat diff --git a/Mathlib/Data/Rat/Defs.lean b/Mathlib/Data/Rat/Defs.lean index 7455c37dd7672..3872ae6560c55 100644 --- a/Mathlib/Data/Rat/Defs.lean +++ b/Mathlib/Data/Rat/Defs.lean @@ -119,8 +119,8 @@ theorem num_den : ∀ {a : ℚ}, a.num /. a.den = a := divInt_self _ theorem num_den' {n d h c} : (⟨n, d, h, c⟩ : ℚ) = n /. d := num_den.symm #align rat.num_denom' Rat.num_den' -theorem coe_int_eq_divInt (z : ℤ) : (z : ℚ) = z /. 1 := num_den' -#align rat.coe_int_eq_mk Rat.coe_int_eq_divInt +theorem intCast_eq_divInt (z : ℤ) : (z : ℚ) = z /. 1 := num_den' +#align rat.coe_int_eq_mk Rat.intCast_eq_divInt /-- Define a (dependent) function or prove `∀ r : ℚ, p r` by dealing with rational numbers of the form `n /. d` with `0 < d` and coprime `n`, `d`. -/ @@ -345,7 +345,7 @@ instance commRing : CommRing ℚ where natCast n := Int.cast n natCast_zero := rfl natCast_succ n := by - simp only [coe_int_eq_divInt, add_def'' one_ne_zero one_ne_zero, + simp only [intCast_eq_divInt, add_def'' one_ne_zero one_ne_zero, ← divInt_one_one, Nat.cast_add, Nat.cast_one, mul_one] instance commGroupWithZero : CommGroupWithZero ℚ := @@ -489,7 +489,7 @@ protected theorem add_divInt (a b c : ℤ) : (a + b) /. c = a /. c + b /. c := theorem divInt_eq_div (n d : ℤ) : n /. d = (n : ℚ) / d := by by_cases d0 : d = 0 · simp [d0, div_zero] - simp [division_def, coe_int_eq_divInt, mul_def' one_ne_zero d0] + simp [division_def, intCast_eq_divInt, mul_def' one_ne_zero d0] #align rat.mk_eq_div Rat.divInt_eq_div theorem divInt_mul_divInt_cancel {x : ℤ} (hx : x ≠ 0) (n d : ℤ) : n /. x * (x /. d) = n /. d := by @@ -509,10 +509,10 @@ theorem divInt_div_divInt_cancel_right {x : ℤ} (hx : x ≠ 0) (n d : ℤ) : rw [div_eq_mul_inv, inv_def', mul_comm, divInt_mul_divInt_cancel hx] #align rat.mk_div_mk_cancel_right Rat.divInt_div_divInt_cancel_right -theorem coe_int_div_eq_divInt {n d : ℤ} : (n : ℚ) / (d) = n /. d := by - repeat' rw [coe_int_eq_divInt] +theorem intCast_div_eq_divInt {n d : ℤ} : (n : ℚ) / (d) = n /. d := by + repeat' rw [intCast_eq_divInt] exact divInt_div_divInt_cancel_left one_ne_zero n d -#align rat.coe_int_div_eq_mk Rat.coe_int_div_eq_divInt +#align rat.coe_int_div_eq_mk Rat.intCast_div_eq_divInt -- Porting note: see porting note above about `Int.cast`@[simp] theorem num_div_den (r : ℚ) : (r.num : ℚ) / (r.den : ℚ) = r := by @@ -522,7 +522,7 @@ theorem num_div_den (r : ℚ) : (r.num : ℚ) / (r.den : ℚ) = r := by theorem coe_int_num_of_den_eq_one {q : ℚ} (hq : q.den = 1) : (q.num : ℚ) = q := by conv_rhs => rw [← @num_den q, hq] - rw [coe_int_eq_divInt] + rw [intCast_eq_divInt] rfl #align rat.coe_int_num_of_denom_eq_one Rat.coe_int_num_of_den_eq_one @@ -538,9 +538,14 @@ instance canLift : CanLift ℚ ℤ (↑) fun q => q.den = 1 := ⟨fun q hq => ⟨q.num, coe_int_num_of_den_eq_one hq⟩⟩ #align rat.can_lift Rat.canLift -theorem coe_nat_eq_divInt (n : ℕ) : ↑n = n /. 1 := by - rw [← Int.cast_natCast, coe_int_eq_divInt] -#align rat.coe_nat_eq_mk Rat.coe_nat_eq_divInt +theorem natCast_eq_divInt (n : ℕ) : ↑n = n /. 1 := by + rw [← Int.cast_natCast, intCast_eq_divInt] +#align rat.coe_nat_eq_mk Rat.natCast_eq_divInt + +-- 2024-04-05 +@[deprecated] alias coe_int_eq_divInt := intCast_eq_divInt +@[deprecated] alias coe_int_div_eq_divInt := intCast_div_eq_divInt +@[deprecated] alias coe_nat_eq_divInt := natCast_eq_divInt @[simp, norm_cast] lemma num_natCast (n : ℕ) : num n = n := rfl #align rat.coe_nat_num Rat.num_natCast diff --git a/Mathlib/Data/Rat/Floor.lean b/Mathlib/Data/Rat/Floor.lean index cbc8711a5944b..a99f26e864a4d 100644 --- a/Mathlib/Data/Rat/Floor.lean +++ b/Mathlib/Data/Rat/Floor.lean @@ -44,7 +44,7 @@ protected theorem le_floor {z : ℤ} : ∀ {r : ℚ}, z ≤ Rat.floor r ↔ (z : have h' := Int.ofNat_lt.2 (Nat.pos_of_ne_zero h) conv => rhs - rw [coe_int_eq_divInt, Rat.le_def zero_lt_one h', mul_one] + rw [intCast_eq_divInt, Rat.le_def zero_lt_one h', mul_one] exact Int.le_ediv_iff_mul_le h' #align rat.le_floor Rat.le_floor @@ -64,7 +64,7 @@ theorem floor_int_div_nat_eq_div {n : ℤ} {d : ℕ} : ⌊(↑n : ℚ) / (↑d : exact mod_cast @Rat.exists_eq_mul_div_num_and_eq_mul_div_den n d (mod_cast hd.ne') rw [n_eq_c_mul_num, d_eq_c_mul_denom] refine' (Int.mul_ediv_mul_of_pos _ _ <| pos_of_mul_pos_left _ <| Int.natCast_nonneg q.den).symm - rwa [← d_eq_c_mul_denom, Int.coe_nat_pos] + rwa [← d_eq_c_mul_denom, Int.natCast_pos] #align rat.floor_int_div_nat_eq_div Rat.floor_int_div_nat_eq_div @[simp, norm_cast] diff --git a/Mathlib/Data/Rat/Lemmas.lean b/Mathlib/Data/Rat/Lemmas.lean index c5a24604b7974..6601eacabe654 100644 --- a/Mathlib/Data/Rat/Lemmas.lean +++ b/Mathlib/Data/Rat/Lemmas.lean @@ -23,7 +23,7 @@ open Rat theorem num_dvd (a) {b : ℤ} (b0 : b ≠ 0) : (a /. b).num ∣ a := by cases' e : a /. b with n d h c - rw [Rat.num_den', divInt_eq_iff b0 (ne_of_gt (Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h)))] at e + rw [Rat.num_den', divInt_eq_iff b0 (ne_of_gt (Int.natCast_pos.2 (Nat.pos_of_ne_zero h)))] at e refine Int.natAbs_dvd.1 <| Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <| c.dvd_of_dvd_mul_right ?_ have := congr_arg Int.natAbs e @@ -33,7 +33,7 @@ theorem num_dvd (a) {b : ℤ} (b0 : b ≠ 0) : (a /. b).num ∣ a := by theorem den_dvd (a b : ℤ) : ((a /. b).den : ℤ) ∣ b := by by_cases b0 : b = 0; · simp [b0] cases' e : a /. b with n d h c - rw [num_den', divInt_eq_iff b0 (ne_of_gt (Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h)))] at e + rw [num_den', divInt_eq_iff b0 (ne_of_gt (Int.natCast_pos.2 (Nat.pos_of_ne_zero h)))] at e refine' Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <| c.symm.dvd_of_dvd_mul_left _ rw [← Int.natAbs_mul, ← Int.natCast_dvd_natCast, Int.dvd_natAbs, ← e]; simp #align rat.denom_dvd Rat.den_dvd @@ -188,7 +188,7 @@ protected theorem inv_neg (q : ℚ) : (-q)⁻¹ = -q⁻¹ := by theorem mul_den_eq_num {q : ℚ} : q * q.den = q.num := by suffices (q.num /. ↑q.den) * (↑q.den /. 1) = q.num /. 1 by conv => pattern (occs := 1) q; (rw [← @num_den q]) - simp only [coe_int_eq_divInt, coe_nat_eq_divInt, num_den] at this ⊢; assumption + simp only [intCast_eq_divInt, natCast_eq_divInt, num_den] at this ⊢; assumption have : (q.den : ℤ) ≠ 0 := ne_of_gt (mod_cast q.pos) rw [Rat.mul_def' this one_ne_zero, mul_comm (q.den : ℤ) 1, divInt_mul_right this] #align rat.mul_denom_eq_num Rat.mul_den_eq_num @@ -228,95 +228,109 @@ theorem div_int_inj {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : Nat.Coprim #align rat.div_int_inj Rat.div_int_inj @[norm_cast] -theorem coe_int_div_self (n : ℤ) : ((n / n : ℤ) : ℚ) = n / n := by +theorem intCast_div_self (n : ℤ) : ((n / n : ℤ) : ℚ) = n / n := by by_cases hn : n = 0 · subst hn simp only [Int.cast_zero, Int.zero_div, zero_div, Int.ediv_zero] · have : (n : ℚ) ≠ 0 := by rwa [← coe_int_inj] at hn simp only [Int.ediv_self hn, Int.cast_one, Ne, not_false_iff, div_self this] -#align rat.coe_int_div_self Rat.coe_int_div_self +#align rat.coe_int_div_self Rat.intCast_div_self @[norm_cast] -theorem coe_nat_div_self (n : ℕ) : ((n / n : ℕ) : ℚ) = n / n := - coe_int_div_self n -#align rat.coe_nat_div_self Rat.coe_nat_div_self +theorem natCast_div_self (n : ℕ) : ((n / n : ℕ) : ℚ) = n / n := + intCast_div_self n +#align rat.coe_nat_div_self Rat.natCast_div_self -theorem coe_int_div (a b : ℤ) (h : b ∣ a) : ((a / b : ℤ) : ℚ) = a / b := by +theorem intCast_div (a b : ℤ) (h : b ∣ a) : ((a / b : ℤ) : ℚ) = a / b := by rcases h with ⟨c, rfl⟩ rw [mul_comm b, Int.mul_ediv_assoc c (dvd_refl b), Int.cast_mul, - coe_int_div_self, Int.cast_mul, mul_div_assoc] -#align rat.coe_int_div Rat.coe_int_div + intCast_div_self, Int.cast_mul, mul_div_assoc] +#align rat.coe_int_div Rat.intCast_div -theorem coe_nat_div (a b : ℕ) (h : b ∣ a) : ((a / b : ℕ) : ℚ) = a / b := by +theorem natCast_div (a b : ℕ) (h : b ∣ a) : ((a / b : ℕ) : ℚ) = a / b := by rcases h with ⟨c, rfl⟩ simp only [mul_comm b, Nat.mul_div_assoc c (dvd_refl b), Nat.cast_mul, mul_div_assoc, - coe_nat_div_self] -#align rat.coe_nat_div Rat.coe_nat_div + natCast_div_self] +#align rat.coe_nat_div Rat.natCast_div -theorem inv_coe_int_num_of_pos {a : ℤ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1 := by +theorem inv_intCast_num_of_pos {a : ℤ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1 := by rw [← ofInt_eq_cast, ofInt, mk_eq_divInt, Rat.inv_def', divInt_eq_div, Nat.cast_one] apply num_div_eq_of_coprime ha0 rw [Int.natAbs_one] exact Nat.coprime_one_left _ -#align rat.inv_coe_int_num_of_pos Rat.inv_coe_int_num_of_pos +#align rat.inv_coe_int_num_of_pos Rat.inv_intCast_num_of_pos -theorem inv_coe_nat_num_of_pos {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1 := - inv_coe_int_num_of_pos (mod_cast ha0 : 0 < (a : ℤ)) -#align rat.inv_coe_nat_num_of_pos Rat.inv_coe_nat_num_of_pos +theorem inv_natCast_num_of_pos {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.num = 1 := + inv_intCast_num_of_pos (mod_cast ha0 : 0 < (a : ℤ)) +#align rat.inv_coe_nat_num_of_pos Rat.inv_natCast_num_of_pos -theorem inv_coe_int_den_of_pos {a : ℤ} (ha0 : 0 < a) : ((a : ℚ)⁻¹.den : ℤ) = a := by +theorem inv_intCast_den_of_pos {a : ℤ} (ha0 : 0 < a) : ((a : ℚ)⁻¹.den : ℤ) = a := by rw [← ofInt_eq_cast, ofInt, mk_eq_divInt, Rat.inv_def', divInt_eq_div, Nat.cast_one] apply den_div_eq_of_coprime ha0 rw [Int.natAbs_one] exact Nat.coprime_one_left _ -#align rat.inv_coe_int_denom_of_pos Rat.inv_coe_int_den_of_pos +#align rat.inv_coe_int_denom_of_pos Rat.inv_intCast_den_of_pos -theorem inv_coe_nat_den_of_pos {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.den = a := by - rw [← Int.ofNat_inj, ← Int.cast_natCast a, inv_coe_int_den_of_pos] +theorem inv_natCast_den_of_pos {a : ℕ} (ha0 : 0 < a) : (a : ℚ)⁻¹.den = a := by + rw [← Int.ofNat_inj, ← Int.cast_natCast a, inv_intCast_den_of_pos] rwa [Nat.cast_pos] -#align rat.inv_coe_nat_denom_of_pos Rat.inv_coe_nat_den_of_pos +#align rat.inv_coe_nat_denom_of_pos Rat.inv_natCast_den_of_pos @[simp] -theorem inv_coe_int_num (a : ℤ) : (a : ℚ)⁻¹.num = Int.sign a := by +theorem inv_intCast_num (a : ℤ) : (a : ℚ)⁻¹.num = Int.sign a := by rcases lt_trichotomy a 0 with lt | rfl | gt · obtain ⟨a, rfl⟩ : ∃ b, -b = a := ⟨-a, a.neg_neg⟩ simp at lt - simp [Rat.inv_neg, inv_coe_int_num_of_pos lt, (Int.sign_eq_one_iff_pos _).mpr lt] + simp [Rat.inv_neg, inv_intCast_num_of_pos lt, (Int.sign_eq_one_iff_pos _).mpr lt] · rfl - · simp [inv_coe_int_num_of_pos gt, (Int.sign_eq_one_iff_pos _).mpr gt] -#align rat.inv_coe_int_num Rat.inv_coe_int_num + · simp [inv_intCast_num_of_pos gt, (Int.sign_eq_one_iff_pos _).mpr gt] +#align rat.inv_coe_int_num Rat.inv_intCast_num @[simp] -theorem inv_coe_nat_num (a : ℕ) : (a : ℚ)⁻¹.num = Int.sign a := - inv_coe_int_num a -#align rat.inv_coe_nat_num Rat.inv_coe_nat_num +theorem inv_natCast_num (a : ℕ) : (a : ℚ)⁻¹.num = Int.sign a := + inv_intCast_num a +#align rat.inv_coe_nat_num Rat.inv_natCast_num @[simp] theorem inv_ofNat_num (a : ℕ) [a.AtLeastTwo] : (no_index (OfNat.ofNat a : ℚ))⁻¹.num = 1 := - inv_coe_nat_num_of_pos (NeZero.pos a) + inv_natCast_num_of_pos (NeZero.pos a) @[simp] -theorem inv_coe_int_den (a : ℤ) : (a : ℚ)⁻¹.den = if a = 0 then 1 else a.natAbs := by +theorem inv_intCast_den (a : ℤ) : (a : ℚ)⁻¹.den = if a = 0 then 1 else a.natAbs := by rw [← Int.ofNat_inj] rcases lt_trichotomy a 0 with lt | rfl | gt · obtain ⟨a, rfl⟩ : ∃ b, -b = a := ⟨-a, a.neg_neg⟩ simp at lt rw [if_neg (by omega)] - simp [Rat.inv_neg, inv_coe_int_den_of_pos lt, abs_of_pos lt] + simp [Rat.inv_neg, inv_intCast_den_of_pos lt, abs_of_pos lt] · rfl · rw [if_neg (by omega)] - simp [inv_coe_int_den_of_pos gt, abs_of_pos gt] -#align rat.inv_coe_int_denom Rat.inv_coe_int_den + simp [inv_intCast_den_of_pos gt, abs_of_pos gt] +#align rat.inv_coe_int_denom Rat.inv_intCast_den @[simp] -theorem inv_coe_nat_den (a : ℕ) : (a : ℚ)⁻¹.den = if a = 0 then 1 else a := by - simpa [-inv_coe_int_den, ofInt_eq_cast] using inv_coe_int_den a -#align rat.inv_coe_nat_denom Rat.inv_coe_nat_den +theorem inv_natCast_den (a : ℕ) : (a : ℚ)⁻¹.den = if a = 0 then 1 else a := by + simpa [-inv_intCast_den, ofInt_eq_cast] using inv_intCast_den a +#align rat.inv_coe_nat_denom Rat.inv_natCast_den + +-- 2024-04-05 +@[deprecated] alias coe_int_div_self := intCast_div_self +@[deprecated] alias coe_nat_div_self := natCast_div_self +@[deprecated] alias coe_int_div := intCast_div +@[deprecated] alias coe_nat_div := natCast_div +@[deprecated] alias inv_coe_int_num_of_pos := inv_intCast_num_of_pos +@[deprecated] alias inv_coe_nat_num_of_pos := inv_natCast_num_of_pos +@[deprecated] alias inv_coe_int_den_of_pos := inv_intCast_den_of_pos +@[deprecated] alias inv_coe_nat_den_of_pos := inv_natCast_den_of_pos +@[deprecated] alias inv_coe_int_num := inv_intCast_num +@[deprecated] alias inv_coe_nat_num := inv_natCast_num +@[deprecated] alias inv_coe_int_den := inv_intCast_den +@[deprecated] alias inv_coe_nat_den := inv_natCast_den @[simp] theorem inv_ofNat_den (a : ℕ) [a.AtLeastTwo] : (no_index (OfNat.ofNat a : ℚ))⁻¹.den = OfNat.ofNat a := - inv_coe_nat_den_of_pos (NeZero.pos a) + inv_natCast_den_of_pos (NeZero.pos a) protected theorem «forall» {p : ℚ → Prop} : (∀ r, p r) ↔ ∀ a b : ℤ, p (a / b) := ⟨fun h _ _ => h _, diff --git a/Mathlib/Data/Rat/Order.lean b/Mathlib/Data/Rat/Order.lean index e4e74a0ce5bed..da65e7a42e303 100644 --- a/Mathlib/Data/Rat/Order.lean +++ b/Mathlib/Data/Rat/Order.lean @@ -53,8 +53,8 @@ theorem divInt_nonneg (a : ℤ) {b : ℤ} (h : 0 < b) : (a /. b).Nonneg ↔ 0 protected theorem nonneg_add {a b} : Rat.Nonneg a → Rat.Nonneg b → Rat.Nonneg (a + b) := numDenCasesOn' a fun n₁ d₁ h₁ => numDenCasesOn' b fun n₂ d₂ h₂ => by - have d₁0 : 0 < (d₁ : ℤ) := Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h₁) - have d₂0 : 0 < (d₂ : ℤ) := Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h₂) + have d₁0 : 0 < (d₁ : ℤ) := Int.natCast_pos.2 (Nat.pos_of_ne_zero h₁) + have d₂0 : 0 < (d₂ : ℤ) := Int.natCast_pos.2 (Nat.pos_of_ne_zero h₂) simp only [d₁0, d₂0, h₁, h₂, mul_pos, divInt_nonneg, add_def'', Ne, Nat.cast_eq_zero, not_false_iff] intro n₁0 n₂0 @@ -64,8 +64,8 @@ protected theorem nonneg_add {a b} : Rat.Nonneg a → Rat.Nonneg b → Rat.Nonne protected theorem nonneg_mul {a b} : Rat.Nonneg a → Rat.Nonneg b → Rat.Nonneg (a * b) := numDenCasesOn' a fun n₁ d₁ h₁ => numDenCasesOn' b fun n₂ d₂ h₂ => by - have d₁0 : 0 < (d₁ : ℤ) := Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h₁) - have d₂0 : 0 < (d₂ : ℤ) := Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h₂) + have d₁0 : 0 < (d₁ : ℤ) := Int.natCast_pos.2 (Nat.pos_of_ne_zero h₁) + have d₂0 : 0 < (d₂ : ℤ) := Int.natCast_pos.2 (Nat.pos_of_ne_zero h₂) rw [mul_def' d₁0.ne.symm d₂0.ne.symm, divInt_nonneg _ d₁0, divInt_nonneg _ d₂0, divInt_nonneg _ (mul_pos d₁0 d₂0)] apply mul_nonneg @@ -73,7 +73,7 @@ protected theorem nonneg_mul {a b} : Rat.Nonneg a → Rat.Nonneg b → Rat.Nonne protected theorem nonneg_antisymm {a} : Rat.Nonneg a → Rat.Nonneg (-a) → a = 0 := numDenCasesOn' a fun n d h => by - have d0 : 0 < (d : ℤ) := Int.coe_nat_pos.2 (Nat.pos_of_ne_zero h) + have d0 : 0 < (d : ℤ) := Int.natCast_pos.2 (Nat.pos_of_ne_zero h) rw [divInt_nonneg _ d0, neg_def, divInt_nonneg _ d0, Right.nonneg_neg_iff, divInt_eq_zero d0.ne.symm] exact fun h₁ h₂ => le_antisymm h₂ h₁ @@ -298,11 +298,11 @@ theorem lt_one_iff_num_lt_denom {q : ℚ} : q < 1 ↔ q.num < q.den := by simp [ theorem abs_def (q : ℚ) : |q| = q.num.natAbs /. q.den := by rcases le_total q 0 with hq | hq · rw [abs_of_nonpos hq] - rw [← @num_den q, ← divInt_zero_one, Rat.le_def (Int.coe_nat_pos.2 q.pos) zero_lt_one, mul_one, + rw [← @num_den q, ← divInt_zero_one, Rat.le_def (Int.natCast_pos.2 q.pos) zero_lt_one, mul_one, zero_mul] at hq rw [Int.ofNat_natAbs_of_nonpos hq, ← neg_def, num_den] · rw [abs_of_nonneg hq] - rw [← @num_den q, ← divInt_zero_one, Rat.le_def zero_lt_one (Int.coe_nat_pos.2 q.pos), mul_one, + rw [← @num_den q, ← divInt_zero_one, Rat.le_def zero_lt_one (Int.natCast_pos.2 q.pos), mul_one, zero_mul] at hq rw [Int.natAbs_of_nonneg hq, num_den] #align rat.abs_def Rat.abs_def diff --git a/Mathlib/Data/Rat/Sqrt.lean b/Mathlib/Data/Rat/Sqrt.lean index 7eda40a1c5f99..b625a8642ece1 100644 --- a/Mathlib/Data/Rat/Sqrt.lean +++ b/Mathlib/Data/Rat/Sqrt.lean @@ -37,7 +37,7 @@ theorem exists_mul_self (x : ℚ) : (∃ q, q * q = x) ↔ Rat.sqrt x * Rat.sqrt theorem sqrt_nonneg (q : ℚ) : 0 ≤ Rat.sqrt q := nonneg_iff_zero_le.1 <| (divInt_nonneg _ <| - Int.coe_nat_pos.2 <| + Int.natCast_pos.2 <| Nat.pos_of_ne_zero fun H => q.den_nz <| Nat.sqrt_eq_zero.1 H).2 <| Int.natCast_nonneg _ #align rat.sqrt_nonneg Rat.sqrt_nonneg diff --git a/Mathlib/Data/Real/Irrational.lean b/Mathlib/Data/Real/Irrational.lean index 596827bc8ab45..96d3dc39bdf62 100644 --- a/Mathlib/Data/Real/Irrational.lean +++ b/Mathlib/Data/Real/Irrational.lean @@ -94,7 +94,7 @@ theorem irrational_sqrt_of_multiplicity_odd (m : ℤ) (hm : 0 < m) (p : ℕ) [hp #align irrational_sqrt_of_multiplicity_odd irrational_sqrt_of_multiplicity_odd theorem Nat.Prime.irrational_sqrt {p : ℕ} (hp : Nat.Prime p) : Irrational (Real.sqrt p) := - @irrational_sqrt_of_multiplicity_odd p (Int.coe_nat_pos.2 hp.pos) p ⟨hp⟩ <| by + @irrational_sqrt_of_multiplicity_odd p (Int.natCast_pos.2 hp.pos) p ⟨hp⟩ <| by simp [multiplicity.multiplicity_self (mt isUnit_iff_dvd_one.1 (mt Int.natCast_dvd_natCast.1 hp.not_dvd_one))] #align nat.prime.irrational_sqrt Nat.Prime.irrational_sqrt diff --git a/Mathlib/Data/Real/NNReal.lean b/Mathlib/Data/Real/NNReal.lean index 65fc39df70922..6bcac134a2d2a 100644 --- a/Mathlib/Data/Real/NNReal.lean +++ b/Mathlib/Data/Real/NNReal.lean @@ -397,9 +397,12 @@ theorem _root_.Real.toNNReal_coe {r : ℝ≥0} : Real.toNNReal r = r := #align real.to_nnreal_coe Real.toNNReal_coe @[simp] -theorem mk_coe_nat (n : ℕ) : @Eq ℝ≥0 (⟨(n : ℝ), n.cast_nonneg⟩ : ℝ≥0) n := +theorem mk_natCast (n : ℕ) : @Eq ℝ≥0 (⟨(n : ℝ), n.cast_nonneg⟩ : ℝ≥0) n := NNReal.eq (NNReal.coe_nat_cast n).symm -#align nnreal.mk_coe_nat NNReal.mk_coe_nat +#align nnreal.mk_coe_nat NNReal.mk_natCast + +-- 2024-04-05 +@[deprecated] alias mk_coe_nat := mk_natCast -- Porting note: place this in the `Real` namespace @[simp] diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean index 21696e8ea3e12..968e35a0e0939 100644 --- a/Mathlib/FieldTheory/Adjoin.lean +++ b/Mathlib/FieldTheory/Adjoin.lean @@ -945,14 +945,18 @@ theorem adjoin_one : F⟮(1 : E)⟯ = ⊥ := #align intermediate_field.adjoin_one IntermediateField.adjoin_one @[simp] -theorem adjoin_int (n : ℤ) : F⟮(n : E)⟯ = ⊥ := by - exact adjoin_simple_eq_bot_iff.mpr (coe_int_mem ⊥ n) -#align intermediate_field.adjoin_int IntermediateField.adjoin_int +theorem adjoin_intCast (n : ℤ) : F⟮(n : E)⟯ = ⊥ := by + exact adjoin_simple_eq_bot_iff.mpr (intCast_mem ⊥ n) +#align intermediate_field.adjoin_int IntermediateField.adjoin_intCast @[simp] -theorem adjoin_nat (n : ℕ) : F⟮(n : E)⟯ = ⊥ := - adjoin_simple_eq_bot_iff.mpr (coe_nat_mem ⊥ n) -#align intermediate_field.adjoin_nat IntermediateField.adjoin_nat +theorem adjoin_natCast (n : ℕ) : F⟮(n : E)⟯ = ⊥ := + adjoin_simple_eq_bot_iff.mpr (natCast_mem ⊥ n) +#align intermediate_field.adjoin_nat IntermediateField.adjoin_natCast + +-- 2024-04-05 +@[deprecated] alias adjoin_int := adjoin_intCast +@[deprecated] alias adjoin_nat := adjoin_natCast section AdjoinRank diff --git a/Mathlib/FieldTheory/IntermediateField.lean b/Mathlib/FieldTheory/IntermediateField.lean index f5a879af5ff7e..c0e8df633f794 100644 --- a/Mathlib/FieldTheory/IntermediateField.lean +++ b/Mathlib/FieldTheory/IntermediateField.lean @@ -234,9 +234,9 @@ protected theorem zsmul_mem {x : L} (hx : x ∈ S) (n : ℤ) : n • x ∈ S := zsmul_mem hx n #align intermediate_field.zsmul_mem IntermediateField.zsmul_mem -protected theorem coe_int_mem (n : ℤ) : (n : L) ∈ S := - coe_int_mem S n -#align intermediate_field.coe_int_mem IntermediateField.coe_int_mem +protected theorem intCast_mem (n : ℤ) : (n : L) ∈ S := + intCast_mem S n +#align intermediate_field.coe_int_mem IntermediateField.intCast_mem protected theorem coe_add (x y : S) : (↑(x + y) : L) = ↑x + ↑y := rfl @@ -268,8 +268,12 @@ protected theorem coe_pow (x : S) (n : ℕ) : (↑(x ^ n : S) : L) = (x : L) ^ n end InheritedLemmas -theorem coe_nat_mem (n : ℕ) : (n : L) ∈ S := by simpa using coe_int_mem S n -#align intermediate_field.coe_nat_mem IntermediateField.coe_nat_mem +theorem natCast_mem (n : ℕ) : (n : L) ∈ S := by simpa using intCast_mem S n +#align intermediate_field.coe_nat_mem IntermediateField.natCast_mem + +-- 2024-04-05 +@[deprecated _root_.natCast_mem] alias coe_nat_mem := natCast_mem +@[deprecated _root_.intCast_mem] alias coe_int_mem := intCast_mem end IntermediateField diff --git a/Mathlib/FieldTheory/KummerExtension.lean b/Mathlib/FieldTheory/KummerExtension.lean index fc813768a6eeb..c1470988e0423 100644 --- a/Mathlib/FieldTheory/KummerExtension.lean +++ b/Mathlib/FieldTheory/KummerExtension.lean @@ -196,7 +196,7 @@ theorem X_pow_sub_C_irreducible_of_odd intro E _ _ x hx have : IsIntegral K x := not_not.mp fun h ↦ by simpa only [degree_zero, degree_X_pow_sub_C hp.pos, - WithBot.nat_ne_bot] using congr_arg degree (hx.symm.trans (dif_neg h)) + WithBot.natCast_ne_bot] using congr_arg degree (hx.symm.trans (dif_neg h)) apply IH (Nat.odd_mul.mp hn).2 intros q hq hqn b hb apply ha q hq (dvd_mul_of_dvd_right hqn p) (Algebra.norm _ b) diff --git a/Mathlib/FieldTheory/Subfield.lean b/Mathlib/FieldTheory/Subfield.lean index 876b43bcb0ec8..b3aa7154223e5 100644 --- a/Mathlib/FieldTheory/Subfield.lean +++ b/Mathlib/FieldTheory/Subfield.lean @@ -86,31 +86,33 @@ instance (priority := 100) toSubgroupClass : SubgroupClass S K := { h with } #align subfield_class.subfield_class.to_subgroup_class SubfieldClass.toSubgroupClass -variable {S} +variable {S} {x : K} @[aesop safe apply (rule_sets := [SetLike])] -theorem coe_rat_mem (s : S) (x : ℚ) : (x : K) ∈ s := by - simpa only [Rat.cast_def] using div_mem (coe_int_mem s x.num) (coe_nat_mem s x.den) -#align subfield_class.coe_rat_mem SubfieldClass.coe_rat_mem +lemma ratCast_mem (s : S) (q : ℚ) : (q : K) ∈ s := by + simpa only [Rat.cast_def] using div_mem (intCast_mem s q.num) (natCast_mem s q.den) +#align subfield_class.coe_rat_mem SubfieldClass.ratCast_mem instance (s : S) : RatCast s := - ⟨fun x => ⟨↑x, coe_rat_mem s x⟩⟩ + ⟨fun x => ⟨↑x, ratCast_mem s x⟩⟩ -@[simp] -theorem coe_rat_cast (s : S) (x : ℚ) : ((x : s) : K) = x := - rfl -#align subfield_class.coe_rat_cast SubfieldClass.coe_rat_cast +@[simp, norm_cast] lemma coe_ratCast (s : S) (x : ℚ) : ((x : s) : K) = x := rfl +#align subfield_class.coe_rat_cast SubfieldClass.coe_ratCast + +-- 2024-04-05 +@[deprecated] alias coe_rat_cast := coe_ratCast +@[deprecated] alias coe_rat_mem := ratCast_mem -- Porting note: Mistranslated: used to be (a • x : K) ∈ s @[aesop safe apply (rule_sets := [SetLike])] theorem rat_smul_mem (s : S) (a : ℚ) (x : s) : a • (x : K) ∈ s := by - simpa only [Rat.smul_def] using mul_mem (coe_rat_mem s a) x.prop + simpa only [Rat.smul_def] using mul_mem (ratCast_mem s a) x.prop #align subfield_class.rat_smul_mem SubfieldClass.rat_smul_mem @[aesop safe apply (rule_sets := [SetLike])] lemma ofScientific_mem (s : S) {b : Bool} {n m : ℕ} : (OfScientific.ofScientific n b m : K) ∈ s := - SubfieldClass.coe_rat_mem .. + SubfieldClass.ratCast_mem .. instance (s : S) : SMul ℚ s := ⟨fun a x => ⟨a • (x : K), rat_smul_mem s a x⟩⟩ @@ -316,9 +318,11 @@ protected theorem zsmul_mem {x : K} (hx : x ∈ s) (n : ℤ) : n • x ∈ s := zsmul_mem hx n #align subfield.zsmul_mem Subfield.zsmul_mem -protected theorem coe_int_mem (n : ℤ) : (n : K) ∈ s := - coe_int_mem s n -#align subfield.coe_int_mem Subfield.coe_int_mem +protected theorem intCast_mem (n : ℤ) : (n : K) ∈ s := intCast_mem s n +#align subfield.coe_int_mem Subfield.intCast_mem + +-- 2024-04-05 +@[deprecated] alias coe_int_mem := intCast_mem theorem zpow_mem {x : K} (hx : x ∈ s) (n : ℤ) : x ^ n ∈ s := by cases n diff --git a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean index 751d0486b9ce5..b5ffef285e792 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Basic.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Basic.lean @@ -228,7 +228,7 @@ theorem SameCycle.exists_pow_eq' [Finite α] : SameCycle f x y → ∃ i < order classical rintro ⟨k, rfl⟩ use (k % orderOf f).natAbs - have h₀ := Int.coe_nat_pos.mpr (orderOf_pos f) + have h₀ := Int.natCast_pos.mpr (orderOf_pos f) have h₁ := Int.emod_nonneg k h₀.ne' rw [← zpow_natCast, Int.natAbs_of_nonneg h₁, zpow_mod_orderOf] refine' ⟨_, by rfl⟩ diff --git a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean index d3c8f7d949deb..df9a406c49d91 100644 --- a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean +++ b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean @@ -261,7 +261,7 @@ instance Subgroup.isCyclic {α : Type u} [Group α] [IsCyclic α] (H : Subgroup by_contradiction fun h => Nat.find_min hex (Int.ofNat_lt.1 <| by - rw [← hk₄]; exact Int.emod_lt_of_pos _ (Int.coe_nat_pos.2 (Nat.find_spec hex).1)) + rw [← hk₄]; exact Int.emod_lt_of_pos _ (Int.natCast_pos.2 (Nat.find_spec hex).1)) ⟨Nat.pos_of_ne_zero h, hk₅⟩ ⟨k / (Nat.find hex : ℤ), Subtype.ext_iff_val.2 diff --git a/Mathlib/LinearAlgebra/Matrix/ZPow.lean b/Mathlib/LinearAlgebra/Matrix/ZPow.lean index 18855b5f620f6..65a22e2e18aea 100644 --- a/Mathlib/LinearAlgebra/Matrix/ZPow.lean +++ b/Mathlib/LinearAlgebra/Matrix/ZPow.lean @@ -107,16 +107,17 @@ theorem zpow_neg_one (A : M) : A ^ (-1 : ℤ) = A⁻¹ := by simp only [zpow_one, Int.ofNat_zero, Int.ofNat_succ, zpow_eq_pow, zero_add] #align matrix.zpow_neg_one Matrix.zpow_neg_one -nonrec theorem zpow_coe_nat (A : M) (n : ℕ) : A ^ (n : ℤ) = A ^ n := - zpow_natCast _ _ -#align matrix.zpow_coe_nat Matrix.zpow_coe_nat +#align matrix.zpow_coe_nat zpow_natCast @[simp] -theorem zpow_neg_coe_nat (A : M) (n : ℕ) : A ^ (-n : ℤ) = (A ^ n)⁻¹ := by +theorem zpow_neg_natCast (A : M) (n : ℕ) : A ^ (-n : ℤ) = (A ^ n)⁻¹ := by cases n · simp · exact DivInvMonoid.zpow_neg' _ _ -#align matrix.zpow_neg_coe_nat Matrix.zpow_neg_coe_nat +#align matrix.zpow_neg_coe_nat Matrix.zpow_neg_natCast + +-- 2024-04-05 +@[deprecated] alias zpow_neg_coe_nat := zpow_neg_natCast theorem _root_.IsUnit.det_zpow {A : M} (h : IsUnit A.det) (n : ℤ) : IsUnit (A ^ n).det := by cases' n with n n @@ -127,18 +128,18 @@ theorem _root_.IsUnit.det_zpow {A : M} (h : IsUnit A.det) (n : ℤ) : IsUnit (A theorem isUnit_det_zpow_iff {A : M} {z : ℤ} : IsUnit (A ^ z).det ↔ IsUnit A.det ∨ z = 0 := by induction' z using Int.induction_on with z _ z _ · simp - · rw [← Int.ofNat_succ, zpow_coe_nat, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero, + · rw [← Int.ofNat_succ, zpow_natCast, det_pow, isUnit_pow_succ_iff, ← Int.ofNat_zero, Int.ofNat_inj] simp - · rw [← neg_add', ← Int.ofNat_succ, zpow_neg_coe_nat, isUnit_nonsing_inv_det_iff, det_pow, + · rw [← neg_add', ← Int.ofNat_succ, zpow_neg_natCast, isUnit_nonsing_inv_det_iff, det_pow, isUnit_pow_succ_iff, neg_eq_zero, ← Int.ofNat_zero, Int.ofNat_inj] simp #align matrix.is_unit_det_zpow_iff Matrix.isUnit_det_zpow_iff theorem zpow_neg {A : M} (h : IsUnit A.det) : ∀ n : ℤ, A ^ (-n) = (A ^ n)⁻¹ - | (n : ℕ) => zpow_neg_coe_nat _ _ + | (n : ℕ) => zpow_neg_natCast _ _ | -[n+1] => by - rw [zpow_negSucc, neg_negSucc, zpow_coe_nat, nonsing_inv_nonsing_inv] + rw [zpow_negSucc, neg_negSucc, zpow_natCast, nonsing_inv_nonsing_inv] rw [det_pow] exact h.pow _ #align matrix.zpow_neg Matrix.zpow_neg @@ -148,15 +149,15 @@ theorem inv_zpow' {A : M} (h : IsUnit A.det) (n : ℤ) : A⁻¹ ^ n = A ^ (-n) : #align matrix.inv_zpow' Matrix.inv_zpow' theorem zpow_add_one {A : M} (h : IsUnit A.det) : ∀ n : ℤ, A ^ (n + 1) = A ^ n * A - | (n : ℕ) => by simp only [← Nat.cast_succ, pow_succ, zpow_coe_nat] + | (n : ℕ) => by simp only [← Nat.cast_succ, pow_succ, zpow_natCast] | -[n+1] => calc A ^ (-(n + 1) + 1 : ℤ) = (A ^ n)⁻¹ := by - rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_coe_nat] + rw [neg_add, neg_add_cancel_right, zpow_neg h, zpow_natCast] _ = (A * A ^ n)⁻¹ * A := by rw [mul_inv_rev, Matrix.mul_assoc, nonsing_inv_mul _ h, Matrix.mul_one] _ = A ^ (-(n + 1 : ℤ)) * A := by - rw [zpow_neg h, ← Int.ofNat_succ, zpow_coe_nat, pow_succ'] + rw [zpow_neg h, ← Int.ofNat_succ, zpow_natCast, pow_succ'] #align matrix.zpow_add_one Matrix.zpow_add_one theorem zpow_sub_one {A : M} (h : IsUnit A.det) (n : ℤ) : A ^ (n - 1) = A ^ n * A⁻¹ := @@ -179,14 +180,14 @@ theorem zpow_add_of_nonpos {A : M} {m n : ℤ} (hm : m ≤ 0) (hn : n ≤ 0) : · exact zpow_add (isUnit_det_of_left_inverse h) m n · obtain ⟨k, rfl⟩ := exists_eq_neg_ofNat hm obtain ⟨l, rfl⟩ := exists_eq_neg_ofNat hn - simp_rw [← neg_add, ← Int.ofNat_add, zpow_neg_coe_nat, ← inv_pow', h, pow_add] + simp_rw [← neg_add, ← Int.ofNat_add, zpow_neg_natCast, ← inv_pow', h, pow_add] #align matrix.zpow_add_of_nonpos Matrix.zpow_add_of_nonpos theorem zpow_add_of_nonneg {A : M} {m n : ℤ} (hm : 0 ≤ m) (hn : 0 ≤ n) : A ^ (m + n) = A ^ m * A ^ n := by obtain ⟨k, rfl⟩ := eq_ofNat_of_zero_le hm obtain ⟨l, rfl⟩ := eq_ofNat_of_zero_le hn - rw [← Int.ofNat_add, zpow_coe_nat, zpow_coe_nat, zpow_coe_nat, pow_add] + rw [← Int.ofNat_add, zpow_natCast, zpow_natCast, zpow_natCast, pow_add] #align matrix.zpow_add_of_nonneg Matrix.zpow_add_of_nonneg theorem zpow_one_add {A : M} (h : IsUnit A.det) (i : ℤ) : A ^ (1 + i) = A * A ^ i := by @@ -248,13 +249,13 @@ theorem zpow_bit0 (A : M) (n : ℤ) : A ^ bit0 n = A ^ n * A ^ n := by #align matrix.zpow_bit0 Matrix.zpow_bit0 theorem zpow_add_one_of_ne_neg_one {A : M} : ∀ n : ℤ, n ≠ -1 → A ^ (n + 1) = A ^ n * A - | (n : ℕ), _ => by simp only [pow_succ, ← Nat.cast_succ, zpow_coe_nat] + | (n : ℕ), _ => by simp only [pow_succ, ← Nat.cast_succ, zpow_natCast] | -1, h => absurd rfl h | -((n : ℕ) + 2), _ => by rcases nonsing_inv_cancel_or_zero A with (⟨h, _⟩ | h) · apply zpow_add_one (isUnit_det_of_left_inverse h) · show A ^ (-((n + 1 : ℕ) : ℤ)) = A ^ (-((n + 2 : ℕ) : ℤ)) * A - simp_rw [zpow_neg_coe_nat, ← inv_pow', h, zero_pow $ Nat.succ_ne_zero _, zero_mul] + simp_rw [zpow_neg_natCast, ← inv_pow', h, zero_pow $ Nat.succ_ne_zero _, zero_mul] #align matrix.zpow_add_one_of_ne_neg_one Matrix.zpow_add_one_of_ne_neg_one set_option linter.deprecated false in @@ -265,14 +266,14 @@ theorem zpow_bit1 (A : M) (n : ℤ) : A ^ bit1 n = A ^ n * A ^ n * A := by #align matrix.zpow_bit1 Matrix.zpow_bit1 theorem zpow_mul (A : M) (h : IsUnit A.det) : ∀ m n : ℤ, A ^ (m * n) = (A ^ m) ^ n - | (m : ℕ), (n : ℕ) => by rw [zpow_coe_nat, zpow_coe_nat, ← pow_mul, ← zpow_coe_nat, Int.ofNat_mul] + | (m : ℕ), (n : ℕ) => by rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast, Int.ofNat_mul] | (m : ℕ), -[n+1] => by - rw [zpow_coe_nat, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_coe_nat] + rw [zpow_natCast, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_natCast] | -[m+1], (n : ℕ) => by - rw [zpow_coe_nat, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_coe_nat, + rw [zpow_natCast, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_natCast, inv_pow'] | -[m+1], -[n+1] => by - rw [zpow_negSucc, zpow_negSucc, negSucc_mul_negSucc, ← Int.ofNat_mul, zpow_coe_nat, inv_pow', ← + rw [zpow_negSucc, zpow_negSucc, negSucc_mul_negSucc, ← Int.ofNat_mul, zpow_natCast, inv_pow', ← pow_mul, nonsing_inv_nonsing_inv] rw [det_pow] exact h.pow _ @@ -285,7 +286,7 @@ theorem zpow_mul' (A : M) (h : IsUnit A.det) (m n : ℤ) : A ^ (m * n) = (A ^ n) @[simp, norm_cast] theorem coe_units_zpow (u : Mˣ) : ∀ n : ℤ, ((u ^ n : Mˣ) : M) = (u : M) ^ n - | (n : ℕ) => by rw [zpow_natCast, zpow_coe_nat, Units.val_pow_eq_pow_val] + | (n : ℕ) => by rw [zpow_natCast, zpow_natCast, Units.val_pow_eq_pow_val] | -[k+1] => by rw [zpow_negSucc, zpow_negSucc, ← inv_pow, u⁻¹.val_pow_eq_pow_val, ← inv_pow', coe_units_inv] #align matrix.coe_units_zpow Matrix.coe_units_zpow @@ -331,13 +332,13 @@ theorem one_div_zpow {A : M} (n : ℤ) : (1 / A) ^ n = 1 / A ^ n := by simp only @[simp] theorem transpose_zpow (A : M) : ∀ n : ℤ, (A ^ n)ᵀ = Aᵀ ^ n - | (n : ℕ) => by rw [zpow_coe_nat, zpow_coe_nat, transpose_pow] + | (n : ℕ) => by rw [zpow_natCast, zpow_natCast, transpose_pow] | -[n+1] => by rw [zpow_negSucc, zpow_negSucc, transpose_nonsing_inv, transpose_pow] #align matrix.transpose_zpow Matrix.transpose_zpow @[simp] theorem conjTranspose_zpow [StarRing R] (A : M) : ∀ n : ℤ, (A ^ n)ᴴ = Aᴴ ^ n - | (n : ℕ) => by rw [zpow_coe_nat, zpow_coe_nat, conjTranspose_pow] + | (n : ℕ) => by rw [zpow_natCast, zpow_natCast, conjTranspose_pow] | -[n+1] => by rw [zpow_negSucc, zpow_negSucc, conjTranspose_nonsing_inv, conjTranspose_pow] #align matrix.conj_transpose_zpow Matrix.conjTranspose_zpow diff --git a/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean b/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean index 506e36011356c..afac459f0a0da 100644 --- a/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean +++ b/Mathlib/MeasureTheory/Constructions/HaarToSphere.lean @@ -72,7 +72,7 @@ theorem toSphere_apply_univ : μ.toSphere univ = dim E * μ (ball 0 1) := by instance : IsFiniteMeasure μ.toSphere where measure_univ_lt_top := by rw [toSphere_apply_univ'] - exact ENNReal.mul_lt_top (ENNReal.nat_ne_top _) <| + exact ENNReal.mul_lt_top (ENNReal.natCast_ne_top _) <| ne_top_of_le_ne_top measure_ball_lt_top.ne <| measure_mono (diff_subset _ _) /-- The measure on `(0, +∞)` that has density `(· ^ n)` with respect to the Lebesgue measure. -/ @@ -121,7 +121,7 @@ theorem measurePreserving_homeomorphUnitSphereProd : rw [(Homeomorph.measurableEmbedding _).map_apply, toSphere_apply' _ hs, volumeIoiPow_apply_Iio, comap_subtype_coe_apply (measurableSet_singleton _).compl, toSphere_apply_aux, this, smul_assoc, μ.addHaar_smul_of_nonneg r.2.out.le, Nat.sub_add_cancel hpos, Nat.cast_pred hpos, - sub_add_cancel, mul_right_comm, ← ENNReal.ofReal_coe_nat, ← ENNReal.ofReal_mul, mul_div_cancel₀] + sub_add_cancel, mul_right_comm, ← ENNReal.ofReal_natCast, ← ENNReal.ofReal_mul, mul_div_cancel₀] exacts [(Nat.cast_pos.2 hpos).ne', Nat.cast_nonneg _] end Measure diff --git a/Mathlib/MeasureTheory/Covering/Besicovitch.lean b/Mathlib/MeasureTheory/Covering/Besicovitch.lean index f7460e78181ed..0f155c65a3712 100644 --- a/Mathlib/MeasureTheory/Covering/Besicovitch.lean +++ b/Mathlib/MeasureTheory/Covering/Besicovitch.lean @@ -599,7 +599,7 @@ theorem exist_finset_disjoint_balls_large_measure (μ : Measure α) [IsFiniteMea simp only [Finset.card_fin, Finset.sum_const, nsmul_eq_mul] rw [ENNReal.mul_div_cancel'] · simp only [Npos, Ne, Nat.cast_eq_zero, not_false_iff] - · exact ENNReal.nat_ne_top _ + · exact ENNReal.natCast_ne_top _ _ ≤ ∑ i, μ (s ∩ v i) := by conv_lhs => rw [A] apply measure_iUnion_fintype_le @@ -612,7 +612,7 @@ theorem exist_finset_disjoint_balls_large_measure (μ : Measure α) [IsFiniteMea apply (ENNReal.mul_lt_mul_left hμs.ne' (measure_lt_top μ s).ne).2 rw [ENNReal.inv_lt_inv] conv_lhs => rw [← add_zero (N : ℝ≥0∞)] - exact ENNReal.add_lt_add_left (ENNReal.nat_ne_top N) zero_lt_one + exact ENNReal.add_lt_add_left (ENNReal.natCast_ne_top N) zero_lt_one have B : μ (o ∩ v i) = ∑' x : u i, μ (o ∩ closedBall x (r x)) := by have : o ∩ v i = ⋃ (x : s) (_ : x ∈ u i), o ∩ closedBall x (r x) := by simp only [v, inter_iUnion] @@ -804,9 +804,9 @@ theorem exists_disjoint_closedBall_covering_ae_of_finiteMeasure_aux (μ : Measur apply ENNReal.tendsto_pow_atTop_nhds_zero_of_lt_one rw [ENNReal.div_lt_iff, one_mul] · conv_lhs => rw [← add_zero (N : ℝ≥0∞)] - exact ENNReal.add_lt_add_left (ENNReal.nat_ne_top N) zero_lt_one + exact ENNReal.add_lt_add_left (ENNReal.natCast_ne_top N) zero_lt_one · simp only [true_or_iff, add_eq_zero_iff, Ne, not_false_iff, one_ne_zero, and_false_iff] - · simp only [ENNReal.nat_ne_top, Ne, not_false_iff, or_true_iff] + · simp only [ENNReal.natCast_ne_top, Ne, not_false_iff, or_true_iff] rw [zero_mul] at C apply le_bot_iff.1 exact le_of_tendsto_of_tendsto' tendsto_const_nhds C fun n => (A n).trans (B n) @@ -904,9 +904,8 @@ theorem exists_closedBall_covering_tsum_measure_le (μ : Measure α) [SigmaFinit HasBesicovitchCovering.no_satelliteConfig obtain ⟨v, s'v, v_open, μv⟩ : ∃ v, v ⊇ s' ∧ IsOpen v ∧ μ v ≤ μ s' + ε / 2 / N := Set.exists_isOpen_le_add _ _ - (by - simp only [ne_eq, ENNReal.div_eq_zero_iff, hε, ENNReal.two_ne_top, or_self, - ENNReal.nat_ne_top, not_false_eq_true]) + (by simp only [ne_eq, ENNReal.div_eq_zero_iff, hε, ENNReal.two_ne_top, or_self, + ENNReal.natCast_ne_top, not_false_eq_true]) have : ∀ x ∈ s', ∃ r1 ∈ f x ∩ Ioo (0 : ℝ) 1, closedBall x r1 ⊆ v := by intro x hx rcases Metric.mem_nhds_iff.1 (v_open.mem_nhds (s'v hx)) with ⟨r, rpos, hr⟩ diff --git a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean index bc2d2002b1513..3b42bbab90f4d 100644 --- a/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean +++ b/Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean @@ -209,7 +209,7 @@ theorem ae_le_of_forall_set_lintegral_le_of_sigmaFinite [SigmaFinite μ] {f g : exact eventually_le_of_tendsto_lt hx this have L2 : ∀ᶠ n : ℕ in (atTop : Filter ℕ), g x ≤ (n : ℝ≥0) := haveI : Tendsto (fun n : ℕ => ((n : ℝ≥0) : ℝ≥0∞)) atTop (𝓝 ∞) := by - simp only [ENNReal.coe_nat] + simp only [ENNReal.coe_natCast] exact ENNReal.tendsto_nat_nhds_top eventually_ge_of_tendsto_gt (hx.trans_le le_top) this apply Set.mem_iUnion.2 diff --git a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean index 2485716bef1ee..bef910140ce00 100644 --- a/Mathlib/MeasureTheory/Function/UniformIntegrable.lean +++ b/Mathlib/MeasureTheory/Function/UniformIntegrable.lean @@ -929,7 +929,7 @@ theorem uniformIntegrable_average refine' le_trans (snorm_sum_le (fun i _ => ((hf₁ i).const_smul _).indicator hs) hp) _ have : ∀ i, s.indicator ((n : ℝ) ⁻¹ • f i) = (↑n : ℝ)⁻¹ • s.indicator (f i) := fun i ↦ indicator_const_smul _ _ _ - simp_rw [this, snorm_const_smul, ← Finset.mul_sum, nnnorm_inv, Real.nnnorm_coe_nat] + simp_rw [this, snorm_const_smul, ← Finset.mul_sum, nnnorm_inv, Real.nnnorm_natCast] by_cases hn : (↑(↑n : ℝ≥0)⁻¹ : ℝ≥0∞) = 0 · simp only [hn, zero_mul, zero_le] refine' le_trans _ (_ : ↑(↑n : ℝ≥0)⁻¹ * n • ENNReal.ofReal ε ≤ ENNReal.ofReal ε) @@ -937,13 +937,13 @@ theorem uniformIntegrable_average conv_rhs => rw [← Finset.card_range n] exact Finset.sum_le_card_nsmul _ _ _ fun i _ => hδ₂ _ _ hs hle · simp only [ENNReal.coe_eq_zero, inv_eq_zero, Nat.cast_eq_zero] at hn - rw [nsmul_eq_mul, ← mul_assoc, ENNReal.coe_inv, ENNReal.coe_nat, - ENNReal.inv_mul_cancel _ (ENNReal.nat_ne_top _), one_mul] + rw [nsmul_eq_mul, ← mul_assoc, ENNReal.coe_inv, ENNReal.coe_natCast, + ENNReal.inv_mul_cancel _ (ENNReal.natCast_ne_top _), one_mul] all_goals simpa only [Ne, Nat.cast_eq_zero] · obtain ⟨C, hC⟩ := hf₃ simp_rw [Finset.smul_sum] refine' ⟨C, fun n => (snorm_sum_le (fun i _ => (hf₁ i).const_smul _) hp).trans _⟩ - simp_rw [snorm_const_smul, ← Finset.mul_sum, nnnorm_inv, Real.nnnorm_coe_nat] + simp_rw [snorm_const_smul, ← Finset.mul_sum, nnnorm_inv, Real.nnnorm_natCast] by_cases hn : (↑(↑n : ℝ≥0)⁻¹ : ℝ≥0∞) = 0 · simp only [hn, zero_mul, zero_le] refine' le_trans _ (_ : ↑(↑n : ℝ≥0)⁻¹ * (n • C : ℝ≥0∞) ≤ C) @@ -951,8 +951,8 @@ theorem uniformIntegrable_average conv_rhs => rw [← Finset.card_range n] exact Finset.sum_le_card_nsmul _ _ _ fun i _ => hC i · simp only [ENNReal.coe_eq_zero, inv_eq_zero, Nat.cast_eq_zero] at hn - rw [nsmul_eq_mul, ← mul_assoc, ENNReal.coe_inv, ENNReal.coe_nat, - ENNReal.inv_mul_cancel _ (ENNReal.nat_ne_top _), one_mul] + rw [nsmul_eq_mul, ← mul_assoc, ENNReal.coe_inv, ENNReal.coe_natCast, + ENNReal.inv_mul_cancel _ (ENNReal.natCast_ne_top _), one_mul] all_goals simpa only [Ne, Nat.cast_eq_zero] /-- The averaging of a uniformly integrable real-valued sequence is also uniformly integrable. -/ diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean index 9e12f74f5e9bf..603d6dff51995 100644 --- a/Mathlib/MeasureTheory/Group/Measure.lean +++ b/Mathlib/MeasureTheory/Group/Measure.lean @@ -702,7 +702,7 @@ theorem measure_lt_top_of_isCompact_of_isMulLeftInvariant (U : Set G) (hU : IsOp μ K ≤ μ (⋃ (g : G) (_ : g ∈ t), (fun h : G => g * h) ⁻¹' U) := measure_mono hKt _ ≤ ∑ g in t, μ ((fun h : G => g * h) ⁻¹' U) := (measure_biUnion_finset_le _ _) _ = Finset.card t * μ U := by simp only [measure_preimage_mul, Finset.sum_const, nsmul_eq_mul] - _ < ∞ := ENNReal.mul_lt_top (ENNReal.nat_ne_top _) h + _ < ∞ := ENNReal.mul_lt_top (ENNReal.natCast_ne_top _) h #align measure_theory.measure_lt_top_of_is_compact_of_is_mul_left_invariant MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant #align measure_theory.measure_lt_top_of_is_compact_of_is_add_left_invariant MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant diff --git a/Mathlib/MeasureTheory/Integral/Lebesgue.lean b/Mathlib/MeasureTheory/Integral/Lebesgue.lean index 61de9c8cff3e5..acf4300b2b38b 100644 --- a/Mathlib/MeasureTheory/Integral/Lebesgue.lean +++ b/Mathlib/MeasureTheory/Integral/Lebesgue.lean @@ -212,7 +212,7 @@ theorem lintegral_eq_nnreal {m : MeasurableSpace α} (f : α → ℝ≥0∞) (μ obtain ⟨n, hn⟩ : ∃ n : ℕ, b < n * μ (φ ⁻¹' {∞}) := exists_nat_mul_gt h_meas (ne_of_lt hb) use (const α (n : ℝ≥0)).restrict (φ ⁻¹' {∞}) simp only [lt_iSup_iff, exists_prop, coe_restrict, φ.measurableSet_preimage, coe_const, - ENNReal.coe_indicator, map_coe_ennreal_restrict, SimpleFunc.map_const, ENNReal.coe_nat, + ENNReal.coe_indicator, map_coe_ennreal_restrict, SimpleFunc.map_const, ENNReal.coe_natCast, restrict_const_lintegral] refine' ⟨indicator_le fun x hx => le_trans _ (hφ _), hn⟩ simp only [mem_preimage, mem_singleton_iff] at hx @@ -910,7 +910,7 @@ theorem ae_eq_of_ae_le_of_lintegral_le {f g : α → ℝ≥0∞} (hfg : f ≤ᵐ have : ∫⁻ x, f x ∂μ + (↑n)⁻¹ * μ { x : α | f x + (n : ℝ≥0∞)⁻¹ ≤ g x } ≤ ∫⁻ x, f x ∂μ := (lintegral_add_mul_meas_add_le_le_lintegral hfg hg n⁻¹).trans hgf rw [(ENNReal.cancel_of_ne hf).add_le_iff_nonpos_right, nonpos_iff_eq_zero, mul_eq_zero] at this - exact this.resolve_left (ENNReal.inv_ne_zero.2 (ENNReal.nat_ne_top _)) + exact this.resolve_left (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _)) refine' hfg.mp ((ae_all_iff.2 this).mono fun x hlt hle => hle.antisymm _) suffices Tendsto (fun n : ℕ => f x + (n : ℝ≥0∞)⁻¹) atTop (𝓝 (f x)) from ge_of_tendsto' this fun i => (hlt i).le diff --git a/Mathlib/MeasureTheory/Measure/Count.lean b/Mathlib/MeasureTheory/Measure/Count.lean index 1e1deefcbe23d..8258a9d792010 100644 --- a/Mathlib/MeasureTheory/Measure/Count.lean +++ b/Mathlib/MeasureTheory/Measure/Count.lean @@ -183,5 +183,5 @@ instance count.isFiniteMeasure [Finite α] : IsFiniteMeasure (Measure.count : Measure α) := ⟨by cases nonempty_fintype α - simpa [Measure.count_apply, tsum_fintype] using (ENNReal.nat_ne_top _).lt_top⟩ + simpa [Measure.count_apply, tsum_fintype] using (ENNReal.natCast_ne_top _).lt_top⟩ #align measure_theory.measure.count.is_finite_measure MeasureTheory.Measure.count.isFiniteMeasure diff --git a/Mathlib/MeasureTheory/Measure/Hausdorff.lean b/Mathlib/MeasureTheory/Measure/Hausdorff.lean index 7313b83650a8e..78c2c08fbaa72 100644 --- a/Mathlib/MeasureTheory/Measure/Hausdorff.lean +++ b/Mathlib/MeasureTheory/Measure/Hausdorff.lean @@ -160,9 +160,9 @@ theorem borel_le_caratheodory (hm : IsMetric μ) : borel X ≤ μ.caratheodory : rw [borel_eq_generateFrom_isClosed] refine' MeasurableSpace.generateFrom_le fun t ht => μ.isCaratheodory_iff_le.2 fun s => _ set S : ℕ → Set X := fun n => {x ∈ s | (↑n)⁻¹ ≤ infEdist x t} - have n0 : ∀ {n : ℕ}, (n⁻¹ : ℝ≥0∞) ≠ 0 := fun {n} => ENNReal.inv_ne_zero.2 (ENNReal.nat_ne_top _) - have Ssep : ∀ n, IsMetricSeparated (S n) t := fun n => - ⟨n⁻¹, n0, fun x hx y hy => hx.2.trans <| infEdist_le_edist_of_mem hy⟩ + have Ssep (n) : IsMetricSeparated (S n) t := + ⟨n⁻¹, ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _), + fun x hx y hy ↦ hx.2.trans <| infEdist_le_edist_of_mem hy⟩ have Ssep' : ∀ n, IsMetricSeparated (S n) (s ∩ t) := fun n => (Ssep n).mono Subset.rfl (inter_subset_right _ _) have S_sub : ∀ n, S n ⊆ s \ t := fun n => @@ -974,7 +974,7 @@ theorem hausdorffMeasure_pi_real {ι : Type*} [Fintype ι] : intro f refine' diam_pi_le_of_le fun b => _ simp only [Real.ediam_Icc, add_div, ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr hn), le_refl, - add_sub_add_left_eq_sub, add_sub_cancel_left, ENNReal.ofReal_one, ENNReal.ofReal_coe_nat] + add_sub_add_left_eq_sub, add_sub_cancel_left, ENNReal.ofReal_one, ENNReal.ofReal_natCast] have C : ∀ᶠ n in atTop, (Set.pi univ fun i : ι => Ioo (a i : ℝ) (b i)) ⊆ ⋃ i : γ n, t n i := by refine' eventually_atTop.2 ⟨1, fun n hn => _⟩ have npos : (0 : ℝ) < n := Nat.cast_pos.2 hn @@ -1025,7 +1025,7 @@ theorem hausdorffMeasure_pi_real {ι : Type*} [Fintype ι] : apply eventually_atTop.2 ⟨1, fun n hn => _⟩ intros n hn simp only [ENNReal.ofReal_div_of_pos (Nat.cast_pos.mpr hn), comp_apply, - ENNReal.ofReal_coe_nat] + ENNReal.ofReal_natCast] · simp only [ENNReal.ofReal_ne_top, Ne, not_false_iff] #align measure_theory.hausdorff_measure_pi_real MeasureTheory.hausdorffMeasure_pi_real diff --git a/Mathlib/NumberTheory/ClassNumber/Finite.lean b/Mathlib/NumberTheory/ClassNumber/Finite.lean index 42deeeffe74d6..a7447559198c0 100644 --- a/Mathlib/NumberTheory/ClassNumber/Finite.lean +++ b/Mathlib/NumberTheory/ClassNumber/Finite.lean @@ -69,8 +69,8 @@ theorem normBound_pos : 0 < normBound abv bS := by ext j k simp [h, DMatrix.zero_apply] simp only [normBound, Algebra.smul_def, eq_natCast] - refine' mul_pos (Int.coe_nat_pos.mpr (Nat.factorial_pos _)) _ - refine' pow_pos (mul_pos (Int.coe_nat_pos.mpr (Fintype.card_pos_iff.mpr ⟨i⟩)) _) _ + refine' mul_pos (Int.natCast_pos.mpr (Nat.factorial_pos _)) _ + refine' pow_pos (mul_pos (Int.natCast_pos.mpr (Fintype.card_pos_iff.mpr ⟨i⟩)) _) _ refine' lt_of_lt_of_le (abv.pos hijk) (Finset.le_max' _ _ _) exact Finset.mem_image.mpr ⟨⟨i, j, k⟩, Finset.mem_univ _, rfl⟩ #align class_group.norm_bound_pos ClassGroup.normBound_pos diff --git a/Mathlib/NumberTheory/DiophantineApproximation.lean b/Mathlib/NumberTheory/DiophantineApproximation.lean index 52080ae914d5f..f994834a34229 100644 --- a/Mathlib/NumberTheory/DiophantineApproximation.lean +++ b/Mathlib/NumberTheory/DiophantineApproximation.lean @@ -142,7 +142,7 @@ theorem exists_nat_abs_mul_sub_round_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) : obtain ⟨j, k, hk₀, hk₁, h⟩ := exists_int_int_abs_mul_sub_le ξ n_pos have hk := toNat_of_nonneg hk₀.le rw [← hk] at hk₀ hk₁ h - exact ⟨k.toNat, coe_nat_pos.mp hk₀, Nat.cast_le.mp hk₁, (round_le (↑k.toNat * ξ) j).trans h⟩ + exact ⟨k.toNat, natCast_pos.mp hk₀, Nat.cast_le.mp hk₁, (round_le (↑k.toNat * ξ) j).trans h⟩ #align real.exists_nat_abs_mul_sub_round_le Real.exists_nat_abs_mul_sub_round_le /-- *Dirichlet's approximation theorem:* @@ -156,7 +156,7 @@ theorem exists_rat_abs_sub_le_and_den_le (ξ : ℝ) {n : ℕ} (n_pos : 0 < n) : have hk₀' : (0 : ℝ) < k := Int.cast_pos.mpr hk₀ have hden : ((j / k : ℚ).den : ℤ) ≤ k := by convert le_of_dvd hk₀ (Rat.den_dvd j k) - exact Rat.coe_int_div_eq_divInt + exact Rat.intCast_div_eq_divInt refine' ⟨j / k, _, Nat.cast_le.mp (hden.trans hk₁)⟩ rw [← div_div, le_div_iff (Nat.cast_pos.mpr <| Rat.pos _ : (0 : ℝ) < _)] refine' (mul_le_mul_of_nonneg_left (Int.cast_le.mpr hden : _ ≤ (k : ℝ)) (abs_nonneg _)).trans _ diff --git a/Mathlib/NumberTheory/Liouville/Basic.lean b/Mathlib/NumberTheory/Liouville/Basic.lean index dfcc9558b8400..37a490a1f73cf 100644 --- a/Mathlib/NumberTheory/Liouville/Basic.lean +++ b/Mathlib/NumberTheory/Liouville/Basic.lean @@ -68,7 +68,7 @@ protected theorem irrational {x : ℝ} (h : Liouville x) : Irrational x := by rw [← Int.ofNat_mul, ← Int.coe_nat_pow, ← Int.ofNat_mul, Int.ofNat_lt] at a1 -- Recall this is by contradiction: we obtained the inequality `b * q ≤ x * q ^ (b + 1)`, so -- we are done. - exact not_le.mpr a1 (Nat.mul_lt_mul_pow_succ (Int.coe_nat_pos.mp ap) (Int.ofNat_lt.mp q1)).le + exact not_le.mpr a1 (Nat.mul_lt_mul_pow_succ (Int.natCast_pos.mp ap) (Int.ofNat_lt.mp q1)).le #align liouville.irrational Liouville.irrational open Polynomial Metric Set Real RingHom @@ -163,7 +163,7 @@ theorem exists_pos_real_of_irrational_root {α : ℝ} (ha : Irrational α) {f : rw [show (a + 1 : ℝ) = ((a + 1 : ℕ) : ℤ) by norm_cast] at hq ⊢ -- key observation: the right-hand side of the inequality is an *integer*. Therefore, -- if its absolute value is not at least one, then it vanishes. Proceed by contradiction - refine' one_le_pow_mul_abs_eval_div (Int.coe_nat_succ_pos a) fun hy => _ + refine' one_le_pow_mul_abs_eval_div (Int.natCast_succ_pos a) fun hy => _ -- As the evaluation of the polynomial vanishes, we found a root of `fR` that is rational. -- We know that `α` is the only root of `fR` in our interval, and `α` is irrational: -- follow your nose. diff --git a/Mathlib/NumberTheory/Liouville/Measure.lean b/Mathlib/NumberTheory/Liouville/Measure.lean index ef4f2a476b9b5..5c1a3d17263e2 100644 --- a/Mathlib/NumberTheory/Liouville/Measure.lean +++ b/Mathlib/NumberTheory/Liouville/Measure.lean @@ -96,7 +96,7 @@ theorem volume_iUnion_setOf_liouvilleWith : measure_biUnion_finset_le _ _ _ = ↑((b + 1) * (2 / (b : ℝ≥0) ^ r)) := by simp only [hB, Int.card_Icc, Finset.sum_const, nsmul_eq_mul, sub_zero, ← Int.ofNat_succ, - Int.toNat_natCast, ← Nat.cast_succ, ENNReal.coe_mul, ENNReal.coe_nat] + Int.toNat_natCast, ← Nat.cast_succ, ENNReal.coe_mul, ENNReal.coe_natCast] _ = _ := by have : 1 - r ≠ 0 := by linarith rw [ENNReal.coe_inj] diff --git a/Mathlib/NumberTheory/Liouville/Residual.lean b/Mathlib/NumberTheory/Liouville/Residual.lean index 630dc600688d1..45afc6d5b478e 100644 --- a/Mathlib/NumberTheory/Liouville/Residual.lean +++ b/Mathlib/NumberTheory/Liouville/Residual.lean @@ -69,7 +69,7 @@ theorem eventually_residual_liouville : ∀ᶠ x in residual ℝ, Liouville x := · convert @mem_ball_self ℝ _ (r : ℝ) _ _ · push_cast; norm_cast; simp [Rat.divInt_mul_right (two_ne_zero), Rat.mkRat_self] · refine' one_div_pos.2 (pow_pos (Int.cast_pos.2 _) _) - exact mul_pos (Int.coe_nat_pos.2 r.pos) zero_lt_two + exact mul_pos (Int.natCast_pos.2 r.pos) zero_lt_two #align eventually_residual_liouville eventually_residual_liouville /-- The set of Liouville numbers in dense. -/ diff --git a/Mathlib/NumberTheory/LucasLehmer.lean b/Mathlib/NumberTheory/LucasLehmer.lean index b20a94e4e673f..85e754bc9dec6 100644 --- a/Mathlib/NumberTheory/LucasLehmer.lean +++ b/Mathlib/NumberTheory/LucasLehmer.lean @@ -346,9 +346,12 @@ set_option linter.uppercaseLean3 false in #align lucas_lehmer.X.coe_mul LucasLehmer.X.coe_mul @[norm_cast] -theorem coe_nat (n : ℕ) : ((n : ℤ) : X q) = (n : X q) := by ext <;> simp +theorem coe_natCast (n : ℕ) : ((n : ℤ) : X q) = (n : X q) := by ext <;> simp set_option linter.uppercaseLean3 false in -#align lucas_lehmer.X.coe_nat LucasLehmer.X.coe_nat +#align lucas_lehmer.X.coe_nat LucasLehmer.X.coe_natCast + +-- 2024-04-05 +@[deprecated] alias coe_nat := coe_natCast /-- The cardinality of `X` is `q^2`. -/ theorem card_eq : Fintype.card (X q) = q ^ 2 := by diff --git a/Mathlib/NumberTheory/Multiplicity.lean b/Mathlib/NumberTheory/Multiplicity.lean index 6766bb3f60761..75a27c88535b7 100644 --- a/Mathlib/NumberTheory/Multiplicity.lean +++ b/Mathlib/NumberTheory/Multiplicity.lean @@ -226,7 +226,7 @@ theorem Int.pow_add_pow {x y : ℤ} (hxy : ↑p ∣ x + y) (hx : ¬↑p ∣ x) { theorem Nat.pow_sub_pow {x y : ℕ} (hxy : p ∣ x - y) (hx : ¬p ∣ x) (n : ℕ) : multiplicity p (x ^ n - y ^ n) = multiplicity p (x - y) + multiplicity p n := by obtain hyx | hyx := le_total y x - · iterate 2 rw [← Int.coe_nat_multiplicity] + · iterate 2 rw [← Int.natCast_multiplicity] rw [Int.ofNat_sub (Nat.pow_le_pow_left hyx n)] rw [← Int.natCast_dvd_natCast] at hxy hx rw [Int.natCast_sub hyx] at * @@ -239,7 +239,7 @@ theorem Nat.pow_sub_pow {x y : ℕ} (hxy : p ∣ x - y) (hx : ¬p ∣ x) (n : theorem Nat.pow_add_pow {x y : ℕ} (hxy : p ∣ x + y) (hx : ¬p ∣ x) {n : ℕ} (hn : Odd n) : multiplicity p (x ^ n + y ^ n) = multiplicity p (x + y) + multiplicity p n := by - iterate 2 rw [← Int.coe_nat_multiplicity] + iterate 2 rw [← Int.natCast_multiplicity] rw [← Int.natCast_dvd_natCast] at hxy hx push_cast at * exact Int.pow_add_pow hp hp1 hxy hx hn @@ -360,13 +360,13 @@ theorem Nat.two_pow_sub_pow {x y : ℕ} (hxy : 2 ∣ x - y) (hx : ¬2 ∣ x) {n multiplicity 2 (x ^ n - y ^ n) + 1 = multiplicity 2 (x + y) + multiplicity 2 (x - y) + multiplicity 2 n := by obtain hyx | hyx := le_total y x - · iterate 3 rw [← multiplicity.Int.coe_nat_multiplicity] + · iterate 3 rw [← multiplicity.Int.natCast_multiplicity] simp only [Int.ofNat_sub hyx, Int.ofNat_sub (pow_le_pow_left' hyx _), Int.ofNat_add, Int.coe_nat_pow] rw [← Int.natCast_dvd_natCast] at hx rw [← Int.natCast_dvd_natCast, Int.ofNat_sub hyx] at hxy convert Int.two_pow_sub_pow hxy hx hn using 2 - rw [← multiplicity.Int.coe_nat_multiplicity] + rw [← multiplicity.Int.natCast_multiplicity] rfl · simp only [Nat.sub_eq_zero_iff_le.mpr hyx, Nat.sub_eq_zero_iff_le.mpr (pow_le_pow_left' hyx n), multiplicity.zero, diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean index ac82237833311..a968f18f47ce9 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean @@ -429,14 +429,14 @@ theorem convexBodySum_volume : (fun hx => (convexBodySumFun_eq_zero_iff _).mp hx) (fun r x => le_of_eq (convexBodySumFun_smul r x)) zero_lt_one] simp_rw [mixedEmbedding.finrank, div_one, Gamma_nat_eq_factorial, ofReal_div_of_pos - (Nat.cast_pos.mpr (Nat.factorial_pos _)), Real.rpow_one, ofReal_coe_nat] + (Nat.cast_pos.mpr (Nat.factorial_pos _)), Real.rpow_one, ofReal_natCast] suffices ∫ x : E K, exp (-convexBodySumFun x) = (2:ℝ) ^ NrRealPlaces K * (π / 2) ^ NrComplexPlaces K by rw [this, convexBodySumFactor, ofReal_mul (by positivity), ofReal_pow zero_le_two, ofReal_pow (by positivity), ofReal_div_of_pos zero_lt_two, ofReal_ofNat, ← NNReal.coe_real_pi, ofReal_coe_nnreal, coe_div (Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero _)), coe_mul, coe_pow, coe_pow, coe_ofNat, coe_div two_ne_zero, - coe_ofNat, coe_nat] + coe_ofNat, coe_natCast] calc _ = (∫ x : {w : InfinitePlace K // IsReal w} → ℝ, ∏ w, exp (- ‖x w‖)) * (∫ x : {w : InfinitePlace K // IsComplex w} → ℂ, ∏ w, exp (- 2 * ‖x w‖)) := by diff --git a/Mathlib/NumberTheory/Padics/PadicIntegers.lean b/Mathlib/NumberTheory/Padics/PadicIntegers.lean index 9608008e5e8ab..1c7794cbc9cd4 100644 --- a/Mathlib/NumberTheory/Padics/PadicIntegers.lean +++ b/Mathlib/NumberTheory/Padics/PadicIntegers.lean @@ -182,10 +182,13 @@ instance : CharZero ℤ_[p] where cast_injective m n h := Nat.cast_injective (by rw [Subtype.ext_iff] at h; norm_cast at h) @[norm_cast] -- @[simp] -- Porting note: not in simpNF -theorem coe_int_eq (z1 z2 : ℤ) : (z1 : ℤ_[p]) = z2 ↔ z1 = z2 := by +theorem intCast_eq (z1 z2 : ℤ) : (z1 : ℤ_[p]) = z2 ↔ z1 = z2 := by suffices (z1 : ℚ_[p]) = z2 ↔ z1 = z2 from Iff.trans (by norm_cast) this norm_cast -#align padic_int.coe_int_eq PadicInt.coe_int_eq +#align padic_int.coe_int_eq PadicInt.intCast_eq + +-- 2024-04-05 +@[deprecated] alias coe_int_eq := intCast_eq /-- A sequence of integers that is Cauchy with respect to the `p`-adic norm converges to a `p`-adic integer. -/ diff --git a/Mathlib/NumberTheory/Padics/PadicVal.lean b/Mathlib/NumberTheory/Padics/PadicVal.lean index 676934bab7b77..92411a215b2b9 100644 --- a/Mathlib/NumberTheory/Padics/PadicVal.lean +++ b/Mathlib/NumberTheory/Padics/PadicVal.lean @@ -330,11 +330,11 @@ protected theorem defn (p : ℕ) [hp : Fact p.Prime] {q : ℚ} {n d : ℤ} (hqz rw [multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1), multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1)] rw [Nat.cast_add, Nat.cast_add] - simp_rw [Int.coe_nat_multiplicity p q.den] + simp_rw [Int.natCast_multiplicity p q.den] ring -- Porting note: was -- simp only [hc1, hc2, multiplicity.mul' (Nat.prime_iff_prime_int.1 hp.1), - -- hp.1.ne_one, hqz, pos_iff_ne_zero, Int.coe_nat_multiplicity p q.den + -- hp.1.ne_one, hqz, pos_iff_ne_zero, Int.natCast_multiplicity p q.den #align padic_val_rat.defn padicValRat.defn /-- A rewrite lemma for `padicValRat p (q * r)` with conditions `q ≠ 0`, `r ≠ 0`. -/ diff --git a/Mathlib/NumberTheory/Pell.lean b/Mathlib/NumberTheory/Pell.lean index 17ed604cadaa6..315af12f504fb 100644 --- a/Mathlib/NumberTheory/Pell.lean +++ b/Mathlib/NumberTheory/Pell.lean @@ -397,7 +397,7 @@ theorem exists_of_not_isSquare (h₀ : 0 < d) (hd : ¬IsSquare d) : obtain ⟨q, hq⟩ := hm.nonempty rw [mem_setOf, sub_eq_zero, mul_comm] at hq obtain ⟨a, ha⟩ := (Int.pow_dvd_pow_iff two_pos).mp ⟨d, hq⟩ - rw [ha, mul_pow, mul_right_inj' (pow_pos (Int.coe_nat_pos.mpr q.pos) 2).ne'] at hq + rw [ha, mul_pow, mul_right_inj' (pow_pos (Int.natCast_pos.mpr q.pos) 2).ne'] at hq exact hd ⟨a, sq a ▸ hq.symm⟩ haveI := neZero_iff.mpr (Int.natAbs_ne_zero.mpr hm₀) let f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q => (q.num, q.den) diff --git a/Mathlib/NumberTheory/PellMatiyasevic.lean b/Mathlib/NumberTheory/PellMatiyasevic.lean index 6928ab5e7831b..5c51b1a5e05fd 100644 --- a/Mathlib/NumberTheory/PellMatiyasevic.lean +++ b/Mathlib/NumberTheory/PellMatiyasevic.lean @@ -337,7 +337,7 @@ theorem eq_pellZd (b : ℤ√(d a1)) (b1 : 1 ≤ b) (hp : IsPell b) : ∃ n, b = let ⟨n, h⟩ := @Zsqrtd.le_arch (d a1) b eq_pell_lem a1 n b b1 hp <| h.trans <| by - rw [Zsqrtd.coe_nat_val] + rw [Zsqrtd.natCast_val] exact Zsqrtd.le_of_le_le (Int.ofNat_le_ofNat_of_le <| le_of_lt <| n_lt_xn _ _) (Int.ofNat_zero_le _) @@ -508,7 +508,7 @@ theorem dvd_of_ysq_dvd {n t} (h : yn a1 n * yn a1 n ∣ yn a1 t) : yn a1 n ∣ t theorem pellZd_succ_succ (n) : pellZd a1 (n + 2) + pellZd a1 n = (2 * a : ℕ) * pellZd a1 (n + 1) := by have : (1 : ℤ√(d a1)) + ⟨a, 1⟩ * ⟨a, 1⟩ = ⟨a, 1⟩ * (2 * a) := by - rw [Zsqrtd.coe_nat_val] + rw [Zsqrtd.natCast_val] change (⟨_, _⟩ : ℤ√(d a1)) = ⟨_, _⟩ rw [dz_val] dsimp [az] diff --git a/Mathlib/NumberTheory/SmoothNumbers.lean b/Mathlib/NumberTheory/SmoothNumbers.lean index 88a8a38f56a5b..cdd20e1de03e0 100644 --- a/Mathlib/NumberTheory/SmoothNumbers.lean +++ b/Mathlib/NumberTheory/SmoothNumbers.lean @@ -167,7 +167,7 @@ def equivProdNatSmoothNumbers {p : ℕ} (hp: p.Prime) : constructor · rw [factorization_mul (pos_iff_ne_zero.mp <| pos_pow_of_pos e hp.pos) hm₀] simp only [factorization_pow, Finsupp.coe_add, Finsupp.coe_smul, nsmul_eq_mul, - Pi.coe_nat, cast_id, Pi.add_apply, Pi.mul_apply, hp.factorization_self, + Pi.natCast_def, cast_id, Pi.add_apply, Pi.mul_apply, hp.factorization_self, mul_one, add_right_eq_self] rw [← factors_count_eq, count_eq_zero] exact fun H ↦ (hm p H).false diff --git a/Mathlib/NumberTheory/Zsqrtd/Basic.lean b/Mathlib/NumberTheory/Zsqrtd/Basic.lean index eeaa5a15dd9e9..1635ac1b4f6e1 100644 --- a/Mathlib/NumberTheory/Zsqrtd/Basic.lean +++ b/Mathlib/NumberTheory/Zsqrtd/Basic.lean @@ -273,43 +273,52 @@ instance nontrivial : Nontrivial (ℤ√d) := ⟨⟨0, 1, (Zsqrtd.ext_iff 0 1).not.mpr (by simp)⟩⟩ @[simp] -theorem coe_nat_re (n : ℕ) : (n : ℤ√d).re = n := +theorem natCast_re (n : ℕ) : (n : ℤ√d).re = n := rfl -#align zsqrtd.coe_nat_re Zsqrtd.coe_nat_re +#align zsqrtd.coe_nat_re Zsqrtd.natCast_re @[simp] theorem ofNat_re (n : ℕ) [n.AtLeastTwo] : (no_index (OfNat.ofNat n) : ℤ√d).re = n := rfl @[simp] -theorem coe_nat_im (n : ℕ) : (n : ℤ√d).im = 0 := +theorem natCast_im (n : ℕ) : (n : ℤ√d).im = 0 := rfl -#align zsqrtd.coe_nat_im Zsqrtd.coe_nat_im +#align zsqrtd.coe_nat_im Zsqrtd.natCast_im @[simp] theorem ofNat_im (n : ℕ) [n.AtLeastTwo] : (no_index (OfNat.ofNat n) : ℤ√d).im = 0 := rfl -theorem coe_nat_val (n : ℕ) : (n : ℤ√d) = ⟨n, 0⟩ := +theorem natCast_val (n : ℕ) : (n : ℤ√d) = ⟨n, 0⟩ := rfl -#align zsqrtd.coe_nat_val Zsqrtd.coe_nat_val +#align zsqrtd.coe_nat_val Zsqrtd.natCast_val @[simp] -theorem coe_int_re (n : ℤ) : (n : ℤ√d).re = n := by cases n <;> rfl -#align zsqrtd.coe_int_re Zsqrtd.coe_int_re +theorem intCast_re (n : ℤ) : (n : ℤ√d).re = n := by cases n <;> rfl +#align zsqrtd.coe_int_re Zsqrtd.intCast_re @[simp] -theorem coe_int_im (n : ℤ) : (n : ℤ√d).im = 0 := by cases n <;> rfl -#align zsqrtd.coe_int_im Zsqrtd.coe_int_im +theorem intCast_im (n : ℤ) : (n : ℤ√d).im = 0 := by cases n <;> rfl +#align zsqrtd.coe_int_im Zsqrtd.intCast_im -theorem coe_int_val (n : ℤ) : (n : ℤ√d) = ⟨n, 0⟩ := by ext <;> simp -#align zsqrtd.coe_int_val Zsqrtd.coe_int_val +theorem intCast_val (n : ℤ) : (n : ℤ√d) = ⟨n, 0⟩ := by ext <;> simp +#align zsqrtd.coe_int_val Zsqrtd.intCast_val instance : CharZero (ℤ√d) where cast_injective m n := by simp [Zsqrtd.ext_iff] @[simp] -theorem ofInt_eq_coe (n : ℤ) : (ofInt n : ℤ√d) = n := by ext <;> simp [ofInt_re, ofInt_im] -#align zsqrtd.of_int_eq_coe Zsqrtd.ofInt_eq_coe +theorem ofInt_eq_intCast (n : ℤ) : (ofInt n : ℤ√d) = n := by ext <;> simp [ofInt_re, ofInt_im] +#align zsqrtd.of_int_eq_coe Zsqrtd.ofInt_eq_intCast + +-- 2024-04-05 +@[deprecated] alias coe_nat_re := natCast_re +@[deprecated] alias coe_nat_im := natCast_im +@[deprecated] alias coe_nat_val := natCast_val +@[deprecated] alias coe_int_re := intCast_re +@[deprecated] alias coe_int_im := intCast_im +@[deprecated] alias coe_int_val := intCast_val +@[deprecated] alias ofInt_eq_coe := ofInt_eq_intCast @[simp] theorem smul_val (n x y : ℤ) : (n : ℤ√d) * ⟨x, y⟩ = ⟨n * x, n * y⟩ := by ext <;> simp @@ -359,8 +368,8 @@ protected theorem coe_int_inj {m n : ℤ} (h : (↑m : ℤ√d) = ↑n) : m = n theorem coe_int_dvd_iff (z : ℤ) (a : ℤ√d) : ↑z ∣ a ↔ z ∣ a.re ∧ z ∣ a.im := by constructor · rintro ⟨x, rfl⟩ - simp only [add_zero, coe_int_re, zero_mul, mul_im, dvd_mul_right, and_self_iff, - mul_re, mul_zero, coe_int_im] + simp only [add_zero, intCast_re, zero_mul, mul_im, dvd_mul_right, and_self_iff, + mul_re, mul_zero, intCast_im] · rintro ⟨⟨r, hr⟩, ⟨i, hi⟩⟩ use ⟨r, i⟩ rw [smul_val, Zsqrtd.ext_iff] @@ -372,8 +381,8 @@ theorem coe_int_dvd_coe_int (a b : ℤ) : (a : ℤ√d) ∣ b ↔ a ∣ b := by rw [coe_int_dvd_iff] constructor · rintro ⟨hre, -⟩ - rwa [coe_int_re] at hre - · rw [coe_int_re, coe_int_im] + rwa [intCast_re] at hre + · rw [intCast_re, intCast_im] exact fun hc => ⟨hc, dvd_zero a⟩ #align zsqrtd.coe_int_dvd_coe_int Zsqrtd.coe_int_dvd_coe_int @@ -1068,7 +1077,7 @@ theorem lift_injective [CharZero R] {d : ℤ} (r : { r : R // r * r = ↑d }) (injective_iff_map_eq_zero (lift r)).mpr fun a ha => by have h_inj : Function.Injective ((↑) : ℤ → R) := Int.cast_injective suffices lift r a.norm = 0 by - simp only [coe_int_re, add_zero, lift_apply_apply, coe_int_im, Int.cast_zero, + simp only [intCast_re, add_zero, lift_apply_apply, intCast_im, Int.cast_zero, zero_mul] at this rwa [← Int.cast_zero, h_inj.eq_iff, norm_eq_zero hd] at this rw [norm_eq_mul_conj, RingHom.map_mul, ha, zero_mul] diff --git a/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean b/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean index ad529e2fa6e1e..526e95749de7a 100644 --- a/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean +++ b/Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean @@ -170,13 +170,16 @@ theorem norm_pos {x : ℤ[i]} : 0 < norm x ↔ x ≠ 0 := by rw [lt_iff_le_and_ne, Ne, eq_comm, norm_eq_zero]; simp [norm_nonneg] #align gaussian_int.norm_pos GaussianInt.norm_pos -theorem abs_coe_nat_norm (x : ℤ[i]) : (x.norm.natAbs : ℤ) = x.norm := +theorem abs_natCast_norm (x : ℤ[i]) : (x.norm.natAbs : ℤ) = x.norm := Int.natAbs_of_nonneg (norm_nonneg _) -#align gaussian_int.abs_coe_nat_norm GaussianInt.abs_coe_nat_norm +#align gaussian_int.abs_coe_nat_norm GaussianInt.abs_natCast_norm + +-- 2024-04-05 +@[deprecated] alias abs_coe_nat_norm := abs_natCast_norm @[simp] theorem nat_cast_natAbs_norm {α : Type*} [Ring α] (x : ℤ[i]) : (x.norm.natAbs : α) = x.norm := by - rw [← Int.cast_natCast, abs_coe_nat_norm] + rw [← Int.cast_natCast, abs_natCast_norm] #align gaussian_int.nat_cast_nat_abs_norm GaussianInt.nat_cast_natAbs_norm theorem natAbs_norm_eq (x : ℤ[i]) : @@ -258,7 +261,7 @@ theorem norm_le_norm_mul_left (x : ℤ[i]) {y : ℤ[i]} (hy : y ≠ 0) : (norm x).natAbs ≤ (norm (x * y)).natAbs := by rw [Zsqrtd.norm_mul, Int.natAbs_mul] exact le_mul_of_one_le_right (Nat.zero_le _) (Int.ofNat_le.1 (by - rw [abs_coe_nat_norm] + rw [abs_natCast_norm] exact Int.add_one_le_of_lt (norm_pos.2 hy))) #align gaussian_int.norm_le_norm_mul_left GaussianInt.norm_le_norm_mul_left diff --git a/Mathlib/Order/Filter/Germ.lean b/Mathlib/Order/Filter/Germ.lean index 668323e008fb4..eb31d9e9754b5 100644 --- a/Mathlib/Order/Filter/Germ.lean +++ b/Mathlib/Order/Filter/Germ.lean @@ -485,7 +485,7 @@ instance natCast [NatCast M] : NatCast (Germ l M) where natCast n := (n : α → M) @[simp] -theorem coe_nat [NatCast M] (n : ℕ) : ((fun _ ↦ n : α → M) : Germ l M) = n := rfl +theorem natCast_def [NatCast M] (n : ℕ) : ((fun _ ↦ n : α → M) : Germ l M) = n := rfl @[simp, norm_cast] theorem const_nat [NatCast M] (n : ℕ) : ((n : M) : Germ l M) = n := rfl @@ -506,7 +506,11 @@ instance intCast [IntCast M] : IntCast (Germ l M) where intCast n := (n : α → M) @[simp] -theorem coe_int [IntCast M] (n : ℤ) : ((fun _ ↦ n : α → M) : Germ l M) = n := rfl +theorem intCast_def [IntCast M] (n : ℤ) : ((fun _ ↦ n : α → M) : Germ l M) = n := rfl + +-- 2024-04-05 +@[deprecated] alias coe_nat := natCast_def +@[deprecated] alias coe_int := intCast_def instance addMonoidWithOne [AddMonoidWithOne M] : AddMonoidWithOne (Germ l M) := { natCast, addMonoid, one with diff --git a/Mathlib/Probability/Distributions/Uniform.lean b/Mathlib/Probability/Distributions/Uniform.lean index 28bf3f5bac0c6..7461cce657d06 100644 --- a/Mathlib/Probability/Distributions/Uniform.lean +++ b/Mathlib/Probability/Distributions/Uniform.lean @@ -231,7 +231,7 @@ def uniformOfFinset (s : Finset α) (hs : s.Nonempty) : PMF α := by have : (s.card : ℝ≥0∞) ≠ 0 := by simpa only [Ne, Nat.cast_eq_zero, Finset.card_eq_zero] using Finset.nonempty_iff_ne_empty.1 hs - exact ENNReal.mul_inv_cancel this <| ENNReal.nat_ne_top s.card + exact ENNReal.mul_inv_cancel this <| ENNReal.natCast_ne_top s.card · exact fun x hx => by simp only [hx, if_false] #align pmf.uniform_of_finset PMF.uniformOfFinset @@ -357,7 +357,7 @@ def ofMultiset (s : Multiset α) (hs : s ≠ 0) : PMF α := _ = 1 := by rw [← Nat.cast_sum, Multiset.toFinset_sum_count_eq s, ENNReal.inv_mul_cancel (Nat.cast_ne_zero.2 (hs ∘ Multiset.card_eq_zero.1)) - (ENNReal.nat_ne_top _)] + (ENNReal.natCast_ne_top _)] )⟩ #align pmf.of_multiset PMF.ofMultiset @@ -379,7 +379,7 @@ theorem mem_support_ofMultiset_iff (a : α) : a ∈ (ofMultiset s hs).support theorem ofMultiset_apply_of_not_mem {a : α} (ha : a ∉ s) : ofMultiset s hs a = 0 := by simpa only [ofMultiset_apply, ENNReal.div_eq_zero_iff, Nat.cast_eq_zero, Multiset.count_eq_zero, - ENNReal.nat_ne_top, or_false_iff] using ha + ENNReal.natCast_ne_top, or_false_iff] using ha #align pmf.of_multiset_apply_of_not_mem PMF.ofMultiset_apply_of_not_mem section Measure diff --git a/Mathlib/Probability/Kernel/WithDensity.lean b/Mathlib/Probability/Kernel/WithDensity.lean index 6c694f321027d..c5cb16866d362 100644 --- a/Mathlib/Probability/Kernel/WithDensity.lean +++ b/Mathlib/Probability/Kernel/WithDensity.lean @@ -219,7 +219,7 @@ theorem isSFiniteKernel_withDensity_of_isFiniteKernel (κ : kernel α β) [IsFin have : (f a b).toReal ≤ n := Nat.le_of_ceil_le hn rw [← ENNReal.le_ofReal_iff_toReal_le (hf_ne_top a b) _] at this · refine' this.trans (le_of_eq _) - rw [ENNReal.ofReal_coe_nat] + rw [ENNReal.ofReal_natCast] · norm_cast exact zero_le _ have h_zero : ∀ a b n, ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0 := by diff --git a/Mathlib/Probability/Martingale/OptionalStopping.lean b/Mathlib/Probability/Martingale/OptionalStopping.lean index 872c4f3198074..16c6b4f5c679e 100644 --- a/Mathlib/Probability/Martingale/OptionalStopping.lean +++ b/Mathlib/Probability/Martingale/OptionalStopping.lean @@ -186,7 +186,7 @@ theorem maximal_ineq [IsFiniteMeasure μ] (hsub : Submartingale f 𝒢 μ) (hnon intro ω hω rw [Set.mem_setOf_eq] at hω have : hitting f {y : ℝ | ↑ε ≤ y} 0 n ω = n := by - classical simp only [hitting, Set.mem_setOf_eq, exists_prop, Pi.coe_nat, Nat.cast_id, + classical simp only [hitting, Set.mem_setOf_eq, exists_prop, Pi.natCast_def, Nat.cast_id, ite_eq_right_iff, forall_exists_index, and_imp] intro m hm hεm exact False.elim diff --git a/Mathlib/Probability/Martingale/Upcrossing.lean b/Mathlib/Probability/Martingale/Upcrossing.lean index 4ff99d584b2d8..a1261d374b54d 100644 --- a/Mathlib/Probability/Martingale/Upcrossing.lean +++ b/Mathlib/Probability/Martingale/Upcrossing.lean @@ -843,9 +843,9 @@ theorem upcrossings_lt_top_iff : constructor <;> rintro ⟨k, hk⟩ · obtain ⟨m, hm⟩ := exists_nat_ge k refine' ⟨m, fun N => Nat.cast_le.1 ((hk N).trans _)⟩ - rwa [← ENNReal.coe_nat, ENNReal.coe_le_coe] + rwa [← ENNReal.coe_natCast, ENNReal.coe_le_coe] · refine' ⟨k, fun N => _⟩ - simp only [ENNReal.coe_nat, Nat.cast_le, hk N] + simp only [ENNReal.coe_natCast, Nat.cast_le, hk N] #align measure_theory.upcrossings_lt_top_iff MeasureTheory.upcrossings_lt_top_iff /-- A variant of Doob's upcrossing estimate obtained by taking the supremum on both sides. -/ diff --git a/Mathlib/RingTheory/Derivation/Basic.lean b/Mathlib/RingTheory/Derivation/Basic.lean index 7f20160654156..edb00623fcbb8 100644 --- a/Mathlib/RingTheory/Derivation/Basic.lean +++ b/Mathlib/RingTheory/Derivation/Basic.lean @@ -148,9 +148,9 @@ theorem map_algebraMap : D (algebraMap R A r) = 0 := by #align derivation.map_algebra_map Derivation.map_algebraMap @[simp] -theorem map_coe_nat (n : ℕ) : D (n : A) = 0 := by +theorem map_natCast (n : ℕ) : D (n : A) = 0 := by rw [← nsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero] -#align derivation.map_coe_nat Derivation.map_coe_nat +#align derivation.map_coe_nat Derivation.map_natCast @[simp] theorem leibniz_pow (n : ℕ) : D (a ^ n) = n • a ^ (n - 1) • D a := by @@ -395,9 +395,13 @@ protected theorem map_sub : D (a - b) = D a - D b := #align derivation.map_sub Derivation.map_sub @[simp] -theorem map_coe_int (n : ℤ) : D (n : A) = 0 := by +theorem map_intCast (n : ℤ) : D (n : A) = 0 := by rw [← zsmul_one, D.map_smul_of_tower n, map_one_eq_zero, smul_zero] -#align derivation.map_coe_int Derivation.map_coe_int +#align derivation.map_coe_int Derivation.map_intCast + +-- 2024-04-05 +@[deprecated] alias map_coe_nat := map_natCast +@[deprecated] alias map_coe_int := map_intCast theorem leibniz_of_mul_eq_one {a b : A} (h : a * b = 1) : D a = -a ^ 2 • D b := by rw [neg_smul] diff --git a/Mathlib/RingTheory/Localization/Away/Basic.lean b/Mathlib/RingTheory/Localization/Away/Basic.lean index c5a4756e5fce2..dd663bc3e3b31 100644 --- a/Mathlib/RingTheory/Localization/Away/Basic.lean +++ b/Mathlib/RingTheory/Localization/Away/Basic.lean @@ -189,9 +189,9 @@ theorem selfZPow_of_nonneg {n : ℤ} (hn : 0 ≤ n) : selfZPow x B n = algebraMa #align self_zpow_of_nonneg selfZPow_of_nonneg @[simp] -theorem selfZPow_coe_nat (d : ℕ) : selfZPow x B d = algebraMap R B x ^ d := +theorem selfZPow_natCast (d : ℕ) : selfZPow x B d = algebraMap R B x ^ d := selfZPow_of_nonneg _ _ (Int.natCast_nonneg d) -#align self_zpow_coe_nat selfZPow_coe_nat +#align self_zpow_coe_nat selfZPow_natCast @[simp] theorem selfZPow_zero : selfZPow x B 0 = 1 := by @@ -211,20 +211,25 @@ theorem selfZPow_of_nonpos {n : ℤ} (hn : n ≤ 0) : #align self_zpow_of_nonpos selfZPow_of_nonpos @[simp] -theorem selfZPow_neg_coe_nat (d : ℕ) : selfZPow x B (-d) = mk' _ (1 : R) (Submonoid.pow x d) := by +theorem selfZPow_neg_natCast (d : ℕ) : selfZPow x B (-d) = mk' _ (1 : R) (Submonoid.pow x d) := by simp [selfZPow_of_nonpos _ _ (neg_nonpos.mpr (Int.natCast_nonneg d))] -#align self_zpow_neg_coe_nat selfZPow_neg_coe_nat +#align self_zpow_neg_coe_nat selfZPow_neg_natCast @[simp] -theorem selfZPow_sub_cast_nat {n m : ℕ} : +theorem selfZPow_sub_natCast {n m : ℕ} : selfZPow x B (n - m) = mk' _ (x ^ n) (Submonoid.pow x m) := by by_cases h : m ≤ n · rw [IsLocalization.eq_mk'_iff_mul_eq, Submonoid.pow_apply, Subtype.coe_mk, ← Int.ofNat_sub h, - selfZPow_coe_nat, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel h] - · rw [← neg_sub, ← Int.ofNat_sub (le_of_not_le h), selfZPow_neg_coe_nat, + selfZPow_natCast, ← map_pow, ← map_mul, ← pow_add, Nat.sub_add_cancel h] + · rw [← neg_sub, ← Int.ofNat_sub (le_of_not_le h), selfZPow_neg_natCast, IsLocalization.mk'_eq_iff_eq] simp [Submonoid.pow_apply, ← pow_add, Nat.sub_add_cancel (le_of_not_le h)] -#align self_zpow_sub_cast_nat selfZPow_sub_cast_nat +#align self_zpow_sub_cast_nat selfZPow_sub_natCast + +-- 2024-04-05 +@[deprecated] alias selfZPow_coe_nat := selfZPow_natCast +@[deprecated] alias selfZPow_neg_coe_nat := selfZPow_neg_natCast +@[deprecated] alias selfZPow_sub_cast_nat := selfZPow_sub_natCast @[simp] theorem selfZPow_add {n m : ℤ} : selfZPow x B (n + m) = selfZPow x B n * selfZPow x B m := by @@ -233,11 +238,11 @@ theorem selfZPow_add {n m : ℤ} : selfZPow x B (n + m) = selfZPow x B n * selfZ selfZPow_of_nonneg _ _ (add_nonneg hn hm), Int.natAbs_add_of_nonneg hn hm, pow_add] · have : n + m = n.natAbs - m.natAbs := by rw [Int.natAbs_of_nonneg hn, Int.ofNat_natAbs_of_nonpos hm.le, sub_neg_eq_add] - rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_neg _ _ hm, this, selfZPow_sub_cast_nat, + rw [selfZPow_of_nonneg _ _ hn, selfZPow_of_neg _ _ hm, this, selfZPow_sub_natCast, IsLocalization.mk'_eq_mul_mk'_one, map_pow] · have : n + m = m.natAbs - n.natAbs := by rw [Int.natAbs_of_nonneg hm, Int.ofNat_natAbs_of_nonpos hn.le, sub_neg_eq_add, add_comm] - rw [selfZPow_of_nonneg _ _ hm, selfZPow_of_neg _ _ hn, this, selfZPow_sub_cast_nat, + rw [selfZPow_of_nonneg _ _ hm, selfZPow_of_neg _ _ hn, this, selfZPow_sub_natCast, IsLocalization.mk'_eq_mul_mk'_one, map_pow, mul_comm] · rw [selfZPow_of_neg _ _ hn, selfZPow_of_neg _ _ hm, selfZPow_of_neg _ _ (add_neg hn hm), Int.natAbs_add_of_nonpos hn.le hm.le, ← mk'_mul, one_mul] @@ -300,7 +305,7 @@ theorem exists_reduced_fraction' {b : B} (hb : b ≠ 0) (hx : Irreducible x) : simp only [← hy] at H obtain ⟨m, a, hyp1, hyp2⟩ := WfDvdMonoid.max_power_factor ha₀ hx refine' ⟨a, m - d, _⟩ - rw [← mk'_one (M := Submonoid.powers x) B, selfZPow_pow_sub, selfZPow_coe_nat, selfZPow_coe_nat, + rw [← mk'_one (M := Submonoid.powers x) B, selfZPow_pow_sub, selfZPow_natCast, selfZPow_natCast, ← map_pow _ _ d, mul_comm _ b, H, hyp2, map_mul, map_pow _ _ m] exact ⟨hyp1, congr_arg _ (IsLocalization.mk'_one _ _)⟩ #align exists_reduced_fraction' exists_reduced_fraction' diff --git a/Mathlib/RingTheory/Multiplicity.lean b/Mathlib/RingTheory/Multiplicity.lean index aa7fb253f6ed4..304253001a00c 100644 --- a/Mathlib/RingTheory/Multiplicity.lean +++ b/Mathlib/RingTheory/Multiplicity.lean @@ -64,7 +64,7 @@ theorem not_dvd_one_of_finite_one_right {a : α} : Finite a 1 → ¬a ∣ 1 := f #align multiplicity.not_dvd_one_of_finite_one_right multiplicity.not_dvd_one_of_finite_one_right @[norm_cast] -theorem Int.coe_nat_multiplicity (a b : ℕ) : multiplicity (a : ℤ) (b : ℤ) = multiplicity a b := by +theorem Int.natCast_multiplicity (a b : ℕ) : multiplicity (a : ℤ) (b : ℤ) = multiplicity a b := by apply Part.ext' · rw [← @finite_iff_dom ℕ, @finite_def ℕ, ← @finite_iff_dom ℤ, @finite_def ℤ] norm_cast @@ -73,7 +73,10 @@ theorem Int.coe_nat_multiplicity (a b : ℕ) : multiplicity (a : ℤ) (b : ℤ) · apply Nat.find_mono norm_cast simp -#align multiplicity.int.coe_nat_multiplicity multiplicity.Int.coe_nat_multiplicity +#align multiplicity.int.coe_nat_multiplicity multiplicity.Int.natCast_multiplicity + +-- 2024-04-05 +@[deprecated] alias Int.coe_nat_multiplicity := Int.natCast_multiplicity theorem not_finite_iff_forall {a b : α} : ¬Finite a b ↔ ∀ n : ℕ, a ^ n ∣ b := ⟨fun h n => @@ -434,8 +437,8 @@ protected theorem neg (a b : α) : multiplicity a (-b) = multiplicity a b := theorem Int.natAbs (a : ℕ) (b : ℤ) : multiplicity a b.natAbs = multiplicity (a : ℤ) b := by cases' Int.natAbs_eq b with h h <;> conv_rhs => rw [h] - · rw [Int.coe_nat_multiplicity] - · rw [multiplicity.neg, Int.coe_nat_multiplicity] + · rw [Int.natCast_multiplicity] + · rw [multiplicity.neg, Int.natCast_multiplicity] #align multiplicity.int.nat_abs multiplicity.Int.natAbs theorem multiplicity_add_of_gt {p a b : α} (h : multiplicity p b < multiplicity p a) : diff --git a/Mathlib/RingTheory/Polynomial/Bernstein.lean b/Mathlib/RingTheory/Polynomial/Bernstein.lean index 204d03afebeaf..dbf8ad2b05751 100644 --- a/Mathlib/RingTheory/Polynomial/Bernstein.lean +++ b/Mathlib/RingTheory/Polynomial/Bernstein.lean @@ -328,7 +328,7 @@ theorem sum_smul (n : ℕ) : refine' Finset.sum_congr rfl fun k _ => (w k).trans _ simp only [x, y, e, pderiv_true_x, pderiv_true_y, Algebra.id.smul_eq_mul, nsmul_eq_mul, Bool.cond_true, Bool.cond_false, add_zero, mul_one, mul_zero, smul_zero, MvPolynomial.aeval_X, - MvPolynomial.pderiv_mul, Derivation.leibniz_pow, Derivation.map_coe_nat, map_natCast, map_pow, + MvPolynomial.pderiv_mul, Derivation.leibniz_pow, Derivation.map_natCast, map_natCast, map_pow, map_mul] · rw [(pderiv true).leibniz_pow, (pderiv true).map_add, pderiv_true_x, pderiv_true_y] simp only [x, y, e, Algebra.id.smul_eq_mul, nsmul_eq_mul, map_natCast, map_pow, map_add, @@ -369,10 +369,10 @@ theorem sum_mul_smul (n : ℕ) : simp only [x, y, e, pderiv_true_x, pderiv_true_y, Algebra.id.smul_eq_mul, nsmul_eq_mul, Bool.cond_true, Bool.cond_false, add_zero, zero_add, mul_zero, smul_zero, mul_one, MvPolynomial.aeval_X, MvPolynomial.pderiv_X_self, MvPolynomial.pderiv_X_of_ne, - Derivation.leibniz_pow, Derivation.leibniz, Derivation.map_coe_nat, map_natCast, map_pow, + Derivation.leibniz_pow, Derivation.leibniz, Derivation.map_natCast, map_natCast, map_pow, map_mul, map_add] -- On the right hand side, we'll just simplify. - · simp only [x, y, e, pderiv_one, pderiv_mul, (pderiv _).leibniz_pow, (pderiv _).map_coe_nat, + · simp only [x, y, e, pderiv_one, pderiv_mul, (pderiv _).leibniz_pow, (pderiv _).map_natCast, (pderiv true).map_add, pderiv_true_x, pderiv_true_y, Algebra.id.smul_eq_mul, add_zero, mul_one, Derivation.map_smul_of_tower, map_nsmul, map_pow, map_add, Bool.cond_true, Bool.cond_false, MvPolynomial.aeval_X, add_sub_cancel, one_pow, smul_smul, diff --git a/Mathlib/RingTheory/Subring/Basic.lean b/Mathlib/RingTheory/Subring/Basic.lean index ef9cf75b8d25a..860ec86deac32 100644 --- a/Mathlib/RingTheory/Subring/Basic.lean +++ b/Mathlib/RingTheory/Subring/Basic.lean @@ -87,13 +87,16 @@ instance (priority := 100) SubringClass.addSubgroupClass (S : Type*) (R : Type u variable [SetLike S R] [hSR : SubringClass S R] (s : S) @[aesop safe apply (rule_sets := [SetLike])] -theorem coe_int_mem (n : ℤ) : (n : R) ∈ s := by simp only [← zsmul_one, zsmul_mem, one_mem] -#align coe_int_mem coe_int_mem +theorem intCast_mem (n : ℤ) : (n : R) ∈ s := by simp only [← zsmul_one, zsmul_mem, one_mem] +#align coe_int_mem intCast_mem + +-- 2024-04-05 +@[deprecated _root_.intCast_mem] alias coe_int_mem := intCast_mem namespace SubringClass instance (priority := 75) toHasIntCast : IntCast s := - ⟨fun n => ⟨n, coe_int_mem s n⟩⟩ + ⟨fun n => ⟨n, intCast_mem s n⟩⟩ #align subring_class.to_has_int_cast SubringClass.toHasIntCast -- Prefer subclasses of `Ring` over subclasses of `SubringClass`. @@ -705,7 +708,7 @@ instance : CompleteLattice (Subring R) := bot := ⊥ bot_le := fun s _x hx => let ⟨n, hn⟩ := mem_bot.1 hx - hn ▸ coe_int_mem s n + hn ▸ intCast_mem s n top := ⊤ le_top := fun _s _x _hx => trivial inf := (· ⊓ ·) diff --git a/Mathlib/RingTheory/Subsemiring/Basic.lean b/Mathlib/RingTheory/Subsemiring/Basic.lean index c7d4953501466..558de99bf8052 100644 --- a/Mathlib/RingTheory/Subsemiring/Basic.lean +++ b/Mathlib/RingTheory/Subsemiring/Basic.lean @@ -41,6 +41,10 @@ variable {S R : Type*} [AddMonoidWithOne R] [SetLike S R] (s : S) theorem natCast_mem [AddSubmonoidWithOneClass S R] (n : ℕ) : (n : R) ∈ s := by induction n <;> simp [zero_mem, add_mem, one_mem, *] #align nat_cast_mem natCast_mem +#align coe_nat_mem natCast_mem + +-- 2024-04-05 +@[deprecated] alias coe_nat_mem := natCast_mem @[aesop safe apply (rule_sets := [SetLike])] lemma ofNat_mem [AddSubmonoidWithOneClass S R] (s : S) (n : ℕ) [n.AtLeastTwo] : @@ -77,11 +81,6 @@ instance (priority := 100) SubsemiringClass.addSubmonoidWithOneClass (S : Type*) variable [SetLike S R] [hSR : SubsemiringClass S R] (s : S) -theorem coe_nat_mem (n : ℕ) : (n : R) ∈ s := by - rw [← nsmul_one] - exact nsmul_mem (one_mem _) _ -#align coe_nat_mem coe_nat_mem - namespace SubsemiringClass -- Prefer subclasses of `NonAssocSemiring` over subclasses of `SubsemiringClass`. @@ -617,7 +616,7 @@ instance : CompleteLattice (Subsemiring R) := bot := ⊥ bot_le := fun s _ hx => let ⟨n, hn⟩ := mem_bot.1 hx - hn ▸ coe_nat_mem s n + hn ▸ natCast_mem s n top := ⊤ le_top := fun _ _ _ => trivial inf := (· ⊓ ·) diff --git a/Mathlib/RingTheory/WittVector/Basic.lean b/Mathlib/RingTheory/WittVector/Basic.lean index 2f509130b48ce..9b1c34b48e9e1 100644 --- a/Mathlib/RingTheory/WittVector/Basic.lean +++ b/Mathlib/RingTheory/WittVector/Basic.lean @@ -194,7 +194,7 @@ private theorem ghostFun_add : ghostFun (x + y) = ghostFun x + ghostFun y := by private theorem ghostFun_nat_cast (i : ℕ) : ghostFun (i : 𝕎 R) = i := show ghostFun i.unaryCast = _ by induction i <;> - simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add, -Pi.coe_nat] + simp [*, Nat.unaryCast, ghostFun_zero, ghostFun_one, ghostFun_add, -Pi.natCast_def] private theorem ghostFun_sub : ghostFun (x - y) = ghostFun x - ghostFun y := by ghost_fun_tac X 0 - X 1, ![x.coeff, y.coeff] @@ -206,7 +206,8 @@ private theorem ghostFun_neg : ghostFun (-x) = -ghostFun x := by ghost_fun_tac - private theorem ghostFun_int_cast (i : ℤ) : ghostFun (i : 𝕎 R) = i := show ghostFun i.castDef = _ by - cases i <;> simp [*, Int.castDef, ghostFun_nat_cast, ghostFun_neg, -Pi.coe_nat, -Pi.coe_int] + cases i <;> simp [*, Int.castDef, ghostFun_nat_cast, ghostFun_neg, -Pi.natCast_def, + -Pi.intCast_def] private lemma ghostFun_nsmul (m : ℕ) (x : WittVector p R) : ghostFun (m • x) = m • ghostFun x := by -- porting note: I had to add the explicit type ascription. diff --git a/Mathlib/RingTheory/WittVector/Frobenius.lean b/Mathlib/RingTheory/WittVector/Frobenius.lean index f70191c8c1c59..698fcb78c7386 100644 --- a/Mathlib/RingTheory/WittVector/Frobenius.lean +++ b/Mathlib/RingTheory/WittVector/Frobenius.lean @@ -181,7 +181,7 @@ theorem map_frobeniusPoly (n : ℕ) : simp only [← RingHom.map_pow, ← C_mul] rw [C_inj] simp only [invOf_eq_inv, eq_intCast, inv_pow, Int.cast_natCast, Nat.cast_mul, Int.cast_mul] - rw [Rat.coe_nat_div _ _ (map_frobeniusPoly.key₁ p (n - i) j hj)] + rw [Rat.natCast_div _ _ (map_frobeniusPoly.key₁ p (n - i) j hj)] simp only [Nat.cast_pow, pow_add, pow_one] suffices (((p ^ (n - i)).choose (j + 1): ℚ) * (p : ℚ) ^ (j - v p ⟨j + 1, j.succ_pos⟩) * ↑p * (p ^ n : ℚ)) diff --git a/Mathlib/RingTheory/ZMod.lean b/Mathlib/RingTheory/ZMod.lean index 11193353a6b0a..d46c165ab9dd6 100644 --- a/Mathlib/RingTheory/ZMod.lean +++ b/Mathlib/RingTheory/ZMod.lean @@ -25,7 +25,7 @@ theorem isReduced_zmod {n : ℕ} : IsReduced (ZMod n) ↔ Squarefree n ∨ n = 0 rw [← RingHom.ker_isRadical_iff_reduced_of_surjective (ZMod.ringHom_surjective <| Int.castRingHom <| ZMod n), ZMod.ker_int_castRingHom, ← isRadical_iff_span_singleton, isRadical_iff_squarefree_or_zero, - Int.squarefree_coe_nat, Nat.cast_eq_zero] + Int.squarefree_natCast, Nat.cast_eq_zero] #align is_reduced_zmod isReduced_zmod instance {n : ℕ} [Fact <| Squarefree n] : IsReduced (ZMod n) := diff --git a/Mathlib/Tactic/Linarith/Preprocessing.lean b/Mathlib/Tactic/Linarith/Preprocessing.lean index 509ef6d171863..bea6ad85a47fd 100644 --- a/Mathlib/Tactic/Linarith/Preprocessing.lean +++ b/Mathlib/Tactic/Linarith/Preprocessing.lean @@ -139,7 +139,7 @@ partial def getNatComparisons (e : Expr) : List (Expr × Expr) := | _ => [] /-- If `e : ℕ`, returns a proof of `0 ≤ (e : C)`. -/ -def mk_coe_nat_nonneg_prf (p : Expr × Expr) : MetaM (Option Expr) := +def mk_natCast_nonneg_prf (p : Expr × Expr) : MetaM (Option Expr) := match p with | ⟨e, target⟩ => try commitIfNoEx (mkAppM ``nat_cast_nonneg #[target, e]) catch e => do @@ -185,7 +185,7 @@ def natToInt : GlobalBranchingPreprocessor where let (a, b) ← getRelSides (← inferType h) pure <| (es.insertList (getNatComparisons a)).insertList (getNatComparisons b) catch _ => pure es - pure [(g, ((← nonnegs.toList.filterMapM mk_coe_nat_nonneg_prf) ++ l : List Expr))] + pure [(g, ((← nonnegs.toList.filterMapM mk_natCast_nonneg_prf) ++ l : List Expr))] end natToInt diff --git a/Mathlib/Topology/EMetricSpace/Basic.lean b/Mathlib/Topology/EMetricSpace/Basic.lean index f0a2e2571454d..5d38a7551daac 100644 --- a/Mathlib/Topology/EMetricSpace/Basic.lean +++ b/Mathlib/Topology/EMetricSpace/Basic.lean @@ -265,7 +265,7 @@ theorem uniformity_basis_edist_nnreal_le : theorem uniformity_basis_edist_inv_nat : (𝓤 α).HasBasis (fun _ => True) fun n : ℕ => { p : α × α | edist p.1 p.2 < (↑n)⁻¹ } := - EMetric.mk_uniformity_basis (fun n _ => ENNReal.inv_pos.2 <| ENNReal.nat_ne_top n) fun _ε ε₀ => + EMetric.mk_uniformity_basis (fun n _ ↦ ENNReal.inv_pos.2 <| ENNReal.natCast_ne_top n) fun _ε ε₀ ↦ let ⟨n, hn⟩ := ENNReal.exists_inv_nat_lt (ne_of_gt ε₀) ⟨n, trivial, le_of_lt hn⟩ #align uniformity_basis_edist_inv_nat uniformity_basis_edist_inv_nat diff --git a/Mathlib/Topology/Instances/Complex.lean b/Mathlib/Topology/Instances/Complex.lean index 10d02dca4a33c..43c75d4eb0234 100644 --- a/Mathlib/Topology/Instances/Complex.lean +++ b/Mathlib/Topology/Instances/Complex.lean @@ -35,7 +35,7 @@ theorem Complex.subfield_eq_of_closed {K : Subfield ℂ} (hc : IsClosed (K : Set rw [← IsClosed.closure_eq hc] apply closure_mono rintro _ ⟨_, rfl⟩ - simp only [Function.comp_apply, ofReal_rat_cast, SetLike.mem_coe, SubfieldClass.coe_rat_mem] + simp only [Function.comp_apply, ofReal_rat_cast, SetLike.mem_coe, SubfieldClass.ratCast_mem] nth_rw 1 [range_comp] refine' subset_trans _ (image_closure_subset_closure_image continuous_ofReal) rw [DenseRange.closure_range Rat.denseEmbedding_coe_real.dense] diff --git a/Mathlib/Topology/Instances/ENNReal.lean b/Mathlib/Topology/Instances/ENNReal.lean index 576fe73a8b95e..bd05a6306f358 100644 --- a/Mathlib/Topology/Instances/ENNReal.lean +++ b/Mathlib/Topology/Instances/ENNReal.lean @@ -175,9 +175,9 @@ theorem tendsto_nhds_top_iff_nnreal {m : α → ℝ≥0∞} {f : Filter α} : theorem tendsto_nhds_top_iff_nat {m : α → ℝ≥0∞} {f : Filter α} : Tendsto m f (𝓝 ∞) ↔ ∀ n : ℕ, ∀ᶠ a in f, ↑n < m a := tendsto_nhds_top_iff_nnreal.trans - ⟨fun h n => by simpa only [ENNReal.coe_nat] using h n, fun h x => + ⟨fun h n => by simpa only [ENNReal.coe_natCast] using h n, fun h x => let ⟨n, hn⟩ := exists_nat_gt x - (h n).mono fun y => lt_trans <| by rwa [← ENNReal.coe_nat, coe_lt_coe]⟩ + (h n).mono fun y => lt_trans <| by rwa [← ENNReal.coe_natCast, coe_lt_coe]⟩ #align ennreal.tendsto_nhds_top_iff_nat ENNReal.tendsto_nhds_top_iff_nat theorem tendsto_nhds_top {m : α → ℝ≥0∞} {f : Filter α} (h : ∀ n : ℕ, ∀ᶠ a in f, ↑n < m a) : diff --git a/Mathlib/Topology/MetricSpace/HausdorffDimension.lean b/Mathlib/Topology/MetricSpace/HausdorffDimension.lean index 7d9751354832e..6aa112930a9a2 100644 --- a/Mathlib/Topology/MetricSpace/HausdorffDimension.lean +++ b/Mathlib/Topology/MetricSpace/HausdorffDimension.lean @@ -518,7 +518,7 @@ theorem dimH_ball_pi (x : ι → ℝ) {r : ℝ} (hr : 0 < r) : cases isEmpty_or_nonempty ι · rwa [dimH_subsingleton, eq_comm, Nat.cast_eq_zero, Fintype.card_eq_zero_iff] exact fun x _ y _ => Subsingleton.elim x y - · rw [← ENNReal.coe_nat] + · rw [← ENNReal.coe_natCast] have : μH[Fintype.card ι] (Metric.ball x r) = ENNReal.ofReal ((2 * r) ^ Fintype.card ι) := by rw [hausdorffMeasure_pi_real, Real.volume_pi_ball _ hr] refine dimH_of_hausdorffMeasure_ne_zero_ne_top ?_ ?_ <;> rw [NNReal.coe_nat_cast, this]