[GOAL]
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
⊢ interior (↑(convexHull ℝ) (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
[PROOFSTEP]
cases subsingleton_or_nontrivial ι
[GOAL]
case inl
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Subsingleton ι
⊢ interior (↑(convexHull ℝ) (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
[PROOFSTEP]
have : range b = univ := AffineSubspace.eq_univ_of_subsingleton_span_eq_top (subsingleton_range _) b.tot
[GOAL]
case inl
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Subsingleton ι
this : range ↑b = univ
⊢ interior (↑(convexHull ℝ) (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
[PROOFSTEP]
simp [this]
[GOAL]
case inr
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
⊢ interior (↑(convexHull ℝ) (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
[PROOFSTEP]
haveI : FiniteDimensional ℝ E := b.finiteDimensional
[GOAL]
case inr
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ interior (↑(convexHull ℝ) (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
[PROOFSTEP]
have : convexHull ℝ (range b) = ⋂ i, b.coord i ⁻¹' Ici 0 := by rw [b.convexHull_eq_nonneg_coord, setOf_forall]; rfl
[GOAL]
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ ↑(convexHull ℝ) (range ↑b) = ⋂ (i : ι), ↑(coord b i) ⁻¹' Ici 0
[PROOFSTEP]
rw [b.convexHull_eq_nonneg_coord, setOf_forall]
[GOAL]
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ ⋂ (i : ι), {x | 0 ≤ ↑(coord b i) x} = ⋂ (i : ι), ↑(coord b i) ⁻¹' Ici 0
[PROOFSTEP]
rfl
[GOAL]
case inr
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this✝ : FiniteDimensional ℝ E
this : ↑(convexHull ℝ) (range ↑b) = ⋂ (i : ι), ↑(coord b i) ⁻¹' Ici 0
⊢ interior (↑(convexHull ℝ) (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
[PROOFSTEP]
ext
[GOAL]
case inr.h
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this✝ : FiniteDimensional ℝ E
this : ↑(convexHull ℝ) (range ↑b) = ⋂ (i : ι), ↑(coord b i) ⁻¹' Ici 0
x✝ : E
⊢ x✝ ∈ interior (↑(convexHull ℝ) (range ↑b)) ↔ x✝ ∈ {x | ∀ (i : ι), 0 < ↑(coord b i) x}
[PROOFSTEP]
simp only [this, interior_iInter, ←
  IsOpenMap.preimage_interior_eq_interior_preimage (isOpenMap_barycentric_coord b _) (continuous_barycentric_coord b _),
  interior_Ici, mem_iInter, mem_setOf_eq, mem_Ioi, mem_preimage]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
hne : Set.Nonempty s
h : AffineIndependent ℝ Subtype.val
⊢ ∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
[PROOFSTEP]
obtain ⟨q, hq⟩ := hne
[GOAL]
case intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
⊢ ∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
[PROOFSTEP]
obtain ⟨ε, ε0, hεu⟩ := Metric.nhds_basis_closedBall.mem_iff.1 (hu.mem_nhds <| hsu hq)
[GOAL]
case intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
⊢ ∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
[PROOFSTEP]
obtain ⟨t, ht₁, ht₂, ht₃⟩ := exists_subset_affineIndependent_affineSpan_eq_top h
[GOAL]
case intro.intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
⊢ ∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
[PROOFSTEP]
let f : P → P := fun y => lineMap q y (ε / dist y q)
[GOAL]
case intro.intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
⊢ ∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
[PROOFSTEP]
have hf : ∀ y, f y ∈ u := by
  refine' fun y => hεu _
  simp only
  rw [Metric.mem_closedBall, lineMap_apply, dist_vadd_left, norm_smul, Real.norm_eq_abs, dist_eq_norm_vsub V y q,
    abs_div, abs_of_pos ε0, abs_of_nonneg (norm_nonneg _), div_mul_comm]
  exact mul_le_of_le_one_left ε0.le (div_self_le_one _)
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
⊢ ∀ (y : P), f y ∈ u
[PROOFSTEP]
refine' fun y => hεu _
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
y : P
⊢ f y ∈ Metric.closedBall q ε
[PROOFSTEP]
simp only
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
y : P
⊢ ↑(lineMap q y) (ε / dist y q) ∈ Metric.closedBall q ε
[PROOFSTEP]
rw [Metric.mem_closedBall, lineMap_apply, dist_vadd_left, norm_smul, Real.norm_eq_abs, dist_eq_norm_vsub V y q, abs_div,
  abs_of_pos ε0, abs_of_nonneg (norm_nonneg _), div_mul_comm]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
y : P
⊢ ‖y -ᵥ q‖ / ‖y -ᵥ q‖ * ε ≤ ε
[PROOFSTEP]
exact mul_le_of_le_one_left ε0.le (div_self_le_one _)
[GOAL]
case intro.intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
⊢ ∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
[PROOFSTEP]
have hεyq : ∀ (y) (_ : y ∉ s), ε / dist y q ≠ 0 := fun y hy =>
  div_ne_zero ε0.ne' (dist_ne_zero.2 (ne_of_mem_of_not_mem hq hy).symm)
[GOAL]
case intro.intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
⊢ ∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
[PROOFSTEP]
classical
let w : t → ℝˣ := fun p => if hp : (p : P) ∈ s then 1 else Units.mk0 _ (hεyq (↑p) hp)
refine' ⟨Set.range fun p : t => lineMap q p (w p : ℝ), _, _, _, _⟩
· intro p hp; use⟨p, ht₁ hp⟩; simp [hp]
· rintro y ⟨⟨p, hp⟩, rfl⟩
  by_cases hps : p ∈ s <;>
      simp only [hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff, Units.val_one,
        Subtype.coe_mk] <;>
    [exact hsu hps; exact hf p]
· exact (ht₂.units_lineMap ⟨q, ht₁ hq⟩ w).range
· rw [affineSpan_eq_affineSpan_lineMap_units (ht₁ hq) w, ht₃]
[GOAL]
case intro.intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
⊢ ∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
[PROOFSTEP]
let w : t → ℝˣ := fun p => if hp : (p : P) ∈ s then 1 else Units.mk0 _ (hεyq (↑p) hp)
[GOAL]
case intro.intro.intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p => if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) (_ : ε / dist (↑p) q ≠ 0)
⊢ ∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
[PROOFSTEP]
refine' ⟨Set.range fun p : t => lineMap q p (w p : ℝ), _, _, _, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p => if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) (_ : ε / dist (↑p) q ≠ 0)
⊢ s ⊆ range fun p => ↑(lineMap q ↑p) ↑(w p)
[PROOFSTEP]
intro p hp
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_1
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p => if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) (_ : ε / dist (↑p) q ≠ 0)
p : P
hp : p ∈ s
⊢ p ∈ range fun p => ↑(lineMap q ↑p) ↑(w p)
[PROOFSTEP]
use⟨p, ht₁ hp⟩
[GOAL]
case h
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p => if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) (_ : ε / dist (↑p) q ≠ 0)
p : P
hp : p ∈ s
⊢ (fun p => ↑(lineMap q ↑p) ↑(w p)) { val := p, property := (_ : p ∈ t) } = p
[PROOFSTEP]
simp [hp]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p => if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) (_ : ε / dist (↑p) q ≠ 0)
⊢ (range fun p => ↑(lineMap q ↑p) ↑(w p)) ⊆ u
[PROOFSTEP]
rintro y ⟨⟨p, hp⟩, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.intro.mk
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p => if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) (_ : ε / dist (↑p) q ≠ 0)
p : P
hp : p ∈ t
⊢ (fun p => ↑(lineMap q ↑p) ↑(w p)) { val := p, property := hp } ∈ u
[PROOFSTEP]
by_cases hps : p ∈ s <;>
    simp only [hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff, Units.val_one,
      Subtype.coe_mk] <;>
  [exact hsu hps; exact hf p]
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_2.intro.mk
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p => if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) (_ : ε / dist (↑p) q ≠ 0)
p : P
hp : p ∈ t
⊢ (fun p => ↑(lineMap q ↑p) ↑(w p)) { val := p, property := hp } ∈ u
[PROOFSTEP]
by_cases hps : p ∈ s
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p => if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) (_ : ε / dist (↑p) q ≠ 0)
p : P
hp : p ∈ t
hps : p ∈ s
⊢ (fun p => ↑(lineMap q ↑p) ↑(w p)) { val := p, property := hp } ∈ u
[PROOFSTEP]
simp only [hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff, Units.val_one, Subtype.coe_mk]
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p => if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) (_ : ε / dist (↑p) q ≠ 0)
p : P
hp : p ∈ t
hps : ¬p ∈ s
⊢ (fun p => ↑(lineMap q ↑p) ↑(w p)) { val := p, property := hp } ∈ u
[PROOFSTEP]
simp only [hps, lineMap_apply_one, Units.val_mk0, dif_neg, dif_pos, not_false_iff, Units.val_one, Subtype.coe_mk]
[GOAL]
case pos
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p => if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) (_ : ε / dist (↑p) q ≠ 0)
p : P
hp : p ∈ t
hps : p ∈ s
⊢ p ∈ u
[PROOFSTEP]
exact hsu hps
[GOAL]
case neg
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p => if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) (_ : ε / dist (↑p) q ≠ 0)
p : P
hp : p ∈ t
hps : ¬p ∈ s
⊢ ↑(lineMap q p) (ε / dist p q) ∈ u
[PROOFSTEP]
exact hf p
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_3
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p => if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) (_ : ε / dist (↑p) q ≠ 0)
⊢ AffineIndependent ℝ Subtype.val
[PROOFSTEP]
exact (ht₂.units_lineMap ⟨q, ht₁ hq⟩ w).range
[GOAL]
case intro.intro.intro.intro.intro.intro.refine'_4
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s u : Set P
hu : IsOpen u
hsu : s ⊆ u
h : AffineIndependent ℝ Subtype.val
q : P
hq : q ∈ s
ε : ℝ
ε0 : 0 < ε
hεu : Metric.closedBall q ε ⊆ u
t : Set P
ht₁ : s ⊆ t
ht₂ : AffineIndependent ℝ fun p => ↑p
ht₃ : affineSpan ℝ t = ⊤
f : P → P := fun y => ↑(lineMap q y) (ε / dist y q)
hf : ∀ (y : P), f y ∈ u
hεyq : ∀ (y : P), ¬y ∈ s → ε / dist y q ≠ 0
w : ↑t → ℝˣ := fun p => if hp : ↑p ∈ s then 1 else Units.mk0 (ε / dist (↑p) q) (_ : ε / dist (↑p) q ≠ 0)
⊢ affineSpan ℝ (range fun p => ↑(lineMap q ↑p) ↑(w p)) = ⊤
[PROOFSTEP]
rw [affineSpan_eq_affineSpan_lineMap_units (ht₁ hq) w, ht₃]
[GOAL]
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
hne : Set.Nonempty u
⊢ ∃ s x, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
[PROOFSTEP]
rcases hne with ⟨x, hx⟩
[GOAL]
case intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
x : P
hx : x ∈ u
⊢ ∃ s x, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
[PROOFSTEP]
rcases hu.exists_between_affineIndependent_span_eq_top (singleton_subset_iff.mpr hx) (singleton_nonempty _)
    (affineIndependent_of_subsingleton _ _) with
  ⟨s, -, hsu, hs⟩
[GOAL]
case intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
u : Set P
hu : IsOpen u
x : P
hx : x ∈ u
s : Set P
hsu : s ⊆ u
hs : AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
⊢ ∃ s x, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
[PROOFSTEP]
exact ⟨s, hsu, hs⟩
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ι : Type u_3
inst✝ : Fintype ι
b : AffineBasis ι ℝ V
⊢ Finset.centroid ℝ Finset.univ ↑b ∈ interior (↑(convexHull ℝ) (range ↑b))
[PROOFSTEP]
haveI := b.nonempty
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
ι : Type u_3
inst✝ : Fintype ι
b : AffineBasis ι ℝ V
this : Nonempty ι
⊢ Finset.centroid ℝ Finset.univ ↑b ∈ interior (↑(convexHull ℝ) (range ↑b))
[PROOFSTEP]
simp only [b.interior_convexHull, mem_setOf_eq, b.coord_apply_centroid (Finset.mem_univ _), inv_pos, Nat.cast_pos,
  Finset.card_pos, Finset.univ_nonempty, forall_true_iff]
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
⊢ Set.Nonempty (interior (↑(convexHull ℝ) s)) ↔ affineSpan ℝ s = ⊤
[PROOFSTEP]
refine' ⟨affineSpan_eq_top_of_nonempty_interior, fun h => _⟩
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
⊢ Set.Nonempty (interior (↑(convexHull ℝ) s))
[PROOFSTEP]
obtain ⟨t, hts, b, hb⟩ := AffineBasis.exists_affine_subbasis h
[GOAL]
case intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
⊢ Set.Nonempty (interior (↑(convexHull ℝ) s))
[PROOFSTEP]
suffices (interior (convexHull ℝ (range b))).Nonempty
  by
  rw [hb, Subtype.range_coe_subtype, setOf_mem_eq] at this 
  refine' this.mono _
  mono*
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
this : Set.Nonempty (interior (↑(convexHull ℝ) (range ↑b)))
⊢ Set.Nonempty (interior (↑(convexHull ℝ) s))
[PROOFSTEP]
rw [hb, Subtype.range_coe_subtype, setOf_mem_eq] at this 
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
this : Set.Nonempty (interior (↑(convexHull ℝ) t))
⊢ Set.Nonempty (interior (↑(convexHull ℝ) s))
[PROOFSTEP]
refine' this.mono _
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
this : Set.Nonempty (interior (↑(convexHull ℝ) t))
⊢ interior (↑(convexHull ℝ) t) ⊆ interior (↑(convexHull ℝ) s)
[PROOFSTEP]
mono*
[GOAL]
case intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ↑b = Subtype.val
⊢ Set.Nonempty (interior (↑(convexHull ℝ) (range ↑b)))
[PROOFSTEP]
lift t to Finset V using b.finite_set
[GOAL]
case intro.intro.intro.intro
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Finset V
hts : ↑t ⊆ s
b : AffineBasis ↑↑t ℝ V
hb : ↑b = Subtype.val
⊢ Set.Nonempty (interior (↑(convexHull ℝ) (range ↑b)))
[PROOFSTEP]
exact ⟨_, b.centroid_mem_interior_convexHull⟩
[GOAL]
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
inst✝ : FiniteDimensional ℝ V
s : Set V
hs : Convex ℝ s
⊢ Set.Nonempty (interior s) ↔ affineSpan ℝ s = ⊤
[PROOFSTEP]
rw [← interior_convexHull_nonempty_iff_affineSpan_eq_top, hs.convexHull_eq]
