awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
hx :
  Membership.mem (γ := Set α)
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
        (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1))))))
    (f x)
⊢ Subset (α := Set α)
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1)))))
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] {y₀} ∪
      closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
        (image (α := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (range (denseSeq (↑s : Type u_1)))))

Tactic:
exact
    Subset.trans (image_closure_subset_closure_image continuous_subtype_val)
      subset_union_right

Premises used: continuous_subtype_val, Set.Subset.trans, Set.subset_union_right, image_closure_subset_closure_image
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
m n : ℕ
h : m ≤ n
dsimp :
  edist
      ((nearestPt
            (fun (k : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ α) y₀ (fun (n : ℕ) (n_ih : α) ↦ (↑(denseSeq (↑s : Type u_1) n) : α)) k)
            n :
          (a : α) → α)
        (f x))
      (f x) ≤
    edist
      ((nearestPt
            (fun (k : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ α) y₀ (fun (n : ℕ) (n_ih : α) ↦ (↑(denseSeq (↑s : Type u_1) n) : α)) k)
            m :
          (a : α) → α)
        (f x))
      (f x)
⊢ edist ((approxOn f hf s y₀ h₀ n : (a : β) → α) x) (f x) ≤ edist ((approxOn f hf s y₀ h₀ m : (a : β) → α) x) (f x)

Tactic:
dsimp only [approxOn, coe_comp, Function.comp_def]

Premises used: Function.comp_def, MeasureTheory.SimpleFunc.coe_comp, MeasureTheory.SimpleFunc.approxOn
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
m n : ℕ
h : m ≤ n
⊢ edist
      ((nearestPt
            (fun (k : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ α) y₀ (fun (n : ℕ) (n_ih : α) ↦ (↑(denseSeq (↑s : Type u_1) n) : α)) k)
            n :
          (a : α) → α)
        (f x))
      (f x) ≤
    edist
      ((nearestPt
            (fun (k : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ α) y₀ (fun (n : ℕ) (n_ih : α) ↦ (↑(denseSeq (↑s : Type u_1) n) : α)) k)
            m :
          (a : α) → α)
        (f x))
      (f x)

Tactic:
edist_nearestPt_le _ _ ((nearestPtInd_le _ _ _).trans h)

Premises used: MeasureTheory.SimpleFunc.nearestPtInd_le, LE.le.trans, MeasureTheory.SimpleFunc.edist_nearestPt_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
m n : ℕ
h : m ≤ n
⊢ edist
      ((nearestPt
            (fun (k : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ α) y₀ (fun (n : ℕ) (n_ih : α) ↦ (↑(denseSeq (↑s : Type u_1) n) : α)) k)
            n :
          (a : α) → α)
        (f x))
      (f x) ≤
    edist
      ((nearestPt
            (fun (k : ℕ) ↦
              Nat.rec (motive := fun (x : ℕ) ↦ α) y₀ (fun (n : ℕ) (n_ih : α) ↦ (↑(denseSeq (↑s : Type u_1) n) : α)) k)
            m :
          (a : α) → α)
        (f x))
      (f x)

Tactic:
exact edist_nearestPt_le _ _ ((nearestPtInd_le _ _ _).trans h)

Premises used: MeasureTheory.SimpleFunc.nearestPtInd_le, LE.le.trans, MeasureTheory.SimpleFunc.edist_nearestPt_le
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
n : ℕ
⊢ edist ((approxOn f hf s y₀ h₀ n : (a : β) → α) x) (f x) ≤ edist y₀ (f x)

Tactic:
edist_approxOn_mono hf h₀ x zero_le

Premises used: zero_le, MeasureTheory.SimpleFunc.edist_approxOn_mono
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
s : Set α
y₀ : α
h₀ : y₀ ∈ s
inst_4 : SeparableSpace.{u_1} (↑s : Type u_1)
x : β
n : ℕ
grw grw₁ : edist y₀ (f x) + edist y₀ (f x) ≤ edist y₀ (f x) + edist y₀ (f x)
⊢ edist y₀ (f x) + edist ((approxOn f hf s y₀ h₀ n : (a : β) → α) x) (f x) ≤ edist y₀ (f x) + edist y₀ (f x)

Tactic:
grw [edist_approxOn_le hf h₀ x n]

Premises used: MeasureTheory.SimpleFunc.edist_approxOn_le
-- 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
he :
  ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ ∅ ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
hmono :
  ∀ ⦃s t : Set (X × Y)⦄,
    s ⊆ t →
      (∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
          MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε) →
        ∃ (g : SimpleFunc (X × Y) α) (s_1 : Set (X × Y)),
          MeasurableSet s_1 ∧ s ⊆ s_1 ∧ ∀ x ∈ s_1, dist (f x) ((g : (a : X × Y) → α) x) < ε
hunion :
  ∀ ⦃s t : Set (X × Y)⦄,
    (∃ (g : SimpleFunc (X × Y) α) (s_1 : Set (X × Y)),
        MeasurableSet s_1 ∧ s ⊆ s_1 ∧ ∀ x ∈ s_1, dist (f x) ((g : (a : X × Y) → α) x) < ε) →
      (∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
          MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε) →
        ∃ (g : SimpleFunc (X × Y) α) (s_1 : Set (X × Y)),
          MeasurableSet s_1 ∧ s ∪ t ⊆ s_1 ∧ ∀ x ∈ s_1, dist (f x) ((g : (a : X × Y) → α) x) < ε
hnhds :
  ∀ x ∈ K,
    ∃ t ∈ 𝓝[K] x,
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
⊢ ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
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

Premises used: IsCompact.induction_on
-- 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
⊢ MeasurableSet (α := X × Y) ∅ ∧
    Subset (α := Set (X × Y)) ∅ ∅ ∧
      ∀ (x : X × Y), Membership.mem (γ := Set (X × Y)) ∅ x → dist (f x) ((0 : (a : X × Y) → α) x) < ε

Tactic:
simp
-- 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
⊢ ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ ∅ ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
exact ⟨0, ∅, by simp⟩
-- 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
t t' : Set (X × Y)
htt' : t ⊆ t'
hmono :
  ∀ (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)),
      MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
⊢ (∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
      MeasurableSet s ∧ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε) →
    ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
      MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
⟨g, s, s_meas, ts, hg⟩
-- 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
t t' : Set (X × Y)
htt' : t ⊆ t'
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)),
    MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
⟨g, s, s_meas, htt'.trans ts, hg⟩

Premises used: HasSubset.Subset.trans, 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
t t' : Set (X × Y)
htt' : t ⊆ t'
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)),
    MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
exact ⟨g, s, s_meas, htt'.trans ts, hg⟩
-- 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
t t' : Set (X × Y)
hunion :
  ∀ (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)),
        MeasurableSet s ∧ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε) →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ t ∪ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
⊢ (∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
      MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε) →
    (∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε) →
      ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
        MeasurableSet s ∧ t ∪ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
⟨g, s, s_meas, ts, hg⟩
-- 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
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) < ε
hunion :
  ∀ (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) < ε),
    ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
      MeasurableSet s ∧ t ∪ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
⊢ (∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
      MeasurableSet s ∧ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε) →
    ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
      MeasurableSet s ∧ t ∪ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
⟨g', s', s'_meas, t's', hg'⟩
-- 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
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) < ε
⊢ ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ t ∪ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
⟨g.piecewise s s_meas g', s ∪ s', s_meas.union s'_meas,
        union_subset_union ts t's', fun p hp ↦ ?_⟩

Premises used: Set.union_subset_union, And.intro, MeasurableSet.union, Exists.intro, Union.union, 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 < ε
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) < ε
hunion : ∀ (p : X × Y) (hp : p ∈ s ∪ s'), dist (f p) ((SimpleFunc.piecewise s s_meas g g' : (a : X × Y) → α) p) < ε
⊢ ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ t ∪ t' ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε

Tactic:
refine ⟨g.piecewise s s_meas g', s ∪ s', s_meas.union s'_meas,
        union_subset_union ts t's', fun p hp ↦ ?_⟩
-- 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
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) < ε
neg : ∀ (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) < ε

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 < ε
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) < ε

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 < ε
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
neg : dist (f p) ((g' : (a : X × Y) → α) p) < ε
⊢ dist (f p) ((SimpleFunc.piecewise s s_meas g g' : (a : X × Y) → α) p) < ε

Tactic:
simp only [SimpleFunc.piecewise_apply, H, ite_false]

Premises used: MeasureTheory.SimpleFunc.piecewise_apply, ite_false
-- 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
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
neg : p ∈ s'
⊢ dist (f p) ((g' : (a : X × Y) → α) p) < ε

Tactic:
apply hg'
-- 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
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
⊢ p ∈ s'

Tactic:
simpa [H] using (mem_union _ _ _).1 hp

Premises used: Set.mem_union, Iff.mp
-- 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),
    IsOpen[inst_1] u ∧ x ∈ u ∧ IsOpen[inst_2] v ∧ y ∈ v ∧ u ×ˢ v ⊆ {z : X × Y | dist (f z) (f (x, y)) < ε}

Tactic:
mem_nhds_prod_iff'.1 <| Metric.continuousAt_iff'.1 hf.continuousAt ε hε

Premises used: mem_nhds_prod_iff', Metric.continuousAt_iff', Continuous.continuousAt, Iff.mp
-- 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
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) < ε
⊢ ∃ 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ε

Premises used: mem_nhds_prod_iff', Metric.continuousAt_iff', Continuous.continuousAt, Iff.mp