-- Mathlib/Analysis/Convex/Visible.lean
/-- One cannot see any point in the interior of a set. -/
lemma IsVisible.eq_of_mem_interior (hsxy : IsVisible 𝕜 s x y) (hy : y ∈ interior s) :
    x = y

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
h : ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False
⊢ False

Tactic:
obtain ⟨_, ⟨⟩⟩ := h.exists

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
hmem✝ : ∀ᶠ (δ : 𝕜) in 𝓝[>] 0, (lineMap y x) δ ∈ s
δ : 𝕜
hmem : (lineMap y x) δ ∈ s
hsbt : δ ∈ Set.Ioo 0 1
⊢ Sbtw 𝕜 y ((lineMap y x) δ) x

Tactic:
aesop

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
⊢ s ∈ 𝓝 ((lineMap y x) 0)

Tactic:
simpa using mem_interior_iff_mem_nhds.1 hy

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
⊢ False

Tactic:
suffices h : ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False by obtain ⟨_, ⟨⟩⟩ := h.exists

Result:
𝕜 : Type u_1
V : Type u_2
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
⊢ ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
⊢ x = y

Tactic:
by_contra! hxy

Result:
𝕜 : Type u_1
V : Type u_2
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
⊢ False

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
⊢ ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False

Tactic:
have hmem : ∀ᶠ (δ : 𝕜) in 𝓝[>] 0, lineMap y x δ ∈ s :=
  lineMap_continuous.continuousWithinAt.eventually_mem
    (by simpa using mem_interior_iff_mem_nhds.1 hy)

Result:
𝕜 : Type u_1
V : Type u_2
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
hmem : ∀ᶠ (δ : 𝕜) in 𝓝[>] 0, (lineMap y x) δ ∈ s
⊢ ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝⁷ : LinearOrderedField 𝕜
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module 𝕜 V
s : Set V
x y : V
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderTopology 𝕜
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
hmem : ∀ᶠ (δ : 𝕜) in 𝓝[>] 0, (lineMap y x) δ ∈ s
⊢ ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False

Tactic:
filter_upwards [hmem, Ioo_mem_nhdsGT zero_lt_one] with δ hmem hsbt using hsxy.symm hmem (by aesop)

Result:
no goals