-- Mathlib/Analysis/Convex/Visible.lean
/-- All points of the convex hull of a set `s` visible from a point `x ∉ convexHull ℝ s` lie in the
convex hull of such points that actually lie in `s`.

Note that the converse does not hold. -/
lemma IsVisible.mem_convexHull_isVisible (hx : x ∉ convexHull ℝ s) (hy : y ∈ convexHull ℝ s)
    (hxy : IsVisible ℝ (convexHull ℝ s) x y) :
    y ∈ convexHull ℝ {z ∈ s | IsVisible ℝ (convexHull ℝ s) x z}

Proof state:
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x y : V
hx : x ∉ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x y
⊢ y ∈ (convexHull ℝ) {z | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x z}

Tactic:
classical
obtain ⟨ι, _, w, a, hw₀, hw₁, ha, rfl⟩ := mem_convexHull_iff_exists_fintype.1 hy
rw [← Fintype.sum_subset (s := {i | w i ≠ 0})
  fun i hi ↦ mem_filter.2 ⟨mem_univ _, left_ne_zero_of_smul hi⟩]
exact (convex_convexHull ..).sum_mem (fun i _ ↦ hw₀ _) (by rwa [sum_filter_ne_zero])
  fun i hi ↦ subset_convexHull _ _ ⟨ha _, IsVisible.of_convexHull_of_pos (fun _ _ ↦ hw₀ _) hw₁
    (by simpa) hx hxy (mem_univ _) <| (hw₀ _).lt_of_ne' (mem_filter.1 hi).2⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x : V
hx : x ∉ (convexHull ℝ) s
ι : Type
w✝ : Fintype ι
w : ι → ℝ
a : ι → V
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
ha : ∀ (i : ι), a i ∈ s
hy : ∑ i : ι, w i • a i ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x (∑ i : ι, w i • a i)
⊢ ∑ i : ι, w i • a i ∈ (convexHull ℝ) {z | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x z}

Tactic:
rw [← Fintype.sum_subset (s := {i | w i ≠ 0})
  fun i hi ↦ mem_filter.2 ⟨mem_univ _, left_ne_zero_of_smul hi⟩]

Result:
case intro.intro.intro.intro.intro.intro.intro
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x : V
hx : x ∉ (convexHull ℝ) s
ι : Type
w✝ : Fintype ι
w : ι → ℝ
a : ι → V
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
ha : ∀ (i : ι), a i ∈ s
hy : ∑ i : ι, w i • a i ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x (∑ i : ι, w i • a i)
⊢ ∑ i ∈ filter (fun i => w i ≠ 0) Finset.univ, w i • a i ∈
    (convexHull ℝ) {z | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x z}

Proof state:
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x : V
hx : x ∉ (convexHull ℝ) s
ι : Type
w✝ : Fintype ι
w : ι → ℝ
a : ι → V
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
ha : ∀ (i : ι), a i ∈ s
hy : ∑ i : ι, w i • a i ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x (∑ i : ι, w i • a i)
i : ι
hi : i ∈ filter (fun i => w i ≠ 0) Finset.univ
⊢ ∀ i ∈ Finset.univ, a i ∈ s

Tactic:
simpa

Result:
no goals

Proof state:
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x y : V
hx : x ∉ (convexHull ℝ) s
hy : y ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x y
⊢ y ∈ (convexHull ℝ) {z | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x z}

Tactic:
obtain ⟨ι, _, w, a, hw₀, hw₁, ha, rfl⟩ := mem_convexHull_iff_exists_fintype.1 hy

Result:
case intro.intro.intro.intro.intro.intro.intro
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x : V
hx : x ∉ (convexHull ℝ) s
ι : Type
w✝ : Fintype ι
w : ι → ℝ
a : ι → V
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
ha : ∀ (i : ι), a i ∈ s
hy : ∑ i : ι, w i • a i ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x (∑ i : ι, w i • a i)
⊢ ∑ i : ι, w i • a i ∈ (convexHull ℝ) {z | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x z}

Proof state:
case intro.intro.intro.intro.intro.intro.intro
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x : V
hx : x ∉ (convexHull ℝ) s
ι : Type
w✝ : Fintype ι
w : ι → ℝ
a : ι → V
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
ha : ∀ (i : ι), a i ∈ s
hy : ∑ i : ι, w i • a i ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x (∑ i : ι, w i • a i)
⊢ ∑ i ∈ filter (fun i => w i ≠ 0) Finset.univ, w i • a i ∈
    (convexHull ℝ) {z | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ) s) x z}

Tactic:
exact (convex_convexHull ..).sum_mem (fun i _ ↦ hw₀ _) (by rwa [sum_filter_ne_zero])
  fun i hi ↦ subset_convexHull _ _ ⟨ha _, IsVisible.of_convexHull_of_pos (fun _ _ ↦ hw₀ _) hw₁
    (by simpa) hx hxy (mem_univ _) <| (hw₀ _).lt_of_ne' (mem_filter.1 hi).2⟩

Result:
no goals

Proof state:
V : Type u_2
inst✝¹ : AddCommGroup V
inst✝ : Module ℝ V
s : Set V
x : V
hx : x ∉ (convexHull ℝ) s
ι : Type
w✝ : Fintype ι
w : ι → ℝ
a : ι → V
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : ∑ i : ι, w i = 1
ha : ∀ (i : ι), a i ∈ s
hy : ∑ i : ι, w i • a i ∈ (convexHull ℝ) s
hxy : IsVisible ℝ ((convexHull ℝ) s) x (∑ i : ι, w i • a i)
⊢ ∑ i ∈ filter (fun i => w i ≠ 0) Finset.univ, w i = 1

Tactic:
rwa [sum_filter_ne_zero]

Result:
no goals