awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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) → ℝ)
⊢ ∃ (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)
have 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)
Tactic: use E
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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)
have h : Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j)
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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)
⊢ 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)
have h₁ : PairwiseDisjoint univ E
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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
⊢ 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)
have h₂ : ∀ (n : Fin N),
  ∀ x ∈ E n,
    a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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
⊢ 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)
have h₃ : ∀ (n : Fin N), MeasurableSet (E n)
Tactic: refine ⟨?_, ?_, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 : ℝ
⊢ 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
have 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
Tactic: simp only [Finset.mem_range, mem_iUnion, mem_Ioc, forall_exists_index, and_imp, y]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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) : ℝ) * ε
⊢ a + ε * HAdd.hAdd (α := ℝ) (↑(↑(⟨n, hn⟩ : Fin N) : ℕ) : ℝ) 1 - ε < z
have linarith : z ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑(⟨n, hn⟩ : Fin N) : ℕ) : ℝ) 1 - ε →
  a + (↑n : ℝ) * ε - z + (z - (a + ε * HAdd.hAdd (α := ℝ) (↑(↑(⟨n, hn⟩ : Fin N) : ℕ) : ℝ) 1 - ε)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
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)
have partition_aux : 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 ε _]⟩⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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))
⊢ Eq (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) (⋃ (j : Fin N), E j)
have h : Subset (α := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ))
  (preimage (β := ℝ) (⇑f : (a : X) → ℝ) (⋃ (i : Fin N), Ioc (y i - ε) (y i)))
Tactic: simp only [E, ← iUnion_inter, ← preimage_iUnion, eq_comm (a := tsupport _), inter_eq_right]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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
⊢ (Disjoint on E) m n
have 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}
Tactic: apply Disjoint.preimage
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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
⊢ 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}
have 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}
Tactic: simp_rw [mem_preimage, mem_Ioc, disjoint_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
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
⊢ x ∉
    {a : X |
      (y n - ε < (f : (a : X) → ℝ) a ∧ (f : (a : X) → ℝ) a ≤ y n) ∧
        Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) a}
have hx₁ : 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
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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
⊢ x ∉
    {a : X |
      (y n - ε < (f : (a : X) → ℝ) a ∧ (f : (a : X) → ℝ) a ≤ y n) ∧
        Membership.mem (γ := Set X) (tsupport (α := ℝ) (⇑f : (a : X) → ℝ)) a}
have h : (f : (a : X) → ℝ) x ≤ y n - ε ∨ y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
Tactic: simp_rw [mem_setOf_eq, not_and_or, not_lt, not_le, or_assoc]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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
⊢ (f : (a : X) → ℝ) x ≤ y n - ε ∨ y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
have h : ∀ (hc : m < n), (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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) → ℝ)
⊢ (f : (a : X) → ℝ) x ≤ y n - ε ∨ y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
have h₁ : ∀ (hc : n < m), (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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 - ε ∨ y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
have h : (f : (a : X) → ℝ) x ≤ y n - ε
Tactic: left
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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
⊢ (f : (a : X) → ℝ) x ≤ y n - ε ∨ y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
have h : y n < (f : (a : X) → ℝ) x ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
Tactic: right
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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 ∨ x ∉ tsupport (α := ℝ) (⇑f : (a : X) → ℝ)
have h : y n < (f : (a : X) → ℝ) x
Tactic: left
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (hypothesis)
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 + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
have 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
Tactic: simp only [mem_inter_iff, mem_preimage, mem_Ioc, E, y] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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
⊢ a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
have h : a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real (goal)
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
⊢ a + ε * (↑(↑n : ℕ) : ℝ) < (f : (a : X) → ℝ) x ∧ (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
have h₁ : (f : (a : X) → ℝ) x ≤ a + ε * HAdd.hAdd (α := ℝ) (↑(↑n : ℕ) : ℝ) 1
Tactic: constructor