chore: enable the flexible and multi-goal linters (#169)

Both of them could help making proofs more robust. For code to be
upstreamed, fixing these is required anyway.

Carleson/Antichain/AntichainOperator.lean

@@ -89,9 +89,9 @@ lemma _root_.ENNReal.div_mul (a : ℝ≥0∞) {b c : ℝ≥0∞} (hb0 : b ≠ 0)
     a / b * c = a / (b / c) := by
   rw [← ENNReal.mul_div_right_comm, ENNReal.div_eq_div_iff (ENNReal.div_ne_zero.mpr ⟨hb0, hc_top⟩)
     _ hb0 hb_top]
-  rw [ENNReal.div_eq_inv_mul, mul_comm a, mul_assoc]
-  simp only [mul_comm b, ← mul_assoc, ENNReal.inv_mul_cancel hc0 hc_top]
-  ring
+  · rw [ENNReal.div_eq_inv_mul, mul_comm a, mul_assoc]
+    simp only [mul_comm b, ← mul_assoc, ENNReal.inv_mul_cancel hc0 hc_top]
+    ring
   · simp only [ne_eq, div_eq_top]
     tauto
 
@@ -114,7 +114,7 @@ private lemma ineq_6_1_7 (x : X) {𝔄 : Set (𝔓 X)} (p : 𝔄) :
           mul_inv_cancel₀ hvol, mul_one]
     _ ≤ 2 ^ a ^ 3 * 2 ^ (5 * a + 100 * a ^ 3) / volume.real (ball x (8 * D ^ 𝔰 p.1)) := by
       gcongr
-      apply (measure_real_ball_pos x (mul_pos (by positivity) (zpow_pos (defaultD_pos _) _)))
+      · exact (measure_real_ball_pos x (mul_pos (by positivity) (zpow_pos (defaultD_pos _) _)))
       · have heq : 2 ^ (100 * a ^ 2) * 2 ^ 5 * (1 / (↑D * 32) * (8 * (D : ℝ) ^ 𝔰 p.1)) =
             (8 * ↑D ^ 𝔰 p.1) := by
           have hD : (D : ℝ) = 2 ^ (100 * a^2) := by simp
@@ -261,8 +261,8 @@ lemma MaximalBoundAntichain {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain (·≤
         (fun _ ↦ ⨍⁻ y, ‖f y‖₊ ∂volume.restrict (ball (𝔠 p.1) (8*D ^ 𝔰 p.1))) := by
       simp only [coe_ofNat, indicator, mem_ball, mul_ite, mul_zero]
       rw [if_pos]
-      gcongr
-      · rw [C_6_1_2, add_comm (5*a), add_assoc]; norm_cast
+      · gcongr
+        rw [C_6_1_2, add_comm (5*a), add_assoc]; norm_cast
         apply pow_le_pow_right₀ one_le_two
         calc
         _ ≤ 101 * a ^ 3  + 6 * a ^ 3:= by
@@ -352,15 +352,15 @@ lemma eLpNorm_maximal_function_le' {𝔄 : Finset (𝔓 X)} (h𝔄 : IsAntichain
       sorry
   · simp only [not_lt, top_le_iff] at hf_top
     rw [hf_top, mul_top]
-    exact le_top
-    · simp only [ne_eq, ENNReal.div_eq_zero_iff, mul_eq_zero, pow_eq_zero_iff',
-      OfNat.ofNat_ne_zero, false_or, false_and, sub_eq_top_iff, two_ne_top, not_false_eq_true,
-      and_true, not_or]
-      refine ⟨?_, mul_ne_top two_ne_top (mul_ne_top (mul_ne_top two_ne_top coe_ne_top)
-        (inv_ne_top.mpr (by simp)))⟩
-      · rw [tsub_eq_zero_iff_le]
-        exact not_le.mpr (lt_trans (by norm_cast)
-          (ENNReal.mul_lt_mul_left' three_ne_zero ofNat_ne_top one_lt_nnq'_coe))
+    · exact le_top
+    simp only [ne_eq, ENNReal.div_eq_zero_iff, mul_eq_zero, pow_eq_zero_iff',
+    OfNat.ofNat_ne_zero, false_or, false_and, sub_eq_top_iff, two_ne_top, not_false_eq_true,
+    and_true, not_or]
+    refine ⟨?_, mul_ne_top two_ne_top (mul_ne_top (mul_ne_top two_ne_top coe_ne_top)
+      (inv_ne_top.mpr (by simp)))⟩
+    rw [tsub_eq_zero_iff_le]
+    exact not_le.mpr (lt_trans (by norm_cast)
+      (ENNReal.mul_lt_mul_left' three_ne_zero ofNat_ne_top one_lt_nnq'_coe))
 
 
 -- lemma 6.1.3, inequality 6.1.10

Carleson/Classical/Approximation.lean

@@ -147,8 +147,8 @@ open Topology Filter
 lemma int_sum_nat {β : Type*} [AddCommGroup β] [TopologicalSpace β] [ContinuousAdd β] {f : ℤ → β} {a : β} (hfa : HasSum f a) :
     Filter.Tendsto (fun N ↦ ∑ n in Icc (-Int.ofNat ↑N) N, f n) Filter.atTop (𝓝 a) := by
   have := Filter.Tendsto.add_const (- (f 0)) hfa.nat_add_neg.tendsto_sum_nat
-  simp at this
-  /-Need to start at 1 instead of zero for the base case to be true· -/
+  simp only [add_neg_cancel_right] at this
+  /- Need to start at 1 instead of zero for the base case to be true. -/
   rw [←tendsto_add_atTop_iff_nat 1] at this
   convert this using 1
   ext N
@@ -165,10 +165,10 @@ lemma int_sum_nat {β : Type*} [AddCommGroup β] [TopologicalSpace β] [Continuo
       · norm_num
         linarith
     rw [this, sum_insert, sum_insert, ih, ← add_assoc]
-    symm
-    rw [sum_range_succ, add_comm, ←add_assoc, add_comm]
-    simp only [Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg, Nat.succ_eq_add_one,
-      Int.ofNat_eq_coe, add_right_inj, add_comm]
+    · symm
+      rw [sum_range_succ, add_comm, ←add_assoc, add_comm]
+      simp only [Nat.cast_add, Nat.cast_one, neg_add_rev, Int.reduceNeg, Nat.succ_eq_add_one,
+        Int.ofNat_eq_coe, add_right_inj, add_comm]
     · simp
     · norm_num
       linarith
@@ -182,7 +182,7 @@ lemma fourierConv_ofTwiceDifferentiable {f : ℝ → ℂ} (periodicf : f.Periodi
   set g : C(AddCircle (2 * π), ℂ) := ⟨AddCircle.liftIco (2*π) 0 f, AddCircle.liftIco_continuous ((periodicf 0).symm) fdiff.continuous.continuousOn⟩ with g_def
   have two_pi_pos' : 0 < 0 + 2 * π := by linarith [Real.two_pi_pos]
   have fourierCoeff_correspondence {i : ℤ} : fourierCoeff g i = fourierCoeffOn two_pi_pos' f i := fourierCoeff_liftIco_eq f i
-  simp at fourierCoeff_correspondence
+  simp only [zero_add] at fourierCoeff_correspondence
   have function_sum : HasSum (fun (i : ℤ) => fourierCoeff g i • fourier i) g := by
     apply hasSum_fourier_series_of_summable
     obtain ⟨C, hC⟩ := fourierCoeffOn_ContDiff_two_bound periodicf fdiff

Carleson/Classical/Basic.lean

@@ -42,8 +42,8 @@ lemma fourierCoeffOn_add {a b : ℝ} {hab : a < b} {f g : ℝ → ℂ} {n : ℤ}
     fourier_coe_apply', Complex.ofReal_sub, Pi.add_apply, smul_eq_mul, mul_add, Complex.real_smul,
     Complex.ofReal_inv]
   rw [← mul_add, ← intervalIntegral.integral_add]
-  ring_nf
-  · apply hf.continuousOn_mul (Continuous.continuousOn _); continuity
+  · ring_nf
+    apply hf.continuousOn_mul (Continuous.continuousOn _); continuity
   · apply hg.continuousOn_mul (Continuous.continuousOn _); continuity
 
 @[simp]
@@ -92,11 +92,11 @@ lemma Function.Periodic.uniformContinuous_of_continuous {f : ℝ → ℂ} {T : 
   have hyb: f y = f (y - n • T) := (hp.sub_zsmul_eq n).symm
   rw [hxa, hyb]
   apply h (x - n • T) _ (y - n • T)
-  rw [Real.dist_eq, abs_lt] at hxy
-  constructor <;> linarith [ha.1, ha.2]
-  rw [Real.dist_eq,zsmul_eq_mul, sub_sub_sub_cancel_right, ← Real.dist_eq]
-  exact hxy.trans_le h1
+  on_goal 1 => rw [Real.dist_eq, abs_lt] at hxy
   constructor <;> linarith [ha.1, ha.2]
+  · rw [Real.dist_eq,zsmul_eq_mul, sub_sub_sub_cancel_right, ← Real.dist_eq]
+    exact hxy.trans_le h1
+  · constructor <;> linarith [ha.1, ha.2]
 
 
 lemma fourier_uniformContinuous {n : ℤ} :

Carleson/Classical/CarlesonOnTheRealLine.lean

@@ -191,16 +191,19 @@ lemma oscillation_control {x : ℝ} {r : ℝ} {f g : Θ ℝ} :
     _ ≤ 2 * r * |↑f - ↑g| := by
       apply Real.iSup_le
       --TODO: investigate strange (delaborator) behavior - why is there still a sup?
-      intro z
-      apply Real.iSup_le
+      on_goal 1 => intro z
+      on_goal 1 => apply Real.iSup_le
       · intro hz
-        simp at hz
+        simp only [Set.mem_prod, mem_ball] at hz
         rw [Real.dist_eq, Real.dist_eq] at hz
         rw [Real.norm_eq_abs]
         calc |(f - g) * (z.1 - x) - (f - g) * (z.2 - x)|
         _ ≤ |(f - g) * (z.1 - x)| + |(f - g) * (z.2 - x)| := by apply abs_sub
         _ = |↑f - ↑g| * |z.1 - x| + |↑f - ↑g| * |z.2 - x| := by congr <;> apply abs_mul
-        _ ≤ |↑f - ↑g| * r + |↑f - ↑g| * r := by gcongr; linarith [hz.1]; linarith [hz.2]
+        _ ≤ |↑f - ↑g| * r + |↑f - ↑g| * r := by
+          gcongr
+          · linarith [hz.1]
+          · linarith [hz.2]
         _ = 2 * r * |↑f - ↑g| := by ring
       all_goals
       repeat
@@ -227,20 +230,20 @@ lemma frequency_ball_doubling {x₁ x₂ r : ℝ} {f g : Θ ℝ} : dist_{x₂, 2
   rw [dist_integer_linear_eq, dist_integer_linear_eq]
   by_cases r_nonneg : r ≥ 0
   · rw [max_eq_left, max_eq_left]
-    ring_nf;rfl
+    · ring_nf; rfl
     all_goals linarith [r_nonneg]
   · rw [max_eq_right, max_eq_right]
-    simp
+    · simp
     all_goals linarith [r_nonneg]
 
   theorem frequency_ball_growth {x₁ x₂ r : ℝ} {f g : Θ ℝ} : 2 * dist_{x₁, r} f g ≤ dist_{x₂, 2 * r} f g := by
     rw [dist_integer_linear_eq, dist_integer_linear_eq]
     by_cases r_nonneg : r ≥ 0
     · rw [max_eq_left, max_eq_left]
-      ring_nf;rfl
+      · ring_nf; rfl
       all_goals linarith [r_nonneg]
     · rw [max_eq_right, max_eq_right]
-      simp
+      · simp
       all_goals linarith [r_nonneg]
 
 lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
@@ -269,7 +272,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
     simp only [Set.mem_univ, mem_ball, true_implies]
     rw [dist_integer_linear_eq]
     convert R'pos
-    simp
+    simp only [mul_eq_zero, OfNat.ofNat_ne_zero, max_eq_right_iff, false_or, abs_eq_zero]
     left
     exact Rpos
   push_neg at Rpos
@@ -303,7 +306,7 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
         exact Rpos.le
       _ = 2 * R * (m₁ - ↑φ) := by
         rw [abs_of_nonpos]
-        simp only [neg_sub]
+        on_goal 1 => simp only [neg_sub]
         norm_cast
         simp only [tsub_le_iff_right, zero_add, Int.cast_le]
         rwa [m₁def, Int.le_floor]
@@ -356,9 +359,9 @@ lemma integer_ball_cover {x : ℝ} {R R' : ℝ} {f : WithFunctionDistance x R}:
   calc 2 * max R 0 * |↑φ - ↑m₃|
     _ = 2 * R * (↑φ - ↑m₃) := by
       rw [abs_of_nonneg]
-      congr
-      rw [max_eq_left_iff]
-      exact Rpos.le
+      · congr
+        rw [max_eq_left_iff]
+        exact Rpos.le
       simp only [sub_nonneg, Int.cast_le]
       rwa [m₃def, Int.ceil_le]
     _ = 2 * R * (φ - f) + 2 * R * (f - m₃) := by ring
@@ -450,9 +453,9 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
             simp
           rw [dist_eq_norm, ← div_le_iff₀ (dist_pos.mpr hxy), Ldef, NNReal.coe_mk]
           apply le_ciSup_of_le _ x
-          apply le_ciSup_of_le _ y
-          apply le_ciSup_of_le _ hxy
-          rfl
+          on_goal 1 => apply le_ciSup_of_le _ y
+          on_goal 1 => apply le_ciSup_of_le _ hxy
+          · rfl
           · use K
             rw [upperBounds]
             simp only [ne_eq, Set.mem_range, exists_prop, and_imp,
@@ -499,8 +502,8 @@ instance real_van_der_Corput : IsCancellative ℝ (defaultτ 4) where
           linarith [pi_le_four]
         · unfold iLipNorm
           gcongr
-          apply le_of_eq Bdef
-          apply le_of_eq Ldef
+          · apply le_of_eq Bdef
+          · apply le_of_eq Ldef
         · rw [← Real.rpow_neg_one]
           apply Real.rpow_le_rpow_of_exponent_le _ (by norm_num)
           simp only [Int.cast_abs, Int.cast_sub, le_add_iff_nonneg_right]
@@ -562,7 +565,9 @@ instance isTwoSidedKernelHilbert : IsTwoSidedKernel 4 K where
    Note: we can simplify the proof in the blueprint by using real interpolation
    `MeasureTheory.exists_hasStrongType_real_interpolation`.
 -/
-lemma Hilbert_strong_2_2 : ∀ r > 0, HasBoundedStrongType (CZOperator K r) 2 2 volume volume (C_Ts 4) := sorry
+lemma Hilbert_strong_2_2 :
+    ∀ r > 0, HasBoundedStrongType (CZOperator K r) 2 2 volume volume (C_Ts 4) :=
+  sorry
 
 
 local notation "T" => carlesonOperatorReal K
@@ -592,7 +597,8 @@ lemma rcarleson {F G : Set ℝ} (hF : MeasurableSet F) (hG : MeasurableSet G)
     (f : ℝ → ℂ) (hmf : Measurable f) (hf : ∀ x, ‖f x‖ ≤ F.indicator 1 x) :
     ∫⁻ x in G, T f x ≤
     ENNReal.ofReal (C10_0_1 4 2) * (volume G) ^ (2 : ℝ)⁻¹ * (volume F) ^ (2 : ℝ)⁻¹ := by
-  have conj_exponents : Real.IsConjExponent 2 2 := by rw [Real.isConjExponent_iff_eq_conjExponent] <;> norm_num
+  have conj_exponents : Real.IsConjExponent 2 2 := by
+    rw [Real.isConjExponent_iff_eq_conjExponent] <;> norm_num
   calc ∫⁻ x in G, T f x
     _ ≤ ∫⁻ x in G, carlesonOperator K f x :=
       lintegral_mono (carlesonOperatorReal_le_carlesonOperator _)

Carleson/Classical/CarlesonOperatorReal.lean

@@ -28,7 +28,7 @@ lemma annulus_real_eq {x r R: ℝ} (r_nonneg : 0 ≤ r) : {y | dist x y ∈ Set.
 lemma annulus_real_volume {x r R : ℝ} (hr : r ∈ Set.Icc 0 R) :
     volume {y | dist x y ∈ Set.Ioo r R} = ENNReal.ofReal (2 * (R - r)) := by
   rw [annulus_real_eq hr.1, measure_union _ measurableSet_Ioo, Real.volume_Ioo, Real.volume_Ioo, ← ENNReal.ofReal_add (by linarith [hr.2]) (by linarith [hr.2])]
-  ring_nf
+  · ring_nf
   rw [Set.disjoint_iff]
   intro y hy
   linarith [hy.1.2, hy.2.1, hr.1]
@@ -152,9 +152,9 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
         simp only [Set.mem_Ioo]
         by_cases h : dist x y < 1
         · rw [Set.indicator_apply, ite_cond_eq_true, Set.indicator_apply, ite_cond_eq_true]
-          · simp
+          · simp only [Set.mem_setOf_eq, eq_iff_iff, iff_true]
             use ht
-          · simp
+          · simp only [Set.mem_setOf_eq, eq_iff_iff, iff_true]
             use hs
         · push_neg at h
           rw [Set.indicator_apply, ite_cond_eq_false, Set.indicator_apply, ite_cond_eq_false]
@@ -168,17 +168,17 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
         simp only [Set.restrict_apply, Subtype.forall]
         intro s hs t ht
         rw [Fdef]
-        simp
+        simp only [Set.mem_Ioo]
         rw [Set.indicator_apply, ite_cond_eq_false, Set.indicator_apply, ite_cond_eq_false]
         · rw [Set.mem_Ioi, min_lt_iff] at ht
-          simp
+          simp only [Set.mem_setOf_eq, eq_iff_iff, iff_false, not_and, not_lt]
           intro h
           rcases ht with h' | h'
           · exfalso
             exact (lt_self_iff_false _).mp (h'.trans h)
           · exact (h'.trans h).le
         · rw [Set.mem_Ioi, min_lt_iff] at hs
-          simp
+          simp only [Set.mem_setOf_eq, eq_iff_iff, iff_false, not_and, not_lt]
           intro h
           rcases hs with h' | h'
           · exfalso
@@ -198,7 +198,8 @@ lemma carlesonOperatorReal_measurable {f : ℝ → ℂ} (f_measurable : Measurab
           rw [Set.mem_setOf_eq, not_not]
           exact contOn y r hy.symm
         rw [Real.dist_eq, abs_eq hr.1.le] at this
-        simp
+        simp only [Finset.coe_insert, Finset.coe_singleton, Set.mem_insert_iff,
+          Set.mem_singleton_iff]
         rcases this with h | h
         · left; linarith
         · right; linarith

Carleson/Classical/ClassicalCarleson.lean

@@ -32,7 +32,7 @@ theorem exceptional_set_carleson {f : ℝ → ℂ}
   have h_periodic : h.Periodic (2 * π) := periodic_f₀.sub periodic_f
   have h_bound : ∀ x, ‖h x‖ ≤ ε' := by
     intro x
-    simp [hdef]
+    simp only [hdef, Pi.sub_apply, Complex.norm_eq_abs]
     rw [← Complex.dist_eq, dist_comm, Complex.dist_eq]
     exact hf₀ x