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 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
this : b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
hc : 0 < √2
⊢ (b - a) / √2 < (‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2) / √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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
this : b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
field_simp : (‖p.1 + p.2‖ - ‖p.1 - p.2‖) * 2 = HPow.hPow (β := ℕ) (√2) 2 * (‖p.1 + p.2‖ - ‖p.1 - p.2‖)
⊢ (‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2) / √2 = (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2

Tactic:
field_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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
this : b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
⊢ LE.le (α := ℝ) 0 2

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 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
this : b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
rw : (‖p.1 + p.2‖ - ‖p.1 - p.2‖) * 2 = 2 * (‖p.1 + p.2‖ - ‖p.1 - p.2‖)
⊢ (‖p.1 + p.2‖ - ‖p.1 - p.2‖) * 2 = HPow.hPow (β := ℕ) (√2) 2 * (‖p.1 + p.2‖ - ‖p.1 - p.2‖)

Tactic:
rw [Real.sq_sqrt (by positivity)]

Premises used: Real.sq_sqrt
-- 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 : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
this : b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
⊢ (‖p.1 + p.2‖ - ‖p.1 - p.2‖) * 2 = 2 * (‖p.1 + p.2‖ - ‖p.1 - p.2‖)

Tactic:
ring
-- 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 : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
this : b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
calc : (b - a) / √2 < (‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2) / √2
calc₁ : (‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2) / √2 = (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2
⊢ (b - a) / √2 < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2

Tactic:
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

Premises used: Norm.norm, HSub.hSub, HDiv.hDiv, Prod.fst, HAdd.hAdd, Real.sqrt, OfNat.ofNat, Prod.snd
-- 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 : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
suffices : b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
⊢ (b - a) / √2 < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2

Tactic:
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
-- 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 : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
⊢ b - a < ‖p.1 + p.2‖ / √2 - a

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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
⊢ ‖p.1 + p.2‖ / √2 - a ≤ ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
calc : b - a < ‖p.1 + p.2‖ / √2 - a
calc₁ : ‖p.1 + p.2‖ / √2 - a ≤ ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
⊢ b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2

Tactic:
calc b - a < ‖p.1 + p.2‖ / √2 - a := by gcongr
      _ ≤ ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2 := by gcongr

Premises used: Prod.fst, Prod.snd
-- 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 : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
⊢ ‖p.1 + p.2‖ - ‖p.1 - p.2‖ ≤ 2 * min ‖p.1‖ ‖p.2‖

Tactic:
have := norm_add_sub_norm_sub_le_two_mul_min p.1 p.2
-- 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 : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
this : ‖p.1 + p.2‖ - ‖p.1 - p.2‖ ≤ 2 * min ‖p.1‖ ‖p.2‖
linarith : min ‖p.1‖ ‖p.2‖ < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 → 2 / 2 = 1
linarith₁ : min ‖p.1‖ ‖p.2‖ < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : min ‖p.1‖ ‖p.2‖ < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 → GT.gt (α := ℝ) 2 0
linarith₃ :
  min ‖p.1‖ ‖p.2‖ < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 →
    ‖p.1 + p.2‖ - ‖p.1 - p.2‖ - 2 * min ‖p.1‖ ‖p.2‖ + (2 * min ‖p.1‖ ‖p.2‖ - (1 * ‖p.1 + p.2‖ - 1 * ‖p.1 - p.2‖)) = 0
⊢ (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 ≤ min ‖p.1‖ ‖p.2‖

Tactic:
linarith
-- 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 : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
calc : (b - a) / √2 < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2
calc₁ : (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 ≤ min ‖p.1‖ ‖p.2‖
⊢ (b - a) / √2 < min ‖p.1‖ ‖p.2‖

Tactic:
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

Premises used: Norm.norm, HSub.hSub, Prod.fst, HAdd.hAdd, Prod.snd, Min.min
-- 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 : ℝ
⊢ Eq (α := ℝ≥0∞)
    ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖} : ℝ≥0∞)
    ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞)
        (SProd.sprod (α := Set E) (β := Set E) {x : E | (b - a) / √2 < ‖x‖} {y : E | (b - a) / √2 < ‖y‖}) :
      ℝ≥0∞)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.prod, rfl
-- 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 : ℝ
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {y : E | (b - a) / √2 < ‖y‖} : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞) 2
rw₁ rw₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {y : E | (b - a) / √2 < ‖y‖} : ℝ≥0∞) ≤
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (b - a) / √2 < ‖x‖} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {y : E | (b - a) / √2 < ‖y‖} : ℝ≥0∞)
⊢ (μ.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

Tactic:
rw [Measure.prod_prod, pow_two]

Premises used: pow_two, MeasureTheory.Measure.prod_prod
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
⊢ normThreshold a 0 = a

Tactic:
rfl

Premises used: ProbabilityTheory.Fernique.normThreshold, arithGeom, rfl
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
⊢ normThreshold a (n + 1) = √2 * normThreshold a n + a

Tactic:
rfl

Premises used: ProbabilityTheory.Fernique.normThreshold, arithGeom, rfl
-- 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_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
n : ℕ
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a (n + 1) < ‖x‖} : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (β := ℕ) ((μ : (a : Set E) → ℝ≥0∞) {x : E | (normThreshold a (n + 1) - a) / √2 < ‖x‖} : ℝ≥0∞)
      2

Tactic:
measure_le_mul_measure_gt_le_of_map_rotation_eq_self h_rot _ _

Premises used: ProbabilityTheory.measure_le_mul_measure_gt_le_of_map_rotation_eq_self
-- 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_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
n : ℕ
h : ∀ (x : E), normThreshold a n = (normThreshold a (n + 1) - a) / √2
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      ((μ : (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:
convert! measure_le_mul_measure_gt_le_of_map_rotation_eq_self h_rot _ _

Premises used: ProbabilityTheory.measure_le_mul_measure_gt_le_of_map_rotation_eq_self
-- 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_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a : ℝ
n : ℕ
x : E
⊢ normThreshold a n = (normThreshold a (n + 1) - a) / √2

Tactic:
simp [normThreshold_add_one]

Premises used: ProbabilityTheory.Fernique.normThreshold_add_one
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
ha_pos : 0 < a
simp : a / (1 - √2) < a
⊢ a / (1 - √2) < normThreshold a 0

Tactic:
simp only [normThreshold_zero]

Premises used: ProbabilityTheory.Fernique.normThreshold_zero
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
ha_pos : 0 < a
⊢ 1 - √2 ≤ 0

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
ha_pos : 0 < a
⊢ 0 < a

Tactic:
ha_pos
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
ha_pos : 0 < a
⊢ a / (1 - √2) < a

Tactic:
calc a / (1 - √2)
  _ ≤ 0 := div_nonpos_of_nonneg_of_nonpos ha_pos.le (by simp)
  _ < a := ha_pos

Premises used: HSub.hSub, LT.lt.le, div_nonpos_of_nonneg_of_nonpos, Real.sqrt, OfNat.ofNat
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
ha_pos : 0 < a
⊢ StrictMono (normThreshold a)

Tactic:
arithGeom_strictMono Real.one_lt_sqrt_two (lt_normThreshold_zero ha_pos)

Premises used: ProbabilityTheory.Fernique.lt_normThreshold_zero, ProbabilityTheory.Fernique.normThreshold, Real.one_lt_sqrt_two, arithGeom_strictMono
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
ha_pos : 0 < a
⊢ Tendsto (normThreshold a) atTop atTop

Tactic:
tendsto_arithGeom_atTop_of_one_lt Real.one_lt_sqrt_two (lt_normThreshold_zero ha_pos)

Premises used: ProbabilityTheory.Fernique.lt_normThreshold_zero, tendsto_arithGeom_atTop_of_one_lt, ProbabilityTheory.Fernique.normThreshold, Real.one_lt_sqrt_two
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
⊢ √2 ≠ 1

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
rw : a * (√2 ^ (n + 1) - 1) * (√2 + 1) = a * (1 + √2) * (√2 ^ (n + 1) - 1)
⊢ normThreshold a n = a * (1 + √2) * (√2 ^ (n + 1) - 1)

Tactic:
rw [normThreshold, arithGeom_same_eq_mul_div (by simp), div_eq_mul_inv, Real.inv_sqrt_two_sub_one]

Premises used: div_eq_mul_inv, ProbabilityTheory.Fernique.normThreshold, Real.inv_sqrt_two_sub_one, arithGeom_same_eq_mul_div
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
⊢ a * (√2 ^ (n + 1) - 1) * (√2 + 1) = a * (1 + √2) * (√2 ^ (n + 1) - 1)

Tactic:
ring
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
simp_rw :
  HPow.hPow (β := ℕ) a 2 * (HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (β := ℕ) (√2 ^ (n + 1 + 1) - 1) 2) ≤
    HPow.hPow (β := ℕ) a 2 * (HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2))
⊢ HPow.hPow (β := ℕ) (normThreshold a (n + 1)) 2 ≤
    HPow.hPow (β := ℕ) a 2 * HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
simp_rw [normThreshold_eq, mul_pow, mul_assoc]

Premises used: mul_assoc, ProbabilityTheory.Fernique.normThreshold_eq, mul_pow
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
hbc : HPow.hPow (β := ℕ) (√2 ^ (n + 1 + 1) - 1) 2 ≤ HPow.hPow (α := ℝ) 2 (n + 2)
⊢ HPow.hPow (β := ℕ) a 2 * (HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (β := ℕ) (√2 ^ (n + 1 + 1) - 1) 2) ≤
    HPow.hPow (β := ℕ) a 2 * (HPow.hPow (β := ℕ) (1 + √2) 2 * HPow.hPow (α := ℝ) 2 (n + 2))

Tactic:
gcongr
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
ha : 0 ≤ √2 ^ (n + 2) - 1
hab : √2 ^ (n + 2) - 1 ≤ √2 ^ (n + 2)
⊢ HPow.hPow (β := ℕ) (√2 ^ (n + 2) - 1) 2 ≤ HPow.hPow (β := ℕ) (√2 ^ (n + 2)) 2

Tactic:
gcongr
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
⊢ 0 ≤ √2 ^ HAdd.hAdd (α := ℕ) 0 2 - 1

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
h : 1 ≤ √2
h₁ : 0 ≤ n
⊢ √2 ^ HAdd.hAdd (α := ℕ) 0 2 - 1 ≤ √2 ^ (n + 2) - 1

Tactic:
gcongr
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
⊢ 1 ≤ √2

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
⊢ 0 ≤ n

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
calc : 0 ≤ √2 ^ HAdd.hAdd (α := ℕ) 0 2 - 1
calc₁ : √2 ^ HAdd.hAdd (α := ℕ) 0 2 - 1 ≤ √2 ^ (n + 2) - 1
⊢ 0 ≤ √2 ^ (n + 2) - 1

Tactic:
calc 0 ≤ √2 ^ (0 + 2) - 1 := by simp
      _ ≤ √2 ^ (n + 2) - 1 := by gcongr <;> simp

Premises used: HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
⊢ LE.le (α := ℝ) 0 1

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
⊢ √2 ^ (n + 2) - 1 ≤ √2 ^ (n + 2)

Tactic:
exact sub_le_self _ (by simp)

Premises used: sub_le_self
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
⊢ LE.le (α := ℝ) 0 2

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
rw : √2 ^ ((n + 2) * 2) = HPow.hPow (α := ℝ) 2 (n + 2)
rw₁ : √2 ^ (2 * (n + 2)) = HPow.hPow (α := ℝ) 2 (n + 2)
rw₂ : HPow.hPow (β := ℕ) (√2) 2 ^ (n + 2) = HPow.hPow (α := ℝ) 2 (n + 2)
rw₃ rw₄ : HPow.hPow (α := ℝ) 2 (n + 2) = HPow.hPow (α := ℝ) 2 (n + 2)
⊢ HPow.hPow (β := ℕ) (√2 ^ (n + 2)) 2 = HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
rw [← pow_mul, mul_comm, pow_mul, Real.sq_sqrt (by positivity)]

Premises used: Real.sq_sqrt, pow_mul, mul_comm
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
a : ℝ
n : ℕ
calc : HPow.hPow (β := ℕ) (√2 ^ (n + 2) - 1) 2 ≤ HPow.hPow (β := ℕ) (√2 ^ (n + 2)) 2
calc₁ : HPow.hPow (β := ℕ) (√2 ^ (n + 2)) 2 = HPow.hPow (α := ℝ) 2 (n + 2)
⊢ HPow.hPow (β := ℕ) (√2 ^ (n + 1 + 1) - 1) 2 ≤ HPow.hPow (α := ℝ) 2 (n + 2)

Tactic:
calc (√2 ^ (n + 2) - 1) ^ 2
  _ ≤ (√2 ^ (n + 2)) ^ 2 := by
    gcongr
    · calc 0 ≤ √2 ^ (0 + 2) - 1 := by simp
      _ ≤ √2 ^ (n + 2) - 1 := by gcongr <;> simp
    · exact sub_le_self _ (by simp)
  _ = 2 ^ (n + 2) := by rw [← pow_mul, mul_comm, pow_mul, Real.sq_sqrt (by positivity)]

Premises used: HSub.hSub, HPow.hPow, HAdd.hAdd, Real.sqrt, 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
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∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
⊢ 2⁻¹ < c

Tactic:
replace hc_gt : 2⁻¹ < c := ha_gt
-- 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∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
⊢ 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∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
⊢ 0 < c

Tactic:
have hc_pos : 0 < c := lt_of_lt_of_le (by simp) hc_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∞)
n : ℕ
c : ℝ≥0∞ := (μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a}
hc_gt : 2⁻¹ < c
hc_pos : 0 < c
⊢ 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∞)
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‖} ≤
    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∞))
⊢ (μ : (a : Set E) → ℝ≥0∞) {x : E | normThreshold a 0 < ‖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 0)

Tactic:
simp only [pow_zero, pow_one, normThreshold_zero]

Premises used: ProbabilityTheory.Fernique.normThreshold_zero, pow_zero, pow_one