awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
Λ : (X →C_c ℝ) →ₚ[ℝ] ℝ
inst_4 : LocallyCompactSpace X
f : X →C_c ℝ
hf : ∀ (x : X), LE.le (α := ℝ) (0 : ℝ) ((f : (a : X) → ℝ) x : ℝ)
K : Set X
hK : IsCompact K
hfK : ∀ x ∈ K, Eq (α := ℝ) ((f : (a : X) → ℝ) x : ℝ) (1 : ℝ)
p : NNReal
hp : (Λ : (a : X →C_c ℝ) → ℝ) f = (↑p : ℝ)
h : (Λ : (a : X →C_c ℝ) → ℝ) f.nnrealPart.toReal = (↑p : ℝ)
h₁ : (Λ : (a : X →C_c ℝ) → ℝ) f = (↑p : ℝ)
h₂ h₃ : (↑p : ℝ) = (↑p : ℝ)
⊢ (↑((toNNRealLinear Λ : (a : X →C_c NNReal) → NNReal) f.nnrealPart) : ℝ) = (↑p : ℝ)

Tactic:
rw [toNNRealLinear_apply, show f.nnrealPart.toReal = f by ext z; simp [hf z], hp]

Premises used: CompactlySupportedContinuousMap.toNNRealLinear_apply
-- 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
n m : Fin N
h : n < m
⊢ a ≤ a

Tactic:
rfl
-- 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
n m : Fin N
h : n < m
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : (↑n : ℕ) + 1 ≤ (↑m : ℕ)
⊢ HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1 ≤ (↑(↑m : ℕ) : ℝ)

Tactic:
norm_cast
-- 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
n m : Fin N
h : n < m
⊢ ε ≤ ε

Tactic:
rfl
-- 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
n m : Fin N
h : n < m
⊢ y n + ε ≤ a + ε * (↑(↑m : ℕ) : ℝ) + ε

Tactic:
exact add_le_add_three (by rfl) ((mul_le_mul_iff_of_pos_left hε).mpr (by norm_cast)) (by rfl)

Premises used: Iff.mpr, add_le_add_three, mul_le_mul_iff_of_pos_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
n m : Fin N
h : n < m
dsimp : a + ε * (↑(↑m : ℕ) : ℝ) + ε = a + ε * HAdd.hAdd (α := ℝ) (↑(↑m : ℕ) : ℝ) 1
⊢ a + ε * (↑(↑m : ℕ) : ℝ) + ε = y m

Tactic:
dsimp [y]
-- 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
n m : Fin N
h : n < m
rw : a + ε * (↑(↑m : ℕ) : ℝ) + ε = a + (ε * (↑(↑m : ℕ) : ℝ) + ε * 1)
rw₁ : a + ε * (↑(↑m : ℕ) : ℝ) + ε = a + (ε * (↑(↑m : ℕ) : ℝ) + ε)
rw₂ rw₃ : a + (ε * (↑(↑m : ℕ) : ℝ) + ε) = a + (ε * (↑(↑m : ℕ) : ℝ) + ε)
⊢ a + ε * (↑(↑m : ℕ) : ℝ) + ε = a + ε * HAdd.hAdd (α := ℝ) (↑(↑m : ℕ) : ℝ) 1

Tactic:
rw [mul_add, mul_one, add_assoc]

Premises used: add_assoc, mul_add, mul_one
-- 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
⊢ ∀ {n m : Fin N} (h : n < m), y n + ε ≤ y m

Tactic:
have hy {n m : Fin N} (h : n < m) : y n + ε ≤ y m := calc
    _ ≤ a + ε * m + ε := by
      exact add_le_add_three (by rfl) ((mul_le_mul_iff_of_pos_left hε).mpr (by norm_cast)) (by rfl)
    _ = _ := by dsimp [y]; rw [mul_add, mul_one, add_assoc]
-- 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) → ℝ)
h :
  Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)
⊢ ∃ (E : Fin N → Set X),
    Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
      PairwiseDisjoint univ E ∧
        (∀ (n : Fin N),
            ∀ x ∈ E n,
              a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
                (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
          ∀ (n : Fin N), MeasurableSet (E n)

Tactic:
use E
-- 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) → ℝ)
⊢ Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)

Tactic:
⟨?_, ?_, ?_, ?_⟩

Premises used: And.intro
-- 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) → ℝ)
h : Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j)
h₁ : PairwiseDisjoint univ E
h₂ :
  ∀ (n : Fin N),
    ∀ x ∈ E n,
      a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
h₃ : ∀ (n : Fin N), MeasurableSet (E n)
⊢ Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j) ∧
    PairwiseDisjoint univ E ∧
      (∀ (n : Fin N),
          ∀ x ∈ E n,
            a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧
              (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1) ∧
        ∀ (n : Fin N), MeasurableSet (E n)

Tactic:
refine ⟨?_, ?_, ?_, ?_⟩
-- 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) → ℝ)
a_1 : ℝ
hz : Membership.mem (γ := Set ℝ) (range (ι := X) (⇑f : (a : X) → ℝ)) a_1
⊢ a_1 ∈ Ioc (a + (↑0 : ℝ) * ε) (a + (↑N : ℝ) * ε)

Tactic:
simpa using Ioo_subset_Ioc_self (hf hz)

Premises used: Set.Ioo_subset_Ioc_self
-- 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) → ℝ)
z : ℝ
simp :
  ∀ (x : ℕ) (x_1 : x < N),
    a + (↑x : ℝ) * ε < z →
      z ≤ a + (↑(x + 1) : ℝ) * ε →
        ∃ (i : Fin N),
          a + ε * HAdd.hAdd (α := ℝ) (↑(↑i : ℕ) : ℝ) 1 - ε < z ∧ z ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑i : ℕ) : ℝ) 1
⊢ Membership.mem (γ := Set ℝ) (⋃ i ∈ Finset.range N, Ioc (a + (↑i : ℝ) * ε) (a + (↑(i + 1) : ℝ) * ε)) z →
    Membership.mem (γ := Set ℝ) (⋃ (n : Fin N), Ioc (y n - ε) (y n)) z

Tactic:
simp only [Finset.mem_range, mem_iUnion, mem_Ioc, forall_exists_index, and_imp, y]

Premises used: and_imp, Set.mem_iUnion, forall_exists_index, Finset.mem_range, Set.mem_Ioc
-- 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) → ℝ)
z : ℝ
n : ℕ
hn : n < N
h : a + (↑n : ℝ) * ε < z
h_1 : z ≤ a + (↑(n + 1) : ℝ) * ε
linarith :
  z ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑(⟨n, hn⟩ : Fin N) : ℕ) : ℝ) 1 - ε →
    a + (↑n : ℝ) * ε - z + (z - (a + ε * HAdd.hAdd (α := ℝ) (↑(↑(⟨n, hn⟩ : Fin N) : ℕ) : ℝ) 1 - ε)) = 0
⊢ a + ε * HAdd.hAdd (α := ℝ) (↑(↑(⟨n, hn⟩ : Fin N) : ℕ) : ℝ) 1 - ε < z

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) → ℝ)
z : ℝ
n : ℕ
hn : n < N
h : a + (↑n : ℝ) * ε < z
h_1 : z ≤ a + (↑(n + 1) : ℝ) * ε
⊢ z ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑(⟨n, hn⟩ : Fin N) : ℕ) : ℝ) 1

Tactic:
simp_all [mul_comm ε _]

Premises used: mul_comm
-- 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) → ℝ)
z : ℝ
⊢ ∀ (x : ℕ) (x_1 : x < N),
    a + (↑x : ℝ) * ε < z →
      z ≤ a + (↑(x + 1) : ℝ) * ε →
        ∃ (i : Fin N),
          a + ε * HAdd.hAdd (α := ℝ) (↑(↑i : ℕ) : ℝ) 1 - ε < z ∧ z ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑i : ℕ) : ℝ) 1

Tactic:
refine fun n hn _ _ ↦ ⟨⟨n, hn⟩, ⟨by linarith, by simp_all [mul_comm ε _]⟩⟩
-- 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) → ℝ)
⊢ Subset (α := Set ℝ) (range (ι := X) (⇑f : (a : X) → ℝ)) (⋃ (n : Fin N), Ioc (y n - ε) (y n))

Tactic:
have partition_aux : range f ⊆ ⋃ n, Ioc (y n - ε) (y n) := calc
      _ ⊆ Ioc (a + (0 : ℕ) * ε) (a + N * ε) := by
        intro _ hz
        simpa using Ioo_subset_Ioc_self (hf hz)
      _ ⊆ ⋃ i ∈ Finset.range N, Ioc (a + ↑i * ε) (a + ↑(i + 1) * ε) :=
        Ioc_subset_biUnion_Ioc N (fun n ↦ a + n * ε)
      _ ⊆ _ := by
        intro z
        simp only [Finset.mem_range, mem_iUnion, mem_Ioc, forall_exists_index, and_imp, y]
        refine fun n hn _ _ ↦ ⟨⟨n, hn⟩, ⟨by linarith, by simp_all [mul_comm ε _]⟩⟩
-- 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) → ℝ)
partition_aux : Subset (α := Set ℝ) (range (ι := X) (⇑f : (a : X) → ℝ)) (⋃ (n : Fin N), Ioc (y n - ε) (y n))
h :
  Subset (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ))
    (preimage (β := ℝ) (⇑f : (a : X) → ℝ) (⋃ (i : Fin N), Ioc (y i - ε) (y i)))
⊢ Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j)

Tactic:
simp only [E, ← iUnion_inter, ← preimage_iUnion, eq_comm (a := tsupport _), inter_eq_right]

Premises used: Set.inter_eq_right, eq_comm, Set.iUnion_inter, Set.preimage_iUnion
-- 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) → ℝ)
partition_aux : Subset (α := Set ℝ) (range (ι := X) (⇑f : (a : X) → ℝ)) (⋃ (n : Fin N), Ioc (y n - ε) (y n))
⊢ Subset (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ))
    (preimage (β := ℝ) (⇑f : (a : X) → ℝ) (⋃ (i : Fin N), Ioc (y i - ε) (y i)))

Tactic:
fun x _ ↦ partition_aux (mem_range_self x)

Premises used: Set.mem_range_self, Set.Mem, iSup, setOf, Set.Subset, Set.preimage, Set.iUnion
-- 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) → ℝ)
partition_aux : Subset (α := Set ℝ) (range (ι := X) (⇑f : (a : X) → ℝ)) (⋃ (n : Fin N), Ioc (y n - ε) (y n))
⊢ Subset (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ))
    (preimage (β := ℝ) (⇑f : (a : X) → ℝ) (⋃ (i : Fin N), Ioc (y i - ε) (y i)))

Tactic:
exact fun x _ ↦ partition_aux (mem_range_self x)

Premises used: Set.mem_range_self
-- 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 →
    ∀ ⦃y : Fin N⦄, Membership.mem (γ := Set (Fin N)) univ y → m ≠ y → (Disjoint on E) m y
⊢ Membership.mem (γ := Set (Fin N)) univ m →
    ∀ ⦃y : Fin N⦄, Membership.mem (γ := Set (Fin N)) univ y → m ≠ y → (Disjoint on E) m y

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) → ℝ)
m : Fin N
h_1 : Membership.mem (γ := Set (Fin N)) univ m
n : Fin N
h : Membership.mem (γ := Set (Fin N)) univ n → m ≠ n → (Disjoint on E) m n
⊢ Membership.mem (γ := Set (Fin N)) univ n → m ≠ n → (Disjoint on E) m n

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) → ℝ)
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
h :
  Disjoint.{u_1} (α := Set X)
    {a : X |
      Membership.mem (γ := Set X) ((⇑f : (a : X) → ℝ) ⁻¹' Ioc (y m - ε) (y m)) a ∧
        Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) a}
    {a : X |
      Membership.mem (γ := Set X) ((⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n)) a ∧
        Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) a}
⊢ (Disjoint on E) m n

Tactic:
apply Disjoint.preimage

Premises used: Disjoint.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) → ℝ)
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
h :
  ∀ ⦃a : X⦄,
    Membership.mem (γ := Set X)
        {a : X |
          (y m - ε < (f : (a : X) → ℝ) a ∧ (f : (a : X) → ℝ) a ≤ y m) ∧
            Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) a}
        a →
      a ∉
        {a : X |
          (y n - ε < (f : (a : X) → ℝ) a ∧ (f : (a : X) → ℝ) a ≤ y n) ∧
            Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) a}
⊢ Disjoint.{u_1} (α := Set X)
    {a : X |
      Membership.mem (γ := Set X) ((⇑f : (a : X) → ℝ) ⁻¹' Ioc (y m - ε) (y m)) a ∧
        Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) a}
    {a : X |
      Membership.mem (γ := Set X) ((⇑f : (a : X) → ℝ) ⁻¹' Ioc (y n - ε) (y n)) a ∧
        Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) a}

Tactic:
simp_rw [mem_preimage, mem_Ioc, disjoint_left]

Premises used: Set.disjoint_left, 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) → ℝ)
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 :
  Membership.mem (γ := Set X)
    {a : X |
      (y m - ε < (f : (a : X) → ℝ) a ∧ (f : (a : X) → ℝ) a ≤ y m) ∧
        Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) a}
    x
⊢ y m - ε < (f : (a : X) → ℝ) x ∧
    (f : (a : X) → ℝ) x ≤ y m ∧ Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) x

Tactic:
rw [mem_setOf_eq, and_assoc] at hx

Premises used: Set.mem_setOf_eq, and_assoc
-- 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 : (f : (a : X) → ℝ) x ≤ y n - ε ∨ y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
⊢ x ∉
    {a : X |
      (y n - ε < (f : (a : X) → ℝ) a ∧ (f : (a : X) → ℝ) a ≤ y n) ∧
        Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) a}

Tactic:
simp_rw [mem_setOf_eq, not_and_or, not_lt, not_le, or_assoc]

Premises used: not_le, Set.mem_setOf_eq, not_lt, not_and_or, or_assoc
-- 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
⊢ m < n ∨ n < m

Tactic:
lia