From bf65d209ffe1a810aa8b391c5061c8f9edcf99e3 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Sun, 10 Nov 2024 11:58:45 -0800 Subject: [PATCH] fixes --- .../ContinuousFunctionalCalculus/Order.lean | 3 ++- .../Additive/PluenneckeRuzsa.lean | 8 +++---- Mathlib/Data/NNReal/Defs.lean | 6 +++-- Mathlib/Order/Hom/Lattice.lean | 2 +- Mathlib/Order/Interval/Finset/Box.lean | 5 ---- .../TensorProduct/MvPolynomial.lean | 23 +++++++++++++------ 6 files changed, 27 insertions(+), 20 deletions(-) diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean index bb02c5b46fae0..951f13526c752 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean @@ -267,9 +267,10 @@ lemma le_iff_norm_sqrt_mul_rpow {a b : A} (hbu : IsUnit b) (ha : 0 ≤ a) (hb : lift b to Aˣ using hbu have hbab : 0 ≤ (b : A) ^ (-(1 / 2) : ℝ) * a * (b : A) ^ (-(1 / 2) : ℝ) := conjugate_nonneg_of_nonneg ha rpow_nonneg + #adaptation_note /-- 2024-11-10 added `(R := A)` -/ conv_rhs => rw [← sq_le_one_iff (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self, star_mul, - IsSelfAdjoint.of_nonneg sqrt_nonneg, IsSelfAdjoint.of_nonneg rpow_nonneg, + IsSelfAdjoint.of_nonneg (R := A) sqrt_nonneg, IsSelfAdjoint.of_nonneg rpow_nonneg, ← mul_assoc, mul_assoc _ _ (sqrt a), sqrt_mul_sqrt_self a, CStarAlgebra.norm_le_one_iff_of_nonneg _ hbab] refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩ diff --git a/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean b/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean index 94e3ef08335bd..2ffee782c3d2e 100644 --- a/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean +++ b/Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean @@ -174,14 +174,14 @@ theorem ruzsa_triangle_inequality_mul_mul_mul (A B C : Finset G) : rw [mem_erase, mem_powerset, ← nonempty_iff_ne_empty] at hU refine cast_le.1 (?_ : (_ : ℚ≥0) ≤ _) push_cast - refine (le_div_iff₀ <| cast_pos.2 hB.card_pos).1 ?_ - rw [mul_div_right_comm, mul_comm _ B] + rw [← le_div_iff₀ (cast_pos.2 hB.card_pos), mul_div_right_comm, mul_comm _ B] refine (Nat.cast_le.2 <| card_le_card_mul_left _ hU.1).trans ?_ refine le_trans ?_ (mul_le_mul (hUA _ hB') (cast_le.2 <| card_le_card <| mul_subset_mul_right hU.2) (zero_le _) (zero_le _)) - rw [← mul_div_right_comm, ← mul_assoc] - refine (le_div_iff₀ <| cast_pos.2 hU.1.card_pos).2 ?_ + #adaptation_note /-- 2024-11-01 `le_div_iff₀` is synthesizing wrong `GroupWithZero` without `@` -/ + rw [← mul_div_right_comm, ← mul_assoc, + @le_div_iff₀ _ (_) _ _ _ _ _ _ _ (cast_pos.2 hU.1.card_pos)] exact mod_cast pluennecke_petridis_inequality_mul C (mul_aux hU.1 hU.2 hUA) /-- **Ruzsa's triangle inequality**. Mul-div-div version. -/ diff --git a/Mathlib/Data/NNReal/Defs.lean b/Mathlib/Data/NNReal/Defs.lean index 9a80187ab708f..3953eec25356f 100644 --- a/Mathlib/Data/NNReal/Defs.lean +++ b/Mathlib/Data/NNReal/Defs.lean @@ -128,7 +128,8 @@ noncomputable example : Inv ℝ≥0 := by infer_instance noncomputable example : Div ℝ≥0 := by infer_instance -example : LE ℝ≥0 := by infer_instance +-- Note(kmill): instance contains `NNReal.instCanonicallyLinearOrderedSemifield` +noncomputable example : LE ℝ≥0 := by infer_instance example : Bot ℝ≥0 := by infer_instance @@ -330,7 +331,8 @@ noncomputable def gi : GaloisInsertion Real.toNNReal (↑) := -- will be noncomputable, everything else should not be. example : OrderBot ℝ≥0 := by infer_instance -example : PartialOrder ℝ≥0 := by infer_instance +-- Note(kmill): instance contains `NNReal.instCanonicallyLinearOrderedSemifield` +noncomputable example : PartialOrder ℝ≥0 := by infer_instance noncomputable example : CanonicallyLinearOrderedAddCommMonoid ℝ≥0 := by infer_instance diff --git a/Mathlib/Order/Hom/Lattice.lean b/Mathlib/Order/Hom/Lattice.lean index 4179afdc3722b..9f1b46ad9eaf5 100644 --- a/Mathlib/Order/Hom/Lattice.lean +++ b/Mathlib/Order/Hom/Lattice.lean @@ -1095,7 +1095,7 @@ def subtypeVal {P : β → Prop} letI := Subtype.lattice Psup Pinf LatticeHom {x : β // P x} β := letI := Subtype.lattice Psup Pinf - .mk (SupHom.subtypeVal Psup) (by simp) + .mk (SupHom.subtypeVal Psup) (by simp [Subtype.coe_inf Pinf]) @[simp] lemma subtypeVal_apply {P : β → Prop} diff --git a/Mathlib/Order/Interval/Finset/Box.lean b/Mathlib/Order/Interval/Finset/Box.lean index 902ac28210bbd..4ad7dc9c23b48 100644 --- a/Mathlib/Order/Interval/Finset/Box.lean +++ b/Mathlib/Order/Interval/Finset/Box.lean @@ -93,11 +93,6 @@ lemma card_box : ∀ {n}, n ≠ 0 → #(box n : Finset (ℤ × ℤ)) = 8 * n | 0 => by simp [Prod.ext_iff] | n + 1 => by simp [box_succ_eq_sdiff, Prod.le_def] - #adaptation_note /-- v4.7.0-rc1: `omega` no longer identifies atoms up to defeq. - (This had become a performance bottleneck.) - We need a tactic for normalising instances, to avoid the `have`/`simp` dance below: -/ - have : @Nat.cast ℤ instNatCastInt n = @Nat.cast ℤ AddMonoidWithOne.toNatCast n := rfl - simp only [this] omega -- TODO: Can this be generalised to locally finite archimedean ordered rings? diff --git a/Mathlib/RingTheory/TensorProduct/MvPolynomial.lean b/Mathlib/RingTheory/TensorProduct/MvPolynomial.lean index 529b84b2a297c..74603fca791d2 100644 --- a/Mathlib/RingTheory/TensorProduct/MvPolynomial.lean +++ b/Mathlib/RingTheory/TensorProduct/MvPolynomial.lean @@ -64,29 +64,35 @@ noncomputable def rTensor : MvPolynomial σ S ⊗[R] N ≃ₗ[S] (σ →₀ ℕ) →₀ (S ⊗[R] N) := TensorProduct.finsuppLeft' _ _ _ _ _ +#adaptation_note /-- 2024-11-10 added `.toFun` -/ lemma rTensor_apply_tmul (p : MvPolynomial σ S) (n : N) : - rTensor (p ⊗ₜ[R] n) = p.sum (fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n)) := + rTensor.toFun (p ⊗ₜ[R] n) = p.sum (fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n)) := TensorProduct.finsuppLeft_apply_tmul p n +#adaptation_note /-- 2024-11-10 added `.toFun` -/ lemma rTensor_apply_tmul_apply (p : MvPolynomial σ S) (n : N) (d : σ →₀ ℕ) : - rTensor (p ⊗ₜ[R] n) d = (coeff d p) ⊗ₜ[R] n := + rTensor.toFun (p ⊗ₜ[R] n) d = (coeff d p) ⊗ₜ[R] n := TensorProduct.finsuppLeft_apply_tmul_apply p n d +#adaptation_note /-- 2024-11-10 added `.toFun` -/ lemma rTensor_apply_monomial_tmul (e : σ →₀ ℕ) (s : S) (n : N) (d : σ →₀ ℕ) : - rTensor (monomial e s ⊗ₜ[R] n) d = if e = d then s ⊗ₜ[R] n else 0 := by + rTensor.toFun (monomial e s ⊗ₜ[R] n) d = if e = d then s ⊗ₜ[R] n else 0 := by simp only [rTensor_apply_tmul_apply, coeff_monomial, ite_tmul] +#adaptation_note /-- 2024-11-10 added `.toFun` -/ lemma rTensor_apply_X_tmul (s : σ) (n : N) (d : σ →₀ ℕ) : - rTensor (X s ⊗ₜ[R] n) d = if Finsupp.single s 1 = d then (1 : S) ⊗ₜ[R] n else 0 := by + rTensor.toFun (X s ⊗ₜ[R] n) d = if Finsupp.single s 1 = d then (1 : S) ⊗ₜ[R] n else 0 := by rw [rTensor_apply_tmul_apply, coeff_X', ite_tmul] +#adaptation_note /-- 2024-11-10 added `.toFun` -/ lemma rTensor_apply (t : MvPolynomial σ S ⊗[R] N) (d : σ →₀ ℕ) : - rTensor t d = ((lcoeff S d).restrictScalars R).rTensor N t := + rTensor.toFun t d = ((lcoeff S d).restrictScalars R).rTensor N t := TensorProduct.finsuppLeft_apply t d +#adaptation_note /-- 2024-11-10 added `.toFun` -/ @[simp] lemma rTensor_symm_apply_single (d : σ →₀ ℕ) (s : S) (n : N) : - rTensor.symm (Finsupp.single d (s ⊗ₜ n)) = + rTensor.symm.toFun (Finsupp.single d (s ⊗ₜ n)) = (monomial d s) ⊗ₜ[R] n := TensorProduct.finsuppLeft_symm_apply_single (R := R) d s n @@ -163,8 +169,9 @@ lemma rTensorAlgHom_toLinearMap : simp only [coeff] erw [finsuppLeft_apply_tmul_apply] +#adaptation_note /-- 2024-11-10 added `.toFun` -/ lemma rTensorAlgHom_apply_eq (p : MvPolynomial σ S ⊗[R] N) : - rTensorAlgHom (S := S) p = rTensor p := by + rTensorAlgHom (S := S) p = rTensor.toFun p := by rw [← AlgHom.toLinearMap_apply, rTensorAlgHom_toLinearMap] rfl @@ -178,6 +185,8 @@ noncomputable def rTensorAlgEquiv : rw [← LinearEquiv.symm_apply_eq] exact finsuppLeft_symm_apply_single (R := R) (0 : σ →₀ ℕ) (1 : S) (1 : N) · intro x y + #adaptation_note /-- 2024-11-10 added `change` -/ + change rTensor.toFun (x * y) = _ erw [← rTensorAlgHom_apply_eq (S := S)] simp only [_root_.map_mul, rTensorAlgHom_apply_eq] rfl