awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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')‖
⊢ ‖f y - f x - (y - x) • f'‖ ≤ ε * ‖y - x‖
have y₂ : 4 * (1 / 2) ^ e * ‖y - x‖ + ‖y - x‖ * (12 * (1 / 2) ^ e) = 16 * ‖y - x‖ * (1 / 2) ^ e
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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ ‖f y - f x - (y - x) • f'‖ ≤ ε * ‖y - x‖
have y₃ : 16 * ‖y - x‖ * (1 / 2) ^ e ≤ 16 * ‖y - x‖ * (ε / 16)
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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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)
⊢ ‖f y - f x - (y - x) • f'‖ ≤ ε * ‖y - x‖
have y₄ : 16 * ‖y - x‖ * (ε / 16) = ε * ‖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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
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
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K} x
have f'K₁ : derivWithin f (Ici x) x ∈ K
Tactic: rw [← this.derivWithin (uniqueDiffOn_Ici x x Set.self_mem_Ici)] at f'K
Cleared hypotheses: f'K, hf', Lf', this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
⊢ MeasurableSet (α := ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ K}
have simp : MeasurableSet (α := ℝ)
  (⋂ (e : ℕ),
    ⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))
Tactic: simp only [differentiable_set_eq_D K hK, D]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
⊢ MeasurableSet (α := ℝ)
    (⋂ (e : ℕ),
      ⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))
have apply_rules : ∀ (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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b : ℕ
⊢ MeasurableSet (α := ℝ)
    (⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ b))
have h : ∀ (b_1 : ℕ),
  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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
b b_1 : ℕ
⊢ MeasurableSet (α := ℝ)
    (⋂ (p : ℕ), ⋂ (_ : p ≥ b_1), ⋂ (q : ℕ), ⋂ (_ : q ≥ b_1), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ b))
have 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))
Tactic: apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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 : ℕ
⊢ MeasurableSet (α := ℝ)
    (⋂ (_ : b_2 ≥ b_1), ⋂ (q : ℕ), ⋂ (_ : q ≥ b_1), B f K ((1 / 2) ^ b_2) ((1 / 2) ^ q) ((1 / 2) ^ b))
have 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))
Tactic: apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
⊢ MeasurableSet (α := ℝ) (⋂ (q : ℕ), ⋂ (_ : q ≥ b_1), B f K ((1 / 2) ^ b_2) ((1 / 2) ^ q) ((1 / 2) ^ b))
have h : ∀ (b_4 : ℕ), 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]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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 : ℕ
⊢ MeasurableSet (α := ℝ) (⋂ (_ : b_4 ≥ b_1), B f K ((1 / 2) ^ b_2) ((1 / 2) ^ b_4) ((1 / 2) ^ b))
have h : ∀ (b_5 : b_4 ≥ b_1), MeasurableSet (B f K ((1 / 2) ^ b_2) ((1 / 2) ^ b_4) ((1 / 2) ^ b))
Tactic: apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
K : Set F
hK : IsComplete K
⊢ MeasurableSet (α := ℝ)
    (⋂ (e : ℕ),
      ⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))
have 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))
Tactic: repeat apply_rules [MeasurableSet.iUnion, MeasurableSet.iInter] <;> intro
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
⊢ MeasurableSet (α := ℝ) {x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x}
have this : IsComplete.{u_1} (α := F) univ
Tactic: have : IsComplete (univ : Set F) := complete_univ
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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}
have h : ∀ (x : ℝ),
  DifferentiableWithinAt ℝ f (Ici x) x ↔
    DifferentiableWithinAt ℝ f (Ici x) x ∧ Membership.mem (γ := Set F) univ (derivWithin f (Ici x) x)
Tactic: convert! measurableSet_of_differentiableWithinAt_Ici_of_isComplete f this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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
have refine : ∀ (s : Set F) (hs : IsClosed[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s),
  MeasurableSet (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Ici x) x) ⁻¹' s)
Tactic: refine measurable_of_isClosed fun s hs => ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
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
⊢ MeasurableSet (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Ici x) x) ⁻¹' s)
have 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})
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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
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 (α := ℝ) ((fun (x : ℝ) ↦ derivWithin f (Ici x) x) ⁻¹' s)
have rw : MeasurableSet (α := ℝ)
  ({x : ℝ | DifferentiableWithinAt ℝ f (Ici x) x ∧ derivWithin f (Ici x) x ∈ s} ∪
    {x : ℝ | ¬DifferentiableWithinAt ℝ f (Ici x) x} ∩ {_x : ℝ | 0 ∈ s})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
⊢ StronglyMeasurable.{0, u_1} (β := F) fun (x : ℝ) ↦ derivWithin f (Ici x) x
have this : let this := borel F;
BorelSpace F
Tactic: borelize F
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
⊢ StronglyMeasurable.{0, u_1} (β := F) fun (x : ℝ) ↦ derivWithin f (Ici x) x
have apply : IsSeparable.{u_1} (α := F) (range fun (x : ℝ) ↦ derivWithin f (Ici x) x)
Tactic: apply stronglyMeasurable_iff_measurable_separable.2 ⟨measurable_derivWithin_Ici f, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
⊢ IsSeparable.{u_1} (α := F) (range fun (x : ℝ) ↦ derivWithin f (Ici x) x)
have obtain : ∀ (t : Set ℝ) (t_count : t.Countable) (ht : Dense t),
  IsSeparable.{u_1} (α := F) (range fun (x : ℝ) ↦ derivWithin f (Ici x) x)
Tactic: obtain ⟨t, t_count, ht⟩ : ∃ t : Set ℝ, t.Countable ∧ Dense t := exists_countable_dense ℝ
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
⊢ IsSeparable.{u_1} (α := F) (range fun (x : ℝ) ↦ derivWithin f (Ici x) x)
have suffices : (range fun (x : ℝ) ↦ derivWithin f (Ici x) x) ⊆
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span ℝ (f '' t)) : Set F)
Tactic: suffices H : range (fun x ↦ derivWithin f (Ici x) x) ⊆ closure (Submodule.span ℝ (f '' t)) from
    IsSeparable.mono (t_count.image f).isSeparable.span.closure H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
⊢ (fun (x : ℝ) ↦ derivWithin f (Ici x) x) x ∈
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span ℝ (f '' t)) : Set F)
have suffices : (range fun (y : ℝ) ↦ derivWithin f (Ici x) y) ⊆
  closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span ℝ (f '' t)) : Set F)
Tactic: suffices H' : range (fun y ↦ derivWithin f (Ici x) y) ⊆ closure (Submodule.span ℝ (f '' t)) from
    H' (mem_range_self _)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
⊢ (range fun (y : ℝ) ↦ derivWithin f (Ici x) y) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑(Submodule.span ℝ (f '' t)) : Set F)
have h : Ici x ⊆ closure (Ici x ∩ t)
Tactic: apply range_derivWithin_subset_closure_span_image
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
⊢ closure (Ioi x ∩ closure t) ⊆ closure (closure (Ioi x ∩ t))
have h : Ioi x ∩ closure t ⊆ closure (Ioi x ∩ t)
Tactic: apply closure_mono
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
⊢ closure (closure (Ioi x ∩ t)) ⊆ closure (Ici x ∩ t)
have rw : closure (Ioi x ∩ t) ⊆ closure (Ici x ∩ t)
Tactic: rw [closure_closure]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
⊢ Ici x ⊆ closure (Ici x ∩ t)
have calc : Ici x = closure (Ioi x ∩ closure t)
Tactic: calc Ici x
    = closure (Ioi x ∩ closure t) := by simp [dense_iff_closure_eq.1 ht]
  _ ⊆ closure (closure (Ioi x ∩ t)) := by
      apply closure_mono
      simpa [inter_comm] using (isOpen_Ioi (a := x)).closure_inter (s := t)
  _ ⊆ closure (Ici x ∩ t) := by
      rw [closure_closure]
      exact closure_mono (inter_subset_inter_left _ Ioi_subset_Ici_self)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
calc : Ici x = closure (Ioi x ∩ closure t)
⊢ Ici x ⊆ closure (Ici x ∩ t)
have calc₁ : closure (Ioi x ∩ closure t) ⊆ closure (closure (Ioi x ∩ t))
Tactic: calc Ici x
    = closure (Ioi x ∩ closure t) := by simp [dense_iff_closure_eq.1 ht]
  _ ⊆ closure (closure (Ioi x ∩ t)) := by
      apply closure_mono
      simpa [inter_comm] using (isOpen_Ioi (a := x)).closure_inter (s := t)
  _ ⊆ closure (Ici x ∩ t) := by
      rw [closure_closure]
      exact closure_mono (inter_subset_inter_left _ Ioi_subset_Ici_self)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
F : Type u_1
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℝ F
f : ℝ → F
inst_2 : CompleteSpace F
this : MeasurableSpace F := borel F
this_1 : BorelSpace F
t : Set ℝ
t_count : t.Countable
ht : Dense t
x : ℝ
calc : Ici x = closure (Ioi x ∩ closure t)
calc₁ : closure (Ioi x ∩ closure t) ⊆ closure (closure (Ioi x ∩ t))
⊢ Ici x ⊆ closure (Ici x ∩ t)
have calc₂ : closure (closure (Ioi x ∩ t)) ⊆ closure (Ici x ∩ t)
Tactic: calc Ici x
    = closure (Ioi x ∩ closure t) := by simp [dense_iff_closure_eq.1 ht]
  _ ⊆ closure (closure (Ioi x ∩ t)) := by
      apply closure_mono
      simpa [inter_comm] using (isOpen_Ioi (a := x)).closure_inter (s := t)
  _ ⊆ closure (Ici x ∩ t) := by
      rw [closure_closure]
      exact closure_mono (inter_subset_inter_left _ Ioi_subset_Ici_self)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
⊢ IsOpen[instTopologicalSpaceProd] {p : α × E | p.2 ∈ A (f p.1) L r s}
have this : ProperSpace E
Tactic: have : ProperSpace E := .of_locallyCompactSpace 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
⊢ IsOpen[instTopologicalSpaceProd] {p : α × E | p.2 ∈ A (f p.1) L r s}
have simp : IsOpen[instTopologicalSpaceProd]
  {p : α × E |
    ∃ (r' : ℝ),
      (r / 2 < r' ∧ r' ≤ r) ∧
        ∀ (y : E),
          dist y p.2 < r' →
            ∀ (z : E),
              dist z p.2 < r' →
                ‖f p.1 z - f p.1 y - HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                  s * r}
Tactic: simp only [A, mem_Ioc, mem_ball, map_sub, mem_setOf_eq]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Measurable (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : LocallyCompactSpace E
F : Type u_3
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
α : Type u_4
inst_6 : TopologicalSpace α
f : α → E → F
r s : ℝ
hf : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (Function.uncurry f)
L : E →L[𝕜] F
this : ProperSpace E
⊢ IsOpen[instTopologicalSpaceProd]
    {p : α × E |
      ∃ (r' : ℝ),
        (r / 2 < r' ∧ r' ≤ r) ∧
          ∀ (y : E),
            dist y p.2 < r' →
              ∀ (z : E),
                dist z p.2 < r' →
                  ‖f p.1 z - f p.1 y -
                        HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                    s * r}
have apply : ∀ (x : α × E),
  Membership.mem (γ := Set (α × E))
      {p : α × E |
        ∃ (r' : ℝ),
          (r / 2 < r' ∧ r' ≤ r) ∧
            ∀ (y : E),
              dist y p.2 < r' →
                ∀ (z : E),
                  dist z p.2 < r' →
                    ‖f p.1 z - f p.1 y -
                          HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                      s * r}
      x →
    {p : α × E |
        ∃ (r' : ℝ),
          (r / 2 < r' ∧ r' ≤ r) ∧
            ∀ (y : E),
              dist y p.2 < r' →
                ∀ (z : E),
                  dist z p.2 < r' →
                    ‖f p.1 z - f p.1 y -
                          HSub.hSub (α := F) (β := F) ((L : (a : E) → F) z : F) ((L : (a : E) → F) y : F)‖ <
                      s * r} ∈
      𝓝 x
Tactic: apply isOpen_iff_mem_nhds.2