awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
⊢ (g • μ).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
have rw : (g • μ).addHaarScalarFactor (g • ν) * (g • ν).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
Tactic: rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_domSMul,
    mul_comm, ← addHaarScalarFactor_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
rw : (g • μ).addHaarScalarFactor (g • ν) * (g • ν).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
⊢ (g • μ).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
have rw₁ : μ.addHaarScalarFactor ν * (g • ν).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
Tactic: rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_domSMul,
    mul_comm, ← addHaarScalarFactor_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
rw : (g • μ).addHaarScalarFactor (g • ν) * (g • ν).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
rw₁ : μ.addHaarScalarFactor ν * (g • ν).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
⊢ (g • μ).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
have rw₂ : (g • ν).addHaarScalarFactor μ * μ.addHaarScalarFactor ν = (g • ν).addHaarScalarFactor ν
Tactic: rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_domSMul,
    mul_comm, ← addHaarScalarFactor_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Haar.Unique (goal)
Goal:
G : Type u_1
A : Type u_2
inst : Group G
inst_1 : AddCommGroup A
inst_2 : DistribMulAction G A
inst_3 : MeasurableSpace A
inst_4 : TopologicalSpace A
inst_5 : BorelSpace A
inst_6 : IsTopologicalAddGroup A
inst_7 : LocallyCompactSpace A
inst_8 : ContinuousConstSMul G A
μ ν : Measure A
inst_9 : μ.IsAddHaarMeasure
inst_10 : ν.IsAddHaarMeasure
g : Gᵈᵐᵃ
rw : (g • μ).addHaarScalarFactor (g • ν) * (g • ν).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
rw₁ : μ.addHaarScalarFactor ν * (g • ν).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
rw₂ : (g • ν).addHaarScalarFactor μ * μ.addHaarScalarFactor ν = (g • ν).addHaarScalarFactor ν
⊢ (g • μ).addHaarScalarFactor μ = (g • ν).addHaarScalarFactor ν
have rw₃ : (g • ν).addHaarScalarFactor ν = (g • ν).addHaarScalarFactor ν
Tactic: rw [addHaarScalarFactor_eq_mul _ (g • ν), addHaarScalarFactor_domSMul,
    mul_comm, ← addHaarScalarFactor_eq_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (f ω))
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((fs i : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ) L (𝓝 (∫⁻ (ω : Ω), (↑(f ω) : ℝ≥0∞) ∂μ))
have refine_1 : ∀ᶠ (n : ι) in L, ∀ᵐ (a : Ω) ∂μ, (↑((fs n : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ≤ (fun (x : Ω) ↦ (↑c : ℝ≥0∞)) a
Tactic: refine tendsto_lintegral_filter_of_dominated_convergence (fun _ ↦ c)
    (Eventually.of_forall fun i ↦ (ENNReal.continuous_coe.comp (fs i).continuous).measurable) ?_
    (@lintegral_const_lt_top _ _ μ _ _ (@ENNReal.coe_ne_top c)).ne ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
f : Ω → ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (f ω))
refine_1 : ∀ᶠ (n : ι) in L, ∀ᵐ (a : Ω) ∂μ, (↑((fs n : (a : Ω) → ℝ≥0) a) : ℝ≥0∞) ≤ (fun (x : Ω) ↦ (↑c : ℝ≥0∞)) a
⊢ Tendsto (fun (i : ι) ↦ ∫⁻ (ω : Ω), (↑((fs i : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ) L (𝓝 (∫⁻ (ω : Ω), (↑(f ω) : ℝ≥0∞) ∂μ))
have refine_2 : ∀ᵐ (a : Ω) ∂μ, Tendsto (fun (n : ι) ↦ (↑((fs n : (a : Ω) → ℝ≥0) a) : ℝ≥0∞)) L (𝓝 (↑(f a) : ℝ≥0∞))
Tactic: refine tendsto_lintegral_filter_of_dominated_convergence (fun _ ↦ c)
    (Eventually.of_forall fun i ↦ (ENNReal.continuous_coe.comp (fs i).continuous).measurable) ?_
    (@lintegral_const_lt_top _ _ μ _ _ (@ENNReal.coe_ne_top c)).ne ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  ∀ᵐ (ω : Ω) ∂μ, Tendsto (β := ℝ≥0) (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ) L
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)
have h : (μ : (a : Set Ω) → ℝ≥0∞) E = ∫⁻ (ω : Ω), (↑(E.indicator (fun (x : Ω) ↦ 1) ω) : ℝ≥0∞) ∂μ
Tactic: convert! tendsto_lintegral_nn_filter_of_le_const μ fs_bdd fs_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  ∀ᵐ (ω : Ω) ∂μ, Tendsto (β := ℝ≥0) (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))
⊢ (μ : (a : Set Ω) → ℝ≥0∞) E = ∫⁻ (ω : Ω), (↑(E.indicator (fun (x : Ω) ↦ 1) ω) : ℝ≥0∞) ∂μ
have aux : ∀ (ω : Ω), E.indicator (fun (x : Ω) ↦ 1) ω = (↑(E.indicator (fun (x : Ω) ↦ 1) ω) : ℝ≥0∞)
Tactic: have aux : ∀ ω, indicator E (fun _ ↦ (1 : ℝ≥0∞)) ω = ↑(indicator E (fun _ ↦ (1 : ℝ≥0)) ω) :=
    fun ω ↦ by simp only [ENNReal.coe_indicator, ENNReal.coe_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
ι : Type u_2
L : Filter ι
inst_3 : L.IsCountablyGenerated
μ : Measure Ω
inst_4 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ι → Ω →ᵇ ℝ≥0
fs_bdd : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂μ, (fs i : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  ∀ᵐ (ω : Ω) ∂μ, Tendsto (β := ℝ≥0) (fun (i : ι) ↦ (fs i : (a : Ω) → ℝ≥0) ω) L (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))
aux : ∀ (ω : Ω), E.indicator (fun (x : Ω) ↦ 1) ω = (↑(E.indicator (fun (x : Ω) ↦ 1) ω) : ℝ≥0∞)
⊢ (μ : (a : Set Ω) → ℝ≥0∞) E = ∫⁻ (ω : Ω), (↑(E.indicator (fun (x : Ω) ↦ 1) ω) : ℝ≥0∞) ∂μ
have h : (μ : (a : Set Ω) → ℝ≥0∞) E = ∫⁻ (x : Ω) in E, 1 ∂μ
Tactic: simp_rw [← aux, lintegral_indicator E_mble]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_1
inst : TopologicalSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_3 : IsFiniteMeasure μ
c : ℝ≥0
E : Set Ω
E_mble : MeasurableSet E
fs : ℕ → Ω →ᵇ ℝ≥0
fs_bdd : ∀ (n : ℕ) (ω : Ω), (fs n : (a : Ω) → ℝ≥0) ω ≤ c
fs_lim :
  Tendsto (β := (ω : Ω) → ℝ≥0) (fun (n : ℕ) (ω : Ω) ↦ (fs n : (a : Ω) → ℝ≥0) ω) atTop (𝓝 (E.indicator fun (x : Ω) ↦ 1))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑((fs n : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) E) : Filter ℝ≥0∞)
have fs_lim' : ∀ (ω : Ω), Tendsto (β := ℝ≥0) (fun (n : ℕ) ↦ (fs n : (a : Ω) → ℝ≥0) ω) atTop (𝓝 (E.indicator (fun (x : Ω) ↦ 1) ω))
Tactic: have fs_lim' :
    ∀ ω, Tendsto (fun n : ℕ ↦ (fs n ω : ℝ≥0)) atTop (𝓝 (indicator E (fun _ ↦ (1 : ℝ≥0)) ω)) := by
    rw [tendsto_pi_nhds] at fs_lim
    exact fun ω ↦ fs_lim ω
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ)
    atTop (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
have apply : Tendsto (β := (ω : Ω) → ℝ≥0) (fun (n : ℕ) (ω : Ω) ↦ ((thickenedIndicator sorry F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) atTop
  (𝓝 (F.indicator fun (x : Ω) ↦ 1))
Tactic: apply measure_of_cont_bdd_of_tendsto_indicator μ F_closed.measurableSet
    (fun n ↦ thickenedIndicator (δs_pos n) F) fun n ω ↦ thickenedIndicator_le_one (δs_pos n) F ω
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
⊢ Tendsto (β := (ω : Ω) → ℝ≥0) (fun (n : ℕ) (ω : Ω) ↦ ((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) atTop
    (𝓝 (F.indicator fun (x : Ω) ↦ 1))
have key : Tendsto (β := (a : Ω) → ℝ≥0) (fun (n : ℕ) ↦ (⇑(thickenedIndicator sorry F) : (a : Ω) → ℝ≥0)) atTop
  (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator fun (x : Ω) ↦ 1))
Tactic: have key := thickenedIndicator_tendsto_indicator_closure δs_pos δs_lim F
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
key :
  Tendsto (β := (a : Ω) → ℝ≥0) (fun (n : ℕ) ↦ (⇑(thickenedIndicator ⋯ F) : (a : Ω) → ℝ≥0)) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator fun (x : Ω) ↦ 1))
⊢ Tendsto (β := (ω : Ω) → ℝ≥0) (fun (n : ℕ) (ω : Ω) ↦ ((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) atTop
    (𝓝 (F.indicator fun (x : Ω) ↦ 1))
have rwa : ∀
  (key :
    Tendsto (β := (a : Ω) → ℝ≥0) (fun (n : ℕ) ↦ (⇑(thickenedIndicator sorry F) : (a : Ω) → ℝ≥0)) atTop
      (𝓝 (F.indicator fun (x : Ω) ↦ 1))),
  Tendsto (β := (ω : Ω) → ℝ≥0) (fun (n : ℕ) (ω : Ω) ↦ ((thickenedIndicator sorry F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) atTop
    (𝓝 (F.indicator fun (x : Ω) ↦ 1))
Tactic: rwa [F_closed.closure_eq] at key
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
δ : ℝ
δ_pos : 0 < δ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ (↑(((thickenedIndicator δ_pos F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)) μ
have refine : ∀ (x : Ω), ‖(↑(((thickenedIndicator δ_pos F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) x) : ℝ)‖ ≤ 1
Tactic: refine .of_bound (by fun_prop) 1 (ae_of_all _ fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ) ∂μ) atTop
    (𝓝 (μ.real F))
have h : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑(((thickenedIndicator sorry F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ)
  atTop (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
Tactic: have h := tendsto_lintegral_thickenedIndicator_of_isClosed μ F_closed δs_pos δs_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ)
    atTop (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
n : ℕ
⊢ ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
    ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
have hfi : Integrable (ε := ℝ) (fun (x : Ω) ↦ (↑(((thickenedIndicator sorry F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) x) : ℝ)) μ
Tactic: rw [lintegral_coe_eq_integral]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ)
    atTop (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ) ∂μ) atTop
    (𝓝 (μ.real F))
have h_eq : ∀ (n : ℕ),
  ∫⁻ (ω : Ω), (↑(((thickenedIndicator sorry F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
    ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
Tactic: have h_eq (n : ℕ) : ∫⁻ ω, thickenedIndicator (δs_pos n) F ω ∂μ
      = ENNReal.ofReal (∫ ω, fs n ω ∂μ) := by
    rw [lintegral_coe_eq_integral]
    exact integrable_thickenedIndicator F (δs_pos _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ)
    atTop (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ) ∂μ) atTop
    (𝓝 (μ.real F))
have h₁ : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
  (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
Tactic: simp_rw [h_eq] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
⊢ Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂μ) fun (n : ℕ) ↦
    (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal
have h₁ : ∀ (n : ℕ), ∫ (ω : Ω), fs n ω ∂μ = (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal
Tactic: ext n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
n : ℕ
⊢ ∫ (ω : Ω), fs n ω ∂μ = (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal
have h₁ : LE.le (α := ℝ) 0 (∫ (ω : Ω), fs n ω ∂μ)
Tactic: rw [ENNReal.toReal_ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ) ∂μ) atTop
    (𝓝 (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) F)))
have h_eq' : Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂μ) fun (n : ℕ) ↦ (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal
Tactic: have h_eq' : (fun n ↦ ∫ ω, fs n ω ∂μ) = fun n ↦ (ENNReal.ofReal (∫ ω, fs n ω ∂μ)).toReal := by
    ext n
    rw [ENNReal.toReal_ofReal]
    exact integral_nonneg fun x ↦ by simp [fs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst : PseudoEMetricSpace Ω
inst_1 : OpensMeasurableSpace Ω
μ : Measure Ω
inst_2 : IsFiniteMeasure μ
F : Set Ω
F_closed : IsClosed[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F
δs : ℕ → ℝ
δs_pos : ∀ (n : ℕ), 0 < δs n
δs_lim : Tendsto δs atTop (𝓝 0)
fs : ℕ → Ω → ℝ := fun (n : ℕ) (ω : Ω) ↦ (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ)
h_eq :
  ∀ (n : ℕ),
    ∫⁻ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ≥0∞) ∂μ =
      ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)
h :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
h_eq' :
  Eq (α := (n : ℕ) → ℝ) (fun (n : ℕ) ↦ ∫ (ω : Ω), fs n ω ∂μ) fun (n : ℕ) ↦
    (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal
⊢ Tendsto (fun (n : ℕ) ↦ ∫ (ω : Ω), (↑(((thickenedIndicator ⋯ F : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) ω) : ℝ) ∂μ) atTop
    (𝓝 (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) F)))
have rwa : Tendsto (fun (n : ℕ) ↦ (ENNReal.ofReal (∫ (ω : Ω), fs n ω ∂μ)).toReal) atTop
  (𝓝 (ENNReal.toReal ((μ : (a : Set Ω) → ℝ≥0∞) F)))
Tactic: rwa [h_eq', ENNReal.tendsto_toReal_iff (by simp) (by finiteness)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
n : ℕ
x : X
⊢ LE.le (α := (fun (x : X) ↦ ℝ≥0) x) (F.indicator (fun (x : X) ↦ 1) x : ℝ≥0)
    ((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x : ℝ≥0)
have pos : ∀ (hxF : x ∈ F),
  LE.le (α := (fun (x : X) ↦ ℝ≥0) x) (F.indicator (fun (x : X) ↦ 1) x : ℝ≥0)
    ((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x : ℝ≥0)
Tactic: by_cases hxF : x ∈ F
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
n : ℕ
x : X
pos :
  ∀ (hxF : x ∈ F),
    LE.le (α := (fun (x : X) ↦ ℝ≥0) x) (F.indicator (fun (x : X) ↦ 1) x : ℝ≥0)
      ((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x : ℝ≥0)
⊢ LE.le (α := (fun (x : X) ↦ ℝ≥0) x) (F.indicator (fun (x : X) ↦ 1) x : ℝ≥0)
    ((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x : ℝ≥0)
have neg : ∀ (hxF : x ∉ F),
  LE.le (α := (fun (x : X) ↦ ℝ≥0) x) (F.indicator (fun (x : X) ↦ 1) x : ℝ≥0)
    ((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x : ℝ≥0)
Tactic: by_cases hxF : x ∈ F
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ (μ : (a : Set X) → ℝ≥0∞) F ≤ ∫⁻ (x : X), (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have h : (μ : (a : Set X) → ℝ≥0∞) F = ∫⁻ (x : X), F.indicator (fun (x : X) ↦ 1) x ∂μ
Tactic: convert_to ∫⁻ x, (F.indicator (fun _ ↦ (1 : ℝ≥0∞))) x ∂μ ≤ ∫⁻ x, hF.apprSeq n x ∂μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
μ : Measure X
n : ℕ
h : (μ : (a : Set X) → ℝ≥0∞) F = ∫⁻ (x : X), F.indicator (fun (x : X) ↦ 1) x ∂μ
⊢ (μ : (a : Set X) → ℝ≥0∞) F ≤ ∫⁻ (x : X), (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have convert_to : ∫⁻ (x : X), F.indicator (fun (x : X) ↦ 1) x ∂μ ≤ ∫⁻ (x : X), (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ
Tactic: convert_to ∫⁻ x, (F.indicator (fun _ ↦ (1 : ℝ≥0∞))) x ∂μ ≤ ∫⁻ x, hF.apprSeq n x ∂μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : HasOuterApproxClosed X
F : Set X
hF : IsClosed[inst] F
inst_2 : MeasurableSpace X
inst_3 : OpensMeasurableSpace X
μ : Measure X
n : ℕ
⊢ (μ : (a : Set X) → ℝ≥0∞) F = ∫⁻ (x : X), F.indicator (fun (x : X) ↦ 1) x ∂μ
have h : (μ : (a : Set X) → ℝ≥0∞) F = ∫⁻ (a : X) in F, 1 ∂μ
Tactic: rw [lintegral_indicator hF.measurableSet]