-- Mathlib/Analysis/Convex/Visible.lean
/-- If a point `x` sees a convex combination of points of a set `s` through `convexHull ℝ s ∌ x`,
then it sees all terms of that combination.

Note that the converse does not hold. -/
lemma IsVisible.of_convexHull_of_pos {ι : Type*} {t : Finset ι} {a : ι → V} {w : ι → 𝕜}
    (hw₀ : ∀ i ∈ t, 0 ≤ w i) (hw₁ : ∑ i ∈ t, w i = 1) (ha : ∀ i ∈ t, a i ∈ s)
    (hx : x ∉ convexHull 𝕜 s) (hw : IsVisible 𝕜 (convexHull 𝕜 s) x (∑ i ∈ t, w i • a i)) {i : ι}
    (hi : i ∈ t) (hwi : 0 < w i) : IsVisible 𝕜 (convexHull 𝕜 s) x (a i)

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝ : 0 < w i
hwi : w i < 1
hε₁ : 1 ≤ 1
hε : (lineMap x (a i)) 1 ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) 1 ≠ x ∧ (lineMap x (a i)) 1 ≠ a i
hε₀ : 0 < 1
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this : 0 < 1 - ε
hwi : 0 < 1 - w i
⊢ 0 ≤ (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝ : 0 < w i
hwi : w i < 1
ε : 𝕜
hε₁ : ε ≤ 1
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
⊢ ε ≠ 1

Tactic:
rintro rfl

Result:
𝕜 : Type u_1
V : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝ : 0 < w i
hwi : w i < 1
hε₁ : 1 ≤ 1
hε : (lineMap x (a i)) 1 ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) 1 ≠ x ∧ (lineMap x (a i)) 1 ≠ a i
hε₀ : 0 < 1
⊢ False

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝ : 0 < w i
hwi : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
⊢ 0 < 1 - ε

Tactic:
linarith

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro.refine_2
𝕜 : Type u_1
V : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this : 0 < 1 - ε
hwi : 0 < 1 - w i
⊢ (w i)⁻¹ < (1 - ε) / ε + (w i)⁻¹

Tactic:
exact lt_add_of_pos_left _ <| by positivity

Result:
no goals

Proof state:
case inr
𝕜 : Type u_1
V : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝ : 0 < w i
hwi : w i < 1
⊢ IsVisible 𝕜 ((convexHull 𝕜) s) x (a i)

Tactic:
rintro _ hε ⟨⟨ε, ⟨hε₀, hε₁⟩, rfl⟩, h⟩

Result:
case inr.intro.intro.intro.intro
𝕜 : Type u_1
V : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝ : 0 < w i
hwi : w i < 1
ε : 𝕜
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
⊢ False

Proof state:
case refine_2
𝕜 : Type u_1
V : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this✝ : 0 < 1 - ε
hwi : 0 < 1 - w i
this : w i • a i + (1 - w i) • ∑ j ∈ t.erase i, (w j / (1 - w i)) • a j = ∑ j ∈ t, w j • a j
⊢ ((1 - (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) * (1 - ε)) • x +
        ((1 - (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) * ε) • a i +
      ((1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) • ∑ j ∈ t.erase i, (w j / (1 - w i)) • a j =
    (1 - (w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) • x +
      (((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹) * w i) • a i +
        ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹) * (1 - w i)) • ∑ j ∈ t.erase i, (w j / (1 - w i)) • a j)

Tactic:
match_scalars <;> field_simp <;> ring

Result:
no goals

Proof state:
𝕜 : Type u_1
V : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this : 0 < 1 - ε
hwi : 0 < 1 - w i
⊢ w i • a i + ∑ x ∈ t.erase i, (1 - w i) • (w x / (1 - w i)) • a x = ∑ j ∈ t, w j • a j

Tactic:
simp_rw [smul_smul, mul_div_cancel₀ _ hwi.ne']

Result:
𝕜 : Type u_1
V : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : ∑ i ∈ t, w i = 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ (convexHull 𝕜) s
hw : IsVisible 𝕜 ((convexHull 𝕜) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi✝¹ : 0 < w i
hwi✝ : w i < 1
ε : 𝕜
hε : (lineMap x (a i)) ε ∈ (convexHull 𝕜) s
h : (lineMap x (a i)) ε ≠ x ∧ (lineMap x (a i)) ε ≠ a i
hε₀ : 0 < ε
hε₁ : ε < 1
this : 0 < 1 - ε
hwi : 0 < 1 - w i
⊢ w i • a i + ∑ x ∈ t.erase i, w x • a x = ∑ j ∈ t, w j • a j