-- 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) δ
hδ₀ : δ = 0
⊢ False

Tactic:
simp [hδ₀] at h

Result:
no goals

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ε₁ : ε ≤ 1
hε : (lineMap x ((lineMap x y) δ)) ε ∈ s
h : (lineMap x ((lineMap x y) δ)) ε ≠ (lineMap x y) δ
hδ₀ : 0 < δ
⊢ False

Tactic:
replace hε₁ : ε < 1 := hε₁.lt_of_ne <| by rintro rfl; simp 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 ((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
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 < δ
⊢ ε ≠ 1

Tactic:
rintro rfl

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δ : (lineMap x y) δ ∈ s
hδ₀ : 0 < δ
hε₀ : 0 ≤ 1
hε₁ : 1 ≤ 1
hε : (lineMap x ((lineMap x y) δ)) 1 ∈ s
h : (lineMap x ((lineMap x y) δ)) 1 ≠ (lineMap x y) δ
⊢ 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
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Tactic:
have hδ₁ : δ ≤ 1 := csInf_le ht ht₁

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
⊢ ∃ 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δ : (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

Tactic:
exact (csInf_le ht ⟨mul_nonneg hε₀ hδ₀.le, hε⟩).not_lt <| mul_lt_of_lt_one_left hδ₀ hε₁

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
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ : (lineMap x y) δ ∈ s
hδ₀ : 0 < δ
hε₀ : 0 ≤ 1
hε₁ : 1 ≤ 1
hε : (lineMap x ((lineMap x y) δ)) 1 ∈ s
h : (lineMap x ((lineMap x y) δ)) 1 ≠ (lineMap x y) δ
⊢ False

Tactic:
simp at h

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
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Tactic:
let t : Set ℝ := Ici 0 ∩ lineMap x y ⁻¹' s

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
⊢ ∃ 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
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Tactic:
let δ : ℝ := sInf t

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
⊢ ∃ 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
⊢ IsVisible ℝ s x ((lineMap x y) δ)

Tactic:
rintro _ hε ⟨⟨ε, ⟨hε₀, hε₁⟩, rfl⟩, -, 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δ₀ : 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

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
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Tactic:
have ht₁ : 1 ∈ t := by simpa [t]

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
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z