awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
c : γ := Classical.ofNonempty
x : γ
s : Finset γ
hxs : x ∉ s
ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f
f : α →ₛ γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑(insert x s) : Set γ)
mx : MeasurableSet.{u_5} (α := α) (preimage (β := γ) (⇑f : (a : α) → γ) {x})
g : α →ₛ γ := piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x}) mx (SimpleFunc.const α c) f
Pg : P g
y : α
hy : y ∉ preimage (β := γ) (⇑f : (a : α) → γ) {x}
⊢ Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
    ((piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ ⋯ g (SimpleFunc.const α x) : (a : α) → γ) y : γ)

Tactic:
simp [g, hy]
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
f : α →ₛ γ
c : γ := Classical.ofNonempty
s : Finset γ
h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)
empty : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑∅ : Set γ)), P f
insert :
  ∀ (x : γ) (s : Finset γ) (hxs : x ∉ s)
    (ih : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f) (f : α →ₛ γ)
    (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑(Insert.insert x s) : Set γ)), P f
⊢ P f

Tactic:
induction s using Finset.induction generalizing f with
  | empty =>
    rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h
    convert! const c
    ext x
    simp [h]
  | insert x s hxs ih =>
    have mx := f.measurableSet_preimage {x}
    let g := SimpleFunc.piecewise (f ⁻¹' {x}) mx (SimpleFunc.const α c) f
    have Pg : P g := by
      apply ih
      simp only [g, SimpleFunc.coe_piecewise, range_piecewise]
      rw [image_compl_preimage, union_diff_distrib, diff_diff_comm, h, Finset.coe_insert,
        insert_diff_self_of_notMem, diff_eq_empty.mpr, Set.empty_union]
      · rw [Set.image_subset_iff]
        convert! Set.subset_univ _
        exact preimage_const_of_mem (mem_singleton _)
      · rwa [Finset.mem_coe]
    convert! pcw mx.compl Pg (const x)
    · ext1 y
      by_cases hy : y ∈ f ⁻¹' {x}
      · simpa [g, hy]
      · simp [g, hy]

Premises used: Finset.coe_empty, Insert.insert, Set.range_subset_singleton, Set.diff_eq_empty
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_5
γ : Type u_6
inst : MeasurableSpace α
inst_1 : Nonempty γ
P : (α →ₛ γ) → Prop
const : ∀ (c : γ), P (SimpleFunc.const α c)
pcw : ∀ ⦃f g : α →ₛ γ⦄ {s : Set α} (hs : MeasurableSet s), P f → P g → P (piecewise s hs f g)
f : α →ₛ γ
c : γ := Classical.ofNonempty
generalize : ∀ (s : Finset γ) (h : f.range \ {c} = s), P f
generalize₁ : ∀ (s : Finset γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), P f
⊢ P f

Tactic:
classical
  generalize h : f.range \ {c} = s
  rw [← Finset.coe_inj, Finset.coe_sdiff, Finset.coe_singleton, SimpleFunc.coe_range] at h
  induction s using Finset.induction generalizing f with
  | empty =>
    rw [Finset.coe_empty, diff_eq_empty, range_subset_singleton] at h
    convert! const c
    ext x
    simp [h]
  | insert x s hxs ih =>
    have mx := f.measurableSet_preimage {x}
    let g := SimpleFunc.piecewise (f ⁻¹' {x}) mx (SimpleFunc.const α c) f
    have Pg : P g := by
      apply ih
      simp only [g, SimpleFunc.coe_piecewise, range_piecewise]
      rw [image_compl_preimage, union_diff_distrib, diff_diff_comm, h, Finset.coe_insert,
        insert_diff_self_of_notMem, diff_eq_empty.mpr, Set.empty_union]
      · rw [Set.image_subset_iff]
        convert! Set.subset_univ _
        exact preimage_const_of_mem (mem_singleton _)
      · rwa [Finset.mem_coe]
    convert! pcw mx.compl Pg (const x)
    · ext1 y
      by_cases hy : y ∈ f ⁻¹' {x}
      · simpa [g, hy]
      · simp [g, hy]

Premises used: MeasureTheory.SimpleFunc.coe_range, Finset.coe_singleton, Finset.coe_empty, Finset.coe_sdiff, Finset.coe_inj, Insert.insert, Set.range_subset_singleton, MeasureTheory.SimpleFunc.range, Set.diff_eq_empty
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
E : Type u_5
x : MeasurableSpace α
inst : MeasurableSpace E
inst_1 : AddCancelMonoid E
inst_2 : MeasurableAdd E
g : α → E
hg : Measurable g
f : α →ₛ E
⊢ Measurable (g + (⇑f : (a : α) → E))

Tactic:
f.measurable_bind (fun b a ↦ g a + b) fun b ↦ hg.add_const b

Premises used: MeasureTheory.SimpleFunc.measurable_bind, Measurable.add_const, HAdd.hAdd
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
E : Type u_5
x : MeasurableSpace α
inst : MeasurableSpace E
inst_1 : AddCancelMonoid E
inst_2 : MeasurableAdd E
g : α → E
hg : Measurable g
f : α →ₛ E
⊢ Measurable ((⇑f : (a : α) → E) + g)

Tactic:
f.measurable_bind (fun b a ↦ b + g a) fun b ↦ hg.const_add b

Premises used: MeasureTheory.SimpleFunc.measurable_bind, Measurable.const_add, HAdd.hAdd
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
mα : MeasurableSpace α
motive : (α → ℝ≥0∞) → Prop
indicator : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun (x : α) ↦ ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ motive fun (x : α) ↦ ⨆ (n : ℕ), ((eapprox f n : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) x

Tactic:
iSup (fun n => (eapprox f n).measurable) (monotone_eapprox f) _

Premises used: MeasureTheory.SimpleFunc.measurable, MeasureTheory.SimpleFunc.eapprox, MeasureTheory.SimpleFunc.monotone_eapprox
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
mα : MeasurableSpace α
motive : (α → ℝ≥0∞) → Prop
indicator : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun (x : α) ↦ ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
h : ∀ (x : α), f x = ⨆ (n : ℕ), ((eapprox f n : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) x
convert! : ∀ (n : ℕ), motive (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
⊢ motive f

Tactic:
convert! iSup (fun n => (eapprox f n).measurable) (monotone_eapprox f) _ using 2

Premises used: MeasureTheory.SimpleFunc.measurable, MeasureTheory.SimpleFunc.eapprox, MeasureTheory.SimpleFunc.monotone_eapprox
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
mα : MeasurableSpace α
motive : (α → ℝ≥0∞) → Prop
indicator : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun (x : α) ↦ ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
x : α
h h₁ : f x = f x
⊢ f x = ⨆ (n : ℕ), ((eapprox f n : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) x

Tactic:
rw [iSup_eapprox_apply hf]

Premises used: MeasureTheory.SimpleFunc.iSup_eapprox_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
mα : MeasurableSpace α
motive : (α → ℝ≥0∞) → Prop
indicator : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun (x : α) ↦ ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), motive (⇑(eapprox f n) : (a : α) → ℝ≥0∞)

Tactic:
fun n =>
      SimpleFunc.induction (fun c s hs => indicator c hs)
        (fun f g hfg hf hg => add hfg f.measurable g.measurable hf hg) (eapprox f n)

Premises used: MeasureTheory.SimpleFunc.induction, MeasureTheory.SimpleFunc.eapprox
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
mα : MeasurableSpace α
motive : (α → ℝ≥0∞) → Prop
indicator : ∀ (c : ℝ≥0∞) ⦃s : Set α⦄, MeasurableSet s → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun (x : α) ↦ ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ ∀ (n : ℕ), motive (⇑(eapprox f n) : (a : α) → ℝ≥0∞)

Tactic:
exact fun n =>
      SimpleFunc.induction (fun c s hs => indicator c hs)
        (fun f g hfg hf hg => add hfg f.measurable g.measurable hf hg) (eapprox f n)
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
motive : (α → ℝ≥0∞) → Prop
indicator :
  ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun (x : α) ↦ ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
⊢ motive f

Tactic:
Measurable.ennreal_induction (fun c s hs ↦ ?_) add iSup hf

Premises used: Measurable.ennreal_induction
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
motive : (α → ℝ≥0∞) → Prop
indicator :
  ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun (x : α) ↦ ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
refine : ∀ (c : ℝ≥0∞) (s : Set α) (hs : MeasurableSet s), motive (s.indicator fun (x : α) ↦ c)
⊢ motive f

Tactic:
refine Measurable.ennreal_induction (fun c s hs ↦ ?_) add iSup hf
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
motive : (α → ℝ≥0∞) → Prop
indicator :
  ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun (x : α) ↦ ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
m n : ℕ
hmn : m ≤ n
a : α
h₁ : 0 ≤ c
grw grw₁ :
  LE.le (α := ℝ≥0∞) ((s ∩ spanningSets μ n).indicator (fun (x : α) ↦ c) a)
    ((s ∩ spanningSets μ n).indicator (fun (x : α) ↦ c) a)
⊢ LE.le (α := ℝ≥0∞) ((s ∩ spanningSets μ m).indicator (fun (x : α) ↦ c) a)
    ((s ∩ spanningSets μ n).indicator (fun (x : α) ↦ c) a)

Tactic:
grw [hmn]
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
motive : (α → ℝ≥0∞) → Prop
indicator :
  ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun (x : α) ↦ ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
h :
  ∀ (a : α),
    Eq (α := ℝ≥0∞) (s.indicator (fun (x : α) ↦ c) a) (⨆ (n : ℕ), (s ∩ spanningSets μ n).indicator (fun (x : α) ↦ c) a)
⊢ motive (s.indicator fun (x : α) ↦ c)

Tactic:
convert!
    iSup (f := fun n ↦ (s ∩ spanningSets μ n).indicator fun _ ↦ c)
      (fun n ↦ measurable_const.indicator (hs.inter (measurableSet_spanningSets ..)))
      (fun m n hmn a ↦ by dsimp; grw [hmn])
      (fun n ↦
        indicator _ (hs.inter (measurableSet_spanningSets ..))
          (measure_inter_lt_top_of_right_ne_top (measure_spanningSets_lt_top ..).ne)) with
    a

Premises used: MeasureTheory.measure_spanningSets_lt_top, MeasureTheory.measure_inter_lt_top_of_right_ne_top, Measurable.indicator, MeasureTheory.measurableSet_spanningSets, measurable_const, LT.lt.ne, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Function.SimpleFunc
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
motive : (α → ℝ≥0∞) → Prop
indicator :
  ∀ (c : ℝ≥0∞) ⦃s : Set α⦄,
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → motive (s.indicator fun (x : α) ↦ c)
add :
  ∀ ⦃f g : α → ℝ≥0∞⦄,
    Disjoint (support f) (support g) → Measurable f → Measurable g → motive f → motive g → motive (f + g)
iSup :
  ∀ ⦃f : ℕ → α → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) → Monotone f → (∀ (n : ℕ), motive (f n)) → motive fun (x : α) ↦ ⨆ (n : ℕ), f n x
f : α → ℝ≥0∞
hf : Measurable f
c : ℝ≥0∞
s : Set α
hs : MeasurableSet s
a : α
⊢ Eq (α := ℝ≥0∞) (s.indicator (fun (x : α) ↦ c) a) (⨆ (n : ℕ), (s ∩ spanningSets μ n).indicator (fun (x : α) ↦ c) a)

Tactic:
simp [← Set.indicator_iUnion_apply (M := ℝ≥0∞) rfl, ← Set.inter_iUnion]

Premises used: Set.indicator_iUnion_apply, Set.inter_iUnion, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
⊢ Eq (α := α →ₛ ℕ) (nearestPtInd e 0) (const α 0)

Tactic:
rfl

Premises used: MeasureTheory.SimpleFunc.nearestPtInd, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
⊢ Eq (α := α →ₛ α) (nearestPt e 0) (const α (e 0))

Tactic:
rfl

Premises used: MeasureTheory.SimpleFunc.const, MeasureTheory.SimpleFunc.nearestPt, MeasureTheory.SimpleFunc.bind, rfl, MeasureTheory.SimpleFunc.map
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
e_c :
  Membership.mem (γ := Set α) (⋂ (k : ℕ), ⋂ (_ : k ≤ N), {x : α | edist (e (N + 1)) x < edist (e k) x}) x =
    ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ (if Membership.mem (γ := Set α) (⋂ (k : ℕ), ⋂ (_ : k ≤ N), {x : α | edist (e (N + 1)) x < edist (e k) x}) x then
      (const α (N + 1) : (a : α) → ℕ) x
    else (nearestPtInd e N : (a : α) → ℕ) x) =
    if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N : (a : α) → ℕ) x

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ Membership.mem (γ := Set α) (⋂ (k : ℕ), ⋂ (_ : k ≤ N), {x : α | edist (e (N + 1)) x < edist (e k) x}) x =
    ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
⊢ LE.le (α := ℕ) ((nearestPtInd e 0 : (a : α) → ℕ) x : ℕ) (0 : ℕ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N : (a : α) → ℕ) x ≤ N
succ : (if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N : (a : α) → ℕ) x) ≤ N + 1
⊢ (nearestPtInd e (N + 1) : (a : α) → ℕ) x ≤ N + 1

Tactic:
simp only [nearestPtInd_succ]

Premises used: MeasureTheory.SimpleFunc.nearestPtInd_succ
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N : (a : α) → ℕ) x ≤ N
pos : (∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x) → N + 1 ≤ N + 1
neg : (¬∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x) → (nearestPtInd e N : (a : α) → ℕ) x ≤ N + 1
⊢ (if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N : (a : α) → ℕ) x) ≤ N + 1

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N : (a : α) → ℕ) x ≤ N
h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ N + 1 ≤ N + 1

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N : (a : α) → ℕ) x ≤ N
h : ¬∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ (nearestPtInd e N : (a : α) → ℕ) x ≤ N + 1

Tactic:
ihN.trans N.le_succ

Premises used: Nat.le_succ, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N : (a : α) → ℕ) x ≤ N
h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ N + 1 ≤ N + 1

Tactic:
exacts [le_rfl, ihN.trans N.le_succ]

Premises used: le_rfl, Nat.le_succ, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
zero : LE.le (α := ℕ) ((nearestPtInd e 0 : (a : α) → ℕ) x : ℕ) (0 : ℕ)
succ : ∀ (N : ℕ) (ihN : (nearestPtInd e N : (a : α) → ℕ) x ≤ N), (nearestPtInd e (N + 1) : (a : α) → ℕ) x ≤ N + 1
⊢ (nearestPtInd e N : (a : α) → ℕ) x ≤ N

Tactic:
induction N with
  | zero => simp
  | succ N ihN =>
    simp only [nearestPtInd_succ]
    split_ifs
    exacts [le_rfl, ihN.trans N.le_succ]

Premises used: le_rfl, MeasureTheory.SimpleFunc.nearestPtInd_succ
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
k : ℕ
hk : k ≤ 0
⊢ edist ((nearestPt e 0 : (a : α) → α) x) x ≤ edist (e k) x

Tactic:
simp [nonpos_iff_eq_zero.1 hk]

Premises used: Iff.mp, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
succ :
  edist (e (if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N : (a : α) → ℕ) x)) x ≤
    edist (e k) x
⊢ edist ((nearestPt e (N + 1) : (a : α) → α) x) x ≤ edist (e k) x

Tactic:
simp only [nearestPt, nearestPtInd_succ, map_apply]

Premises used: MeasureTheory.SimpleFunc.nearestPtInd_succ, MeasureTheory.SimpleFunc.nearestPt, MeasureTheory.SimpleFunc.map_apply
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
pos : ∀ (h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x), edist (e (N + 1)) x ≤ edist (e k) x
neg :
  ∀ (h : ¬∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x),
    edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e k) x
⊢ edist (e (if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N : (a : α) → ℕ) x)) x ≤
    edist (e k) x

Tactic:
split_ifs with h
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
pos : ∀ (hk : N + 1 ≤ N + 1), edist (e (N + 1)) x ≤ edist (e (N + 1)) x
pos₁ : ∀ (hk : k < N + 1), edist (e (N + 1)) x ≤ edist (e k) x
⊢ edist (e (N + 1)) x ≤ edist (e k) x

Tactic:
rcases hk.eq_or_lt with (rfl | hk)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
hk : N + 1 ≤ N + 1
⊢ edist (e (N + 1)) x ≤ edist (e (N + 1)) x

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
k : ℕ
hk_1 : k ≤ N + 1
h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
hk : k < N + 1
⊢ edist (e (N + 1)) x ≤ edist (e k) x

Tactic:
(h k (Nat.lt_succ_iff.1 hk)).le

Premises used: LT.lt.le, Nat.lt_succ_iff, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
hk : N + 1 ≤ N + 1
⊢ edist (e (N + 1)) x ≤ edist (e (N + 1)) x

Tactic:
exacts [le_rfl, (h k (Nat.lt_succ_iff.1 hk)).le]

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
h : ¬∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x
⊢ ∃ k ≤ N, edist (e k) x ≤ edist (e (N + 1)) x

Tactic:
push Not at h

Premises used: Not
-- Module: Mathlib.MeasureTheory.Function.SimpleFuncDense
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
h : ∃ k ≤ N, edist (e k) x ≤ edist (e (N + 1)) x
neg :
  ∀ (l : ℕ) (hlN : l ≤ N) (hxl : edist (e l) x ≤ edist (e (N + 1)) x),
    edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e k) x
⊢ edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e k) x

Tactic:
rcases h with ⟨l, hlN, hxl⟩