awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Fernique
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
⊢ ∀ m < Nat.find (p := fun (n : ℕ) ↦ x ≤ t n) h, ¬x ≤ t m

Tactic:
have h' m := Nat.find_min h (m := m)
-- Module: Mathlib.Probability.Distributions.Fernique
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
⊢ ∀ m < Nat.find (p := fun (n : ℕ) ↦ x ≤ t n) h, t m < x

Tactic:
simp only [not_le] at h'

Premises used: not_le
-- Module: Mathlib.Probability.Distributions.Fernique
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, t m < x
⊢ Nat.find (p := fun (n : ℕ) ↦ x ≤ t n) h - 1 < Nat.find (p := fun (n : ℕ) ↦ x ≤ t n) h

Tactic:
simp [hx]
-- Module: Mathlib.Probability.Distributions.Fernique
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, t m < x
⊢ x ≤ t (Nat.find (p := fun (n : ℕ) ↦ x ≤ t n) h - 1 + 1)

Tactic:
simp [Nat.find_spec h, hx]

Premises used: Nat.find_spec
-- Module: Mathlib.Probability.Distributions.Fernique
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, t m < x
⊢ ∃ (n : ℕ), t n < x ∧ x ≤ t (n + 1)

Tactic:
exact ⟨Nat.find h - 1, h' _ (by simp [hx]), by simp [Nat.find_spec h, hx]⟩
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
θ : ℝ
x y : E × E
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))
⊢ (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)

Tactic:
simp only [Prod.fst_add, smul_add, Prod.snd_add, neg_smul, Prod.mk_add_mk]

Premises used: Prod.mk_add_mk, neg_smul, Prod.fst_add, Prod.snd_add, smul_add
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
θ : ℝ
x y : E × E
⊢ (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:
abel_nf
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
θ c : ℝ
x : E × E
⊢ (Real.cos θ • (c • x).1 + Real.sin θ • (c • x).2, -Real.sin θ • (c • x).1 + Real.cos θ • (c • x).2) =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ)
      (Real.cos θ • x.1 + Real.sin θ • x.2, -Real.sin θ • x.1 + Real.cos θ • x.2)

Tactic:
simp [smul_comm c]

Premises used: SMulCommClass.smul_comm
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
θ : ℝ
x : E × E
⊢ (ContinuousLinearMap.rotation θ : (a : E × E) → E × E) x =
    (Real.cos θ • x.1 + Real.sin θ • x.2, -Real.sin θ • x.1 + Real.cos θ • x.2)

Tactic:
rfl

Premises used: 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 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∞)
⊢ 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‖})

Tactic:
rw [Measure.prod_prod]

Premises used: MeasureTheory.Measure.prod_prod
-- 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∞) (SProd.sprod (α := Set E) (β := Set E) {x : E | ‖x‖ ≤ a} {y : E | b < ‖y‖}) :
      ℝ≥0∞)
    ((μ.prod μ : (a : Set (E × E)) → ℝ≥0∞) {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖} : ℝ≥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 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∞)
⊢ 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∞)

Tactic:
rw [h]
-- 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 : ℝ
⊢ Measurable.{u_1, u_1} (α := E × E) (β := E × E) (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E)

Tactic:
fun_prop
-- 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 :
  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∞)
rw₁ : MeasurableSet.{u_1} (α := E × E) {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}
⊢ 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∞)

Tactic:
rw [Measure.map_apply (by fun_prop)]

Premises used: MeasureTheory.Measure.map_apply
-- 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 : ℝ
⊢ MeasurableSet.{u_1} (α := E × E) {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}

Tactic:
MeasurableSet.inter ?_ ?_

Premises used: Set.Mem, setOf, Set.inter, MeasurableSet.inter
-- 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 : ℝ
refine_1 : MeasurableSet.{u_1} (α := E × E) fun (p : E × E) ↦ Real.le✝ ‖p.1‖ a
refine_2 : MeasurableSet.{u_1} (α := E × E) fun (p : E × E) ↦ Real.lt✝ b ‖p.2‖
⊢ MeasurableSet.{u_1} (α := E × E) {p : E × E | ‖p.1‖ ≤ a ∧ b < ‖p.2‖}

Tactic:
refine MeasurableSet.inter ?_ ?_

Premises used: MeasurableSet.inter
-- 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 : ℝ
funProp : inst_3 ≤ inst_3
funProp₁ : MeasurableEmbedding (β := ℝ) fun (p2 : E) ↦ ‖p2‖
⊢ Measurable (β := ℝ) fun (p : E × E) ↦ ‖p.1‖

Tactic:
fun_prop
-- 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 : ℝ
⊢ Measurable (β := ℝ) fun (p : E × E) ↦ a

Tactic:
fun_prop
-- 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 : ℝ
⊢ MeasurableSet.{u_1} (α := E × E) {p : E × E | ‖p.1‖ ≤ a}

Tactic:
exact measurableSet_le (by fun_prop) (by fun_prop)

Premises used: measurableSet_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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ Measurable (β := ℝ) fun (p : E × E) ↦ b

Tactic:
fun_prop
-- 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 : ℝ
funProp : inst_3 ≤ inst_3
funProp₁ : MeasurableEmbedding (β := ℝ) fun (p2 : E) ↦ ‖p2‖
⊢ Measurable (β := ℝ) fun (p : E × E) ↦ ‖p.2‖

Tactic:
fun_prop
-- 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 : ℝ
⊢ MeasurableSet.{u_1} (α := E × E) {p : E × E | b < ‖p.2‖}

Tactic:
exact measurableSet_lt (by fun_prop) (by fun_prop)

Premises used: measurableSet_lt
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
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}
⊢ 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:
congr 1
-- 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 : ℝ
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}
⊢ 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:
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]

Premises used: neg_smul, Real.cos_pi_div_four, neg_neg, Real.sin_neg, Set.preimage_setOf_eq, ContinuousLinearMap.rotation_apply, Real.cos_neg, Real.sin_pi_div_four
-- 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 : ℝ
simp : 2⁻¹ * |√2| = (√2)⁻¹
⊢ ‖2⁻¹ * √2‖ = (√2)⁻¹

Tactic:
simp only [norm_mul, norm_inv, Real.norm_ofNat, Real.norm_eq_abs]

Premises used: norm_mul, norm_inv, Real.norm_eq_abs, Real.norm_ofNat
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
⊢ 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 : ℝ
rw : 2⁻¹ * √2 = (√2)⁻¹
⊢ 2⁻¹ * |√2| = (√2)⁻¹

Tactic:
rw [abs_of_nonneg (by positivity)]

Premises used: abs_of_nonneg
-- 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 : ℝ
⊢ LE.le (α := ℝ) 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
inst_5 : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
a b : ℝ
nth_rw : (HPow.hPow (β := ℕ) (√2) 2)⁻¹ * √2 = (√2)⁻¹
⊢ 2⁻¹ * √2 = (√2)⁻¹

Tactic:
nth_rw 1 [← Real.sq_sqrt (by simp : (0 : ℝ) ≤ 2)]

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 : ℝ
⊢ √2 ≠ 0

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 : ℝ
rw : (√2 * √2)⁻¹ * √2 = (√2)⁻¹
rw₁ : (√2)⁻¹ * (√2)⁻¹ * √2 = (√2)⁻¹
rw₂ : (√2)⁻¹ * ((√2)⁻¹ * √2) = (√2)⁻¹
rw₃ : (√2)⁻¹ * 1 = (√2)⁻¹
rw₄ rw₅ : (√2)⁻¹ = (√2)⁻¹
⊢ (HPow.hPow (β := ℕ) (√2) 2)⁻¹ * √2 = (√2)⁻¹

Tactic:
rw [pow_two, mul_inv, mul_assoc, inv_mul_cancel₀ (by positivity), mul_one]

Premises used: pow_two, mul_inv, mul_assoc, mul_one, inv_mul_cancel₀
-- 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 : ℝ
⊢ ‖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]
-- 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 : ℝ
h_twos : ‖2⁻¹ * √2‖ = (√2)⁻¹
h₁ : ∀ (p : E × E), ‖(√2 / 2) • p.1 + -((√2 / 2) • p.2)‖ = ‖p.1 - p.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}

Tactic:
congr! with p
-- 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 : ℝ
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‖
h₆ h₇ : (√2)⁻¹ * ‖p.1 - p.2‖ = (√2)⁻¹ * ‖p.1 - p.2‖
⊢ ‖(√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]

Premises used: norm_smul, sub_eq_add_neg, smul_sub, div_eq_inv_mul
-- 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 : ℝ
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‖
h₅ h₆ : (√2)⁻¹ * ‖p.1 + p.2‖ = (√2)⁻¹ * ‖p.1 + p.2‖
⊢ ‖(√2 / 2) • p.1 + (√2 / 2) • p.2‖ = ‖p.1 + p.2‖ / √2

Tactic:
rw [← smul_add, norm_smul, div_eq_inv_mul, div_eq_inv_mul, h_twos]

Premises used: norm_smul, div_eq_inv_mul, smul_add
-- 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 : ℝ
⊢ 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∞)

Tactic:
measure_mono fun p ↦ ?_

Premises used: MeasureTheory.measure_mono
-- 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 : ℝ
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
⊢ 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∞)

Tactic:
refine measure_mono fun p ↦ ?_

Premises used: MeasureTheory.measure_mono
-- 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
simp : ‖p.1 - p.2‖ / √2 ≤ a → b < ‖p.1 + p.2‖ / √2 → (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖
⊢ 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:
simp only [Set.mem_setOf_eq, and_imp]

Premises used: and_imp, Set.mem_setOf_eq
-- 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) / √2 < min ‖p.1‖ ‖p.2‖
⊢ (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖

Tactic:
suffices (b - a) / √2 < min ‖p.1‖ ‖p.2‖ from lt_min_iff.mp this