awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable Y μ
s : Set γ
hs : MeasurableSet s
pos :
  Eq (α := ℝ≥0∞) ((map (fun (a : α) ↦ (X a, Y a)) μ : (a : Set (β × γ)) → ℝ≥0∞) (Prod.snd ⁻¹' s) : ℝ≥0∞)
    (((map Y μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
pos₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β × γ) (fun (x : α) ↦ (X x, Y x)) (Prod.snd ⁻¹' s)) : ℝ≥0∞)
    (((map Y μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
pos₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β × γ) (fun (x : α) ↦ (X x, Y x)) (Prod.snd ⁻¹' s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Y ⁻¹' s) : ℝ≥0∞)
pos₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (X x, Y x)) ⁻¹' SProd.sprod (α := Set β) univ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (Y ⁻¹' s) : ℝ≥0∞)
pos₄ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' univ ∩ Y ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Y ⁻¹' s) : ℝ≥0∞)
pos₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ Y ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Y ⁻¹' s) : ℝ≥0∞)
pos₆ pos₇ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Y ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Y ⁻¹' s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (((snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ) : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)
    (((map Y μ : Measure γ) : (a : Set γ) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [Measure.snd_apply hs, Measure.map_apply_of_aemeasurable (hX.prodMk hY) (measurable_snd hs),
      Measure.map_apply_of_aemeasurable hY hs, ← univ_prod, mk_preimage_prod, preimage_univ,
      univ_inter]

Premises used: Set.univ_prod, Set.univ_inter, AEMeasurable.prodMk, MeasureTheory.Measure.map_apply_of_aemeasurable, measurable_snd, Set.preimage_univ, MeasureTheory.Measure.snd_apply, Set.mk_preimage_prod
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
contrapose : ∀ (hY : AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ), AEMeasurable Y μ
⊢ ¬AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ

Tactic:
contrapose hY
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ
⊢ AEMeasurable Y μ

Tactic:
measurable_snd.comp_aemeasurable hY

Premises used: measurable_snd, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ
⊢ AEMeasurable Y μ

Tactic:
exact measurable_snd.comp_aemeasurable hY

Premises used: measurable_snd, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
⊢ ¬AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ

Tactic:
have : ¬AEMeasurable (fun x ↦ (X x, Y x)) μ := by
      contrapose hY
      exact measurable_snd.comp_aemeasurable hY
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
hY : ¬AEMeasurable Y μ
this : ¬AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ
⊢ Eq (α := Measure γ) (snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map Y μ)

Tactic:
simp [map_of_not_aemeasurable, hY, this]

Premises used: MeasureTheory.Measure.map_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : Measurable X
⊢ Eq (α := Measure γ) (snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map Y μ)

Tactic:
snd_map_prodMk₀ hX.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.snd_map_prodMk₀
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ ν : Measure (α × β)
⊢ (μ + ν).snd = μ.snd + ν.snd

Tactic:
Measure.map_add _ _ measurable_snd

Premises used: MeasureTheory.Measure.map_add, MeasureTheory.Measure.snd, measurable_snd
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ι : Type u_4
μ : ι → Measure (α × β)
⊢ (sum μ).snd = sum fun (n : ι) ↦ (μ n).snd

Tactic:
map_sum measurable_snd.aemeasurable

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.map_sum, MeasureTheory.Measure.snd, measurable_snd
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ μ : Measure (α × β)
h : ρ ≤ μ
⊢ ρ.snd ≤ μ.snd

Tactic:
map_mono h measurable_snd

Premises used: measurable_snd, MeasureTheory.Measure.map_mono
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
rw : map (Prod.fst ∘ Prod.swap) ρ = ρ.snd
⊢ fst (map Prod.swap ρ) = ρ.snd

Tactic:
rw [Measure.fst, Measure.map_map measurable_fst measurable_swap]

Premises used: measurable_swap, MeasureTheory.Measure.map_map, measurable_fst, MeasureTheory.Measure.fst
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
⊢ map (Prod.fst ∘ Prod.swap) ρ = ρ.snd

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
rw : map (Prod.snd ∘ Prod.swap) ρ = ρ.fst
⊢ snd (map Prod.swap ρ) = ρ.fst

Tactic:
rw [Measure.snd, Measure.map_map measurable_snd measurable_swap]

Premises used: MeasureTheory.Measure.snd, measurable_swap, measurable_snd, MeasureTheory.Measure.map_map
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
⊢ map (Prod.snd ∘ Prod.swap) ρ = ρ.fst

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
inst_3 : SFinite μb
inst_4 : SFinite μc
h :
  ∀ (s : Set (α × β × γ)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ((μa.prod μb).prod μc) :
            (a : Set (α × β × γ)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((μa.prod (μb.prod μc) : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ((μa.prod μb).prod μc) = μa.prod (μb.prod μc)

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
inst_3 : SFinite μb
inst_4 : SFinite μc
s : Set (α × β × γ)
hs : MeasurableSet s
⊢ ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)

Tactic:
have A (x : α) : MeasurableSet (Prod.mk x ⁻¹' s) := measurable_prodMk_left hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
inst_3 : SFinite μb
inst_4 : SFinite μc
s : Set (α × β × γ)
hs : MeasurableSet s
A : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
⊢ MeasurableSet (α := (α × β) × γ) ((⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s)

Tactic:
have B : MeasurableSet (MeasurableEquiv.prodAssoc ⁻¹' s) :=
      MeasurableEquiv.prodAssoc.measurable hs
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
inst_3 : SFinite μb
inst_4 : SFinite μc
s : Set (α × β × γ)
hs : MeasurableSet s
A : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
B : MeasurableSet (α := (α × β) × γ) ((⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s)
h :
  ∫⁻ (x : α),
      ∫⁻ (y : β),
        (μc : (a : Set γ) → ℝ≥0∞)
          (Prod.mk (x, y) ⁻¹' (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s) ∂μb ∂μa =
    ∫⁻ (x : α), ∫⁻ (x_1 : β), (μc : (a : Set γ) → ℝ≥0∞) (Prod.mk x_1 ⁻¹' Prod.mk x ⁻¹' s) ∂μb ∂μa
⊢ Eq (α := ℝ≥0∞)
    ((map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ((μa.prod μb).prod μc) :
          (a : Set (α × β × γ)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((μa.prod (μb.prod μc) : (a : Set (α × β × γ)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp_rw [map_apply MeasurableEquiv.prodAssoc.measurable hs, Measure.prod_apply hs,
    Measure.prod_apply (A _), Measure.prod_apply B,
    lintegral_prod _ (measurable_measure_prodMk_left B).aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.map_apply, MeasureTheory.Measure.prod_apply, MeasureTheory.lintegral_prod, MeasurableEquiv.prodAssoc, measurable_measure_prodMk_left, MeasurableEquiv.measurable
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
μa : Measure α
μb : Measure β
μc : Measure γ
inst_3 : SFinite μb
inst_4 : SFinite μc
s : Set (α × β × γ)
hs : MeasurableSet s
A : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
B : MeasurableSet (α := (α × β) × γ) ((⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s)
⊢ ∫⁻ (x : α),
      ∫⁻ (y : β),
        (μc : (a : Set γ) → ℝ≥0∞)
          (Prod.mk (x, y) ⁻¹' (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s) ∂μb ∂μa =
    ∫⁻ (x : α), ∫⁻ (x_1 : β), (μc : (a : Set γ) → ℝ≥0∞) (Prod.mk x_1 ⁻¹' Prod.mk x ⁻¹' s) ∂μb ∂μa

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Measure.Prod
Goal:
α₁ : Type u_4
β₁ : Type u_5
γ₁ : Type u_6
inst : MeasureSpace α₁
inst_1 : MeasureSpace β₁
inst_2 : MeasureSpace γ₁
inst_3 : SFinite.{u_5} (α := β₁) (m0 := MeasureSpace.toMeasurableSpace) volume
inst_4 : SFinite.{u_6} (α := γ₁) (m0 := MeasureSpace.toMeasurableSpace) volume
⊢ MeasurePreserving (α := (α₁ × β₁) × γ₁) (β := α₁ × β₁ × γ₁)
    (⇑MeasurableEquiv.prodAssoc : (a : (α₁ × β₁) × γ₁) → α₁ × β₁ × γ₁) (volume : Measure ((α₁ × β₁) × γ₁))
    (volume : Measure (α₁ × β₁ × γ₁))

Tactic:
MeasureTheory.measurePreserving_prodAssoc volume volume volume

Premises used: MeasureTheory.measurePreserving_prodAssoc, MeasureTheory.MeasureSpace.volume
-- 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
apply :
  ∀ (f : Ultrafilter (FiniteMeasure E)) (hf : {μ : FiniteMeasure E | μ.mass ≤ C} ∈ f),
    ∃ (x : FiniteMeasure E),
      Membership.mem (γ := Set (FiniteMeasure E)) {μ : FiniteMeasure E | μ.mass ≤ C} x ∧
        (↑f : Filter (FiniteMeasure E)) ≤ 𝓝 x
⊢ IsCompact.{u_1} (X := FiniteMeasure E) {μ : FiniteMeasure E | μ.mass ≤ C}

Tactic:
apply isCompact_iff_ultrafilter_le_nhds'.2 (fun f hf ↦ ?_)

Premises used: Iff.mpr, isCompact_iff_ultrafilter_le_nhds'
-- 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 ℝ
a :
  Membership.mem (γ := Ultrafilter ℝ)
    (Ultrafilter.map (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) f)
    (Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖))
⊢ ∃ x ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖),
    (↑(Ultrafilter.map (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) f) : Filter ℝ) ≤
      𝓝 x

Tactic:
apply IsCompact.ultrafilter_le_nhds' isCompact_Icc

Premises used: IsCompact.ultrafilter_le_nhds', CompactIccSpace.isCompact_Icc
-- 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 ℝ
a :
  (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) ⁻¹'
      Icc (-((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ∈
    f
⊢ Membership.mem (γ := Ultrafilter ℝ)
    (Ultrafilter.map (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) f)
    (Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖))

Tactic:
simp only [neg_mul, Ultrafilter.mem_map]

Premises used: Ultrafilter.mem_map, neg_mul
-- 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 :
  ∀ (μ : FiniteMeasure E) (hμ : μ.mass ≤ C),
    Membership.mem (γ := Set (FiniteMeasure E))
      ((fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) ⁻¹'
        Icc (-((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖))
      μ
⊢ (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) ⁻¹'
      Icc (-((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ∈
    f

Tactic:
filter_upwards [hf] with μ hμ
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ -((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E) ∧
    ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E) ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖

Tactic:
⟨?_, ?_⟩

Premises used: And.intro
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
h : -((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)
h₁ : ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E) ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖
⊢ -((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E) ∧
    ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E) ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖

Tactic:
refine ⟨?_, ?_⟩
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
simp : (↑μ : Measure E).real univ * ‖g.toBoundedContinuousFunction‖ ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖
⊢ -((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), -‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E)

Tactic:
simp only [integral_const, smul_eq_mul, mul_neg, neg_le_neg_iff]

Premises used: MeasureTheory.integral_const, smul_eq_mul, mul_neg, neg_le_neg_iff
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
hbc : (↑μ : Measure E).real univ ≤ (↑C : ℝ)
⊢ (↑μ : Measure E).real univ * ‖g.toBoundedContinuousFunction‖ ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖

Tactic:
gcongr
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ (↑μ : Measure E).real univ ≤ (↑C : ℝ)

Tactic:
hμ

Premises used: MeasureTheory.Measure.real, ENNReal.toReal, NNReal.toReal
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ (↑μ : Measure E).real univ ≤ (↑C : ℝ)

Tactic:
exact hμ
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
hf₁ : Integrable (ε := ℝ) (fun (x : E) ↦ -‖g.toBoundedContinuousFunction‖) (↑μ : Measure E)
hg : Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑μ : Measure E)
h : LE.le (α := E → ℝ) (fun (x : E) ↦ -‖g.toBoundedContinuousFunction‖) (⇑g : (a : E) → ℝ)
⊢ LE.le (α := ℝ) (∫ (x : E), -‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E))
    (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))

Tactic:
gcongr
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ -‖g.toBoundedContinuousFunction‖) (↑μ : Measure E)

Tactic:
simp
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑μ : Measure E)

Tactic:
g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport

Premises used: ContinuousMap.continuous, CompactlySupportedContinuousMap.hasCompactSupport, Continuous.integrable_of_hasCompactSupport, CompactlySupportedContinuousMap.toContinuousMap
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑μ : Measure E)

Tactic:
exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport

Premises used: ContinuousMap.continuous, CompactlySupportedContinuousMap.hasCompactSupport, Continuous.integrable_of_hasCompactSupport, CompactlySupportedContinuousMap.toContinuousMap
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
x : E
h : |(g : (a : E) → ℝ) x| ≤ ‖g.toBoundedContinuousFunction‖
⊢ LE.le (α := (fun (a : E) ↦ ℝ) x) ((fun (x : E) ↦ -‖g.toBoundedContinuousFunction‖) x : ℝ) ((g : (a : E) → ℝ) x : ℝ)

Tactic:
apply neg_le_of_abs_le

Premises used: neg_le_of_abs_le
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
x : E
⊢ |(g : (a : E) → ℝ) x| ≤ ‖g.toBoundedContinuousFunction‖

Tactic:
g.toBoundedContinuousFunction.norm_coe_le_norm x

Premises used: CompactlySupportedContinuousMap.toBoundedContinuousFunction, BoundedContinuousFunction.norm_coe_le_norm
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
x : E
⊢ |(g : (a : E) → ℝ) x| ≤ ‖g.toBoundedContinuousFunction‖

Tactic:
exact g.toBoundedContinuousFunction.norm_coe_le_norm x

Premises used: CompactlySupportedContinuousMap.toBoundedContinuousFunction, BoundedContinuousFunction.norm_coe_le_norm
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
calc : -((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), -‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E)
calc₁ :
  LE.le (α := ℝ) (∫ (x : E), -‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E))
    (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
⊢ -((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)

Tactic:
calc - (C * ‖g.toBoundedContinuousFunction‖)
      _ ≤ ∫ (x : E), - ‖g.toBoundedContinuousFunction‖ ∂μ := by
        simp only [integral_const, smul_eq_mul, mul_neg, neg_le_neg_iff]
        gcongr
        exact hμ
      _ ≤ ∫ x, g x ∂μ := by
        gcongr
        · simp
        · exact g.continuous.integrable_of_hasCompactSupport g.hasCompactSupport
        · intro x
          apply neg_le_of_abs_le
          exact g.toBoundedContinuousFunction.norm_coe_le_norm x

Premises used: Norm.norm, HMul.hMul, CompactlySupportedContinuousMap.toBoundedContinuousFunction, NNReal.toReal
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
hf₁ : Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑μ : Measure E)
hg : Integrable (ε := ℝ) (fun (x : E) ↦ ‖g.toBoundedContinuousFunction‖) (↑μ : Measure E)
h : LE.le (α := E → ℝ) (⇑g : (a : E) → ℝ) fun (x : E) ↦ ‖g.toBoundedContinuousFunction‖
⊢ LE.le (α := ℝ) (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
    (∫ (x : E), ‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E))

Tactic:
gcongr
-- 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 ℝ
μ : FiniteMeasure E
hμ : μ.mass ≤ C
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ ‖g.toBoundedContinuousFunction‖) (↑μ : Measure E)

Tactic:
simp