awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasure (goal)
Goal:
Ω' : Type u_2
inst : MeasurableSpace Ω'
inst_1 : TopologicalSpace Ω'
inst_2 : BorelSpace Ω'
Ω : Type u_3
inst_3 : MeasurableSpace Ω
inst_4 : TopologicalSpace Ω
inst_5 : BorelSpace Ω
inst_6 : NormalSpace Ω'
f : Ω → Ω'
hf : IsClosedEmbedding f
M : Set (FiniteMeasure Ω') :=
  {μ : FiniteMeasure Ω' | Eq (α := ℝ≥0) ((μ : (a : Set Ω') → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)}
A :
  IsEmbedding.{u_2, u_2} (X := { x : FiniteMeasure Ω' // x ∈ M })
    (Subtype.val (p := fun (x : FiniteMeasure Ω') ↦ x ∈ M))
⊢ Continuous[instTopologicalSpaceSubtype, instTopologicalSpace]
    (M.restrict (π := fun (μ : FiniteMeasure Ω') ↦ FiniteMeasure Ω) fun (μ : FiniteMeasure Ω') ↦ comap f μ)
have rw : ContinuousOn.{u_2, u_3} (Y := FiniteMeasure Ω) (fun (μ : FiniteMeasure Ω') ↦ comap f μ) M
Tactic: rw [← continuousOn_iff_continuous_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureExt (goal)
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)
⊢ (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
have rw : Subalgebra.SeparatesPoints.{u_1, 0, 0} (α := E)
  (Subalgebra.comap (B := C(E, 𝕜)) (AlgHom.compLeftContinuous ℝ ofRealAm sorry)
    (Subalgebra.restrictScalars ℝ (StarSubalgebra.toSubalgebra (StarSubalgebra.map (toContinuousMapStarₐ 𝕜) A))))
Tactic: rw [RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureExt (hypothesis)
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)
⊢ P = P'
have hA_toReal : (Subalgebra.map (toContinuousMapₐ ℝ) A_toReal).SeparatesPoints
Tactic: have hA_toReal : (A_toReal.map (toContinuousMapₐ ℝ)).SeparatesPoints := by
    rw [RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict]
    exact Subalgebra.SeparatesPoints.rclike_to_real hA
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureExt (goal)
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
g : E →ᵇ ℝ
hgA_toReal : g ∈ A_toReal
⊢ Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
have rw : Eq.{u_2 + 1} (α := 𝕜) (∫ (x : E), (↑((g : (a : E) → ℝ) x) : 𝕜) ∂P) (∫ (x : E), (↑((g : (a : E) → ℝ) x) : 𝕜) ∂P')
Tactic: rw [← @ofReal_inj 𝕜, ← integral_ofReal, ← integral_ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureExt (hypothesis)
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
⊢ P = P'
have heq' : ∀ g ∈ A_toReal, Eq (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂P) (∫ (x : E), (g : (a : E) → ℝ) x ∂P')
Tactic: have heq' : ∀ g ∈ A_toReal, ∫ x, (g : E → ℝ) x ∂P = ∫ x, (g : E → ℝ) x ∂P' := by
    intro g hgA_toReal
    rw [← @ofReal_inj 𝕜, ← integral_ofReal, ← integral_ofReal]
    exact heq _ hgA_toReal
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureExt (goal)
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')
⊢ P = P'
have h : ∀ (f : E →ᵇ ℝ), Eq (α := ℝ) (∫ (x : E), (f : (a : E) → ℝ) x ∂P) (∫ (x : E), (f : (a : E) → ℝ) x ∂P')
Tactic: apply ext_of_forall_integral_eq_of_IsFiniteMeasure
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureExt (goal)
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)
have nth_rewrite : Tendsto (fun (ε : ℝ) ↦ 6 * √ε) (𝓝[>] 0) (𝓝 (HMul.hMul (α := ℝ) 6 0))
Tactic: nth_rewrite 3 [← mul_zero 6]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureExt (goal)
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) (𝓝 (HMul.hMul (α := ℝ) 6 0))
have apply : Tendsto sqrt (𝓝 0) (𝓝 0)
Tactic: apply tendsto_nhdsWithin_of_tendsto_nhds (Tendsto.const_mul 6 _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureExt (goal)
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)
have nth_rewrite : Tendsto sqrt (𝓝 0) (𝓝 √0)
Tactic: nth_rewrite 2 [← sqrt_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureExt (hypothesis)
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 →ᵇ ℝ
⊢ Eq (α := ℝ) (∫ (x : E), (f : (a : E) → ℝ) x ∂P) (∫ (x : E), (f : (a : E) → ℝ) x ∂P')
have h0 : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureExt (goal)
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)
have 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
Tactic: apply squeeze_zero' (eventually_nhdsWithin_of_forall (fun x _ => abs_nonneg _))
      (eventually_nhdsWithin_of_forall _) h0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureExt (hypothesis)
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)
⊢ Eq (α := ℝ) (∫ (x : E), (f : (a : E) → ℝ) x ∂P) (∫ (x : E), (f : (a : E) → ℝ) x ∂P')
have lim1 : 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ε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasureExt (hypothesis)
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)
⊢ Eq (α := ℝ) (∫ (x : E), (f : (a : E) → ℝ) x ∂P) (∫ (x : E), (f : (a : E) → ℝ) x ∂P')
have 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')|)
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))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
μ : (i : ι) → FiniteMeasure (α i)
⊢ Eq (α := ℝ≥0) ((pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0) univ) (∏ x : ι, (μ x : (a : Set (α x)) → ℝ≥0) univ)
have rw : Eq (α := ℝ≥0) ((pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0) (Set.pi (α := α) univ fun (i : ι) ↦ univ) : ℝ≥0)
  (∏ x : ι, (μ x : (a : Set (α x)) → ℝ≥0) univ : ℝ≥0)
Tactic: rw [← pi_univ (univ : Set ι), pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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)
⊢ Eq (α := ℝ≥0) ((pi (α := α) μ : (a : Set ((i : ι) → α i)) → ℝ≥0) univ) (∏ x : ι, (μ x : (a : Set (α x)) → ℝ≥0) univ)
have rw₁ : Eq (α := ℝ≥0) (∏ i : ι, (μ i : (a : Set (α i)) → ℝ≥0) univ) (∏ x : ι, (μ x : (a : Set (α x)) → ℝ≥0) univ)
Tactic: rw [← pi_univ (univ : Set ι), pi_pi]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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))
⊢ Eq (α := FiniteMeasure ((i : ι) → β i)) ((pi (α := α) μ).map fun (x : (i : ι) → α i) (i : ι) ↦ f i (x i))
    (pi (α := β) fun (i : ι) ↦ (μ i).map (f i))
have 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))
Tactic: apply Subtype.ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
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))
⊢ 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)))
have 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)))
Tactic: rw [Measure.pi_map_pi f_mble]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
⊢ Continuous[Pi.topologicalSpace, instTopologicalSpace] fun (μ : (i : ι) → ProbabilityMeasure (α i)) ↦ pi (α := α) μ
have refine : ∀ (μ : (i : ι) → ProbabilityMeasure (α i)),
  ContinuousAt (Y := ProbabilityMeasure ((i : ι) → α i)) (fun (μ : (i : ι) → ProbabilityMeasure (α i)) ↦ pi (α := α) μ)
    μ
Tactic: refine continuous_iff_continuousAt.2 (fun μ ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)
s' : (i : ι) → Set (α i)
s'meas : ∀ (i : ι), MeasurableSet (s' i)
hs' : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s' i)) : ℝ≥0) (0 : ℝ≥0)
⊢ Set.pi (α := α) univ s ∩ Set.pi (α := α) univ s' ∈ S
have refine : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier ((fun (i : ι) ↦ s i ∩ s' i) i)) : ℝ≥0) (0 : ℝ≥0)
Tactic: refine ⟨fun i ↦ s i ∩ s' i, pi_inter_distrib.symm, fun i ↦ (smeas i).inter (s'meas i),
      fun i ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
s : (i : ι) → Set (α i)
smeas : ∀ (i : ι), MeasurableSet (s i)
hs : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)
s' : (i : ι) → Set (α i)
s'meas : ∀ (i : ι), MeasurableSet (s' i)
hs' : ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s' i)) : ℝ≥0) (0 : ℝ≥0)
i : ι
⊢ Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier ((fun (i : ι) ↦ s i ∩ s' i) i)) : ℝ≥0) (0 : ℝ≥0)
have simp_rw : ∀
  (hs :
    ∀ (i : ι), Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (s i)) : ℝ≥0∞) (0 : ℝ≥0∞))
  (hs' :
    ∀ (i : ι),
      Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (s' i)) : ℝ≥0∞) (0 : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) (((↑(μ i) : Measure (α i)) : (a : Set (α i)) → ℝ≥0∞) (frontier (s i ∩ s' i)) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [null_iff_toMeasure_null] at hs hs' ⊢
Cleared hypotheses: hs, hs'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.FiniteMeasurePi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : Fintype ι
inst_1 : (i : ι) → MeasurableSpace (α i)
inst_2 : (i : ι) → TopologicalSpace (α i)
inst_3 : ∀ (i : ι), SecondCountableTopology.{u_2} (α i)
inst_4 : ∀ (i : ι), PseudoMetrizableSpace.{u_2} (α i)
inst_5 : ∀ (i : ι), OpensMeasurableSpace.{u_2} (α i)
μ : (i : ι) → ProbabilityMeasure (α i)
S : Set (Set ((i : ι) → α i)) :=
  {t : Set ((i : ι) → α i) |
    ∃ (s : (i : ι) → Set (α i)),
      t = Set.pi (α := α) univ s ∧
        (∀ (i : ι), MeasurableSet (s i)) ∧
          ∀ (i : ι), Eq (α := ℝ≥0) ((μ i : (a : Set (α i)) → ℝ≥0) (frontier (s i)) : ℝ≥0) (0 : ℝ≥0)}
⊢ ContinuousAt (Y := ProbabilityMeasure ((i : ι) → α i)) (fun (μ : (i : ι) → ProbabilityMeasure (α i)) ↦ pi (α := α) μ)
    μ
have this : IsPiSystem S
Tactic: have : IsPiSystem S := by
    rintro - ⟨s, rfl, smeas, hs⟩ - ⟨s', rfl, s'meas, hs'⟩ -
    refine ⟨fun i ↦ s i ∩ s' i, pi_inter_distrib.symm, fun i ↦ (smeas i).inter (s'meas i),
      fun i ↦ ?_⟩
    simp_rw [null_iff_toMeasure_null] at hs hs' ⊢
    exact null_frontier_inter (hs i) (hs' i)