awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
y_le : y - x ≤ (1 / 2) ^ (n e + 1)
yone : y - x ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : y - x ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < y - x
m_ge : n e ≤ m
km : k = m + 1
J : ‖f y - f x - (y - x) • L e (n e) m‖ ≤ 4 * (1 / 2) ^ e * ‖y - x‖
⊢ 4 * (1 / 2) ^ e * ‖y - x‖ + ‖y - x‖ * (12 * (1 / 2) ^ e) = 16 * ‖y - x‖ * (1 / 2) ^ e

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
y_le : y - x ≤ (1 / 2) ^ (n e + 1)
yone : y - x ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : y - x ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < y - x
m_ge : n e ≤ m
km : k = m + 1
J : ‖f y - f x - (y - x) • L e (n e) m‖ ≤ 4 * (1 / 2) ^ e * ‖y - x‖
ha : 0 ≤ 16 * ‖y - x‖
⊢ 16 * ‖y - x‖ * (1 / 2) ^ e ≤ 16 * ‖y - x‖ * (ε / 16)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
y_le : y - x ≤ (1 / 2) ^ (n e + 1)
yone : y - x ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : y - x ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < y - x
m_ge : n e ≤ m
km : k = m + 1
J : ‖f y - f x - (y - x) • L e (n e) m‖ ≤ 4 * (1 / 2) ^ e * ‖y - x‖
⊢ 16 * ‖y - x‖ * (ε / 16) = ε * ‖y - x‖

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
e : ℕ
he : (1 / 2) ^ e < ε / 16
y : ℝ
hy : y ∈ Icc x (x + (1 / 2) ^ (n e + 1))
xy : x < y
yzero : 0 < y - x
y_le : y - x ≤ (1 / 2) ^ (n e + 1)
yone : y - x ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : y - x ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < y - x
m_ge : n e ≤ m
km : k = m + 1
J : ‖f y - f x - (y - x) • L e (n e) m‖ ≤ 4 * (1 / 2) ^ e * ‖y - x‖
y₁ : ‖f y - f x - (y - x) • f'‖ = ‖f y - f x - (y - x) • L e (n e) m + (y - x) • (L e (n e) m - f')‖
y₂ : 4 * (1 / 2) ^ e * ‖y - x‖ + ‖y - x‖ * (12 * (1 / 2) ^ e) = 16 * ‖y - x‖ * (1 / 2) ^ e
y₃ : 16 * ‖y - x‖ * (1 / 2) ^ e ≤ 16 * ‖y - x‖ * (ε / 16)
y₄ : 16 * ‖y - x‖ * (ε / 16) = ε * ‖y - x‖
⊢ ‖f y - f x - (y - x) • f'‖ ≤ ε * ‖y - x‖

Tactic:
calc
      ‖f y - f x - (y - x) • f'‖ =
          ‖f y - f x - (y - x) • L e (n e) m + (y - x) • (L e (n e) m - f')‖ := by
        simp only [smul_sub, sub_add_sub_cancel]
      _ ≤ 4 * (1 / 2) ^ e * ‖y - x‖ + ‖y - x‖ * (12 * (1 / 2) ^ e) :=
        norm_add_le_of_le J <| by rw [norm_smul]; gcongr; exact Lf' _ _ m_ge
      _ = 16 * ‖y - x‖ * (1 / 2) ^ e := by ring
      _ ≤ 16 * ‖y - x‖ * (ε / 16) := by gcongr
      _ = ε * ‖y - x‖ := by ring

Premises used: HMul.hMul, HSub.hSub, HDiv.hDiv, HPow.hPow, norm_add_le_of_le, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this_1 : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
this : HasDerivWithinAt f f' (Ici x) x
⊢ derivWithin f (Ici x) x ∈ K

Tactic:
rw [← this.derivWithin (uniqueDiffOn_Ici x x Set.self_mem_Ici)] at f'K

Premises used: HasDerivWithinAt.derivWithin, uniqueDiffOn_Ici, Set.self_mem_Ici
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this_1 : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
this : HasDerivWithinAt f f' (Ici x) x
f'K₁ : derivWithin f (Ici x) x ∈ K
⊢ Tendsto L0 atTop (𝓝 f')

Tactic:
rw [← this.derivWithin (uniqueDiffOn_Ici x x Set.self_mem_Ici)] at f'K

Premises used: HasDerivWithinAt.derivWithin, uniqueDiffOn_Ici, Set.self_mem_Ici
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this_1 : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
this : HasDerivWithinAt f f' (Ici x) x
f'K₁ : derivWithin f (Ici x) x ∈ K
hf'₁ : Tendsto L0 atTop (𝓝 f')
⊢ ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e

Tactic:
rw [← this.derivWithin (uniqueDiffOn_Ici x x Set.self_mem_Ici)] at f'K

Premises used: HasDerivWithinAt.derivWithin, uniqueDiffOn_Ici, Set.self_mem_Ici
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this_1 : CauchySeq L0
f' : F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
this : HasDerivWithinAt f f' (Ici x) x
f'K₁ : derivWithin f (Ici x) x ∈ K
hf'₁ : Tendsto L0 atTop (𝓝 f')
Lf'₁ : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
⊢ HasDerivWithinAt f f' (Ici x) x

Tactic:
rw [← this.derivWithin (uniqueDiffOn_Ici x x Set.self_mem_Ici)] at f'K

Premises used: HasDerivWithinAt.derivWithin, uniqueDiffOn_Ici, Set.self_mem_Ici
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this_1 : CauchySeq L0
f' : F
f'K : derivWithin f (Ici x) x ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
this : HasDerivWithinAt f f' (Ici x) x
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x

Tactic:
⟨this.differentiableWithinAt, f'K⟩

Premises used: Set.Mem, setOf, HasDerivWithinAt.differentiableWithinAt, And.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
x : ℝ
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → F
hn :
  ∀ (e p q : ℕ),
    n e ≤ p →
      n e ≤ q → L e p q ∈ K ∧ x ∈ A f (L e p q) ((1 / 2) ^ p) ((1 / 2) ^ e) ∩ A f (L e p q) ((1 / 2) ^ q) ((1 / 2) ^ e)
M :
  ∀ (e p q e' p' q' : ℕ), n e ≤ p → n e ≤ q → n e' ≤ p' → n e' ≤ q' → e ≤ e' → ‖L e p q - L e' p' q'‖ ≤ 12 * (1 / 2) ^ e
L0 : ℕ → F := fun (e : ℕ) ↦ L e (n e) (n e)
this_1 : CauchySeq L0
f' : F
f'K : derivWithin f (Ici x) x ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * (1 / 2) ^ e
this : HasDerivWithinAt f f' (Ici x) x
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x

Tactic:
exact ⟨this.differentiableWithinAt, f'K⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
⊢ {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} = D f K

Tactic:
Subset.antisymm (differentiable_set_subset_D _) (D_subset_differentiable_set hK)

Premises used: Set.Subset.antisymm, RightDerivMeasurableAux.D_subset_differentiable_set, RightDerivMeasurableAux.differentiable_set_subset_D
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
simp :
  MeasurableSet (α := ℝ)
    (⋂ (e : ℕ),
      ⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))
⊢ MeasurableSet (α := ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}

Tactic:
simp only [differentiable_set_eq_D K hK, D]

Premises used: RightDerivMeasurableAux.differentiable_set_eq_D, RightDerivMeasurableAux.D
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
apply_rules :
  ∀ (b : ℕ),
    MeasurableSet (α := ℝ)
      (⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ b))
⊢ MeasurableSet (α := ℝ)
    (⋂ (e : ℕ),
      ⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]

Premises used: MeasurableSet.iUnion, MeasurableSet.iInter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b : ℕ
h :
  ∀ (b_1 : ℕ),
    MeasurableSet (α := ℝ)
      (⋂ (p : ℕ), ⋂ (_ : p ≥ b_1), ⋂ (q : ℕ), ⋂ (_ : q ≥ b_1), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ b))
⊢ MeasurableSet (α := ℝ)
    (⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ b))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]

Premises used: MeasurableSet.iUnion, MeasurableSet.iInter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b b_1 : ℕ
h :
  ∀ (b_2 : ℕ),
    MeasurableSet (α := ℝ)
      (⋂ (_ : b_2 ≥ b_1), ⋂ (q : ℕ), ⋂ (_ : q ≥ b_1), B f K ((1 / 2) ^ b_2) ((1 / 2) ^ q) ((1 / 2) ^ b))
⊢ MeasurableSet (α := ℝ)
    (⋂ (p : ℕ), ⋂ (_ : p ≥ b_1), ⋂ (q : ℕ), ⋂ (_ : q ≥ b_1), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ b))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]

Premises used: MeasurableSet.iUnion, MeasurableSet.iInter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b b_1 b_2 : ℕ
h :
  ∀ (b_3 : b_2 ≥ b_1),
    MeasurableSet (α := ℝ) (⋂ (q : ℕ), ⋂ (_ : q ≥ b_1), B f K ((1 / 2) ^ b_2) ((1 / 2) ^ q) ((1 / 2) ^ b))
⊢ MeasurableSet (α := ℝ)
    (⋂ (_ : b_2 ≥ b_1), ⋂ (q : ℕ), ⋂ (_ : q ≥ b_1), B f K ((1 / 2) ^ b_2) ((1 / 2) ^ q) ((1 / 2) ^ b))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]

Premises used: MeasurableSet.iUnion, MeasurableSet.iInter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b b_1 b_2 : ℕ
b_3 : b_2 ≥ b_1
h : ∀ (b_4 : ℕ), MeasurableSet (α := ℝ) (⋂ (_ : b_4 ≥ b_1), B f K ((1 / 2) ^ b_2) ((1 / 2) ^ b_4) ((1 / 2) ^ b))
⊢ MeasurableSet (α := ℝ) (⋂ (q : ℕ), ⋂ (_ : q ≥ b_1), B f K ((1 / 2) ^ b_2) ((1 / 2) ^ q) ((1 / 2) ^ b))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]

Premises used: MeasurableSet.iUnion, MeasurableSet.iInter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b b_1 b_2 : ℕ
b_3 : b_2 ≥ b_1
b_4 : ℕ
h : ∀ (b_5 : b_4 ≥ b_1), MeasurableSet (B f K ((1 / 2) ^ b_2) ((1 / 2) ^ b_4) ((1 / 2) ^ b))
⊢ MeasurableSet (α := ℝ) (⋂ (_ : b_4 ≥ b_1), B f K ((1 / 2) ^ b_2) ((1 / 2) ^ b_4) ((1 / 2) ^ b))

Tactic:
apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]

Premises used: MeasurableSet.iUnion, MeasurableSet.iInter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
h : ∀ (b b_1 b_2 : ℕ), b_2 ≥ b_1 → ∀ b_4 ≥ b_1, MeasurableSet (B f K ((1 / 2) ^ b_2) ((1 / 2) ^ b_4) ((1 / 2) ^ b))
⊢ MeasurableSet (α := ℝ)
    (⋂ (e : ℕ),
      ⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))

Tactic:
repeat apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter] <;> intro

Premises used: MeasurableSet.iUnion, MeasurableSet.iInter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b b_1 b_2 : ℕ
b_3 : b_2 ≥ b_1
b_4 : ℕ
b_5 : b_4 ≥ b_1
⊢ MeasurableSet (B f K ((1 / 2) ^ b_2) ((1 / 2) ^ b_4) ((1 / 2) ^ b))

Tactic:
measurableSet_B

Premises used: RightDerivMeasurableAux.measurableSet_B
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b b_1 b_2 : ℕ
b_3 : b_2 ≥ b_1
b_4 : ℕ
b_5 : b_4 ≥ b_1
⊢ MeasurableSet (B f K ((1 / 2) ^ b_2) ((1 / 2) ^ b_4) ((1 / 2) ^ b))

Tactic:
exact measurableSet_B

Premises used: RightDerivMeasurableAux.measurableSet_B
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
⊢ IsComplete.{u_1} (α := F) univ

Tactic:
have : IsComplete (univ : Set F) := complete_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : IsComplete.{u_1} (α := F) univ
⊢ MeasurableSet (α := ℝ)
    {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ Membership.mem (γ := Set F) univ (derivWithin f (Ici x) x)}

Tactic:
measurableSet_of_differentiableWithinAt_Ici_of_isComplete f this

Premises used: measurableSet_of_differentiableWithinAt_Ici_of_isComplete
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : IsComplete.{u_1} (α := F) univ
h :
  ∀ (x : ℝ),
    DifferentiableWithinAt ℝ f (Ici x) x ↔
      DifferentiableWithinAt ℝ f (Ici x) x ∧ Membership.mem (γ := Set F) univ (derivWithin f (Ici x) x)
⊢ MeasurableSet (α := ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x}

Tactic:
convert! measurableSet_of_differentiableWithinAt_Ici_of_isComplete f this

Premises used: measurableSet_of_differentiableWithinAt_Ici_of_isComplete
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : IsComplete.{u_1} (α := F) univ
x : ℝ
⊢ DifferentiableWithinAt ℝ f (Ici x) x ↔
    DifferentiableWithinAt ℝ f (Ici x) x ∧ Membership.mem (γ := Set F) univ (derivWithin f (Ici x) x)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
inst_3 : MeasurableSpace F
inst_4 : BorelSpace F
⊢ Measurable.{0, u_1} (β := F) fun (x : ℝ) ↦ derivWithin f (Ici x) x

Tactic:
measurable_of_isClosed fun s hs => ?_

Premises used: measurable_of_isClosed
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
inst_3 : MeasurableSpace F
inst_4 : BorelSpace F
refine :
  ∀ (s : Set F) (hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
    MeasurableSet (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Ici x) x) ⁻¹' s)
⊢ Measurable.{0, u_1} (β := F) fun (x : ℝ) ↦ derivWithin f (Ici x) x

Tactic:
refine measurable_of_isClosed fun s hs => ?_

Premises used: measurable_of_isClosed
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
inst_3 : MeasurableSpace F
inst_4 : BorelSpace F
s : Set F
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
⊢ Eq (α := Set ℝ) ((fun (x : ℝ) ↦ derivWithin f (Ici x) x) ⁻¹' s)
    ({x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x : ℝ | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x : ℝ | 0 ∈ s})

Tactic:
have :
    (fun x => derivWithin f (Ici x) x) ⁻¹' s =
      { x | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s } ∪
        { x | ¬DifferentiableWithinAt ℝ f (Ici x) x } ∩ { _x | (0 : F) ∈ s } :=
    Set.ext fun x => mem_preimage.trans derivWithin_mem_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
inst_3 : MeasurableSpace F
inst_4 : BorelSpace F
s : Set F
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
this :
  Eq (α := Set ℝ) ((fun (x : ℝ) ↦ derivWithin f (Ici x) x) ⁻¹' s)
    ({x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x : ℝ | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x : ℝ | 0 ∈ s})
rw :
  MeasurableSet (α := ℝ)
    ({x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x : ℝ | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x : ℝ | 0 ∈ s})
⊢ MeasurableSet (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Ici x) x) ⁻¹' s)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
inst_3 : MeasurableSpace F
inst_4 : BorelSpace F
s : Set F
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
this :
  Eq (α := Set ℝ) ((fun (x : ℝ) ↦ derivWithin f (Ici x) x) ⁻¹' s)
    ({x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x : ℝ | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x : ℝ | 0 ∈ s})
⊢ MeasurableSet (α := ℝ)
    ({x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x : ℝ | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x : ℝ | 0 ∈ s})

Tactic:
(measurableSet_of_differentiableWithinAt_Ici_of_isComplete _ hs.isComplete).union
      ((measurableSet_of_differentiableWithinAt_Ici _).compl.inter (MeasurableSet.const _))

Premises used: measurableSet_of_differentiableWithinAt_Ici_of_isComplete, MeasurableSet.compl, MeasurableSet.const, MeasurableSet.union, IsClosed.isComplete, measurableSet_of_differentiableWithinAt_Ici, MeasurableSet.inter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
inst_3 : MeasurableSpace F
inst_4 : BorelSpace F
s : Set F
hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
this :
  Eq (α := Set ℝ) ((fun (x : ℝ) ↦ derivWithin f (Ici x) x) ⁻¹' s)
    ({x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x : ℝ | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x : ℝ | 0 ∈ s})
⊢ MeasurableSet (α := ℝ)
    ({x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
      {x : ℝ | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x : ℝ | 0 ∈ s})

Tactic:
exact
    (measurableSet_of_differentiableWithinAt_Ici_of_isComplete _ hs.isComplete).union
      ((measurableSet_of_differentiableWithinAt_Ici _).compl.inter (MeasurableSet.const _))

Premises used: measurableSet_of_differentiableWithinAt_Ici_of_isComplete, MeasurableSet.compl, MeasurableSet.const, MeasurableSet.union, IsClosed.isComplete, measurableSet_of_differentiableWithinAt_Ici, MeasurableSet.inter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
⊢ let this := borel F;
  BorelSpace F

Tactic:
borelize F