-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem uniqueDiffWithinAt_convex {s : Set G} (conv : Convex ℝ s) (hs : (interior s).Nonempty)
    {x : G} (hx : x ∈ closure s) : UniqueDiffWithinAt ℝ s x

Proof state:
case intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
⊢ (fun x_1 => x_1 - x) '' interior s ⊆ tangentConeAt ℝ s x

Tactic:
rintro _ ⟨z, zs, rfl⟩

Result:
case intro.intro.intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
z : G
zs : z ∈ interior s
⊢ (fun x_1 => x_1 - x) z ∈ tangentConeAt ℝ s x

Proof state:
case intro.intro.intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
z : G
zs : z ∈ interior s
⊢ openSegment ℝ x z ⊆ interior s

Tactic:
exact conv.openSegment_closure_interior_subset_interior hx zs

Result:
no goals

Proof state:
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ UniqueDiffWithinAt ℝ s x

Tactic:
refine ⟨Dense.of_closure ?_, hx⟩

Result:
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ Dense (closure ↑(Submodule.span ℝ (tangentConeAt ℝ s x)))

Proof state:
case intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
⊢ UniqueDiffWithinAt ℝ s x

Tactic:
suffices y - x ∈ interior (tangentConeAt ℝ s x) by
  refine ⟨Dense.of_closure ?_, hx⟩
  simp [(Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
      ⟨y - x, interior_mono Submodule.subset_span this⟩]

Result:
case intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
⊢ y - x ∈ interior (tangentConeAt ℝ s x)

Proof state:
case intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
⊢ tangentConeAt ℝ s x ∈ 𝓝 (y - x)

Tactic:
replace hy : interior s ∈ 𝓝 y := IsOpen.mem_nhds isOpen_interior hy

Result:
case intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
⊢ tangentConeAt ℝ s x ∈ 𝓝 (y - x)

Proof state:
case intro.intro.intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
z : G
zs : z ∈ interior s
⊢ (fun x_1 => x_1 - x) z ∈ tangentConeAt ℝ s x

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

Result:
case intro.intro.intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
z : G
zs : z ∈ interior s
⊢ openSegment ℝ x z ⊆ interior s

Proof state:
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
hs : (interior s).Nonempty
x : G
hx : x ∈ closure s
⊢ UniqueDiffWithinAt ℝ s x

Tactic:
rcases hs with ⟨y, hy⟩

Result:
case intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
⊢ UniqueDiffWithinAt ℝ s x

Proof state:
case intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
⊢ tangentConeAt ℝ s x ∈ 𝓝 (y - x)

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

Result:
case intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : interior s ∈ 𝓝 y
⊢ (fun x_1 => x_1 - x) '' interior s ⊆ tangentConeAt ℝ s x

Proof state:
case intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
⊢ y - x ∈ interior (tangentConeAt ℝ s x)

Tactic:
rw [mem_interior_iff_mem_nhds]

Result:
case intro
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
⊢ tangentConeAt ℝ s x ∈ 𝓝 (y - x)

Proof state:
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
s : Set G
conv : Convex ℝ s
x : G
hx : x ∈ closure s
y : G
hy : y ∈ interior s
this : y - x ∈ interior (tangentConeAt ℝ s x)
⊢ Dense (closure ↑(Submodule.span ℝ (tangentConeAt ℝ s x)))

Tactic:
simp [(Submodule.span ℝ (tangentConeAt ℝ s x)).eq_top_of_nonempty_interior'
    ⟨y - x, interior_mono Submodule.subset_span this⟩]

Result:
no goals