awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSpace γ
X : α → β
Y : α → γ
μ : Measure α
hX : AEMeasurable X μ
pos :
  ∀ (hY : AEMeasurable Y μ), Eq (α := Measure γ) (snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map Y μ)
⊢ Eq (α := Measure γ) (snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map Y μ)
have neg : ∀ (hY : ¬AEMeasurable Y μ), Eq (α := Measure γ) (snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map Y μ)
Tactic: by_cases hY : AEMeasurable Y μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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 μ
⊢ Eq (α := Measure γ) (snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map Y μ)
have pos : ∀ (s : Set γ) (hs : MeasurableSet s),
  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: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ 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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ 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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ 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∞)
have pos₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := β × γ) (fun (x : α) ↦ (X x, Y x)) (Prod.snd ⁻¹' s)) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (Y ⁻¹' 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ 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∞)
have pos₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ((fun (x : α) ↦ (X x, Y x)) ⁻¹' SProd.sprod (α := Set β) univ s) : ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) (Y ⁻¹' 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ 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∞)
have pos₄ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (X ⁻¹' univ ∩ Y ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Y ⁻¹' 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ 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∞)
have pos₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (univ ∩ Y ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Y ⁻¹' 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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∞)
⊢ 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∞)
have pos₆ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Y ⁻¹' s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Y ⁻¹' 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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)) μ
have contrapose : ∀ (hY : AEMeasurable (β := β × γ) (fun (x : α) ↦ (X x, Y x)) μ), AEMeasurable Y μ
Tactic: contrapose hY
Cleared hypotheses: hY
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
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 μ
⊢ Eq (α := Measure γ) (snd.{u_2, u_3} (α := β) (map (fun (a : α) ↦ (X a, Y a)) μ)) (map Y μ)
have this : ¬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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
⊢ fst (map Prod.swap ρ) = ρ.snd
have rw : map (Prod.fst ∘ Prod.swap) ρ = ρ.snd
Tactic: rw [Measure.fst, Measure.map_map measurable_fst measurable_swap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
ρ : Measure (α × β)
⊢ snd (map Prod.swap ρ) = ρ.fst
have rw : map (Prod.snd ∘ Prod.swap) ρ = ρ.fst
Tactic: rw [Measure.snd, Measure.map_map measurable_snd measurable_swap]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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
⊢ map (⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ((μa.prod μb).prod μc) = μa.prod (μb.prod μc)
have 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∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
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
⊢ 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∞)
have A : ∀ (x : α), MeasurableSet (Prod.mk x ⁻¹' s)
Tactic: have A (x : α) : MeasurableSet (Prod.mk x ⁻¹' s) := measurable_prodMk_left hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (hypothesis)
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)
⊢ 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∞)
have B : MeasurableSet (α := (α × β) × γ) ((⇑MeasurableEquiv.prodAssoc : (a : (α × β) × γ) → α × β × γ) ⁻¹' s)
Tactic: have B : MeasurableSet (MeasurableEquiv.prodAssoc ⁻¹' s) :=
      MeasurableEquiv.prodAssoc.measurable hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prod (goal)
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)
⊢ 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∞)
have 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
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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
⊢ IsCompact.{u_1} (X := FiniteMeasure E) {μ : FiniteMeasure E | μ.mass ≤ C}
have 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
Tactic: apply isCompact_iff_ultrafilter_le_nhds'.2 (fun f hf ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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 ℝ
⊢ ∃ x ∈ Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖),
    (↑(Ultrafilter.map (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) f) : Filter ℝ) ≤
      𝓝 x
have 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‖))
Tactic: apply IsCompact.ultrafilter_le_nhds' isCompact_Icc
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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 ℝ
⊢ Membership.mem (γ := Ultrafilter ℝ)
    (Ultrafilter.map (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) f)
    (Icc (-(↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖))
have a : (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) ⁻¹'
    Icc (-((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ∈
  f
Tactic: simp only [neg_mul, Ultrafilter.mem_map]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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 ℝ
⊢ (fun (μ : FiniteMeasure E) ↦ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)) ⁻¹'
      Icc (-((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖)) ((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ∈
    f
have 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‖))
    μ
Tactic: filter_upwards [hf] with μ hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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‖
have h : -((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E)
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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)
⊢ -((↑C : ℝ) * ‖g.toBoundedContinuousFunction‖) ≤ ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E) ∧
    ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E) ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖
have h₁ : ∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E) ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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.toBoundedContinuousFunction‖ ∂(↑μ : Measure E)
have simp : (↑μ : Measure E).real univ * ‖g.toBoundedContinuousFunction‖ ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖
Tactic: simp only [integral_const, smul_eq_mul, mul_neg, neg_le_neg_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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 * ‖g.toBoundedContinuousFunction‖ ≤ (↑C : ℝ) * ‖g.toBoundedContinuousFunction‖
have hbc : (↑μ : Measure E).real univ ≤ (↑C : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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
⊢ LE.le (α := ℝ) (∫ (x : E), -‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E))
    (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
have hf₁ : Integrable (ε := ℝ) (fun (x : E) ↦ -‖g.toBoundedContinuousFunction‖) (↑μ : Measure E)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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)
⊢ LE.le (α := ℝ) (∫ (x : E), -‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E))
    (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
have hg : Integrable (ε := ℝ) (⇑g : (a : E) → ℝ) (↑μ : Measure E)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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)
⊢ LE.le (α := ℝ) (∫ (x : E), -‖g.toBoundedContinuousFunction‖ ∂(↑μ : Measure E))
    (∫ (x : E), (g : (a : E) → ℝ) x ∂(↑μ : Measure E))
have h : LE.le (α := E → ℝ) (fun (x : E) ↦ -‖g.toBoundedContinuousFunction‖) (⇑g : (a : E) → ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Prokhorov (goal)
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
⊢ LE.le (α := (fun (a : E) ↦ ℝ) x) ((fun (x : E) ↦ -‖g.toBoundedContinuousFunction‖) x : ℝ) ((g : (a : E) → ℝ) x : ℝ)
have h : |(g : (a : E) → ℝ) x| ≤ ‖g.toBoundedContinuousFunction‖
Tactic: apply neg_le_of_abs_le