awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ ∀ (n : ℕ), ‖d n‖ ≤ u n

Tactic:
simpa [dist_eq_norm] using hvu

Premises used: dist_eq_norm
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ Tendsto d atTop (𝓝 0)

Tactic:
exact squeeze_zero_norm (by simpa [dist_eq_norm] using hvu) u_lim

Premises used: squeeze_zero_norm
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, x + (d ∘ φ) n ∈ s

Tactic:
.of_forall fun n ↦ (M _).1

Premises used: Filter.Eventually.of_forall, And.left
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ ∀ᶠ (n : ℕ) in atTop, x + (d ∘ φ) n ∈ s

Tactic:
exact .of_forall fun n ↦ (M _).1
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ Tendsto (fun (n : ℕ) ↦ (c ∘ φ) n • (d ∘ φ) n) atTop (𝓝 l)

Tactic:
hφ
-- Module: Mathlib.Analysis.Calculus.TangentCone.ProperSpace
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : ProperSpace E
s : Set E
x : E
hx : AccPt x (𝓟 s)
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
v : (n : ℕ) → E
hvx : ∀ (n : ℕ), v n ≠ x
hvu : ∀ (n : ℕ), v n ∈ closedBall x (u n)
hvs : ∀ (n : ℕ), v n ∈ s
d : (n : ℕ) → E := fun (n : ℕ) ↦ v n - x
M : ∀ (n : ℕ), x + d n ∈ s \ {x}
r : 𝕜
hr : 1 < ‖r‖
c : (n : ℕ) → 𝕜
c_ne : ∀ (n : ℕ), c n ≠ 0
c_le : ∀ (n : ℕ), ‖c n • d n‖ < 1
le_c : ∀ (n : ℕ), 1 / ‖r‖ ≤ ‖c n • d n‖
hc : ∀ (n : ℕ), ‖c n‖⁻¹ ≤ 1⁻¹ * ‖r‖ * ‖d n‖
l : E
l_mem : Membership.mem (γ := Set E) (closedBall 0 1 \ ball 0 (1 / ‖r‖)) l
φ : ℕ → ℕ
φ_strict : StrictMono φ
hφ : Tendsto ((fun (n : ℕ) ↦ c n • d n) ∘ φ) atTop (𝓝 l)
⊢ Tendsto (fun (n : ℕ) ↦ (c ∘ φ) n • (d ∘ φ) n) atTop (𝓝 l)

Tactic:
exact hφ
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
⊢ y - x ∈ tangentConeAt ℝ≥0 s x

Tactic:
mem_tangentConeAt_of_add_smul_mem (tendsto_id'.mpr <| nhdsGT_le_nhdsNE 0) ?_

Premises used: Iff.mpr, Set.Mem, Filter.tendsto_id', nhdsGT_le_nhdsNE, OfNat.ofNat, mem_tangentConeAt_of_add_smul_mem
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
refine : ∀ᶠ (n : ℝ≥0) in 𝓝[>] 0, x + id n • (y - x) ∈ s
⊢ y - x ∈ tangentConeAt ℝ≥0 s x

Tactic:
refine mem_tangentConeAt_of_add_smul_mem (tendsto_id'.mpr <| nhdsGT_le_nhdsNE 0) ?_

Premises used: Iff.mpr, Filter.tendsto_id', nhdsGT_le_nhdsNE, OfNat.ofNat, mem_tangentConeAt_of_add_smul_mem
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
h₁ : ∀ (a : ℝ≥0) (ha : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) a), x + id a • (y - x) ∈ s
⊢ ∀ᶠ (n : ℝ≥0) in 𝓝[>] 0, x + id n • (y - x) ∈ s

Tactic:
filter_upwards [Ioo_mem_nhdsGT one_pos] with a ha

Premises used: one_pos, Ioo_mem_nhdsGT
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) a
h₁ : x + id a • (y - x) ∈ openSegment ℝ x y
⊢ x + id a • (y - x) ∈ s

Tactic:
apply h
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) a
h₁ :
  Membership.mem (γ := Set E) (image (α := ℝ) (⇑(AffineMap.lineMap x y) : (a : ℝ) → E) (Ioo 0 1)) (x + id a • (y - x))
⊢ x + id a • (y - x) ∈ openSegment ℝ x y

Tactic:
rw [openSegment_eq_image_lineMap]

Premises used: openSegment_eq_image_lineMap
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) a
right : (AffineMap.lineMap x y : (a : ℝ) → E) (↑a : ℝ) = x + id a • (y - x)
⊢ Membership.mem (γ := Set E) (image (α := ℝ) (⇑(AffineMap.lineMap x y) : (a : ℝ) → E) (Ioo 0 1)) (x + id a • (y - x))

Tactic:
use a, mod_cast ha
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
a : ℝ≥0
ha : Membership.mem (γ := Set ℝ≥0) (Ioo 0 1) a
⊢ (AffineMap.lineMap x y : (a : ℝ) → E) (↑a : ℝ) = x + id a • (y - x)

Tactic:
simp [AffineMap.lineMap_apply_module', add_comm, NNReal.smul_def]

Premises used: AffineMap.lineMap_apply_module', add_comm, NNReal.smul_def
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : openSegment ℝ x y ⊆ s
⊢ y - x ∈ tangentConeAt ℝ s x

Tactic:
tangentConeAt_mono_field (sub_mem_posTangentConeAt_of_openSegment_subset h)

Premises used: Set.Mem, tangentConeAt_mono_field, sub_mem_posTangentConeAt_of_openSegment_subset
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x y : E
h : segment ℝ x y ⊆ s
⊢ y - x ∈ tangentConeAt ℝ s x

Tactic:
mem_tangentConeAt_of_openSegment_subset ((openSegment_subset_segment ℝ x y).trans h)

Premises used: Real, HasSubset.Subset.trans, openSegment_subset_segment, mem_tangentConeAt_of_openSegment_subset
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hs : (interior s).Nonempty
hx : x ∈ closure[inst_2] s
rcases : ∀ (y : E) (hy : y ∈ interior s), Eq (α := Submodule ℝ E) (Submodule.span ℝ (tangentConeAt ℝ s x)) ⊤
⊢ Eq (α := Submodule ℝ E) (Submodule.span ℝ (tangentConeAt ℝ s x)) ⊤

Tactic:
rcases hs with ⟨y, hy⟩
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
apply : (interior (↑(Submodule.span ℝ (tangentConeAt ℝ s x)) : Set E)).Nonempty
⊢ Eq (α := Submodule ℝ E) (Submodule.span ℝ (tangentConeAt ℝ s x)) ⊤

Tactic:
apply (Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'

Premises used: Real, Submodule.eq_top_of_nonempty_interior', Submodule.span, tangentConeAt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ (interior (↑(Submodule.span ℝ (tangentConeAt ℝ s x)) : Set E)).Nonempty

Tactic:
⟨y - x, interior_mono Submodule.subset_span this⟩

Premises used: interior_mono, HSub.hSub, Set.Nonempty, Exists.intro, Submodule.subset_span
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ (interior (↑(Submodule.span ℝ (tangentConeAt ℝ s x)) : Set E)).Nonempty

Tactic:
exact ⟨y - x, interior_mono Submodule.subset_span this⟩
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : y ∈ interior s
suffices : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ Eq (α := Submodule ℝ E) (Submodule.span ℝ (tangentConeAt ℝ s x)) ⊤

Tactic:
suffices y - x ∈ interior (tangentConeAt ℝ s x) by
    apply (Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
    exact ⟨y - x, interior_mono Submodule.subset_span this⟩
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : y ∈ interior s
rw : tangentConeAt ℝ s x ∈ 𝓝 (y - x)
⊢ y - x ∈ interior (tangentConeAt ℝ s x)

Tactic:
rw [mem_interior_iff_mem_nhds]

Premises used: mem_interior_iff_mem_nhds
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : y ∈ interior s
⊢ interior s ∈ 𝓝 y

Tactic:
replace hy : interior s ∈ 𝓝 y := IsOpen.mem_nhds isOpen_interior hy
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : interior s ∈ 𝓝 y
apply : (fun (x_1 : E) ↦ x_1 - x) '' interior s ⊆ tangentConeAt ℝ s x
⊢ tangentConeAt ℝ s x ∈ 𝓝 (y - x)

Tactic:
apply mem_of_superset ((isOpenMap_sub_right x).image_mem_nhds hy)

Premises used: IsOpenMap.image_mem_nhds, isOpenMap_sub_right, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : interior s ∈ 𝓝 y
z : E
zs : z ∈ interior s
⊢ (fun (x_1 : E) ↦ x_1 - x) z ∈ tangentConeAt ℝ s x

Tactic:
mem_tangentConeAt_of_openSegment_subset (Subset.trans ?_ interior_subset)

Premises used: interior_subset, Set.Mem, Set.Subset.trans, mem_tangentConeAt_of_openSegment_subset
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : interior s ∈ 𝓝 y
z : E
zs : z ∈ interior s
refine : openSegment ℝ x z ⊆ interior s
⊢ (fun (x_1 : E) ↦ x_1 - x) z ∈ tangentConeAt ℝ s x

Tactic:
refine mem_tangentConeAt_of_openSegment_subset (Subset.trans ?_ interior_subset)

Premises used: interior_subset, Set.Subset.trans, mem_tangentConeAt_of_openSegment_subset
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : interior s ∈ 𝓝 y
z : E
zs : z ∈ interior s
⊢ openSegment ℝ x z ⊆ interior s

Tactic:
conv.openSegment_closure_interior_subset_interior hx zs

Premises used: Convex.openSegment_closure_interior_subset_interior
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
x : E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hx : x ∈ closure[inst_2] s
y : E
hy : interior s ∈ 𝓝 y
z : E
zs : z ∈ interior s
⊢ openSegment ℝ x z ⊆ interior s

Tactic:
exact conv.openSegment_closure_interior_subset_interior hx zs

Premises used: Convex.openSegment_closure_interior_subset_interior
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hs : (interior s).Nonempty
x : E
hx : x ∈ closure[inst_2] s
⊢ UniqueDiffWithinAt ℝ s x

Tactic:
simp [uniqueDiffWithinAt_iff, conv.span_tangentConeAt hs hx, hx]

Premises used: Convex.span_tangentConeAt, uniqueDiffWithinAt_iff
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousSMul ℝ E
s : Set E
inst_4 : IsTopologicalAddGroup E
conv : Convex ℝ s
hs : (interior s).Nonempty
⊢ UniqueDiffOn ℝ s

Tactic:
fun _ xs => uniqueDiffWithinAt_convex conv hs (subset_closure xs)

Premises used: UniqueDiffOn, subset_closure, uniqueDiffWithinAt_convex
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a : ℝ
⊢ (interior (Ici a)).Nonempty

Tactic:
simp only [interior_Ici, nonempty_Ioi]

Premises used: interior_Ici, Set.nonempty_Ioi
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a : ℝ
⊢ (interior (Iic a)).Nonempty

Tactic:
simp only [interior_Iic, nonempty_Iio]

Premises used: interior_Iic, Set.nonempty_Iio
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a : ℝ
⊢ UniqueDiffOn ℝ (Ioi a)

Tactic:
isOpen_Ioi.uniqueDiffOn

Premises used: isOpen_Ioi, IsOpen.uniqueDiffOn
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a : ℝ
⊢ UniqueDiffOn ℝ (Iio a)

Tactic:
isOpen_Iio.uniqueDiffOn

Premises used: isOpen_Iio, IsOpen.uniqueDiffOn
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a b : ℝ
hab : a < b
⊢ (interior (Icc a b)).Nonempty

Tactic:
simp only [interior_Icc, nonempty_Ioo, hab]

Premises used: interior_Icc, Set.nonempty_Ioo
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a b : ℝ
hab : a < b
⊢ (interior (Ico a b)).Nonempty

Tactic:
simp only [interior_Ico, nonempty_Ioo, hab]

Premises used: Set.nonempty_Ioo, interior_Ico
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a b : ℝ
hab : ¬a < b
⊢ UniqueDiffOn ℝ (Ico a b)

Tactic:
simp only [Ico_eq_empty hab, uniqueDiffOn_empty]

Premises used: Set.Ico_eq_empty, uniqueDiffOn_empty
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a b : ℝ
hab : a < b
⊢ (interior (Ioc a b)).Nonempty

Tactic:
simp only [interior_Ioc, nonempty_Ioo, hab]

Premises used: Set.nonempty_Ioo, interior_Ioc
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a b : ℝ
hab : ¬a < b
⊢ UniqueDiffOn ℝ (Ioc a b)

Tactic:
simp only [Ioc_eq_empty hab, uniqueDiffOn_empty]

Premises used: Set.Ioc_eq_empty, uniqueDiffOn_empty
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a b : ℝ
⊢ UniqueDiffOn ℝ (Ioo a b)

Tactic:
isOpen_Ioo.uniqueDiffOn

Premises used: isOpen_Ioo, IsOpen.uniqueDiffOn
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
⊢ UniqueDiffOn ℝ (E := ℝ) (Icc 0 1)

Tactic:
uniqueDiffOn_Icc zero_lt_one

Premises used: uniqueDiffOn_Icc, zero_lt_one
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a b t : ℝ
ht : t ∈ Ioo a b
⊢ UniqueDiffWithinAt ℝ (Ioo a b) t

Tactic:
IsOpen.uniqueDiffWithinAt isOpen_Ioo ht

Premises used: isOpen_Ioo, IsOpen.uniqueDiffWithinAt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a : ℝ
⊢ (interior (Ioi a)).Nonempty

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a : ℝ
⊢ a ∈ closure (Ioi a)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a : ℝ
⊢ (interior (Iio a)).Nonempty

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
a : ℝ
⊢ a ∈ closure (Iio a)

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
x : ℝ
⊢ UniqueDiffWithinAt ℝ (Ici x) x

Tactic:
(uniqueDiffWithinAt_Ioi x).mono Set.Ioi_subset_Ici_self

Premises used: Set.Ioi_subset_Ici_self, uniqueDiffWithinAt_Ioi, UniqueDiffWithinAt.mono
-- Module: Mathlib.Analysis.Calculus.TangentCone.Real
Goal:
x : ℝ
⊢ UniqueDiffWithinAt ℝ (Iic x) x

Tactic:
(uniqueDiffWithinAt_Iio x).mono Set.Iio_subset_Iic_self

Premises used: uniqueDiffWithinAt_Iio, UniqueDiffWithinAt.mono, Set.Iio_subset_Iic_self
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
R : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
inst_3 : FirstCountableTopology E
s : Set E
x y : E
mp :
  y ∈ tangentConeAt R s x →
    ∃ (c : ℕ → R) (d : ℕ → E),
      Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
mpr :
  (∃ (c : ℕ → R) (d : ℕ → E),
      Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)) →
    y ∈ tangentConeAt R s x
⊢ y ∈ tangentConeAt R s x ↔
    ∃ (c : ℕ → R) (d : ℕ → E),
      Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
R : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
inst_3 : FirstCountableTopology E
s : Set E
x y : E
h : y ∈ tangentConeAt R s x
⊢ (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot

Tactic:
simp only [tangentConeAt_def, Set.mem_setOf, ← map₂_smul, ← map_prod_eq_map₂, ClusterPt,
      ← neBot_inf_comap_iff_map'] at h

Premises used: Filter.map₂_smul, Set.mem_setOf, tangentConeAt_def, Filter.neBot_inf_comap_iff_map', Filter.map_prod_eq_map₂, ClusterPt
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
R : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
inst_3 : FirstCountableTopology E
s : Set E
x y : E
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
mp :
  ∀ (cd : ℕ → R × E)
    (hcd :
      Tendsto cd atTop
        (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
          SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))),
    ∃ (c : ℕ → R) (d : ℕ → E),
      Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)
⊢ ∃ (c : ℕ → R) (d : ℕ → E),
    Tendsto d atTop (𝓝 0) ∧ (∀ᶠ (n : ℕ) in atTop, x + d n ∈ s) ∧ Tendsto (fun (n : ℕ) ↦ c n • d n) atTop (𝓝 y)

Tactic:
rcases @exists_seq_tendsto _ _ _ h with ⟨cd, hcd⟩

Premises used: Filter.exists_seq_tendsto
-- Module: Mathlib.Analysis.Calculus.TangentCone.Seq
Goal:
R : Type u_1
E : Type u_2
inst : AddCommGroup E
inst_1 : SMul R E
inst_2 : TopologicalSpace E
inst_3 : FirstCountableTopology E
s : Set E
x y : E
h :
  (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0)).NeBot
cd : ℕ → R × E
hcd :
  Tendsto cd atTop
    (comap (fun (p : R × E) ↦ p.1 • p.2) (𝓝 y) ⊓
      SProd.sprod (α := Filter R) (β := Filter E) ⊤ (𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' s] 0))
⊢ Tendsto ((fun (p : R × E) ↦ p.1 • p.2) ∘ cd) atTop (𝓝 y) ∧
    Tendsto.{0, u_1} (β := R) (fun (n : ℕ) ↦ (cd n).1) atTop ⊤ ∧
      Tendsto.{0, u_2} (β := E) (fun (n : ℕ) ↦ (cd n).2) atTop (𝓝 0) ∧
        ∀ᶠ (n : ℕ) in atTop, Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' s) (cd n).2

Tactic:
simp only [tendsto_inf, tendsto_comap_iff, tendsto_prod_iff', tendsto_nhdsWithin_iff] at hcd

Premises used: Filter.tendsto_inf, tendsto_nhdsWithin_iff, Filter.tendsto_prod_iff', Filter.tendsto_comap_iff