awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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∞)
⊢ (μ : (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∞)
have 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∞)
Tactic: rw [← mul_assoc, ENNReal.inv_mul_cancel hc_pos.ne' hc_lt_top.ne, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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∞)
⊢ (μ : (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∞)
have 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∞)
Tactic: rw [← mul_assoc, ENNReal.inv_mul_cancel hc_pos.ne' hc_lt_top.ne, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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 (β := ℕ) (c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2 =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
have 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)
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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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)
⊢ c⁻¹ * HPow.hPow (β := ℕ) (c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2 =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
have rw₁ : c⁻¹ * (HPow.hPow (β := ℕ) c 2 * ((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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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)
⊢ c⁻¹ * HPow.hPow (β := ℕ) (c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2 =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
have rw₂ : c⁻¹ * HPow.hPow (β := ℕ) c 2 * ((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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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)
⊢ c⁻¹ * HPow.hPow (β := ℕ) (c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2 =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
have rw₃ : c⁻¹ * (c * 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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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)
⊢ c⁻¹ * HPow.hPow (β := ℕ) (c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2 =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
have rw₄ : c⁻¹ * c * 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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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)
⊢ c⁻¹ * HPow.hPow (β := ℕ) (c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2 =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
have rw₅ : 1 * 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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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)
⊢ c⁻¹ * HPow.hPow (β := ℕ) (c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2 =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
have rw₆ : 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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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)
⊢ c⁻¹ * HPow.hPow (β := ℕ) (c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2 =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
have rw₇ : c * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * 2) =
  c * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * HPow.hPow (α := ℕ) (β := ℕ) 2 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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
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)
⊢ c⁻¹ * HPow.hPow (β := ℕ) (c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 n) 2 =
    c * ((1 - c) / c) ^ HPow.hPow (α := ℕ) 2 (n + 1)
have rw₈ : c * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * 2) = c * ((1 - c) / c) ^ (HPow.hPow (α := ℕ) 2 n * 2)
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]