-- Module: Mathlib.MeasureTheory.Measure.IntegralCharFun
Goal:
μ : Measure ℝ
r : ℝ
inst : IsProbabilityMeasure μ
hr : 0 < r
integrable_sinc_const_mul : ∀ (r : ℝ), Integrable (ε := ℝ) (fun (x : ℝ) ↦ sinc (r * x)) μ
calc : μ.real {x : ℝ | r < |x|} = μ.real {x : ℝ | 2 < |2 * r⁻¹ * x|}
calc₁ : μ.real {x : ℝ | 2 < |2 * r⁻¹ * x|} = ∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ
calc₂ :
  ∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 ∂μ =
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ)
calc₃ :
  HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ) ≤
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ)
calc₄ :
  HMul.hMul (α := ℝ) 2 (∫ (x : ℝ) in {x : ℝ | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ) ≤
    HMul.hMul (α := ℝ) 2 (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ)
calc₅ :
  HMul.hMul (α := ℝ) 2 (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ) ≤
    2 * Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ)
calc₆ :
  2 * Norm.norm (E := ℝ) (∫ (x : ℝ), 1 - sinc (2 * r⁻¹ * x) ∂μ) =
    2⁻¹ * r * ‖2 * (↑r : ℂ)⁻¹ + 2 * (↑r⁻¹ : ℂ) - 2 * (2 * (↑r⁻¹ : ℂ)) * (↑(∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ) : ℂ)‖
calc₇ :
  2⁻¹ * r * ‖2 * (↑r : ℂ)⁻¹ + 2 * (↑r⁻¹ : ℂ) - 2 * (2 * (↑r⁻¹ : ℂ)) * (↑(∫ (x : ℝ), sinc (2 * r⁻¹ * x) ∂μ) : ℂ)‖ =
    2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ t)
⊢ μ.real {x : ℝ | r < |x|} ≤ 2⁻¹ * r * Norm.norm (E := ℂ) (∫ (t : ℝ) in -2 * r⁻¹..2 * r⁻¹, 1 - charFun μ t)

Tactic:
calc μ.real {x | r < |x|}
  _ = μ.real {x | 2 < |2 * r⁻¹ * x|} := by
    congr 1 with x
    simp only [Set.mem_setOf_eq, abs_mul, Nat.abs_ofNat]
    rw [abs_of_nonneg (a := r⁻¹) (by positivity), mul_assoc, ← inv_mul_lt_iff₀ (by positivity),
      inv_mul_cancel₀ (by positivity), lt_inv_mul_iff₀ (by positivity), mul_one]
  _ = ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 1 ∂μ := by simp
  _ = 2 * ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 2⁻¹ ∂μ := by
    rw [← integral_const_mul]
    congr with _
    rw [mul_inv_cancel₀ (by positivity)]
  _ ≤ 2 * ∫ x in {x | 2 < |2 * r⁻¹ * x|}, 1 - sinc (2 * r⁻¹ * x) ∂μ := by
    gcongr (2 : ℝ) * ?_
    refine setIntegral_mono_on ?_
      ((integrable_const _).sub (integrable_sinc_const_mul _)).integrableOn ?_ fun x hx ↦ ?_
    · exact Integrable.integrableOn <| by fun_prop
    · exact MeasurableSet.preimage measurableSet_Ioi (by fun_prop)
    · have hx_ne : 2 * r⁻¹ * x ≠ 0 := by
        intro hx0
        simp only [hx0, Set.mem_setOf_eq, abs_zero] at hx
        linarith
      rw [le_sub_iff_add_le, ← le_sub_iff_add_le']
      norm_num
      rw [one_div]
      refine (sinc_le_inv_abs hx_ne).trans ?_
      exact (inv_le_inv₀ (by positivity) (by positivity)).mpr (le_of_lt hx)
  _ ≤ 2 * ∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ := by
    grw [setIntegral_le_integral (by fun_prop) <| ae_of_all _ fun x ↦ ?_]
    simp only [Pi.zero_apply, sub_nonneg]
    exact sinc_le_one (2 * r⁻¹ * x)
  _ ≤ 2 * ‖∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ‖ := by
    gcongr
    exact Real.le_norm_self _
  _ = 2⁻¹ * r *
      ‖2 * (r : ℂ)⁻¹ + 2 * r⁻¹ - 2 * (2 * r⁻¹) * ∫ x, sinc (2 * r⁻¹ * x) ∂μ‖ := by
    norm_cast
    rw [← two_mul, mul_assoc 2, ← mul_sub, norm_mul, Real.norm_ofNat, ← mul_assoc,
      ← mul_one_sub, norm_mul, Real.norm_of_nonneg (r := 2 * r⁻¹) (by positivity), ← mul_assoc]
    congr
    · ring_nf
      rw [mul_inv_cancel₀ (by positivity), one_mul]
    · rw [integral_sub (integrable_const _) (integrable_sinc_const_mul _)]
      simp
  _ = 2⁻¹ * r * ‖∫ t in (-2 * r⁻¹)..(2 * r⁻¹), 1 - charFun μ t‖ := by
    rw [intervalIntegral.integral_sub intervalIntegrable_const intervalIntegrable_charFun, neg_mul,
      integral_charFun_Icc (by positivity)]
    simp

Premises used: HMul.hMul, abs, setOf, MeasureTheory.Measure.real, Complex.ofReal, Inv.inv, LT.lt, OfNat.ofNat, Neg.neg