-- Mathlib/Analysis/Convex/Visible.lean
/-- If `s` is a closed set, then any point `x` sees some point of `s` in any direction where there
is something to see. -/
lemma IsClosed.exists_wbtw_isVisible (hs : IsClosed s) (hy : y ∈ s) (x : V) :
    ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Proof state:
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ₀ : 0 ≤ δ
hδ : (lineMap x y) δ ∈ s
ε : ℝ
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
hε : (lineMap x ((lineMap x y) δ)) ε ∈ s
h : (lineMap x ((lineMap x y) δ)) ε ≠ (lineMap x y) δ
⊢ δ ≠ 0

Tactic:
rintro hδ₀

Result:
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ₀✝ : 0 ≤ δ
hδ : (lineMap x y) δ ∈ s
ε : ℝ
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
hε : (lineMap x ((lineMap x y) δ)) ε ∈ s
h : (lineMap x ((lineMap x y) δ)) ε ≠ (lineMap x y) δ
hδ₀ : δ = 0
⊢ False

Proof state:
case intro.intro.intro.intro.intro.intro
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ : (lineMap x y) δ ∈ s
ε : ℝ
hε₀ : 0 ≤ ε
hε : (lineMap x ((lineMap x y) δ)) ε ∈ s
h : (lineMap x ((lineMap x y) δ)) ε ≠ (lineMap x y) δ
hδ₀ : 0 < δ
hε₁ : ε < 1
⊢ False

Tactic:
rw [lineMap_lineMap_right] at hε

Result:
case intro.intro.intro.intro.intro.intro
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ : (lineMap x y) δ ∈ s
ε : ℝ
hε₀ : 0 ≤ ε
hε : (lineMap x y) (ε * δ) ∈ s
h : (lineMap x ((lineMap x y) δ)) ε ≠ (lineMap x y) δ
hδ₀ : 0 < δ
hε₁ : ε < 1
⊢ False

Proof state:
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Tactic:
obtain ⟨hδ₀, hδ⟩ : 0 ≤ δ ∧ lineMap x y δ ∈ s :=
  (isClosed_Ici.inter <| hs.preimage lineMap_continuous).csInf_mem ⟨1, ht₁⟩ ht

Result:
case intro
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ₀ : 0 ≤ δ
hδ : (lineMap x y) δ ∈ s
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Proof state:
case intro
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ₀ : 0 ≤ δ
hδ : (lineMap x y) δ ∈ s
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Tactic:
refine ⟨lineMap x y δ, hδ, wbtw_lineMap_iff.2 <| .inr ⟨hδ₀, hδ₁⟩, ?_⟩

Result:
case intro
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ₀ : 0 ≤ δ
hδ : (lineMap x y) δ ∈ s
⊢ IsVisible ℝ s x ((lineMap x y) δ)

Proof state:
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
⊢ 1 ∈ t

Tactic:
simpa [t]

Result:
no goals

Proof state:
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Tactic:
have ht : BddBelow t := bddBelow_Ici.inter_of_left

Result:
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Proof state:
case intro.intro.intro.intro.intro.intro
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ₀ : 0 ≤ δ
hδ : (lineMap x y) δ ∈ s
ε : ℝ
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
hε : (lineMap x ((lineMap x y) δ)) ε ∈ s
h : (lineMap x ((lineMap x y) δ)) ε ≠ (lineMap x y) δ
⊢ False

Tactic:
replace hδ₀ : 0 < δ := hδ₀.lt_of_ne' <| by rintro hδ₀; simp [hδ₀] at h

Result:
case intro.intro.intro.intro.intro.intro
V : Type u_2
inst✝⁴ : AddCommGroup V
inst✝³ : Module ℝ V
s : Set V
y : V
inst✝² : TopologicalSpace V
inst✝¹ : IsTopologicalAddGroup V
inst✝ : ContinuousSMul ℝ V
hs : IsClosed s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ ⇑(lineMap x y) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ : (lineMap x y) δ ∈ s
ε : ℝ
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
hε : (lineMap x ((lineMap x y) δ)) ε ∈ s
h : (lineMap x ((lineMap x y) δ)) ε ≠ (lineMap x y) δ
hδ₀ : 0 < δ
⊢ False