Theorem: ExtremePointsofHpolytope (src/MainTheorem.lean)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
⊢ ∀ x ∈ Hpolytope hH_, x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
Tactic:
rintro x hxH
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_) ↔ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
Tactic:
constructor
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_) → ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}

case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
⊢ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x} → x ∈ Set.extremePoints ℝ (Hpolytope hH_)

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_) → ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
Tactic:
intro hxEx
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : x ∈ Set.extremePoints ℝ (Hpolytope hH_)
⊢ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : x ∈ Set.extremePoints ℝ (Hpolytope hH_)
⊢ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
Tactic:
rw [Set.eq_singleton_iff_unique_mem]
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : x ∈ Set.extremePoints ℝ (Hpolytope hH_)
⊢ x ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) ∧ ∀ x_1 ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x), x_1 = x

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : x ∈ Set.extremePoints ℝ (Hpolytope hH_)
⊢ x ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) ∧ ∀ x_1 ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x), x_1 = x
Tactic:
refine ⟨ fun HiS ⟨ Hi_, hHi_, h ⟩ => h ▸ hHi_.2, ?_ ⟩
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : x ∈ Set.extremePoints ℝ (Hpolytope hH_)
⊢ ∀ x_1 ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x), x_1 = x

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : x ∈ Set.extremePoints ℝ (Hpolytope hH_)
⊢ ∀ x_1 ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x), x_1 = x
Tactic:
contrapose! hxEx
State after:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : ∃ x_1 ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x), x_1 ≠ x
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)

State before:
case mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hxEx : ∃ x_1 ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x), x_1 ≠ x
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)
Tactic:
rcases hxEx with ⟨ y, hy, hyx ⟩
State after:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)

State before:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)
Tactic:
have hxyy : x ∈ openSegment ℝ ((2:ℝ) • x - y) y := by
  clear hyx hy hxH hH_
  rw [openSegment_eq_image, Set.mem_image]
  refine ⟨ 1/2, by norm_num, ?_ ⟩
  rw [(by norm_num : (1:ℝ) - 1 / 2 = 1 / 2), smul_sub, sub_add_cancel, smul_smul,
    div_mul_cancel _ (by linarith), one_smul]
  done
State after:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)

State before:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)
Tactic:
have hmemsegmemI : ∀ v, v ∈ segment ℝ ((2:ℝ) • x - y) y →
  ∀ Hi_, Hi_ ∈ Hpolytope.I H_ x → v ∈ SetLike.coe Hi_ := by
  rintro v hv Hi_ hHi_
  rw [Set.mem_sInter] at hy
  specialize hy (frontier <| SetLike.coe Hi_) ⟨ Hi_, hHi_, rfl ⟩
  have hHi_2 := hHi_.2
  rw [frontierHalfspace_Hyperplane] at hy hHi_2
  apply IsClosed.frontier_subset <| Halfspace_closed Hi_
  rw [frontierHalfspace_Hyperplane]
  apply Set.mem_of_mem_of_subset hv
  apply (convex_iff_segment_subset.mp <| Hyperplane_convex Hi_) _ hy
  have h21 : Finset.sum Finset.univ ![(2:ℝ), -1] = 1 := by
    rw [Fin.sum_univ_two, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons]
    linarith
    done
  have h2x_y := Hyperplane_affineClosed Hi_ ![x, y] (by
    rw [Matrix.range_cons, Matrix.range_cons, Matrix.range_empty, Set.union_empty];
    exact Set.union_subset (Set.singleton_subset_iff.mpr hHi_2) (Set.singleton_subset_iff.mpr hy))
    ![2, -1] h21
  rw [Finset.affineCombination_eq_linear_combination _ _ _ h21, Fin.sum_univ_two, Matrix.cons_val_zero,
    Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.head_cons, neg_one_smul, ← sub_eq_add_neg] at h2x_y
  exact h2x_y
State after:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)

State before:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ x ∉ Set.extremePoints ℝ (Hpolytope hH_)
Tactic:
rw [mem_extremePoints]
State after:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ ¬(x ∈ Hpolytope hH_ ∧ ∀ x₁ ∈ Hpolytope hH_, ∀ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x)

State before:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ ¬(x ∈ Hpolytope hH_ ∧ ∀ x₁ ∈ Hpolytope hH_, ∀ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x)
Tactic:
push_neg
State after:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ x ∈ Hpolytope hH_ → ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)

State before:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ x ∈ Hpolytope hH_ → ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
rintro hxH'
State after:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)

State before:
case mp.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
rcases hmemballmemIc with ⟨ ε, hε, hmemballmemIc ⟩
State after:
case mp.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
ε : ℝ
hε : ε > 0
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)

State before:
case mp.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
ε : ℝ
hε : ε > 0
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
rcases hxSegBallInterSeg ((2:ℝ) • x - y) y ε ⟨ hxyy, fun h => hyx h.2 ⟩ hε with
  ⟨ x1, x2, hmem, hsub, hne ⟩
State after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
ε : ℝ
hε : ε > 0
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : ¬(x1 = x ∧ x2 = x)
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
ε : ℝ
hε : ε > 0
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : ¬(x1 = x ∧ x2 = x)
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
push_neg at hne
State after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
ε : ℝ
hε : ε > 0
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
hxH' : x ∈ Hpolytope hH_
ε : ℝ
hε : ε > 0
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
clear hxH' hε hyx hy hxH hxyy
State after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x₁ ∈ Hpolytope hH_, ∃ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
unfold Hpolytope
State after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x₁ ∈ ⋂₀ (SetLike.coe '' H_), ∃ x₂ ∈ ⋂₀ (SetLike.coe '' H_), x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hmem : x ∈ openSegment ℝ x1 x2
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hne : x1 = x → x2 ≠ x
⊢ ∃ x₁ ∈ ⋂₀ (SetLike.coe '' H_), ∃ x₂ ∈ ⋂₀ (SetLike.coe '' H_), x ∈ openSegment ℝ x₁ x₂ ∧ (x₁ = x → x₂ ≠ x)
Tactic:
refine ⟨ x1, ?_, x2, ?_, ⟨ hmem, hne ⟩ ⟩ <;> clear hmem hne <;>
rw [Set.mem_sInter] <;>
intro Hi_s hHi_s <;>
rw [Set.mem_image] at hHi_s <;>
rcases hHi_s with ⟨ Hi_, hHi_, rfl ⟩
State after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ x1 ∈ ↑Hi_

case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ x2 ∈ ↑Hi_

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
⊢ x ∈ openSegment ℝ (2 • x - y) y
Tactic:
clear hyx hy hxH hH_
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ x ∈ openSegment ℝ (2 • x - y) y

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ x ∈ openSegment ℝ (2 • x - y) y
Tactic:
rw [openSegment_eq_image, Set.mem_image]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ ∃ x_1 ∈ Set.Ioo 0 1, (1 - x_1) • (2 • x - y) + x_1 • y = x

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ ∃ x_1 ∈ Set.Ioo 0 1, (1 - x_1) • (2 • x - y) + x_1 • y = x
Tactic:
refine ⟨ 1/2, by norm_num, ?_ ⟩
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ (1 - 1 / 2) • (2 • x - y) + (1 / 2) • y = x

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ (1 - 1 / 2) • (2 • x - y) + (1 / 2) • y = x
Tactic:
rw [(by norm_num : (1:ℝ) - 1 / 2 = 1 / 2), smul_sub, sub_add_cancel, smul_smul,
  div_mul_cancel _ (by linarith), one_smul]
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ 1 / 2 ∈ Set.Ioo 0 1
Tactic:
norm_num
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ 1 - 1 / 2 = 1 / 2
Tactic:
norm_num
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
x y : E
⊢ 2 ≠ 0
Tactic:
linarith
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hball : ∃ ε > 0, Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
⊢ ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
Tactic:
rcases hball with ⟨ ε, hε, hball ⟩
State after:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
ε : ℝ
hε : ε > 0
hball : Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
⊢ ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_

State before:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
ε : ℝ
hε : ε > 0
hball : Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
⊢ ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
Tactic:
refine ⟨ ε, hε, fun v hv Hi_ hHi_ => ?_ ⟩
State after:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
ε : ℝ
hε : ε > 0
hball : Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
v : E
hv : v ∈ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ v ∈ ↑Hi_

State before:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
ε : ℝ
hε : ε > 0
hball : Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
v : E
hv : v ∈ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ v ∈ ↑Hi_
Tactic:
apply interior_subset
State after:
case intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
ε : ℝ
hε : ε > 0
hball : Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
v : E
hv : v ∈ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ v ∈ interior ↑Hi_

State before:
case intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
ε : ℝ
hε : ε > 0
hball : Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
v : E
hv : v ∈ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ v ∈ interior ↑Hi_
Tactic:
exact (Set.mem_sInter.mp <| hball hv) (interior <| SetLike.coe Hi_) ⟨ Hi_, hHi_, rfl ⟩
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
⊢ ∃ ε > 0, Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
Tactic:
unfold Hpolytope at hxH
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
⊢ ∃ ε > 0, Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hxIcinterior : x ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
hIcinteriorOpen : IsOpen (⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x)))
⊢ ∃ ε > 0, Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
Tactic:
rw [Metric.isOpen_iff] at hIcinteriorOpen
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hxIcinterior : x ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
hIcinteriorOpen :
  ∀ x_1 ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x)),
    ∃ ε > 0, Metric.ball x_1 ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
⊢ ∃ ε > 0, Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hxIcinterior : x ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
hIcinteriorOpen :
  ∀ x_1 ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x)),
    ∃ ε > 0, Metric.ball x_1 ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
⊢ ∃ ε > 0, Metric.ball x ε ⊆ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
Tactic:
exact hIcinteriorOpen x hxIcinterior
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
⊢ x ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
Tactic:
rintro HiS ⟨ Hi_, hHi_, rfl ⟩
State after:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ x ∈ (fun x => interior ↑x) Hi_

State before:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ x ∈ (fun x => interior ↑x) Hi_
Tactic:
rw [Set.mem_diff, Hpolytope.I_mem, IsClosed.frontier_eq <| Halfspace_closed Hi_,
  Set.mem_diff] at hHi_
State after:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ ∧ ¬(Hi_ ∈ H_ ∧ x ∈ ↑Hi_ ∧ x ∉ interior ↑Hi_)
⊢ x ∈ (fun x => interior ↑x) Hi_

State before:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ ∧ ¬(Hi_ ∈ H_ ∧ x ∈ ↑Hi_ ∧ x ∉ interior ↑Hi_)
⊢ x ∈ (fun x => interior ↑x) Hi_
Tactic:
push_neg at hHi_
State after:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ ∧ (Hi_ ∈ H_ → x ∈ ↑Hi_ → x ∈ interior ↑Hi_)
⊢ x ∈ (fun x => interior ↑x) Hi_

State before:
case intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_ ∧ (Hi_ ∈ H_ → x ∈ ↑Hi_ → x ∈ interior ↑Hi_)
⊢ x ∈ (fun x => interior ↑x) Hi_
Tactic:
exact hHi_.2 hHi_.1 <| hxH Hi_ ⟨ Hi_, hHi_.1, rfl ⟩
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hxIcinterior : x ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
⊢ IsOpen (⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x)))
Tactic:
apply Set.Finite.isOpen_sInter (Set.Finite.image _ (Set.Finite.diff hH_ _))
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hxIcinterior : x ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
⊢ ∀ t ∈ (fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x), IsOpen t

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ ⋂₀ (SetLike.coe '' H_)
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hxIcinterior : x ∈ ⋂₀ ((fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x))
⊢ ∀ t ∈ (fun x => interior ↑x) '' (H_ \ Hpolytope.I H_ x), IsOpen t
Tactic:
exact fun _ ⟨ Hi_, _, h ⟩ => h ▸ isOpen_interior
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
⊢ ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
Tactic:
rintro v hv Hi_ hHi_
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ v ∈ ↑Hi_

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : y ∈ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x)
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ v ∈ ↑Hi_
Tactic:
rw [Set.mem_sInter] at hy
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : ∀ t ∈ (fun x => frontier ↑x) '' Hpolytope.I H_ x, y ∈ t
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ v ∈ ↑Hi_

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hy : ∀ t ∈ (fun x => frontier ↑x) '' Hpolytope.I H_ x, y ∈ t
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ v ∈ ↑Hi_
Tactic:
specialize hy (frontier <| SetLike.coe Hi_) ⟨ Hi_, hHi_, rfl ⟩
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ frontier ↑Hi_
⊢ v ∈ ↑Hi_

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ frontier ↑Hi_
⊢ v ∈ ↑Hi_
Tactic:
have hHi_2 := hHi_.2
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ frontier ↑Hi_
hHi_2 : x ∈ frontier ↑Hi_
⊢ v ∈ ↑Hi_

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ frontier ↑Hi_
hHi_2 : x ∈ frontier ↑Hi_
⊢ v ∈ ↑Hi_
Tactic:
rw [frontierHalfspace_Hyperplane] at hy hHi_2
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ v ∈ ↑Hi_

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ v ∈ ↑Hi_
Tactic:
apply IsClosed.frontier_subset <| Halfspace_closed Hi_
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ v ∈ frontier ↑Hi_

State before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ v ∈ frontier ↑Hi_
Tactic:
rw [frontierHalfspace_Hyperplane]
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ v ∈ {x | ↑Hi_.f x = Hi_.α}

State before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ v ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
apply Set.mem_of_mem_of_subset hv
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ segment ℝ (2 • x - y) y ⊆ {x | ↑Hi_.f x = Hi_.α}

State before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ segment ℝ (2 • x - y) y ⊆ {x | ↑Hi_.f x = Hi_.α}
Tactic:
apply (convex_iff_segment_subset.mp <| Hyperplane_convex Hi_) _ hy
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
have h21 : Finset.sum Finset.univ ![(2:ℝ), -1] = 1 := by
  rw [Fin.sum_univ_two, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons]
  linarith
  done
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
have h2x_y := Hyperplane_affineClosed Hi_ ![x, y] (by
  rw [Matrix.range_cons, Matrix.range_cons, Matrix.range_empty, Set.union_empty];
  exact Set.union_subset (Set.singleton_subset_iff.mpr hHi_2) (Set.singleton_subset_iff.mpr hy))
  ![2, -1] h21
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
h2x_y : (Finset.affineCombination ℝ Finset.univ ![x, y]) ![2, -1] ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
h2x_y : (Finset.affineCombination ℝ Finset.univ ![x, y]) ![2, -1] ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
rw [Finset.affineCombination_eq_linear_combination _ _ _ h21, Fin.sum_univ_two, Matrix.cons_val_zero,
  Matrix.cons_val_one, Matrix.head_cons, Matrix.cons_val_zero, Matrix.cons_val_one,
  Matrix.head_cons, neg_one_smul, ← sub_eq_add_neg] at h2x_y
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
h2x_y : 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
h2x_y : 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 • x - y ∈ {x | ↑Hi_.f x = Hi_.α}
Tactic:
exact h2x_y
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ Finset.sum Finset.univ ![2, -1] = 1
Tactic:
rw [Fin.sum_univ_two, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.head_cons]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 + -1 = 1

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
⊢ 2 + -1 = 1
Tactic:
linarith
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
⊢ Set.range ![x, y] ⊆ {x | ↑Hi_.f x = Hi_.α}
Tactic:
rw [Matrix.range_cons, Matrix.range_cons, Matrix.range_empty, Set.union_empty]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
⊢ {x} ∪ {y} ⊆ {x | ↑Hi_.f x = Hi_.α}

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
y : E
hyx : y ≠ x
hxyy : x ∈ openSegment ℝ (2 • x - y) y
hmemballmemIc : ∃ ε > 0, ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
v : E
hv : v ∈ segment ℝ (2 • x - y) y
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hy : y ∈ {x | ↑Hi_.f x = Hi_.α}
hHi_2 : x ∈ {x | ↑Hi_.f x = Hi_.α}
h21 : Finset.sum Finset.univ ![2, -1] = 1
⊢ {x} ∪ {y} ⊆ {x | ↑Hi_.f x = Hi_.α}
Tactic:
exact Set.union_subset (Set.singleton_subset_iff.mpr hHi_2) (Set.singleton_subset_iff.mpr hy)
State after:
no goals

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ x1 ∈ ↑Hi_
Tactic:
specialize hsub (left_mem_segment ℝ x1 x2)
State after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
⊢ x1 ∈ ↑Hi_

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
⊢ x1 ∈ ↑Hi_
Tactic:
rcases (em (Hi_ ∈ Hpolytope.I H_ x)) with (hinI | hninI)
State after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x1 ∈ ↑Hi_

case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ x1 ∈ ↑Hi_

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x1 ∈ ↑Hi_
Tactic:
apply hmemsegmemI x1 ?_ Hi_ hinI
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x1 ∈ segment ℝ (2 • x - y) y

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x1 ∈ segment ℝ (2 • x - y) y
Tactic:
apply openSegment_subset_segment
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x1 ∈ openSegment ℝ (2 • x - y) y

State before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x1 ∈ openSegment ℝ (2 • x - y) y
Tactic:
exact Set.mem_of_mem_inter_left hsub
State after:
no goals

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ x1 ∈ ↑Hi_
Tactic:
have : Hi_ ∈ H_ \ Hpolytope.I H_ x := by
  rw [Set.mem_diff]
  exact ⟨ hHi_, hninI ⟩
State after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
this : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ x1 ∈ ↑Hi_

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_1.intro.intro.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
this : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ x1 ∈ ↑Hi_
Tactic:
exact hmemballmemIc x1 (Set.mem_of_mem_inter_right hsub) Hi_ this
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ Hi_ ∈ H_ \ Hpolytope.I H_ x
Tactic:
rw [Set.mem_diff]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ Hi_ ∈ H_ ∧ Hi_ ∉ Hpolytope.I H_ x

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x1 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ Hi_ ∈ H_ ∧ Hi_ ∉ Hpolytope.I H_ x
Tactic:
exact ⟨ hHi_, hninI ⟩
State after:
no goals

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
hsub : segment ℝ x1 x2 ⊆ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
⊢ x2 ∈ ↑Hi_
Tactic:
specialize hsub (right_mem_segment ℝ x1 x2)
State after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
⊢ x2 ∈ ↑Hi_

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
⊢ x2 ∈ ↑Hi_
Tactic:
rcases (em (Hi_ ∈ Hpolytope.I H_ x)) with (hinI | hninI)
State after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x2 ∈ ↑Hi_

case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ x2 ∈ ↑Hi_

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x2 ∈ ↑Hi_
Tactic:
apply hmemsegmemI x2 ?_ Hi_ hinI
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x2 ∈ segment ℝ (2 • x - y) y

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x2 ∈ segment ℝ (2 • x - y) y
Tactic:
apply openSegment_subset_segment
State after:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x2 ∈ openSegment ℝ (2 • x - y) y

State before:
case a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hinI : Hi_ ∈ Hpolytope.I H_ x
⊢ x2 ∈ openSegment ℝ (2 • x - y) y
Tactic:
exact Set.mem_of_mem_inter_left hsub
State after:
no goals

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ x2 ∈ ↑Hi_
Tactic:
have : Hi_ ∈ H_ \ Hpolytope.I H_ x := by
  rw [Set.mem_diff]
  exact ⟨ hHi_, hninI ⟩
State after:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
this : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ x2 ∈ ↑Hi_

State before:
case mp.intro.intro.intro.intro.intro.intro.intro.intro.refine_2.intro.intro.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
this : Hi_ ∈ H_ \ Hpolytope.I H_ x
⊢ x2 ∈ ↑Hi_
Tactic:
exact hmemballmemIc x2 (Set.mem_of_mem_inter_right hsub) Hi_ this
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ Hi_ ∈ H_ \ Hpolytope.I H_ x
Tactic:
rw [Set.mem_diff]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ Hi_ ∈ H_ ∧ Hi_ ∉ Hpolytope.I H_ x

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x y : E
hmemsegmemI : ∀ v ∈ segment ℝ (2 • x - y) y, ∀ Hi_ ∈ Hpolytope.I H_ x, v ∈ ↑Hi_
ε : ℝ
hmemballmemIc : ∀ v ∈ Metric.ball x ε, ∀ Hi_ ∈ H_ \ Hpolytope.I H_ x, v ∈ ↑Hi_
x1 x2 : E
Hi_ : Halfspace E
hHi_ : Hi_ ∈ H_
hsub : x2 ∈ openSegment ℝ (2 • x - y) y ∩ Metric.ball x ε
hninI : Hi_ ∉ Hpolytope.I H_ x
⊢ Hi_ ∈ H_ ∧ Hi_ ∉ Hpolytope.I H_ x
Tactic:
exact ⟨ hHi_, hninI ⟩
State after:
no goals

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
⊢ ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x} → x ∈ Set.extremePoints ℝ (Hpolytope hH_)
Tactic:
intro hinterx
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_)

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
⊢ x ∈ Set.extremePoints ℝ (Hpolytope hH_)
Tactic:
rw [mem_extremePoints]
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
⊢ x ∈ Hpolytope hH_ ∧ ∀ x₁ ∈ Hpolytope hH_, ∀ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
⊢ x ∈ Hpolytope hH_ ∧ ∀ x₁ ∈ Hpolytope hH_, ∀ x₂ ∈ Hpolytope hH_, x ∈ openSegment ℝ x₁ x₂ → x₁ = x ∧ x₂ = x
Tactic:
refine ⟨ hxH, λ x1 hx1 x2 hx2 hx => ?_ ⟩
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
⊢ x1 = x ∧ x2 = x

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
⊢ x1 = x ∧ x2 = x
Tactic:
have : segment ℝ x1 x2 ⊆ {x} → x1 = x ∧ x2 = x := by
  rw [Set.Nonempty.subset_singleton_iff (Set.nonempty_of_mem (left_mem_segment ℝ x1 x2)),
    Set.eq_singleton_iff_unique_mem]
  exact fun hseg => ⟨ hseg.2 x1 (left_mem_segment ℝ x1 x2),
    hseg.2 x2 (right_mem_segment ℝ x1 x2) ⟩
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
this : segment ℝ x1 x2 ⊆ {x} → x1 = x ∧ x2 = x
⊢ x1 = x ∧ x2 = x

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
this : segment ℝ x1 x2 ⊆ {x} → x1 = x ∧ x2 = x
⊢ x1 = x ∧ x2 = x
Tactic:
apply this
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
this : segment ℝ x1 x2 ⊆ {x} → x1 = x ∧ x2 = x
⊢ segment ℝ x1 x2 ⊆ {x}

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
this : segment ℝ x1 x2 ⊆ {x} → x1 = x ∧ x2 = x
⊢ segment ℝ x1 x2 ⊆ {x}
Tactic:
clear this
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
⊢ segment ℝ x1 x2 ⊆ {x}

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
⊢ segment ℝ x1 x2 ⊆ {x}
Tactic:
rw [← hinterx, Set.subset_sInter_iff]
State after:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
⊢ ∀ t' ∈ (fun x => frontier ↑x) '' Hpolytope.I H_ x, segment ℝ x1 x2 ⊆ t'

State before:
case mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
⊢ ∀ t' ∈ (fun x => frontier ↑x) '' Hpolytope.I H_ x, segment ℝ x1 x2 ⊆ t'
Tactic:
rintro HiS ⟨ Hi_, hHi_, rfl ⟩
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ segment ℝ x1 x2 ⊆ (fun x => frontier ↑x) Hi_

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ segment ℝ x1 x2 ⊆ (fun x => frontier ↑x) Hi_
Tactic:
simp only
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
have hfxα : Hi_.f.1 x = Hi_.α := by
  have : x ∈ {x} := by
    exact Set.mem_singleton x
  rw [← hinterx, Set.mem_sInter] at this
  specialize this (frontier <| SetLike.coe Hi_) ⟨ Hi_, hHi_, rfl ⟩
  rw [frontierHalfspace_Hyperplane, Set.mem_setOf] at this
  exact this
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
clear hinterx hxH
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
rw [mem_Hpolytope] at hx1 hx2
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 : E
hx1 : ∀ Hi ∈ H_, ↑Hi.f x1 ≤ Hi.α
x2 : E
hx2 : ∀ Hi ∈ H_, ↑Hi.f x2 ≤ Hi.α
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 : E
hx1 : ∀ Hi ∈ H_, ↑Hi.f x1 ≤ Hi.α
x2 : E
hx2 : ∀ Hi ∈ H_, ↑Hi.f x2 ≤ Hi.α
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
specialize hx1 Hi_ hHi_.1
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 x2 : E
hx2 : ∀ Hi ∈ H_, ↑Hi.f x2 ≤ Hi.α
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 x2 : E
hx2 : ∀ Hi ∈ H_, ↑Hi.f x2 ≤ Hi.α
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
specialize hx2 Hi_ hHi_.1
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
clear hHi_ hH_ H_
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
⊢ segment ℝ x1 x2 ⊆ frontier ↑Hi_
Tactic:
rw [frontierHalfspace_Hyperplane]
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
⊢ segment ℝ x1 x2 ⊆ {x | ↑Hi_.f x = Hi_.α}

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
⊢ segment ℝ x1 x2 ⊆ {x | ↑Hi_.f x = Hi_.α}
Tactic:
have := Hyperplane_convex Hi_
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
this : Convex ℝ {x | ↑Hi_.f x = Hi_.α}
⊢ segment ℝ x1 x2 ⊆ {x | ↑Hi_.f x = Hi_.α}

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
this : Convex ℝ {x | ↑Hi_.f x = Hi_.α}
⊢ segment ℝ x1 x2 ⊆ {x | ↑Hi_.f x = Hi_.α}
Tactic:
rw [convex_iff_segment_subset] at this
State after:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
this :
  ∀ ⦃x : E⦄, x ∈ {x | ↑Hi_.f x = Hi_.α} → ∀ ⦃y : E⦄, y ∈ {x | ↑Hi_.f x = Hi_.α} → segment ℝ x y ⊆ {x | ↑Hi_.f x = Hi_.α}
⊢ segment ℝ x1 x2 ⊆ {x | ↑Hi_.f x = Hi_.α}

State before:
case mpr.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
this :
  ∀ ⦃x : E⦄, x ∈ {x | ↑Hi_.f x = Hi_.α} → ∀ ⦃y : E⦄, y ∈ {x | ↑Hi_.f x = Hi_.α} → segment ℝ x y ⊆ {x | ↑Hi_.f x = Hi_.α}
⊢ segment ℝ x1 x2 ⊆ {x | ↑Hi_.f x = Hi_.α}
Tactic:
apply this <;>
clear this <;>
rw [Set.mem_setOf] <;>
by_contra h <;>
push_neg at h <;>
have hlt := lt_of_le_of_ne (by assumption) h <;>
clear h
State after:
case mpr.intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
⊢ False

case mpr.intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
⊢ False

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
⊢ segment ℝ x1 x2 ⊆ {x} → x1 = x ∧ x2 = x
Tactic:
rw [Set.Nonempty.subset_singleton_iff (Set.nonempty_of_mem (left_mem_segment ℝ x1 x2)),
  Set.eq_singleton_iff_unique_mem]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
⊢ (x ∈ segment ℝ x1 x2 ∧ ∀ x_1 ∈ segment ℝ x1 x2, x_1 = x) → x1 = x ∧ x2 = x

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
⊢ (x ∈ segment ℝ x1 x2 ∧ ∀ x_1 ∈ segment ℝ x1 x2, x_1 = x) → x1 = x ∧ x2 = x
Tactic:
exact fun hseg => ⟨ hseg.2 x1 (left_mem_segment ℝ x1 x2),
  hseg.2 x2 (right_mem_segment ℝ x1 x2) ⟩
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ ↑Hi_.f x = Hi_.α
Tactic:
have : x ∈ {x} := by
  exact Set.mem_singleton x
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : x ∈ {x}
⊢ ↑Hi_.f x = Hi_.α

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : x ∈ {x}
⊢ ↑Hi_.f x = Hi_.α
Tactic:
rw [← hinterx, Set.mem_sInter] at this
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : ∀ t ∈ (fun x => frontier ↑x) '' Hpolytope.I H_ x, x ∈ t
⊢ ↑Hi_.f x = Hi_.α

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : ∀ t ∈ (fun x => frontier ↑x) '' Hpolytope.I H_ x, x ∈ t
⊢ ↑Hi_.f x = Hi_.α
Tactic:
specialize this (frontier <| SetLike.coe Hi_) ⟨ Hi_, hHi_, rfl ⟩
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : x ∈ frontier ↑Hi_
⊢ ↑Hi_.f x = Hi_.α

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : x ∈ frontier ↑Hi_
⊢ ↑Hi_.f x = Hi_.α
Tactic:
rw [frontierHalfspace_Hyperplane, Set.mem_setOf] at this
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : ↑Hi_.f x = Hi_.α
⊢ ↑Hi_.f x = Hi_.α

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
this : ↑Hi_.f x = Hi_.α
⊢ ↑Hi_.f x = Hi_.α
Tactic:
exact this
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
x : E
hxH : x ∈ Hpolytope hH_
hinterx : ⋂₀ ((fun x => frontier ↑x) '' Hpolytope.I H_ x) = {x}
x1 : E
hx1 : x1 ∈ Hpolytope hH_
x2 : E
hx2 : x2 ∈ Hpolytope hH_
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hHi_ : Hi_ ∈ Hpolytope.I H_ x
⊢ x ∈ {x}
Tactic:
exact Set.mem_singleton x
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
h : ↑Hi_.f x2 ≠ Hi_.α
⊢ ↑Hi_.f x2 ≤ Hi_.α
Tactic:
assumption
State after:
no goals

State before:
case mpr.intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
⊢ False
Tactic:
rw [openSegment_eq_image', Set.mem_image] at hx
State after:
case mpr.intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : ∃ x_1 ∈ Set.Ioo 0 1, x1 + x_1 • (x2 - x1) = x
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
⊢ False

State before:
case mpr.intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : ∃ x_1 ∈ Set.Ioo 0 1, x1 + x_1 • (x2 - x1) = x
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
⊢ False
Tactic:
rcases hx with ⟨ t, ht, rfl ⟩
State after:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f (x1 + t • (x2 - x1)) = Hi_.α
⊢ False

State before:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f (x1 + t • (x2 - x1)) = Hi_.α
⊢ False
Tactic:
rw [Hi_.f.1.map_add, Hi_.f.1.map_smul] at hfxα
State after:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
⊢ False

State before:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
⊢ False
Tactic:
have : Hi_.f.1 x1 + t • Hi_.f.1 (x2 - x1) + (1-t) • Hi_.f.1 (x2 - x1) > Hi_.α := by
  rw [hfxα, gt_iff_lt]
  exact lt_add_of_le_of_pos (by linarith) <|
    (smul_pos_iff_of_pos_left (by linarith [ht.2])).mpr <|
    (smul_pos_iff_of_pos_left ht.1).mp <| pos_of_lt_add_right <| hfxα.symm ▸ hlt
State after:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
this : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) + (1 - t) • ↑Hi_.f (x2 - x1) > Hi_.α
⊢ False

State before:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
this : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) + (1 - t) • ↑Hi_.f (x2 - x1) > Hi_.α
⊢ False
Tactic:
rw [add_assoc, ← add_smul, add_sub, add_comm t 1, add_sub_cancel, one_smul, ← Hi_.f.1.map_add, add_comm, sub_add_cancel] at this
State after:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
this : ↑Hi_.f x2 > Hi_.α
⊢ False

State before:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
this : ↑Hi_.f x2 > Hi_.α
⊢ False
Tactic:
linarith
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
⊢ ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) + (1 - t) • ↑Hi_.f (x2 - x1) > Hi_.α
Tactic:
rw [hfxα, gt_iff_lt]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
⊢ Hi_.α < Hi_.α + (1 - t) • ↑Hi_.f (x2 - x1)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
⊢ Hi_.α < Hi_.α + (1 - t) • ↑Hi_.f (x2 - x1)
Tactic:
exact lt_add_of_le_of_pos (by linarith) <|
  (smul_pos_iff_of_pos_left (by linarith [ht.2])).mpr <|
  (smul_pos_iff_of_pos_left ht.1).mp <| pos_of_lt_add_right <| hfxα.symm ▸ hlt
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
⊢ Hi_.α ≤ Hi_.α
Tactic:
linarith
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x1 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x1 + t • ↑Hi_.f (x2 - x1) = Hi_.α
⊢ 0 < 1 - t
Tactic:
linarith [ht.2]
State after:
no goals

State before:
case mpr.intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : x ∈ openSegment ℝ x1 x2
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
⊢ False
Tactic:
rw [openSegment_symm, openSegment_eq_image', Set.mem_image] at hx
State after:
case mpr.intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : ∃ x_1 ∈ Set.Ioo 0 1, x2 + x_1 • (x1 - x2) = x
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
⊢ False

State before:
case mpr.intro.intro.a
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x x1 x2 : E
hx : ∃ x_1 ∈ Set.Ioo 0 1, x2 + x_1 • (x1 - x2) = x
Hi_ : Halfspace E
hfxα : ↑Hi_.f x = Hi_.α
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
⊢ False
Tactic:
rcases hx with ⟨ t, ht, rfl ⟩
State after:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f (x2 + t • (x1 - x2)) = Hi_.α
⊢ False

State before:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f (x2 + t • (x1 - x2)) = Hi_.α
⊢ False
Tactic:
rw [Hi_.f.1.map_add, Hi_.f.1.map_smul] at hfxα
State after:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ False

State before:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ False
Tactic:
have : Hi_.f.1 x2 + t • Hi_.f.1 (x1 - x2) + (1-t) • Hi_.f.1 (x1 - x2) > Hi_.α := by
  rw [hfxα, gt_iff_lt]
  exact lt_add_of_le_of_pos (by linarith) <|
    (smul_pos_iff_of_pos_left (by linarith [ht.2])).mpr <|
    (smul_pos_iff_of_pos_left ht.1).mp <| pos_of_lt_add_right <| hfxα.symm ▸ hlt
State after:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
this : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) + (1 - t) • ↑Hi_.f (x1 - x2) > Hi_.α
⊢ False

State before:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
this : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) + (1 - t) • ↑Hi_.f (x1 - x2) > Hi_.α
⊢ False
Tactic:
rw [add_assoc, ← add_smul, add_sub, add_comm t 1, add_sub_cancel, one_smul,
  ← Hi_.f.1.map_add, add_comm, sub_add_cancel] at this
State after:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
this : ↑Hi_.f x1 > Hi_.α
⊢ False

State before:
case mpr.intro.intro.a.intro.intro
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
this : ↑Hi_.f x1 > Hi_.α
⊢ False
Tactic:
linarith
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) + (1 - t) • ↑Hi_.f (x1 - x2) > Hi_.α
Tactic:
rw [hfxα, gt_iff_lt]
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ Hi_.α < Hi_.α + (1 - t) • ↑Hi_.f (x1 - x2)

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ Hi_.α < Hi_.α + (1 - t) • ↑Hi_.f (x1 - x2)
Tactic:
exact lt_add_of_le_of_pos (by linarith) <|
  (smul_pos_iff_of_pos_left (by linarith [ht.2])).mpr <|
  (smul_pos_iff_of_pos_left ht.1).mp <| pos_of_lt_add_right <| hfxα.symm ▸ hlt
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ Hi_.α ≤ Hi_.α
Tactic:
linarith
State after:
no goals

State before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
x1 x2 : E
Hi_ : Halfspace E
hx1 : ↑Hi_.f x1 ≤ Hi_.α
hx2 : ↑Hi_.f x2 ≤ Hi_.α
hlt : ↑Hi_.f x2 < Hi_.α
t : ℝ
ht : t ∈ Set.Ioo 0 1
hfxα : ↑Hi_.f x2 + t • ↑Hi_.f (x1 - x2) = Hi_.α
⊢ 0 < 1 - t
Tactic:
linarith [ht.2]
State after:
no goals