awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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
have hε₂ : 0 < ε
Tactic: replace hε₀ : 0 < ε := hε₀.lt_of_ne <| by rintro rfl; simp at h
Cleared hypotheses: hε₀
-- 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 : 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
have hε₂ : ε < 1
Tactic: replace hε₁ : ε < 1 := hε₁.lt_of_ne <| by rintro rfl; simp at h
Cleared hypotheses: hε₁
-- 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 : 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
⊢ 0 < 1 - ε
have linarith : 1 - ε ≤ 0 → ε - 1 + (1 - ε - 0) = 0
Tactic: linarith
-- 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 : 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
have this : 0 < 1 - ε
Tactic: have : 0 < 1 - ε := by linarith
-- 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 : 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 - ε
⊢ 0 < 1 - w i
have linarith : 1 - w i ≤ 0 → w i - 1 + (1 - w i - 0) = 0
Tactic: linarith
-- 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 : 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
have hwi₁ : 0 < 1 - w i
Tactic: have hwi : 0 < 1 - w i := by linarith
-- 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 : 0 < 1 - ε
hwi : 0 < 1 - w i
⊢ False
have inr : 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 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 ?_⟩
-- 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 : 0 < 1 - ε
hwi : 0 < 1 - w i
inr :
  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)
⊢ False
have inr₁ : (w i)⁻¹ < (1 - ε) / ε + (w i)⁻¹
Tactic: 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 ?_⟩
-- 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 : 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)
have refine_1 : (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1) ≤ 1
Tactic: refine ⟨((1 - w i) / w i) / ((1 - ε) / ε + (1 - w i) / w i + 1), ⟨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_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
refine_1 : (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1) ≤ 1
⊢ 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)
have refine_2 : 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: refine ⟨((1 - w i) / w i) / ((1 - ε) / ε + (1 - w i) / w i + 1), ⟨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_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
⊢ (1 - w i) / w i / ((1 - ε) / ε + (1 - w i) / w i + 1) ≤ 1
have refine_1 : (1 - w i) / w i ≤ (1 - ε) / ε + (1 - w i) / w i + 1
Tactic: refine (div_le_one <| by positivity).2 ?_
-- 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 : 0 < 1 - ε
hwi : 0 < 1 - w i
⊢ 0 + (1 - w i) / w i + 0 ≤ (1 - ε) / ε + (1 - w i) / w i + 1
have h₁ : 0 ≤ (1 - ε) / ε
Tactic: gcongr
-- 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 : 0 < 1 - ε
hwi : 0 < 1 - w i
h₁ : 0 ≤ (1 - ε) / ε
⊢ 0 + (1 - w i) / w i + 0 ≤ (1 - ε) / ε + (1 - w i) / w i + 1
have h₂ : LE.le.{u_1} (α := 𝕜) 0 1
Tactic: gcongr
-- 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 : 0 < 1 - ε
hwi : 0 < 1 - w i
⊢ (1 - w i) / w i ≤ (1 - ε) / ε + (1 - w i) / w i + 1
have w₁ : (1 - w i) / w i = 0 + (1 - w i) / w i + 0
Tactic: 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
-- 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 : 0 < 1 - ε
hwi : 0 < 1 - w i
w₁ : (1 - w i) / w i = 0 + (1 - w i) / w i + 0
⊢ (1 - w i) / w i ≤ (1 - ε) / ε + (1 - w i) / w i + 1
have w₂ : 0 + (1 - w i) / w i + 0 ≤ (1 - ε) / ε + (1 - w i) / w i + 1
Tactic: 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
-- 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 : 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
have rw : 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: rw [smul_sum]
-- 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 : 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
have simp_rw : w i • a i + ∑ x ∈ t.erase i, w x • a x = ∑ j ∈ t, w j • a j
Tactic: simp_rw [smul_smul, mul_div_cancel₀ _ hwi.ne']
-- 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
⊢ 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)
have 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
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
-- 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
⊢ 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)
have 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))
Tactic: simp_rw [lineMap_apply_module, ← this]
-- 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
⊢ (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 - ε) * 1) =
  (1 - (w i)⁻¹ / ((1 - ε) / ε + (w i)⁻¹)) * 1
Tactic: match_scalars