From c557306ec06e7c3ff266310a18f5a77e986d8727 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Sun, 17 Dec 2023 12:19:31 +1100 Subject: [PATCH] fixes --- Mathlib/Data/Finset/NoncommProd.lean | 2 +- .../MeasureTheory/Covering/BesicovitchVectorSpace.lean | 3 +-- Mathlib/MeasureTheory/Measure/Stieltjes.lean | 2 +- Mathlib/NumberTheory/Dioph.lean | 2 +- Mathlib/NumberTheory/LucasLehmer.lean | 9 ++++----- Mathlib/NumberTheory/Padics/Hensel.lean | 2 +- 6 files changed, 9 insertions(+), 11 deletions(-) diff --git a/Mathlib/Data/Finset/NoncommProd.lean b/Mathlib/Data/Finset/NoncommProd.lean index 2c6a89119baa7..ab0133e010833 100644 --- a/Mathlib/Data/Finset/NoncommProd.lean +++ b/Mathlib/Data/Finset/NoncommProd.lean @@ -478,7 +478,7 @@ theorem noncommProd_mul_single [Fintype ι] [DecidableEq ι] (x : ∀ i, M i) : noncommProd_eq_pow_card (univ.erase i), one_pow, mul_one] simp only [MonoidHom.single_apply, ne_eq, Pi.mulSingle_eq_same] · intro j hj - simp? at hj says simp only [mem_univ, not_true_eq_false, mem_erase, ne_eq, and_true] at hj + simp? at hj says simp only [mem_erase, ne_eq, mem_univ, and_true] at hj simp only [MonoidHom.single_apply, Pi.mulSingle, Function.update, Eq.ndrec, Pi.one_apply, ne_eq, dite_eq_right_iff] intro h diff --git a/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean b/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean index 9c29756ed1b05..7ddcdff18db69 100644 --- a/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean +++ b/Mathlib/MeasureTheory/Covering/BesicovitchVectorSpace.lean @@ -177,8 +177,7 @@ theorem card_le_of_separated (s : Finset E) (hs : ∀ c ∈ s, ‖c‖ ≤ 2) have K : (s.card : ℝ) ≤ (5 : ℝ) ^ finrank ℝ E := by have := ENNReal.toReal_le_of_le_ofReal (pow_nonneg ρpos.le _) J simp? [ENNReal.toReal_mul] at this says - simp only [one_div, inv_pow, ENNReal.toReal_mul, ENNReal.toReal_nat, inv_nonneg, ge_iff_le, - div_pow] at this + simp only [one_div, inv_pow, ENNReal.toReal_mul, ENNReal.toReal_nat, div_pow] at this simpa [div_eq_mul_inv, zero_le_two] using this exact mod_cast K #align besicovitch.card_le_of_separated Besicovitch.card_le_of_separated diff --git a/Mathlib/MeasureTheory/Measure/Stieltjes.lean b/Mathlib/MeasureTheory/Measure/Stieltjes.lean index 7b235e52ad43b..a5b77fdc9637c 100644 --- a/Mathlib/MeasureTheory/Measure/Stieltjes.lean +++ b/Mathlib/MeasureTheory/Measure/Stieltjes.lean @@ -361,7 +361,7 @@ theorem measure_singleton (a : ℝ) : f.measure {a} = ofReal (f a - leftLim f a) exists_seq_strictMono_tendsto a have A : {a} = ⋂ n, Ioc (u n) a := by refine' Subset.antisymm (fun x hx => by simp [mem_singleton_iff.1 hx, u_lt_a]) fun x hx => _ - simp? at hx says simp only [gt_iff_lt, not_lt, ge_iff_le, mem_iInter, mem_Ioc] at hx + simp? at hx says simp only [mem_iInter, mem_Ioc] at hx have : a ≤ x := le_of_tendsto' u_lim fun n => (hx n).1.le simp [le_antisymm this (hx 0).2] have L1 : Tendsto (fun n => f.measure (Ioc (u n) a)) atTop (𝓝 (f.measure {a})) := by diff --git a/Mathlib/NumberTheory/Dioph.lean b/Mathlib/NumberTheory/Dioph.lean index 74b7ef18f145f..08605491f4c84 100644 --- a/Mathlib/NumberTheory/Dioph.lean +++ b/Mathlib/NumberTheory/Dioph.lean @@ -360,7 +360,7 @@ theorem DiophList.forall (l : List (Set <| α → ℕ)) (d : l.Forall Dioph) : ⟨β, Poly.sumsq pl, fun v => (h v).trans <| exists_congr fun t => (Poly.sumsq_eq_zero _ _).symm⟩ induction' l with S l IH exact ⟨ULift Empty, [], fun _ => by simp⟩ - simp? at d says simp only [imp_false, List.forall_cons] at d + simp? at d says simp only [List.forall_cons] at d exact let ⟨⟨β, p, pe⟩, dl⟩ := d let ⟨γ, pl, ple⟩ := IH dl diff --git a/Mathlib/NumberTheory/LucasLehmer.lean b/Mathlib/NumberTheory/LucasLehmer.lean index 0d162b815dea4..33399d0928cc5 100644 --- a/Mathlib/NumberTheory/LucasLehmer.lean +++ b/Mathlib/NumberTheory/LucasLehmer.lean @@ -152,8 +152,8 @@ theorem residue_eq_zero_iff_sMod_eq_zero (p : ℕ) (w : 1 < p) : -- and `lucas_lehmer_residue p = 0 → 2^p - 1 ∣ s_mod p (p-2)`. intro h simp? [ZMod.int_cast_zmod_eq_zero_iff_dvd] at h says - simp only [ge_iff_le, ZMod.int_cast_zmod_eq_zero_iff_dvd, gt_iff_lt, zero_lt_two, pow_pos, - cast_pred, cast_pow, cast_ofNat] at h + simp only [ZMod.int_cast_zmod_eq_zero_iff_dvd, gt_iff_lt, zero_lt_two, pow_pos, cast_pred, + cast_pow, cast_ofNat] at h apply Int.eq_zero_of_dvd_of_nonneg_of_lt _ _ h <;> clear h · apply sMod_nonneg _ (Nat.lt_of_succ_lt w) · exact sMod_lt _ (Nat.lt_of_succ_lt w) (p - 2) @@ -425,9 +425,8 @@ theorem ω_pow_formula (p' : ℕ) (h : lucasLehmerResidue (p' + 2) = 0) : dsimp [lucasLehmerResidue] at h rw [sZMod_eq_s p'] at h simp? [ZMod.int_cast_zmod_eq_zero_iff_dvd] at h says - simp only [ge_iff_le, add_le_iff_nonpos_left, nonpos_iff_eq_zero, add_tsub_cancel_right, - ZMod.int_cast_zmod_eq_zero_iff_dvd, gt_iff_lt, zero_lt_two, pow_pos, cast_pred, cast_pow, - cast_ofNat] at h + simp only [add_tsub_cancel_right, ZMod.int_cast_zmod_eq_zero_iff_dvd, gt_iff_lt, zero_lt_two, + pow_pos, cast_pred, cast_pow, cast_ofNat] at h cases' h with k h use k replace h := congr_arg (fun n : ℤ => (n : X (q (p' + 2)))) h diff --git a/Mathlib/NumberTheory/Padics/Hensel.lean b/Mathlib/NumberTheory/Padics/Hensel.lean index bb4b424e11a41..dadcf261ad4be 100644 --- a/Mathlib/NumberTheory/Padics/Hensel.lean +++ b/Mathlib/NumberTheory/Padics/Hensel.lean @@ -354,7 +354,7 @@ private theorem bound : ∀ {ε}, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → ‖F.derivative.eval a‖ * T ^ 2 ^ n < ε := by have := bound' hnorm simp? [Tendsto, nhds] at this says - simp only [Tendsto, nhds_def, Set.mem_setOf_eq, not_and, le_iInf_iff, le_principal_iff, mem_map, + simp only [Tendsto, nhds_def, Set.mem_setOf_eq, le_iInf_iff, le_principal_iff, mem_map, mem_atTop_sets, ge_iff_le, Set.mem_preimage, and_imp] at this intro ε hε cases' this (ball 0 ε) (mem_ball_self hε) isOpen_ball with N hN