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 : 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)
⊢ IsVisible 𝕜 ((convexHull 𝕜 : (a : Set V) → Set V) s) x (a i)
have 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
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 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
⊢ x = y
have by_contra! : ∀ (hxy : x ≠ y), False
Tactic: by_contra! hxy
-- 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 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
⊢ False
have suffices : ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False
Tactic: suffices h : ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False by obtain ⟨_, ⟨⟩⟩ := h.exists
-- 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 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, False
have hmem : ∀ᶠ (δ : 𝕜) 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)
-- 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 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 : ∀ᶠ (δ : 𝕜) in 𝓝[>] 0, Membership.mem (α := V) s ((lineMap y x : (a : 𝕜) → V) δ : V)
⊢ ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False
have h : ∀ (a : 𝕜),
  Membership.mem (γ := Set 𝕜)
    {x_1 : 𝕜 |
      Membership.mem (γ := Set 𝕜)
          {x_2 : 𝕜 | (fun (δ : 𝕜) ↦ Membership.mem (α := V) s ((lineMap y x : (a : 𝕜) → V) δ : V)) x_2} x_1 →
        Membership.mem (γ := Set 𝕜)
          {x : 𝕜 |
            Membership.mem (γ := Set 𝕜) (Set.Ioo 0 1) x →
              Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (_δ : 𝕜) ↦ False) x} x}
          x_1}
    a
Tactic: filter_upwards [hmem, Ioo_mem_nhdsGT zero_lt_one] with δ hmem hsbt using hsxy.symm hmem (by aesop)
-- 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 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 : ∀ᶠ (δ : 𝕜) in 𝓝[>] 0, Membership.mem (α := V) s ((lineMap y x : (a : 𝕜) → V) δ : V)
h :
  ∀ (a : 𝕜),
    Membership.mem (γ := Set 𝕜)
      {x_1 : 𝕜 |
        Membership.mem (γ := Set 𝕜)
            {x_2 : 𝕜 | (fun (δ : 𝕜) ↦ Membership.mem (α := V) s ((lineMap y x : (a : 𝕜) → V) δ : V)) x_2} x_1 →
          Membership.mem (γ := Set 𝕜)
            {x : 𝕜 |
              Membership.mem (γ := Set 𝕜) (Set.Ioo 0 1) x →
                Membership.mem (γ := Set 𝕜) {x : 𝕜 | (fun (_δ : 𝕜) ↦ False) x} x}
            x_1}
      a
⊢ ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False
have h₁ : ∀ (a : 𝕜),
  Membership.mem (α := V) s ((lineMap y x : (a : 𝕜) → V) a : V) → Membership.mem (γ := Set 𝕜) (Set.Ioo 0 1) a → False
Tactic: filter_upwards [hmem, Ioo_mem_nhdsGT zero_lt_one] with δ hmem hsbt using hsxy.symm hmem (by aesop)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x y : V
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
hy : Membership.mem (γ := Set V) ((convexHull ℝ : (a : Set V) → Set V) s : Set V) y
hxy : IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y
⊢ Membership.mem (γ := Set V)
    ((convexHull ℝ : (a : Set V) → Set V) {z : V | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x z} :
      Set V)
    y
have obtain : ∀ (ι : Type) (w : Fintype ι) (w_1 : ι → ℝ) (a : ι → V) (hw₀ : ∀ (i : ι), 0 ≤ w_1 i)
  (hw₁ : Eq (α := ℝ) (∑ i : ι, w_1 i) 1) (ha : ∀ (i : ι), a i ∈ s)
  (hy : Membership.mem (γ := Set V) ((convexHull ℝ : (a : Set V) → Set V) s : Set V) (∑ i : ι, w_1 i • a i))
  (hxy : IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x (∑ i : ι, w_1 i • a i)),
  Membership.mem (γ := Set V)
    ((convexHull ℝ : (a : Set V) → Set V) {z : V | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x z} :
      Set V)
    (∑ i : ι, w_1 i • a i)
Tactic: obtain ⟨ι, _, w, a, hw₀, hw₁, ha, rfl⟩ := mem_convexHull_iff_exists_fintype.1 hy
Cleared hypotheses: y, hy, hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x : V
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
ι : Type
w_1 : Fintype ι
w : ι → ℝ
a : ι → V
hw₀ : ∀ (i : ι), 0 ≤ w i
hw₁ : Eq (α := ℝ) (∑ i : ι, w i) 1
ha : ∀ (i : ι), a i ∈ s
hy : Membership.mem (γ := Set V) ((convexHull ℝ : (a : Set V) → Set V) s : Set V) (∑ i : ι, w i • a i)
hxy : IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x (∑ i : ι, w i • a i)
⊢ Membership.mem (γ := Set V)
    ((convexHull ℝ : (a : Set V) → Set V) {z : V | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x z} :
      Set V)
    (∑ i : ι, w i • a i)
have rw : Membership.mem (γ := Set V)
  ((convexHull ℝ : (a : Set V) → Set V) {z : V | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x z} :
    Set V)
  (∑ i : ι with w i ≠ 0, w i • a i)
Tactic: rw [← Fintype.sum_subset (s := {i | w i ≠ 0})
    fun i hi ↦ mem_filter.2 ⟨mem_univ _, left_ne_zero_of_smul hi⟩]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x y : V
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
hy : Membership.mem (γ := Set V) ((convexHull ℝ : (a : Set V) → Set V) s : Set V) y
hxy : IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y
⊢ Membership.mem (γ := Set V)
    ((convexHull ℝ : (a : Set V) → Set V) {z : V | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x z} :
      Set V)
    y
have obtain : ∀ (ι : Type) (w : Fintype ι) (w_1 : ι → ℝ) (a : ι → V) (hw₀ : ∀ (i : ι), 0 ≤ w_1 i)
  (hw₁ : Eq (α := ℝ) (∑ i : ι, w_1 i) 1) (ha : ∀ (i : ι), a i ∈ s)
  (hy : Membership.mem (γ := Set V) ((convexHull ℝ : (a : Set V) → Set V) s : Set V) (∑ i : ι, w_1 i • a i))
  (hxy : IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x (∑ i : ι, w_1 i • a i)),
  Membership.mem (γ := Set V)
    ((convexHull ℝ : (a : Set V) → Set V) {z : V | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x z} :
      Set V)
    (∑ i : ι, w_1 i • a i)
Tactic: classical
  obtain ⟨ι, _, w, a, hw₀, hw₁, ha, rfl⟩ := mem_convexHull_iff_exists_fintype.1 hy
  rw [← Fintype.sum_subset (s := {i | w i ≠ 0})
    fun i hi ↦ mem_filter.2 ⟨mem_univ _, left_ne_zero_of_smul hi⟩]
  exact (convex_convexHull ..).sum_mem (fun i _ ↦ hw₀ _) (by rwa [sum_filter_ne_zero])
    fun i hi ↦ subset_convexHull _ _ ⟨ha _, IsVisible.of_convexHull_of_pos (fun _ _ ↦ hw₀ _) hw₁
      (by simpa) hx hxy (mem_univ _) <| (hw₀ _).lt_of_ne' (mem_filter.1 hi).2⟩
Cleared hypotheses: y, hy, hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x y : V
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
hy : Membership.mem (γ := Set V) ((convexHull ℝ : (a : Set V) → Set V) s : Set V) y
hxy : IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y
obtain :
  ∀ (ι : Type) (w : Fintype ι) (w_1 : ι → ℝ) (a : ι → V) (hw₀ : ∀ (i : ι), 0 ≤ w_1 i)
    (hw₁ : Eq (α := ℝ) (∑ i : ι, w_1 i) 1) (ha : ∀ (i : ι), a i ∈ s)
    (hy : Membership.mem (γ := Set V) ((convexHull ℝ : (a : Set V) → Set V) s : Set V) (∑ i : ι, w_1 i • a i))
    (hxy : IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x (∑ i : ι, w_1 i • a i)),
    Membership.mem (γ := Set V)
      ((convexHull ℝ : (a : Set V) → Set V) {z : V | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x z} :
        Set V)
      (∑ i : ι, w_1 i • a i)
⊢ Membership.mem (γ := Set V)
    ((convexHull ℝ : (a : Set V) → Set V) {z : V | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x z} :
      Set V)
    y
have obtain₁ : ∀ (ι : Type) (w : Fintype ι) (w_1 : ι → ℝ) (a : ι → V) (hw₀ : ∀ (i : ι), 0 ≤ w_1 i)
  (hw₁ : Eq (α := ℝ) (∑ i : ι, w_1 i) 1) (ha : ∀ (i : ι), a i ∈ s)
  (hy : Membership.mem (γ := Set V) ((convexHull ℝ : (a : Set V) → Set V) s : Set V) (∑ i : ι, w_1 i • a i))
  (hxy : IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x (∑ i : ι, w_1 i • a i)),
  Membership.mem (γ := Set V)
    ((convexHull ℝ : (a : Set V) → Set V) {z : V | z ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x z} :
      Set V)
    (∑ i : ι with w_1 i ≠ 0, w_1 i • a i)
Tactic: classical
  obtain ⟨ι, _, w, a, hw₀, hw₁, ha, rfl⟩ := mem_convexHull_iff_exists_fintype.1 hy
  rw [← Fintype.sum_subset (s := {i | w i ≠ 0})
    fun i hi ↦ mem_filter.2 ⟨mem_univ _, left_ne_zero_of_smul hi⟩]
  exact (convex_convexHull ..).sum_mem (fun i _ ↦ hw₀ _) (by rwa [sum_filter_ne_zero])
    fun i hi ↦ subset_convexHull _ _ ⟨ha _, IsVisible.of_convexHull_of_pos (fun _ _ ↦ hw₀ _) hw₁
      (by simpa) hx hxy (mem_univ _) <| (hw₀ _).lt_of_ne' (mem_filter.1 hi).2⟩
Cleared hypotheses: y, hy, hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (hypothesis)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
y : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ (⇑(lineMap x y) : (a : ℝ) → V) ⁻¹' s
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z
have ht₁ : 1 ∈ t
Tactic: have ht₁ : 1 ∈ t := by simpa [t]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (hypothesis)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
y : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ (⇑(lineMap x y) : (a : ℝ) → V) ⁻¹' s
ht₁ : 1 ∈ t
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z
have ht : BddBelow t
Tactic: have ht : BddBelow t := bddBelow_Ici.inter_of_left
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (hypothesis)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
y : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ (⇑(lineMap x y) : (a : ℝ) → V) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z
have hδ₁ : δ ≤ 1
Tactic: have hδ₁ : δ ≤ 1 := csInf_le ht ht₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (hypothesis)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
y : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ (⇑(lineMap x y) : (a : ℝ) → V) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z
have hδ₀ : 0 ≤ δ
Tactic: obtain ⟨hδ₀, hδ⟩ : 0 ≤ δ ∧ lineMap x y δ ∈ s :=
    (isClosed_Ici.inter <| hs.preimage lineMap_continuous).csInf_mem ⟨1, ht₁⟩ ht
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (hypothesis)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
y : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ (⇑(lineMap x y) : (a : ℝ) → V) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ₀ : 0 ≤ δ
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z
have hδ : Membership.mem (α := V) s ((lineMap x y : (a : ℝ) → V) δ : V)
Tactic: obtain ⟨hδ₀, hδ⟩ : 0 ≤ δ ∧ lineMap x y δ ∈ s :=
    (isClosed_Ici.inter <| hs.preimage lineMap_continuous).csInf_mem ⟨1, ht₁⟩ ht
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
y : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ (⇑(lineMap x y) : (a : ℝ) → V) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ₀ : 0 ≤ δ
hδ : Membership.mem (α := V) s ((lineMap x y : (a : ℝ) → V) δ : V)
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z
have refine : IsVisible ℝ s x ((lineMap x y : (a : ℝ) → V) δ)
Tactic: refine ⟨lineMap x y δ, hδ, wbtw_lineMap_iff.2 <| .inr ⟨hδ₀, hδ₁⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (hypothesis)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
y : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ (⇑(lineMap x y) : (a : ℝ) → V) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ₀ : 0 ≤ δ
hδ : Membership.mem (α := V) s ((lineMap x y : (a : ℝ) → V) δ : V)
ε : ℝ
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
hε : Membership.mem (α := V) s ((lineMap x ((lineMap x y : (a : ℝ) → V) δ) : (a : ℝ) → V) ε : V)
h : Ne (α := V) ((lineMap x ((lineMap x y : (a : ℝ) → V) δ) : (a : ℝ) → V) ε : V) ((lineMap x y : (a : ℝ) → V) δ : V)
⊢ False
have hδ₂ : 0 < δ
Tactic: replace hδ₀ : 0 < δ := hδ₀.lt_of_ne' <| by rintro hδ₀; simp [hδ₀] at h
Cleared hypotheses: hδ₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (hypothesis)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
y : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ (⇑(lineMap x y) : (a : ℝ) → V) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ : Membership.mem (α := V) s ((lineMap x y : (a : ℝ) → V) δ : V)
ε : ℝ
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
hε : Membership.mem (α := V) s ((lineMap x ((lineMap x y : (a : ℝ) → V) δ) : (a : ℝ) → V) ε : V)
h : Ne (α := V) ((lineMap x ((lineMap x y : (a : ℝ) → V) δ) : (a : ℝ) → V) ε : V) ((lineMap x y : (a : ℝ) → V) δ : V)
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 (hypothesis)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
y : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] s
hy : y ∈ s
x : V
t : Set ℝ := Set.Ici 0 ∩ (⇑(lineMap x y) : (a : ℝ) → V) ⁻¹' s
ht₁ : 1 ∈ t
ht : BddBelow t
δ : ℝ := sInf t
hδ₁ : δ ≤ 1
hδ : Membership.mem (α := V) s ((lineMap x y : (a : ℝ) → V) δ : V)
ε : ℝ
hε₀ : 0 ≤ ε
hε : Membership.mem (α := V) s ((lineMap x ((lineMap x y : (a : ℝ) → V) δ) : (a : ℝ) → V) ε : V)
h : Ne (α := V) ((lineMap x ((lineMap x y : (a : ℝ) → V) δ) : (a : ℝ) → V) ε : V) ((lineMap x y : (a : ℝ) → V) δ : V)
hδ₀ : 0 < δ
hε₁ : ε < 1
⊢ False
have hε₂ : Membership.mem (α := V) s ((lineMap x y : (a : ℝ) → V) (ε * δ) : V)
Tactic: rw [lineMap_lineMap_right] at hε
Cleared hypotheses: hε, h, hδ₀, hε₁
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] ((convexHull ℝ : (a : Set V) → Set V) s)
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
y : V
hy : Membership.mem (γ := Set V) ((convexHull ℝ : (a : Set V) → Set V) s : Set V) y
⊢ y ∈ (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V)
have obtain : ∀ (z : V) (hz : Membership.mem (γ := Set V) ((convexHull ℝ : (a : Set V) → Set V) s : Set V) z) (hxzy : Wbtw ℝ x z y)
  (hxz : IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x z),
  y ∈ (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V)
Tactic: obtain ⟨z, hz, hxzy, hxz⟩ := hs.exists_wbtw_isVisible hy x
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] ((convexHull ℝ : (a : Set V) → Set V) s)
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
⊢ Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
    Module.rank ℝ
      ↥(span ℝ
          (↑(HVAdd.hVAdd (β := AffineSubspace ℝ V) (-x)
                (affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))) :
            Set V))
have push_cast : Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
  Module.rank ℝ
    ↥(span ℝ
        (-x +ᵥ
          (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V)))
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] ((convexHull ℝ : (a : Set V) → Set V) s)
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
⊢ Module.rank ℝ ↥(span ℝ (-x +ᵥ s)) ≤
    Module.rank ℝ
      ↥(span ℝ
          (-x +ᵥ
            (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) :
              Set V)))
have refine : LE.le (α := Submodule ℝ V) (span ℝ (-x +ᵥ s))
  (span ℝ
    (-x +ᵥ
      (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V)))
Tactic: refine Submodule.rank_mono ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] ((convexHull ℝ : (a : Set V) → Set V) s)
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
⊢ LE.le (α := Submodule ℝ V) (span ℝ (-x +ᵥ s))
    (span ℝ
      (-x +ᵥ
        (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V)))
have h : s ⊆ (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Visible (goal)
Goal:
V : Type u_2
inst : AddCommGroup V
inst_1 : Module ℝ V
s : Set V
x : V
inst_2 : TopologicalSpace V
inst_3 : IsTopologicalAddGroup V
inst_4 : ContinuousSMul ℝ V
hs : IsClosed[inst_2] ((convexHull ℝ : (a : Set V) → Set V) s)
hx : x ∉ ((convexHull ℝ : (a : Set V) → Set V) s : Set V)
h :
  -x +ᵥ (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) : Set V) =
    (↑(span ℝ
          (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) :
      Set V)
⊢ Module.rank ℝ
      ↥(span ℝ
          (↑(HVAdd.hVAdd (β := AffineSubspace ℝ V) (-x)
                (affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))) :
            Set V)) =
    Module.rank ℝ
      ↥(span ℝ
          (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))
have rw : Module.rank ℝ
    ↥(span ℝ
        (-x +ᵥ
          (↑(affineSpan ℝ ({x} ∪ {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y})) :
            Set V))) =
  Module.rank ℝ
    ↥(span ℝ (HVAdd.hVAdd (β := Set V) (-x) {y : V | y ∈ s ∧ IsVisible ℝ ((convexHull ℝ : (a : Set V) → Set V) s) x y}))
Tactic: rw [AffineSubspace.coe_pointwise_vadd, h, span_span]