fixes

leanprover-community · Dec 17, 2023 · c557306 · c557306
1 parent 3908754
commit c557306
Show file tree

Hide file tree

Showing 6 changed files with 9 additions and 11 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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