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∞)
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 < (1 - c).toReal

Tactic:
simp [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, hc_one_sub_lt_top]

Premises used: ENNReal.toReal_pos_iff, tsub_pos_iff_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
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
⊢ 0 < (c / (1 - c)).toReal

Tactic:
have hc_ratio_pos : 0 < (c / (1 - c)).toReal := by
    rw [ENNReal.toReal_div, div_pos_iff_of_pos_right]
    · simp [ENNReal.toReal_pos_iff, hc_pos, hc_lt_top]
    · simp [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, hc_one_sub_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 < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (ENNReal.ofReal
        (rexp
          (-Real.log
                (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
                    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                      ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
            HPow.hPow (α := ℝ) 2 n)))

Tactic:
(measure_gt_normThreshold_le_rpow h_rot ha_gt n).trans_eq ?_

Premises used: LE.le.trans_eq, ProbabilityTheory.Fernique.measure_gt_normThreshold_le_rpow
-- 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 < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
refine :
  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∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (ENNReal.ofReal
        (rexp
          (-Real.log
                (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
                    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                      ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
            HPow.hPow (α := ℝ) 2 n)))
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a n < ‖x‖} ≤
    HMul.hMul (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (ENNReal.ofReal
        (rexp
          (-Real.log
                (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
                    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                      ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
            HPow.hPow (α := ℝ) 2 n)))

Tactic:
refine (measure_gt_normThreshold_le_rpow h_rot ha_gt n).trans_eq ?_

Premises used: LE.le.trans_eq, ProbabilityTheory.Fernique.measure_gt_normThreshold_le_rpow
-- 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 < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
e_a :
  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 =
    ENNReal.ofReal
      (rexp
        (-Real.log
              (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
                  (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                    ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
          HPow.hPow (α := ℝ) 2 n))
⊢ 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∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      (ENNReal.ofReal
        (rexp
          (-Real.log
                (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
                    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                      ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
            HPow.hPow (α := ℝ) 2 n)))

Tactic:
congr
-- 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 < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ 0 <
    (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal⁻¹

Tactic:
positivity
-- 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 < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ 0 <
    (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
            (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
              ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal⁻¹ ^
      HPow.hPow (α := ℝ) 2 n

Tactic:
positivity
-- 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 < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ 0 ≤
    (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
          (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal⁻¹

Tactic:
positivity
-- 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 < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ 0 ≤ HPow.hPow (α := ℝ) 2 n

Tactic:
positivity
-- 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 < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
e_a :
  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 =
    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
e_a₁ :
  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∞) ≠
    ∞
⊢ 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 =
    ENNReal.ofReal
      (rexp
        (-Real.log
              (HDiv.hDiv (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
                  (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞)
                    ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞))).toReal *
          HPow.hPow (α := ℝ) 2 n))

Tactic:
rw [← Real.log_inv, mul_comm (Real.log _), ← Real.log_rpow (by positivity),
    Real.exp_log (by positivity), ← ENNReal.ofReal_rpow_of_nonneg (by positivity) (by positivity),
    ENNReal.toReal_div, inv_div, ← ENNReal.toReal_div, ENNReal.ofReal_toReal]

Premises used: Real.log_rpow, ENNReal.ofReal_rpow_of_nonneg, ENNReal.ofReal_toReal, Real.exp_log, Real.log, mul_comm, inv_div, Real.log_inv, 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 < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
e_a e_a₁ e_a₂ e_a₃ :
  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 =
    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
⊢ 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 =
    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

Tactic:
norm_cast
-- 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 < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ≠ ∞

Tactic:
finiteness
-- 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 < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ 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}
hc_pos : 0 < c
hc_lt : c < 1
hc_lt_top : c < ∞
hc_one_sub_lt_top : 1 - c < ∞
hc_ratio_pos : 0 < (c / (1 - c)).toReal
⊢ 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:
exact ENNReal.div_ne_top (by finiteness) (lt_trans (by simp) ha_gt).ne'

Premises used: lt_trans, LT.lt.ne', ENNReal.div_ne_top
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 0 < 8 * HPow.hPow (β := ℕ) (1 + √2) 2

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
refine : 1 < c.toReal / (1 - c).toReal
⊢ 0 < logRatio c

Tactic:
refine div_pos (Real.log_pos ?_) (by positivity)

Premises used: Real.log_pos, div_pos
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
rw : 0 < (1 - c).toReal ∧ (1 - c).toReal < c.toReal ∨ (1 - c).toReal < 0 ∧ c.toReal < (1 - c).toReal
⊢ 1 < c.toReal / (1 - c).toReal

Tactic:
rw [one_lt_div_iff]

Premises used: one_lt_div_iff
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 0 < (1 - c).toReal ∧ (1 - c).toReal < c.toReal ∨ (1 - c).toReal < 0 ∧ c.toReal < (1 - c).toReal

Tactic:
Or.inl ⟨?_, ?_⟩

Premises used: And.intro, Or.inl
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
refine_1 : 0 < (1 - c).toReal
refine_2 : (1 - c).toReal < c.toReal
⊢ 0 < (1 - c).toReal ∧ (1 - c).toReal < c.toReal ∨ (1 - c).toReal < 0 ∧ c.toReal < (1 - c).toReal

Tactic:
refine Or.inl ⟨?_, ?_⟩

Premises used: Or.inl
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
refine_1 : 1 - c < ∞
⊢ 0 < (1 - c).toReal

Tactic:
simp only [ENNReal.toReal_pos_iff, tsub_pos_iff_lt, hc_lt, true_and]

Premises used: ENNReal.toReal_pos_iff, tsub_pos_iff_lt, true_and
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 1 - c < ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 1 - c ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ c ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
refine_2 : 1 - c < c
⊢ (1 - c).toReal < c.toReal

Tactic:
refine (ENNReal.toReal_lt_toReal (by finiteness) (by finiteness)).mpr ?_

Premises used: Iff.mpr, ENNReal.toReal_lt_toReal
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 1 - c < c

Tactic:
ENNReal.sub_lt_of_lt_add hc_lt.le ?_

Premises used: LT.lt.le, ENNReal.sub_lt_of_lt_add
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
refine_2 : 1 < c + c
⊢ 1 - c < c

Tactic:
refine ENNReal.sub_lt_of_lt_add hc_lt.le ?_

Premises used: LT.lt.le, ENNReal.sub_lt_of_lt_add
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
refine_2 : 1 < 2 * c
⊢ 1 < c + c

Tactic:
rw [← two_mul]

Premises used: two_mul
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 1 / 2 < c
hc_lt : c < 1
⊢ Ne (α := ℝ≥0∞) 2 0 ∨ Ne (α := ℝ≥0∞) 1 0

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 1 / 2 < c
hc_lt : c < 1
⊢ Ne (α := ℝ≥0∞) 2 ∞ ∨ Ne (α := ℝ≥0∞) 1 ∞

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
refine_2 : ∀ (hc_gt : 1 / 2 < c) (hc_lt : c < 1), 1 < 2 * c
refine_2₁ : ∀ (hc_gt : 1 < c * 2) (hc_lt : c < 1), 1 < 2 * c
refine_2₂ refine_2₃ refine_2₄ refine_2₅ : ∀ (hc_gt : 1 < 2 * c) (hc_lt : c < 1), 1 < 2 * c
⊢ 1 < 2 * c

Tactic:
rwa [inv_eq_one_div, ENNReal.div_lt_iff (by simp) (by simp), mul_comm] at hc_gt

Premises used: inv_eq_one_div, mul_comm, ENNReal.div_lt_iff
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_ge : 2⁻¹ ≤ c
hc_le : c ≤ 1
inl : c = 2⁻¹ → 0 ≤ logRatio c
inr : 2⁻¹ < c → 0 ≤ logRatio c
⊢ 0 ≤ logRatio c

Tactic:
cases hc_ge.eq_or_lt'

Premises used: LE.le.eq_or_lt'
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_ge : 2⁻¹ ≤ c
hc_le : c ≤ 1
h : c = 2⁻¹
⊢ 0 ≤ logRatio c

Tactic:
simp [logRatio, *]

Premises used: ProbabilityTheory.Fernique.logRatio
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_ge : 2⁻¹ ≤ c
hc_le : c ≤ 1
h : 2⁻¹ < c
inr : 1 = c → 0 ≤ logRatio c
inr₁ : c < 1 → 0 ≤ logRatio c
⊢ 0 ≤ logRatio c

Tactic:
cases hc_le.eq_or_lt'

Premises used: LE.le.eq_or_lt'
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_ge : 2⁻¹ ≤ c
hc_le : c ≤ 1
h : 2⁻¹ < c
h_1 : 1 = c
⊢ 0 ≤ logRatio c

Tactic:
simp [logRatio, *]

Premises used: ProbabilityTheory.Fernique.logRatio
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_ge : 2⁻¹ ≤ c
hc_le : c ≤ 1
h : 2⁻¹ < c
h_1 : c < 1
⊢ 0 ≤ logRatio c

Tactic:
(logRatio_pos ‹_› ‹_›).le

Premises used: LT.lt.le, ProbabilityTheory.Fernique.logRatio_pos
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c : ℝ≥0∞
hc_ge : 2⁻¹ ≤ c
hc_le : c ≤ 1
h : 2⁻¹ < c
h_1 : c < 1
⊢ 0 ≤ logRatio c

Tactic:
exact (logRatio_pos ‹_› ‹_›).le

Premises used: LT.lt.le, ProbabilityTheory.Fernique.logRatio_pos
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
hab : 0 < c.toReal / (1 - c).toReal
hab₁ : 0 < (1 - d).toReal
hab₂ : d ≠ ∞
hab₃ : 1 - c ≠ ∞
⊢ Real.log (c.toReal / (1 - c).toReal) / (8 * HPow.hPow (β := ℕ) (1 + √2) 2) ≤
    Real.log (d.toReal / (1 - d).toReal) / (8 * HPow.hPow (β := ℕ) (1 + √2) 2)

Tactic:
gcongr
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < c.toReal / (1 - c).toReal

Tactic:
div_pos ?_ ?_

Premises used: div_pos
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
hab : 0 < c.toReal
hab₁ : 0 < (1 - c).toReal
⊢ 0 < c.toReal / (1 - c).toReal

Tactic:
refine div_pos ?_ ?_

Premises used: div_pos
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
hab : 0 < c ∧ c < ∞
⊢ 0 < c.toReal

Tactic:
rw [ENNReal.toReal_pos_iff]

Premises used: ENNReal.toReal_pos_iff
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ LT.lt (α := ℝ≥0∞) 0 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ d < ∞

Tactic:
finiteness
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
c d : ℝ≥0∞
hc : 2⁻¹ < c
hd : d < 1
h : c ≤ d
⊢ 0 < c ∧ c < ∞

Tactic:
exact ⟨lt_trans (by norm_num) hc, h.trans_lt (by finiteness)⟩