awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
m : Fin N
h_1 : Membership.mem (γ := Set (Fin N)) univ m
n : Fin N
h_2 : Membership.mem (γ := Set (Fin N)) univ n
hmn : m ≠ n
x : X
hx :
  y m - ε < (f : (a : X) → ℝ) x ∧
    (f : (a : X) → ℝ) x ≤ y m ∧ Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
h : ∀ (hc : m < n), (f : (a : X) → ℝ) x ≤ y n - ε ∨ y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
h₁ :
  ∀ (hc : n < m), (f : (a : X) → ℝ) x ≤ y n - ε ∨ y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
⊢ (f : (a : X) → ℝ) x ≤ y n - ε ∨ y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)

Tactic:
rcases (by lia : m < n ∨ n < m) with hc | hc
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
m : Fin N
h_1 : Membership.mem (γ := Set (Fin N)) univ m
n : Fin N
h_2 : Membership.mem (γ := Set (Fin N)) univ n
hmn : m ≠ n
x : X
hx :
  y m - ε < (f : (a : X) → ℝ) x ∧
    (f : (a : X) → ℝ) x ≤ y m ∧ Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
hc : m < n
h : (f : (a : X) → ℝ) x ≤ y n - ε
⊢ (f : (a : X) → ℝ) x ≤ y n - ε ∨ y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)

Tactic:
left
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
m : Fin N
h : Membership.mem (γ := Set (Fin N)) univ m
n : Fin N
h_1 : Membership.mem (γ := Set (Fin N)) univ n
hmn : m ≠ n
x : X
hx :
  y m - ε < (f : (a : X) → ℝ) x ∧
    (f : (a : X) → ℝ) x ≤ y m ∧ Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
hc : m < n
⊢ (f : (a : X) → ℝ) x ≤ y n - ε

Tactic:
le_trans hx.2.1 (le_tsub_of_add_le_right (hy hc))

Premises used: And.right, And.left, le_tsub_of_add_le_right, le_trans
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
m : Fin N
h : Membership.mem (γ := Set (Fin N)) univ m
n : Fin N
h_1 : Membership.mem (γ := Set (Fin N)) univ n
hmn : m ≠ n
x : X
hx :
  y m - ε < (f : (a : X) → ℝ) x ∧
    (f : (a : X) → ℝ) x ≤ y m ∧ Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
hc : m < n
⊢ (f : (a : X) → ℝ) x ≤ y n - ε

Tactic:
exact le_trans hx.2.1 (le_tsub_of_add_le_right (hy hc))

Premises used: And.right, And.left, le_tsub_of_add_le_right, le_trans
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
m : Fin N
h_1 : Membership.mem (γ := Set (Fin N)) univ m
n : Fin N
h_2 : Membership.mem (γ := Set (Fin N)) univ n
hmn : m ≠ n
x : X
hx :
  y m - ε < (f : (a : X) → ℝ) x ∧
    (f : (a : X) → ℝ) x ≤ y m ∧ Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
hc : n < m
h : y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
⊢ (f : (a : X) → ℝ) x ≤ y n - ε ∨ y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)

Tactic:
right
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
m : Fin N
h_1 : Membership.mem (γ := Set (Fin N)) univ m
n : Fin N
h_2 : Membership.mem (γ := Set (Fin N)) univ n
hmn : m ≠ n
x : X
hx :
  y m - ε < (f : (a : X) → ℝ) x ∧
    (f : (a : X) → ℝ) x ≤ y m ∧ Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
hc : n < m
h : y n < (f : (a : X) → ℝ) x
⊢ y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)

Tactic:
left
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
m : Fin N
h : Membership.mem (γ := Set (Fin N)) univ m
n : Fin N
h_1 : Membership.mem (γ := Set (Fin N)) univ n
hmn : m ≠ n
x : X
hx :
  y m - ε < (f : (a : X) → ℝ) x ∧
    (f : (a : X) → ℝ) x ≤ y m ∧ Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
hc : n < m
⊢ y n < (f : (a : X) → ℝ) x

Tactic:
lt_of_le_of_lt (le_tsub_of_add_le_right (hy hc)) hx.1

Premises used: lt_of_le_of_lt, And.left, le_tsub_of_add_le_right
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
m : Fin N
h : Membership.mem (γ := Set (Fin N)) univ m
n : Fin N
h_1 : Membership.mem (γ := Set (Fin N)) univ n
hmn : m ≠ n
x : X
hx :
  y m - ε < (f : (a : X) → ℝ) x ∧
    (f : (a : X) → ℝ) x ≤ y m ∧ Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
hc : n < m
⊢ y n < (f : (a : X) → ℝ) x

Tactic:
exact lt_of_le_of_lt (le_tsub_of_add_le_right (hy hc)) hx.1

Premises used: lt_of_le_of_lt, And.left, le_tsub_of_add_le_right
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
n : Fin N
h :
  ∀ x ∈ E n,
    a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
⊢ ∀ x ∈ E n,
    a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1

Tactic:
_
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
n : Fin N
x : X
hx : x ∈ E n
⊢ (a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 - ε < (f : (a : X) → ℝ) x ∧
      (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
    Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x

Tactic:
simp only [mem_inter_iff, mem_preimage, mem_Ioc, E, y] at hx

Premises used: Set.mem_inter_iff, Set.mem_Ioc, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
n : Fin N
x : X
hx :
  (a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 - ε < (f : (a : X) → ℝ) x ∧
      (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
    Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
h : a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x
h₁ : (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
⊢ a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
n : Fin N
x : X
hx :
  (a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 - ε < (f : (a : X) → ℝ) x ∧
      (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
    Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
linarith :
  (f : (a : X) → ℝ) x ≤ a + ε * (↑(↑n : ℕ) : ℝ) →
    HSub.hSub (β := ℝ) (a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 - ε) ((f : (a : X) → ℝ) x : ℝ) +
        HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (a + ε * (↑(↑n : ℕ) : ℝ)) =
      0
⊢ a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
n : Fin N
x : X
hx :
  (a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 - ε < (f : (a : X) → ℝ) x ∧
      (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
    Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x
linarith :
  a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 < (f : (a : X) → ℝ) x →
    HSub.hSub (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) +
        HSub.hSub (β := ℝ) (a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ((f : (a : X) → ℝ) x : ℝ) =
      0
⊢ (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
⊢ ∀ (n : Fin N), MeasurableSet (E n)

Tactic:
fun _ ↦ (f.1.measurable measurableSet_Ioc).inter measurableSet_closure

Premises used: measurableSet_closure, CompactlySupportedContinuousMap.toContinuousMap, measurableSet_Ioc, ContinuousMap.measurable, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
f : X →C_c ℝ
a ε : ℝ
hε : 0 < ε
N : ℕ
hf : range (ι := X) (⇑f : (a : X) → ℝ) ⊆ Ioo a (a + (↑N : ℝ) * ε)
b : ℝ := a + (↑N : ℝ) * ε
y : Fin N → ℝ := fun (n : Fin N) ↦ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
hy : ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m
E : (n : Fin N) → Set X :=
  fun (n : Fin N) ↦ (⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n) ∩ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
⊢ ∀ (n : Fin N), MeasurableSet (E n)

Tactic:
exact fun _ ↦ (f.1.measurable measurableSet_Ioc).inter measurableSet_closure

Premises used: measurableSet_closure, CompactlySupportedContinuousMap.toContinuousMap, measurableSet_Ioc, ContinuousMap.measurable, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
⊢ ε.toNNReal ≠ 0

Tactic:
have hε' := ne_of_gt <| Real.toNNReal_pos.mpr hε
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
obtain :
  ∀ (V₁ : Opens X)
    (hV₁ :
      E ⊆ (↑V₁ : Set X) ∧
        (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)),
    ∃ (V : Opens X),
      E ⊆ (↑V : Set X) ∧
        (∀ x ∈ V, (f : (a : X) → ℝ) x < c) ∧
          ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑V : Set X) ≤
            HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
⊢ ∃ (V : Opens X),
    E ⊆ (↑V : Set X) ∧
      (∀ x ∈ V, (f : (a : X) → ℝ) x < c) ∧
        ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑V : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)

Tactic:
obtain ⟨V₁ : Opens X, hV₁⟩ := Content.outerMeasure_exists_open μ hμ hε'

Premises used: TopologicalSpace.Opens, MeasureTheory.Content.outerMeasure_exists_open
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
h :
  E ⊆ (↑(V₁ ⊓ V₂) : Set X) ∧
    (∀ x ∈ V₁ ⊓ V₂, (f : (a : X) → ℝ) x < c) ∧
      ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V₁ ⊓ V₂) : Set X) ≤
        HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
⊢ ∃ (V : Opens X),
    E ⊆ (↑V : Set X) ∧
      (∀ x ∈ V, (f : (a : X) → ℝ) x < c) ∧
        ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑V : Set X) ≤
          HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)

Tactic:
use V₁ ⊓ V₂
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
⊢ E ⊆ (↑(V₁ ⊓ V₂) : Set X) ∧
    (∀ x ∈ V₁ ⊓ V₂, (f : (a : X) → ℝ) x < c) ∧
      ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V₁ ⊓ V₂) : Set X) ≤
        HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)

Tactic:
⟨subset_inter hV₁.1 hfE, ?_, ?_⟩

Premises used: Set.subset_inter, And.left, And.intro
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
h : ∀ x ∈ V₁ ⊓ V₂, (f : (a : X) → ℝ) x < c
h₁ :
  ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V₁ ⊓ V₂) : Set X) ≤
    HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)
⊢ E ⊆ (↑(V₁ ⊓ V₂) : Set X) ∧
    (∀ x ∈ V₁ ⊓ V₂, (f : (a : X) → ℝ) x < c) ∧
      ((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V₁ ⊓ V₂) : Set X) ≤
        HAdd.hAdd (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (ENNReal.ofReal ε)

Tactic:
refine ⟨subset_inter hV₁.1 hfE, ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
x : X
hx : x ∈ V₁ ⊓ V₂
h : ∀ x ∈ V₂.carrier, (f : (a : X) → ℝ) x < c
⊢ (f : (a : X) → ℝ) x < c

Tactic:
suffices ∀ x ∈ V₂.carrier, f x < c from this x (mem_of_mem_inter_right hx)
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
x : X
hx : x ∈ V₁ ⊓ V₂
⊢ ∀ x ∈ V₂.carrier, (f : (a : X) → ℝ) x < c

Tactic:
fun _ a ↦ a

Premises used: Set.Mem, setOf, Set.preimage, Set.Iio
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
x : X
hx : x ∈ V₁ ⊓ V₂
⊢ ∀ x ∈ V₂.carrier, (f : (a : X) → ℝ) x < c

Tactic:
exact fun _ a ↦ a
-- Module: Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : T2Space X
inst_2 : MeasurableSpace X
inst_3 : BorelSpace X
f : X →C_c ℝ
ε : ℝ
hε : 0 < ε
E : Set X
μ : Content X
hμ : Ne (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (∞ : ℝ≥0∞)
hμ' : MeasurableSet E
c : ℝ
hfE : ∀ x ∈ E, (f : (a : X) → ℝ) x < c
hε' : ε.toNNReal ≠ 0
V₁ : Opens X
hV₁ :
  E ⊆ (↑V₁ : Set X) ∧
    (μ.outerMeasure : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) ≤
      HAdd.hAdd (α := ℝ≥0∞) ((μ.outerMeasure : (a : Set X) → ℝ≥0∞) E : ℝ≥0∞) (↑ε.toNNReal : ℝ≥0∞)
V₂ : Opens X := { carrier := (⇑f : (a : X) → ℝ) ⁻¹' Iio c, is_open' := ⋯ }
⊢ LE.le (α := ℝ≥0∞) (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑(V₁ ⊓ V₂) : Set X) : ℝ≥0∞)
    (((μ.measure : Measure X) : (a : Set X) → ℝ≥0∞) (↑V₁ : Set X) : ℝ≥0∞)

Tactic:
simp [measure_mono]

Premises used: MeasureTheory.measure_mono