Fewer set_options

Author: YaelDillies

APAP/FiniteField.lean

@@ -155,7 +155,6 @@ public lemma global_dichotomy [DecidableEq G] [MeasurableSpace G] [DiscreteMeasu
 
 variable {q n : ℕ} [Module (ZMod q) G] {A₁ A₂ : Finset G} (S : Finset G) {α : ℝ}
 
-set_option linter.flexible false in
 -- Public because it is in the blueprint
 public lemma ap_in_ff [DecidableEq G] (hq : q.Prime) (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹)
     (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hαA₁ : α ≤ A₁.dens) (hαA₂ : α ≤ A₂.dens) :
@@ -171,7 +170,9 @@ public lemma ap_in_ff [DecidableEq G] (hq : q.Prime) (hα₀ : 0 < α) (hα₂ :
   have : 0 ≤ log α⁻¹ := by bound
   have : 0 ≤ log (ε * α)⁻¹ := by bound
   obtain rfl | hS := S.eq_empty_or_nonempty
-  · exact ⟨⊤, inferInstance, by simp [hε₀.le]; positivity⟩
+  · refine ⟨⊤, inferInstance, ?_, by simp [hε₀.le]⟩
+    simp only [finrank_top, tsub_self, CharP.cast_eq_zero, mul_inv_rev, inv_pow]
+    positivity
   have hA₁ : σ[A₁, univ] ≤ α⁻¹ :=
     calc
       _ ≤ (A₁.dens⁻¹ : ℝ) := by norm_cast; exact addConst_le_inv_dens
@@ -262,7 +263,6 @@ lemma ap_in_ff' [DecidableEq G] (hq : q.Prime) (hα₀ : 0 < α) (hα₂ : α 
   simpa [← conjneg_mu] using ap_in_ff S hq (A₂ := -A₂) hα₀ hα₂ hε₀ hε₁ hαA₁ (by simpa)
 
 set_option backward.isDefEq.respectTransparency false in
-set_option linter.flexible false in
 set_option maxHeartbeats 400000 in
 -- FIXME: Get rid of raised heartbeats
 -- Public because it is in the blueprint
@@ -278,7 +278,10 @@ public lemma di_in_ff [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpa
   let p : ℕ := 2 * ⌈𝓛 γ⌉₊
   let f : G → ℝ := balance (μ A)
   obtain rfl | hA₀ := A.eq_empty_or_nonempty
-  · exact ⟨⊤, Classical.decPred _, by simp; positivity⟩
+  · refine ⟨⊤, Classical.decPred _, ?_, by simp⟩
+    simp only [finrank_top, tsub_self, CharP.cast_eq_zero, dens_empty, NNRat.cast_zero, inv_zero,
+      log_zero, add_zero, one_pow, mul_one]
+    positivity
   obtain ⟨p', hp', unbalancing⟩ :
     ∃ p' : ℕ, p' ≤ 2 ^ 10 * (ε / 2)⁻¹ ^ 2 * p ∧
       1 + ε / 2 / 2 ≤ ‖card G • (f ○ᵈ f) + 1‖_[p', μ univ] := by
@@ -327,7 +330,7 @@ public lemma di_in_ff [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpa
         (4⁻¹ : ℝ) * A.dens ^ (2 * q') ≤ A₁.dens ∧ (4⁻¹ : ℝ) * A.dens ^ (2 * q') ≤ A₂.dens := by
     refine sifting_cor (ε := ε / 16) (δ := ε / 32) (by positivity) (by linarith)
       (by positivity) (p := q') (even_two_mul _)
-      (le_mul_of_one_le_right zero_le_two <| by simp; positivity) ?_ hA₀
+      (le_mul_of_one_le_right zero_le_two <| by lia) ?_ hA₀
     calc
       (ε / 16)⁻¹ * log (2 / (ε / 32)) = 2 ^ 4 * ε⁻¹ ^ 1 * log (64 / ε) := by ring_nf
       _ ≤ 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε) := by gcongr <;> norm_num
@@ -447,9 +450,8 @@ public lemma di_in_ff [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpa
         rw [← wInner_one_dddconv_eq_ddconv_wInner_one, dddconv_right_comm,
           ddconv_dddconv_right_comm (μ A), wInner_one_dddconv_eq_ddconv_wInner_one,
           ← dddconv_wInner_one_eq_wInner_one_ddconv, ← conj_wInner_symm]
-        simp [wInner_one_eq_sum, smul_sum, mul_assoc]
-        congr! 1
-        group
+        simp only [nsmul_eq_mul, mul_assoc, wInner_one_eq_sum, inner_apply, conj_trivial, map_sum,
+          smul_sum]
       _ ≤ card G • (‖μ_[ℝ] (Set.toFinset V) ∗ᵈ μ A‖_[∞] * ‖μ_[ℝ] A ∗ᵈ μ A₂ ○ᵈ μ A₁‖_[1]) := by
         gcongr; exact wInner_one_le_dLpNorm_mul_dLpNorm _ _
       _ = _ := by
@@ -465,7 +467,6 @@ public lemma di_in_ff [DecidableEq G] [MeasurableSpace G] [DiscreteMeasurableSpa
         · exact ddconv_nonneg mu_nonneg mu_nonneg
         · exact mu_nonneg
 
-set_option linter.flexible false in
 public theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFree (α := G) A) :
     finrank (ZMod q) G ≤ 2 ^ 156 * 𝓛 A.dens ^ 9 := by
   let n : ℝ := finrank (ZMod q) G
@@ -554,7 +555,7 @@ public theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : Th
         (hB.vadd_set (a := -x) |>.mono <| by simp [B'])
     · calc
         α ≤ B.dens := hαβ
-        _ ≤ (1 + 64⁻¹) * B.dens := by simp [one_add_mul]; positivity
+        _ ≤ (1 + 64⁻¹) * B.dens := by simp [one_add_mul, NNRat.cast_nonneg]
         _ ≤ B'.dens := hβ
     · refine (h.not_ge <| ?_).elim
       calc