awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Prod
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, y) ∈ support (uncurry f)

Tactic:
have : (x, y) ∈ Function.support f.uncurry := hx
-- Module: Mathlib.MeasureTheory.Integral.Prod
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_2 : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
y : Y
x : X
hx : f x y ≠ 0
this : (x, y) ∈ support (uncurry f)
⊢ x ∈ U

Tactic:
mem_image_of_mem _ (subset_tsupport _ this)

Premises used: Set.Mem, subset_tsupport, Set.mem_image_of_mem
-- Module: Mathlib.MeasureTheory.Integral.Prod
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_2 : Fact (LT.lt (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) V : ℝ≥0∞) (∞ : ℝ≥0∞))
y : Y
x : X
hx : f x y ≠ 0
this : (x, y) ∈ support (uncurry f)
⊢ x ∈ U

Tactic:
exact mem_image_of_mem _ (subset_tsupport _ this)

Premises used: subset_tsupport, Set.mem_image_of_mem
-- Module: Mathlib.MeasureTheory.Integral.Prod
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 ∂μ ∂ν)
f₅ : Eq.{u_3 + 1} (α := E) (∫ (y : Y), ∫ (x : X) in U, f x y ∂μ ∂ν) (∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν)
⊢ Eq.{u_3 + 1} (α := E) (∫ (x : X), ∫ (y : Y), 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)
-- Module: Mathlib.MeasureTheory.Integral.Regular
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)
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)
⊢ 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)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Integral.Regular
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 :
  ∀ (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 ∂μ)
⊢ 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:
simp only [le_iInf_iff]

Premises used: le_iInf_iff
-- Module: Mathlib.MeasureTheory.Integral.Regular
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₁ : ∀ x ∈ k, 1 ≤ f x
⊢ (μ : (a : Set X) → ENNReal) k ≤ ENNReal.ofReal (∫ (x : X), f x ∂μ)

Tactic:
apply (f_cont.integrable_of_hasCompactSupport f_comp).measure_le_integral

Premises used: Continuous.integrable_of_hasCompactSupport, MeasureTheory.Integrable.measure_le_integral
-- Module: Mathlib.MeasureTheory.Integral.Regular
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
⊢ 0 ≤ᶠ[ae μ] f

Tactic:
Eventually.of_forall f_nonneg

Premises used: Filter.Eventually.of_forall, Filter.EventuallyLE
-- Module: Mathlib.MeasureTheory.Integral.Regular
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
⊢ 0 ≤ᶠ[ae μ] f

Tactic:
exact Eventually.of_forall f_nonneg

Premises used: Filter.Eventually.of_forall
-- Module: Mathlib.MeasureTheory.Integral.Regular
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
x : X
hx : x ∈ k
⊢ 1 ≤ f x

Tactic:
simp [fk hx]
-- Module: Mathlib.MeasureTheory.Integral.Regular
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
⊢ ∀ x ∈ k, 1 ≤ f x

Tactic:
exact fun x hx ↦ by simp [fk hx]
-- Module: Mathlib.MeasureTheory.Integral.Regular
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
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
⊢ 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_of_forall_gt (fun r hr ↦ ?_)

Premises used: le_of_forall_gt
-- Module: Mathlib.MeasureTheory.Integral.Regular
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
simp : ∃ (i : X → ℝ), Continuous i ∧ HasCompactSupport i ∧ EqOn i 1 k ∧ 0 ≤ i ∧ ENNReal.ofReal (∫ (x : X), i x ∂μ) < r
⊢ ⨅ (f : X → ℝ),
      ⨅ (_ : Continuous f),
        ⨅ (_ : HasCompactSupport f), ⨅ (_ : EqOn f 1 k), ⨅ (_ : 0 ≤ f), ENNReal.ofReal (∫ (x : X), f x ∂μ) <
    r

Tactic:
simp only [iInf_lt_iff, exists_prop]

Premises used: exists_prop, iInf_lt_iff
-- Module: Mathlib.MeasureTheory.Integral.Regular
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), k ⊆ U ∧ IsOpen U ∧ (μ : (a : Set X) → ENNReal) U < r

Tactic:
hk.exists_isOpen_lt_of_lt r hr

Premises used: IsCompact.exists_isOpen_lt_of_lt
-- Module: Mathlib.MeasureTheory.Integral.Regular
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
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
⊢ ∃ (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

Premises used: IsCompact.exists_isOpen_lt_of_lt
-- Module: Mathlib.MeasureTheory.Integral.Regular
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
⊢ ∃ (f : C(X, ℝ)),
    EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 1 k ∧
      EqOn (β := ℝ) (⇑f : (a : X) → ℝ) 0 Uᶜ ∧
        HasCompactSupport (α := X) (β := ℝ) (⇑f : (a : X) → ℝ) ∧
          ∀ (x : X), Membership.mem (α := ℝ) (γ := Set ℝ) (Icc 0 1) ((f : (a : X) → ℝ) x : ℝ)

Tactic:
exists_continuous_one_zero_of_isCompact
      hk U_open.isClosed_compl (disjoint_compl_right_iff_subset.mpr kU)

Premises used: Iff.mpr, exists_continuous_one_zero_of_isCompact, Set.disjoint_compl_right_iff_subset, IsOpen.isClosed_compl
-- Module: Mathlib.MeasureTheory.Integral.Regular
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
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
⊢ ∃ (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)

Premises used: Iff.mpr, exists_continuous_one_zero_of_isCompact, Set.disjoint_compl_right_iff_subset, IsOpen.isClosed_compl
-- Module: Mathlib.MeasureTheory.Integral.Regular
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
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:
⟨f, f_cont, f_comp, fk, fun x ↦ (f_range x).1, ?_⟩

Premises used: And.left, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Regular
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
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 : ℝ)
refine : ENNReal.ofReal (∫ (x : X), f x ∂μ) < r
⊢ ∃ (i : X → ℝ), Continuous i ∧ HasCompactSupport i ∧ EqOn i 1 k ∧ 0 ≤ i ∧ ENNReal.ofReal (∫ (x : X), i x ∂μ) < r

Tactic:
refine ⟨f, f_cont, f_comp, fk, fun x ↦ (f_range x).1, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.Regular
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
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 : ℝ)
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) < r

Tactic:
(integral_le_measure (fun x _hx ↦ (f_range x).2) (fun x hx ↦ (fU hx).le)).trans_lt mu_U

Premises used: Eq.le, MeasureTheory.integral_le_measure, And.right, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Integral.Regular
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
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 : ℝ)
⊢ ENNReal.ofReal (∫ (x : X), f x ∂μ) < r

Tactic:
exact (integral_le_measure (fun x _hx ↦ (f_range x).2) (fun x hx ↦ (fU hx).le)).trans_lt mu_U

Premises used: Eq.le, MeasureTheory.integral_le_measure, And.right, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
a :
  LE.le (α := ENNReal) ((μ : (a : Set X) → ENNReal) U : ENNReal)
    (⨆ (f : X → ℝ),
        ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)
a₁ :
  LE.le (α := ENNReal)
    (⨆ (f : X → ℝ),
        ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)
    ((μ : (a : Set X) → ENNReal) U : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set X) → ENNReal) U : ENNReal)
    (⨆ (f : X → ℝ),
        ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
apply :
  ∀ (r : ENNReal) (hr : r < (μ : (a : Set X) → ENNReal) U),
    r <
      ⨆ (f : X → ℝ),
        ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ)
⊢ LE.le (α := ENNReal) ((μ : (a : Set X) → ENNReal) U : ENNReal)
    (⨆ (f : X → ℝ),
        ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ) :
      ENNReal)

Tactic:
apply le_of_forall_lt (fun r hr ↦ ?_)

Premises used: le_of_forall_lt
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
simp : ∃ (i : X → ℝ), Continuous i ∧ EqOn i 0 Uᶜ ∧ 0 ≤ i ∧ i ≤ 1 ∧ r < ENNReal.ofReal (∫ (x : X), i x ∂μ)
⊢ r <
    ⨆ (f : X → ℝ),
      ⨆ (_ : Continuous f), ⨆ (_ : EqOn f 0 Uᶜ), ⨆ (_ : 0 ≤ f), ⨆ (_ : f ≤ 1), ENNReal.ofReal (∫ (x : X), f x ∂μ)

Tactic:
simp only [lt_iSup_iff, exists_prop]

Premises used: exists_prop, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Integral.Regular
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : T2Space X
U : Set X
hU : IsOpen U
μ : Measure X
inst_4 : IsFiniteMeasure μ
inst_5 : μ.InnerRegularCompactLTTop
inst_6 : NormalSpace X
r : ENNReal
hr : r < (μ : (a : Set X) → ENNReal) U
⊢ Ne (α := ENNReal) ((μ : (a : Set X) → ENNReal) U : ENNReal) (⊤ : ENNReal)

Tactic:
simp