awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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 ∈ 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))
⊢ ∃ (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:
use fun n ↦ thickenedIndicator (δ := (1 : ℝ) / (n + 1)) Nat.one_div_pos_of_nat F

Premises used: thickenedIndicator
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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))

Tactic:
⟨?_, ⟨?_, ?_⟩⟩

Premises used: And.intro
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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)
h₂ :
  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))
⊢ (∀ (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))

Tactic:
refine ⟨?_, ⟨?_, ?_⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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)

Tactic:
fun n x ↦ thickenedIndicator_le_one Nat.one_div_pos_of_nat F x

Premises used: thickenedIndicator_le_one, Nat.one_div_pos_of_nat
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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)

Tactic:
exact fun n x ↦ thickenedIndicator_le_one Nat.one_div_pos_of_nat F x

Premises used: thickenedIndicator_le_one, Nat.one_div_pos_of_nat
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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 ∈ 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)

Tactic:
fun n x hxF ↦ one_le_thickenedIndicator_apply X Nat.one_div_pos_of_nat hxF

Premises used: Nat.one_div_pos_of_nat, one_le_thickenedIndicator_apply
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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 ∈ 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)

Tactic:
exact fun n x hxF ↦ one_le_thickenedIndicator_apply X Nat.one_div_pos_of_nat hxF

Premises used: Nat.one_div_pos_of_nat, one_le_thickenedIndicator_apply
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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 (β := (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))

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
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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))
h :
  ∀
    (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))
⊢ 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))

Tactic:
rw [tendsto_pi_nhds] at *

Premises used: tendsto_pi_nhds
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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
h :
  Tendsto (β := ℝ≥0)
    (fun (i : ℕ) ↦
      (((fun (n : ℕ) ↦ (thickenedIndicator (δ := 1 / HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ⋯ F : X →ᵇ ℝ≥0)) i : X →ᵇ ℝ≥0) :
          (a : X) → ℝ≥0)
        x)
    atTop (𝓝 ((closure[inst] F).indicator (fun (x : X) ↦ 1) 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))

Tactic:
nth_rw 2 [← IsClosed.closure_eq hF]

Premises used: IsClosed.closure_eq
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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 (𝓝 ((closure[inst] F).indicator (fun (x : X) ↦ 1) x))

Tactic:
key x
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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 (𝓝 ((closure[inst] F).indicator (fun (x : X) ↦ 1) x))

Tactic:
exact key x
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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
measure_univ_lt_top : LT.lt (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure ν

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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
⊢ ∫⁻ (x : Ω), (↑(((1 : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂μ =
    ∫⁻ (x : Ω), (↑(((1 : Ω →ᵇ ℝ≥0) : (a : Ω) → ℝ≥0) x) : ℝ≥0∞) ∂ν

Tactic:
have whole := h 1
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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∞) ∂ν
⊢ 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

Premises used: MeasureTheory.lintegral_const, BoundedContinuousFunction.coe_one, Pi.one_apply, ENNReal.coe_one, one_mul
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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 : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [← whole]
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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 ν

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]
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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 ν
⊢ 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 μ
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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∞)
⊢ 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 ν
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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∞)
⊢ 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_μ
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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∞)

Tactic:
tendsto_nhds_unique obs_μ obs_ν

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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∞)

Tactic:
exact tendsto_nhds_unique obs_μ obs_ν

Premises used: tendsto_nhds_unique
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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∞) ∂ν
⊢ ∀ {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
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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∞)
apply : inst = MeasurableSpace.generateFrom {s : Set Ω | IsClosed[inst_1] s}
⊢ μ = ν

Tactic:
apply ext_of_generate_finite _ ?_ isPiSystem_isClosed

Premises used: MeasureTheory.ext_of_generate_finite, isPiSystem_isClosed
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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∞)
⊢ ∀ (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:
fun F F_closed ↦ key F_closed
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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∞)
⊢ ∀ (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:
exact fun F F_closed ↦ key F_closed
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
key isClosed_univ

Premises used: isClosed_univ
-- Module: Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
exact key isClosed_univ

Premises used: isClosed_univ