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 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
h₁ h₂ :
  ∀ (δ : 𝕜) (hmem : Membership.mem (α := V) s ((lineMap y x : (a : 𝕜) → V) δ : V))
    (hsbt : Membership.mem (γ := Set 𝕜) (Set.Ioo 0 1) δ), False
⊢ ∀ᶠ (_δ : 𝕜) in 𝓝[>] 0, False

Tactic:
filter_upwards [hmem, Ioo_mem_nhdsGT zero_lt_one] with δ hmem hsbt using hsxy.symm hmem (by aesop)

Premises used: IsVisible.symm, zero_lt_one, Ioo_mem_nhdsGT
-- 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
hs : IsOpen[inst_7] s
hsxy : IsVisible 𝕜 s x y
hy : y ∈ s
⊢ y ∈ interior s

Tactic:
simpa [hs.interior_eq]

Premises used: IsOpen.interior_eq
-- Module: Mathlib.Analysis.Convex.Visible
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

Tactic:
obtain ⟨ι, _, w, a, hw₀, hw₁, ha, rfl⟩ := mem_convexHull_iff_exists_fintype.1 hy

Premises used: mem_convexHull_iff_exists_fintype, Iff.mp, IsVisible.rfl
-- Module: Mathlib.Analysis.Convex.Visible
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)
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)
⊢ 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)

Tactic:
rw [← Fintype.sum_subset (s := {i | w i ≠ 0})
    fun i hi ↦ mem_filter.2 ⟨mem_univ _, left_ne_zero_of_smul hi⟩]

Premises used: Iff.mpr, Finset.mem_univ, left_ne_zero_of_smul, And.intro, Finset.mem_filter, Fintype.sum_subset
-- Module: Mathlib.Analysis.Convex.Visible
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)
rwa rwa₁ rwa₂ rwa₃ : Eq (α := ℝ) (∑ x : ι, w x) 1
⊢ Eq (α := ℝ) (∑ i : ι with w i ≠ 0, w i) 1

Tactic:
rwa [sum_filter_ne_zero]

Premises used: Finset.sum_filter_ne_zero
-- Module: Mathlib.Analysis.Convex.Visible
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)
i : ι
hi : Membership.mem (γ := Finset ι) {i : ι | w i ≠ 0} i
⊢ ∀ (i : ι), Membership.mem (γ := Finset ι) Finset.univ i → a i ∈ s

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.Visible
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 : ι with w i ≠ 0, w i • a i)

Tactic:
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⟩
-- Module: Mathlib.Analysis.Convex.Visible
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)
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)
⊢ 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

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⟩

Premises used: mem_convexHull_iff_exists_fintype, Iff.mp, IsVisible.rfl
-- Module: Mathlib.Analysis.Convex.Visible
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
⊢ 1 ∈ t

Tactic:
simpa [t]
-- Module: Mathlib.Analysis.Convex.Visible
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
⊢ 1 ∈ t

Tactic:
have ht₁ : 1 ∈ t := by simpa [t]
-- Module: Mathlib.Analysis.Convex.Visible
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
⊢ BddBelow t

Tactic:
have ht : BddBelow t := bddBelow_Ici.inter_of_left
-- Module: Mathlib.Analysis.Convex.Visible
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
⊢ δ ≤ 1

Tactic:
have hδ₁ : δ ≤ 1 := csInf_le ht ht₁
-- Module: Mathlib.Analysis.Convex.Visible
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
⊢ 0 ≤ δ ∧ Membership.mem (α := V) s ((lineMap x y : (a : ℝ) → V) δ : V)

Tactic:
(isClosed_Ici.inter <| hs.preimage lineMap_continuous).csInf_mem ⟨1, ht₁⟩ ht

Premises used: Set.Ici, Set.Mem, setOf, AffineMap.lineMap_continuous, Set.inter, Set.preimage, Exists.intro, IsClosed.preimage, IsClosed.inter, IsClosed.csInf_mem, OfNat.ofNat, isClosed_Ici
-- Module: Mathlib.Analysis.Convex.Visible
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
⊢ 0 ≤ δ

Tactic:
obtain ⟨hδ₀, hδ⟩ : 0 ≤ δ ∧ lineMap x y δ ∈ s :=
    (isClosed_Ici.inter <| hs.preimage lineMap_continuous).csInf_mem ⟨1, ht₁⟩ ht

Premises used: AffineMap.lineMap, AffineMap.lineMap_continuous, Exists.intro, IsClosed.preimage, IsClosed.inter, IsClosed.csInf_mem, OfNat.ofNat, DFunLike.coe, isClosed_Ici
-- Module: Mathlib.Analysis.Convex.Visible
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 ≤ δ
⊢ 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

Premises used: AffineMap.lineMap, AffineMap.lineMap_continuous, Exists.intro, IsClosed.preimage, IsClosed.inter, IsClosed.csInf_mem, OfNat.ofNat, DFunLike.coe, isClosed_Ici
-- Module: Mathlib.Analysis.Convex.Visible
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

Tactic:
⟨lineMap x y δ, hδ, wbtw_lineMap_iff.2 <| .inr ⟨hδ₀, hδ₁⟩, ?_⟩

Premises used: Iff.mpr, wbtw_lineMap_iff, AffineMap.lineMap, And.intro, Exists.intro, DFunLike.coe, Or.inr
-- Module: Mathlib.Analysis.Convex.Visible
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)
refine : IsVisible ℝ s x ((lineMap x y : (a : ℝ) → V) δ)
⊢ ∃ z ∈ s, Wbtw ℝ x z y ∧ IsVisible ℝ s x z

Tactic:
refine ⟨lineMap x y δ, hδ, wbtw_lineMap_iff.2 <| .inr ⟨hδ₀, hδ₁⟩, ?_⟩
-- Module: Mathlib.Analysis.Convex.Visible
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δ₀_1 : 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)
hδ₀ : δ = 0
⊢ False

Tactic:
simp [hδ₀] at h
-- Module: Mathlib.Analysis.Convex.Visible
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)
⊢ 0 < δ

Tactic:
replace hδ₀ : 0 < δ := hδ₀.lt_of_ne' <| by rintro hδ₀; simp [hδ₀] at h
-- Module: Mathlib.Analysis.Convex.Visible
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ε₀ : LE.le (α := ℝ) 0 1
hε₁ : LE.le (α := ℝ) 1 1
hε : Membership.mem (α := V) s ((lineMap x ((lineMap x y : (a : ℝ) → V) δ) : (a : ℝ) → V) 1 : V)
h : Ne (α := V) ((lineMap x ((lineMap x y : (a : ℝ) → V) δ) : (a : ℝ) → V) 1 : V) ((lineMap x y : (a : ℝ) → V) δ : V)
⊢ False

Tactic:
simp at h
-- Module: Mathlib.Analysis.Convex.Visible
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 < δ
⊢ ε < 1

Tactic:
replace hε₁ : ε < 1 := hε₁.lt_of_ne <| by rintro rfl; simp at h
-- Module: Mathlib.Analysis.Convex.Visible
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
⊢ Membership.mem (α := V) s ((lineMap x y : (a : ℝ) → V) (ε * δ) : V)

Tactic:
rw [lineMap_lineMap_right] at hε

Premises used: AffineMap.lineMap_lineMap_right
-- Module: Mathlib.Analysis.Convex.Visible
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
hε₂ : Membership.mem (α := V) s ((lineMap x y : (a : ℝ) → V) (ε * δ) : V)
⊢ Ne (α := V) ((lineMap x ((lineMap x y : (a : ℝ) → V) δ) : (a : ℝ) → V) ε : V) ((lineMap x y : (a : ℝ) → V) δ : V)

Tactic:
rw [lineMap_lineMap_right] at hε

Premises used: AffineMap.lineMap_lineMap_right
-- Module: Mathlib.Analysis.Convex.Visible
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
hε₂ : Membership.mem (α := V) s ((lineMap x y : (a : ℝ) → V) (ε * δ) : V)
h₁ : Ne (α := V) ((lineMap x ((lineMap x y : (a : ℝ) → V) δ) : (a : ℝ) → V) ε : V) ((lineMap x y : (a : ℝ) → V) δ : V)
⊢ 0 < δ

Tactic:
rw [lineMap_lineMap_right] at hε

Premises used: AffineMap.lineMap_lineMap_right
-- Module: Mathlib.Analysis.Convex.Visible
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
hε₂ : Membership.mem (α := V) s ((lineMap x y : (a : ℝ) → V) (ε * δ) : V)
h₁ : Ne (α := V) ((lineMap x ((lineMap x y : (a : ℝ) → V) δ) : (a : ℝ) → V) ε : V) ((lineMap x y : (a : ℝ) → V) δ : V)
hδ₂ : 0 < δ
⊢ ε < 1

Tactic:
rw [lineMap_lineMap_right] at hε

Premises used: AffineMap.lineMap_lineMap_right
-- Module: Mathlib.Analysis.Convex.Visible
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 y : (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

Tactic:
(csInf_le ht ⟨mul_nonneg hε₀ hδ₀.le, hε⟩).not_gt <| mul_lt_of_lt_one_left hδ₀ hε₁

Premises used: mul_nonneg, LT.lt.le, LE.le.not_gt, And.intro, csInf_le, mul_lt_of_lt_one_left
-- Module: Mathlib.Analysis.Convex.Visible
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 y : (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

Tactic:
exact (csInf_le ht ⟨mul_nonneg hε₀ hδ₀.le, hε⟩).not_gt <| mul_lt_of_lt_one_left hδ₀ hε₁

Premises used: mul_nonneg, LT.lt.le, LE.le.not_gt, And.intro, csInf_le, mul_lt_of_lt_one_left
-- Module: Mathlib.Analysis.Convex.Visible
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
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)
⊢ 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

Premises used: IsClosed.exists_wbtw_isVisible
-- Module: Mathlib.Analysis.Convex.Visible
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
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:
AffineSubspace.right_mem_of_wbtw hxzy (subset_affineSpan _ _ <| subset_union_left rfl)
    (affineSpan_mono _ subset_union_right <| convexHull_subset_affineSpan _ <|
      hxz.mem_convexHull_isVisible hx hz) (ne_of_mem_of_not_mem hz hx).symm

Premises used: IsVisible.mem_convexHull_isVisible, Set.Mem, Set.subset_union_right, Ne.symm, ne_of_mem_of_not_mem, Set.subset_union_left, subset_affineSpan, affineSpan_mono, convexHull_subset_affineSpan, rfl, AffineSubspace.right_mem_of_wbtw