awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : E) in 𝓝[interior s] x,
        ‖HSub.hSub (β := E →L[ℝ] F) (f' x_1 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_1 - x) : E →L[ℝ] F)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ :
  Metric.ball x δ ∩ interior s ⊆
    {x_1 : E |
      (fun (x_2 : E) ↦
          ‖HSub.hSub (β := E →L[ℝ] F) (f' x_2 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_2 - x) : E →L[ℝ] F)‖ ≤
            ε * ‖x_2 - x‖)
        x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
xt_mem : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → x + h • v + (t * h) • w ∈ interior s
g : (t : ℝ) → F :=
  fun (t : ℝ) ↦
    f (x + h • v + (t * h) • w) - HSMul.hSMul (β := F) (t * h) ((f' x : (a : E) → F) w : F) -
        HSMul.hSMul (β := F) (t * HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
      HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) (t * h) 2 / 2)
        ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)
g' : (t : ℝ) → F :=
  fun (t : ℝ) ↦
    HSub.hSub (α := F) ((f' (x + h • v + (t * h) • w) : (a : E) → F) (h • w) : F)
          (HSMul.hSMul (β := F) h ((f' x : (a : E) → F) w : F)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
      HSMul.hSMul (β := F) (t * HPow.hPow (β := ℕ) h 2)
        ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)
hg' :
  g' = fun (t : ℝ) ↦
    HSub.hSub (α := F) ((f' (x + h • v + (t * h) • w) : (a : E) → F) (h • w) : F)
          (HSMul.hSMul (β := F) h ((f' x : (a : E) → F) w : F)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
      HSMul.hSMul (β := F) (t * HPow.hPow (β := ℕ) h 2)
        ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)
g_deriv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivWithinAt g (g' t) (Icc 0 1) t
g'_bound :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ico 0 1) t → ‖g' t‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * HPow.hPow (β := ℕ) h 2
I : ‖g 1 - g 0‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * HPow.hPow (β := ℕ) h 2
h₁ : ε * ((‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) h 2) = ε * ((‖v‖ + ‖w‖) * ‖w‖) * HPow.hPow (β := ℕ) h 2
⊢ ε * ‖(‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) h 2‖ = ε * ((‖v‖ + ‖w‖) * ‖w‖) * HPow.hPow (β := ℕ) h 2

Tactic:
simp (discharger := positivity) only [Real.norm_eq_abs, abs_of_nonneg]

Premises used: abs_of_nonneg, Real.norm_eq_abs
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 :
  ∀ ⦃c : ℝ⦄,
    0 < c →
      ∀ᶠ (x_1 : E) in 𝓝[interior s] x,
        ‖HSub.hSub (β := E →L[ℝ] F) (f' x_1 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_1 - x) : E →L[ℝ] F)‖ ≤ c * ‖x_1 - x‖
v w : E
hv : x + v ∈ interior s
hw : x + v + w ∈ interior s
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : δ > 0
sδ :
  Metric.ball x δ ∩ interior s ⊆
    {x_1 : E |
      (fun (x_2 : E) ↦
          ‖HSub.hSub (β := E →L[ℝ] F) (f' x_2 - f' x) ((f'' : (a : E) → E →L[ℝ] F) (x_2 - x) : E →L[ℝ] F)‖ ≤
            ε * ‖x_2 - x‖)
        x_1}
E1 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h * (‖v‖ + ‖w‖) < δ
E2 : ∀ᶠ (h : ℝ) in 𝓝[>] 0, h < 1
h : ℝ
hδ : h * (‖v‖ + ‖w‖) < δ
h_lt_1 : h < 1
hpos : 0 < h
xt_mem : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → x + h • v + (t * h) • w ∈ interior s
g : (t : ℝ) → F :=
  fun (t : ℝ) ↦
    f (x + h • v + (t * h) • w) - HSMul.hSMul (β := F) (t * h) ((f' x : (a : E) → F) w : F) -
        HSMul.hSMul (β := F) (t * HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
      HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) (t * h) 2 / 2)
        ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)
g' : (t : ℝ) → F :=
  fun (t : ℝ) ↦
    HSub.hSub (α := F) ((f' (x + h • v + (t * h) • w) : (a : E) → F) (h • w) : F)
          (HSMul.hSMul (β := F) h ((f' x : (a : E) → F) w : F)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
      HSMul.hSMul (β := F) (t * HPow.hPow (β := ℕ) h 2)
        ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)
hg' :
  g' = fun (t : ℝ) ↦
    HSub.hSub (α := F) ((f' (x + h • v + (t * h) • w) : (a : E) → F) (h • w) : F)
          (HSMul.hSMul (β := F) h ((f' x : (a : E) → F) w : F)) -
        HSMul.hSMul (β := F) (HPow.hPow (β := ℕ) h 2)
          ((((f'' : (a : E) → E →L[ℝ] F) v : E →L[ℝ] F) : (a : E) → F) w : F) -
      HSMul.hSMul (β := F) (t * HPow.hPow (β := ℕ) h 2)
        ((((f'' : (a : E) → E →L[ℝ] F) w : E →L[ℝ] F) : (a : E) → F) w : F)
g_deriv : ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Icc 0 1) t → HasDerivWithinAt g (g' t) (Icc 0 1) t
g'_bound :
  ∀ (t : ℝ), Membership.mem (γ := Set ℝ) (Ico 0 1) t → ‖g' t‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * HPow.hPow (β := ℕ) h 2
I : ‖g 1 - g 0‖ ≤ ε * ((‖v‖ + ‖w‖) * ‖w‖) * HPow.hPow (β := ℕ) h 2
⊢ ε * ((‖v‖ + ‖w‖) * ‖w‖ * HPow.hPow (β := ℕ) h 2) = ε * ((‖v‖ + ‖w‖) * ‖w‖) * HPow.hPow (β := ℕ) h 2

Tactic:
ring
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
⊢ 0 < 1 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
⊢ 1 / 2 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
⊢ Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)

Tactic:
have A : (1 : ℝ) / 2 ∈ Ioc (0 : ℝ) 1 := ⟨by simp, by norm_num⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
⊢ 0 ≤ 1 / 2

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
⊢ 1 / 2 ≤ 1

Tactic:
norm_num
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)

Tactic:
have B : (1 : ℝ) / 2 ∈ Icc (0 : ℝ) 1 := ⟨by simp, by norm_num⟩
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
⊢ x + HSMul.hSMul (α := ℝ) 4 v + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 4 w - (x + HSMul.hSMul (α := ℝ) 4 v)) ∈ interior s

Tactic:
s_conv.interior.add_smul_sub_mem h4v h4w B

Premises used: Convex.interior, Convex.add_smul_sub_mem
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h :
  x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w =
    x + HSMul.hSMul (α := ℝ) 4 v + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 4 w - (x + HSMul.hSMul (α := ℝ) 4 v))
⊢ x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s

Tactic:
convert! s_conv.interior.add_smul_sub_mem h4v h4w B using 1

Premises used: Convex.interior, Convex.add_smul_sub_mem
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
⊢ x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w =
    x + HSMul.hSMul (α := ℝ) 4 v + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 4 w - (x + HSMul.hSMul (α := ℝ) 4 v))

Tactic:
module
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
⊢ x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s

Tactic:
have h2v2w : x + (2 : ℝ) • v + (2 : ℝ) • w ∈ interior s := by
    convert! s_conv.interior.add_smul_sub_mem h4v h4w B using 1
    module
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
⊢ x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s

Tactic:
h2v2w
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w = x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w
⊢ x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s

Tactic:
convert! h2v2w using 1
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
⊢ x + (HSMul.hSMul (α := ℕ) 2 v + w) + w = x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w

Tactic:
module
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
⊢ x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s

Tactic:
have h2vww : x + (2 • v + w) + w ∈ interior s := by
    convert! h2v2w using 1
    module
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
⊢ x + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 4 v - x) ∈ interior s

Tactic:
s_conv.add_smul_sub_mem_interior xs h4v A

Premises used: Convex.add_smul_sub_mem_interior
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h : x + HSMul.hSMul (α := ℝ) 2 v = x + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 4 v - x)
⊢ x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s

Tactic:
convert! s_conv.add_smul_sub_mem_interior xs h4v A using 1

Premises used: Convex.add_smul_sub_mem_interior
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
⊢ x + HSMul.hSMul (α := ℝ) 2 v = x + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 4 v - x)

Tactic:
module
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
⊢ x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s

Tactic:
have h2v : x + (2 : ℝ) • v ∈ interior s := by
    convert! s_conv.add_smul_sub_mem_interior xs h4v A using 1
    module
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
⊢ x + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 4 w - x) ∈ interior s

Tactic:
s_conv.add_smul_sub_mem_interior xs h4w A

Premises used: Convex.add_smul_sub_mem_interior
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h : x + HSMul.hSMul (α := ℝ) 2 w = x + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 4 w - x)
⊢ x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s

Tactic:
convert! s_conv.add_smul_sub_mem_interior xs h4w A using 1

Premises used: Convex.add_smul_sub_mem_interior
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
⊢ x + HSMul.hSMul (α := ℝ) 2 w = x + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 4 w - x)

Tactic:
module
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
⊢ x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s

Tactic:
have h2w : x + (2 : ℝ) • w ∈ interior s := by
    convert! s_conv.add_smul_sub_mem_interior xs h4w A using 1
    module
-- Module: Mathlib.Analysis.Calculus.FDeriv.Symmetric
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 : E
h4v : x + HSMul.hSMul (α := ℝ) 4 v ∈ interior s
h4w : x + HSMul.hSMul (α := ℝ) 4 w ∈ interior s
A : Membership.mem (γ := Set ℝ) (Ioc 0 1) (1 / 2)
B : Membership.mem (γ := Set ℝ) (Icc 0 1) (1 / 2)
h2v2w : x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
h2vww : x + (HSMul.hSMul (α := ℕ) 2 v + w) + w ∈ interior s
h2v : x + HSMul.hSMul (α := ℝ) 2 v ∈ interior s
h2w : x + HSMul.hSMul (α := ℝ) 2 w ∈ interior s
⊢ x + (1 / 2) • (x + HSMul.hSMul (α := ℝ) 2 v + HSMul.hSMul (α := ℝ) 2 w - x) ∈ interior s

Tactic:
s_conv.add_smul_sub_mem_interior xs h2v2w A

Premises used: Convex.add_smul_sub_mem_interior