awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (goal)
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_2} (α := F) fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) x
this :
  g =
    Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
h2x : Membership.mem (α := E) (tsupport f) ((L.symm : (a : E' × ℝ) → E) x : E)
hg :
  HasLineDerivAt ℝ
    (Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ))
    (g' ((L.symm : (a : E' × ℝ) → E) x)) ((L.symm : (a : E' × ℝ) → E) x) v
h : x = ((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) ((L.symm : (a : E' × ℝ) → E) x)
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) (g' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)
have h₁ : Eq (α := E' × ℝ) (0, 1) (((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) v)
Tactic: convert! hg.of_comp using 1
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
hf : Continuous f
⊢ MeasurableSet.{u_2} (α := E) {x : E | LineDifferentiableAt 𝕜 f x v}
have this : let this := borel 𝕜;
BorelSpace 𝕜
Tactic: borelize 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
⊢ MeasurableSet.{u_2} (α := E) {x : E | LineDifferentiableAt 𝕜 f x v}
have hg : Continuous (Function.uncurry g)
Tactic: have hg : Continuous g.uncurry := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : MeasurableSpace F
inst_10 : BorelSpace F
hf : Continuous f
⊢ Measurable.{u_2, u_3} (β := F) fun (x : E) ↦ lineDeriv 𝕜 f x v
have this : let this := borel 𝕜;
BorelSpace 𝕜
Tactic: borelize 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : MeasurableSpace F
inst_10 : BorelSpace F
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
⊢ Measurable.{u_2, u_3} (β := F) fun (x : E) ↦ lineDeriv 𝕜 f x v
have hg : Continuous (Function.uncurry g)
Tactic: have hg : Continuous g.uncurry := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : SecondCountableTopologyEither E F
hf : Continuous f
⊢ StronglyMeasurable.{u_2, u_3} (β := F) fun (x : E) ↦ lineDeriv 𝕜 f x v
have this : let this := borel 𝕜;
BorelSpace 𝕜
Tactic: borelize 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : SecondCountableTopologyEither E F
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
⊢ StronglyMeasurable.{u_2, u_3} (β := F) fun (x : E) ↦ lineDeriv 𝕜 f x v
have hg : Continuous (Function.uncurry g)
Tactic: have hg : Continuous g.uncurry := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
hf : Continuous f
⊢ MeasurableSet.{u_2} (α := E × E) {p : E × E | LineDifferentiableAt 𝕜 f p.1 p.2}
have this : let this := borel 𝕜;
BorelSpace 𝕜
Tactic: borelize 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun (p : E × E) (t : 𝕜) ↦ f (p.1 + t • p.2)
⊢ MeasurableSet.{u_2} (α := E × E) {p : E × E | LineDifferentiableAt 𝕜 f p.1 p.2}
have this : Continuous (Function.uncurry g)
Tactic: have : Continuous g.uncurry :=
    hf.comp <| (continuous_fst.comp continuous_fst).add
    <| continuous_snd.smul (continuous_snd.comp continuous_fst)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
hf : Continuous f
this_1 : MeasurableSpace 𝕜 := borel 𝕜
this_2 : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun (p : E × E) (t : 𝕜) ↦ f (p.1 + t • p.2)
this : Continuous (Function.uncurry g)
⊢ MeasurableSet.{u_2} (α := E × E) {p : E × E | LineDifferentiableAt 𝕜 f p.1 p.2}
have M_meas : MeasurableSet (α := Prod.{u_2, u_1} (E × E) 𝕜) {q : Prod.{u_2, u_1} (E × E) 𝕜 | DifferentiableAt 𝕜 (g q.1) q.2}
Tactic: have M_meas : MeasurableSet {q : (E × E) × 𝕜 | DifferentiableAt 𝕜 (g q.1) q.2} :=
    measurableSet_of_differentiableAt_with_param 𝕜 this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
inst_10 : MeasurableSpace F
inst_11 : BorelSpace F
hf : Continuous f
⊢ Measurable.{u_2, u_3} (β := F) fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2
have this : let this := borel 𝕜;
BorelSpace 𝕜
Tactic: borelize 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
inst_10 : MeasurableSpace F
inst_11 : BorelSpace F
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun (p : E × E) (t : 𝕜) ↦ f (p.1 + t • p.2)
⊢ Measurable.{u_2, u_3} (β := F) fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2
have this : Continuous (Function.uncurry g)
Tactic: have : Continuous g.uncurry :=
    hf.comp <| (continuous_fst.comp continuous_fst).add
    <| continuous_snd.smul (continuous_snd.comp continuous_fst)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
hf : Continuous f
⊢ StronglyMeasurable.{u_2, u_3} (β := F) fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2
have this : let this := borel 𝕜;
BorelSpace 𝕜
Tactic: borelize 𝕜
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.Measurable (hypothesis)
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun (p : E × E) (t : 𝕜) ↦ f (p.1 + t • p.2)
⊢ StronglyMeasurable.{u_2, u_3} (β := F) fun (p : E × E) ↦ lineDeriv 𝕜 f p.1 p.2
have this : Continuous (Function.uncurry g)
Tactic: have : Continuous g.uncurry :=
    hf.comp <| (continuous_fst.comp continuous_fst).add
    <| continuous_snd.smul (continuous_snd.comp continuous_fst)
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : AddCommGroup E
inst_2 : Module 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : QuadraticMap 𝕜 E F
⊢ Eq (α := (x v : E) → F) (lineDeriv 𝕜 (⇑f : (a : E) → F)) (polar (⇑f : (a : E) → F))
have h : ∀ (a b : E), Eq.{u_3 + 1} (α := F) (lineDeriv 𝕜 (⇑f : (a : E) → F) a b) (polar (⇑f : (a : E) → F) a b)
Tactic: ext a b
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x y : E
h : ∃ᶠ (t : ℝ) in 𝓝[>] 0, x + t • y ∈ s
⊢ y ∈ posTangentConeAt s x
have h₁ : NeBot (α := ℝ≥0) (𝓝[>] 0 ⊓ 𝓟 {x_1 : ℝ≥0 | x + (↑x_1 : ℝ) • y ∈ s})
Tactic: rw [← NNReal.coe_zero, ← NNReal.map_coe_nhdsGT, frequently_map, frequently_iff_neBot] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x y : E
h : NeBot (α := ℝ≥0) (𝓝[>] 0 ⊓ 𝓟 {x_1 : ℝ≥0 | x + (↑x_1 : ℝ) • y ∈ s})
⊢ y ∈ posTangentConeAt s x
have hc₀ : Tendsto (α := ℝ≥0) id (𝓝[>] 0 ⊓ 𝓟 {t : ℝ≥0 | x + (↑t : ℝ) • y ∈ s}) (𝓝[≠] 0)
Tactic: apply mem_tangentConeAt_of_add_smul_mem (l := 𝓝[>] (0 : ℝ≥0) ⊓ 𝓟 {t | x + (t : ℝ) • y ∈ s})
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x y : E
h : NeBot (α := ℝ≥0) (𝓝[>] 0 ⊓ 𝓟 {x_1 : ℝ≥0 | x + (↑x_1 : ℝ) • y ∈ s})
hc₀ : Tendsto (α := ℝ≥0) id (𝓝[>] 0 ⊓ 𝓟 {t : ℝ≥0 | x + (↑t : ℝ) • y ∈ s}) (𝓝[≠] 0)
⊢ y ∈ posTangentConeAt s x
have hmem : ∀ᶠ (n : ℝ≥0) in 𝓝[>] 0 ⊓ 𝓟 {t : ℝ≥0 | x + (↑t : ℝ) • y ∈ s}, x + id n • y ∈ s
Tactic: apply mem_tangentConeAt_of_add_smul_mem (l := 𝓝[>] (0 : ℝ≥0) ⊓ 𝓟 {t | x + (t : ℝ) • y ∈ s})
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Set E
x y : E
h : NeBot (α := ℝ≥0) (𝓝[>] 0 ⊓ 𝓟 {x_1 : ℝ≥0 | x + (↑x_1 : ℝ) • y ∈ s})
hc₀ : Tendsto (α := ℝ≥0) id (𝓝[>] 0 ⊓ 𝓟 {t : ℝ≥0 | x + (↑t : ℝ) • y ∈ s}) (𝓝[≠] 0)
hmem : ∀ᶠ (n : ℝ≥0) in 𝓝[>] 0 ⊓ 𝓟 {t : ℝ≥0 | x + (↑t : ℝ) • y ∈ s}, x + id n • y ∈ s
⊢ y ∈ posTangentConeAt s x
have apply : ℝ≥0 → ℝ≥0
Tactic: apply mem_tangentConeAt_of_add_smul_mem (l := 𝓝[>] (0 : ℝ≥0) ⊓ 𝓟 {t | x + (t : ℝ) • y ∈ s})
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
⊢ LE.le (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) (0 : ℝ)
have rcases : ∀ (ι : Type u) (l : Filter ι) (hl : l.NeBot) (c : ι → ℝ≥0) (d : ι → E) (hd₀ : Tendsto d l (𝓝 0))
  (hd : ∀ᶠ (n : ι) in l, a + d n ∈ s) (hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)),
  LE.le (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) (0 : ℝ)
Tactic: rcases exists_fun_of_mem_tangentConeAt hy with ⟨ι, l, hl, c, d, hd₀, hd, hcd⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
⊢ LE.le (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) (0 : ℝ)
have suffices : ∀ᶠ (n : ι) in l, c n • (f (a + d n) - f a) ≤ 0
Tactic: suffices ∀ᶠ n in l, c n • (f (a + d n) - f a) ≤ 0 from
    le_of_tendsto (hf.lim hd₀ hd hcd) this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
⊢ ∀ᶠ (n : ι) in l, c n • (f (a + d n) - f a) ≤ 0
have hd₁ : Tendsto (fun (n : ι) ↦ a + d n) l (𝓝[s] (a + 0))
Tactic: replace hd : Tendsto (fun n => a + d n) l (𝓝[s] (a + 0)) :=
    tendsto_nhdsWithin_iff.2 ⟨tendsto_const_nhds.add hd₀, hd⟩
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (hypothesis)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
hd : Tendsto (fun (n : ι) ↦ a + d n) l (𝓝[s] (a + 0))
⊢ ∀ᶠ (n : ι) in l, c n • (f (a + d n) - f a) ≤ 0
have hd₁ : Tendsto (fun (n : ι) ↦ a + d n) l (𝓝[s] a)
Tactic: rw [add_zero] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
s : Set E
a y : E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
hy : y ∈ posTangentConeAt s a
ι : Type u
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → E
hd₀ : Tendsto d l (𝓝 0)
hcd : Tendsto (fun (n : ι) ↦ c n • d n) l (𝓝 y)
hd : Tendsto (fun (n : ι) ↦ a + d n) l (𝓝[s] a)
⊢ ∀ᶠ (n : ι) in l, c n • (f (a + d n) - f a) ≤ 0
have refine : ∀ (n : ι) (hn : f (a + d n) ≤ f a), c n • (f (a + d n) - f a) ≤ 0
Tactic: refine hd.eventually h |>.mono fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ LE.le (α := ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ) (0 : ℝ)
have rw : LE.le (α := ℝ) ((0 : (a : E) → ℝ) y : ℝ) ((0 : (a : E) → ℝ) y : ℝ)
Tactic: rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ Eq (α := ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ) (0 : ℝ)
have rw : Eq (α := ℝ) ((0 : (a : E) → ℝ) y : ℝ) (0 : ℝ)
Tactic: rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ LE.le (α := ℝ) (0 : ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ)
have rw : LE.le (α := ℝ) 0 0
Tactic: rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMinOn f s a
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ Eq (α := ℝ) ((fderivWithin ℝ f s a : (a : E) → ℝ) y : ℝ) (0 : ℝ)
have rw : Eq (α := ℝ) ((0 : (a : E) → ℝ) y : ℝ) (0 : ℝ)
Tactic: rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
⊢ f' = 0
have h₁ : ∀ (y : E), Eq (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) ((0 : (a : E) → ℝ) y : ℝ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ Eq (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) ((0 : (a : E) → ℝ) y : ℝ)
have h₁ : y ∈ posTangentConeAt univ a
Tactic: apply (h.on univ).hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
h₁ : y ∈ posTangentConeAt univ a
⊢ Eq (α := ℝ) ((f' : (a : E) → ℝ) y : ℝ) ((0 : (a : E) → ℝ) y : ℝ)
have h₂ : -y ∈ posTangentConeAt univ a
Tactic: apply (h.on univ).hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ y ∈ posTangentConeAt univ a
have h₁ : Membership.mem (γ := Set E) univ y
Tactic: rw [posTangentConeAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
E : Type u
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
f' : StrongDual ℝ E
a : E
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ -y ∈ posTangentConeAt univ a
have h₁ : Membership.mem (γ := Set E) univ (-y)
Tactic: rw [posTangentConeAt_univ]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
s : Set ℝ
a : ℝ
⊢ 1 ∈ posTangentConeAt s a ↔ a ∈ closure (Ioi a ∩ s)
have mp : 1 ∈ posTangentConeAt s a → a ∈ closure (Ioi a ∩ s)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
s : Set ℝ
a : ℝ
mp : 1 ∈ posTangentConeAt s a → a ∈ closure (Ioi a ∩ s)
⊢ 1 ∈ posTangentConeAt s a ↔ a ∈ closure (Ioi a ∩ s)
have mpr : a ∈ closure (Ioi a ∩ s) → 1 ∈ posTangentConeAt s a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
⊢ a ∈ closure (Ioi a ∩ s)
have mp : ∀ (ι : Type) (l : Filter ι) (hl : l.NeBot) (c : ι → ℝ≥0) (d : ι → ℝ) (hd₀ : Tendsto d l (𝓝 0))
  (hd : ∀ᶠ (n : ι) in l, a + d n ∈ s) (hcd : Tendsto (β := ℝ) (fun (n : ι) ↦ c n • d n) l (𝓝 1)),
  a ∈ closure (Ioi a ∩ s)
Tactic: rcases exists_fun_of_mem_tangentConeAt h with ⟨ι, l, hl, c, d, hd₀, hd, hcd⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (hypothesis)
Goal:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (β := ℝ) (fun (n : ι) ↦ c n • d n) l (𝓝 1)
⊢ a ∈ closure (Ioi a ∩ s)
have this : Tendsto (fun (x : ι) ↦ a + d x) l (𝓝 a)
Tactic: have : Tendsto (a + d ·) l (𝓝 a) := by
      simpa only [add_zero] using tendsto_const_nhds.add hd₀
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (β := ℝ) (fun (n : ι) ↦ c n • d n) l (𝓝 1)
this : Tendsto (fun (x : ι) ↦ a + d x) l (𝓝 a)
⊢ a ∈ closure (Ioi a ∩ s)
have mp : ∀ᶠ (x : ι) in l, a + d x ∈ Ioi a ∩ s
Tactic: apply mem_closure_of_tendsto this
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (β := ℝ) (fun (n : ι) ↦ c n • d n) l (𝓝 1)
this : Tendsto (fun (x : ι) ↦ a + d x) l (𝓝 a)
⊢ ∀ᶠ (x : ι) in l, a + d x ∈ Ioi a ∩ s
have h₁ : ∀ (n : ι) (hcdn : 0 < c n • d n) (hdn : a + d n ∈ s), a + d n ∈ Ioi a ∩ s
Tactic: filter_upwards [hcd.eventually_const_lt one_pos, hd] with n hcdn hdn
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
s : Set ℝ
a : ℝ
h : 1 ∈ posTangentConeAt s a
ι : Type
l : Filter ι
hl : l.NeBot
c : ι → ℝ≥0
d : ι → ℝ
hd₀ : Tendsto d l (𝓝 0)
hd : ∀ᶠ (n : ι) in l, a + d n ∈ s
hcd : Tendsto (β := ℝ) (fun (n : ι) ↦ c n • d n) l (𝓝 1)
this : Tendsto (fun (x : ι) ↦ a + d x) l (𝓝 a)
n : ι
hcdn : 0 < c n • d n
hdn : a + d n ∈ s
⊢ a + d n ∈ Ioi a ∩ s
have h₁ : a + d n ∈ Ioi a
Tactic: refine ⟨?_, hdn⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LocalExtr.Basic (goal)
Goal:
s : Set ℝ
a : ℝ
h : a ∈ closure (Ioi a ∩ s)
⊢ 1 ∈ posTangentConeAt s a
have mpr : ∃ᶠ (t : ℝ) in 𝓝[>] 0, a + HSMul.hSMul (β := ℝ) t 1 ∈ s
Tactic: apply mem_posTangentConeAt_of_frequently_mem