awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
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
⊢ (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))
have match_scalars₁ : (1 - (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1)) * (ε * 1) = (w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹) * (w i * 1)
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
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)
⊢ (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))
have match_scalars₂ : (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1) * 1 = (w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹) * ((1 - w i) * 1)
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (hypothesis)
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
⊢ 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)
have 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)
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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
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)
have inr : ∀ i_1 ∈ t.erase i, 0 ≤ w i_1 / (1 - w i)
Tactic: refine (convex_convexHull _ _).mem_of_wbtw this hε <| (convex_convexHull _ _).sum_mem ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
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)
⊢ 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)
have inr₁ : Eq.{u_1 + 1} (α := 𝕜) (∑ i_1 ∈ t.erase i, w i_1 / (1 - w i)) 1
Tactic: refine (convex_convexHull _ _).mem_of_wbtw this hε <| (convex_convexHull _ _).sum_mem ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
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
⊢ 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)
have inr₂ : ∀ i_1 ∈ t.erase i, Membership.mem (γ := Set V) ((convexHull 𝕜 : (a : Set V) → Set V) s : Set V) (a i_1)
Tactic: refine (convex_convexHull _ _).mem_of_wbtw this hε <| (convex_convexHull _ _).sum_mem ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
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
⊢ 0 ≤ w j / (1 - w i)
have inr : 0 ≤ w j → 0 ≤ w j / (1 - w i)
Tactic: positivity [hw₀ j <| erase_subset _ _ hj]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
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)
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i_1 ∈ t.erase i, w i_1 / (1 - w i)) 1
have inr : (∑ i ∈ t.erase i, w i) / (1 - w i) = 1
Tactic: rw [← sum_div, sum_erase_eq_sub hi, hw₁, div_self hwi.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
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
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i_1 ∈ t.erase i, w i_1 / (1 - w i)) 1
have inr₁ : (∑ x ∈ t, w x - w i) / (1 - w i) = 1
Tactic: rw [← sum_div, sum_erase_eq_sub hi, hw₁, div_self hwi.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
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
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i_1 ∈ t.erase i, w i_1 / (1 - w i)) 1
have inr₂ : (1 - w i) / (1 - w i) = 1
Tactic: rw [← sum_div, sum_erase_eq_sub hi, hw₁, div_self hwi.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
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
⊢ Eq.{u_1 + 1} (α := 𝕜) (∑ i_1 ∈ t.erase i, w i_1 / (1 - w i)) 1
have inr₃ : Eq.{u_1 + 1} (α := 𝕜) 1 1
Tactic: rw [← sum_div, sum_erase_eq_sub hi, hw₁, div_self hwi.ne']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
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
⊢ IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)
have inl : ∀ (hwi : w i = 1), 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
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)
⊢ IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)
have inr : ∀ (hwi : w i < 1), 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