awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
h : LinearMap.CompatibleSMul E F ℝ 𝕜 := ⋯
h_1 : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := ⋯
f'R : E → E →L[ℝ] F := fun (x : E) ↦ ContinuousLinearMap.restrictScalars ℝ (f' x)
f''R : E →L[ℝ] E →L[ℝ] F := ContinuousLinearMap.bilinearRestrictScalars ℝ f''
⊢ ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y

Tactic:
have hfR : ∀ᶠ y in 𝓝 x, HasFDerivAt f (f'R y) y := by
    filter_upwards [hf] with y hy using HasFDerivAt.restrictScalars ℝ hy
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
h : LinearMap.CompatibleSMul E F ℝ 𝕜 := ⋯
h_1 : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := ⋯
f'R : E → E →L[ℝ] F := fun (x : E) ↦ ContinuousLinearMap.restrictScalars ℝ (f' x)
f''R : E →L[ℝ] E →L[ℝ] F := ContinuousLinearMap.bilinearRestrictScalars ℝ f''
hfR : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
simp :
  ∀
    (hx :
      Tendsto (β := ℝ)
        (fun (x' : E) ↦
          ‖x' - x‖⁻¹ * ‖HSub.hSub (β := E →L[𝕜] F) (f' x' - f' x) ((f'' : (a : E) → E →L[𝕜] F) (x' - x) : E →L[𝕜] F)‖)
        (𝓝 x) (𝓝 0)),
    Tendsto (β := ℝ)
      (fun (x' : E) ↦
        ‖x' - x‖⁻¹ * ‖HSub.hSub (β := E →L[ℝ] F) (f'R x' - f'R x) ((f''R : (a : E) → E →L[ℝ] F) (x' - x) : E →L[ℝ] F)‖)
      (𝓝 x) (𝓝 0)
⊢ HasFDerivAt f'R f''R x

Tactic:
simp only [hasFDerivAt_iff_tendsto] at hx ⊢

Premises used: hasFDerivAt_iff_tendsto
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
v w : E
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
h : LinearMap.CompatibleSMul E F ℝ 𝕜 := ⋯
h_1 : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := ⋯
f'R : E → E →L[ℝ] F := fun (x : E) ↦ ContinuousLinearMap.restrictScalars ℝ (f' x)
f''R : E →L[ℝ] E →L[ℝ] F := ContinuousLinearMap.bilinearRestrictScalars ℝ f''
hfR : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
hx :
  Tendsto (β := ℝ)
    (fun (x' : E) ↦
      ‖x' - x‖⁻¹ * ‖HSub.hSub (β := E →L[𝕜] F) (f' x' - f' x) ((f'' : (a : E) → E →L[𝕜] F) (x' - x) : E →L[𝕜] F)‖)
    (𝓝 x) (𝓝 0)
⊢ Tendsto (β := ℝ)
    (fun (x' : E) ↦
      ‖x' - x‖⁻¹ * ‖HSub.hSub (β := E →L[ℝ] F) (f'R x' - f'R x) ((f''R : (a : E) → E →L[ℝ] F) (x' - x) : E →L[ℝ] F)‖)
    (𝓝 x) (𝓝 0)

Tactic:
hx

Premises used: setOf, ContinuousLinearMap.opNorm
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
v w : E
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
h : LinearMap.CompatibleSMul E F ℝ 𝕜 := ⋯
h_1 : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := ⋯
f'R : E → E →L[ℝ] F := fun (x : E) ↦ ContinuousLinearMap.restrictScalars ℝ (f' x)
f''R : E →L[ℝ] E →L[ℝ] F := ContinuousLinearMap.bilinearRestrictScalars ℝ f''
hfR : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
hx :
  Tendsto (β := ℝ)
    (fun (x' : E) ↦
      ‖x' - x‖⁻¹ * ‖HSub.hSub (β := E →L[𝕜] F) (f' x' - f' x) ((f'' : (a : E) → E →L[𝕜] F) (x' - x) : E →L[𝕜] F)‖)
    (𝓝 x) (𝓝 0)
⊢ Tendsto (β := ℝ)
    (fun (x' : E) ↦
      ‖x' - x‖⁻¹ * ‖HSub.hSub (β := E →L[ℝ] F) (f'R x' - f'R x) ((f''R : (a : E) → E →L[ℝ] F) (x' - x) : E →L[ℝ] F)‖)
    (𝓝 x) (𝓝 0)

Tactic:
exact hx
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
h : LinearMap.CompatibleSMul E F ℝ 𝕜 := ⋯
h_1 : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := ⋯
f'R : E → E →L[ℝ] F := fun (x : E) ↦ ContinuousLinearMap.restrictScalars ℝ (f' x)
f''R : E →L[ℝ] E →L[ℝ] F := ContinuousLinearMap.bilinearRestrictScalars ℝ f''
hfR : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
⊢ HasFDerivAt f'R f''R x

Tactic:
have : HasFDerivAt f'R f''R x := by
    simp only [hasFDerivAt_iff_tendsto] at hx ⊢
    exact hx
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
h : LinearMap.CompatibleSMul E F ℝ 𝕜 := ⋯
h_1 : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := ⋯
f'R : E → E →L[ℝ] F := fun (x : E) ↦ ContinuousLinearMap.restrictScalars ℝ (f' x)
f''R : E →L[ℝ] E →L[ℝ] F := ContinuousLinearMap.bilinearRestrictScalars ℝ f''
hfR : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
this : HasFDerivAt f'R f''R x
change :
  Eq.{u_3 + 1} (α := F) ((((f''R : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
    ((((f''R : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
⊢ Eq.{u_3 + 1} (α := F) ((((f'' : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((f'' : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
change f''R v w = f''R w v

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
h : LinearMap.CompatibleSMul E F ℝ 𝕜 := ⋯
h_1 : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := ⋯
f'R : E → E →L[ℝ] F := fun (x : E) ↦ ContinuousLinearMap.restrictScalars ℝ (f' x)
f''R : E →L[ℝ] E →L[ℝ] F := ContinuousLinearMap.bilinearRestrictScalars ℝ f''
hfR : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
this : HasFDerivAt f'R f''R x
⊢ Eq.{u_3 + 1} (α := F) ((((f''R : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
    ((((f''R : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)

Tactic:
second_derivative_symmetric_of_eventually_of_real hfR this v w

Premises used: second_derivative_symmetric_of_eventually_of_real
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
x : E
f'' : E →L[𝕜] E →L[𝕜] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
x_1 : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
x_2 : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
x_3 : NormedSpace ℝ F := NormedSpace.restrictScalars ℝ 𝕜 F
h : LinearMap.CompatibleSMul E F ℝ 𝕜 := ⋯
h_1 : LinearMap.CompatibleSMul E (E →L[𝕜] F) ℝ 𝕜 := ⋯
f'R : E → E →L[ℝ] F := fun (x : E) ↦ ContinuousLinearMap.restrictScalars ℝ (f' x)
f''R : E →L[ℝ] E →L[ℝ] F := ContinuousLinearMap.bilinearRestrictScalars ℝ f''
hfR : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
this : HasFDerivAt f'R f''R x
⊢ Eq.{u_3 + 1} (α := F) ((((f''R : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)
    ((((f''R : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)

Tactic:
exact second_derivative_symmetric_of_eventually_of_real hfR this v w

Premises used: second_derivative_symmetric_of_eventually_of_real
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
inst_5 : IsRCLikeNormedField 𝕜
f' : E → E →L[𝕜] F
f'' : E →L[𝕜] E →L[𝕜] F
x : E
hf : ∀ (y : E), HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
⊢ Eq.{u_3 + 1} (α := F) ((((f'' : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((f'' : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
second_derivative_symmetric_of_eventually (Filter.Eventually.of_forall hf) hx v w

Premises used: Filter.Eventually.of_forall, second_derivative_symmetric_of_eventually
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
h : IsRCLikeNormedField 𝕜
n : ℕ∞ω
⊢ minSmoothness 𝕜 n = n

Tactic:
simp [minSmoothness, h]

Premises used: minSmoothness
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
simp : n ≤ if IsRCLikeNormedField 𝕜 then n else ω
⊢ n ≤ minSmoothness 𝕜 n

Tactic:
simp only [minSmoothness]

Premises used: minSmoothness
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
pos : IsRCLikeNormedField 𝕜 → n ≤ n
neg : ¬IsRCLikeNormedField 𝕜 → n ≤ ω
⊢ n ≤ if IsRCLikeNormedField 𝕜 then n else ω

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
h : IsRCLikeNormedField 𝕜
⊢ n ≤ n

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
h : ¬IsRCLikeNormedField 𝕜
⊢ n ≤ ω

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ∞ω
simp : (if IsRCLikeNormedField 𝕜 then n + m else ω) = (if IsRCLikeNormedField 𝕜 then n else ω) + m
⊢ minSmoothness 𝕜 (n + m) = minSmoothness 𝕜 n + m

Tactic:
simp only [minSmoothness]

Premises used: minSmoothness
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ∞ω
pos : IsRCLikeNormedField 𝕜 → n + m = n + m
neg : ¬IsRCLikeNormedField 𝕜 → ω = ω + m
⊢ (if IsRCLikeNormedField 𝕜 then n + m else ω) = (if IsRCLikeNormedField 𝕜 then n else ω) + m

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ∞ω
h : IsRCLikeNormedField 𝕜
⊢ n + m = n + m

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ∞ω
h : ¬IsRCLikeNormedField 𝕜
⊢ ω = ω + m

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : ℕ∞ω
hmn : m ≤ n
simp : (if IsRCLikeNormedField 𝕜 then m else ω) ≤ if IsRCLikeNormedField 𝕜 then n else ω
⊢ minSmoothness 𝕜 m ≤ minSmoothness 𝕜 n

Tactic:
simp only [minSmoothness]

Premises used: minSmoothness
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : ℕ∞ω
hmn : m ≤ n
pos : IsRCLikeNormedField 𝕜 → m ≤ n
neg : ¬IsRCLikeNormedField 𝕜 → LE.le (α := ℕ∞ω) ω ω
⊢ (if IsRCLikeNormedField 𝕜 then m else ω) ≤ if IsRCLikeNormedField 𝕜 then n else ω

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : ℕ∞ω
hmn : m ≤ n
h : IsRCLikeNormedField 𝕜
⊢ m ≤ n

Tactic:
simp [hmn]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : ℕ∞ω
hmn : m ≤ n
h : ¬IsRCLikeNormedField 𝕜
⊢ LE.le (α := ℕ∞ω) ω ω

Tactic:
simp [hmn]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
simp : (if IsRCLikeNormedField 𝕜 then n else ω) = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜
⊢ minSmoothness 𝕜 n = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜

Tactic:
simp only [minSmoothness]

Premises used: minSmoothness
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
pos : ∀ (h : IsRCLikeNormedField 𝕜), n = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜
neg : ∀ (h : ¬IsRCLikeNormedField 𝕜), Eq (α := ℕ∞ω) ω ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜
⊢ (if IsRCLikeNormedField 𝕜 then n else ω) = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
h : IsRCLikeNormedField 𝕜
⊢ n = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
h : ¬IsRCLikeNormedField 𝕜
⊢ Eq (α := ℕ∞ω) ω ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : minSmoothness 𝕜 (↑m : ℕ∞ω) ≤ n
simp :
  ∀ (hm : (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n),
    ∃ (n' : ℕ∞ω), (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
⊢ ∃ (n' : ℕ∞ω), minSmoothness 𝕜 (↑m : ℕ∞ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
simp only [minSmoothness] at hm ⊢

Premises used: minSmoothness
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n
pos : ∀ (h : IsRCLikeNormedField 𝕜), ∃ (n' : ℕ∞ω), (↑m : ℕ∞ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
neg : ∀ (h : ¬IsRCLikeNormedField 𝕜), ∃ (n' : ℕ∞ω), ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
⊢ ∃ (n' : ℕ∞ω), (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n
h : IsRCLikeNormedField 𝕜
⊢ (↑m : ℕ∞ω) ≤ n

Tactic:
simp only [h, ↓reduceIte] at hm

Premises used: reduceIte
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
h : IsRCLikeNormedField 𝕜
hm : (↑m : ℕ∞ω) ≤ n
⊢ Ne (α := ℕ∞ω) (↑m : ℕ∞ω) ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
h : IsRCLikeNormedField 𝕜
hm : (↑m : ℕ∞ω) ≤ n
⊢ ∃ (n' : ℕ∞ω), (↑m : ℕ∞ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
exact ⟨m, le_rfl, hm, by simp⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n
h : ¬IsRCLikeNormedField 𝕜
⊢ ω ≤ n

Tactic:
simp only [h, ↓reduceIte] at hm

Premises used: reduceIte
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
h : ¬IsRCLikeNormedField 𝕜
hm : ω ≤ n
⊢ ω ≤ n

Tactic:
simp [hm]
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
h : ¬IsRCLikeNormedField 𝕜
hm : ω ≤ n
⊢ Ne (α := ℕ∞ω) ω ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
h : ¬IsRCLikeNormedField 𝕜
hm : ω ≤ n
⊢ ∃ (n' : ℕ∞ω), ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞

Tactic:
refine ⟨ω, le_rfl, by simp [hm], by simp⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
pos : ∀ (h : IsRCLikeNormedField 𝕜), IsSymmSndFDerivAt 𝕜 f x
neg : ∀ (h : ¬IsRCLikeNormedField 𝕜), IsSymmSndFDerivAt 𝕜 f x
⊢ IsSymmSndFDerivAt 𝕜 f x

Tactic:
by_cases h : IsRCLikeNormedField 𝕜

Premises used: IsRCLikeNormedField
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
pos : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (fderiv 𝕜 f y) y
pos₁ : HasFDerivAt (F := E →L[𝕜] F) (fderiv 𝕜 f) (fderiv 𝕜 (fderiv 𝕜 f) x) x
⊢ Eq.{u_3 + 1} (α := F) ((((fderiv 𝕜 (fderiv 𝕜 f) x : (a : E) → E →L[𝕜] F) v : E →L[𝕜] F) : (a : E) → F) w : F)
    ((((fderiv 𝕜 (fderiv 𝕜 f) x : (a : E) → E →L[𝕜] F) w : E →L[𝕜] F) : (a : E) → F) v : F)

Tactic:
apply second_derivative_symmetric_of_eventually (f := f) (f' := fderiv 𝕜 f) (x := x)

Premises used: second_derivative_symmetric_of_eventually
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
⊢ Eq (α := ℕ∞ω) 2 ∞ → minSmoothness 𝕜 2 = ω

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
pos : ∀ (u : Set E) (hu : u ∈ 𝓝 x) (h'u : ContDiffOn 𝕜 2 f u), ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (fderiv 𝕜 f y) y
⊢ ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (fderiv 𝕜 f y) y

Tactic:
obtain ⟨u, hu, h'u⟩ : ∃ u ∈ 𝓝 x, ContDiffOn 𝕜 2 f u :=
        (hf.of_le hn).contDiffOn (m := 2) le_minSmoothness (by simp)

Premises used: le_minSmoothness, nhds, ContDiffAt.contDiffOn, ContDiffAt.of_le
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v w : E
u : Set E
hu : u ∈ 𝓝 x
h'u : ContDiffOn 𝕜 2 f u
pos :
  ∀ (v : Set E) (vu : v ⊆ u) (v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v) (xv : x ∈ v),
    ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (fderiv 𝕜 f y) y
⊢ ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (fderiv 𝕜 f y) y

Tactic:
rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, xv⟩

Premises used: mem_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v_1 w : E
u : Set E
hu : u ∈ 𝓝 x
h'u : ContDiffOn 𝕜 2 f u
v : Set E
vu : v ⊆ u
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
xv : x ∈ v
h₁ : ∀ (y : E) (hy : y ∈ v), HasFDerivAt f (fderiv 𝕜 f y) y
⊢ ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (fderiv 𝕜 f y) y

Tactic:
filter_upwards [v_open.mem_nhds xv] with y hy

Premises used: IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v_1 w : E
u : Set E
hu : u ∈ 𝓝 x
h'u : ContDiffOn 𝕜 2 f u
v : Set E
vu : v ⊆ u
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
xv : x ∈ v
y : E
hy : y ∈ v
⊢ ContDiffAt 𝕜 2 f y

Tactic:
have := (h'u.mono vu y hy).contDiffAt (v_open.mem_nhds hy)
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v_1 w : E
u : Set E
hu : u ∈ 𝓝 x
h'u : ContDiffOn 𝕜 2 f u
v : Set E
vu : v ⊆ u
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
xv : x ∈ v
y : E
hy : y ∈ v
this : ContDiffAt 𝕜 2 f y
⊢ DifferentiableAt 𝕜 f y

Tactic:
this.differentiableAt two_ne_zero

Premises used: ContDiffAt.differentiableAt, two_ne_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v_1 w : E
u : Set E
hu : u ∈ 𝓝 x
h'u : ContDiffOn 𝕜 2 f u
v : Set E
vu : v ⊆ u
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
xv : x ∈ v
y : E
hy : y ∈ v
this : ContDiffAt 𝕜 2 f y
⊢ DifferentiableAt 𝕜 f y

Tactic:
exact this.differentiableAt two_ne_zero

Premises used: ContDiffAt.differentiableAt, two_ne_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v_1 w : E
u : Set E
hu : u ∈ 𝓝 x
h'u : ContDiffOn 𝕜 2 f u
v : Set E
vu : v ⊆ u
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
xv : x ∈ v
y : E
hy : y ∈ v
⊢ DifferentiableAt 𝕜 f y

Tactic:
have : DifferentiableAt 𝕜 f y := by
        have := (h'u.mono vu y hy).contDiffAt (v_open.mem_nhds hy)
        exact this.differentiableAt two_ne_zero
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
n : ℕ∞ω
hf : ContDiffAt 𝕜 n f x
hn : minSmoothness 𝕜 2 ≤ n
h : IsRCLikeNormedField 𝕜
v_1 w : E
u : Set E
hu : u ∈ 𝓝 x
h'u : ContDiffOn 𝕜 2 f u
v : Set E
vu : v ⊆ u
v_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] v
xv : x ∈ v
y : E
hy : y ∈ v
this : DifferentiableAt 𝕜 f y
⊢ HasFDerivAt f (fderiv 𝕜 f y) y

Tactic:
DifferentiableAt.hasFDerivAt this

Premises used: DifferentiableAt.hasFDerivAt