Bump mathlib

LeanAPAP.lean

@@ -4,6 +4,7 @@ import LeanAPAP.Integer
 import LeanAPAP.Mathlib.Algebra.BigOperators.Group.Finset
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Algebra.Group.Basic
+import LeanAPAP.Mathlib.Algebra.Group.Pointwise.Finset
 import LeanAPAP.Mathlib.Algebra.Group.Subgroup.Basic
 import LeanAPAP.Mathlib.Algebra.Order.BigOperators.Group.Finset
 import LeanAPAP.Mathlib.Algebra.Order.Field.Defs
@@ -24,8 +25,8 @@ import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Operations
 import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Mathlib.Data.Finset.Density
-import LeanAPAP.Mathlib.Data.Finset.Pointwise.Basic
 import LeanAPAP.Mathlib.Data.Finset.Preimage
+import LeanAPAP.Mathlib.Data.Fintype.Basic
 import LeanAPAP.Mathlib.Data.Real.ConjExponents
 import LeanAPAP.Mathlib.Data.ZMod.Module
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup

LeanAPAP/Mathlib/Data/Finset/Pointwise/Basic.lean → LeanAPAP/Mathlib/Algebra/Group/Pointwise/Finset.lean

@@ -1,5 +1,5 @@
+import Mathlib.Algebra.Group.Pointwise.Finset.Basic
 import Mathlib.Data.Finset.Density
-import Mathlib.Data.Finset.Pointwise.Basic
 
 open scoped Pointwise
 

LeanAPAP/Mathlib/Data/Fintype/Basic.lean

@@ -0,0 +1,3 @@
+import Mathlib.Data.Fintype.Basic
+
+attribute [simp] Finset.univ_nonempty

LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean

@@ -1,6 +1,5 @@
 import Mathlib.MeasureTheory.Function.EssSup
 import Mathlib.Probability.ConditionalProbability
-import LeanAPAP.Mathlib.MeasureTheory.Measure.Count
 
 open Filter MeasureTheory ProbabilityTheory
 open scoped ENNReal

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -200,7 +200,7 @@ lemma big_shifts (S : Finset G) (L : Finset (Fin k → G)) (hk : k ≠ 0)
     ∃ a : Fin k → G, a ∈ L ∧
       L.card * S.card ≤ (A + S).card ^ k * (univ.filter fun t : G ↦ (a - fun _ ↦ t) ∈ L).card := by
   rcases S.eq_empty_or_nonempty with (rfl | hS)
-  · simpa only [card_empty, mul_zero, zero_le', and_true_iff] using hL'
+  · simpa only [card_empty, mul_zero, zero_le', and_true] using hL'
   have hS' : 0 < S.card := by rwa [card_pos]
   have : (L + S.piDiag (Fin k)).card ≤ (A + S).card ^ k := by
     refine (card_le_card (add_subset_add_right hL)).trans ?_
@@ -421,7 +421,7 @@ lemma almost_periodicity (ε : ℝ) (hε : 0 < ε) (hε' : ε ≤ 1) (m : ℕ) (
     exact T_bound hK₂ L.card S.card A.card (A + S).card _ 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_iff] at ht
+  simp only [exists_prop, exists_eq_right, 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
 

LeanAPAP/Physics/DRC.lean

@@ -94,7 +94,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
         (dconv_nonneg indicate_nonneg indicate_nonneg) _) fun _ ↦ by simp -- positivity
     refine Fintype.sum_pos $ this.gt_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_iff,
+      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]
   set A₁ := fun s ↦ B₁ ∩ c p A s
   set A₂ := fun s ↦ B₂ ∩ c p A s
@@ -111,7 +111,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
         (2 * ∑ x, (μ B₁ ○ μ B₂) x * (𝟭_[ℝ] A ○ 𝟭 A) x ^ p * f x) by
     obtain ⟨s, -, hs⟩ := exists_lt_of_sum_lt this
     refine ⟨_, inter_subset_left (s₂ := c p A s), _, inter_subset_left (s₂ := c p A s), ?_⟩
-    simp only [indicate_apply, mem_filter, mem_univ, true_and_iff, boole_mul] at hs
+    simp only [indicate_apply, mem_filter, mem_univ, true_and, boole_mul] at hs
     split_ifs at hs with h; swap
     · simp only [zero_mul, dL2Inner_eq_sum, Function.comp_apply, RCLike.inner_apply,
         RCLike.conj_to_real] at hs
@@ -133,7 +133,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     all_goals exact Nat.cast_le.2 $ card_mono inter_subset_left
   rw [← sum_mul, lemma_0, nsmul_eq_mul, Nat.cast_mul, ← sum_mul, mul_right_comm, ← hgB,
     mul_left_comm, ← mul_assoc]
-  simp only [indicate_apply, boole_mul, mem_filter, mem_univ, true_and_iff, ← sum_filter,
+  simp only [indicate_apply, boole_mul, mem_filter, mem_univ, true_and, ← sum_filter,
     mul_lt_mul_right hf, Function.comp_apply]
   by_cases h : ∀ s, g s ≠ 0 → M ^ 2 ≤ g s
   · rw [← sum_filter_ne_zero (s := filter _ _), Finset.filter_comm,
@@ -161,7 +161,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
           := mul_le_mul_of_nonneg_left
             (sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity) hM.le
       _ = _ := ?_
-  · simp only [mem_filter, mem_univ, true_and_iff, Nat.cast_nonneg, and_imp]
+  · simp only [mem_filter, mem_univ, true_and, Nat.cast_nonneg, 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,

LeanAPAP/Physics/Unbalancing.lean

@@ -34,7 +34,7 @@ lemma pow_inner_nonneg' {f : G → ℂ} (hf : g ○ g = f) (hν : h ○ h = (↑
   have : ∀ x, ∀ yz ∈ univ.filter fun yz : G × G ↦ yz.1 - yz.2 = x,
     conj ((g ○ g) x) ^ k * (h yz.1 * conj (h yz.2)) =
       conj ((g ○ g) (yz.1 - yz.2)) ^ k * (h yz.1 * conj (h yz.2)) := by
-    simp only [mem_filter, mem_univ, true_and_iff]
+    simp only [mem_filter, mem_univ, true_and]
     rintro _ _ rfl
     rfl
   refine (sum_congr rfl fun _ _ ↦ sum_congr rfl $ this _).trans ?_
@@ -121,7 +121,7 @@ private lemma unbalancing'' (p : ℕ) (hp : 5 ≤ p) (hp₁ : Odd p) (hε₀ : 0
       _ = (3 / 4) ^ p * ε ^ p * ∑ i in P \ T, (ν i : ℝ) := by rw [← sum_mul, mul_comm, mul_pow]
       _ ≤ 4⁻¹ * ε ^ p * ∑ i, (ν i : ℝ) := ?_
       _ = 4⁻¹ * ε ^ p := by norm_cast; simp [hν₁]
-    · simp only [mem_sdiff, mem_filter, mem_univ, true_and_iff, not_le, P, T] at hi
+    · simp only [mem_sdiff, mem_filter, mem_univ, true_and, not_le, P, T] at hi
       exact mul_le_mul_of_nonneg_left (pow_le_pow_left hi.1 hi.2.le _) (by positivity)
     · refine mul_le_mul (mul_le_mul_of_nonneg_right (le_trans (pow_le_pow_of_le_one ?_ ?_ hp) ?_)
         ?_) (sum_le_univ_sum_of_nonneg fun i ↦ ?_) ?_ ?_ <;>

LeanAPAP/Prereqs/AddChar/Basic.lean

@@ -1,5 +1,5 @@
+import Mathlib.Algebra.BigOperators.Expect
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
-import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Inner.Discrete.Defs
 
 open Finset hiding card

LeanAPAP/Prereqs/Balance.lean

@@ -1,4 +1,4 @@
-import LeanAPAP.Prereqs.Expect.Basic
+import Mathlib.Algebra.BigOperators.Expect
 
 /-!
 # Balancing a function

LeanAPAP/Prereqs/Convolution/Compact.lean

@@ -1,4 +1,6 @@
+import LeanAPAP.Mathlib.Data.Fintype.Basic
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
+import LeanAPAP.Prereqs.Expect.Basic
 import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Function.Indicator.Defs