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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
h_ne : ¬∃ (b : ℝ), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)

Tactic:
push Not at h_meas_Ioo h_ne

Premises used: Not
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ¬∃ (a : ℝ),
      0 < a ∧
        LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) ∧
          LT.lt (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (1 : ℝ≥0∞)
h_ne : ¬∃ (b : ℝ), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
h_meas_Ioo₁ :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
⊢ ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
push Not at h_meas_Ioo h_ne

Premises used: Not
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
this : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
⊢ False

Tactic:
simp at this
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
suffices : LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
⊢ False

Tactic:
suffices μ .univ ≤ 2⁻¹ by simp at this
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
a a' : ℝ
ha : 0 < a'
by_contra : ∀ (h_lt : ¬LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)), False
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)

Tactic:
by_contra h_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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
a a' : ℝ
ha : 0 < a'
h_lt : ¬LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
⊢ False

Tactic:
h_ne a' ?_
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
a a' : ℝ
ha : 0 < a'
h_lt : ¬LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
refine : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ False

Tactic:
refine h_ne a' ?_
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
a a' : ℝ
ha : 0 < a'
h_lt : ¬LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
le_antisymm prob_le_one (h_meas_Ioo a' ha (not_le.mp h_lt))

Premises used: not_le, MeasureTheory.prob_le_one, le_antisymm, Iff.mp
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
a a' : ℝ
ha : 0 < a'
h_lt : ¬LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
exact le_antisymm prob_le_one (h_meas_Ioo a' ha (not_le.mp h_lt))

Premises used: not_le, MeasureTheory.prob_le_one, le_antisymm, Iff.mp
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
a : ℝ
⊢ ∀ (a' : ℝ) (ha : 0 < a'), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)

Tactic:
have h_of_pos a' (ha : 0 < a') : μ {x | ‖x‖ ≤ a'} ≤ 2⁻¹ := by
        by_contra h_lt
        refine h_ne a' ?_
        exact le_antisymm prob_le_one (h_meas_Ioo a' ha (not_le.mp h_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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
a : ℝ
h_of_pos : ∀ (a' : ℝ) (ha : 0 < a'), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
inl : ∀ (ha : a ≤ 0), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
inr : ∀ (ha : 0 < a), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)

Tactic:
rcases le_or_gt a 0 with ha | ha

Premises used: le_or_gt, OfNat.ofNat
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
a : ℝ
h_of_pos : ∀ (a' : ℝ) (ha : 0 < a'), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
ha : a ≤ 0
x : E
hx : Membership.mem (γ := Set E) {x : E | ‖x‖ ≤ a} x
⊢ LE.le (α := ℝ) 0 1

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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
a : ℝ
h_of_pos : ∀ (a' : ℝ) (ha : 0 < a'), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
ha : a ≤ 0
⊢ LT.lt (α := ℝ) 0 1

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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
a : ℝ
h_of_pos : ∀ (a' : ℝ) (ha : 0 < a'), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
ha : a ≤ 0
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)

Tactic:
calc μ {x | ‖x‖ ≤ a}
        _ ≤ μ {x | ‖x‖ ≤ 1} := measure_mono fun x hx ↦ hx.trans (ha.trans (by positivity))
        _ ≤ 2⁻¹ := h_of_pos _ (by positivity)

Premises used: Norm.norm, setOf, LE.le, MeasureTheory.measure_mono, 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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
a : ℝ
h_of_pos : ∀ (a' : ℝ) (ha : 0 < a'), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
ha : 0 < a
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)

Tactic:
h_of_pos a ha
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
a : ℝ
h_of_pos : ∀ (a' : ℝ) (ha : 0 < a'), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a'} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
ha : 0 < a
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)

Tactic:
exact h_of_pos a ha
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ ∀ (a : ℝ), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)

Tactic:
have h_le a : μ {x | ‖x‖ ≤ a} ≤ 2⁻¹ := by
      have h_of_pos a' (ha : 0 < a') : μ {x | ‖x‖ ≤ a'} ≤ 2⁻¹ := by
        by_contra h_lt
        refine h_ne a' ?_
        exact le_antisymm prob_le_one (h_meas_Ioo a' ha (not_le.mp h_lt))
      rcases le_or_gt a 0 with ha | ha
      · calc μ {x | ‖x‖ ≤ a}
        _ ≤ μ {x | ‖x‖ ≤ 1} := measure_mono fun x hx ↦ hx.trans (ha.trans (by positivity))
        _ ≤ 2⁻¹ := h_of_pos _ (by positivity)
      · exact h_of_pos a ha
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
h_le : ∀ (a : ℝ), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
h :
  ∀ (x : E),
    Membership.mem (γ := Set E) Set.univ x ↔ Membership.mem (γ := Set E) (⋃ (a : ℕ), {x : E | ‖x‖ ≤ (↑a : ℝ)}) x
⊢ Eq.{u_1 + 1} (α := Set E) Set.univ (⋃ (a : ℕ), {x : E | ‖x‖ ≤ (↑a : ℝ)})

Tactic:
ext 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
inst_5 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
h_le : ∀ (a : ℝ), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
x : E
h : ∃ (i : ℕ), ‖x‖ ≤ (↑i : ℝ)
⊢ Membership.mem (γ := Set E) Set.univ x ↔ Membership.mem (γ := Set E) (⋃ (a : ℕ), {x : E | ‖x‖ ≤ (↑a : ℝ)}) x

Tactic:
simp only [Set.mem_univ, Set.mem_iUnion, Set.mem_setOf_eq, true_iff]

Premises used: Set.mem_iUnion, true_iff, Set.mem_setOf_eq, Set.mem_univ
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
h_le : ∀ (a : ℝ), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
x : E
⊢ ∃ (i : ℕ), ‖x‖ ≤ (↑i : ℝ)

Tactic:
exists_nat_ge _

Premises used: exists_nat_ge
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
h_le : ∀ (a : ℝ), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
x : E
⊢ ∃ (i : ℕ), ‖x‖ ≤ (↑i : ℝ)

Tactic:
exact exists_nat_ge _

Premises used: exists_nat_ge
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
h_le : ∀ (a : ℝ), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Set E) Set.univ (⋃ (a : ℕ), {x : E | ‖x‖ ≤ (↑a : ℝ)})

Tactic:
have h_univ : (Set.univ : Set E) = ⋃ a : ℕ, {x | ‖x‖ ≤ a} := by
      ext x
      simp only [Set.mem_univ, Set.mem_iUnion, Set.mem_setOf_eq, true_iff]
      exact exists_nat_ge _
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
h_le : ∀ (a : ℝ), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
h_univ : Eq.{u_1 + 1} (α := Set E) Set.univ (⋃ (a : ℕ), {x : E | ‖x‖ ≤ (↑a : ℝ)})
rw : LE.le (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ (↑i : ℝ)}) 2⁻¹
rw₁ : Monotone.{0, u_1} (β := Set E) fun (a : ℕ) ↦ {x : E | ‖x‖ ≤ (↑a : ℝ)}
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)

Tactic:
rw [h_univ, Monotone.measure_iUnion]

Premises used: Monotone.measure_iUnion
-- 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 : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
h_meas_Ioo :
  ∀ (a : ℝ) (_ : 0 < a) (_ : LT.lt (α := ℝ≥0∞) (2⁻¹ : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
h_ne : ∀ (b : ℝ), Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ b} : ℝ≥0∞) (1 : ℝ≥0∞)
h_le : ∀ (a : ℝ), LE.le (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞) (2⁻¹ : ℝ≥0∞)
h_univ : Eq.{u_1 + 1} (α := Set E) Set.univ (⋃ (a : ℕ), {x : E | ‖x‖ ≤ (↑a : ℝ)})
⊢ LE.le (α := ℝ≥0∞) (⨆ (i : ℕ), (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ (↑i : ℝ)}) 2⁻¹

Tactic:
simp [h_le]