Theorem: DualOfVpolytope_compactHpolytope (src/MainTheorem.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS) ∧ IsCompact (Hpolytope hH_)
Tactic:
suffices hHeqVdual : ∃ (H_ : Set (Halfspace E)) (hH_ : H_.Finite),
  Hpolytope hH_ = polarDual (Vpolytope hS) from by
  rcases hHeqVdual with ⟨H_, hH_, hHeqVdual⟩
  refine ⟨ H_, hH_, hHeqVdual, ?_ ⟩
  exact hHeqVdual ▸ (polarDual_compact_if (Closed_Vpolytope hS) (Convex_Vpolytope hS) hS0)
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS)
Tactic:
use pointDual '' (Subtype.val ⁻¹' (S \ {0}))
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ ∃ (hH_ : Set.Finite (pointDual '' (Subtype.val ⁻¹' (S \ {0})))), Hpolytope hH_ = polarDual (Vpolytope hS)

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ ∃ (hH_ : Set.Finite (pointDual '' (Subtype.val ⁻¹' (S \ {0})))), Hpolytope hH_ = polarDual (Vpolytope hS)
Tactic:
use (by
  apply Set.Finite.image
  apply Set.Finite.preimage _ _
  apply Set.injOn_of_injective
  exact Subtype.val_injective
  exact Set.Finite.diff hS {0}
  done)
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Hpolytope ⋯ = polarDual (Vpolytope hS)

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Hpolytope ⋯ = polarDual (Vpolytope hS)
Tactic:
apply subset_antisymm
State after:
case h.a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Hpolytope ⋯ ⊆ polarDual (Vpolytope hS)

case h.a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ polarDual (Vpolytope hS) ⊆ Hpolytope ⋯

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
hHeqVdual : ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS) ∧ IsCompact (Hpolytope hH_)
Tactic:
rcases hHeqVdual with ⟨H_, hH_, hHeqVdual⟩
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHeqVdual : Hpolytope hH_ = polarDual (Vpolytope hS)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS) ∧ IsCompact (Hpolytope hH_)

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHeqVdual : Hpolytope hH_ = polarDual (Vpolytope hS)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = polarDual (Vpolytope hS) ∧ IsCompact (Hpolytope hH_)
Tactic:
refine ⟨ H_, hH_, hHeqVdual, ?_ ⟩
State after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHeqVdual : Hpolytope hH_ = polarDual (Vpolytope hS)
⊢ IsCompact (Hpolytope hH_)

State before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
H_ : Set (Halfspace E)
hH_ : Set.Finite H_
hHeqVdual : Hpolytope hH_ = polarDual (Vpolytope hS)
⊢ IsCompact (Hpolytope hH_)
Tactic:
exact hHeqVdual ▸ (polarDual_compact_if (Closed_Vpolytope hS) (Convex_Vpolytope hS) hS0)
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Set.Finite (pointDual '' (Subtype.val ⁻¹' (S \ {0})))
Tactic:
apply Set.Finite.image
State after:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Set.Finite (Subtype.val ⁻¹' (S \ {0}))

State before:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Set.Finite (Subtype.val ⁻¹' (S \ {0}))
Tactic:
apply Set.Finite.preimage _ _
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Set.InjOn Subtype.val (Subtype.val ⁻¹' (S \ {0}))

E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Set.Finite (S \ {0})

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Set.InjOn Subtype.val (Subtype.val ⁻¹' (S \ {0}))

E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Set.Finite (S \ {0})
Tactic:
apply Set.injOn_of_injective
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Function.Injective Subtype.val

E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Set.Finite (S \ {0})

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Function.Injective Subtype.val

E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Set.Finite (S \ {0})
Tactic:
exact Subtype.val_injective
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Set.Finite (S \ {0})

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Set.Finite (S \ {0})
Tactic:
exact Set.Finite.diff hS {0}
State after:
no goals

State before:
case h.a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Hpolytope ⋯ ⊆ polarDual (Vpolytope hS)
Tactic:
intro x hx
State after:
case h.a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ Hpolytope ⋯
⊢ x ∈ polarDual (Vpolytope hS)

State before:
case h.a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ Hpolytope ⋯
⊢ x ∈ polarDual (Vpolytope hS)
Tactic:
cases' (em (x = 0)) with h h
State after:
case h.a.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ Hpolytope ⋯
h : x = 0
⊢ x ∈ polarDual (Vpolytope hS)

case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ Hpolytope ⋯
h : ¬x = 0
⊢ x ∈ polarDual (Vpolytope hS)

State before:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ Hpolytope ⋯
h : ¬x = 0
⊢ x ∈ polarDual (Vpolytope hS)
Tactic:
rw [mem_Hpolytope] at hx
State after:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
⊢ x ∈ polarDual (Vpolytope hS)

State before:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
⊢ x ∈ polarDual (Vpolytope hS)
Tactic:
rw [mem_polarDual]
State after:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
⊢ ∀ x_1 ∈ Vpolytope hS, ⟪x_1, x⟫_ℝ ≤ 1

State before:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
⊢ ∀ x_1 ∈ Vpolytope hS, ⟪x_1, x⟫_ℝ ≤ 1
Tactic:
intro p hp
State after:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
⊢ ⟪p, x⟫_ℝ ≤ 1

State before:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
⊢ ⟪p, x⟫_ℝ ≤ 1
Tactic:
let x' := (⟨ x, h ⟩ : { p : E // p ≠ 0 })
State after:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h }
⊢ ⟪p, x⟫_ℝ ≤ 1

State before:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h }
⊢ ⟪p, x⟫_ℝ ≤ 1
Tactic:
have hx' : ↑x' = x := rfl
State after:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h }
hx' : ↑x' = x
⊢ ⟪p, x⟫_ℝ ≤ 1

State before:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h }
hx' : ↑x' = x
⊢ ⟪p, x⟫_ℝ ≤ 1
Tactic:
rw [← hx', real_inner_comm, ←mem_pointDual]
State after:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h }
hx' : ↑x' = x
⊢ p ∈ ↑(pointDual x')

State before:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h }
hx' : ↑x' = x
⊢ p ∈ ↑(pointDual x')
Tactic:
suffices h : S ⊆ SetLike.coe (pointDual x') from by
  apply convexHull_min h <| Halfspace_convex (pointDual x')
  exact hp
State after:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h }
hx' : ↑x' = x
⊢ S ⊆ ↑(pointDual x')

State before:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h }
hx' : ↑x' = x
⊢ S ⊆ ↑(pointDual x')
Tactic:
intro s hs
State after:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h }
hx' : ↑x' = x
s : E
hs : s ∈ S
⊢ s ∈ ↑(pointDual x')

State before:
case h.a.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h }
hx' : ↑x' = x
s : E
hs : s ∈ S
⊢ s ∈ ↑(pointDual x')
Tactic:
cases' (em (s = 0)) with h h
State after:
case h.a.inr.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : s = 0
⊢ s ∈ ↑(pointDual x')

case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
⊢ s ∈ ↑(pointDual x')

State before:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
⊢ s ∈ ↑(pointDual x')
Tactic:
specialize hx (pointDual ⟨ s, h ⟩) (Set.mem_image_of_mem _ ?_)
State after:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
⊢ { val := s, property := h } ∈ Subtype.val ⁻¹' (S \ {0})

case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
hx : ↑(pointDual { val := s, property := h }).f x ≤ (pointDual { val := s, property := h }).α
⊢ s ∈ ↑(pointDual x')

State before:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
hx : ↑(pointDual { val := s, property := h }).f x ≤ (pointDual { val := s, property := h }).α
⊢ s ∈ ↑(pointDual x')
Tactic:
rw [← Halfspace_mem, mem_pointDual, Subtype.coe_mk] at hx
State after:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
hx : ⟪s, x⟫_ℝ ≤ 1
⊢ s ∈ ↑(pointDual x')

State before:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
hx : ⟪s, x⟫_ℝ ≤ 1
⊢ s ∈ ↑(pointDual x')
Tactic:
rw [mem_pointDual, Subtype.coe_mk, real_inner_comm]
State after:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
hx : ⟪s, x⟫_ℝ ≤ 1
⊢ ⟪s, x⟫_ℝ ≤ 1

State before:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
hx : ⟪s, x⟫_ℝ ≤ 1
⊢ ⟪s, x⟫_ℝ ≤ 1
Tactic:
exact hx
State after:
no goals

State before:
case h.a.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ Hpolytope ⋯
h : x = 0
⊢ x ∈ polarDual (Vpolytope hS)
Tactic:
rw [h]
State after:
case h.a.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ Hpolytope ⋯
h : x = 0
⊢ 0 ∈ polarDual (Vpolytope hS)

State before:
case h.a.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ Hpolytope ⋯
h : x = 0
⊢ 0 ∈ polarDual (Vpolytope hS)
Tactic:
exact polarDual_origin (Vpolytope hS)
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
h : S ⊆ ↑(pointDual x')
⊢ p ∈ ↑(pointDual x')
Tactic:
apply convexHull_min h <| Halfspace_convex (pointDual x')
State after:
case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
h : S ⊆ ↑(pointDual x')
⊢ p ∈ (convexHull ℝ) S

State before:
case a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
h : S ⊆ ↑(pointDual x')
⊢ p ∈ (convexHull ℝ) S
Tactic:
exact hp
State after:
no goals

State before:
case h.a.inr.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : s = 0
⊢ s ∈ ↑(pointDual x')
Tactic:
exact h ▸ pointDual_origin x'
State after:
no goals

State before:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
⊢ { val := s, property := h } ∈ Subtype.val ⁻¹' (S \ {0})
Tactic:
rw [Set.mem_preimage, Subtype.coe_mk, Set.mem_diff]
State after:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
⊢ s ∈ S ∧ s ∉ {0}

State before:
case h.a.inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : ∀ Hi ∈ pointDual '' (Subtype.val ⁻¹' (S \ {0})), ↑Hi.f x ≤ Hi.α
h✝ : ¬x = 0
p : E
hp : p ∈ Vpolytope hS
x' : { p // p ≠ 0 } := { val := x, property := h✝ }
hx' : ↑x' = x
s : E
hs : s ∈ S
h : ¬s = 0
⊢ s ∈ S ∧ s ∉ {0}
Tactic:
exact ⟨ hs, h ⟩
State after:
no goals

State before:
case h.a
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ polarDual (Vpolytope hS) ⊆ Hpolytope ⋯
Tactic:
apply Set.sInter_subset_sInter
State after:
case h.a.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' (S \ {0}))) ⊆
    SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' Vpolytope hS))

State before:
case h.a.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' (S \ {0}))) ⊆
    SetLike.coe '' (pointDual '' (Subtype.val ⁻¹' Vpolytope hS))
Tactic:
apply Set.image_subset
State after:
case h.a.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ pointDual '' (Subtype.val ⁻¹' (S \ {0})) ⊆ pointDual '' (Subtype.val ⁻¹' Vpolytope hS)

State before:
case h.a.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ pointDual '' (Subtype.val ⁻¹' (S \ {0})) ⊆ pointDual '' (Subtype.val ⁻¹' Vpolytope hS)
Tactic:
apply Set.image_subset
State after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Subtype.val ⁻¹' (S \ {0}) ⊆ Subtype.val ⁻¹' Vpolytope hS

State before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ Subtype.val ⁻¹' (S \ {0}) ⊆ Subtype.val ⁻¹' Vpolytope hS
Tactic:
rw [Set.preimage_subset_preimage_iff]
State after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ Vpolytope hS

case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ Set.range Subtype.val

State before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ Vpolytope hS

case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ Set.range Subtype.val
Tactic:
apply subset_trans (by simp)  <| subset_convexHull _ _
State after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ Set.range Subtype.val

State before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ Set.range Subtype.val
Tactic:
rw [Subtype.range_coe_subtype]
State after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ {x | x ≠ 0}

State before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ {x | x ≠ 0}
Tactic:
intro x hx
State after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ S \ {0}
⊢ x ∈ {x | x ≠ 0}

State before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ S \ {0}
⊢ x ∈ {x | x ≠ 0}
Tactic:
rw [Set.mem_diff, Set.mem_singleton_iff] at hx
State after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ S ∧ ¬x = 0
⊢ x ∈ {x | x ≠ 0}

State before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ S ∧ ¬x = 0
⊢ x ∈ {x | x ≠ 0}
Tactic:
rw [Set.mem_setOf]
State after:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ S ∧ ¬x = 0
⊢ x ≠ 0

State before:
case h.a.h.h.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
x : E
hx : x ∈ S ∧ ¬x = 0
⊢ x ≠ 0
Tactic:
exact hx.2
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
S : Set E
hS : Set.Finite S
hS0 : 0 ∈ interior (Vpolytope hS)
⊢ S \ {0} ⊆ S
Tactic:
simp
State after:
no goals