Find the Lean result you need, then inspect the actual proof.

theorem PFR_conjecture (hA₀ : A.Nonempty) (hA : (A + A).ncard ≤ K * A.ncard) :     ∃ (H : Submodule (ZMod 2) G) (c : Set G),      Nat.card c < 2 * K ^ 12 ∧ (H : Set G).ncard ≤ A.ncard ∧ A ⊆ c + H := by  obtain ⟨A_pos, -, K_pos⟩ : (0 : ℝ) < A.ncard ∧ (0 : ℝ) < (A + A).ncard ∧ 0 < K :=    PFR_conjecture_pos_aux' A.toFinite hA₀ hA  -- consider the subgroup `H` given by Lemma `PFR_conjecture_aux`.  obtain ⟨H, c, hc, IHA, IAH, A_subs_cH⟩ : ∃ (H : Submodule (ZMod 2) G) (c : Set G),    Nat.card c ≤ K ^ (13/2) * A.ncard ^ (1/2) * (H : Set G).ncard ^ (-1/2)      ∧ (H : Set G).ncard ≤ K ^ 11 * A.ncard ∧ A.ncard ≤ K ^ 11 * (H : Set G).ncard      ∧ A ⊆ c + H :=    PFR_conjecture_aux hA₀ hA  have H_pos : (0 : ℝ) < (H : Set G).ncard := by    have : 0 < (H : Set G).ncard := Nat.card_pos; positivity  rcases le_or_gt ((H : Set G).ncard) A.ncard with h|h  -- If `#H ≤ #A`, then `H` satisfies the conclusion of the theorem  · refine ⟨H, c, ?_, h, A_subs_cH⟩    calc    Nat.card c ≤ K ^ (13/2 : ℝ) * A.ncard ^ (1/2 : ℝ) * (H : Set G).ncard ^ (-1/2 : ℝ) := hc    _ ≤ K ^ (13/2 : ℝ) * (K ^ 11 * (H : Set G).ncard) ^ (1/2) * (H : Set G).ncard ^ (-1/2 : ℝ) := by      gcongr    _ = K ^ 12 := by rpow_ring; norm_num    _ < 2 * K ^ 12 := by linarith [show 0 < K ^ 12 by positivity]  -- otherwise, we decompose `H` into cosets of one of its subgroups `H'`, chosen so that  -- `#A / 2 < #H' ≤ #A`. This `H'` satisfies the desired conclusion.  · obtain ⟨H', IH'A, IAH', H'H⟩ : ∃ H' : Submodule (ZMod 2) G, Nat.card H' ≤ A.ncard          ∧ A.ncard < 2 * Nat.card H' ∧ H' ≤ H := by      have A_pos' : 0 < A.ncard := mod_cast A_pos      exact ZModModule.exists_submodule_subset_card_le Nat.prime_two H h.le A_pos'.ne'    have : (A.ncard / 2 : ℝ) < Nat.card H' := by      rw [div_lt_iff₀ zero_lt_two, mul_comm]; norm_cast    have H'_pos : (0 : ℝ) < Nat.card H' := by      have : 0 < Nat.card H' := Nat.card_pos; positivity    obtain ⟨u, HH'u, hu⟩ :=      H'.toAddSubgroup.exists_left_transversal_of_le (H := H.toAddSubgroup) H'H    dsimp at HH'u    refine ⟨H', c + u, ?_, IH'A, by rwa [add_assoc, HH'u]⟩    calc    (Nat.card (c + u) : ℝ)      ≤ Nat.card c * Nat.card u := mod_cast natCard_add_le    _ ≤ (K ^ (13/2 : ℝ) * A.ncard ^ (1 / 2 : ℝ) * ((H : Set G).ncard ^ (-1 / 2 : ℝ)))          * ((H : Set G).ncard / Nat.card H') := by        gcongr        apply le_of_eq        rw [eq_div_iff H'_pos.ne']        norm_cast    _ < (K ^ (13/2) * A.ncard ^ (1 / 2) * ((H : Set G).ncard ^ (-1 / 2)))          * ((H : Set G).ncard / (A.ncard / 2)) := by        gcongr    _ = 2 * K ^ (13/2) * A.ncard ^ (-1/2) * (H : Set G).ncard ^ (1/2) := by        field_simp        rpow_ring        norm_num    _ ≤ 2 * K ^ (13/2) * A.ncard ^ (-1/2) * (K ^ 11 * A.ncard) ^ (1/2) := by        gcongr    _ = 2 * K ^ 12 := by        rpow_ring        norm_num

theorem classical_carleson {f : ℝ → ℂ} (cont_f : Continuous f) (periodic_f : f.Periodic (2 * π)) :    ∀ᵐ x, Tendsto (S_ · f x) atTop (𝓝 (f x)) := by  -- Reduce to a.e. convergence on [0,2π]  apply @Function.Periodic.ae_of_ae_restrict _ two_pi_pos 0  · rw [Function.Periodic]    intro x    conv => pattern S_ _ _ _; rw [partialFourierSum_periodic]    conv => pattern f _; rw [periodic_f]  apply ae_restrict_of_ae_eq_of_ae_restrict Ico_ae_eq_Icc.symm  rw [zero_add]  -- Show a.e. convergence on [0,2π]  rw [Measure.restrict_congr_set Ioc_ae_eq_Icc.symm]  exact carleson_interval' cont_f periodic_f

lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ ∧ x ∈ A - A ∧ x ∈ f.support)    (hB : (B₁ ∩ B₂).Nonempty) (hA : A.Nonempty) :    ∃ A₁, A₁ ⊆ B₁ ∧ ∃ A₂, A₂ ⊆ B₂ ∧      ⟪μ_[ℝ] A₁ ○ᵈ μ A₂, (↑) ∘ f⟫_[ℝ] * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ p        ≤ 2 * ∑ x, (μ B₁ ○ᵈ μ B₂) x * (𝟭_[A, ℝ] ○ᵈ 𝟭_[A]) x ^ p * f x ∧      (4 : ℝ) ⁻¹ * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ (2 * p) / #A ^ (2 * p)        ≤ #A₁ / #B₁ ∧      (4 : ℝ) ⁻¹ * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ (2 * p) / #A ^ (2 * p)        ≤ #A₂ / #B₂ := by  have := hB.mono inter_subset_left  have := hB.mono inter_subset_right  have hp₀ : p ≠ 0 := by positivity  have := dLpNorm_ddconv_pos hp₀ hB hA  set M : ℝ :=    2 ⁻¹ * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ p * (sqrt #B₁ * sqrt #B₂) / #A ^ p      with hM_def  have hM : 0 < M := by rw [hM_def]; positivity  replace hf : 0 < ∑ x, (μ_[ℝ] B₁ ○ᵈ μ B₂) x * (𝟭_[A] ○ᵈ 𝟭_[A]) x ^ p * f x := by    have : 0 ≤ μ_[ℝ] B₁ ○ᵈ μ B₂ * (𝟭_[A] ○ᵈ 𝟭_[A]) ^ p * (↑) ∘ f := -- positivity      mul_nonneg (mul_nonneg (dddconv_nonneg mu_nonneg mu_nonneg) <| pow_nonneg        (dddconv_nonneg Set.indicator_one_nonneg Set.indicator_one_nonneg) _) fun _ ↦ by simp    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_dddconv,      Set.indicator_one_nonneg, mu_nonneg, Set.support_indicator_one, 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  set g : (Fin p → G) → ℝ := fun s ↦ #(A₁ s) * #(A₂ s) with hg_def  have hg : ∀ s, 0 ≤ g s := fun s ↦ by rw [hg_def]; dsimp; positivity  have hgB : ∑ s, g s = #B₁ * #B₂ * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ p := by    have hAdddconv : 0 ≤ 𝟭_[(A : Set G), ℝ] ○ᵈ 𝟭_[A] :=      dddconv_nonneg Set.indicator_one_nonneg Set.indicator_one_nonneg    simpa only [wLpNorm_pow_eq_sum_norm hp₀, norm_of_nonneg (hAdddconv _), NNReal.smul_def,      NNReal.coe_dddconv, NNReal.coe_comp_mu, wInner_one_eq_sum, Pi.one_apply, inner_apply',      ← coe_inter, conj_to_real, mul_one, sum_dddconv, sum_indicator_one, nsmul_eq_mul,      Nat.cast_mul, g, A₁, A₂] using! lemma_0 p B₁ B₂ A 1  suffices ∑ s, ⟪𝟭_[A₁ s, ℝ] ○ᵈ 𝟭_[A₂ s], (↑) ∘ f⟫_[ℝ] * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ p    < ∑ s, 𝟭_[({s | M ^ 2 ≤ g s} : Finset _)] s * g s *        (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 [Set.indicator_apply, boole_mul] at hs    split_ifs at hs with h; swap    · simp only [zero_mul, wInner_one_eq_sum, Function.comp_apply, RCLike.inner_apply',        RCLike.conj_to_real] at hs      have : 0 ≤ 𝟭_[(A₁ s : Set G), ℝ] ○ᵈ 𝟭_[A₂ s] :=        dddconv_nonneg Set.indicator_one_nonneg Set.indicator_one_nonneg      -- positivity      cases hs.not_ge <|        mul_nonneg (sum_nonneg fun x _ ↦ mul_nonneg (this _) <| by positivity) <| by positivity    have : (4 : ℝ) ⁻¹ * ‖𝟭_[A, ℝ] ○ᵈ 𝟭_[A]‖_[p, μ B₁ ○ᵈ μ B₂] ^ (2 * p) / #A ^ (2 * p)      ≤ #(A₁ s) / #B₁ * (#(A₂ s) / #B₂) := by      rw [div_mul_div_comm, le_div_iff₀ (by positivity)]      simpa [hg_def, hM_def, mul_pow, div_pow, pow_mul', show (2 : ℝ) ^ 2 = 4 by norm_num,        mul_div_right_comm] using h    refine ⟨(lt_of_mul_lt_mul_left (hs.trans_eq' ?_) <| hg s).le, this.trans <|      mul_le_of_le_one_right ?_ <| div_le_one_of_le₀ ?_ ?_, this.trans <|      mul_le_of_le_one_left ?_ <| div_le_one_of_le₀ ?_ ?_⟩    · simp_rw [A₁, A₂, g, ← card_smul_mu, smul_dddconv, dddconv_smul, ← Nat.cast_smul_eq_nsmul ℝ,        wInner_smul_left, smul_eq_mul, star_trivial, mul_assoc, A₁, A₂]    any_goals positivity    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 [Set.indicator_apply, boole_mul, mem_coe, mem_filter, mem_univ, true_and, ← sum_filter,    mul_lt_mul_iff_left₀ 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,      filter_true_of_mem fun s hs ↦ h s (mem_filter.1 hs).2, ← sum_filter_ne_zero]    refine lt_mul_of_one_lt_left (sum_pos (fun s hs ↦ (h _ (mem_filter.1 hs).2).trans_lt' <|      by positivity) ?_) one_lt_two    rw [← sum_filter_ne_zero] at hgB    exact nonempty_of_sum_ne_zero <| hgB.trans_ne <| by positivity  push Not at h  obtain ⟨s, hs⟩ := h  suffices h : (2 : ℝ) * ∑ s with g s < M ^ 2, g s < ∑ s, g s by    refine (le_or_lt_of_add_le_add ?_).resolve_left h.not_ge    simp_rw [← not_le, ← compl_filter, ← two_mul, ← mul_add, sum_compl_add_sum]    rfl  rw [← lt_div_iff₀' (zero_lt_two' ℝ), div_eq_inv_mul]  calc    ∑ s with g s < M ^ 2, g s = ∑ s with g s < M ^ 2 ∧ g s ≠ 0, sqrt (g s) * sqrt (g s)          := by simp_rw [mul_self_sqrt (hg _), ← filter_filter, sum_filter_ne_zero]    _ < ∑ s with g s < M ^ 2 ∧ g s ≠ 0, M * sqrt (g s)        := sum_lt_sum_of_nonempty ⟨s, mem_filter.2 ⟨mem_univ _, hs.symm⟩⟩ ?_    _ ≤ ∑ s, M * sqrt (g s) := sum_le_univ_sum_of_nonneg fun s ↦ by positivity    _ = M * (∑ s, sqrt #(A₁ s) * sqrt #(A₂ s))        := by simp_rw [mul_sum, g, sqrt_mul <| Nat.cast_nonneg _]    _ ≤ 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, 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,    ← mul_assoc, hM_def, div_mul_cancel₀, ← sqrt_mul, mul_assoc, mul_self_sqrt, hgB, mul_right_comm,    mul_assoc]  all_goals positivity