awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst_4 : IsFiniteMeasure P'
A : Subalgebra ℝ (E →ᵇ ℝ)
hε : 0 < ε
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
g : E →ᵇ ℝ
hgA : g ∈ A
one_add_inv_mul_mem : ∀ (n : ℕ), g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n ∈ A
rw :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ ∫ (x : E), (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x ∂P') atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P'))
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ ∫ (x : E), (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x ∂P) atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P'))

Tactic:
rw [funext fun n => heq _ (one_add_inv_mul_mem n)]

Premises used: HMul.hMul, Nat.cast, funext, Inv.inv, HPow.hPow, HAdd.hAdd, HSMul.hSMul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst_4 : IsFiniteMeasure P'
A : Subalgebra ℝ (E →ᵇ ℝ)
hε : 0 < ε
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
g : E →ᵇ ℝ
hgA : g ∈ A
one_add_inv_mul_mem : ∀ (n : ℕ), g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n ∈ A
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ ∫ (x : E), (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x ∂P') atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P'))

Tactic:
tendsto_integral_mul_one_add_inv_smul_sq_pow g hε

Premises used: tendsto_integral_mul_one_add_inv_smul_sq_pow
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst_4 : IsFiniteMeasure P'
A : Subalgebra ℝ (E →ᵇ ℝ)
hε : 0 < ε
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
g : E →ᵇ ℝ
hgA : g ∈ A
one_add_inv_mul_mem : ∀ (n : ℕ), g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n ∈ A
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ ∫ (x : E), (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x ∂P') atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P'))

Tactic:
exact tendsto_integral_mul_one_add_inv_smul_sq_pow g hε

Premises used: tendsto_integral_mul_one_add_inv_smul_sq_pow
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst_4 : IsFiniteMeasure P'
A : Subalgebra ℝ (E →ᵇ ℝ)
hε : 0 < ε
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
g : E →ᵇ ℝ
hgA : g ∈ A
one_add_inv_mul_mem : ∀ (n : ℕ), g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n ∈ A
⊢ Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ ∫ (x : E), (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x ∂P) atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P'))

Tactic:
have limP : Tendsto (fun n : ℕ => ∫ x, (g * (1 + (n : ℝ)⁻¹ • -(ε • g * g)) ^ n) x ∂P) atTop
      (𝓝 (∫ x, mulExpNegMulSq ε (g x) ∂P')) := by
    rw [funext fun n => heq _ (one_add_inv_mul_mem n)]
    exact tendsto_integral_mul_one_add_inv_smul_sq_pow g hε
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst_4 : IsFiniteMeasure P'
A : Subalgebra ℝ (E →ᵇ ℝ)
hε : 0 < ε
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
g : E →ᵇ ℝ
hgA : g ∈ A
one_add_inv_mul_mem : ∀ (n : ℕ), g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n ∈ A
limP :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ ∫ (x : E), (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x ∂P) atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P'))
⊢ Eq (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
    (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')

Tactic:
tendsto_nhds_unique
    (tendsto_integral_mul_one_add_inv_smul_sq_pow g hε) limP

Premises used: tendsto_integral_mul_one_add_inv_smul_sq_pow, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
P' : Measure E
inst_4 : IsFiniteMeasure P'
A : Subalgebra ℝ (E →ᵇ ℝ)
hε : 0 < ε
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
g : E →ᵇ ℝ
hgA : g ∈ A
one_add_inv_mul_mem : ∀ (n : ℕ), g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n ∈ A
limP :
  Tendsto (β := ℝ)
    (fun (n : ℕ) ↦ ∫ (x : E), (g * (1 + HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (-(ε • g * g))) ^ n : (a : E) → ℝ) x ∂P) atTop
    (𝓝 (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P'))
⊢ Eq (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
    (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P')

Tactic:
exact tendsto_nhds_unique
    (tendsto_integral_mul_one_add_inv_smul_sq_pow g hε) limP

Premises used: tendsto_integral_mul_one_add_inv_smul_sq_pow, tendsto_nhds_unique
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : (P : (a : Set E) → ℝ≥0∞) Kᶜ < (↑ε.toNNReal : ℝ≥0∞)
apply : P.real Kᶜ * (√ε)⁻¹ < √ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| <
    √ε

Tactic:
apply lt_of_le_of_lt (norm_integral_sub_setIntegral_le
    (Eventually.of_forall (fun _ => abs_mulExpNegMulSq_le hε)) hK
    (integrable_mulExpNegMulSq_comp f hε))

Premises used: lt_of_le_of_lt, MeasureTheory.norm_integral_sub_setIntegral_le, Filter.Eventually.of_forall, integrable_mulExpNegMulSq_comp
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : (P : (a : Set E) → ℝ≥0∞) Kᶜ < (↑ε.toNNReal : ℝ≥0∞)
rw : P.real Kᶜ < ε
⊢ P.real Kᶜ * (√ε)⁻¹ < √ε

Tactic:
rw [mul_inv_lt_iff₀ (sqrt_pos_of_pos hε), mul_self_sqrt (le_of_lt hε)]

Premises used: mul_inv_lt_iff₀, le_of_lt, Real.mul_self_sqrt, Real.sqrt_pos_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : (P : (a : Set E) → ℝ≥0∞) Kᶜ < (↑ε.toNNReal : ℝ≥0∞)
⊢ P.real Kᶜ < ε

Tactic:
toReal_lt_of_lt_ofReal hKP

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_lt_of_lt_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
f : C(E, ℝ)
K : Set E
hK : MeasurableSet K
hε : 0 < ε
hKP : (P : (a : Set E) → ℝ≥0∞) Kᶜ < (↑ε.toNNReal : ℝ≥0∞)
⊢ P.real Kᶜ < ε

Tactic:
exact toReal_lt_of_lt_ofReal hKP

Premises used: ENNReal.toReal_lt_of_lt_ofReal
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
K : Set E
hK : IsCompact K
hKmeas : MeasurableSet K
f g : C(E, ℝ)
δ : ℝ
hε : 0 < ε
hfg : ∀ x ∈ K, |HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)| < δ
rw :
  Norm.norm (E := ℝ)
      (∫ (a : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) a) - ε.mulExpNegMulSq ((f : (a : E) → ℝ) a) ∂P) ≤
    δ * ENNReal.toReal ((P : (a : Set E) → ℝ≥0∞) K)
⊢ |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| ≤
    δ * ENNReal.toReal ((P : (a : Set E) → ℝ≥0∞) K)

Tactic:
rw [← (integral_sub (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas g)
      (integrable_mulExpNegMulSq_comp_restrict_of_isCompact hK hKmeas f)), ← norm_eq_abs]

Premises used: MeasureTheory.integral_sub, integrable_mulExpNegMulSq_comp_restrict_of_isCompact, Real.norm_eq_abs
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
K : Set E
hK : IsCompact K
hKmeas : MeasurableSet K
f g : C(E, ℝ)
δ : ℝ
hε : 0 < ε
hfg : ∀ x ∈ K, |HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)| < δ
⊢ Norm.norm (E := ℝ)
      (∫ (a : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) a) - ε.mulExpNegMulSq ((f : (a : E) → ℝ) a) ∂P) ≤
    δ * ENNReal.toReal ((P : (a : Set E) → ℝ≥0∞) K)

Tactic:
norm_setIntegral_le_of_norm_le_const hK.measure_lt_top
    (fun x hxK => le_trans (dist_mulExpNegMulSq_le_dist hε) (hfg x hxK).le)

Premises used: MeasureTheory.Measure.real, LT.lt.le, MeasureTheory.norm_setIntegral_le_of_norm_le_const, IsCompact.measure_lt_top, Real.dist_mulExpNegMulSq_le_dist, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
E : Type u_1
inst : TopologicalSpace E
inst_1 : MeasurableSpace E
inst_2 : BorelSpace E
P : Measure E
inst_3 : IsFiniteMeasure P
ε : ℝ
K : Set E
hK : IsCompact K
hKmeas : MeasurableSet K
f g : C(E, ℝ)
δ : ℝ
hε : 0 < ε
hfg : ∀ x ∈ K, |HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)| < δ
⊢ Norm.norm (E := ℝ)
      (∫ (a : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) a) - ε.mulExpNegMulSq ((f : (a : E) → ℝ) a) ∂P) ≤
    δ * ENNReal.toReal ((P : (a : Set E) → ℝ≥0∞) K)

Tactic:
exact norm_setIntegral_le_of_norm_le_const hK.measure_lt_top
    (fun x hxK => le_trans (dist_mulExpNegMulSq_le_dist hε) (hfg x hxK).le)

Premises used: LT.lt.le, MeasureTheory.norm_setIntegral_le_of_norm_le_const, IsCompact.measure_lt_top, le_trans
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
pos :
  ∀ (hPP' : P = 0 ∧ P' = 0),
    |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
          (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
      6 * √ε
neg :
  ∀ (hPP' : ¬(P = 0 ∧ P' = 0)),
    |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
          (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
      6 * √ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε

Tactic:
by_cases hPP' : P = 0 ∧ P' = 0
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : P = 0 ∧ P' = 0
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε

Tactic:
simp only [hPP', integral_zero_measure, sub_self, abs_zero, Nat.ofNat_pos,
    mul_nonneg_iff_of_pos_left, (le_of_lt (sqrt_pos_of_pos hε))]

Premises used: sub_self, le_of_lt, Nat.ofNat_pos, abs_zero, mul_nonneg_iff_of_pos_left, Real.sqrt_pos_of_pos, MeasureTheory.integral_zero_measure
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
rw :
  ∀ (hPP' : ¬P = 0 ∨ ¬P' = 0),
    let const := max (P.real Set.univ) (P'.real Set.univ);
    0 < const
⊢ 0 < const

Tactic:
rw [not_and_or] at hPP'

Premises used: not_and_or
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬P = 0 ∨ ¬P' = 0
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
inl : ∀ (hP0 : ¬P = 0), 0 < const
inr : ∀ (hP'0 : ¬P' = 0), 0 < const
⊢ 0 < const

Tactic:
rcases hPP' with hP0 | hP'0
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
hP0 : ¬P = 0
⊢ Ne (α := ℝ≥0∞) ((P : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
hP0 : ¬P = 0
⊢ 0 < const

Tactic:
exact lt_max_of_lt_left
        (toReal_pos ((Measure.measure_univ_ne_zero).mpr hP0) (by finiteness))

Premises used: Iff.mpr, lt_max_of_lt_left, MeasureTheory.Measure.measure_univ_ne_zero, ENNReal.toReal_pos
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
hP'0 : ¬P' = 0
⊢ Ne (α := ℝ≥0∞) ((P' : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
hP'0 : ¬P' = 0
⊢ 0 < const

Tactic:
exact lt_max_of_lt_right
        (toReal_pos ((Measure.measure_univ_ne_zero).mpr hP'0) (by finiteness))

Premises used: Iff.mpr, MeasureTheory.Measure.measure_univ_ne_zero, lt_max_of_lt_right, ENNReal.toReal_pos
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
⊢ 0 < const

Tactic:
have pos_of_measure : 0 < const := by
    rw [not_and_or] at hPP'
    rcases hPP' with hP0 | hP'0
    · exact lt_max_of_lt_left
        (toReal_pos ((Measure.measure_univ_ne_zero).mpr hP0) (by finiteness))
    · exact lt_max_of_lt_right
        (toReal_pos ((Measure.measure_univ_ne_zero).mpr hP'0) (by finiteness))
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
neg :
  ∀ KP ⊆ Set.univ,
    ∀ (hKPco : IsCompact KP) (hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP)
      (hKP : (P : (a : Set E) → ℝ≥0∞) (Set.univ \ KP) < ENNReal.ofReal ε),
      |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
            (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
        6 * √ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε

Tactic:
obtain ⟨KP, _, hKPco, hKPcl, hKP⟩ := MeasurableSet.exists_isCompact_isClosed_diff_lt
    (MeasurableSet.univ) (measure_ne_top P Set.univ) (ofReal_pos.mpr hε).ne'

Premises used: Iff.mpr, MeasurableSet.exists_isCompact_isClosed_diff_lt, Set.univ, MeasureTheory.measure_ne_top, LT.lt.ne', ENNReal.ofReal_pos, MeasurableSet.univ
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
hKP : (P : (a : Set E) → ℝ≥0∞) (Set.univ \ KP) < ENNReal.ofReal ε
neg :
  ∀ KP' ⊆ Set.univ,
    ∀ (hKP'co : IsCompact KP') (hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP')
      (hKP' : (P' : (a : Set E) → ℝ≥0∞) (Set.univ \ KP') < ENNReal.ofReal ε),
      |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
            (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
        6 * √ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')| ≤
    6 * √ε

Tactic:
obtain ⟨KP', _, hKP'co, hKP'cl, hKP'⟩ := MeasurableSet.exists_isCompact_isClosed_diff_lt
    (MeasurableSet.univ) (measure_ne_top P' Set.univ) (ofReal_pos.mpr hε).ne'

Premises used: Iff.mpr, MeasurableSet.exists_isCompact_isClosed_diff_lt, Set.univ, MeasureTheory.measure_ne_top, LT.lt.ne', ENNReal.ofReal_pos, MeasurableSet.univ
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
hKP : (P : (a : Set E) → ℝ≥0∞) (Set.univ \ KP) < ENNReal.ofReal ε
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
hKP' : (P' : (a : Set E) → ℝ≥0∞) (Set.univ \ KP') < ENNReal.ofReal ε
K : Set E := KP ∪ KP'
⊢ IsCompact (KP ∪ KP')

Tactic:
have hKco := IsCompact.union hKPco hKP'co
-- Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSqIntegral
Goal:
ε : ℝ
E : Type u_2
inst : MeasurableSpace E
inst_1 : PseudoEMetricSpace E
inst_2 : BorelSpace E
inst_3 : CompleteSpace E
inst_4 : SecondCountableTopology E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ (E →ᵇ ℝ)
hA : (Subalgebra.map (toContinuousMapₐ ℝ) A).SeparatesPoints
heq : ∀ g ∈ A, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := max (P.real Set.univ) (P'.real Set.univ)
pos_of_measure : 0 < const
KP : Set E
left : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
hKP : (P : (a : Set E) → ℝ≥0∞) (Set.univ \ KP) < ENNReal.ofReal ε
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
hKP' : (P' : (a : Set E) → ℝ≥0∞) (Set.univ \ KP') < ENNReal.ofReal ε
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
⊢ IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')

Tactic:
have hKcl := IsClosed.union hKPcl hKP'cl