awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
apply :
  ∀ (g : E →ᵇ ℝ),
    Tendsto (β := ℝ) (fun (i : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑(id i) : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μlim' : Measure E)))
⊢ Tendsto id (↑f : Filter (FiniteMeasure E)) (𝓝 μlim')

Tactic:
apply FiniteMeasure.tendsto_of_forall_integral_tendsto (fun g ↦ ?_)

Premises used: MeasureTheory.FiniteMeasure.tendsto_of_forall_integral_tendsto
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
g : E →ᵇ ℝ
g' : E →C_c ℝ := { toFun := (⇑g : (a : E) → ℝ), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
⊢ Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g' : (a : E) → ℝ) x ∂(↑μ : Measure E))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g'))

Tactic:
hΛ g'
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
g : E →ᵇ ℝ
g' : E →C_c ℝ := { toFun := (⇑g : (a : E) → ℝ), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
h : ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μlim' : Measure E) = Λ g'
⊢ Tendsto (β := ℝ) (fun (i : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑(id i) : Measure E))
    (↑f : Filter (FiniteMeasure E)) (𝓝 (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μlim' : Measure E)))

Tactic:
convert! hΛ g'
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
g : E →ᵇ ℝ
g' : E →C_c ℝ := { toFun := (⇑g : (a : E) → ℝ), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
h : ∫ (x : E), (g' : (a : E) → ℝ) x ∂(↑μlim' : Measure E) = Λ g'
⊢ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μlim' : Measure E) = Λ g'

Tactic:
change ∫ (x : E), g' x ∂μlim' = Λ g'
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
g : E →ᵇ ℝ
g' : E →C_c ℝ := { toFun := (⇑g : (a : E) → ℝ), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
h : (Λ' : (a : E →C_c ℝ) → ℝ) g' = Λ g'
⊢ ∫ (x : E), (g' : (a : E) → ℝ) x ∂(↑μlim' : Measure E) = Λ g'

Tactic:
simp only [FiniteMeasure.toMeasure_mk, RealRMK.integral_rieszMeasure, μlim', μlim]

Premises used: RealRMK.integral_rieszMeasure, MeasureTheory.FiniteMeasure.toMeasure_mk
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
f : Ultrafilter (FiniteMeasure E)
hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f
Λ : (g : E →C_c ℝ) → ℝ
h₀Λ :
  ∀ (g : E →C_c ℝ), Λ g ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)
hΛ :
  ∀ (g : E →C_c ℝ),
    Tendsto (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
      (↑f : Filter (FiniteMeasure E)) (𝓝 (Λ g))
Λ' : (E →C_c ℝ) →ₚ[ℝ] ℝ := { toFun := Λ, map_add' := ⋯, map_smul' := ⋯, monotone' := ⋯ }
μlim : Measure E := RealRMK.rieszMeasure Λ'
μlim_le : (μlim : (a : Set E) → ℝ≥0∞) univ ≤ ENNReal.ofReal (↑C : ℝ)
μlim' : FiniteMeasure E := Subtype.mk (p := fun (μ : Measure E) ↦ IsFiniteMeasure μ) μlim ⋯
g : E →ᵇ ℝ
g' : E →C_c ℝ := { toFun := (⇑g : (a : E) → ℝ), continuous_toFun := ⋯, hasCompactSupport' := ⋯ }
⊢ (Λ' : (a : E →C_c ℝ) → ℝ) g' = Λ g'

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
⊢ Eq.{u_1 + 1} (α := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass = C}
    ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
⊢ Eq.{u_1 + 1} (α := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass = C}
    ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})

Tactic:
have : {μ : FiniteMeasure E | μ.mass = C} = {μ | μ.mass ≤ C} ∩ {μ | μ.mass = C} := by grind
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
this :
  Eq.{u_1 + 1} (α := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass = C}
    ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})
rw : IsCompact.{u_1} (X := FiniteMeasure E) ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})
⊢ IsCompact.{u_1} (X := FiniteMeasure E) {μ : FiniteMeasure E | μ.mass = C}

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
this :
  Eq.{u_1 + 1} (α := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass = C}
    ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})
apply : IsClosed[instTopologicalSpace] {μ : FiniteMeasure E | μ.mass = C}
⊢ IsCompact.{u_1} (X := FiniteMeasure E) ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})

Tactic:
apply IsCompact.inter_right (isCompact_setOf_finiteMeasure_le_of_compactSpace E C)

Premises used: isCompact_setOf_finiteMeasure_le_of_compactSpace, IsCompact.inter_right
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
this :
  Eq.{u_1 + 1} (α := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass = C}
    ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})
⊢ Continuous[instTopologicalSpace, _] mass

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
this :
  Eq.{u_1 + 1} (α := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass = C}
    ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})
⊢ Continuous[instTopologicalSpace, _] fun (μ : FiniteMeasure E) ↦ C

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
C : ℝ≥0
this :
  Eq.{u_1 + 1} (α := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass = C}
    ({μ : FiniteMeasure E | μ.mass ≤ C} ∩ {μ : FiniteMeasure E | μ.mass = C})
⊢ IsClosed[instTopologicalSpace] {μ : FiniteMeasure E | μ.mass = C}

Tactic:
exact isClosed_eq (by fun_prop) (by fun_prop)

Premises used: isClosed_eq
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
isCompact_univ : IsCompact.{u_1} (X := ProbabilityMeasure E) univ
⊢ CompactSpace.{u_1} (ProbabilityMeasure E)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
isCompact_univ : IsCompact.{u_1} (X := FiniteMeasure E) (ProbabilityMeasure.toFiniteMeasure '' univ)
⊢ IsCompact.{u_1} (X := ProbabilityMeasure E) univ

Tactic:
apply (ProbabilityMeasure.toFiniteMeasure_isEmbedding E).isCompact_iff.2

Premises used: Iff.mpr, Topology.IsEmbedding.isCompact_iff, MeasureTheory.ProbabilityMeasure.toFiniteMeasure_isEmbedding
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
inst_4 : CompactSpace E
⊢ IsCompact.{u_1} (X := FiniteMeasure E) (ProbabilityMeasure.toFiniteMeasure '' univ)

Tactic:
simpa using isCompact_setOf_finiteMeasure_eq_of_compactSpace E 1

Premises used: isCompact_setOf_finiteMeasure_eq_of_compactSpace, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
⊢ IsClosedEmbedding f

Tactic:
have hf : IsClosedEmbedding f := IsClosedEmbedding.subtypeVal hK.isClosed
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
⊢ range f = K

Tactic:
have rf : range f = K := Subtype.range_val
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
h₁ : {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} ⊆ F '' T
h₂ : F '' T ⊆ {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)}
⊢ {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} = F '' T

Tactic:
apply Subset.antisymm

Premises used: Set.Subset.antisymm
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
⊢ ∃ x ∈ T, F x = μ

Tactic:
⟨μ.comap f, (FiniteMeasure.mass_comap_le _ _).trans hμ.1, ?_⟩

Premises used: MeasureTheory.FiniteMeasure.comap, MeasureTheory.FiniteMeasure.mass_comap_le, And.left, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
h₁ : F (FiniteMeasure.comap f μ) = μ
⊢ ∃ x ∈ T, F x = μ

Tactic:
refine ⟨μ.comap f, (FiniteMeasure.mass_comap_le _ _).trans hμ.1, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
h₁ :
  ∀ (s : Set E) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) (((↑(F (FiniteMeasure.comap f μ)) : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
      (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ F (FiniteMeasure.comap f μ) = μ

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
s : Set E
hs : MeasurableSet s
h₁ :
  Eq (α := ℝ≥0∞)
    (((Measure.map f (↑(FiniteMeasure.comap f μ) : Measure (↑K : Type u_1)) : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((↑(F (FiniteMeasure.comap f μ)) : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [toMeasure_map, F]

Premises used: MeasureTheory.FiniteMeasure.toMeasure_map
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
s : Set E
hs : MeasurableSet s
h₁ :
  Eq (α := ℝ≥0∞)
    ((((↑(FiniteMeasure.comap f μ) : Measure (↑K : Type u_1)) : Measure (↑K : Type u_1)) :
          (a : Set { x : E // x ∈ K }) → ℝ≥0∞)
        (Subtype.val (p := fun (x : E) ↦ x ∈ K) ⁻¹' s) :
      ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map f (↑(FiniteMeasure.comap f μ) : Measure (↑K : Type u_1)) : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.map_apply measurable_subtype_coe hs]

Premises used: measurable_subtype_coe, MeasureTheory.Measure.map_apply
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
s : Set E
hs : MeasurableSet s
h₁ :
  Eq (α := ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞)
        (s ∩ range (ι := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K))) :
      ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)
h₂ : ∀ (s : Set { x : E // x ∈ K }), MeasurableSet s → MeasurableSet (Subtype.val (p := fun (x : E) ↦ x ∈ K) '' s)
h₃ : MeasurableSet (α := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K) ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.comap f (↑μ : Measure E) : Measure (↑K : Type u_1)) : (a : Set { x : E // x ∈ K }) → ℝ≥0∞)
        (Subtype.val (p := fun (x : E) ↦ x ∈ K) ⁻¹' s) :
      ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.comap_apply _ (Subtype.val_injective), image_preimage_eq_inter_range]

Premises used: Subtype.val_injective, MeasureTheory.Measure.comap_apply, Set.image_preimage_eq_inter_range
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
s : Set E
hs : MeasurableSet s
h₁ :
  ∀ᵐ (x : E) ∂(↑μ : Measure E),
    Membership.mem (γ := Set E) (range (ι := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K))) x
⊢ Eq (α := ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞)
        (s ∩ range (ι := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K))) :
      ℝ≥0∞)
    (((↑μ : Measure E) : (a : Set E) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [← Measure.restrict_apply hs, Measure.restrict_eq_self_of_ae_mem]

Premises used: MeasureTheory.Measure.restrict_apply, MeasureTheory.Measure.restrict_eq_self_of_ae_mem
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
s : Set E
hs : MeasurableSet s
h₁ : Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)
⊢ ∀ᵐ (x : E) ∂(↑μ : Measure E),
    Membership.mem (γ := Set E) (range (ι := { x : E // x ∈ K }) (Subtype.val (p := fun (x : E) ↦ x ∈ K))) x

Tactic:
apply (null_iff_toMeasure_null (↑μ) (range f)ᶜ).mp

Premises used: Compl.compl, Iff.mp, Set.range, MeasureTheory.FiniteMeasure.null_iff_toMeasure_null
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
s : Set E
hs : MeasurableSet s
h₁ : Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)
⊢ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) (range f)ᶜ : ℝ≥0) (0 : ℝ≥0)

Tactic:
rw [rf]
-- Module: Mathlib.MeasureTheory.Measure.Prokhorov
Goal:
E : Type u_1
inst : MeasurableSpace E
inst_1 : TopologicalSpace E
inst_2 : T2Space E
inst_3 : BorelSpace E
C : ℝ≥0
K : Set E
hK : IsCompact K
f : (↑K : Type u_1) → E := Subtype.val (p := fun (x : E) ↦ x ∈ K)
hf : IsClosedEmbedding f
rf : range f = K
F : FiniteMeasure (↑K : Type u_1) → FiniteMeasure E := fun (μ : FiniteMeasure (↑K : Type u_1)) ↦ μ.map f
T : Set (FiniteMeasure (↑K : Type u_1)) := {μ : FiniteMeasure (↑K : Type u_1) | μ.mass ≤ C}
μ : FiniteMeasure E
hμ :
  Membership.mem (γ := Set (FiniteMeasure E))
    {μ : FiniteMeasure E | μ.mass ≤ C ∧ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)} μ
s : Set E
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0) ((μ : (a : Set E) → ℝ≥0) Kᶜ : ℝ≥0) (0 : ℝ≥0)

Tactic:
hμ.2

Premises used: And.right