-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSqIntegral.lean
theorem dist_integral_mulExpNegMulSq_comp_le (f : E →ᵇ ℝ)
    {A : Subalgebra ℝ C(E, ℝ)} (hA : A.SeparatesPoints)
    (hbound : ∀ g ∈ A, ∃ C, ∀ x y : E, dist (g x) (g y) ≤ C)
    (heq : ∀ g ∈ A, ∫ x, (g : E → ℝ) x ∂P = ∫ x, (g : E → ℝ) x ∂P') (hε : 0 < ε) :
    |∫ x, mulExpNegMulSq ε (f x) ∂P - ∫ x, mulExpNegMulSq ε (f x) ∂P'| ≤ 6 * sqrt ε

Proof state:
case inr
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ C(E, ℝ)
hA : A.SeparatesPoints
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
const : ℝ := (P Set.univ).toReal ⊔ (P' Set.univ).toReal
hP'0 : ¬P' = 0
⊢ 0 < const

Tactic:
exact lt_max_of_lt_right
  (toReal_pos ((Measure.measure_univ_ne_zero).mpr hP'0) (measure_ne_top P' Set.univ))

Result:
no goals

Proof state:
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ C(E, ℝ)
hA : A.SeparatesPoints
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := (P Set.univ).toReal ⊔ (P' Set.univ).toReal
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
hKPbound : P (KP ∪ KP')ᶜ < ↑ε.toNNReal
hKP'bound : P' (KP ∪ KP')ᶜ < ↑ε.toNNReal
g : C(E, ℝ)
hgA : g ∈ A
hgapprox : ∀ x ∈ KP ∪ KP', ‖g x - f.toContinuousMap x‖ < √ε * const⁻¹
line1 : |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| < √ε
line3 : |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P| < √ε
line5 : |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P'| < √ε
line7 : |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P' - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| < √ε
⊢ const⁻¹ * (P (KP ∪ KP')).toReal ≤ 1

Tactic:
apply inv_mul_le_one_of_le₀ (le_max_of_le_left _) (le_of_lt pos_of_measure)

Result:
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ C(E, ℝ)
hA : A.SeparatesPoints
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := (P Set.univ).toReal ⊔ (P' Set.univ).toReal
pos_of_measure : 0 < const
KP : Set E
left✝¹ : KP ⊆ Set.univ
hKPco : IsCompact KP
hKPcl : IsClosed KP
KP' : Set E
left✝ : KP' ⊆ Set.univ
hKP'co : IsCompact KP'
hKP'cl : IsClosed KP'
K : Set E := KP ∪ KP'
hKco : IsCompact (KP ∪ KP')
hKcl : IsClosed (KP ∪ KP')
hKP : P KPᶜ < ENNReal.ofReal ε
hKP' : P' KP'ᶜ < ENNReal.ofReal ε
hKPbound : P (KP ∪ KP')ᶜ < ↑ε.toNNReal
hKP'bound : P' (KP ∪ KP')ᶜ < ↑ε.toNNReal
g : C(E, ℝ)
hgA : g ∈ A
hgapprox : ∀ x ∈ KP ∪ KP', ‖g x - f.toContinuousMap x‖ < √ε * const⁻¹
line1 : |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P| < √ε
line3 : |∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (g x) ∂P| < √ε
line5 : |∫ (x : E), ε.mulExpNegMulSq (g x) ∂P' - ∫ (x : E) in K, ε.mulExpNegMulSq (g x) ∂P'| < √ε
line7 : |∫ (x : E) in K, ε.mulExpNegMulSq (f x) ∂P' - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| < √ε
⊢ (P (KP ∪ KP')).toReal ≤ (P Set.univ).toReal

Proof state:
case neg
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ C(E, ℝ)
hA : A.SeparatesPoints
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε

Tactic:
let const : ℝ := (max (P Set.univ).toReal (P' Set.univ).toReal)

Result:
case neg
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ C(E, ℝ)
hA : A.SeparatesPoints
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬(P = 0 ∧ P' = 0)
const : ℝ := (P Set.univ).toReal ⊔ (P' Set.univ).toReal
⊢ |∫ (x : E), ε.mulExpNegMulSq (f x) ∂P - ∫ (x : E), ε.mulExpNegMulSq (f x) ∂P'| ≤ 6 * √ε

Proof state:
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ C(E, ℝ)
hA : A.SeparatesPoints
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
hPP' : ¬P = 0 ∨ ¬P' = 0
const : ℝ := (P Set.univ).toReal ⊔ (P' Set.univ).toReal
⊢ 0 < const

Tactic:
rcases hPP' with hP0 | hP'0

Result:
case inl
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ C(E, ℝ)
hA : A.SeparatesPoints
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
const : ℝ := (P Set.univ).toReal ⊔ (P' Set.univ).toReal
hP0 : ¬P = 0
⊢ 0 < const

case inr
ε : ℝ
E : Type u_2
inst✝⁶ : MeasurableSpace E
inst✝⁵ : PseudoEMetricSpace E
inst✝⁴ : BorelSpace E
inst✝³ : CompleteSpace E
inst✝² : SecondCountableTopology E
P P' : Measure E
inst✝¹ : IsFiniteMeasure P
inst✝ : IsFiniteMeasure P'
f : E →ᵇ ℝ
A : Subalgebra ℝ C(E, ℝ)
hA : A.SeparatesPoints
hbound : ∀ g ∈ A, ∃ C, ∀ (x y : E), dist (g x) (g y) ≤ C
heq : ∀ g ∈ A, ∫ (x : E), g x ∂P = ∫ (x : E), g x ∂P'
hε : 0 < ε
const : ℝ := (P Set.univ).toReal ⊔ (P' Set.univ).toReal
hP'0 : ¬P' = 0
⊢ 0 < const