From b72ddd8f67eba47cffd3f3422d6c01f1e666c23f Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 9 May 2024 05:29:02 +0000 Subject: [PATCH] feat: backport changes from lean-pr-testing-4096 (#12772) These changes will be required after https://github.com/leanprover/lean4/pull/4096, but they all look like positive readability changes to me anyway (the things being filled in are sort of hard to work out with time travelling to later lines in the proofs!), so I think we can backport them all to `master`. Co-authored-by: Scott Morrison --- Mathlib/Algebra/Order/CauSeq/Completion.lean | 2 +- Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean | 4 ++-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean | 2 +- Mathlib/Computability/AkraBazzi/AkraBazzi.lean | 2 +- Mathlib/GroupTheory/Coset.lean | 2 +- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean | 2 +- Mathlib/MeasureTheory/Measure/Haar/Unique.lean | 2 +- Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean | 2 +- Mathlib/Order/PrimeIdeal.lean | 2 +- Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean | 2 +- Mathlib/Topology/ContinuousFunction/Bounded.lean | 2 +- 11 files changed, 12 insertions(+), 12 deletions(-) diff --git a/Mathlib/Algebra/Order/CauSeq/Completion.lean b/Mathlib/Algebra/Order/CauSeq/Completion.lean index e835ea0fc6a27..43f63c26c1587 100644 --- a/Mathlib/Algebra/Order/CauSeq/Completion.lean +++ b/Mathlib/Algebra/Order/CauSeq/Completion.lean @@ -236,7 +236,7 @@ theorem inv_mk {f} (hf) : (@mk α _ β _ abv _ f)⁻¹ = mk (inv f hf) := #align cau_seq.completion.inv_mk CauSeq.Completion.inv_mk theorem cau_seq_zero_ne_one : ¬(0 : CauSeq _ abv) ≈ 1 := fun h => - have : LimZero (1 - 0) := Setoid.symm h + have : LimZero (1 - 0 : CauSeq _ abv) := Setoid.symm h have : LimZero 1 := by simpa by apply one_ne_zero <| const_limZero.1 this #align cau_seq.completion.cau_seq_zero_ne_one CauSeq.Completion.cau_seq_zero_ne_one diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean index 06304fe75c151..e63fdf1c2ad26 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean @@ -160,7 +160,7 @@ variable (𝕜 E F) ‖fst 𝕜 E F‖ = 1 := by refine le_antisymm (norm_fst_le ..) ?_ let ⟨e, he⟩ := exists_ne (0 : E) - have : ‖e‖ ≤ _ * max ‖e‖ ‖0‖ := (fst 𝕜 E F).le_opNorm (e, 0) + have : ‖e‖ ≤ _ * max ‖e‖ ‖(0 : F)‖ := (fst 𝕜 E F).le_opNorm (e, 0) rw [norm_zero, max_eq_left (norm_nonneg e)] at this rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr he), one_mul] @@ -170,7 +170,7 @@ variable (𝕜 E F) ‖snd 𝕜 E F‖ = 1 := by refine le_antisymm (norm_snd_le ..) ?_ let ⟨f, hf⟩ := exists_ne (0 : F) - have : ‖f‖ ≤ _ * max ‖0‖ ‖f‖ := (snd 𝕜 E F).le_opNorm (0, f) + have : ‖f‖ ≤ _ * max ‖(0 : E)‖ ‖f‖ := (snd 𝕜 E F).le_opNorm (0, f) rw [norm_zero, max_eq_right (norm_nonneg f)] at this rwa [← mul_le_mul_iff_of_pos_right (norm_pos_iff.mpr hf), one_mul] diff --git a/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean b/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean index 35b5932ff26a3..60ffd6fc7e1e9 100644 --- a/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean +++ b/Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean @@ -96,7 +96,7 @@ theorem not_integrableOn_Ioi_rpow (s : ℝ) : ¬ IntegrableOn (fun x ↦ x ^ s) · have : IntegrableOn (fun x ↦ x ^ s) (Ioo (0 : ℝ) 1) := h.mono Ioo_subset_Ioi_self le_rfl rw [integrableOn_Ioo_rpow_iff zero_lt_one] at this exact hs.not_lt this - · have : IntegrableOn (fun x ↦ x ^ s) (Ioi 1) := h.mono (Ioi_subset_Ioi zero_le_one) le_rfl + · have : IntegrableOn (fun x ↦ x ^ s) (Ioi (1 : ℝ)) := h.mono (Ioi_subset_Ioi zero_le_one) le_rfl rw [integrableOn_Ioi_rpow_iff zero_lt_one] at this exact hs.not_lt this diff --git a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean index ab91ba6657b6b..914f92776b9ff 100644 --- a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean +++ b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean @@ -520,7 +520,7 @@ lemma tendsto_zero_sumCoeffsExp : Tendsto (fun (p : ℝ) => ∑ i, a i * (b i) ^ linarith lemma tendsto_atTop_sumCoeffsExp : Tendsto (fun (p : ℝ) => ∑ i, a i * (b i) ^ p) atBot atTop := by - have h₁ : Tendsto (fun p => (a (max_bi b) : ℝ) * b (max_bi b) ^ p) atBot atTop := + have h₁ : Tendsto (fun p : ℝ => (a (max_bi b) : ℝ) * b (max_bi b) ^ p) atBot atTop := Tendsto.mul_atTop (R.a_pos (max_bi b)) (by simp) <| tendsto_rpow_atBot_of_base_lt_one _ (by have := R.b_pos (max_bi b); linarith) (R.b_lt_one _) diff --git a/Mathlib/GroupTheory/Coset.lean b/Mathlib/GroupTheory/Coset.lean index 3e22b20e912cd..0f4b46c1664b1 100644 --- a/Mathlib/GroupTheory/Coset.lean +++ b/Mathlib/GroupTheory/Coset.lean @@ -148,7 +148,7 @@ variable [Monoid α] (s : Submonoid α) @[to_additive mem_own_leftAddCoset] theorem mem_own_leftCoset (a : α) : a ∈ a • (s : Set α) := - suffices a * 1 ∈ a • ↑s by simpa + suffices a * 1 ∈ a • (s : Set α) by simpa mem_leftCoset a (one_mem s : 1 ∈ s) #align mem_own_left_coset mem_own_leftCoset #align mem_own_left_add_coset mem_own_leftAddCoset diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 6a5351e8839ba..b7885fae4ed40 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -118,7 +118,7 @@ def invertibleEquivDetInvertible : Invertible A ≃ Invertible A.det where variable {A B} theorem mul_eq_one_comm : A * B = 1 ↔ B * A = 1 := - suffices ∀ A B, A * B = 1 → B * A = 1 from ⟨this A B, this B A⟩ + suffices ∀ A B : Matrix n n α, A * B = 1 → B * A = 1 from ⟨this A B, this B A⟩ fun A B h => by letI : Invertible B.det := detInvertibleOfLeftInverse _ _ h letI : Invertible B := invertibleOfDetInvertible B diff --git a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean index 6a74cbf3e0ea6..39ef8d37ab32f 100644 --- a/Mathlib/MeasureTheory/Measure/Haar/Unique.lean +++ b/Mathlib/MeasureTheory/Measure/Haar/Unique.lean @@ -492,7 +492,7 @@ lemma measure_preimage_isMulLeftInvariant_eq_smul_of_hasCompactSupport · simpa using (u_mem n).2.le have I1 := I μ' (by infer_instance) simp_rw [M] at I1 - have J1 : ∫ (x : G), indicator {1} (fun _ ↦ 1) (f x) ∂μ' + have J1 : ∫ (x : G), indicator {1} (fun _ ↦ (1 : ℝ)) (f x) ∂μ' = ∫ (x : G), indicator {1} (fun _ ↦ 1) (f x) ∂(haarScalarFactor μ' μ • μ) := tendsto_nhds_unique I1 (I (haarScalarFactor μ' μ • μ) (by infer_instance)) have J2 : ENNReal.toReal (μ' (f ⁻¹' {1})) diff --git a/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean b/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean index 9a94e2cc82300..1e5a747035295 100644 --- a/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean +++ b/Mathlib/NumberTheory/Zsqrtd/QuadraticReciprocity.lean @@ -88,7 +88,7 @@ theorem prime_of_nat_prime_of_mod_four_eq_three (p : ℕ) [hp : Fact p.Prime] (h irreducible_iff_prime.1 <| by_contradiction fun hpi => let ⟨a, b, hab⟩ := sq_add_sq_of_nat_prime_of_not_irreducible p hpi - have : ∀ a b : ZMod 4, a ^ 2 + b ^ 2 ≠ ↑p := by + have : ∀ a b : ZMod 4, a ^ 2 + b ^ 2 ≠ (p : ZMod 4) := by erw [← ZMod.natCast_mod p 4, hp3]; decide this a b (hab ▸ by simp) #align gaussian_int.prime_of_nat_prime_of_mod_four_eq_three GaussianInt.prime_of_nat_prime_of_mod_four_eq_three diff --git a/Mathlib/Order/PrimeIdeal.lean b/Mathlib/Order/PrimeIdeal.lean index 00ca6fc656f29..137da1310f5c3 100644 --- a/Mathlib/Order/PrimeIdeal.lean +++ b/Mathlib/Order/PrimeIdeal.lean @@ -158,7 +158,7 @@ instance (priority := 100) IsMaximal.isPrime [IsMaximal I] : IsPrime I := by let J := I ⊔ principal x have hJuniv : (J : Set P) = Set.univ := IsMaximal.maximal_proper (lt_sup_principal_of_not_mem ‹_›) - have hyJ : y ∈ ↑J := Set.eq_univ_iff_forall.mp hJuniv y + have hyJ : y ∈ (J : Set P) := Set.eq_univ_iff_forall.mp hJuniv y rw [coe_sup_eq] at hyJ rcases hyJ with ⟨a, ha, b, hb, hy⟩ rw [hy] diff --git a/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean b/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean index 21b12711a50b1..86bc20cf4ce1f 100644 --- a/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean @@ -175,7 +175,7 @@ theorem dvd_pow_natDegree_of_eval₂_eq_zero {f : R →+* A} (hf : Function.Inje (Ideal.mem_span_singleton.mpr <| dvd_refl x)).pow_natDegree_le_of_root_of_monic_mem _ ((monic_scaleRoots_iff x).mpr hp) _ le_rfl rw [injective_iff_map_eq_zero'] at hf - have : eval₂ _ _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h + have : eval₂ f _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h rwa [hz, Polynomial.eval₂_at_apply, hf] at this #align polynomial.dvd_pow_nat_degree_of_eval₂_eq_zero Polynomial.dvd_pow_natDegree_of_eval₂_eq_zero diff --git a/Mathlib/Topology/ContinuousFunction/Bounded.lean b/Mathlib/Topology/ContinuousFunction/Bounded.lean index c37c0582b37d3..39ec9997fa04d 100644 --- a/Mathlib/Topology/ContinuousFunction/Bounded.lean +++ b/Mathlib/Topology/ContinuousFunction/Bounded.lean @@ -581,7 +581,7 @@ theorem arzela_ascoli₂ (s : Set β) (hs : IsCompact s) (A : Set (α →ᵇ β) IsCompact A := by /- This version is deduced from the previous one by restricting to the compact type in the target, using compactness there and then lifting everything to the original space. -/ - have M : LipschitzWith 1 (↑) := LipschitzWith.subtype_val s + have M : LipschitzWith 1 Subtype.val := LipschitzWith.subtype_val s let F : (α →ᵇ s) → α →ᵇ β := comp (↑) M refine' IsCompact.of_isClosed_subset ((_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed fun f hf => _