awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s
t : (m : E) → ℝ
ts : ∀ (m : E), x + HSMul.hSMul (α := ℝ) 4 (z + t m • m) ∈ interior s
tpos : ∀ (m : E), 0 < t m
C :
  ∀ (m : E),
    Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) m : E →L[ℝ] F) : (a : E) → F) z : F)
      ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) m : F)
this :
  HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)) +
      t w •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)
          (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)) =
    HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)) +
      t v •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)
          (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
⊢ HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
    HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
have a : HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) +
      (HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
          (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)) +
        t v •
          HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)
            (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))) -
    (HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F) +
      (HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
          (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)) +
        t w •
          HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)
            (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)))) =
  0
Tactic: linear_combination (norm := module) this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s
t : (m : E) → ℝ
ts : ∀ (m : E), x + HSMul.hSMul (α := ℝ) 4 (z + t m • m) ∈ interior s
tpos : ∀ (m : E), 0 < t m
C :
  ∀ (m : E),
    Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) m : E →L[ℝ] F) : (a : E) → F) z : F)
      ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) m : F)
this :
  HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)) +
      t w •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)
          (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)) =
    HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)) +
      t v •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)
          (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
⊢ Eq.{u_2 + 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)
have this₁ : HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
  HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
Tactic: have : (t v * t w) • (f'' v) w = (t v * t w) • (f'' w) v := by
    linear_combination (norm := module) this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
s : Set E
s_conv : Convex ℝ s
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ x ∈ interior s, HasFDerivAt f (f' x) x
x : E
xs : x ∈ s
hx : HasFDerivWithinAt f' f'' (interior s) x
v w y : E
hy : y ∈ interior s
z : E
hz : z = (1 / 4) • (y - x)
A : ∀ (m : E), Tendsto (fun (t : ℝ) ↦ x + HSMul.hSMul (α := ℝ) 4 (z + t • m)) (𝓝 0) (𝓝 y)
B : ∀ (m : E), ∀ᶠ (t : ℝ) in 𝓝[>] 0, x + HSMul.hSMul (α := ℝ) 4 (z + t • m) ∈ interior s
t : (m : E) → ℝ
ts : ∀ (m : E), x + HSMul.hSMul (α := ℝ) 4 (z + t m • m) ∈ interior s
tpos : ∀ (m : E), 0 < t m
C :
  ∀ (m : E),
    Eq.{u_2 + 1} (α := F) ((((f'' : (a : E) → E →L[ℝ] F) m : E →L[ℝ] F) : (a : E) → F) z : F)
      ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) m : F)
this_1 :
  HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)) +
      t w •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)
          (HSMul.hSMul (β := F) (t v) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F)) =
    HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) z : F)
        (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) w : F)) +
      t v •
        HAdd.hAdd (α := F) ((((f'' : (a : E) → E →L[ℝ] F) z : E →L[ℝ] F) : (a : E) → F) v : F)
          (HSMul.hSMul (β := F) (t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F))
this :
  HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) =
    HSMul.hSMul (β := F) (t v * t w) ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) v : F)
⊢ Eq.{u_2 + 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)
have apply : t v * t w ≠ 0
Tactic: apply smul_right_injective F _ this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
⊢ Eq.{u_2 + 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)
have rcases : ∀ (ε : ℝ) (εpos : ε > 0) (hε : Metric.ball x ε ⊆ {x : E | (fun (y : E) ↦ HasFDerivAt f (f' y) y) x}),
  Eq.{u_2 + 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: rcases Metric.mem_nhds_iff.1 hf with ⟨ε, εpos, hε⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ {x : E | (fun (y : E) ↦ HasFDerivAt f (f' y) y) x}
⊢ (interior (Metric.ball x ε)).Nonempty
have rwa : (Metric.ball x ε).Nonempty
Tactic: rwa [Metric.isOpen_ball.interior_eq, Metric.nonempty_ball]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ {x : E | (fun (y : E) ↦ HasFDerivAt f (f' y) y) x}
rwa : (Metric.ball x ε).Nonempty
⊢ (interior (Metric.ball x ε)).Nonempty
have rwa₁ : 0 < ε
Tactic: rwa [Metric.isOpen_ball.interior_eq, Metric.nonempty_ball]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
x : E
f : E → F
f' : E → E →L[ℝ] F
f'' : E →L[ℝ] E →L[ℝ] F
hf : ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f' y) y
hx : HasFDerivAt f' f'' x
v w : E
ε : ℝ
εpos : ε > 0
hε : Metric.ball x ε ⊆ {x : E | (fun (y : E) ↦ HasFDerivAt f (f' y) y) x}
⊢ Eq.{u_2 + 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)
have A : (interior (Metric.ball x ε)).Nonempty
Tactic: have A : (interior (Metric.ball x ε)).Nonempty := by
    rwa [Metric.isOpen_ball.interior_eq, Metric.nonempty_ball]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
have h : ∀ (a : E),
  Membership.mem (γ := Set E)
    {x : E |
      Membership.mem (γ := Set E) {x : E | (fun (y : E) ↦ HasFDerivAt f (f' y) y) x} x →
        Membership.mem (γ := Set E) {x : E | (fun (y : E) ↦ HasFDerivAt f (f'R y) y) x} x}
    a
Tactic: filter_upwards [hf] with y hy using HasFDerivAt.restrictScalars ℝ hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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_1 : LinearMap.CompatibleSMul E F ℝ 𝕜 := ⋯
h_2 : 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''
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x : E |
        Membership.mem (γ := Set E) {x : E | (fun (y : E) ↦ HasFDerivAt f (f' y) y) x} x →
          Membership.mem (γ := Set E) {x : E | (fun (y : E) ↦ HasFDerivAt f (f'R y) y) x} x}
      a
⊢ ∀ᶠ (y : E) in 𝓝 x, HasFDerivAt f (f'R y) y
have h₁ : ∀ (a : E), HasFDerivAt f (f' a) a → HasFDerivAt f (f'R a) a
Tactic: filter_upwards [hf] with y hy using HasFDerivAt.restrictScalars ℝ hy
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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''
⊢ 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)
have hfR : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
have 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)
Tactic: simp only [hasFDerivAt_iff_tendsto] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
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
⊢ 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)
have this : HasFDerivAt f'R f''R x
Tactic: have : HasFDerivAt f'R f''R x := by
    simp only [hasFDerivAt_iff_tendsto] at hx ⊢
    exact hx
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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'' : (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)
have 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)
Tactic: change f''R v w = f''R w v
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
⊢ n ≤ minSmoothness 𝕜 n
have simp : n ≤ if IsRCLikeNormedField 𝕜 then n else ω
Tactic: simp only [minSmoothness]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
⊢ n ≤ if IsRCLikeNormedField 𝕜 then n else ω
have pos : IsRCLikeNormedField 𝕜 → n ≤ n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
pos : IsRCLikeNormedField 𝕜 → n ≤ n
⊢ n ≤ if IsRCLikeNormedField 𝕜 then n else ω
have neg : ¬IsRCLikeNormedField 𝕜 → n ≤ ω
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ∞ω
⊢ minSmoothness 𝕜 (n + m) = minSmoothness 𝕜 n + m
have simp : (if IsRCLikeNormedField 𝕜 then n + m else ω) = (if IsRCLikeNormedField 𝕜 then n else ω) + m
Tactic: simp only [minSmoothness]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ∞ω
⊢ (if IsRCLikeNormedField 𝕜 then n + m else ω) = (if IsRCLikeNormedField 𝕜 then n else ω) + m
have pos : IsRCLikeNormedField 𝕜 → n + m = n + m
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n m : ℕ∞ω
pos : IsRCLikeNormedField 𝕜 → n + m = n + m
⊢ (if IsRCLikeNormedField 𝕜 then n + m else ω) = (if IsRCLikeNormedField 𝕜 then n else ω) + m
have neg : ¬IsRCLikeNormedField 𝕜 → ω = ω + m
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : ℕ∞ω
hmn : m ≤ n
⊢ minSmoothness 𝕜 m ≤ minSmoothness 𝕜 n
have simp : (if IsRCLikeNormedField 𝕜 then m else ω) ≤ if IsRCLikeNormedField 𝕜 then n else ω
Tactic: simp only [minSmoothness]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : ℕ∞ω
hmn : m ≤ n
⊢ (if IsRCLikeNormedField 𝕜 then m else ω) ≤ if IsRCLikeNormedField 𝕜 then n else ω
have pos : IsRCLikeNormedField 𝕜 → m ≤ n
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
m n : ℕ∞ω
hmn : m ≤ n
pos : IsRCLikeNormedField 𝕜 → m ≤ n
⊢ (if IsRCLikeNormedField 𝕜 then m else ω) ≤ if IsRCLikeNormedField 𝕜 then n else ω
have neg : ¬IsRCLikeNormedField 𝕜 → LE.le (α := ℕ∞ω) ω ω
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
⊢ minSmoothness 𝕜 n = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜
have simp : (if IsRCLikeNormedField 𝕜 then n else ω) = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜
Tactic: simp only [minSmoothness]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
⊢ (if IsRCLikeNormedField 𝕜 then n else ω) = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜
have pos : ∀ (h : IsRCLikeNormedField 𝕜), n = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
pos : ∀ (h : IsRCLikeNormedField 𝕜), n = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜
⊢ (if IsRCLikeNormedField 𝕜 then n else ω) = ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜
have neg : ∀ (h : ¬IsRCLikeNormedField 𝕜), Eq (α := ℕ∞ω) ω ∞ ↔ n = ∞ ∧ IsRCLikeNormedField 𝕜
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : minSmoothness 𝕜 (↑m : ℕ∞ω) ≤ n
⊢ ∃ (n' : ℕ∞ω), minSmoothness 𝕜 (↑m : ℕ∞ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
have simp : ∀ (hm : (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n),
  ∃ (n' : ℕ∞ω), (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
Tactic: simp only [minSmoothness] at hm ⊢
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n
⊢ ∃ (n' : ℕ∞ω), (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
have pos : ∀ (h : IsRCLikeNormedField 𝕜), ∃ (n' : ℕ∞ω), (↑m : ℕ∞ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n
pos : ∀ (h : IsRCLikeNormedField 𝕜), ∃ (n' : ℕ∞ω), (↑m : ℕ∞ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
⊢ ∃ (n' : ℕ∞ω), (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
have neg : ∀ (h : ¬IsRCLikeNormedField 𝕜), ∃ (n' : ℕ∞ω), ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n
h : IsRCLikeNormedField 𝕜
⊢ ∃ (n' : ℕ∞ω), (↑m : ℕ∞ω) ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
have hm₁ : (↑m : ℕ∞ω) ≤ n
Tactic: simp only [h, ↓reduceIte] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
n : ℕ∞ω
m : ℕ
hm : (if IsRCLikeNormedField 𝕜 then (↑m : ℕ∞ω) else ω) ≤ n
h : ¬IsRCLikeNormedField 𝕜
⊢ ∃ (n' : ℕ∞ω), ω ≤ n' ∧ n' ≤ n ∧ n' ≠ ∞
have hm₁ : ω ≤ n
Tactic: simp only [h, ↓reduceIte] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Calculus.FDeriv.Symmetric (goal)
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
⊢ IsSymmSndFDerivAt 𝕜 f x
have pos : ∀ (h : IsRCLikeNormedField 𝕜), IsSymmSndFDerivAt 𝕜 f x
Tactic: by_cases h : IsRCLikeNormedField 𝕜