awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
k N : ℕ
hk : k ≤ N
zero : ∀ {k : ℕ} (hk : k ≤ 0), edist ((nearestPt e 0 : (a : α) → α) x) x ≤ edist (e k) x
⊢ edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
have succ : ∀ (N : ℕ) (ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x) {k : ℕ}
  (hk : k ≤ N + 1), edist ((nearestPt e (N + 1) : (a : α) → α) x) x ≤ edist (e k) x
Tactic: induction N generalizing k with
  | zero => simp [nonpos_iff_eq_zero.1 hk]
  | succ N ihN =>
    simp only [nearestPt, nearestPtInd_succ, map_apply]
    split_ifs with h
    · rcases hk.eq_or_lt with (rfl | hk)
      exacts [le_rfl, (h k (Nat.lt_succ_iff.1 hk)).le]
    · push Not at h
      rcases h with ⟨l, hlN, hxl⟩
      rcases hk.eq_or_lt with (rfl | hk)
      exacts [(ihN hlN).trans hxl, ihN (Nat.lt_succ_iff.1 hk)]
Cleared hypotheses: k, N, hk
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
⊢ Tendsto (fun (N : ℕ) ↦ (nearestPt e N : (a : α) → α) x) atTop (𝓝 x)
have refine : ∀ (ε : ℝ≥0∞) (hε : 0 < ε),
  ∃ (ia : ℕ), True ∧ ∀ x_1 ∈ Ici ia, Membership.mem (α := α) (eball x ε) ((nearestPt e x_1 : (a : α) → α) x : α)
Tactic: refine (atTop_basis.tendsto_iff nhds_basis_eball).2 fun ε hε => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ (ia : ℕ), True ∧ ∀ x_1 ∈ Ici ia, Membership.mem (α := α) (eball x ε) ((nearestPt e x_1 : (a : α) → α) x : α)
have rcases : ∀ (N : ℕ) (hN : edist x (e N) < ε),
  ∃ (ia : ℕ), True ∧ ∀ x_1 ∈ Ici ia, Membership.mem (α := α) (eball x ε) ((nearestPt e x_1 : (a : α) → α) x : α)
Tactic: rcases EMetric.mem_closure_iff.1 hx ε hε with ⟨_, ⟨N, rfl⟩, hN⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
hx : x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] (range e)
ε : ℝ≥0∞
hε : 0 < ε
N : ℕ
hN : edist x (e N) < ε
⊢ ∃ (ia : ℕ), True ∧ ∀ x_1 ∈ Ici ia, Membership.mem (α := α) (eball x ε) ((nearestPt e x_1 : (a : α) → α) x : α)
have hN₁ : edist (e N) x < ε
Tactic: rw [edist_comm] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (hypothesis)
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)
n : ℕ
x : β
⊢ Membership.mem (α := α) s ((approxOn f hf s y₀ h₀ n : (a : β) → α) x : α)
have this : Nonempty.{u_1 + 1} (↑s : Type u_1)
Tactic: haveI : Nonempty s := ⟨⟨y₀, h₀⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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)
n : ℕ
x : β
this : Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ Membership.mem (α := α) s ((approxOn f hf s y₀ h₀ n : (a : β) → α) x : α)
have suffices : ∀ (n : ℕ),
  Membership.mem (α := α) s
    (Nat.casesOn (motive := fun (x : ℕ) ↦ α) n y₀
        (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (denseSeq (↑s : Type u_1))) :
      α)
Tactic: suffices ∀ n, (Nat.casesOn n y₀ ((↑) ∘ denseSeq s) : α) ∈ s by apply this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : Zero α
inst_5 : Preorder α
f : β → α
hf : 0 ≤ f
hfm : Measurable f
inst_6 : SeparableSpace.{u_1} (↑(range f ∪ {0}) : Type u_1)
n : ℕ
⊢ range f ∪ {0} ⊆ Ici 0
have simp : range f ⊆ Ici 0
Tactic: simp only [Set.union_singleton, Set.insert_subset_iff, Set.mem_Ici, le_refl, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : Zero α
inst_5 : Preorder α
f : β → α
hf : 0 ≤ f
hfm : Measurable f
inst_6 : SeparableSpace.{u_1} (↑(range f ∪ {0}) : Type u_1)
n : ℕ
⊢ 0 ≤ approxOn f hfm (range f ∪ {0}) 0 ⋯ n
have this : range f ∪ {0} ⊆ Ici 0
Tactic: have : range f ∪ {0} ⊆ Set.Ici 0 := by
    simp only [Set.union_singleton, Set.insert_subset_iff, Set.mem_Ici, le_refl, true_and]
    rintro - ⟨x, rfl⟩
    exact hf x
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (hypothesis)
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 : β
hx : f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Tendsto (fun (n : ℕ) ↦ (approxOn f hf s y₀ h₀ n : (a : β) → α) x) atTop (𝓝 (f x))
have this : Nonempty.{u_1 + 1} (↑s : Type u_1)
Tactic: haveI : Nonempty s := ⟨⟨y₀, h₀⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (hypothesis)
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 : β
hx : f x ∈ closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace] s
this this₁ : Nonempty.{u_1 + 1} (↑s : Type u_1)
⊢ Tendsto (fun (n : ℕ) ↦ (approxOn f hf s y₀ h₀ n : (a : β) → α) x) atTop (𝓝 (f x))
have 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)
Tactic: rw [← @Subtype.range_coe _ s, ← image_univ, ← (denseRange_denseSeq s).closure_eq] at hx
Cleared hypotheses: hx, this
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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)
⊢ Tendsto (fun (n : ℕ) ↦ (approxOn f hf s y₀ h₀ n : (a : β) → α) x) atTop (𝓝 (f x))
have simp : Tendsto
  (fun (n : ℕ) ↦
    ((⇑(nearestPt
              (fun (k : ℕ) ↦
                Nat.casesOn (motive := fun (x : ℕ) ↦ α) k y₀
                  (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
                    (denseSeq (↑s : Type u_1))))
              n) :
          (a : α) → α) ∘
        f)
      x)
  atTop (𝓝 (f x))
Tactic: simp -iota only [approxOn, coe_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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)
⊢ Tendsto
    (fun (n : ℕ) ↦
      ((⇑(nearestPt
                (fun (k : ℕ) ↦
                  Nat.casesOn (motive := fun (x : ℕ) ↦ α) k y₀
                    (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
                      (denseSeq (↑s : Type u_1))))
                n) :
            (a : α) → α) ∘
          f)
        x)
    atTop (𝓝 (f x))
have refine : Subset.{u_1} (α := Set α)
  (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
    (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1)))))
  (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
    (range fun (k : ℕ) ↦
      Nat.casesOn (motive := fun (x : ℕ) ↦ α) k y₀
        (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (denseSeq (↑s : Type u_1)))))
Tactic: refine tendsto_nearestPt (closure_minimal ?_ isClosed_closure hx)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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.{u_1} (α := Set α)
    (image (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (closure[instTopologicalSpaceSubtype] (range (denseSeq (↑s : Type u_1)))))
    (closure[PseudoEMetricSpace.toUniformSpace.toTopologicalSpace]
      (range fun (k : ℕ) ↦
        Nat.casesOn (motive := fun (x : ℕ) ↦ α) k y₀
          (Function.comp (β := (↑s : Type u_1)) (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (denseSeq (↑s : Type u_1)))))
have simp : 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: simp -iota only [Nat.range_casesOn, closure_union, range_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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 ((approxOn f hf s y₀ h₀ n : (a : β) → α) x) (f x) ≤ edist ((approxOn f hf s y₀ h₀ m : (a : β) → α) x) (f x)
have 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)
Tactic: dsimp only [approxOn, coe_comp, Function.comp_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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 y₀ (f x) + edist ((approxOn f hf s y₀ h₀ n : (a : β) → α) x) (f x) ≤ edist y₀ (f x) + edist y₀ (f x)
have grw : edist y₀ (f x) + edist y₀ (f x) ≤ edist y₀ (f x) + edist y₀ (f x)
Tactic: grw [edist_approxOn_le hf h₀ x 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 : 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 ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
have he : ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
  MeasurableSet s ∧ ∅ ⊆ 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
-- 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
he :
  ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ ∅ ⊆ 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) < ε
have 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) < ε
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
-- 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
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) < ε
⊢ ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
have 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) < ε
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
-- 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
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) < ε
⊢ ∃ (g : SimpleFunc (X × Y) α) (s : Set (X × Y)),
    MeasurableSet s ∧ K ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
have 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) < ε
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
-- 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)
htt' : t ⊆ 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 : Set (X × Y)),
      MeasurableSet s ∧ t ⊆ s ∧ ∀ x ∈ s, dist (f x) ((g : (a : X × Y) → α) x) < ε
have 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) < ε
Tactic: ⟨g, s, s_meas, ts, 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
t t' : Set (X × Y)
⊢ (∃ (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) < ε
have 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) < ε
Tactic: ⟨g, s, s_meas, ts, 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
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)),
      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) < ε
have 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) < ε
Tactic: ⟨g', s', s'_meas, t's', 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
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) < ε
have hunion : ∀ (p : X × Y) (hp : p ∈ s ∪ s'), dist (f p) ((SimpleFunc.piecewise s s_meas g g' : (a : X × Y) → α) p) < ε
Tactic: refine ⟨g.piecewise s s_meas g', s ∪ s', s_meas.union s'_meas,
        union_subset_union ts t's', fun p hp ↦ ?_⟩