-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
calc :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | b < ‖x‖} : ℝ≥0∞) =
    (μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) (SProd.sprod (α := Set E) (β := Set E) {x : E | ‖x‖ ≤ a} {y : E | b < ‖y‖})
calc₁ :
  Eq (α := ℝ≥0∞) ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} : ℝ≥0∞)
    (((Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) : Measure (E × E)) :
          (a : Set (E × E)) → ℝ≥0∞)
        {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} :
      ℝ≥0∞)
calc₂ :
  Eq (α := ℝ≥0∞)
    (((Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) : Measure (E × E)) :
          (a : Set (E × E)) → ℝ≥0∞)
        {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} :
      ℝ≥0∞)
    ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2} : ℝ≥0∞)
calc₃ :
  LE.le (α := ℝ≥0∞)
    ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2} : ℝ≥0∞)
    ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖} : ℝ≥0∞)
calc₄ :
  (μ.prod μ : (a : Set (E × E)) → ℝ≥0∞)
      (SProd.sprod (α := Set E) (β := Set E) {x : E | (b - a) / √2 < ‖x‖} {y : E | (b - a) / √2 < ‖y‖}) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞) 2
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | b < ‖x‖} : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞) 2

Tactic:
calc μ {x | ‖x‖ ≤ a} * μ {x | b < ‖x‖}
  _ = (μ.prod μ) ({x | ‖x‖ ≤ a} ×ˢ {y | b < ‖y‖}) := by rw [Measure.prod_prod]
    -- This is the measure of two bands in the plane (draw a picture!)
  _ = (μ.prod μ) {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} := rfl
  _ = ((μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4)))) {p | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} := by
    -- We can rotate the bands since `μ.prod μ` is invariant under rotation
    rw [h]
  _ = (μ.prod μ) {p | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2} := by
    rw [Measure.map_apply (by fun_prop)]
    swap
    · refine MeasurableSet.inter ?_ ?_
      · change MeasurableSet {p : E × E | ‖p.1‖ ≤ a}
        exact measurableSet_le (by fun_prop) (by fun_prop)
      · change MeasurableSet {p : E × E | b < ‖p.2‖}
        exact measurableSet_lt (by fun_prop) (by fun_prop)
    congr 1
    simp only [Set.preimage_setOf_eq, ContinuousLinearMap.rotation_apply, Real.cos_neg,
      Real.cos_pi_div_four, Real.sin_neg, Real.sin_pi_div_four, neg_smul, neg_neg]
    have h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹ := by
      simp only [norm_mul, norm_inv, Real.norm_ofNat, Real.norm_eq_abs]
      rw [abs_of_nonneg (by positivity)]
      nth_rw 1 [← Real.sq_sqrt (by simp : (0 : ℝ) ≤ 2)]
      rw [pow_two, mul_inv, mul_assoc, inv_mul_cancel₀ (by positivity), mul_one]
    congr! with p
    · rw [← sub_eq_add_neg, ← smul_sub, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
    · rw [← smul_add, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
  _ ≤ (μ.prod μ) {p | (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖} := by
    -- The rotated bands are contained in quadrants.
    refine measure_mono fun p ↦ ?_
    simp only [Set.mem_setOf_eq, and_imp]
    intro hp1 hp2
    suffices (b - a) / √2 < min ‖p.1‖ ‖p.2‖ from lt_min_iff.mp this
    calc (b - a) / √2
    _ < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 := by
      suffices b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2 by
        calc (b - a) / √2 < (‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2) / √2 := by gcongr
        _ = (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 := by
          field_simp; rw [Real.sq_sqrt (by positivity)]; ring
      calc b - a < ‖p.1 + p.2‖ / √2 - a := by gcongr
      _ ≤ ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2 := by gcongr
    _ ≤ min ‖p.1‖ ‖p.2‖ := by
      have := norm_add_sub_norm_sub_le_two_mul_min p.1 p.2
      linarith
  _ = (μ.prod μ) ({x | (b - a) / √2 < ‖x‖} ×ˢ {y | (b - a) / √2 < ‖y‖}) := rfl
  _ ≤ μ {x | (b - a) / √2 < ‖x‖} ^ 2 := by rw [Measure.prod_prod, pow_two]

Premises used: Norm.norm, Real.pi, SProd.sprod, setOf, HSub.hSub, HDiv.hDiv, ContinuousLinearMap.rotation, LE.le, Prod.fst, And, MeasureTheory.Measure.prod, HAdd.hAdd, MeasureTheory.Measure.map, LT.lt, Real.sqrt, OfNat.ofNat, Prod.snd, DFunLike.coe, Neg.neg, rfl