Theorem: Hpolytope_of_Vpolytope_subsingleton (src/MainTheorem.lean)

State before:
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
cases' hStrivial.eq_empty_or_singleton with hSempty hSsingleton
State after:
case inl
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
hSempty : S = ∅
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

case inr
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
hSsingleton : ∃ x, S = {x}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

State before:
case inl
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
hSempty : S = ∅
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rw [Vpolytope, hSempty, convexHull_empty]
State after:
case inl
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
hSempty : S = ∅
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅

State before:
case inl
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
hSempty : S = ∅
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = ∅
Tactic:
exact empty_Hpolytope
State after:
no goals

State before:
case inr
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
hSsingleton : ∃ x, S = {x}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases hSsingleton with ⟨ x, hx ⟩
State after:
case inr.intro
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
x : E
hx : S = {x}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

State before:
case inr.intro
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
x : E
hx : S = {x}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases @origin_Hpolytope E _ _ _ _ with ⟨ H_, hH_Fin, hH_ ⟩
State after:
case inr.intro.intro.intro
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
x : E
hx : S = {x}
H_ : Set (Halfspace E)
hH_Fin : Set.Finite H_
hH_ : Hpolytope hH_Fin = {0}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

State before:
case inr.intro.intro.intro
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
x : E
hx : S = {x}
H_ : Set (Halfspace E)
hH_Fin : Set.Finite H_
hH_ : Hpolytope hH_Fin = {0}
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
refine ⟨ Halfspace_translation x '' H_, hH_Fin.image (Halfspace_translation x), ?_ ⟩
State after:
case inr.intro.intro.intro
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
x : E
hx : S = {x}
H_ : Set (Halfspace E)
hH_Fin : Set.Finite H_
hH_ : Hpolytope hH_Fin = {0}
⊢ Hpolytope ⋯ = Vpolytope hS

State before:
case inr.intro.intro.intro
E : Type
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : Set.Subsingleton S
x : E
hx : S = {x}
H_ : Set (Halfspace E)
hH_Fin : Set.Finite H_
hH_ : Hpolytope hH_Fin = {0}
⊢ Hpolytope ⋯ = Vpolytope hS
Tactic:
rw [Vpolytope, hx, convexHull_singleton, Hpolytope_translation hH_Fin, hH_, Set.singleton_add_singleton, zero_add]
State after:
no goals