awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
zero :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
        (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
        ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))

Tactic:
rw [ENNReal.mul_div_cancel hc_pos.ne' hc_lt_top.ne]

Premises used: LT.lt.ne', ENNReal.mul_div_cancel, LT.lt.ne
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)

Tactic:
le_of_eq ?_

Premises used: le_of_eq
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
zero :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} ≤
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)

Tactic:
refine le_of_eq ?_

Premises used: le_of_eq
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
funProp : inst_3 ≤ inst_3
funProp₁ : MeasurableEmbedding (β := ℝ) fun (a : E) ↦ ‖a‖
⊢ Measurable.{u_1, 0} (α := E) norm

Tactic:
fun_prop
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
⊢ Measurable (β := ℝ) fun (x : E) ↦ a

Tactic:
fun_prop
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
zero :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) {a_1 : E | ‖a_1‖ ≤ a}ᶜ : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)

Tactic:
rw [← prob_compl_eq_one_sub (measurableSet_le (by fun_prop) (by fun_prop))]

Premises used: measurableSet_le, MeasureTheory.prob_compl_eq_one_sub
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
zero : ∀ (x : E), a < ‖x‖ ↔ x ∉ {a_1 : E | ‖a_1‖ ≤ a}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | a < ‖x‖} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) {a_1 : E | ‖a_1‖ ≤ a}ᶜ : ℝ≥0∞)

Tactic:
congr with x
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
x : E
⊢ a < ‖x‖ ↔ x ∉ {a_1 : E | ‖a_1‖ ≤ a}

Tactic:
simp
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
n : ℕ
hn :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
          ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ^
        HPow.hPow (α := ℕ) 2 n)
⊢ HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} : ℝ≥0∞) 2

Tactic:
have h_mul_le : c * μ {x | normThreshold a (n + 1) < ‖x‖}
        ≤ μ {x | normThreshold a n < ‖x‖} ^ 2 :=
      measure_le_mul_measure_gt_normThreshold_le_of_map_rotation_eq_self h_rot _ _
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
n : ℕ
hn :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
          ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ^
        HPow.hPow (α := ℕ) 2 n)
h_mul_le :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} : ℝ≥0∞) 2
rw :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} =
    HMul.hMul (β := ℝ≥0∞) (c⁻¹ * c) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞)
rw₁ :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞)
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} =
    c⁻¹ * HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞)

Tactic:
rw [← mul_assoc, ENNReal.inv_mul_cancel hc_pos.ne' hc_lt_top.ne, one_mul]

Premises used: mul_assoc, LT.lt.ne', ENNReal.inv_mul_cancel, one_mul, LT.lt.ne
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
n : ℕ
hn :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
          ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ^
        HPow.hPow (α := ℕ) 2 n)
h_mul_le :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} : ℝ≥0∞) 2
⊢ c⁻¹ * HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞) ≤
    c⁻¹ * HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} : ℝ≥0∞) 2

Tactic:
gcongr
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
n : ℕ
hn :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
          ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ^
        HPow.hPow (α := ℕ) 2 n)
h_mul_le :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} : ℝ≥0∞) 2
⊢ c⁻¹ * HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} : ℝ≥0∞) 2 ≤
    c⁻¹ * HPow.hPow (β := ℕ) (c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2

Tactic:
gcongr
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
n : ℕ
hn :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
          ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ^
        HPow.hPow (α := ℕ) 2 n)
h_mul_le :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} : ℝ≥0∞) 2
rw :
  c⁻¹ * (HPow.hPow (β := ℕ) c 2 * HPow.hPow (β := ℕ) (((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2) =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
rw₁ :
  c⁻¹ * (HPow.hPow (β := ℕ) c 2 * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * 2)) =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
rw₂ :
  c⁻¹ * HPow.hPow (β := ℕ) c 2 * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * 2) =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
rw₃ : c⁻¹ * (c * c) * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * 2) = c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
rw₄ : c⁻¹ * c * c * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * 2) = c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
rw₅ : 1 * c * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * 2) = c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
rw₆ : c * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * 2) = c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
rw₇ :
  c * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * 2) =
    c * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * HPow.hPow (α := ℕ) (β := ℕ) 2 1)
rw₈ rw₉ : c * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * 2) = c * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * 2)
⊢ c⁻¹ * HPow.hPow (β := ℕ) (c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2 =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)

Tactic:
rw [mul_pow, ← pow_mul, ← mul_assoc, pow_two, ← mul_assoc,
        ENNReal.inv_mul_cancel hc_pos.ne' hc_lt_top.ne, one_mul, pow_add, pow_one]

Premises used: pow_two, mul_assoc, pow_add, pow_mul, LT.lt.ne', pow_one, ENNReal.inv_mul_cancel, mul_pow, one_mul, LT.lt.ne
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
hc_lt_top : c < ∞
n : ℕ
hn :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
          ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ^
        HPow.hPow (α := ℕ) 2 n)
h_mul_le :
  HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} : ℝ≥0∞) 2
calc :
  (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} =
    c⁻¹ * HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞)
calc₁ :
  c⁻¹ * HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞) ≤
    c⁻¹ * HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} : ℝ≥0∞) 2
calc₂ :
  c⁻¹ * HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} : ℝ≥0∞) 2 ≤
    c⁻¹ * HPow.hPow (β := ℕ) (c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2
calc₃ :
  c⁻¹ * HPow.hPow (β := ℕ) (c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2 =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (HDiv.hDiv (β := ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))
          ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ^
        HPow.hPow (α := ℕ) 2 (n + 1))

Tactic:
calc μ {x | normThreshold a (n + 1) < ‖x‖}
    _ = c⁻¹ * (c * μ {x | normThreshold a (n + 1) < ‖x‖}) := by
      rw [← mul_assoc, ENNReal.inv_mul_cancel hc_pos.ne' hc_lt_top.ne, one_mul]
    _ ≤ c⁻¹ * μ {x | normThreshold a n < ‖x‖} ^ 2 := by gcongr
    _ ≤ c⁻¹ * (c * ((1 - c) / c) ^ 2 ^ n) ^ 2 := by gcongr
    _ = c * ((1 - c) / c) ^ 2 ^ (n + 1) := by
      rw [mul_pow, ← pow_mul, ← mul_assoc, pow_two, ← mul_assoc,
        ENNReal.inv_mul_cancel hc_pos.ne' hc_lt_top.ne, one_mul, pow_add, pow_one]

Premises used: Norm.norm, HMul.hMul, setOf, HSub.hSub, HDiv.hDiv, ProbabilityTheory.Fernique.normThreshold, HPow.hPow, HAdd.hAdd, LT.lt, OfNat.ofNat, DFunLike.coe
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
⊢ LT.lt (α := ℝ≥0∞) 0 2⁻¹

Tactic:
simp
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
⊢ 0 < c

Tactic:
have hc_pos : 0 < c := lt_of_lt_of_le (by simp) ha_gt.le
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_pos : 0 < c
⊢ c < 1

Tactic:
replace hc_lt : c < 1 := ha_lt
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
⊢ c < ∞

Tactic:
have hc_lt_top : c < ∞ := measure_lt_top _ _
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
⊢ LT.lt (α := ℝ≥0∞) 1 2

Tactic:
simp
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
⊢ 1 - c < ∞

Tactic:
have hc_one_sub_lt_top : 1 - c < ∞ := lt_top_of_lt (b := 2) (tsub_le_self.trans_lt (by simp))
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
rw : 0 < c.toReal
rw₁ : 0 < (1 - c).toReal
⊢ 0 < (c / (1 - c)).toReal

Tactic:
rw [ENNReal.toReal_div, div_pos_iff_of_pos_right]

Premises used: div_pos_iff_of_pos_right, ENNReal.toReal_div
-- 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
a : ℝ
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
ha_gt : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
ha_lt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
⊢ 0 < c.toReal

Tactic:
simp [ENNReal.toReal_pos_iff, hc_pos, hc_lt_top]

Premises used: ENNReal.toReal_pos_iff