-- Module: Mathlib.Analysis.Convex.Visible
Goal:
𝕜 : Type u_1
V : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup V
inst_4 : Module 𝕜 V
s : Set V
x : V
ι : Type u_4
t : Finset ι
a : ι → V
w : ι → 𝕜
hw₀ : ∀ i ∈ t, 0 ≤ w i
hw₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i ∈ t, w i) 1
ha : ∀ i ∈ t, a i ∈ s
hx : x ∉ ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
hw : IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (∑ i ∈ t, w i • a i)
i : ι
hi : i ∈ t
hwi : 0 < w i
inl : ∀ (hwi : w i = 1), IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)
inr inr₁ : ∀ (hwi : w i < 1), IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)
inr₂ :
  ∀ (hwi : w i < 1) (ε : 𝕜) (hε₀ : 0 ≤ ε) (hε₁ : ε ≤ 1)
    (hε :
      Membership.mem (α := V) (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
        ((lineMap x (a i) : (a : 𝕜) → V) ε : V))
    (h : (lineMap x (a i) : (a : 𝕜) → V) ε ≠ x ∧ (lineMap x (a i) : (a : 𝕜) → V) ε ≠ a i), False
inr₃ :
  ∀ (hwi : w i < 1) (ε : 𝕜) (hε₁ : ε ≤ 1)
    (hε :
      Membership.mem (α := V) (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
        ((lineMap x (a i) : (a : 𝕜) → V) ε : V))
    (h : (lineMap x (a i) : (a : 𝕜) → V) ε ≠ x ∧ (lineMap x (a i) : (a : 𝕜) → V) ε ≠ a i) (hε₀ : 0 < ε), False
inr₄ :
  ∀ (hwi : w i < 1) (ε : 𝕜)
    (hε :
      Membership.mem (α := V) (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
        ((lineMap x (a i) : (a : 𝕜) → V) ε : V))
    (h : (lineMap x (a i) : (a : 𝕜) → V) ε ≠ x ∧ (lineMap x (a i) : (a : 𝕜) → V) ε ≠ a i) (hε₀ : 0 < ε) (hε₁ : ε < 1),
    False
inr₅ :
  ∀ (hwi : w i < 1) (ε : 𝕜)
    (hε :
      Membership.mem (α := V) (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
        ((lineMap x (a i) : (a : 𝕜) → V) ε : V))
    (h : (lineMap x (a i) : (a : 𝕜) → V) ε ≠ x ∧ (lineMap x (a i) : (a : 𝕜) → V) ε ≠ a i) (hε₀ : 0 < ε) (hε₁ : ε < 1)
    (this : 0 < 1 - ε), False
inr₆ :
  ∀ (hwi : w i < 1) (ε : 𝕜)
    (hε :
      Membership.mem (α := V) (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
        ((lineMap x (a i) : (a : 𝕜) → V) ε : V))
    (h : (lineMap x (a i) : (a : 𝕜) → V) ε ≠ x ∧ (lineMap x (a i) : (a : 𝕜) → V) ε ≠ a i) (hε₀ : 0 < ε) (hε₁ : ε < 1)
    (this : 0 < 1 - ε) (hwi : 0 < 1 - w i), False
inr₇ :
  ∀ (hwi : w i < 1) (ε : 𝕜)
    (hε :
      Membership.mem (α := V) (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
        ((lineMap x (a i) : (a : 𝕜) → V) ε : V))
    (h : (lineMap x (a i) : (a : 𝕜) → V) ε ≠ x ∧ (lineMap x (a i) : (a : 𝕜) → V) ε ≠ a i) (hε₀ : 0 < ε) (hε₁ : ε < 1)
    (this : 0 < 1 - ε) (hwi : 0 < 1 - w i),
    Membership.mem (α := V) (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
      ((lineMap x (∑ j ∈ t, w j • a j) : (a : 𝕜) → V) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) : V)
inr₈ inr₉ :
  ∀ (hwi : w i < 1) (ε : 𝕜)
    (hε :
      Membership.mem (α := V) (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V)
        ((lineMap x (a i) : (a : 𝕜) → V) ε : V))
    (h : (lineMap x (a i) : (a : 𝕜) → V) ε ≠ x ∧ (lineMap x (a i) : (a : 𝕜) → V) ε ≠ a i) (hε₀ : 0 < ε) (hε₁ : ε < 1)
    (this : 0 < 1 - ε) (hwi : 0 < 1 - w i), (w i)⁻¹ < (1 - ε) / ε + (w i)⁻¹
⊢ IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)

Tactic:
classical
  obtain hwi | hwi : w i = 1 ∨ w i < 1 := eq_or_lt_of_le <| (single_le_sum hw₀ hi).trans_eq hw₁
  · convert! hw
    rw [← one_smul 𝕜 (a i), ← hwi, eq_comm]
    rw [← hwi, ← sub_eq_zero, ← sum_erase_eq_sub hi,
      sum_eq_zero_iff_of_nonneg fun j hj ↦ hw₀ _ <| erase_subset _ _ hj] at hw₁
    refine sum_eq_single _ (fun j hj hji ↦ ?_) (by simp [hi])
    rw [hw₁ _ <| mem_erase.2 ⟨hji, hj⟩, zero_smul]
  rintro _ hε ⟨⟨ε, ⟨hε₀, hε₁⟩, rfl⟩, h⟩
  replace hε₀ : 0 < ε := hε₀.lt_of_ne <| by rintro rfl; simp at h
  replace hε₁ : ε < 1 := hε₁.lt_of_ne <| by rintro rfl; simp at h
  have : 0 < 1 - ε := by linarith
  have hwi : 0 < 1 - w i := by linarith
  refine hw (z := lineMap x (∑ j ∈ t, w j • a j) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)))
    ?_ <| sbtw_lineMap_iff.2 ⟨(ne_of_mem_of_not_mem ((convex_convexHull ..).sum_mem hw₀ hw₁
    fun i hi ↦ subset_convexHull _ _ <| ha _ hi) hx).symm, by positivity,
    (div_lt_one <| by positivity).2 ?_⟩
  · have : Wbtw 𝕜
      (lineMap x (a i) ε)
      (lineMap x (∑ j ∈ t, w j • a j) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)))
      (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j) := by
      refine ⟨((1 - w i) / w i) / ((1 - ε) / ε + (1 - w i) / w i + 1), ⟨by positivity, ?_⟩, ?_⟩
      · refine (div_le_one <| by positivity).2 ?_
        calc
          (1 - w i) / w i = 0 + (1 - w i) / w i + 0 := by simp
          _ ≤ (1 - ε) / ε + (1 - w i) / w i + 1 := by gcongr <;> positivity
      have :
        w i • a i + (1 - w i) • ∑ j ∈ t.erase i, (w j / (1 - w i)) • a j = ∑ j ∈ t, w j • a j := by
        rw [smul_sum]
        simp_rw [smul_smul, mul_div_cancel₀ _ hwi.ne']
        exact add_sum_erase _ (fun i ↦ w i • a i) hi
      simp_rw [lineMap_apply_module, ← this]
      match_scalars <;> field
    refine (convex_convexHull _ _).mem_of_wbtw this hε <| (convex_convexHull _ _).sum_mem ?_ ?_ ?_
    · intro j hj
      positivity [hw₀ j <| erase_subset _ _ hj]
    · rw [← sum_div, sum_erase_eq_sub hi, hw₁, div_self hwi.ne']
    · exact fun j hj ↦ subset_convexHull _ _ <| ha _ <| erase_subset _ _ hj
  · exact lt_add_of_pos_left _ <| by positivity

Premises used: Iff.mpr, LE.le.trans_eq, sub_eq_zero, subset_convexHull, Ne.symm, eq_comm, convex_convexHull, eq_or_lt_of_le, Finset.sum_eq_single, one_smul, ne_of_mem_of_not_mem, LT.lt.ne', Finset.sum_div, zero_smul, And.intro, Finset.single_le_sum, lt_add_of_pos_left, sbtw_lineMap_iff, Convex.sum_mem, IsVisible.rfl, div_self