awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_1 : 0 < w i
hwi_2 : 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 • a i + ∑ x ∈ t.erase i, w x • a x = ∑ j ∈ t, w j • a j

Tactic:
exact add_sum_erase _ (fun i ↦ w i • a i) hi

Premises used: Finset.add_sum_erase, HSMul.hSMul
-- 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_1 : 0 < w i
hwi_2 : 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 • a i + HSMul.hSMul (β := V) (1 - w i) (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j) = ∑ j ∈ t, w j • a j

Tactic:
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
-- 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_1 : 0 < w i
hwi_2 : 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_1 : 0 < 1 - ε
hwi : 0 < 1 - w i
this : w i • a i + HSMul.hSMul (β := V) (1 - w i) (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j) = ∑ j ∈ t, w j • a j
refine_2 :
  (1 - (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) • ((1 - ε) • x + ε • a i) +
      HSMul.hSMul (β := V) ((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 + HSMul.hSMul (β := V) (1 - w i) (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j))
⊢ Eq.{u_2 + 1} (α := V)
    (((lineMap ((lineMap x (a i) : (a : 𝕜) → V) ε) (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j) : 𝕜 →ᵃ[𝕜] V) :
          (a : 𝕜) → V)
        ((1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) :
      V)
    ((lineMap x (∑ j ∈ t, w j • a j) : (a : 𝕜) → V) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) : V)

Tactic:
simp_rw [lineMap_apply_module, ← this]

Premises used: AffineMap.lineMap_apply_module
-- 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_1 : 0 < w i
hwi_2 : 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_1 : 0 < 1 - ε
hwi : 0 < 1 - w i
this : w i • a i + HSMul.hSMul (β := V) (1 - w i) (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j) = ∑ j ∈ t, w j • a j
match_scalars :
  (1 - (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) * ((1 - ε) * 1) =
    (1 - (w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) * 1
match_scalars₁ :
  (1 - (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) * (ε * 1) = (w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹) * (w i * 1)
match_scalars₂ :
  (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1) * 1 = (w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹) * ((1 - w i) * 1)
⊢ (1 - (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) • ((1 - ε) • x + ε • a i) +
      HSMul.hSMul (β := V) ((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 + HSMul.hSMul (β := V) (1 - w i) (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j))

Tactic:
match_scalars
-- 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_1 : 0 < w i
hwi_2 : 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_1 : 0 < 1 - ε
hwi : 0 < 1 - w i
this : w i • a i + HSMul.hSMul (β := V) (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 - ε) * 1) =
    (1 - (w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) * 1

Tactic:
field
-- 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_1 : 0 < w i
hwi_2 : 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_1 : 0 < 1 - ε
hwi : 0 < 1 - w i
this : w i • a i + HSMul.hSMul (β := V) (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) = (w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹) * (w i * 1)

Tactic:
field
-- 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_1 : 0 < w i
hwi_2 : 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_1 : 0 < 1 - ε
hwi : 0 < 1 - w i
this : w i • a i + HSMul.hSMul (β := V) (1 - w i) (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j) = ∑ j ∈ t, w j • a j
⊢ (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1) * 1 = (w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹) * ((1 - w i) * 1)

Tactic:
field
-- 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_1 : 0 < w i
hwi_2 : 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
⊢ Wbtw 𝕜 (P := V) ((lineMap x (a i) : (a : 𝕜) → V) ε : V)
    ((lineMap x (∑ j ∈ t, w j • a j) : (a : 𝕜) → V) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) : V)
    (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j : V)

Tactic:
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
-- 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_1 : 0 < w i
hwi_2 : 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_1 : 0 < 1 - ε
hwi : 0 < 1 - w i
this :
  Wbtw 𝕜 (P := V) ((lineMap x (a i) : (a : 𝕜) → V) ε : V)
    ((lineMap x (∑ j ∈ t, w j • a j) : (a : 𝕜) → V) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) : V)
    (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j : V)
⊢ 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)

Tactic:
(convex_convexHull _ _).mem_of_wbtw this hε <| (convex_convexHull _ _).sum_mem ?_ ?_ ?_

Premises used: Convex.mem_of_wbtw, Set.Mem, convex_convexHull, Convex.sum_mem
-- 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_1 : 0 < w i
hwi_2 : 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_1 : 0 < 1 - ε
hwi : 0 < 1 - w i
this :
  Wbtw 𝕜 (P := V) ((lineMap x (a i) : (a : 𝕜) → V) ε : V)
    ((lineMap x (∑ j ∈ t, w j • a j) : (a : 𝕜) → V) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) : V)
    (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j : V)
inr : ∀ i_1 ∈ t.erase i, 0 ≤ w i_1 / (1 - w i)
inr₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i_1 ∈ t.erase i, w i_1 / (1 - w i)) 1
inr₂ : ∀ i_1 ∈ t.erase i, Membership.mem (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V) (a i_1)
⊢ 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)

Tactic:
refine (convex_convexHull _ _).mem_of_wbtw this hε <| (convex_convexHull _ _).sum_mem ?_ ?_ ?_

Premises used: Convex.mem_of_wbtw, convex_convexHull, Convex.sum_mem
-- 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_1 : 0 < w i
hwi_2 : 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_1 : 0 < 1 - ε
hwi : 0 < 1 - w i
this :
  Wbtw 𝕜 (P := V) ((lineMap x (a i) : (a : 𝕜) → V) ε : V)
    ((lineMap x (∑ j ∈ t, w j • a j) : (a : 𝕜) → V) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) : V)
    (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j : V)
j : ι
hj : j ∈ t.erase i
inr inr₁ inr₂ inr₃ : 0 ≤ w j → 0 ≤ w j / (1 - w i)
⊢ 0 ≤ w j / (1 - w i)

Tactic:
positivity [hw₀ j <| erase_subset _ _ hj]

Premises used: Finset.erase_subset
-- 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_1 : 0 < w i
hwi_2 : 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_1 : 0 < 1 - ε
hwi : 0 < 1 - w i
this :
  Wbtw 𝕜 (P := V) ((lineMap x (a i) : (a : 𝕜) → V) ε : V)
    ((lineMap x (∑ j ∈ t, w j • a j) : (a : 𝕜) → V) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) : V)
    (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j : V)
inr : (∑ i ∈ t.erase i, w i) / (1 - w i) = 1
inr₁ : (∑ x ∈ t, w x - w i) / (1 - w i) = 1
inr₂ : (1 - w i) / (1 - w i) = 1
inr₃ inr₄ : Eq.{u_1 + 1} (α := 𝕜) 1 1
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i_1 ∈ t.erase i, w i_1 / (1 - w i)) 1

Tactic:
rw [← sum_div, sum_erase_eq_sub hi, hw₁, div_self hwi.ne']

Premises used: LT.lt.ne', Finset.sum_div, Finset.sum_erase_eq_sub, div_self
-- 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_1 : 0 < w i
hwi_2 : 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_1 : 0 < 1 - ε
hwi : 0 < 1 - w i
this :
  Wbtw 𝕜 (P := V) ((lineMap x (a i) : (a : 𝕜) → V) ε : V)
    ((lineMap x (∑ j ∈ t, w j • a j) : (a : 𝕜) → V) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) : V)
    (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j : V)
⊢ ∀ i_1 ∈ t.erase i, Membership.mem (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V) (a i_1)

Tactic:
fun j hj ↦ subset_convexHull _ _ <| ha _ <| erase_subset _ _ hj

Premises used: subset_convexHull, Finset.erase_subset
-- 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_1 : 0 < w i
hwi_2 : 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_1 : 0 < 1 - ε
hwi : 0 < 1 - w i
this :
  Wbtw 𝕜 (P := V) ((lineMap x (a i) : (a : 𝕜) → V) ε : V)
    ((lineMap x (∑ j ∈ t, w j • a j) : (a : 𝕜) → V) ((w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) : V)
    (∑ j ∈ t.erase i, (w j / (1 - w i)) • a j : V)
⊢ ∀ i_1 ∈ t.erase i, Membership.mem (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V) (a i_1)

Tactic:
exact fun j hj ↦ subset_convexHull _ _ <| ha _ <| erase_subset _ _ hj

Premises used: subset_convexHull, Finset.erase_subset
-- 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_1 : 0 < w i
hwi_2 : 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
⊢ 0 < (1 - ε) / ε

Tactic:
positivity
-- 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_1 : 0 < w i
hwi_2 : 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)⁻¹

Tactic:
exact lt_add_of_pos_left _ <| by positivity

Premises used: lt_add_of_pos_left
-- 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 y : V
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
by_contra! : ∀ (hxy : x ≠ y), False
⊢ x = y

Tactic:
by_contra! hxy
-- 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 y : V
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
h : ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False
⊢ False

Tactic:
obtain ⟨_, ⟨⟩⟩ := h.exists

Premises used: Filter.Eventually.exists
-- 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 y : V
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
suffices : ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False
⊢ False

Tactic:
suffices h : ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False by obtain ⟨_, ⟨⟩⟩ := h.exists
-- 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 y : V
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
⊢ Membership.mem (γ := Filter V) (𝓝 ((lineMap y x : (a : 𝕜) → V) 0) : Filter V) s

Tactic:
simpa using mem_interior_iff_mem_nhds.1 hy

Premises used: mem_interior_iff_mem_nhds, Iff.mp
-- 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 y : V
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
⊢ ∀ᶠ (δ : 𝕜) in 𝓝[>] 0, Membership.mem (α := V) s ((lineMap y x : (a : 𝕜) → V) δ : V)

Tactic:
have hmem : ∀ᶠ (δ : 𝕜) in 𝓝[>] 0, lineMap y x δ ∈ s :=
    lineMap_continuous.continuousWithinAt.eventually_mem
      (by simpa using mem_interior_iff_mem_nhds.1 hy)
-- 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 y : V
inst_5 : TopologicalSpace 𝕜
inst_6 : OrderTopology 𝕜
inst_7 : TopologicalSpace V
inst_8 : IsTopologicalAddGroup V
inst_9 : ContinuousSMul 𝕜 V
hsxy : IsVisible 𝕜 s x y
hy : y ∈ interior s
hxy : x ≠ y
hmem_1 : ∀ᶠ (δ : 𝕜) in 𝓝[>] 0, Membership.mem (α := V) s ((lineMap y x : (a : 𝕜) → V) δ : V)
δ : 𝕜
hmem : Membership.mem (α := V) s ((lineMap y x : (a : 𝕜) → V) δ : V)
hsbt : Membership.mem (γ := Set 𝕜) (Set.Ioo 0 1) δ
⊢ Sbtw 𝕜 y ((lineMap y x : (a : 𝕜) → V) δ) x

Tactic:
aesop