awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℕ
⊢ ∫⁻ (x : X), F.indicator (fun (x : X) ↦ 1) x ∂μ ≤ ∫⁻ (x : X), (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) x) : ℝ≥0∞) ∂μ
have hfg : LE.le (α := X → ℝ≥0∞) (F.indicator fun (x : X) ↦ 1) fun (a : X) ↦ (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) a) : ℝ≥0∞)
Tactic: apply lintegral_mono
-- 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 : ℕ
x : X
⊢ LE.le (α := (fun (a : X) ↦ ℝ≥0∞) x) (F.indicator (fun (x : X) ↦ 1) x)
    ((fun (a : X) ↦ (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) a) : ℝ≥0∞)) x)
have pos : ∀ (hxF : x ∈ F),
  LE.le (α := (fun (a : X) ↦ ℝ≥0∞) x) (F.indicator (fun (x : X) ↦ 1) x)
    ((fun (a : X) ↦ (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) a) : ℝ≥0∞)) x)
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 : ℕ
x : X
pos :
  ∀ (hxF : x ∈ F),
    LE.le (α := (fun (a : X) ↦ ℝ≥0∞) x) (F.indicator (fun (x : X) ↦ 1) x)
      ((fun (a : X) ↦ (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) a) : ℝ≥0∞)) x)
⊢ LE.le (α := (fun (a : X) ↦ ℝ≥0∞) x) (F.indicator (fun (x : X) ↦ 1) x)
    ((fun (a : X) ↦ (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) a) : ℝ≥0∞)) x)
have neg : ∀ (hxF : x ∉ F),
  LE.le (α := (fun (a : X) ↦ ℝ≥0∞) x) (F.indicator (fun (x : X) ↦ 1) x)
    ((fun (a : X) ↦ (↑((hF.apprSeq (F := F) n : (a : X) → ℝ≥0) a) : ℝ≥0∞)) x)
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 : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
⊢ HasOuterApproxClosed X
have refine : ∀ (F : Set X) (hF : IsClosed[inst] F),
  ∃ (fseq : ℕ → X →ᵇ ℝ≥0),
    (∀ (n : ℕ) (x : X), LE.le (α := ℝ≥0) ((fseq n : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)) ∧
      (∀ (n : ℕ), ∀ x ∈ F, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((fseq n : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
        Tendsto (β := (x : X) → ℝ≥0) (fun (n : ℕ) (x : X) ↦ (fseq n : (a : X) → ℝ≥0) x) atTop
          (𝓝 (F.indicator fun (x : X) ↦ 1))
Tactic: refine ⟨fun F hF ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst] F
⊢ ∃ (fseq : ℕ → X →ᵇ ℝ≥0),
    (∀ (n : ℕ) (x : X), LE.le (α := ℝ≥0) ((fseq n : (a : X) → ℝ≥0) x : ℝ≥0) (1 : ℝ≥0)) ∧
      (∀ (n : ℕ), ∀ x ∈ F, LE.le (α := ℝ≥0) (1 : ℝ≥0) ((fseq n : (a : X) → ℝ≥0) x : ℝ≥0)) ∧
        Tendsto (β := (x : X) → ℝ≥0) (fun (n : ℕ) (x : X) ↦ (fseq n : (a : X) → ℝ≥0) x) atTop
          (𝓝 (F.indicator fun (x : X) ↦ 1))
have h : (∀ (n : ℕ) (x : X),
    LE.le (α := ℝ≥0)
      ((((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) sorry F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
            (a : X) → ℝ≥0)
          x :
        ℝ≥0)
      (1 : ℝ≥0)) ∧
  (∀ (n : ℕ),
      ∀ x ∈ F,
        LE.le (α := ℝ≥0) (1 : ℝ≥0)
          ((((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) sorry F : X →ᵇ ℝ≥0)) n :
                  X →ᵇ ℝ≥0) :
                (a : X) → ℝ≥0)
              x :
            ℝ≥0)) ∧
    Tendsto (β := (x : X) → ℝ≥0)
      (fun (n : ℕ) (x : X) ↦
        (((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) sorry F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
            (a : X) → ℝ≥0)
          x)
      atTop (𝓝 (F.indicator fun (x : X) ↦ 1))
Tactic: use fun n ↦ thickenedIndicator (δ := (1 : ℝ) / (n + 1)) Nat.one_div_pos_of_nat F
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst] F
⊢ (∀ (n : ℕ) (x : X),
      LE.le (α := ℝ≥0)
        ((((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
              (a : X) → ℝ≥0)
            x :
          ℝ≥0)
        (1 : ℝ≥0)) ∧
    (∀ (n : ℕ),
        ∀ x ∈ F,
          LE.le (α := ℝ≥0) (1 : ℝ≥0)
            ((((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n :
                    X →ᵇ ℝ≥0) :
                  (a : X) → ℝ≥0)
                x :
              ℝ≥0)) ∧
      Tendsto (β := (x : X) → ℝ≥0)
        (fun (n : ℕ) (x : X) ↦
          (((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
              (a : X) → ℝ≥0)
            x)
        atTop (𝓝 (F.indicator fun (x : X) ↦ 1))
have h : ∀ (n : ℕ) (x : X),
  LE.le (α := ℝ≥0)
    ((((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) sorry F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
          (a : X) → ℝ≥0)
        x :
      ℝ≥0)
    (1 : ℝ≥0)
Tactic: refine ⟨?_, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst] F
h :
  ∀ (n : ℕ) (x : X),
    LE.le (α := ℝ≥0)
      ((((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
            (a : X) → ℝ≥0)
          x :
        ℝ≥0)
      (1 : ℝ≥0)
⊢ (∀ (n : ℕ) (x : X),
      LE.le (α := ℝ≥0)
        ((((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
              (a : X) → ℝ≥0)
            x :
          ℝ≥0)
        (1 : ℝ≥0)) ∧
    (∀ (n : ℕ),
        ∀ x ∈ F,
          LE.le (α := ℝ≥0) (1 : ℝ≥0)
            ((((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n :
                    X →ᵇ ℝ≥0) :
                  (a : X) → ℝ≥0)
                x :
              ℝ≥0)) ∧
      Tendsto (β := (x : X) → ℝ≥0)
        (fun (n : ℕ) (x : X) ↦
          (((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
              (a : X) → ℝ≥0)
            x)
        atTop (𝓝 (F.indicator fun (x : X) ↦ 1))
have h₁ : ∀ (n : ℕ),
  ∀ x ∈ F,
    LE.le (α := ℝ≥0) (1 : ℝ≥0)
      ((((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) sorry F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
            (a : X) → ℝ≥0)
          x :
        ℝ≥0)
Tactic: refine ⟨?_, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst] F
h :
  ∀ (n : ℕ) (x : X),
    LE.le (α := ℝ≥0)
      ((((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
            (a : X) → ℝ≥0)
          x :
        ℝ≥0)
      (1 : ℝ≥0)
h₁ :
  ∀ (n : ℕ),
    ∀ x ∈ F,
      LE.le (α := ℝ≥0) (1 : ℝ≥0)
        ((((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
              (a : X) → ℝ≥0)
            x :
          ℝ≥0)
⊢ (∀ (n : ℕ) (x : X),
      LE.le (α := ℝ≥0)
        ((((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
              (a : X) → ℝ≥0)
            x :
          ℝ≥0)
        (1 : ℝ≥0)) ∧
    (∀ (n : ℕ),
        ∀ x ∈ F,
          LE.le (α := ℝ≥0) (1 : ℝ≥0)
            ((((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n :
                    X →ᵇ ℝ≥0) :
                  (a : X) → ℝ≥0)
                x :
              ℝ≥0)) ∧
      Tendsto (β := (x : X) → ℝ≥0)
        (fun (n : ℕ) (x : X) ↦
          (((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
              (a : X) → ℝ≥0)
            x)
        atTop (𝓝 (F.indicator fun (x : X) ↦ 1))
have h₂ : Tendsto (β := (x : X) → ℝ≥0)
  (fun (n : ℕ) (x : X) ↦
    (((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) sorry F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
        (a : X) → ℝ≥0)
      x)
  atTop (𝓝 (F.indicator fun (x : X) ↦ 1))
Tactic: refine ⟨?_, ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst] F
⊢ Tendsto (β := (x : X) → ℝ≥0)
    (fun (n : ℕ) (x : X) ↦
      (((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
          (a : X) → ℝ≥0)
        x)
    atTop (𝓝 (F.indicator fun (x : X) ↦ 1))
have key : Tendsto (β := (a : X) → ℝ≥0)
  (fun (n : ℕ) ↦ (⇑(thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) sorry F) : (a : X) → ℝ≥0)) atTop
  (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator fun (x : X) ↦ 1))
Tactic: have key := thickenedIndicator_tendsto_indicator_closure
              (δseq := fun (n : ℕ) ↦ (1 : ℝ) / (n + 1))
              (fun _ ↦ Nat.one_div_pos_of_nat) tendsto_one_div_add_atTop_nhds_zero_nat F
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst] F
key :
  Tendsto (β := (a : X) → ℝ≥0)
    (fun (n : ℕ) ↦ (⇑(thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F) : (a : X) → ℝ≥0)) atTop
    (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator fun (x : X) ↦ 1))
⊢ Tendsto (β := (x : X) → ℝ≥0)
    (fun (n : ℕ) (x : X) ↦
      (((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) n : X →ᵇ ℝ≥0) :
          (a : X) → ℝ≥0)
        x)
    atTop (𝓝 (F.indicator fun (x : X) ↦ 1))
have h : ∀
  (key :
    ∀ (x : X),
      Tendsto (β := ℝ≥0)
        (fun (i : ℕ) ↦ ((thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) sorry F : X →ᵇ ℝ≥0) : (a : X) → ℝ≥0) x)
        atTop (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator (fun (x : X) ↦ 1) x)))
  (x : X),
  Tendsto (β := ℝ≥0)
    (fun (i : ℕ) ↦
      (((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) sorry F : X →ᵇ ℝ≥0)) i : X →ᵇ ℝ≥0) :
          (a : X) → ℝ≥0)
        x)
    atTop (𝓝 (F.indicator (fun (x : X) ↦ 1) x))
Tactic: rw [tendsto_pi_nhds] at *
Cleared hypotheses: key
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace.PseudoMetrizableSpace X
this : PseudoMetricSpace X := TopologicalSpace.pseudoMetrizableSpacePseudoMetric X
F : Set X
hF : IsClosed[inst] F
key :
  ∀ (x : X),
    Tendsto (β := ℝ≥0)
      (fun (i : ℕ) ↦ ((thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑i : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0) : (a : X) → ℝ≥0) x)
      atTop (𝓝 ((closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] F).indicator (fun (x : X) ↦ 1) x))
x : X
⊢ Tendsto (β := ℝ≥0)
    (fun (i : ℕ) ↦
      (((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) i : X →ᵇ ℝ≥0) :
          (a : X) → ℝ≥0)
        x)
    atTop (𝓝 (F.indicator (fun (x : X) ↦ 1) x))
have h : Tendsto (β := ℝ≥0)
  (fun (i : ℕ) ↦
    (((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) sorry F : X →ᵇ ℝ≥0)) i : X →ᵇ ℝ≥0) :
        (a : X) → ℝ≥0)
      x)
  atTop (𝓝 ((closure[inst] F).indicator (fun (x : X) ↦ 1) x))
Tactic: nth_rw 2 [← IsClosed.closure_eq hF]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
F : Set Ω
F_closed : IsClosed[inst_1] F
⊢ IsFiniteMeasure ν
have measure_univ_lt_top : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
F : Set Ω
F_closed : IsClosed[inst_1] F
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have whole : ∫⁻ (x : Ω), (↑(((1 : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ =
  ∫⁻ (x : Ω), (↑(((1 : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
Tactic: have whole := h 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
F : Set Ω
F_closed : IsClosed[inst_1] F
whole :
  ∫⁻ (x : Ω), (↑(((1 : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ =
    ∫⁻ (x : Ω), (↑(((1 : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have whole₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: simp only [BoundedContinuousFunction.coe_one, Pi.one_apply, ENNReal.coe_one, lintegral_const,
      one_mul] at whole
Cleared hypotheses: whole
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
F : Set Ω
F_closed : IsClosed[inst_1] F
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have ν_finite : IsFiniteMeasure ν
Tactic: have ν_finite : IsFiniteMeasure ν := by
    constructor
    have whole := h 1
    simp only [BoundedContinuousFunction.coe_one, Pi.one_apply, ENNReal.coe_one, lintegral_const,
      one_mul] at whole
    simp [← whole]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
F : Set Ω
F_closed : IsClosed[inst_1] F
ν_finite : IsFiniteMeasure ν
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have obs_μ : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : Ω), (↑((F_closed.apprSeq (F := F) n : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ) atTop
  (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
Tactic: have obs_μ := HasOuterApproxClosed.tendsto_lintegral_apprSeq F_closed μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
F : Set Ω
F_closed : IsClosed[inst_1] F
ν_finite : IsFiniteMeasure ν
obs_μ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : Ω), (↑((F_closed.apprSeq (F := F) n : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have obs_ν : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : Ω), (↑((F_closed.apprSeq (F := F) n : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν) atTop
  (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
Tactic: have obs_ν := HasOuterApproxClosed.tendsto_lintegral_apprSeq F_closed ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : OpensMeasurableSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
F : Set Ω
F_closed : IsClosed[inst_1] F
ν_finite : IsFiniteMeasure ν
obs_μ :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : Ω), (↑((F_closed.apprSeq (F := F) n : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ) atTop
    (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
obs_ν :
  Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : Ω), (↑((F_closed.apprSeq (F := F) n : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν) atTop
    (𝓝 ((ν : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
have obs_μ₁ : Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∫⁻ (x : Ω), (↑((F_closed.apprSeq (F := F) n : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν) atTop
  (𝓝 ((μ : (a : Set Ω) → ℝ≥0∞) F) : Filter ℝ≥0∞)
Tactic: simp_rw [h] at obs_μ
Cleared hypotheses: obs_μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
⊢ μ = ν
have key : ∀ {F : Set Ω} (F_closed : IsClosed[inst_1] F),
  Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
Tactic: have key := @measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure Ω _ _ _ _ μ ν _ h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
key :
  ∀ {F : Set Ω} (F_closed : IsClosed[inst_1] F),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
⊢ μ = ν
have hμν : ∀ (s : Set Ω),
  Membership.mem (γ := Set (Set Ω)) {s : Set Ω | IsClosed[inst_1] s} s →
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply ext_of_generate_finite _ ?_ isPiSystem_isClosed
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
key :
  ∀ {F : Set Ω} (F_closed : IsClosed[inst_1] F),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
hμν :
  ∀ (s : Set Ω),
    Membership.mem (γ := Set (Set Ω)) {s : Set Ω | IsClosed[inst_1] s} s →
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν
have h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
Tactic: apply ext_of_generate_finite _ ?_ isPiSystem_isClosed
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
key :
  ∀ {F : Set Ω} (F_closed : IsClosed[inst_1] F),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
hμν :
  ∀ (s : Set Ω),
    Membership.mem (γ := Set (Set Ω)) {s : Set Ω | IsClosed[inst_1] s} s →
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞)
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ μ = ν
have apply : inst = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[inst_1] s}
Tactic: apply ext_of_generate_finite _ ?_ isPiSystem_isClosed
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
key :
  ∀ {F : Set Ω} (F_closed : IsClosed[inst_1] F),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
⊢ inst = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[inst_1] s}
have rw : borel Ω = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[inst_1] s}
Tactic: rw [BorelSpace.measurable_eq (α := Ω), borel_eq_generateFrom_isClosed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
h :
  ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
key :
  ∀ {F : Set Ω} (F_closed : IsClosed[inst_1] F),
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) F : ℝ≥0∞)
rw : borel Ω = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[inst_1] s}
⊢ inst = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[inst_1] s}
have rw₁ : Eq.{u_1 + 1} (α := MeasurableSpace Ω) (MeasurableSpace.generateFrom {s : Set Ω | IsClosed[inst_1] s})
  (MeasurableSpace.generateFrom {s : Set Ω | IsClosed[inst_1] s})
Tactic: rw [BorelSpace.measurable_eq (α := Ω), borel_eq_generateFrom_isClosed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.HasOuterApproxClosed (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : TopologicalSpace Ω
inst_2 : HasOuterApproxClosed Ω
inst_3 : BorelSpace Ω
μ ν : Measure Ω
inst_4 : IsFiniteMeasure μ
inst_5 : IsFiniteMeasure ν
h : ∀ (f : Ω →ᵇ ℝ), Eq (α := ℝ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂μ) (∫ (x : Ω), (f : (a : Ω) → ℝ) x ∂ν)
⊢ μ = ν
have h₁ : ∀ (f : Ω →ᵇ ℝ≥0), ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ = ∫⁻ (x : Ω), (↑((f : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν
Tactic: apply ext_of_forall_lintegral_eq_of_IsFiniteMeasure