awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
x : X
y : Y
u : Set X
v : Set Y
hu : IsOpen[inst_1] u
xu : x ∈ u
hv : IsOpen[inst_2] v
yv : y ∈ v
huv : u ×ˢ v ⊆ {z : X × Y | dist (f z) (f (x, y)) < ε}
⊢ ∃ t ∈ 𝓝[K] (x, y),
    ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
      MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
⟨u ×ˢ v, nhdsWithin_le_nhds <| (hu.prod hv).mem_nhds (mk_mem_prod xu yv), ?_⟩

Premises used: SProd.sprod, nhdsWithin_le_nhds, And.intro, IsOpen.mem_nhds, Exists.intro, Set.mk_mem_prod, IsOpen.prod
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
x : X
y : Y
u : Set X
v : Set Y
hu : IsOpen[inst_1] u
xu : x ∈ u
hv : IsOpen[inst_2] v
yv : y ∈ v
huv : u ×ˢ v ⊆ {z : X × Y | dist (f z) (f (x, y)) < ε}
hnhds :
  ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ u ×ˢ v ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
⊢ ∃ t ∈ 𝓝[K] (x, y),
    ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
      MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
refine ⟨u ×ˢ v, nhdsWithin_le_nhds <| (hu.prod hv).mem_nhds (mk_mem_prod xu yv), ?_⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
x : X
y : Y
u : Set X
v : Set Y
hu : IsOpen[inst_1] u
xu : x ∈ u
hv : IsOpen[inst_2] v
yv : y ∈ v
huv : u ×ˢ v ⊆ {z : X × Y | dist (f z) (f (x, y)) < ε}
⊢ ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ u ×ˢ v ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
⟨SimpleFunc.const _ (f (x, y)), u ×ˢ v, hu.measurableSet.prod hv.measurableSet,
        Subset.rfl, fun z hz ↦ huv hz⟩

Premises used: MeasureTheory.SimpleFunc.const, SProd.sprod, IsOpen.measurableSet, MeasurableSet.prod, Prod.mk, Set.Subset.rfl, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
K : Set (X × Y)
hK : IsCompact K
x : X
y : Y
u : Set X
v : Set Y
hu : IsOpen[inst_1] u
xu : x ∈ u
hv : IsOpen[inst_2] v
yv : y ∈ v
huv : u ×ˢ v ⊆ {z : X × Y | dist (f z) (f (x, y)) < ε}
⊢ ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ u ×ˢ v ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
exact ⟨SimpleFunc.const _ (f (x, y)), u ×ˢ v, hu.measurableSet.prod hv.measurableSet,
        Subset.rfl, fun z hz ↦ huv hz⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
⊢ ∀ (K : Set (X × Y)),
    IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
have M : ∀ (K : Set (X × Y)), IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α), ∃ (s : Set (X × Y)), MeasurableSet s ∧ K ⊆ s ∧
      ∀ x ∈ s, dist (f x) (g x) < ε := by
    intro K hK
    apply IsCompact.induction_on
      (p := fun t ↦ ∃ (g : SimpleFunc (X × Y) α), ∃ (s : Set (X × Y)), MeasurableSet s ∧ t ⊆ s ∧
        ∀ x ∈ s, dist (f x) (g x) < ε) hK
    · exact ⟨0, ∅, by simp⟩
    · intro t t' htt' ⟨g, s, s_meas, ts, hg⟩
      exact ⟨g, s, s_meas, htt'.trans ts, hg⟩
    · intro t t' ⟨g, s, s_meas, ts, hg⟩ ⟨g', s', s'_meas, t's', hg'⟩
      refine ⟨g.piecewise s s_meas g', s ∪ s', s_meas.union s'_meas,
        union_subset_union ts t's', fun p hp ↦ ?_⟩
      by_cases H : p ∈ s
      · simpa [H, SimpleFunc.piecewise_apply] using hg p H
      · simp only [SimpleFunc.piecewise_apply, H, ite_false]
        apply hg'
        simpa [H] using (mem_union _ _ _).1 hp
    · rintro ⟨x, y⟩ -
      obtain ⟨u, v, hu, xu, hv, yv, huv⟩ : ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧
        u ×ˢ v ⊆ {z | dist (f z) (f (x, y)) < ε} :=
          mem_nhds_prod_iff'.1 <| Metric.continuousAt_iff'.1 hf.continuousAt ε hε
      refine ⟨u ×ˢ v, nhdsWithin_le_nhds <| (hu.prod hv).mem_nhds (mk_mem_prod xu yv), ?_⟩
      exact ⟨SimpleFunc.const _ (f (x, y)), u ×ˢ v, hu.measurableSet.prod hv.measurableSet,
        Subset.rfl, fun z hz ↦ huv hz⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M :
  ∀ (K : Set (X × Y)),
    IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
⊢ ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ tsupport f ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
M _ h'f
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M :
  ∀ (K : Set (X × Y)),
    IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
obtain :
  ∀ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)) (s_meas : MeasurableSet s) (fs : tsupport f ⊆ s)
    (hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε),
    ∃ (g : SimpleFunc (X × Y) α), ∀ (x : X × Y), dist (f x) ((g : (a : X × Y) → α) x) < ε
⊢ ∃ (g : SimpleFunc (X × Y) α), ∀ (x : X × Y), dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
obtain ⟨g, s, s_meas, fs, hg⟩ : ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ tsupport f ⊆ s ∧ ∀ (x : X × Y), x ∈ s → dist (f x) (g x) < ε := M _ h'f

Premises used: MeasureTheory.SimpleFunc, tsupport, Prod, Set
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M :
  ∀ (K : Set (X × Y)),
    IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
⊢ ∃ (g : SimpleFunc (X × Y) α), ∀ (x : X × Y), dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
⟨g.piecewise s s_meas 0, fun p ↦ ?_⟩

Premises used: Exists.intro, OfNat.ofNat, MeasureTheory.SimpleFunc.piecewise
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M :
  ∀ (K : Set (X × Y)),
    IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
refine : ∀ (p : X × Y), dist (f p) ((SimpleFunc.piecewise s s_meas g 0 : (a : X × Y) → α) p) < ε
⊢ ∃ (g : SimpleFunc (X × Y) α), ∀ (x : X × Y), dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
refine ⟨g.piecewise s s_meas 0, fun p ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M :
  ∀ (K : Set (X × Y)),
    IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
p : X × Y
pos : ∀ (H : p ∈ s), dist (f p) ((SimpleFunc.piecewise s s_meas g 0 : (a : X × Y) → α) p) < ε
neg : ∀ (H : p ∉ s), dist (f p) ((SimpleFunc.piecewise s s_meas g 0 : (a : X × Y) → α) p) < ε
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0 : (a : X × Y) → α) p) < ε

Tactic:
by_cases H : p ∈ s
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M :
  ∀ (K : Set (X × Y)),
    IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
p : X × Y
H : p ∈ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0 : (a : X × Y) → α) p) < ε

Tactic:
simpa [H, SimpleFunc.piecewise_apply] using hg p H

Premises used: MeasureTheory.SimpleFunc.piecewise_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M :
  ∀ (K : Set (X × Y)),
    IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
p : X × Y
H : p ∉ s
contrapose! : ∀ (H : f p ≠ 0), p ∈ s
⊢ f p = 0

Tactic:
contrapose! H
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M :
  ∀ (K : Set (X × Y)),
    IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
p : X × Y
H : f p ≠ 0
⊢ p ∈ support f

Tactic:
rw [← Function.mem_support] at H

Premises used: Function.mem_support
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M :
  ∀ (K : Set (X × Y)),
    IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
p : X × Y
H : p ∈ support f
⊢ p ∈ s

Tactic:
fs (subset_tsupport _ H)

Premises used: subset_tsupport
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M :
  ∀ (K : Set (X × Y)),
    IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
p : X × Y
H : p ∈ support f
⊢ p ∈ s

Tactic:
exact fs (subset_tsupport _ H)

Premises used: subset_tsupport
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M :
  ∀ (K : Set (X × Y)),
    IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
p : X × Y
H : p ∉ s
⊢ f p = 0

Tactic:
have : f p = 0 := by
      contrapose! H
      rw [← Function.mem_support] at H
      exact fs (subset_tsupport _ H)
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : PseudoMetricSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
h'f : HasCompactSupport f
ε : ℝ
hε : 0 < ε
M :
  ∀ (K : Set (X × Y)),
    IsCompact K →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
fs : tsupport f ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
p : X × Y
H : p ∉ s
this : f p = 0
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0 : (a : X × Y) → α) p) < ε

Tactic:
simp [SimpleFunc.piecewise_apply, H, this, hε]

Premises used: MeasureTheory.SimpleFunc.piecewise_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
inst_9 : MeasurableSpace α
inst_10 : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
⊢ ∃ (u : ℕ → ℝ), StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0)

Tactic:
exists_seq_strictAnti_tendsto (0 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
inst_9 : MeasurableSpace α
inst_10 : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
obtain : ∀ (u : ℕ → ℝ) (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)), Measurable f
⊢ Measurable f

Tactic:
obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
inst_9 : MeasurableSpace α
inst_10 : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
⊢ ∀ (n : ℕ), ∃ (g : SimpleFunc (X × Y) α), ∀ (x : X × Y), dist (f x) ((g : (a : X × Y) → α) x) < u n

Tactic:
have : ∀ n, ∃ (g : SimpleFunc (X × Y) α), ∀ x, dist (f x) (g x) < u n :=
    fun n ↦ h'f.exists_simpleFunc_approx_of_prod hf (u_pos n)
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
inst_9 : MeasurableSpace α
inst_10 : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this_1 : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
this : ∀ (n : ℕ), ∃ (g : SimpleFunc (X × Y) α), ∀ (x : X × Y), dist (f x) ((g : (a : X × Y) → α) x) < u n
choose :
  ∀ (g : (n : ℕ) → SimpleFunc (X × Y) α) (hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n : (a : X × Y) → α) x) < u n),
    Measurable f
⊢ Measurable f

Tactic:
choose g hg using this
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
inst_9 : MeasurableSpace α
inst_10 : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : (n : ℕ) → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n : (a : X × Y) → α) x) < u n
x : X × Y
rw : Tendsto (β := ℝ) (fun (b : ℕ) ↦ dist ((g b : (a : X × Y) → α) x) (f x)) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ (g n : (a : X × Y) → α) x) atTop (𝓝 (f x))

Tactic:
rw [tendsto_iff_dist_tendsto_zero]

Premises used: tendsto_iff_dist_tendsto_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
inst_9 : MeasurableSpace α
inst_10 : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : (n : ℕ) → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n : (a : X × Y) → α) x) < u n
x : X × Y
apply : ∀ (n : ℕ), dist ((g n : (a : X × Y) → α) x) (f x) ≤ u n
⊢ Tendsto (β := ℝ) (fun (b : ℕ) ↦ dist ((g b : (a : X × Y) → α) x) (f x)) atTop (𝓝 0)

Tactic:
apply squeeze_zero (fun n ↦ dist_nonneg) (fun n ↦ ?_) u_lim

Premises used: squeeze_zero, dist_nonneg
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
X : Type u_3
Y : Type u_4
α : Type u_5
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
inst_9 : MeasurableSpace α
inst_10 : BorelSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
g : (n : ℕ) → SimpleFunc (X × Y) α
hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n : (a : X × Y) → α) x) < u n
x : X × Y
n : ℕ
rw : dist (f x) ((g n : (a : X × Y) → α) x) ≤ u n
⊢ dist ((g n : (a : X × Y) → α) x) (f x) ≤ u n

Tactic:
rw [dist_comm]

Premises used: dist_comm