awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
f : E →ᵇ ℝ
nth_rewrite : Tendsto (fun (ε : ℝ) ↦ 6 * √ε) (𝓝[>] 0) (𝓝 (HMul.hMul (α := ℝ) 6 0))
⊢ Tendsto (β := ℝ) (fun (ε : ℝ) ↦ 6 * √ε) (𝓝[>] 0) (𝓝 0)

Tactic:
nth_rewrite 3 [← mul_zero 6]

Premises used: MulZeroClass.mul_zero, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
f : E →ᵇ ℝ
apply : Tendsto sqrt (𝓝 0) (𝓝 0)
⊢ Tendsto (fun (ε : ℝ) ↦ 6 * √ε) (𝓝[>] 0) (𝓝 (HMul.hMul (α := ℝ) 6 0))

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds (Tendsto.const_mul 6 _)

Premises used: Filter.Tendsto.const_mul, tendsto_nhdsWithin_of_tendsto_nhds, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
f : E →ᵇ ℝ
nth_rewrite : Tendsto sqrt (𝓝 0) (𝓝 √0)
⊢ Tendsto sqrt (𝓝 0) (𝓝 0)

Tactic:
nth_rewrite 2 [← sqrt_zero]

Premises used: Real.sqrt_zero
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
f : E →ᵇ ℝ
⊢ Tendsto sqrt (𝓝 0) (𝓝 √0)

Tactic:
Continuous.tendsto continuous_sqrt 0

Premises used: Real.continuous_sqrt, Continuous.tendsto, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
f : E →ᵇ ℝ
⊢ Tendsto sqrt (𝓝 0) (𝓝 √0)

Tactic:
exact Continuous.tendsto continuous_sqrt 0

Premises used: Real.continuous_sqrt, Continuous.tendsto, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
f : E →ᵇ ℝ
⊢ Tendsto (β := ℝ) (fun (ε : ℝ) ↦ 6 * √ε) (𝓝[>] 0) (𝓝 0)

Tactic:
have h0 : Tendsto (fun ε : ℝ => 6 * √ε) (𝓝[>] 0) (𝓝 0) := by
    nth_rewrite 3 [← mul_zero 6]
    apply tendsto_nhdsWithin_of_tendsto_nhds (Tendsto.const_mul 6 _)
    nth_rewrite 2 [← sqrt_zero]
    exact Continuous.tendsto continuous_sqrt 0
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
f : E →ᵇ ℝ
h0 : Tendsto (β := ℝ) (fun (ε : ℝ) ↦ 6 * √ε) (𝓝[>] 0) (𝓝 0)
apply :
  ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Ioi 0) x →
      |HSub.hSub (α := ℝ) (∫ (x_1 : E), x.mulExpNegMulSq ((f : (a : E) → ℝ) x_1) ∂P)
            (∫ (x_1 : E), x.mulExpNegMulSq ((f : (a : E) → ℝ) x_1) ∂P')| ≤
        6 * √x
⊢ Tendsto (β := ℝ)
    (fun (ε : ℝ) ↦
      |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
          (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')|)
    (𝓝[>] 0) (𝓝 0)

Tactic:
apply squeeze_zero' (eventually_nhdsWithin_of_forall (fun x _ => abs_nonneg _))
      (eventually_nhdsWithin_of_forall _) h0

Premises used: abs_nonneg, eventually_nhdsWithin_of_forall, squeeze_zero'
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
f : E →ᵇ ℝ
h0 : Tendsto (β := ℝ) (fun (ε : ℝ) ↦ 6 * √ε) (𝓝[>] 0) (𝓝 0)
⊢ ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Ioi 0) x →
      |HSub.hSub (α := ℝ) (∫ (x_1 : E), x.mulExpNegMulSq ((f : (a : E) → ℝ) x_1) ∂P)
            (∫ (x_1 : E), x.mulExpNegMulSq ((f : (a : E) → ℝ) x_1) ∂P')| ≤
        6 * √x

Tactic:
fun ε hε => dist_integral_mulExpNegMulSq_comp_le f hA_toReal heq' hε

Premises used: dist_integral_mulExpNegMulSq_comp_le
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
f : E →ᵇ ℝ
h0 : Tendsto (β := ℝ) (fun (ε : ℝ) ↦ 6 * √ε) (𝓝[>] 0) (𝓝 0)
⊢ ∀ (x : ℝ),
    Membership.mem (γ := Set ℝ) (Set.Ioi 0) x →
      |HSub.hSub (α := ℝ) (∫ (x_1 : E), x.mulExpNegMulSq ((f : (a : E) → ℝ) x_1) ∂P)
            (∫ (x_1 : E), x.mulExpNegMulSq ((f : (a : E) → ℝ) x_1) ∂P')| ≤
        6 * √x

Tactic:
exact fun ε hε => dist_integral_mulExpNegMulSq_comp_le f hA_toReal heq' hε

Premises used: dist_integral_mulExpNegMulSq_comp_le
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
f : E →ᵇ ℝ
h0 : Tendsto (β := ℝ) (fun (ε : ℝ) ↦ 6 * √ε) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (β := ℝ)
    (fun (ε : ℝ) ↦
      |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
          (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')|)
    (𝓝[>] 0) (𝓝 0)

Tactic:
have lim1 : Tendsto (fun ε => |∫ x, mulExpNegMulSq ε (f x) ∂P - ∫ x, mulExpNegMulSq ε (f x) ∂P'|)
      (𝓝[>] 0) (𝓝 0) := by
    apply squeeze_zero' (eventually_nhdsWithin_of_forall (fun x _ => abs_nonneg _))
      (eventually_nhdsWithin_of_forall _) h0
    exact fun ε hε => dist_integral_mulExpNegMulSq_comp_le f hA_toReal heq' hε
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
f : E →ᵇ ℝ
h0 : Tendsto (β := ℝ) (fun (ε : ℝ) ↦ 6 * √ε) (𝓝[>] 0) (𝓝 0)
lim1 :
  Tendsto (β := ℝ)
    (fun (ε : ℝ) ↦
      |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
          (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')|)
    (𝓝[>] 0) (𝓝 0)
⊢ Tendsto
    (fun (ε : ℝ) ↦
      |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
          (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')|)
    (𝓝[>] 0) (𝓝 |HSub.hSub (α := ℝ) (∫ (x : E), (f : (a : E) → ℝ) x ∂P) (∫ (x : E), (f : (a : E) → ℝ) x ∂P')|)

Tactic:
have lim2 : Tendsto (fun ε => |∫ x, mulExpNegMulSq ε (f x) ∂P
      - ∫ x, mulExpNegMulSq ε (f x) ∂P'|) (𝓝[>] 0)
      (𝓝 |∫ x, f x ∂↑P - ∫ x, f x ∂↑P'|) :=
    Tendsto.abs (Tendsto.sub (tendsto_integral_mulExpNegMulSq_comp f)
      (tendsto_integral_mulExpNegMulSq_comp f))
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
f : E →ᵇ ℝ
h0 : Tendsto (β := ℝ) (fun (ε : ℝ) ↦ 6 * √ε) (𝓝[>] 0) (𝓝 0)
lim1 :
  Tendsto (β := ℝ)
    (fun (ε : ℝ) ↦
      |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
          (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')|)
    (𝓝[>] 0) (𝓝 0)
lim2 :
  Tendsto
    (fun (ε : ℝ) ↦
      |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
          (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')|)
    (𝓝[>] 0) (𝓝 |HSub.hSub (α := ℝ) (∫ (x : E), (f : (a : E) → ℝ) x ∂P) (∫ (x : E), (f : (a : E) → ℝ) x ∂P')|)
⊢ Eq (α := ℝ) (∫ (x : E), (f : (a : E) → ℝ) x ∂P) (∫ (x : E), (f : (a : E) → ℝ) x ∂P')

Tactic:
eq_of_abs_sub_eq_zero (tendsto_nhds_unique lim2 lim1)

Premises used: eq_of_abs_sub_eq_zero, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : PseudoEMetricSpace E
inst_3 : BorelSpace E
inst_4 : CompleteSpace E
inst_5 : SecondCountableTopology E
P P' : Measure E
inst_6 : IsFiniteMeasure P
inst_7 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
A_toReal : Subalgebra ℝ (E →ᵇ ℝ) :=
  Subalgebra.comap (AlgHom.compLeftContinuousBounded ℝ ofRealAm (C := 1) ⋯)
    (Subalgebra.restrictScalars ℝ A.toSubalgebra)
hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
f : E →ᵇ ℝ
h0 : Tendsto (β := ℝ) (fun (ε : ℝ) ↦ 6 * √ε) (𝓝[>] 0) (𝓝 0)
lim1 :
  Tendsto (β := ℝ)
    (fun (ε : ℝ) ↦
      |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
          (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')|)
    (𝓝[>] 0) (𝓝 0)
lim2 :
  Tendsto
    (fun (ε : ℝ) ↦
      |HSub.hSub (α := ℝ) (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P)
          (∫ (x : E), ε.mulExpNegMulSq ((f : (a : E) → ℝ) x) ∂P')|)
    (𝓝[>] 0) (𝓝 |HSub.hSub (α := ℝ) (∫ (x : E), (f : (a : E) → ℝ) x ∂P) (∫ (x : E), (f : (a : E) → ℝ) x ∂P')|)
⊢ Eq (α := ℝ) (∫ (x : E), (f : (a : E) → ℝ) x ∂P) (∫ (x : E), (f : (a : E) → ℝ) x ∂P')

Tactic:
exact eq_of_abs_sub_eq_zero (tendsto_nhds_unique lim2 lim1)

Premises used: eq_of_abs_sub_eq_zero, tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
⊢ P = P'

Tactic:
ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable hA heq

Premises used: MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasureExt
Goal:
E : Type u_1
𝕜 : Type u_2
inst : RCLike 𝕜
inst_1 : MeasurableSpace E
inst_2 : TopologicalSpace E
inst_3 : PolishSpace E
inst_4 : BorelSpace E
P P' : Measure E
inst_5 : IsFiniteMeasure P
inst_6 : IsFiniteMeasure P'
A : StarSubalgebra 𝕜 (E →ᵇ 𝕜)
hA :
  Subalgebra.SeparatesPoints.{u_1, u_2, u_2} (α := E) (A := 𝕜)
    (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))
heq : ∀ g ∈ A, Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P) (∫ (x : E), (g : (a : E) → 𝕜) x ∂P')
this : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace E := TopologicalSpace.upgradeIsCompletelyMetrizable E
⊢ P = P'

Tactic:
exact ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable hA heq

Premises used: MeasureTheory.ext_of_forall_mem_subalgebra_integral_eq_of_pseudoEMetric_complete_countable
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → FiniteMeasure (α i)
⊢ (↑(pi (α := α) μ) : Measure ((i : ι) → α i)) = Measure.pi (α := α) fun (i : ι) ↦ (↑(μ i) : Measure (α i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → FiniteMeasure (α i)
s : (i : ι) → Set (α i)
⊢ Eq (α := ℝ≥0) ((pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0) (Set.pi (α := α) univ s) : ℝ≥0)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0) (s i) : ℝ≥0)

Tactic:
simp [coeFn_def]

Premises used: MeasureTheory.FiniteMeasure.coeFn_def
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → FiniteMeasure (α i)
rw :
  Eq (α := ℝ≥0) ((pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0) (Set.pi (α := α) univ fun (i : ι) ↦ univ) : ℝ≥0)
    (∏ x : ι, (μ x : (a : Set (α x)) → ℝ≥0) univ : ℝ≥0)
rw₁ rw₂ : Eq (α := ℝ≥0) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0) univ) (∏ x : ι, (μ x : (a : Set (α x)) → ℝ≥0) univ)
⊢ Eq (α := ℝ≥0) ((pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0) univ) (∏ x : ι, (μ x : (a : Set (α x)) → ℝ≥0) univ)

Tactic:
rw [← pi_univ (univ : Set ι), pi_pi]

Premises used: Set.univ, MeasureTheory.FiniteMeasure.pi_pi, Set.pi_univ
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → FiniteMeasure (α i)
β : ι → Type u_3
inst_2 : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → α i → β i
f_mble : ∀ (i : ι), AEMeasurable (f i) (↑(μ i) : Measure (α i))
a :
  Eq (α := Measure ((i : ι) → β i))
    (↑((pi (α := α) μ).map fun (x : (i : ι) → α i) (i : ι) ↦ f i (x i)) : Measure ((i : ι) → β i))
    (↑(pi (α := β) fun (i : ι) ↦ (μ i).map (f i)) : Measure ((i : ι) → β i))
⊢ Eq (α := FiniteMeasure ((i : ι) → β i)) ((pi (α := α) μ).map fun (x : (i : ι) → α i) (i : ι) ↦ f i (x i))
    (pi (α := β) fun (i : ι) ↦ (μ i).map (f i))

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → FiniteMeasure (α i)
β : ι → Type u_3
inst_2 : (i : ι) → MeasurableSpace (β i)
f : (i : ι) → α i → β i
f_mble : ∀ (i : ι), AEMeasurable (f i) (↑(μ i) : Measure (α i))
a a₁ :
  Eq (α := Measure ((i : ι) → β i)) (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) (↑(μ i) : Measure (α i)))
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) (↑(μ i) : Measure (α i)))
⊢ Eq (α := Measure ((i : ι) → β i))
    (Measure.map (fun (x : (i : ι) → α i) (i : ι) ↦ f i (x i))
      (Measure.pi (α := α) fun (i : ι) ↦ (↑(μ i) : Measure (α i))))
    (Measure.pi (α := β) fun (i : ι) ↦ Measure.map (f i) (↑(μ i) : Measure (α i)))

Tactic:
rw [Measure.pi_map_pi f_mble]

Premises used: MeasureTheory.Measure.pi_map_pi
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
⊢ (↑(pi (α := α) μ) : Measure ((i : ι) → α i)) = Measure.pi (α := α) fun (i : ι) ↦ (↑(μ i) : Measure (α i))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.FiniteMeasurePi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
s : (i : ι) → Set (α i)
⊢ Eq (α := ℝ≥0) ((pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0) (Set.pi (α := α) univ s) : ℝ≥0)
    (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0) (s i) : ℝ≥0)

Tactic:
simp [coeFn_def]

Premises used: MeasureTheory.ProbabilityMeasure.coeFn_def