awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g' : SimpleFunc (X × Y) α
s' : Set (X × Y)
s'_meas : MeasurableSet s'
t's' : t' ⊆ s'
hg' : ∀ x ∈ s', dist (f x) ((g' : (a : X × Y) → α) x) < ε
p : X × Y
hp : p ∈ s ∪ s'
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g g' : (a : X × Y) → α) p) < ε
have pos : ∀ (H : p ∈ s), dist (f p) ((SimpleFunc.piecewise s s_meas g g' : (a : X × Y) → α) p) < ε
Tactic: by_cases H : p ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g' : SimpleFunc (X × Y) α
s' : Set (X × Y)
s'_meas : MeasurableSet s'
t's' : t' ⊆ s'
hg' : ∀ x ∈ s', dist (f x) ((g' : (a : X × Y) → α) x) < ε
p : X × Y
hp : p ∈ s ∪ s'
pos : ∀ (H : p ∈ s), dist (f p) ((SimpleFunc.piecewise s s_meas g g' : (a : X × Y) → α) p) < ε
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g g' : (a : X × Y) → α) p) < ε
have neg : ∀ (H : p ∉ s), dist (f p) ((SimpleFunc.piecewise s s_meas g g' : (a : X × Y) → α) p) < ε
Tactic: by_cases H : p ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g' : SimpleFunc (X × Y) α
s' : Set (X × Y)
s'_meas : MeasurableSet s'
t's' : t' ⊆ s'
hg' : ∀ x ∈ s', dist (f x) ((g' : (a : X × Y) → α) x) < ε
p : X × Y
hp : p ∈ s ∪ s'
H : p ∉ s
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g g' : (a : X × Y) → α) p) < ε
have neg : dist (f p) ((g' : (a : X × Y) → α) p) < ε
Tactic: simp only [SimpleFunc.piecewise_apply, H, ite_false]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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
t t' : Set (X × Y)
g : SimpleFunc (X × Y) α
s : Set (X × Y)
s_meas : MeasurableSet s
ts : t ⊆ s
hg : ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
g' : SimpleFunc (X × Y) α
s' : Set (X × Y)
s'_meas : MeasurableSet s'
t's' : t' ⊆ s'
hg' : ∀ x ∈ s', dist (f x) ((g' : (a : X × Y) → α) x) < ε
p : X × Y
hp : p ∈ s ∪ s'
H : p ∉ s
⊢ dist (f p) ((g' : (a : X × Y) → α) p) < ε
have neg : p ∈ s'
Tactic: apply hg'
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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
⊢ ∃ 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) < ε
have hnhds : ∀ (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: 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ε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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) < ε
have hnhds : ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
  MeasurableSet s ∧ u ×ˢ v ⊆ 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), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (hypothesis)
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 < ε
⊢ ∃ (g : SimpleFunc (X × Y) α), ∀ (x : X × Y), dist (f x) ((g : (a : X × Y) → α) x) < ε
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 : (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⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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) α), ∀ (x : X × Y), dist (f x) ((g : (a : X × Y) → α) x) < ε
have 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) < ε
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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) < ε
have refine : ∀ (p : X × Y), dist (f p) ((SimpleFunc.piecewise s s_meas g 0 : (a : X × Y) → α) p) < ε
Tactic: refine ⟨g.piecewise s s_meas 0, fun p ↦ ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0 : (a : X × Y) → α) p) < ε
have pos : ∀ (H : p ∈ s), dist (f p) ((SimpleFunc.piecewise s s_meas g 0 : (a : X × Y) → α) p) < ε
Tactic: by_cases H : p ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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) < ε
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g 0 : (a : X × Y) → α) p) < ε
have neg : ∀ (H : p ∉ s), dist (f p) ((SimpleFunc.piecewise s s_meas g 0 : (a : X × Y) → α) p) < ε
Tactic: by_cases H : p ∈ s
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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
have contrapose! : ∀ (H : f p ≠ 0), p ∈ s
Tactic: contrapose! H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (hypothesis)
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 ∈ s
have H₁ : p ∈ support f
Tactic: rw [← Function.mem_support] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (hypothesis)
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) < ε
have this : f p = 0
Tactic: have : f p = 0 := by
      contrapose! H
      rw [← Function.mem_support] at H
      exact fs (subset_tsupport _ H)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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 α
⊢ Measurable f
have obtain : ∀ (u : ℕ → ℝ) (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)), 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 : ℝ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (hypothesis)
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)
⊢ Measurable f
have this₁ : ∀ (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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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
⊢ Measurable f
have choose : ∀ (g : (n : ℕ) → SimpleFunc (X × Y) α) (hg : ∀ (n : ℕ) (x : X × Y), dist (f x) ((g n : (a : X × Y) → α) x) < u n),
  Measurable f
Tactic: choose g hg using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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
⊢ Tendsto (fun (n : ℕ) ↦ (g n : (a : X × Y) → α) x) atTop (𝓝 (f x))
have rw : Tendsto (β := ℝ) (fun (b : ℕ) ↦ dist ((g b : (a : X × Y) → α) x) (f x)) atTop (𝓝 0)
Tactic: rw [tendsto_iff_dist_tendsto_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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
⊢ Tendsto (β := ℝ) (fun (b : ℕ) ↦ dist ((g b : (a : X × Y) → α) x) (f x)) atTop (𝓝 0)
have apply : ∀ (n : ℕ), dist ((g n : (a : X × Y) → α) x) (f x) ≤ u n
Tactic: apply squeeze_zero (fun n ↦ dist_nonneg) (fun n ↦ ?_) u_lim
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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 : ℕ
⊢ dist ((g n : (a : X × Y) → α) x) (f x) ≤ u n
have rw : dist (f x) ((g n : (a : X × Y) → α) x) ≤ u n
Tactic: rw [dist_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (hypothesis)
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
⊢ Measurable f
have A : ∀ (x : X × Y), Tendsto (fun (n : ℕ) ↦ (g n : (a : X × Y) → α) x) atTop (𝓝 (f x))
Tactic: have A : ∀ x, Tendsto (fun n ↦ g n x) atTop (𝓝 (f x)) := by
    intro x
    rw [tendsto_iff_dist_tendsto_zero]
    apply squeeze_zero (fun n ↦ dist_nonneg) (fun n ↦ ?_) u_lim
    rw [dist_comm]
    exact (hg n x).le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
x : β
n : ℕ
⊢ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖₊ ≤ ‖f x - y₀‖₊
have this : edist ((approxOn f hf s y₀ h₀ n : (a : β) → E) x) (f x) ≤ edist y₀ (f x)
Tactic: have := edist_approxOn_le hf h₀ x n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDenseLp (hypothesis)
Goal:
β : Type u_2
E : Type u_4
inst : MeasurableSpace β
inst_1 : MeasurableSpace E
inst_2 : NormedAddCommGroup E
inst_3 : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_4} (↑s : Type u_4)
x : β
n : ℕ
this : edist ((approxOn f hf s y₀ h₀ n : (a : β) → E) x) (f x) ≤ edist y₀ (f x)
⊢ ‖HSub.hSub (α := E) ((approxOn f hf s y₀ h₀ n : (a : β) → E) x : E) (f x)‖₊ ≤ ‖f x - y₀‖₊
have this₁ : edist ((approxOn f hf s y₀ h₀ n : (a : β) → E) x) (f x) ≤ edist (f x) y₀
Tactic: rw [edist_comm y₀] at this
Cleared hypotheses: this