awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
⊢ (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε

Tactic:
simp only [← Set.compl_eq_univ_diff] at hKP hKP'

Premises used: Set.compl_eq_univ_diff
-- 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')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP₁ : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
⊢ (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε

Tactic:
simp only [← Set.compl_eq_univ_diff] at hKP hKP'

Premises used: Set.compl_eq_univ_diff
-- 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
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
⊢ (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)

Tactic:
have hKPbound : P (KP ∪ KP')ᶜ < ε.toNNReal := lt_of_le_of_lt
        (measure_mono (Set.compl_subset_compl_of_subset (Set.subset_union_left))) hKP
-- 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
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
⊢ (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)

Tactic:
have hKP'bound : P' (KP ∪ KP')ᶜ < ε.toNNReal := lt_of_le_of_lt
        (measure_mono (Set.compl_subset_compl_of_subset (Set.subset_union_right))) hKP'
-- 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
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
neg :
  ∀ (g' : C(E, ℝ)) (hg'A : g' ∈ Subalgebra.map (toContinuousMapₐ ℝ) A)
    (hg'approx :
      ∀ x ∈ KP ∪ KP',
        ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹),
    |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 ⟨g', hg'A, hg'approx⟩ :=
      ContinuousMap.exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints
      hA f hKco (Left.mul_pos (sqrt_pos_of_pos hε) (inv_pos_of_pos pos_of_measure))

Premises used: toContinuousMap, ContinuousMap.exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints, inv_pos_of_pos, Left.mul_pos, Real.sqrt_pos_of_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)
pos_of_measure : 0 < const
KP : Set E
left : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'A : g' ∈ Subalgebra.map (toContinuousMapₐ ℝ) A
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
⊢ ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'

Tactic:
simp only [Subalgebra.mem_map] at hg'A

Premises used: Subalgebra.mem_map
-- 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
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
⊢ g ∈ A

Tactic:
have hgA : g ∈ A := hg'A.choose_spec.1
-- 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
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
rw : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
⊢ ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹

Tactic:
rw [← coe_toContinuousMapₐ ℝ g, hg'A.choose_spec.2]

Premises used: Exists.choose_spec, Real, And.right, BoundedContinuousFunction.coe_toContinuousMapₐ
-- 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
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
⊢ ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹

Tactic:
hg'approx

Premises used: Set.Mem
-- 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
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
⊢ ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹

Tactic:
exact hg'approx
-- 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
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
⊢ ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹

Tactic:
have hgapprox : ∀ x ∈ K, ‖g x - f x‖ < √ε * const⁻¹ := by
    rw [← coe_toContinuousMapₐ ℝ g, hg'A.choose_spec.2]
    exact hg'approx
-- 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
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
⊢ |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| <
    √ε

Tactic:
have line1 : |∫ x, mulExpNegMulSq ε (f x) ∂P
      - ∫ x in K, mulExpNegMulSq ε (f x) ∂P| < √ε :=
    abs_integral_sub_setIntegral_mulExpNegMulSq_comp_lt
      f (IsClosed.measurableSet hKcl) hε hKPbound
-- 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
KP' : Set E
left_1 : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (KP ∪ KP')
hKP : (P : (a : Set E) → ℝ≥0∞) KPᶜ < ENNReal.ofReal ε
hKP' : (P' : (a : Set E) → ℝ≥0∞) KP'ᶜ < ENNReal.ofReal ε
hKPbound : (P : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
hKP'bound : (P' : (a : Set E) → ℝ≥0∞) (KP ∪ KP')ᶜ < (↑ε.toNNReal : ℝ≥0∞)
g' : C(E, ℝ)
hg'approx :
  ∀ x ∈ KP ∪ KP',
    ‖HSub.hSub (α := ℝ) (β := ℝ) ((g' : (a : E) → ℝ) x : ℝ) (((↑f : C(E, ℝ)) : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
hg'A : ∃ x ∈ A, (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g'
g : E →ᵇ ℝ := hg'A.choose (p := fun (x : E →ᵇ ℝ) ↦ x ∈ A ∧ (toContinuousMapₐ ℝ : (a : E →ᵇ ℝ) → C(E, ℝ)) x = g')
hgA : g ∈ A
hgapprox : ∀ x ∈ K, ‖HSub.hSub (α := ℝ) (β := ℝ) ((g : (a : E) → ℝ) x : ℝ) ((f : (a : E) → ℝ) x : ℝ)‖ < √ε * const⁻¹
line1 :
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)| <
    √ε
rw :
  |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
        (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)| <
    √ε
⊢ |HSub.hSub (α := ℝ) (∫ (x : E) in K, ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)
        (∫ (x : E), ε.mulExpNegMulSq ((g : (a : E) → ℝ) x) ∂P)| <
    √ε

Tactic:
rw [abs_sub_comm]

Premises used: abs_sub_comm