awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
y : Y
x : X
hx : x ∉ U
⊢ f x y = 0
have contrapose! : ∀ (hx : f x y ≠ 0), x ∈ U
Tactic: contrapose! hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
y : Y
x : X
hx : f x y ≠ 0
⊢ x ∈ U
have this₁ : (x, y) ∈ support (uncurry f)
Tactic: have : (x, y) ∈ Function.support f.uncurry := hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν)
have f₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ)
Tactic: calc
  ∫ x, (∫ y, f x y ∂ν) ∂μ = ∫ x, (∫ y in V, f x y ∂ν) ∂μ := by
    congr 1 with x
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
    contrapose! hy
    have : (x, y) ∈ Function.support f.uncurry := hy
    exact mem_image_of_mem _ (subset_tsupport _ this)
  _ = ∫ x in U, (∫ y in V, f x y ∂ν) ∂μ := by
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
    have : ∀ y, f x y = 0 := by
      intro y
      contrapose! hx
      have : (x, y) ∈ Function.support f.uncurry := hx
      exact mem_image_of_mem _ (subset_tsupport _ this)
    simp [this]
  _ = ∫ y in V, (∫ x in U, f x y ∂μ) ∂ν := by
    apply integral_integral_swap
    apply (integrableOn_iff_integrable_of_support_subset (subset_tsupport f.uncurry)).mp
    refine ⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩
    obtain ⟨C, hC⟩ : ∃ C, ∀ p, ‖f.uncurry p‖ ≤ C := hf.bounded_above_of_compact_support h'f
    exact .of_bounded (C := C) (.of_forall hC)
  _ = ∫ y, (∫ x in U, f x y ∂μ) ∂ν := by
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)
    have : ∀ x, f x y = 0 := by
      intro x
      contrapose! hy
      have : (x, y) ∈ Function.support f.uncurry := hy
      exact mem_image_of_mem _ (subset_tsupport _ this)
    simp [this]
  _ = ∫ y, (∫ x, f x y ∂μ) ∂ν := by
    congr 1 with y
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)
    contrapose! hx
    have : (x, y) ∈ Function.support f.uncurry := hx
    exact mem_image_of_mem _ (subset_tsupport _ this)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
f₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν)
have f₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ) (∫ (x : X) in U, ∫ (y : Y) in V, f x y ∂ν ∂μ)
Tactic: calc
  ∫ x, (∫ y, f x y ∂ν) ∂μ = ∫ x, (∫ y in V, f x y ∂ν) ∂μ := by
    congr 1 with x
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
    contrapose! hy
    have : (x, y) ∈ Function.support f.uncurry := hy
    exact mem_image_of_mem _ (subset_tsupport _ this)
  _ = ∫ x in U, (∫ y in V, f x y ∂ν) ∂μ := by
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
    have : ∀ y, f x y = 0 := by
      intro y
      contrapose! hx
      have : (x, y) ∈ Function.support f.uncurry := hx
      exact mem_image_of_mem _ (subset_tsupport _ this)
    simp [this]
  _ = ∫ y in V, (∫ x in U, f x y ∂μ) ∂ν := by
    apply integral_integral_swap
    apply (integrableOn_iff_integrable_of_support_subset (subset_tsupport f.uncurry)).mp
    refine ⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩
    obtain ⟨C, hC⟩ : ∃ C, ∀ p, ‖f.uncurry p‖ ≤ C := hf.bounded_above_of_compact_support h'f
    exact .of_bounded (C := C) (.of_forall hC)
  _ = ∫ y, (∫ x in U, f x y ∂μ) ∂ν := by
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)
    have : ∀ x, f x y = 0 := by
      intro x
      contrapose! hy
      have : (x, y) ∈ Function.support f.uncurry := hy
      exact mem_image_of_mem _ (subset_tsupport _ this)
    simp [this]
  _ = ∫ y, (∫ x, f x y ∂μ) ∂ν := by
    congr 1 with y
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)
    contrapose! hx
    have : (x, y) ∈ Function.support f.uncurry := hx
    exact mem_image_of_mem _ (subset_tsupport _ this)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
f₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ)
f₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ) (∫ (x : X) in U, ∫ (y : Y) in V, f x y ∂ν ∂μ)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν)
have f₃ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in U, ∫ (y : Y) in V, f x y ∂ν ∂μ) (∫ (y : Y) in V, ∫ (x : X) in U, f x y ∂μ ∂ν)
Tactic: calc
  ∫ x, (∫ y, f x y ∂ν) ∂μ = ∫ x, (∫ y in V, f x y ∂ν) ∂μ := by
    congr 1 with x
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
    contrapose! hy
    have : (x, y) ∈ Function.support f.uncurry := hy
    exact mem_image_of_mem _ (subset_tsupport _ this)
  _ = ∫ x in U, (∫ y in V, f x y ∂ν) ∂μ := by
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
    have : ∀ y, f x y = 0 := by
      intro y
      contrapose! hx
      have : (x, y) ∈ Function.support f.uncurry := hx
      exact mem_image_of_mem _ (subset_tsupport _ this)
    simp [this]
  _ = ∫ y in V, (∫ x in U, f x y ∂μ) ∂ν := by
    apply integral_integral_swap
    apply (integrableOn_iff_integrable_of_support_subset (subset_tsupport f.uncurry)).mp
    refine ⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩
    obtain ⟨C, hC⟩ : ∃ C, ∀ p, ‖f.uncurry p‖ ≤ C := hf.bounded_above_of_compact_support h'f
    exact .of_bounded (C := C) (.of_forall hC)
  _ = ∫ y, (∫ x in U, f x y ∂μ) ∂ν := by
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)
    have : ∀ x, f x y = 0 := by
      intro x
      contrapose! hy
      have : (x, y) ∈ Function.support f.uncurry := hy
      exact mem_image_of_mem _ (subset_tsupport _ this)
    simp [this]
  _ = ∫ y, (∫ x, f x y ∂μ) ∂ν := by
    congr 1 with y
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)
    contrapose! hx
    have : (x, y) ∈ Function.support f.uncurry := hx
    exact mem_image_of_mem _ (subset_tsupport _ this)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
f₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ)
f₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ) (∫ (x : X) in U, ∫ (y : Y) in V, f x y ∂ν ∂μ)
f₃ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in U, ∫ (y : Y) in V, f x y ∂ν ∂μ) (∫ (y : Y) in V, ∫ (x : X) in U, f x y ∂μ ∂ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν)
have f₄ : Eq.{u_3 + 1} (α := E) (∫ (y : Y) in V, ∫ (x : X) in U, f x y ∂μ ∂ν) (∫ (y : Y), ∫ (x : X) in U, f x y ∂μ ∂ν)
Tactic: calc
  ∫ x, (∫ y, f x y ∂ν) ∂μ = ∫ x, (∫ y in V, f x y ∂ν) ∂μ := by
    congr 1 with x
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
    contrapose! hy
    have : (x, y) ∈ Function.support f.uncurry := hy
    exact mem_image_of_mem _ (subset_tsupport _ this)
  _ = ∫ x in U, (∫ y in V, f x y ∂ν) ∂μ := by
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
    have : ∀ y, f x y = 0 := by
      intro y
      contrapose! hx
      have : (x, y) ∈ Function.support f.uncurry := hx
      exact mem_image_of_mem _ (subset_tsupport _ this)
    simp [this]
  _ = ∫ y in V, (∫ x in U, f x y ∂μ) ∂ν := by
    apply integral_integral_swap
    apply (integrableOn_iff_integrable_of_support_subset (subset_tsupport f.uncurry)).mp
    refine ⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩
    obtain ⟨C, hC⟩ : ∃ C, ∀ p, ‖f.uncurry p‖ ≤ C := hf.bounded_above_of_compact_support h'f
    exact .of_bounded (C := C) (.of_forall hC)
  _ = ∫ y, (∫ x in U, f x y ∂μ) ∂ν := by
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)
    have : ∀ x, f x y = 0 := by
      intro x
      contrapose! hy
      have : (x, y) ∈ Function.support f.uncurry := hy
      exact mem_image_of_mem _ (subset_tsupport _ this)
    simp [this]
  _ = ∫ y, (∫ x, f x y ∂μ) ∂ν := by
    congr 1 with y
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)
    contrapose! hx
    have : (x, y) ∈ Function.support f.uncurry := hx
    exact mem_image_of_mem _ (subset_tsupport _ this)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
X : Type u_5
Y : Type u_6
inst_2 : TopologicalSpace X
inst_3 : TopologicalSpace Y
inst_4 : MeasurableSpace X
inst_5 : MeasurableSpace Y
inst_6 : OpensMeasurableSpace X
inst_7 : OpensMeasurableSpace Y
f : X → Y → E
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry f)
h'f : HasCompactSupport (uncurry f)
μ : Measure X
ν : Measure Y
inst_8 : IsFiniteMeasureOnCompacts μ
inst_9 : IsFiniteMeasureOnCompacts ν
U : Set X := Prod.fst '' tsupport (uncurry f)
this_1 : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞))
V : Set Y := Prod.snd '' tsupport (uncurry f)
this : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
f₁ : Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ)
f₂ : Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y) in V, f x y ∂ν ∂μ) (∫ (x : X) in U, ∫ (y : Y) in V, f x y ∂ν ∂μ)
f₃ : Eq.{u_3 + 1} (α := E) (∫ (x : X) in U, ∫ (y : Y) in V, f x y ∂ν ∂μ) (∫ (y : Y) in V, ∫ (x : X) in U, f x y ∂μ ∂ν)
f₄ : Eq.{u_3 + 1} (α := E) (∫ (y : Y) in V, ∫ (x : X) in U, f x y ∂μ ∂ν) (∫ (y : Y), ∫ (x : X) in U, f x y ∂μ ∂ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ) (∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν)
have f₅ : Eq.{u_3 + 1} (α := E) (∫ (y : Y), ∫ (x : X) in U, f x y ∂μ ∂ν) (∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν)
Tactic: calc
  ∫ x, (∫ y, f x y ∂ν) ∂μ = ∫ x, (∫ y in V, f x y ∂ν) ∂μ := by
    congr 1 with x
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
    contrapose! hy
    have : (x, y) ∈ Function.support f.uncurry := hy
    exact mem_image_of_mem _ (subset_tsupport _ this)
  _ = ∫ x in U, (∫ y in V, f x y ∂ν) ∂μ := by
    apply (setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
    have : ∀ y, f x y = 0 := by
      intro y
      contrapose! hx
      have : (x, y) ∈ Function.support f.uncurry := hx
      exact mem_image_of_mem _ (subset_tsupport _ this)
    simp [this]
  _ = ∫ y in V, (∫ x in U, f x y ∂μ) ∂ν := by
    apply integral_integral_swap
    apply (integrableOn_iff_integrable_of_support_subset (subset_tsupport f.uncurry)).mp
    refine ⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩
    obtain ⟨C, hC⟩ : ∃ C, ∀ p, ‖f.uncurry p‖ ≤ C := hf.bounded_above_of_compact_support h'f
    exact .of_bounded (C := C) (.of_forall hC)
  _ = ∫ y, (∫ x in U, f x y ∂μ) ∂ν := by
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)
    have : ∀ x, f x y = 0 := by
      intro x
      contrapose! hy
      have : (x, y) ∈ Function.support f.uncurry := hy
      exact mem_image_of_mem _ (subset_tsupport _ this)
    simp [this]
  _ = ∫ y, (∫ x, f x y ∂μ) ∂ν := by
    congr 1 with y
    apply setIntegral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)
    contrapose! hx
    have : (x, y) ∈ Function.support f.uncurry := hx
    exact mem_image_of_mem _ (subset_tsupport _ this)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : μ.InnerRegularCompactLTTop
inst_5 : LocallyCompactSpace X
inst_6 : RegularSpace X
⊢ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) k : ENNReal)
    (⨅ (f : X → ℝ),
        ⨅ (_ : Continuous f),
          ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)
have a : LE.le (α := ENNReal) ((μ : (a : Set X) → ENNReal) k : ENNReal)
  (⨅ (f : X → ℝ),
      ⨅ (_ : Continuous f),
        ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
    ENNReal)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : μ.InnerRegularCompactLTTop
inst_5 : LocallyCompactSpace X
inst_6 : RegularSpace X
a :
  LE.le (α := ENNReal) ((μ : (a : Set X) → ENNReal) k : ENNReal)
    (⨅ (f : X → ℝ),
        ⨅ (_ : Continuous f),
          ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) k : ENNReal)
    (⨅ (f : X → ℝ),
        ⨅ (_ : Continuous f),
          ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)
have a₁ : LE.le (α := ENNReal)
  (⨅ (f : X → ℝ),
      ⨅ (_ : Continuous f),
        ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
    ENNReal)
  ((μ : (a : Set X) → ENNReal) k : ENNReal)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : μ.InnerRegularCompactLTTop
inst_5 : LocallyCompactSpace X
inst_6 : RegularSpace X
⊢ LE.le (α := ENNReal) ((μ : (a : Set X) → ENNReal) k : ENNReal)
    (⨅ (f : X → ℝ),
        ⨅ (_ : Continuous f),
          ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)
have a : ∀ (i : X → ℝ) (i_1 : Continuous i) (i_2 : HasCompactSupport i) (i_3 : EqOn i 1 k) (i_4 : 0 ≤ i),
  (μ : (a : Set X) → ENNReal) k ≤ ENNReal.ofReal (∫ (x : X), i x ∂μ)
Tactic: simp only [le_iInf_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : μ.InnerRegularCompactLTTop
inst_5 : LocallyCompactSpace X
inst_6 : RegularSpace X
f : X → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport f
fk : EqOn f 1 k
f_nonneg : 0 ≤ f
⊢ (μ : (a : Set X) → ENNReal) k ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
have a : 0 ≤ᶠ[ae μ] f
Tactic: apply (f_cont.integrable_of_hasCompactSupport f_comp).measure_le_integral
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : μ.InnerRegularCompactLTTop
inst_5 : LocallyCompactSpace X
inst_6 : RegularSpace X
f : X → ℝ
f_cont : Continuous f
f_comp : HasCompactSupport f
fk : EqOn f 1 k
f_nonneg : 0 ≤ f
a : 0 ≤ᶠ[ae μ] f
⊢ (μ : (a : Set X) → ENNReal) k ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)
have a₁ : ∀ x ∈ k, 1 ≤ f x
Tactic: apply (f_cont.integrable_of_hasCompactSupport f_comp).measure_le_integral
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : μ.InnerRegularCompactLTTop
inst_5 : LocallyCompactSpace X
inst_6 : RegularSpace X
⊢ LE.le (α := ENNReal)
    (⨅ (f : X → ℝ),
        ⨅ (_ : Continuous f),
          ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)
    ((μ : (a : Set X) → ENNReal) k : ENNReal)
have apply : ∀ (r : ENNReal) (hr : (μ : (a : Set X) → ENNReal) k < r),
  ⨅ (f : X → ℝ),
      ⨅ (_ : Continuous f),
        ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) <
    r
Tactic: apply le_of_forall_gt (fun r hr ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : μ.InnerRegularCompactLTTop
inst_5 : LocallyCompactSpace X
inst_6 : RegularSpace X
r : ENNReal
hr : (μ : (a : Set X) → ENNReal) k < r
⊢ ⨅ (f : X → ℝ),
      ⨅ (_ : Continuous f),
        ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) <
    r
have simp : ∃ (i : X → ℝ), Continuous i ∧ HasCompactSupport i ∧ EqOn i 1 k ∧ 0 ≤ i ∧ ENNReal.ofReal (∫ (x : X), i x ∂μ) < r
Tactic: simp only [iInf_lt_iff, exists_prop]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : μ.InnerRegularCompactLTTop
inst_5 : LocallyCompactSpace X
inst_6 : RegularSpace X
r : ENNReal
hr : (μ : (a : Set X) → ENNReal) k < r
⊢ ∃ (i : X → ℝ), Continuous i ∧ HasCompactSupport i ∧ EqOn i 1 k ∧ 0 ≤ i ∧ ENNReal.ofReal (∫ (x : X), i x ∂μ) < r
have obtain : ∀ (U : Set X) (kU : k ⊆ U) (U_open : IsOpen U) (mu_U : (μ : (a : Set X) → ENNReal) U < r),
  ∃ (i : X → ℝ), Continuous i ∧ HasCompactSupport i ∧ EqOn i 1 k ∧ 0 ≤ i ∧ ENNReal.ofReal (∫ (x : X), i x ∂μ) < r
Tactic: obtain ⟨U, kU, U_open, mu_U⟩ : ∃ U, k ⊆ U ∧ IsOpen U ∧ μ U < r :=
      hk.exists_isOpen_lt_of_lt r hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Regular (goal)
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
k : Set X
hk : IsCompact k
μ : Measure X
inst_3 : IsFiniteMeasureOnCompacts μ
inst_4 : μ.InnerRegularCompactLTTop
inst_5 : LocallyCompactSpace X
inst_6 : RegularSpace X
r : ENNReal
hr : (μ : (a : Set X) → ENNReal) k < r
U : Set X
kU : k ⊆ U
U_open : IsOpen U
mu_U : (μ : (a : Set X) → ENNReal) U < r
⊢ ∃ (i : X → ℝ), Continuous i ∧ HasCompactSupport i ∧ EqOn i 1 k ∧ 0 ≤ i ∧ ENNReal.ofReal (∫ (x : X), i x ∂μ) < r
have obtain : ∀ (f : X → ℝ) (f_cont : Continuous f)
  (fk : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 1 k)
  (fU : EqOn (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) 0 Uᶜ)
  (f_comp : HasCompactSupport (α := X) (β := ℝ) (⇑{ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ))
  (f_range :
    ∀ (x : X),
      Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1)
        (({ toFun := f, continuous_toFun := f_cont : C(X, ℝ) } : (a : X) → ℝ) x : ℝ)),
  ∃ (i : X → ℝ), Continuous i ∧ HasCompactSupport i ∧ EqOn i 1 k ∧ 0 ≤ i ∧ ENNReal.ofReal (∫ (x : X), i x ∂μ) < r
Tactic: obtain ⟨⟨f, f_cont⟩, fk, fU, f_comp, f_range⟩ : ∃ (f : C(X, ℝ)), EqOn f 1 k ∧ EqOn f 0 Uᶜ
        ∧ HasCompactSupport f ∧ ∀ (x : X), f x ∈ Icc 0 1 := exists_continuous_one_zero_of_isCompact
      hk U_open.isClosed_compl (disjoint_compl_right_iff_subset.mpr kU)