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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
rw : (√2 * √2)⁻¹ * √2 = (√2)⁻¹
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]
-- 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)⁻¹
rw₁ : (√2)⁻¹ * (√2)⁻¹ * √2 = (√2)⁻¹
rw₂ : (√2)⁻¹ * ((√2)⁻¹ * √2) = (√2)⁻¹
⊢ (HPow.hPow (β := ℕ) (√2) 2)⁻¹ * √2 = (√2)⁻¹
have rw₃ : (√2)⁻¹ * 1 = (√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)⁻¹
rw₁ : (√2)⁻¹ * (√2)⁻¹ * √2 = (√2)⁻¹
rw₂ : (√2)⁻¹ * ((√2)⁻¹ * √2) = (√2)⁻¹
rw₃ : (√2)⁻¹ * 1 = (√2)⁻¹
⊢ (HPow.hPow (β := ℕ) (√2) 2)⁻¹ * √2 = (√2)⁻¹
have rw₄ : (√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 (hypothesis)
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))
    {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}
have h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
Tactic: have h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹ := by
      simp only [norm_mul, norm_inv, Real.norm_ofNat, Real.norm_eq_abs]
      rw [abs_of_nonneg (by positivity)]
      nth_rw 1 [← Real.sq_sqrt (by simp : (0 : ℝ) ≤ 2)]
      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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
⊢ 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}
have h₁ : ∀ (p : E × E), ‖(√2 / 2) • p.1 + -((√2 / 2) • p.2)‖ = ‖p.1 - p.2‖ / √2
Tactic: congr! with p
-- 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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
h₁ : ∀ (p : E × E), ‖(√2 / 2) • p.1 + -((√2 / 2) • p.2)‖ = ‖p.1 - p.2‖ / √2
⊢ 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}
have h₂ : ∀ (p : E × E), ‖(√2 / 2) • p.1 + (√2 / 2) • p.2‖ = ‖p.1 + p.2‖ / √2
Tactic: congr! with p
-- 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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
⊢ ‖(√2 / 2) • p.1 + -((√2 / 2) • p.2)‖ = ‖p.1 - p.2‖ / √2
have h₁ : ‖(√2 / 2) • p.1 - (√2 / 2) • p.2‖ = ‖p.1 - p.2‖ / √2
Tactic: rw [← sub_eq_add_neg, ← smul_sub, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
-- 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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
h₁ : ‖(√2 / 2) • p.1 - (√2 / 2) • p.2‖ = ‖p.1 - p.2‖ / √2
⊢ ‖(√2 / 2) • p.1 + -((√2 / 2) • p.2)‖ = ‖p.1 - p.2‖ / √2
have h₂ : ‖(√2 / 2) • (p.1 - p.2)‖ = ‖p.1 - p.2‖ / √2
Tactic: rw [← sub_eq_add_neg, ← smul_sub, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
-- 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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
h₁ : ‖(√2 / 2) • p.1 - (√2 / 2) • p.2‖ = ‖p.1 - p.2‖ / √2
h₂ : ‖(√2 / 2) • (p.1 - p.2)‖ = ‖p.1 - p.2‖ / √2
⊢ ‖(√2 / 2) • p.1 + -((√2 / 2) • p.2)‖ = ‖p.1 - p.2‖ / √2
have h₃ : ‖√2 / 2‖ * ‖p.1 - p.2‖ = ‖p.1 - p.2‖ / √2
Tactic: rw [← sub_eq_add_neg, ← smul_sub, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
-- 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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
h₁ : ‖(√2 / 2) • p.1 - (√2 / 2) • p.2‖ = ‖p.1 - p.2‖ / √2
h₂ : ‖(√2 / 2) • (p.1 - p.2)‖ = ‖p.1 - p.2‖ / √2
h₃ : ‖√2 / 2‖ * ‖p.1 - p.2‖ = ‖p.1 - p.2‖ / √2
⊢ ‖(√2 / 2) • p.1 + -((√2 / 2) • p.2)‖ = ‖p.1 - p.2‖ / √2
have h₄ : ‖2⁻¹ * √2‖ * ‖p.1 - p.2‖ = ‖p.1 - p.2‖ / √2
Tactic: rw [← sub_eq_add_neg, ← smul_sub, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
-- 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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
h₁ : ‖(√2 / 2) • p.1 - (√2 / 2) • p.2‖ = ‖p.1 - p.2‖ / √2
h₂ : ‖(√2 / 2) • (p.1 - p.2)‖ = ‖p.1 - p.2‖ / √2
h₃ : ‖√2 / 2‖ * ‖p.1 - p.2‖ = ‖p.1 - p.2‖ / √2
h₄ : ‖2⁻¹ * √2‖ * ‖p.1 - p.2‖ = ‖p.1 - p.2‖ / √2
⊢ ‖(√2 / 2) • p.1 + -((√2 / 2) • p.2)‖ = ‖p.1 - p.2‖ / √2
have h₅ : ‖2⁻¹ * √2‖ * ‖p.1 - p.2‖ = (√2)⁻¹ * ‖p.1 - p.2‖
Tactic: rw [← sub_eq_add_neg, ← smul_sub, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
-- 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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
h₁ : ‖(√2 / 2) • p.1 - (√2 / 2) • p.2‖ = ‖p.1 - p.2‖ / √2
h₂ : ‖(√2 / 2) • (p.1 - p.2)‖ = ‖p.1 - p.2‖ / √2
h₃ : ‖√2 / 2‖ * ‖p.1 - p.2‖ = ‖p.1 - p.2‖ / √2
h₄ : ‖2⁻¹ * √2‖ * ‖p.1 - p.2‖ = ‖p.1 - p.2‖ / √2
h₅ : ‖2⁻¹ * √2‖ * ‖p.1 - p.2‖ = (√2)⁻¹ * ‖p.1 - p.2‖
⊢ ‖(√2 / 2) • p.1 + -((√2 / 2) • p.2)‖ = ‖p.1 - p.2‖ / √2
have h₆ : (√2)⁻¹ * ‖p.1 - p.2‖ = (√2)⁻¹ * ‖p.1 - p.2‖
Tactic: rw [← sub_eq_add_neg, ← smul_sub, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
-- 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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
⊢ ‖(√2 / 2) • p.1 + (√2 / 2) • p.2‖ = ‖p.1 + p.2‖ / √2
have h₁ : ‖(√2 / 2) • (p.1 + p.2)‖ = ‖p.1 + p.2‖ / √2
Tactic: rw [← smul_add, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
-- 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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
h₁ : ‖(√2 / 2) • (p.1 + p.2)‖ = ‖p.1 + p.2‖ / √2
⊢ ‖(√2 / 2) • p.1 + (√2 / 2) • p.2‖ = ‖p.1 + p.2‖ / √2
have h₂ : ‖√2 / 2‖ * ‖p.1 + p.2‖ = ‖p.1 + p.2‖ / √2
Tactic: rw [← smul_add, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
-- 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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
h₁ : ‖(√2 / 2) • (p.1 + p.2)‖ = ‖p.1 + p.2‖ / √2
h₂ : ‖√2 / 2‖ * ‖p.1 + p.2‖ = ‖p.1 + p.2‖ / √2
⊢ ‖(√2 / 2) • p.1 + (√2 / 2) • p.2‖ = ‖p.1 + p.2‖ / √2
have h₃ : ‖2⁻¹ * √2‖ * ‖p.1 + p.2‖ = ‖p.1 + p.2‖ / √2
Tactic: rw [← smul_add, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
-- 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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
h₁ : ‖(√2 / 2) • (p.1 + p.2)‖ = ‖p.1 + p.2‖ / √2
h₂ : ‖√2 / 2‖ * ‖p.1 + p.2‖ = ‖p.1 + p.2‖ / √2
h₃ : ‖2⁻¹ * √2‖ * ‖p.1 + p.2‖ = ‖p.1 + p.2‖ / √2
⊢ ‖(√2 / 2) • p.1 + (√2 / 2) • p.2‖ = ‖p.1 + p.2‖ / √2
have h₄ : ‖2⁻¹ * √2‖ * ‖p.1 + p.2‖ = (√2)⁻¹ * ‖p.1 + p.2‖
Tactic: rw [← smul_add, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
-- 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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
p : E × E
h₁ : ‖(√2 / 2) • (p.1 + p.2)‖ = ‖p.1 + p.2‖ / √2
h₂ : ‖√2 / 2‖ * ‖p.1 + p.2‖ = ‖p.1 + p.2‖ / √2
h₃ : ‖2⁻¹ * √2‖ * ‖p.1 + p.2‖ = ‖p.1 + p.2‖ / √2
h₄ : ‖2⁻¹ * √2‖ * ‖p.1 + p.2‖ = (√2)⁻¹ * ‖p.1 + p.2‖
⊢ ‖(√2 / 2) • p.1 + (√2 / 2) • p.2‖ = ‖p.1 + p.2‖ / √2
have h₅ : (√2)⁻¹ * ‖p.1 + p.2‖ = (√2)⁻¹ * ‖p.1 + p.2‖
Tactic: rw [← smul_add, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]
-- 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 : ℝ
⊢ LE.le (α := ℝ≥0∞)
    ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2} : ℝ≥0∞)
    ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖} : ℝ≥0∞)
have refine : ∀ (p : E × E),
  Membership.mem (γ := Set (E × E)) {p : E × E | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2} p →
    Membership.mem (γ := Set (E × E)) {p : E × E | (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖} p
Tactic: refine measure_mono fun p ↦ ?_
-- 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 : ℝ
p : E × E
⊢ Membership.mem (γ := Set (E × E)) {p : E × E | ‖p.1 - p.2‖ / √2 ≤ a ∧ b < ‖p.1 + p.2‖ / √2} p →
    Membership.mem (γ := Set (E × E)) {p : E × E | (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖} p
have simp : ‖p.1 - p.2‖ / √2 ≤ a → b < ‖p.1 + p.2‖ / √2 → (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖
Tactic: simp only [Set.mem_setOf_eq, and_imp]
-- 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 : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
⊢ (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖
have suffices : (b - a) / √2 < min ‖p.1‖ ‖p.2‖
Tactic: suffices (b - a) / √2 < min ‖p.1‖ ‖p.2‖ from lt_min_iff.mp this
-- 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 : ℝ
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
⊢ (b - a) / √2 < (‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2) / √2
have hc : 0 < √2
Tactic: gcongr
-- 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 : ℝ
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‖ / √2 - ‖p.1 - p.2‖ / √2) / √2 = (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2
have field_simp : (‖p.1 + p.2‖ - ‖p.1 - p.2‖) * 2 = HPow.hPow (β := ℕ) (√2) 2 * (‖p.1 + p.2‖ - ‖p.1 - p.2‖)
Tactic: field_simp
-- 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 : ℝ
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 = HPow.hPow (β := ℕ) (√2) 2 * (‖p.1 + p.2‖ - ‖p.1 - p.2‖)
have rw : (‖p.1 + p.2‖ - ‖p.1 - p.2‖) * 2 = 2 * (‖p.1 + p.2‖ - ‖p.1 - p.2‖)
Tactic: rw [Real.sq_sqrt (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 : ℝ
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
⊢ (b - a) / √2 < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2
have calc : (b - a) / √2 < (‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √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
-- 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 : ℝ
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
⊢ (b - a) / √2 < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2
have calc₁ : (‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2) / √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
-- 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 : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
⊢ (b - a) / √2 < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2
have suffices : b - a < ‖p.1 + p.2‖ / √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
-- 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 : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
⊢ b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
have calc : b - a < ‖p.1 + p.2‖ / √2 - a
Tactic: calc b - a < ‖p.1 + p.2‖ / √2 - a := by gcongr
      _ ≤ ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2 := by gcongr
-- 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 : ℝ
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
⊢ b - a < ‖p.1 + p.2‖ / √2 - ‖p.1 - p.2‖ / √2
have calc₁ : ‖p.1 + p.2‖ / √2 - 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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (hypothesis)
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‖
have this : ‖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
-- 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 : ℝ
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‖
⊢ (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 ≤ min ‖p.1‖ ‖p.2‖
have linarith : min ‖p.1‖ ‖p.2‖ < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 → 2 / 2 = 1
Tactic: linarith
-- 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 : ℝ
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
⊢ (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 ≤ min ‖p.1‖ ‖p.2‖
have linarith₁ : min ‖p.1‖ ‖p.2‖ < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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 : ℝ
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
⊢ (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 ≤ min ‖p.1‖ ‖p.2‖
have linarith₂ : min ‖p.1‖ ‖p.2‖ < (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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 : ℝ
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
⊢ (‖p.1 + p.2‖ - ‖p.1 - p.2‖) / 2 ≤ min ‖p.1‖ ‖p.2‖
have 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
Tactic: linarith