Bump mathlib to v4.22.0

Author: YaelDillies

LeanAPAP/Extras/BSG.lean

@@ -18,15 +18,15 @@ private lemma oneOfPair_mem :
     x ∈ oneOfPair H X ↔ x ∈ X ∧ (3 / 4 : ℝ) * #X ≤ #{yz ∈ H | yz.1 = x} := mem_filter
 
 private lemma oneOfPair_mem' (hH : H ⊆ X ×ˢ X) : #{yz ∈ H | yz.1 = x} = #{c ∈ X | (x, c) ∈ H} := by
-  refine card_nbij' Prod.snd (fun c ↦ (x, c)) ?_ (by simp) (by aesop) (by simp)
-  simp (config := { contextual := true }) only [eq_comm, Prod.forall, mem_filter, and_imp, and_true]
-  exact fun a b hab _ ↦ (mem_product.1 (hH hab)).2
+  refine card_nbij' Prod.snd (fun c ↦ (x, c)) ?_ (by simp [Set.MapsTo])
+    (by aesop (add simp [Set.LeftInvOn])) (by simp [Set.LeftInvOn])
+  simpa +contextual [Set.MapsTo, eq_comm] using fun a b hab _ ↦ (mem_product.1 (hH hab)).2
 
 private lemma oneOfPair_bound_one :
     ∑ x ∈ X \ oneOfPair H X, (#{yz ∈ H | yz.1 = x} : ℝ) ≤ (3 / 4) * #X ^ 2 :=
   calc _ ≤ ∑ _x ∈ X \ oneOfPair H X, (3 / 4 : ℝ) * #X := by
         gcongr with i hi
-        simp only [oneOfPair, ← filter_not, Prod.forall, not_le, not_lt, mem_filter] at hi
+        simp only [oneOfPair, ← filter_not, not_le, mem_filter] at hi
         exact hi.2.le
        _ = #(X \ oneOfPair H X) * ((3 / 4 : ℝ) * #X) := by simp
        _ ≤ #X * ((3 / 4 : ℝ) * #X) := by gcongr; exact sdiff_subset
@@ -72,13 +72,8 @@ lemma quadruple_bound_right {a b : α} (H : Finset (α × α)) (X : Finset α) (
         fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c) : ℝ)
       ≤ #(((B ×ˢ B) ×ˢ B ×ˢ B).filter fun ⟨⟨a₁, a₂⟩, a₃, a₄⟩ ↦ (a₁ - a₂) - (a₃ - a₄) = a - b) := by
   rw [← h, Nat.cast_le]
-  refine card_le_card_of_injOn Sigma.snd ?_ ?_
-  · simp only [not_and, mem_product, and_imp, Prod.forall, mem_sigma, mem_filter, Sigma.forall]
-    intro c a₁ a₂ a₃ a₄ _ _ _ ha₁ ha₂ ha₃ ha₄ h₁ h₂
-    simp [*]
-  simp only [Set.InjOn, not_and, mem_product, and_imp, Prod.forall, mem_sigma, mem_filter,
-    Sigma.forall, Sigma.mk.inj_iff, heq_eq_eq, Prod.mk.injEq]
-  simp (config := {contextual := true})
+  refine card_le_card_of_injOn Sigma.snd (by simp +contextual [Set.MapsTo, *]) ?_
+  simp +contextual [Set.InjOn]
   aesop
 
 end
@@ -93,7 +88,8 @@ lemma thing_one : (𝟭_[R] B ○ 𝟭 A) x = ∑ y, 𝟭 A y * 𝟭 B (x + y) :
 lemma thing_one_right : (𝟭_[R] A ○ 𝟭 B) x = #(A ∩ (x +ᵥ B)) := by
   rw [indicate_dconv_indicate_apply]
   congr 1
-  apply card_nbij' Prod.fst (fun a ↦ (a, a - x)) <;> aesop (add simp [mem_vadd_finset])
+  apply card_nbij' Prod.fst (fun a ↦ (a, a - x)) <;>
+    aesop (add simp [Set.MapsTo, Set.LeftInvOn, Set.mem_vadd_set])
 
 lemma thing_two : ∑ s, (𝟭_[R] A ○ 𝟭 B) s = #A * #B := by
   simp only [sum_dconv, conj_indicate_apply, sum_indicate]
@@ -264,8 +260,8 @@ lemma lemma_one {c K : ℝ} (hc : 0 < c) (hK : 0 < K) (hE : K⁻¹ * (#A ^ 2 * #
     ← filter_mem_eq_inter]
   refine Nat.cast_le.2 <| card_le_card ?_
   rintro ⟨a, b⟩
-  simp (config := { contextual := true }) only [not_le, mem_product, mem_inter, and_imp,
-    Prod.forall, not_lt, mem_filter, H_choice, filter_congr_decidable, and_self, true_and, X]
+  simp +contextual only [not_le, mem_product, mem_inter, and_imp, mem_filter, H_choice, and_self,
+    true_and, X]
   rintro _ _ _ _ h
   -- I'd like automation to handle the rest of this
   refine h.le.trans ?_
@@ -338,7 +334,7 @@ lemma quadruple_bound_left {a b : G} {K : ℝ} {H : Finset (G × G)}
     _ ≤ ∑ c ∈ X with (a, c) ∈ H ∧ (b, c) ∈ H, (#(((B ×ˢ B) ×ˢ B ×ˢ B).filter
         fun ((a₁, a₂), a₃, a₄) ↦ a₁ - a₂ = a - c ∧ a₃ - a₄ = b - c) : ℝ) := by
       gcongr with i hi
-      simp only [not_and, mem_filter] at hi
+      simp only [mem_filter] at hi
       exact quadruple_bound_other hi.2.1 hi.2.2 hH
     _ = _ := by rw [card_sigma, Nat.cast_sum]
 

LeanAPAP/FiniteField.lean

@@ -259,7 +259,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
       (ε / 2) (by positivity) (div_le_one_of_le₀ (hε₁.le.trans <| by norm_num) <| by norm_num)
       (card G • (balance (μ A) ○ balance (μ A))) (sqrt (card G) • balance (μ A)) (μ univ) ?_ ?_ ?_
     · ext a : 1
-      simp [smul_dconv, dconv_smul, smul_smul, ← mul_assoc, ← sq, ← Complex.ofReal_pow]
+      simp [smul_dconv, dconv_smul, ← mul_assoc, ← sq, ← Complex.ofReal_pow]
     · simp
     · have global_dichotomy := global_dichotomy hA₀ hγC hγ hAC
       simpa [wLpNorm_nsmul, ← nsmul_eq_mul, div_le_iff₀' (show (0 : ℝ) < card G by positivity),
@@ -417,7 +417,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
         rw [← wInner_one_dconv_eq_conv_wInner_one, dconv_right_comm, conv_dconv_right_comm (μ A),
           wInner_one_dconv_eq_conv_wInner_one, ← dconv_wInner_one_eq_wInner_one_conv,
           ← conj_wInner_symm]
-        simp [wInner_one_eq_sum, inner_apply', smul_sum, mul_assoc]
+        simp [wInner_one_eq_sum, smul_sum, mul_assoc]
         congr! 1
         group
       _ ≤ card G • (‖μ_[ℝ] (Set.toFinset V) ∗ μ A‖_[∞] * ‖μ_[ℝ] A ∗ μ A₂ ○ μ A₁‖_[1]) := by
@@ -476,7 +476,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
         2⁻¹ ≤ card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ]) := by
     induction' i with i ih hi
     · exact ⟨G, inferInstance, inferInstance, inferInstance, inferInstance, A, by simp [n], hA,
-        by simp [α], by simp [α, nnratCast_dens, Fintype.card_subtype, subset_iff]⟩
+        by simp [α], by simp [α, nnratCast_dens]⟩
     obtain ⟨V, _, _, _, _, B, hV, hB, hαβ, hBV⟩ := ih
     obtain hB' | hB' := le_or_gt 2⁻¹ (card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ])
     · exact ⟨V, inferInstance, inferInstance, inferInstance, inferInstance, B,

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -62,7 +62,7 @@ lemma my_markov (hc : 0 < c) (hg : ∀ a ∈ A, 0 ≤ g a) (h : ∑ a ∈ A, g a
   have := h.trans'
     (sum_le_sum_of_subset_of_nonneg (filter_subset (¬g · ≤ c) A) fun i hi _ ↦ hg _ hi)
   have :=
-    (card_nsmul_le_sum _ _ c (by simp (config := { contextual := true }) [le_of_lt])).trans this
+    (card_nsmul_le_sum _ _ c (by simp +contextual [le_of_lt])).trans this
   rw [nsmul_eq_mul, mul_right_comm] at this
   have := le_of_mul_le_mul_right this hc
   rw [filter_not, cast_card_sdiff (filter_subset _ _)] at this
@@ -135,7 +135,7 @@ lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :
   refine (RCLike.marcinkiewicz_zygmund (by linarith only [hm]) f' ?_).trans_eq' ?_
   · intro i
     rw [Fintype.sum_piFinset_apply, sum_sub_distrib]
-    simp only [sub_eq_zero, sum_const, indicate_apply]
+    simp only [sum_const]
     rw [← Pi.smul_apply (card A), ← smul_conv, card_smul_mu, conv_eq_sum_sub']
     simp only [boole_mul, indicate_apply]
     rw [← sum_filter, filter_mem_eq_inter, univ_inter, sub_self, smul_zero]
@@ -155,7 +155,7 @@ lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) :
     refine fun f ↦ sum_congr rfl fun x hx ↦ ?_
     exact sum_congr rfl fun y hy ↦ if_pos <| add_mem_add hx hy
   rw [this]
-  have (x y) :
+  have (x y : Fin k → G) :
       ∑ s₁ ∈ S.piDiag (Fin k), ∑ s₂ ∈ S.piDiag (Fin k), ite (y + s₂ = x + s₁) (1 : ℝ) 0 =
         ite (x - y ∈ univ.piDiag (Fin k)) 1 0 *
           ∑ s₁ ∈ S.piDiag (Fin k), ∑ s₂ ∈ S.piDiag (Fin k), ite (s₂ = x + s₁ - y) 1 0 := by
@@ -200,8 +200,7 @@ lemma big_shifts (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0)
     refine (card_le_card (add_subset_add_right hL)).trans ?_
     rw [← Fintype.card_piFinset_const]
     refine card_le_card fun i hi ↦ ?_
-    simp only [mem_add, mem_piDiag, Fintype.mem_piFinset, exists_prop, exists_and_left,
-      exists_exists_and_eq_and] at hi ⊢
+    simp only [mem_add, mem_piDiag, Fintype.mem_piFinset, exists_exists_and_eq_and] at hi ⊢
     obtain ⟨y, hy, a, ha, rfl⟩ := hi
     intro j
     exact ⟨y j, hy _, a, ha, rfl⟩
@@ -220,7 +219,6 @@ lemma big_shifts (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0)
 
 variable [MeasurableSpace G]
 
-
 namespace AlmostPeriodicity
 
 def LProp (k m : ℕ) (ε : ℝ) (f : G → ℂ) (A : Finset G) (a : Fin k → G) : Prop :=
@@ -302,9 +300,7 @@ lemma lemma28 (hε : 0 < ε) (hm : 1 ≤ m) (hk : (64 : ℝ) * m / ε ^ 2 ≤ k)
       (8 * m) ^ m * k ^ (m - 1) * ∑ a ∈ A ^^ k, ∑ i, (2 * ‖f‖_[2 * m]) ^ (2 * m) :=
     lemma28_part_two hm hA
   refine le_trans (mod_cast this) ?_
-  simp only [sum_const, Fintype.card_piFinset_const, nsmul_eq_mul, Nat.cast_pow]
-  refine (lemma28_end hε hm hk).trans_eq' ?_
-  simp [mul_assoc, card_fin]
+  simpa [mul_assoc] using lemma28_end hε hm hk
 
 open MeasureTheory in
 lemma just_the_triangle_inequality {t : G} {a : Fin k → G} (ha : a ∈ l k m ε f A)
@@ -406,7 +402,7 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (
     exact T_bound hK₂ #L #S #A #(A + S) _ rfl hL' this
       (by rw [← cast_addConst_mul_card]; gcongr) hA.card_pos hε hε' hm
   intro t ht
-  simp only [exists_prop, exists_eq_right, mem_filter, mem_univ, true_and] at ht
+  simp only [mem_filter, mem_univ, true_and] at ht
   have := just_the_triangle_inequality ha ht hk.bot_lt hm
   rwa [neg_neg, mul_div_cancel₀ _ (two_ne_zero' ℝ)] at this
 
@@ -440,7 +436,7 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
       _ = _ := by simp [div_div_eq_mul_div, ← mul_div_right_comm, mul_right_comm, div_pow]
       _ ≤ _ := hKT
   set F : G → ℂ := τ t (μ A ∗ 𝟭 B) - μ A ∗ 𝟭 B
-  have (x) :=
+  have (x : G) :=
     calc
       (τ t (μ A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C : G → ℂ) x
         = (F ∗ μ C) x := by simp [sub_conv, F]

LeanAPAP/Physics/DRC.lean

@@ -29,7 +29,7 @@ private lemma lemma_0 (p : ℕ) (B₁ B₂ A : Finset G) (f : G → ℝ) :
   refine Fintype.sum_equiv (Equiv.neg _) _ _ fun s ↦ ?_
   rw [← smul_mul_assoc, mul_smul_mul_comm, card_smul_mu_apply, card_smul_mu_apply,
     indicate_inter_apply, indicate_inter_apply, mul_mul_mul_comm, prod_mul_distrib]
-  simp [c, indicate_inf_apply, ← translate_indicate, sub_eq_add_neg, mul_assoc, add_comm]
+  simp [c, indicate_inf_apply, sub_eq_add_neg, mul_assoc, add_comm]
 
 private lemma sum_c (p : ℕ) (B A : Finset G) : ∑ s, #(B ∩ c p A s) = #A ^ p * #B := by
   simp only [card_eq_sum_indicate, indicate_inter_apply, c, indicate_inf_apply, mul_sum, sum_mul,
@@ -91,7 +91,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     have : 0 ≤ μ_[ℝ] B₁ ○ μ B₂ * (𝟭 A ○ 𝟭 A) ^ p * (↑) ∘ f :=
       mul_nonneg (mul_nonneg (dconv_nonneg mu_nonneg mu_nonneg) <| pow_nonneg
         (dconv_nonneg indicate_nonneg indicate_nonneg) _) fun _ ↦ by simp -- positivity
-    refine Fintype.sum_pos <| this.gt_iff_ne.2 <| support_nonempty_iff.1 ?_
+    refine Fintype.sum_pos <| this.lt_iff_ne'.2 <| support_nonempty_iff.1 ?_
     simp only [support_comp_eq, Set.Nonempty, and_assoc, support_mul', support_dconv,
       indicate_nonneg, mu_nonneg, support_indicate, support_mu, NNReal.coe_eq_zero, iff_self,
       forall_const, Set.mem_inter_iff, ← coe_sub, mem_coe, support_pow' _ hp₀, hf]
@@ -160,7 +160,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     _ ≤ M * (sqrt (∑ s, #(A₁ s)) * sqrt (∑ s, #(A₂ s))) := by
       gcongr; exact sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity
     _ = _ := ?_
-  · simp only [mem_filter, mem_univ, true_and, Nat.cast_nonneg, and_imp]
+  · simp only [mem_filter, mem_univ, true_and, and_imp]
     exact fun s hsM hs ↦ mul_lt_mul_of_pos_right ((sqrt_lt' hM).2 hsM) <|
       sqrt_pos.2 <| (hg _).lt_of_ne' hs
   rw [sum_cast_c, sum_cast_c, sqrt_mul', sqrt_mul', mul_mul_mul_comm (sqrt _), mul_self_sqrt,
@@ -187,17 +187,16 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
     c.Nonempty := by
     simp_rw [nonempty_iff_ne_empty]
     rintro rfl
-    simp [pow_mul', (zero_lt_four' ℝ).not_ge, inv_mul_le_iff₀ (zero_lt_four' ℝ), mul_assoc,
-      div_nonpos_iff, mul_nonpos_iff, (pow_pos (dLpNorm_conv_pos hp₀.ne' hB hA) 2).not_ge,
-      hp₀, hp₀.ne', hA.ne_empty] at h
+    simp [pow_mul', inv_mul_le_iff₀ (zero_lt_four' ℝ), div_nonpos_iff,
+      (pow_pos (dLpNorm_conv_pos hp₀.ne' hB hA) 2).not_ge, hp₀.ne', hA.ne_empty] at h
   have hA₁ : A₁.Nonempty := aux _ _ hcard₁
   have hA₂ : A₂.Nonempty := aux _ _ hcard₂
   clear hcard₁ hcard₂ aux
   rw [sub_le_comm]
   calc
     _ = ∑ x ∈ (s p ε B₁ B₂ A)ᶜ, (μ A₁ ○ μ A₂) x := ?_
     _ = ⟪μ_[ℝ] A₁ ○ μ A₂, (↑) ∘ 𝟭_[ℝ≥0] ((s (↑p) ε B₁ B₂ A)ᶜ)⟫_[ℝ] := by
-      simp [wInner_one_eq_sum, -mem_compl, -mem_s, apply_ite NNReal.toReal, indicate_apply]
+      simp [wInner_one_eq_sum, -mem_compl, -mem_s, indicate_apply]
     _ ≤ _ := (le_div_iff₀ <| dLpNorm_conv_pos hp₀.ne' hB hA).2 h
     _ ≤ _ := ?_
   · simp_rw [sub_eq_iff_eq_add', sum_add_sum_compl, sum_dconv, map_mu]
@@ -252,8 +251,7 @@ lemma sifting_cor (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0 < δ) (hp : Even p
       rw [nnratCast_dens, le_div_iff₀, ← mul_div_right_comm]
       calc
         _ = (‖𝟭_[ℝ] A ○ 𝟭 A‖_[1, μ univ] : ℝ) := by
-          simp [mu, wLpNorm_smul_right, hp₀, dL1Norm_dconv, card_univ, inv_mul_eq_div]
-
+          simp [mu, wLpNorm_smul_right, dL1Norm_dconv, card_univ, inv_mul_eq_div]
         _ ≤ _ := wLpNorm_mono_right (one_le_two.trans <| by norm_cast) _ _
       · exact Nat.cast_pos.2 hA.card_pos
     obtain ⟨A₁, -, A₂, -, h, hcard₁, hcard₂⟩ :=

LeanAPAP/Physics/Unbalancing.lean

@@ -30,12 +30,11 @@ lemma pow_inner_nonneg' {f : G → ℂ} (hf : g ○ g = f) (hν : h ○ h = (↑
         simpa using hyz
     _ = _ := by
       rw [← hf, ← hν, wInner_one_eq_sum]
-      simp only [PiLp.toLp_apply, Pi.pow_apply, RCLike.inner_apply, map_pow]
+      simp only [Pi.pow_apply, RCLike.inner_apply, map_pow]
       simp_rw [dconv_apply h, sum_mul]
   simp_rw [dconv_apply_sub, sum_fiberwise, ← univ_product_univ, sum_product]
   simp only [sum_pow', sum_mul_sum, map_mul, starRingEnd_self_apply, Fintype.piFinset_univ,
-    ← Complex.conj_mul', sum_product, map_sum, map_prod,
-    mul_mul_mul_comm (g _), ← prod_mul_distrib]
+    ← Complex.conj_mul', map_sum, map_prod]
   simp only [mul_sum, @sum_comm _ _ (Fin k → G), mul_comm (conj _), prod_mul_distrib, Pi.conj_apply]
   rw [sum_comm]
   congr with x
@@ -193,7 +192,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
         rpow_le_rpow ?_ (sum_le_sum_of_subset_of_nonneg (subset_univ _) fun i _ _ ↦ ?_) ?_
     _ = _ := by
         rw [wLpNorm_eq_sum_nnnorm (by positivity) (by simp)]
-        simp [NNReal.smul_def, hp'.ne', p', (p'_pos hp hε₀ hε₁).le]
+        simp [p', (p'_pos hp hε₀ hε₁).le]
   all_goals positivity
 
 /-- The unbalancing step. Note that we do the physical proof in order to avoid the Fourier

LeanAPAP/Prereqs/Bohr/Basic.lean

@@ -194,26 +194,27 @@ example [Finite G] : Finite (AddChar G ℂ) := by infer_instance
 
 open scoped Classical in
 noncomputable instance [Finite G] : SupSet (BohrSet G) where
-  sSup B :=
-    { frequencies := {ψ | ⨆ i ∈ B, i.ewidth ψ < ⊤},
-      ewidth := fun ψ => ⨆ i ∈ B, ewidth i ψ
-      mem_frequencies := fun ψ => by simp [mem_frequencies] }
+  sSup B := {
+    frequencies := {ψ | ⨆ i ∈ B, i.ewidth ψ < ⊤},
+    ewidth ψ := ⨆ i ∈ B, ewidth i ψ
+    mem_frequencies := by simp
+  }
 
 lemma iInf_lt_top {α β : Type*} [CompleteLattice β] {S : Set α} {f : α → β}:
     (⨅ i ∈ S, f i) < ⊤ ↔ ∃ i ∈ S, f i < ⊤ := by
   simp [lt_top_iff_ne_top]
 
 open scoped Classical in
 noncomputable instance [Finite G] : InfSet (BohrSet G) where
-  sInf B :=
-    { frequencies := {ψ | ∃ i ∈ B, i.ewidth ψ < ⊤},
-      ewidth := fun ψ => ⨅ i ∈ B, ewidth i ψ
-      mem_frequencies := by simp [iInf_lt_top] }
+  sInf B := {
+    frequencies := {ψ | ∃ i ∈ B, i.ewidth ψ < ⊤},
+    ewidth ψ := ⨅ i ∈ B, ewidth i ψ
+    mem_frequencies := by simp
+  }
 
 noncomputable def minimalAxioms [Finite G] :
     CompletelyDistribLattice.MinimalAxioms (BohrSet G) :=
-  Function.Injective.completelyDistribLatticeMinimalAxioms .of BohrSet.ewidth
-    ewidth_injective
+  ewidth_injective.completelyDistribLatticeMinimalAxioms .of BohrSet.ewidth
     (fun _ _ => rfl)
     (fun _ _ => rfl)
     (fun B => by
@@ -270,7 +271,7 @@ open scoped Classical
 noncomputable instance instSMul : SMul ℝ (BohrSet G) where
   smul ρ B := BohrSet.mk B.frequencies
       (fun ψ => if ψ ∈ B.frequencies then Real.nnabs ρ * B.ewidth ψ else ⊤) fun ψ => by
-        simp only [lt_top_iff_ne_top, ite_ne_right_iff, Classical.not_imp, iff_self_and]
+        simp only [lt_top_iff_ne_top, ite_ne_right_iff, iff_self_and]
         intro hψ
         refine ENNReal.mul_ne_top (by simp) ?_
         rwa [←lt_top_iff_ne_top, ←mem_frequencies]
@@ -302,8 +303,8 @@ end smul
 lemma eq_zero_of_ewidth_eq_zero {B : BohrSet G} [Finite G] (h : B.ewidth = 0) :
     B.chordSet = {0} := by
   rw [Set.eq_singleton_iff_unique_mem]
-  simp only [zero_mem, true_and, mem_chordSet_iff_nnnorm_width, map_zero_eq_one, sub_self,
-    norm_zero, true_and, NNReal.zero_le_coe, implies_true, nnnorm_zero, zero_le]
+  simp only [mem_chordSet_iff_nnnorm_width, map_zero_eq_one, sub_self, nnnorm_zero, zero_le,
+    implies_true, true_and]
   intro x hx
   by_contra!
   rw [←AddChar.exists_apply_ne_zero] at this