awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → E →L[𝕜] 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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : Membership.mem (γ := Set E) (ball 0 ((1 / 2) ^ (n e + 1))) y
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : ‖y‖ ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < ‖y‖
m_ge : n e ≤ m
km : k = m + 1
J1 : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L e (n e) m : (a : E) → F) (x + y - x) : F)‖ ≤ (1 / 2) ^ e * (1 / 2) ^ m
J2 : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L e (n e) m : (a : E) → F) y : F)‖ ≤ 4 * (1 / 2) ^ e * ‖y‖
⊢ ‖L e (n e) m - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e

Tactic:
exact Lf' _ _ m_ge
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → E →L[𝕜] 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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : Membership.mem (γ := Set E) (ball 0 ((1 / 2) ^ (n e + 1))) y
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : ‖y‖ ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < ‖y‖
m_ge : n e ≤ m
km : k = m + 1
J1 : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L e (n e) m : (a : E) → F) (x + y - x) : F)‖ ≤ (1 / 2) ^ e * (1 / 2) ^ m
J2 : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L e (n e) m : (a : E) → F) y : F)‖ ≤ 4 * (1 / 2) ^ e * ‖y‖
⊢ 4 * (1 / 2) ^ e * ‖y‖ + 12 * ‖c‖ * (1 / 2) ^ e * ‖y‖ = (4 + 12 * ‖c‖) * ‖y‖ * (1 / 2) ^ e

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → E →L[𝕜] 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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : Membership.mem (γ := Set E) (ball 0 ((1 / 2) ^ (n e + 1))) y
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : ‖y‖ ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < ‖y‖
m_ge : n e ≤ m
km : k = m + 1
J1 : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L e (n e) m : (a : E) → F) (x + y - x) : F)‖ ≤ (1 / 2) ^ e * (1 / 2) ^ m
J2 : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L e (n e) m : (a : E) → F) y : F)‖ ≤ 4 * (1 / 2) ^ e * ‖y‖
ha : 0 ≤ (4 + 12 * ‖c‖) * ‖y‖
⊢ (4 + 12 * ‖c‖) * ‖y‖ * (1 / 2) ^ e ≤ (4 + 12 * ‖c‖) * ‖y‖ * (ε / (4 + 12 * ‖c‖))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → E →L[𝕜] 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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : Membership.mem (γ := Set E) (ball 0 ((1 / 2) ^ (n e + 1))) y
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : ‖y‖ ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < ‖y‖
m_ge : n e ≤ m
km : k = m + 1
J1 : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L e (n e) m : (a : E) → F) (x + y - x) : F)‖ ≤ (1 / 2) ^ e * (1 / 2) ^ m
J2 : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L e (n e) m : (a : E) → F) y : F)‖ ≤ 4 * (1 / 2) ^ e * ‖y‖
⊢ (4 + 12 * ‖c‖) * ‖y‖ * (ε / (4 + 12 * ‖c‖)) = ε * ‖y‖

Tactic:
field
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → E →L[𝕜] 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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun (e : ℕ) ↦ L e (n e) (n e)
this : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
ε : ℝ
εpos : 0 < ε
pos : 0 < 4 + 12 * ‖c‖
e : ℕ
he : (1 / 2) ^ e < ε / (4 + 12 * ‖c‖)
y : E
hy : Membership.mem (γ := Set E) (ball 0 ((1 / 2) ^ (n e + 1))) y
y_pos : ¬y = 0
yzero : 0 < ‖y‖
y_lt : ‖y‖ < (1 / 2) ^ (n e + 1)
yone : ‖y‖ ≤ 1
k : ℕ
k_gt : n e < k
m : ℕ := k - 1
h'k : ‖y‖ ≤ (1 / 2) ^ (m + 1)
hk : (1 / 2) ^ (m + 1 + 1) < ‖y‖
m_ge : n e ≤ m
km : k = m + 1
J1 : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L e (n e) m : (a : E) → F) (x + y - x) : F)‖ ≤ (1 / 2) ^ e * (1 / 2) ^ m
J2 : ‖HSub.hSub (β := F) (f (x + y) - f x) ((L e (n e) m : (a : E) → F) y : F)‖ ≤ 4 * (1 / 2) ^ e * ‖y‖
f₁ : 4 * (1 / 2) ^ e * ‖y‖ + 12 * ‖c‖ * (1 / 2) ^ e * ‖y‖ = (4 + 12 * ‖c‖) * ‖y‖ * (1 / 2) ^ e
f₂ : (4 + 12 * ‖c‖) * ‖y‖ * (1 / 2) ^ e ≤ (4 + 12 * ‖c‖) * ‖y‖ * (ε / (4 + 12 * ‖c‖))
f₃ : (4 + 12 * ‖c‖) * ‖y‖ * (ε / (4 + 12 * ‖c‖)) = ε * ‖y‖
⊢ ‖HSub.hSub (β := F) (f (x + y) - f x) ((f' : (a : E) → F) y : F)‖ ≤ ε * ‖y‖

Tactic:
calc
      ‖f (x + y) - f x - f' y‖ = ‖f (x + y) - f x - L e (n e) m y + (L e (n e) m - f') y‖ :=
        congr_arg _ (by simp)
      _ ≤ 4 * (1 / 2) ^ e * ‖y‖ + 12 * ‖c‖ * (1 / 2) ^ e * ‖y‖ :=
        norm_add_le_of_le J2 <| (le_opNorm _ _).trans <| by gcongr; exact Lf' _ _ m_ge
      _ = (4 + 12 * ‖c‖) * ‖y‖ * (1 / 2) ^ e := by ring
      _ ≤ (4 + 12 * ‖c‖) * ‖y‖ * (ε / (4 + 12 * ‖c‖)) := by gcongr
      _ = ε * ‖y‖ := by field

Premises used: Norm.norm, HMul.hMul, ContinuousLinearMap.le_opNorm, HSub.hSub, HDiv.hDiv, congr_arg, HAdd.hAdd, norm_add_le_of_le, LE.le.trans, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → E →L[𝕜] 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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun (e : ℕ) ↦ L e (n e) (n e)
this_1 : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
this : HasFDerivAt f f' x
⊢ fderiv 𝕜 f x ∈ K

Tactic:
rw [← this.fderiv] at f'K

Premises used: HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → E →L[𝕜] 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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun (e : ℕ) ↦ L e (n e) (n e)
this_1 : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
this : HasFDerivAt f f' x
f'K₁ : fderiv 𝕜 f x ∈ K
⊢ Tendsto L0 atTop (𝓝 f')

Tactic:
rw [← this.fderiv] at f'K

Premises used: HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → E →L[𝕜] 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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun (e : ℕ) ↦ L e (n e) (n e)
this_1 : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
this : HasFDerivAt f f' x
f'K₁ : fderiv 𝕜 f x ∈ K
hf'₁ : Tendsto L0 atTop (𝓝 f')
⊢ ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e

Tactic:
rw [← this.fderiv] at f'K

Premises used: HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → E →L[𝕜] 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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun (e : ℕ) ↦ L e (n e) (n e)
this_1 : CauchySeq L0
f' : E →L[𝕜] F
f'K : f' ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
this : HasFDerivAt f f' x
f'K₁ : fderiv 𝕜 f x ∈ K
hf'₁ : Tendsto L0 atTop (𝓝 f')
Lf'₁ : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
⊢ HasFDerivAt f f' x

Tactic:
rw [← this.fderiv] at f'K

Premises used: HasFDerivAt.fderiv
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → E →L[𝕜] 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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun (e : ℕ) ↦ L e (n e) (n e)
this_1 : CauchySeq L0
f' : E →L[𝕜] F
f'K : fderiv 𝕜 f x ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
this : HasFDerivAt f f' x
⊢ Membership.mem (γ := Set E) {x : E | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} x

Tactic:
⟨this.differentiableAt, f'K⟩

Premises used: Set.Mem, setOf, HasFDerivAt.differentiableAt, And.intro
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
P : ∀ {n : ℕ}, 0 < (1 / 2) ^ n
c : 𝕜
hc : 1 < ‖c‖
x : E
hx : x ∈ D f K
n : (e : ℕ) → ℕ
L : (e p q : ℕ) → E →L[𝕜] 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 * ‖c‖ * (1 / 2) ^ e
L0 : ℕ → E →L[𝕜] F := fun (e : ℕ) ↦ L e (n e) (n e)
this_1 : CauchySeq L0
f' : E →L[𝕜] F
f'K : fderiv 𝕜 f x ∈ K
hf' : Tendsto L0 atTop (𝓝 f')
Lf' : ∀ (e p : ℕ), n e ≤ p → ‖L e (n e) p - f'‖ ≤ 12 * ‖c‖ * (1 / 2) ^ e
this : HasFDerivAt f f' x
⊢ Membership.mem (γ := Set E) {x : E | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} x

Tactic:
exact ⟨this.differentiableAt, f'K⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
hK : IsComplete K
⊢ {x : E | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K} = D f K

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

Premises used: Set.Subset.antisymm, FDerivMeasurableAux.differentiable_set_subset_D, FDerivMeasurableAux.D_subset_differentiable_set
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
K : Set (E →L[𝕜] F)
hK : IsComplete K
simp :
  MeasurableSet.{u_2} (α := E)
    (⋂ (e : ℕ),
      ⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))
⊢ MeasurableSet.{u_2} (α := E) {x : E | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ K}

Tactic:
simp only [D, differentiable_set_eq_D K hK]

Premises used: FDerivMeasurableAux.differentiable_set_eq_D, FDerivMeasurableAux.D
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
K : Set (E →L[𝕜] F)
hK : IsComplete K
⊢ MeasurableSet.{u_2} (α := E)
    (⋂ (e : ℕ),
      ⋃ (n : ℕ), ⋂ (p : ℕ), ⋂ (_ : p ≥ n), ⋂ (q : ℕ), ⋂ (_ : q ≥ n), B f K ((1 / 2) ^ p) ((1 / 2) ^ q) ((1 / 2) ^ e))

Tactic:
aesop
    (add safe apply [MeasurableSet.iUnion, MeasurableSet.iInter, isOpen_B])
    (add unsafe IsOpen.measurableSet)

Premises used: IsOpen.measurableSet, ContinuousLinearMap.apply, MeasurableSet.iUnion, FDerivMeasurableAux.isOpen_B, MeasurableSet.iInter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
inst_7 : CompleteSpace F
⊢ IsComplete (α := E →L[𝕜] F) univ

Tactic:
have : IsComplete (univ : Set (E →L[𝕜] F)) := complete_univ
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
inst_7 : CompleteSpace F
this : IsComplete (α := E →L[𝕜] F) univ
⊢ MeasurableSet.{u_2} (α := E)
    {x : E | DifferentiableAt 𝕜 f x ∧ Membership.mem (γ := Set (E →L[𝕜] F)) univ (fderiv 𝕜 f x)}

Tactic:
measurableSet_of_differentiableAt_of_isComplete 𝕜 f this

Premises used: measurableSet_of_differentiableAt_of_isComplete
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
inst_7 : CompleteSpace F
this : IsComplete (α := E →L[𝕜] F) univ
h :
  ∀ (x : E), DifferentiableAt 𝕜 f x ↔ DifferentiableAt 𝕜 f x ∧ Membership.mem (γ := Set (E →L[𝕜] F)) univ (fderiv 𝕜 f x)
⊢ MeasurableSet.{u_2} (α := E) {x : E | DifferentiableAt 𝕜 f x}

Tactic:
convert! measurableSet_of_differentiableAt_of_isComplete 𝕜 f this

Premises used: measurableSet_of_differentiableAt_of_isComplete
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
inst_7 : CompleteSpace F
this : IsComplete (α := E →L[𝕜] F) univ
x : E
⊢ DifferentiableAt 𝕜 f x ↔ DifferentiableAt 𝕜 f x ∧ Membership.mem (γ := Set (E →L[𝕜] F)) univ (fderiv 𝕜 f x)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
inst_7 : CompleteSpace F
⊢ Measurable (β := E →L[𝕜] F) (fderiv 𝕜 f)

Tactic:
measurable_of_isClosed fun s hs => ?_

Premises used: measurable_of_isClosed
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
inst_7 : CompleteSpace F
refine : ∀ (s : Set (E →L[𝕜] F)) (hs : IsClosed s), MeasurableSet (fderiv 𝕜 f ⁻¹' s)
⊢ Measurable (β := E →L[𝕜] F) (fderiv 𝕜 f)

Tactic:
refine measurable_of_isClosed fun s hs => ?_

Premises used: measurable_of_isClosed
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
inst_7 : CompleteSpace F
s : Set (E →L[𝕜] F)
hs : IsClosed s
⊢ fderiv 𝕜 f ⁻¹' s =
    {x : E | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x : E | ¬DifferentiableAt 𝕜 f x} ∩ {_x : E | 0 ∈ s}

Tactic:
have :
    fderiv 𝕜 f ⁻¹' s =
      { x | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s } ∪
        { x | ¬DifferentiableAt 𝕜 f x } ∩ { _x | (0 : E →L[𝕜] F) ∈ s } :=
    Set.ext fun x => mem_preimage.trans fderiv_mem_iff
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
inst_7 : CompleteSpace F
s : Set (E →L[𝕜] F)
hs : IsClosed s
this :
  fderiv 𝕜 f ⁻¹' s =
    {x : E | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x : E | ¬DifferentiableAt 𝕜 f x} ∩ {_x : E | 0 ∈ s}
rw :
  MeasurableSet.{u_2} (α := E)
    ({x : E | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x : E | ¬DifferentiableAt 𝕜 f x} ∩ {_x : E | 0 ∈ s})
⊢ MeasurableSet (fderiv 𝕜 f ⁻¹' s)

Tactic:
rw [this]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
inst_7 : CompleteSpace F
s : Set (E →L[𝕜] F)
hs : IsClosed s
this :
  fderiv 𝕜 f ⁻¹' s =
    {x : E | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x : E | ¬DifferentiableAt 𝕜 f x} ∩ {_x : E | 0 ∈ s}
⊢ MeasurableSet.{u_2} (α := E)
    ({x : E | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x : E | ¬DifferentiableAt 𝕜 f x} ∩ {_x : E | 0 ∈ s})

Tactic:
(measurableSet_of_differentiableAt_of_isComplete _ _ hs.isComplete).union
      ((measurableSet_of_differentiableAt _ _).compl.inter (MeasurableSet.const _))

Premises used: setOf, measurableSet_of_differentiableAt_of_isComplete, MeasurableSet.compl, MeasurableSet.const, measurableSet_of_differentiableAt, MeasurableSet.union, IsClosed.isComplete, MeasurableSet.inter
-- Module: Mathlib.Analysis.Calculus.FDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : MeasurableSpace E
inst_6 : OpensMeasurableSpace E
inst_7 : CompleteSpace F
s : Set (E →L[𝕜] F)
hs : IsClosed s
this :
  fderiv 𝕜 f ⁻¹' s =
    {x : E | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x : E | ¬DifferentiableAt 𝕜 f x} ∩ {_x : E | 0 ∈ s}
⊢ MeasurableSet.{u_2} (α := E)
    ({x : E | DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s} ∪ {x : E | ¬DifferentiableAt 𝕜 f x} ∩ {_x : E | 0 ∈ s})

Tactic:
exact
    (measurableSet_of_differentiableAt_of_isComplete _ _ hs.isComplete).union
      ((measurableSet_of_differentiableAt _ _).compl.inter (MeasurableSet.const _))

Premises used: measurableSet_of_differentiableAt_of_isComplete, MeasurableSet.compl, MeasurableSet.const, measurableSet_of_differentiableAt, MeasurableSet.union, IsClosed.isComplete, MeasurableSet.inter