awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
case :
  (∫⁻ (x : ℝ) in Iio 0, exponentialPDF r x) + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x =
    ENNReal.ofReal (1 - rexp (-(r * x)))
case₁ : 0 + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
case₂ case₃ case₄ : ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
case₅ :
  ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0) =
    ENNReal.ofReal (1 - rexp (-(r * x)))
case₆ : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume = ENNReal.ofReal (1 - rexp (-(r * x)))
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))
have case₇ : (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Icc 0 x)) fun (a : ℝ) ↦ r * rexp (-(r * a))) =
  (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
Tactic: case pos =>
    rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
      zero_add]
    simp only [exponentialPDF_eq]
    rw [setLIntegral_congr_fun measurableSet_Icc (g := fun x ↦ ENNReal.ofReal (r * rexp (-(r * x))))
      (by intro a ha; simp [ha.1])]
    rw [← ENNReal.toReal_eq_toReal_iff' _ ENNReal.ofReal_ne_top,
        ← integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun _ ↦ le_of_lt
        (mul_pos hr (exp_pos _)))]
    · have : ∫ a in uIoc 0 x, r * rexp (-(r * a)) = ∫ a in 0..x, r * rexp (-(r * a)) := by
        rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul]
      rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
      rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
      · rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
        norm_num; ring
      · simp only [intervalIntegrable_iff, uIoc_of_le h]
        exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
      · have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)
      · simp only [neg_mul, one_mul]
        exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
    · refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)
      rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
      exact exp_neg_integrableOn_Ioc hr
    · refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
      rw [integrableOn_Icc_iff_integrableOn_Ioc]
      exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
case :
  (∫⁻ (x : ℝ) in Iio 0, exponentialPDF r x) + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x =
    ENNReal.ofReal (1 - rexp (-(r * x)))
case₁ : 0 + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
case₂ case₃ case₄ : ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
case₅ :
  ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0) =
    ENNReal.ofReal (1 - rexp (-(r * x)))
case₆ : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume = ENNReal.ofReal (1 - rexp (-(r * x)))
case₇ :
  (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Icc 0 x)) fun (a : ℝ) ↦ r * rexp (-(r * a))) =
    (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))
have case₈ : AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x)))
  (Measure.restrict volume (Icc 0 x))
Tactic: case pos =>
    rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
      zero_add]
    simp only [exponentialPDF_eq]
    rw [setLIntegral_congr_fun measurableSet_Icc (g := fun x ↦ ENNReal.ofReal (r * rexp (-(r * x))))
      (by intro a ha; simp [ha.1])]
    rw [← ENNReal.toReal_eq_toReal_iff' _ ENNReal.ofReal_ne_top,
        ← integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun _ ↦ le_of_lt
        (mul_pos hr (exp_pos _)))]
    · have : ∫ a in uIoc 0 x, r * rexp (-(r * a)) = ∫ a in 0..x, r * rexp (-(r * a)) := by
        rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul]
      rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
      rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
      · rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
        norm_num; ring
      · simp only [intervalIntegrable_iff, uIoc_of_le h]
        exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
      · have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)
      · simp only [neg_mul, one_mul]
        exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
    · refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)
      rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
      exact exp_neg_integrableOn_Ioc hr
    · refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
      rw [integrableOn_Icc_iff_integrableOn_Ioc]
      exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
case :
  (∫⁻ (x : ℝ) in Iio 0, exponentialPDF r x) + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x =
    ENNReal.ofReal (1 - rexp (-(r * x)))
case₁ : 0 + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
case₂ case₃ case₄ : ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
case₅ :
  ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0) =
    ENNReal.ofReal (1 - rexp (-(r * x)))
case₆ : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume = ENNReal.ofReal (1 - rexp (-(r * x)))
case₇ :
  (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Icc 0 x)) fun (a : ℝ) ↦ r * rexp (-(r * a))) =
    (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
case₈ :
  AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x)))
    (Measure.restrict volume (Icc 0 x))
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))
have case₉ : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume ≠ ∞
Tactic: case pos =>
    rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
      zero_add]
    simp only [exponentialPDF_eq]
    rw [setLIntegral_congr_fun measurableSet_Icc (g := fun x ↦ ENNReal.ofReal (r * rexp (-(r * x))))
      (by intro a ha; simp [ha.1])]
    rw [← ENNReal.toReal_eq_toReal_iff' _ ENNReal.ofReal_ne_top,
        ← integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun _ ↦ le_of_lt
        (mul_pos hr (exp_pos _)))]
    · have : ∫ a in uIoc 0 x, r * rexp (-(r * a)) = ∫ a in 0..x, r * rexp (-(r * a)) := by
        rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul]
      rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
      rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
      · rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
        norm_num; ring
      · simp only [intervalIntegrable_iff, uIoc_of_le h]
        exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
      · have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)
      · simp only [neg_mul, one_mul]
        exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
    · refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)
      rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
      exact exp_neg_integrableOn_Ioc hr
    · refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
      rw [integrableOn_Icc_iff_integrableOn_Ioc]
      exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
⊢ (↑(cdf (expMeasure r)) : ℝ → ℝ) x = if 0 ≤ x then 1 - rexp (-(r * x)) else 0
have rw : 0 ≤ if 0 ≤ x then 1 - rexp (-(r * x)) else 0
Tactic: rw [cdf_expMeasure_eq_lintegral hr, lintegral_exponentialPDF_eq_antiDeriv hr x,
    ENNReal.toReal_ofReal_eq_iff]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
⊢ 0 ≤ if 0 ≤ x then 1 - rexp (-(r * x)) else 0
have pos : ∀ (h : 0 ≤ x), 0 ≤ 1 - rexp (-(r * x))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
pos : ∀ (h : 0 ≤ x), 0 ≤ 1 - rexp (-(r * x))
⊢ 0 ≤ if 0 ≤ x then 1 - rexp (-(r * x)) else 0
have neg : ∀ (h : ¬0 ≤ x), LE.le (α := ℝ) 0 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ 1 - rexp (-(r * x))
have pos : 0 ≤ r * x
Tactic: simp only [sub_nonneg, exp_le_one_iff, Left.neg_nonpos_iff]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (hypothesis)
Goal:
β : Type u_1
inst : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
⊢ ∃ (n : ℕ), x ≤ t n
have ht_tendsto₁ : ∀ (b : β), ∃ (a : ℕ), b ≤ t a
Tactic: simp only [tendsto_atTop_atTop_iff_of_monotone ht_mono.monotone] at ht_tendsto
Cleared hypotheses: ht_tendsto
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (hypothesis)
Goal:
β : Type u_1
inst : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
⊢ ∃ (n : ℕ), t n < x ∧ x ≤ t (n + 1)
have h : ∃ (n : ℕ), x ≤ t n
Tactic: have h : ∃ n, x ≤ t n := by
    simp only [tendsto_atTop_atTop_iff_of_monotone ht_mono.monotone] at ht_tendsto
    exact ht_tendsto x
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (hypothesis)
Goal:
β : Type u_1
inst : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
h : ∃ (n : ℕ), x ≤ t n
⊢ ∃ (n : ℕ), t n < x ∧ x ≤ t (n + 1)
have h' : ∀ m < Nat.find (p := fun (n : ℕ) ↦ x ≤ t n) h, ¬x ≤ t m
Tactic: have h' m := Nat.find_min h (m := m)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (hypothesis)
Goal:
β : Type u_1
inst : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
h : ∃ (n : ℕ), x ≤ t n
h' : ∀ m < Nat.find (p := fun (n : ℕ) ↦ x ≤ t n) h, ¬x ≤ t m
⊢ ∃ (n : ℕ), t n < x ∧ x ≤ t (n + 1)
have h'₁ : ∀ m < Nat.find (p := fun (n : ℕ) ↦ x ≤ t n) h, t m < x
Tactic: simp only [not_le] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
θ : ℝ
x y : E × E
⊢ (Real.cos θ • (x + y).1 + Real.sin θ • (x + y).2, -Real.sin θ • (x + y).1 + Real.cos θ • (x + y).2) =
    (Real.cos θ • x.1 + Real.sin θ • x.2, -Real.sin θ • x.1 + Real.cos θ • x.2) +
      (Real.cos θ • y.1 + Real.sin θ • y.2, -Real.sin θ • y.1 + Real.cos θ • y.2)
have simp : (Real.cos θ • x.1 + Real.cos θ • y.1 + (Real.sin θ • x.2 + Real.sin θ • y.2),
    -(Real.sin θ • x.1) + -(Real.sin θ • y.1) + (Real.cos θ • x.2 + Real.cos θ • y.2)) =
  (Real.cos θ • x.1 + Real.sin θ • x.2 + (Real.cos θ • y.1 + Real.sin θ • y.2),
    -(Real.sin θ • x.1) + Real.cos θ • x.2 + (-(Real.sin θ • y.1) + Real.cos θ • y.2))
Tactic: simp only [Prod.fst_add, smul_add, Prod.snd_add, neg_smul, Prod.mk_add_mk]
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
      ((μ : (a : Set E) → ℝ≥0∞) {x : E | b < ‖x‖} : ℝ≥0∞) =
    (μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) (SProd.sprod (α := Set E) (β := Set E) {x : E | ‖x‖ ≤ a} {y : E | b < ‖y‖})
have rw : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) {x : E | b < ‖x‖} : ℝ≥0∞) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) {x : E | ‖x‖ ≤ a} : ℝ≥0∞)
    ((μ : (a : Set E) → ℝ≥0∞) {y : E | b < ‖y‖} : ℝ≥0∞)
Tactic: rw [Measure.prod_prod]
-- 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
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 | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} : ℝ≥0∞)
    (((Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) : Measure (E × E)) :
          (a : Set (E × E)) → ℝ≥0∞)
        {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} :
      ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} : ℝ≥0∞)
  ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} : ℝ≥0∞)
Tactic: rw [h]
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) : Measure (E × E)) :
          (a : Set (E × E)) → ℝ≥0∞)
        {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} :
      ℝ≥0∞)
    ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2} : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞)
      (Set.preimage (β := E × E) (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E)
        {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}) :
    ℝ≥0∞)
  ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2} : ℝ≥0∞)
Tactic: rw [Measure.map_apply (by fun_prop)]
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
rw :
  Eq (α := ℝ≥0∞)
    ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞)
        (Set.preimage (β := E × E) (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E)
          {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}) :
      ℝ≥0∞)
    ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2} : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) : Measure (E × E)) :
          (a : Set (E × E)) → ℝ≥0∞)
        {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} :
      ℝ≥0∞)
    ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2} : ℝ≥0∞)
have rw₁ : MeasurableSet.{u_1} (α := E × E) {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}
Tactic: rw [Measure.map_apply (by fun_prop)]
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ MeasurableSet.{u_1} (α := E × E) {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}
have refine_1 : MeasurableSet.{u_1} (α := E × E) fun (p : E × E) ↦ Real.le✝ ‖p.1‖ a
Tactic: refine MeasurableSet.inter ?_ ?_
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
refine_1 : MeasurableSet.{u_1} (α := E × E) fun (p : E × E) ↦ Real.le✝ ‖p.1‖ a
⊢ MeasurableSet.{u_1} (α := E × E) {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}
have refine_2 : MeasurableSet.{u_1} (α := E × E) fun (p : E × E) ↦ Real.lt✝ b ‖p.2‖
Tactic: refine MeasurableSet.inter ?_ ?_
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ Measurable (β := ℝ) fun (p : E × E) ↦ ‖p.1‖
have funProp : inst_3 ≤ inst_3
Tactic: fun_prop
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
funProp : inst_3 ≤ inst_3
⊢ Measurable (β := ℝ) fun (p : E × E) ↦ ‖p.1‖
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (p2 : E) ↦ ‖p2‖
Tactic: fun_prop
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ Measurable (β := ℝ) fun (p : E × E) ↦ ‖p.2‖
have funProp : inst_3 ≤ inst_3
Tactic: fun_prop
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
funProp : inst_3 ≤ inst_3
⊢ Measurable (β := ℝ) fun (p : E × E) ↦ ‖p.2‖
have funProp₁ : MeasurableEmbedding (β := ℝ) fun (p2 : E) ↦ ‖p2‖
Tactic: fun_prop
-- 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
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∞)
        (Set.preimage (β := E × E) (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E)
          {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}) :
      ℝ≥0∞)
    ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2} : ℝ≥0∞)
have h₁ : Eq.{u_1 + 1} (α := Set (E × E))
  (Set.preimage (β := E × E) (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E)
    {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖})
  {p : E × E | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}
Tactic: congr 1
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ Eq.{u_1 + 1} (α := Set (E × E))
    (Set.preimage (β := E × E) (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E)
      {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖})
    {p : E × E | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}
have h₁ : Eq.{u_1 + 1} (α := Set (E × E))
  {a_1 : E × E | ‖(√2 / 2) • a_1.1 + -((√2 / 2) • a_1.2)‖ ≤ a ∧ b < ‖(√2 / 2) • a_1.1 + (√2 / 2) • a_1.2‖}
  {p : E × E | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2}
Tactic: simp only [Set.preimage_setOf_eq, ContinuousLinearMap.rotation_apply, Real.cos_neg,
      Real.cos_pi_div_four, Real.sin_neg, Real.sin_pi_div_four, neg_smul, neg_neg]
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ ‖2⁻¹ * √2‖ = (√2)⁻¹
have simp : 2⁻¹ * |√2| = (√2)⁻¹
Tactic: simp only [norm_mul, norm_inv, Real.norm_ofNat, Real.norm_eq_abs]
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ 2⁻¹ * |√2| = (√2)⁻¹
have rw : 2⁻¹ * √2 = (√2)⁻¹
Tactic: rw [abs_of_nonneg (by positivity)]
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ 2⁻¹ * √2 = (√2)⁻¹
have nth_rw : (HPow.hPow (β := ℕ) (√2) 2)⁻¹ * √2 = (√2)⁻¹
Tactic: nth_rw 1 [← Real.sq_sqrt (by simp : (0 : ℝ) ≤ 2)]
-- 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ (HPow.hPow (β := ℕ) (√2) 2)⁻¹ * √2 = (√2)⁻¹
have rw : (√2 * √2)⁻¹ * √2 = (√2)⁻¹
Tactic: rw [pow_two, mul_inv, mul_assoc, inv_mul_cancel₀ (by positivity), mul_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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
rw : (√2 * √2)⁻¹ * √2 = (√2)⁻¹
⊢ (HPow.hPow (β := ℕ) (√2) 2)⁻¹ * √2 = (√2)⁻¹
have rw₁ : (√2)⁻¹ * (√2)⁻¹ * √2 = (√2)⁻¹
Tactic: rw [pow_two, mul_inv, mul_assoc, inv_mul_cancel₀ (by positivity), mul_one]