awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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 : α
pos :
  ∀ (hy : Membership.mem (γ := Set α) (preimage (β := γ) (⇑f : (a : α) → γ) {x}) y),
    Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
      ((piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ ⋯ g (SimpleFunc.const α x) : (a : α) → γ) y : γ)
⊢ Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
    ((piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ ⋯ g (SimpleFunc.const α x) : (a : α) → γ) y : γ)
have neg : ∀ (hy : y ∉ preimage (β := γ) (⇑f : (a : α) → γ) {x}),
  Eq.{u_6 + 1} (α := γ) ((f : (a : α) → γ) y : γ)
    ((piecewise (preimage (β := γ) (⇑f : (a : α) → γ) {x})ᶜ sorry g (SimpleFunc.const α x) : (a : α) → γ) y : γ)
Tactic: by_cases hy : y ∈ f ⁻¹' {x}
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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 γ)
⊢ P f
have empty : ∀ (f : α →ₛ γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑∅ : Set γ)), 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]
Cleared hypotheses: f, s, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ P f
have 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 x s) : Set γ)), 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]
Cleared hypotheses: f, s, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ P f
have generalize : ∀ (s : Finset γ) (h : f.range \ {c} = s), 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ P f
have generalize₁ : ∀ (s : Finset γ) (h : range.{u_6, u_5 + 1} (ι := α) (⇑f : (a : α) → γ) \ {c} = (↑s : Set γ)), 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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 f
have h : ∀ (x : α), f x = ⨆ (n : ℕ), ((eapprox f n : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) x
Tactic: convert! iSup (fun n => (eapprox f n).measurable) (monotone_eapprox f) _ using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ motive f
have convert! : ∀ (n : ℕ), motive (⇑(eapprox f n) : (a : α) → ℝ≥0∞)
Tactic: convert! iSup (fun n => (eapprox f n).measurable) (monotone_eapprox f) _ using 2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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 : α
⊢ f x = ⨆ (n : ℕ), ((eapprox f n : SimpleFunc α ℝ≥0∞) : (a : α) → ℝ≥0∞) x
have h : f x = f x
Tactic: rw [iSup_eapprox_apply hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
have refine : ∀ (c : ℝ≥0∞) (s : Set α) (hs : MeasurableSet s), motive (s.indicator fun (x : α) ↦ c)
Tactic: refine Measurable.ennreal_induction (fun c s hs ↦ ?_) add iSup hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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 : α
⊢ LE.le (α := ℝ≥0∞) ((s ∩ spanningSets μ m).indicator (fun (x : α) ↦ c) a)
    ((s ∩ spanningSets μ n).indicator (fun (x : α) ↦ c) a)
have h₁ : 0 ≤ c
Tactic: grw [hmn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ LE.le (α := ℝ≥0∞) ((s ∩ spanningSets μ m).indicator (fun (x : α) ↦ c) a)
    ((s ∩ spanningSets μ n).indicator (fun (x : α) ↦ c) a)
have grw : LE.le (α := ℝ≥0∞) ((s ∩ spanningSets μ n).indicator (fun (x : α) ↦ c) a)
  ((s ∩ spanningSets μ n).indicator (fun (x : α) ↦ c) a)
Tactic: grw [hmn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFunc (goal)
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
⊢ motive (s.indicator fun (x : α) ↦ c)
have h : ∀ (a : α),
  Eq (α := ℝ≥0∞) (s.indicator (fun (x : α) ↦ c) a) (⨆ (n : ℕ), (s ∩ spanningSets μ n).indicator (fun (x : α) ↦ c) a)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
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
have 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
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N : (a : α) → ℕ) x ≤ N
⊢ (nearestPtInd e (N + 1) : (a : α) → ℕ) x ≤ N + 1
have succ : (if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N : (a : α) → ℕ) x) ≤ N + 1
Tactic: simp only [nearestPtInd_succ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
x : α
N : ℕ
ihN : (nearestPtInd e N : (a : α) → ℕ) x ≤ N
⊢ (if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N : (a : α) → ℕ) x) ≤ N + 1
have pos : (∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x) → N + 1 ≤ N + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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
⊢ (if ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x then N + 1 else (nearestPtInd e N : (a : α) → ℕ) x) ≤ N + 1
have neg : (¬∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x) → (nearestPtInd e N : (a : α) → ℕ) x ≤ N + 1
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
⊢ (nearestPtInd e N : (a : α) → ℕ) x ≤ N
have zero : LE.le (α := ℕ) ((nearestPtInd e 0 : (a : α) → ℕ) x : ℕ) (0 : ℕ)
Tactic: induction N with
  | zero => simp
  | succ N ihN =>
    simp only [nearestPtInd_succ]
    split_ifs
    exacts [le_rfl, ihN.trans N.le_succ]
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : PseudoEMetricSpace α
inst_2 : OpensMeasurableSpace α
e : ℕ → α
N : ℕ
x : α
zero : LE.le (α := ℕ) ((nearestPtInd e 0 : (a : α) → ℕ) x : ℕ) (0 : ℕ)
⊢ (nearestPtInd e N : (a : α) → ℕ) x ≤ N
have succ : ∀ (N : ℕ) (ihN : (nearestPtInd e N : (a : α) → ℕ) x ≤ N), (nearestPtInd e (N + 1) : (a : α) → ℕ) x ≤ N + 1
Tactic: induction N with
  | zero => simp
  | succ N ihN =>
    simp only [nearestPtInd_succ]
    split_ifs
    exacts [le_rfl, ihN.trans N.le_succ]
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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
⊢ edist ((nearestPt e (N + 1) : (a : α) → α) x) x ≤ edist (e k) x
have 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
Tactic: simp only [nearestPt, nearestPtInd_succ, map_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (goal)
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
⊢ 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
have pos : ∀ (h : ∀ k ≤ N, edist (e (N + 1)) x < edist (e k) x), edist (e (N + 1)) x ≤ edist (e k) x
Tactic: split_ifs with 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 : α
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
⊢ 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
have 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
Tactic: split_ifs with 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 : α
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
⊢ edist (e (N + 1)) x ≤ edist (e k) x
have pos : ∀ (hk : N + 1 ≤ N + 1), edist (e (N + 1)) x ≤ edist (e (N + 1)) x
Tactic: rcases hk.eq_or_lt with (rfl | hk)
Cleared hypotheses: k, 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 : α
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
⊢ edist (e (N + 1)) x ≤ edist (e k) x
have pos₁ : ∀ (hk : k < N + 1), edist (e (N + 1)) x ≤ edist (e k) x
Tactic: rcases hk.eq_or_lt with (rfl | hk)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.SimpleFuncDense (hypothesis)
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
⊢ edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e k) x
have h₁ : ∃ k ≤ N, edist (e k) x ≤ edist (e (N + 1)) x
Tactic: push Not at h
Cleared hypotheses: 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 : α
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
⊢ edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e k) x
have 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
Tactic: rcases h with ⟨l, hlN, hxl⟩
Cleared hypotheses: 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 : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
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
have neg : ∀ (hk : N + 1 ≤ N + 1), edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e (N + 1)) x
Tactic: rcases hk.eq_or_lt with (rfl | hk)
Cleared hypotheses: k, 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 : α
N : ℕ
ihN : ∀ {k : ℕ} (hk : k ≤ N), edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
k : ℕ
hk : k ≤ N + 1
l : ℕ
hlN : l ≤ N
hxl : edist (e l) x ≤ edist (e (N + 1)) x
neg : ∀ (hk : N + 1 ≤ N + 1), edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e (N + 1)) x
⊢ edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e k) x
have neg₁ : ∀ (hk : k < N + 1), edist (e ((nearestPtInd e N : (a : α) → ℕ) x)) x ≤ edist (e k) x
Tactic: rcases hk.eq_or_lt with (rfl | 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 : α
k N : ℕ
hk : k ≤ N
⊢ edist ((nearestPt e N : (a : α) → α) x) x ≤ edist (e k) x
have zero : ∀ {k : ℕ} (hk : k ≤ 0), edist ((nearestPt e 0 : (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