internlm/Lean-Github huggingface dataset:
Theorem: MainTheoremOfPolytopes
Proof state before:
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
⊢ (∀ (S : Set E) (hS : Set.Finite S), ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS) ∧
    ∀ {H_ : Set (Halfspace E)} (hH_ : Set.Finite H_),
      IsCompact (Hpolytope hH_) → ∃ S, ∃ (hS : Set.Finite S), Hpolytope hH_ = Vpolytope hS
Tactic:
constructor
Proof state after:
case left
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
⊢ ∀ (S : Set E) (hS : Set.Finite S), ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

case right
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
⊢ ∀ {H_ : Set (Halfspace E)} (hH_ : Set.Finite H_),
    IsCompact (Hpolytope hH_) → ∃ S, ∃ (hS : Set.Finite S), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
⊢ ∀ (S : Set E) (hS : Set.Finite S), ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
intro S hS
Proof state after:
case left
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
cases' em (S.Nontrivial) with hSnontrivial hStrivial
Proof state after:
case left.inl
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

case left.inr
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hStrivial : ¬Set.Nontrivial S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
have := Set.nontrivial_coe_sort.mpr hSnontrivial
Proof state after:
case left.inl
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this : Nontrivial ↑S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this : Nontrivial ↑S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
have hSnonempty := hSnontrivial.nonempty
Proof state after:
case left.inl
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this : Nontrivial ↑S
hSnonempty : Set.Nonempty S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this : Nontrivial ↑S
hSnonempty : Set.Nonempty S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
have := Set.nonempty_coe_sort.mpr hSnonempty
Proof state after:
case left.inl
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases hSnontrivial.nonempty with ⟨ s, hs ⟩
Proof state after:
case left.inl.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
have hsaff : s ∈ affineSpan ℝ S := by apply subset_affineSpan; exact hs
Proof state after:
case left.inl.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
let SpanS := affineSpan ℝ S
Proof state after:
case left.inl.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
let s' : SpanS := ⟨ s, hsaff ⟩
Proof state after:
case left.inl.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
s' : ↥SpanS := { val := s, property := hsaff }
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
s' : ↥SpanS := { val := s, property := hsaff }
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases (Nonempty_iff_Nonempty_interior_in_direction hs this) with ⟨ x, hx ⟩
Proof state after:
case left.inl.intro.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
s' : ↥SpanS := { val := s, property := hsaff }
x : ↥(AffineSubspace.direction (affineSpan ℝ S))
hx : x ∈ interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S))
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl.intro.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝¹ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this✝ : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
s' : ↥SpanS := { val := s, property := hsaff }
x : ↥(AffineSubspace.direction (affineSpan ℝ S))
hx : x ∈ interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S))
this :
  ∃ S', Set.Finite S' ∧ (convexHull ℝ) S' = ⇑(AffineIsometryEquiv.VSubconst ℝ s') '' (Subtype.val ⁻¹' (convexHull ℝ) S)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases this with ⟨ S', hS'Fin, hS'eq ⟩
Proof state after:
case left.inl.intro.intro.intro.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
s' : ↥SpanS := { val := s, property := hsaff }
x : ↥(AffineSubspace.direction (affineSpan ℝ S))
hx : x ∈ interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S))
S' : Set ↥(AffineSubspace.direction SpanS)
hS'Fin : Set.Finite S'
hS'eq : (convexHull ℝ) S' = ⇑(AffineIsometryEquiv.VSubconst ℝ s') '' (Subtype.val ⁻¹' (convexHull ℝ) S)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl.intro.intro.intro.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
s' : ↥SpanS := { val := s, property := hsaff }
x : ↥(AffineSubspace.direction (affineSpan ℝ S))
hx : x ∈ interior (⇑(AffineIsometryEquiv.VSubconst ℝ { val := s, property := ⋯ }) '' (Subtype.val ⁻¹' (convexHull ℝ) S))
S' : Set ↥(AffineSubspace.direction SpanS)
hS'Fin : Set.Finite S'
hS'eq : (convexHull ℝ) S' = ⇑(AffineIsometryEquiv.VSubconst ℝ s') '' (Subtype.val ⁻¹' (convexHull ℝ) S)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rw [← hS'eq] at hx
Proof state after:
case left.inl.intro.intro.intro.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
s' : ↥SpanS := { val := s, property := hsaff }
x : ↥(AffineSubspace.direction (affineSpan ℝ S))
S' : Set ↥(AffineSubspace.direction SpanS)
hx : x ∈ interior ((convexHull ℝ) S')
hS'Fin : Set.Finite S'
hS'eq : (convexHull ℝ) S' = ⇑(AffineIsometryEquiv.VSubconst ℝ s') '' (Subtype.val ⁻¹' (convexHull ℝ) S)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl.intro.intro.intro.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
s' : ↥SpanS := { val := s, property := hsaff }
x : ↥(AffineSubspace.direction (affineSpan ℝ S))
S' : Set ↥(AffineSubspace.direction SpanS)
hx : x ∈ interior ((convexHull ℝ) S')
hS'Fin : Set.Finite S'
hS'eq : (convexHull ℝ) S' = ⇑(AffineIsometryEquiv.VSubconst ℝ s') '' (Subtype.val ⁻¹' (convexHull ℝ) S)
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
have hS' : (interior (Vpolytope hS'Fin)).Nonempty := Set.nonempty_of_mem hx
Proof state after:
case left.inl.intro.intro.intro.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
s' : ↥SpanS := { val := s, property := hsaff }
x : ↥(AffineSubspace.direction (affineSpan ℝ S))
S' : Set ↥(AffineSubspace.direction SpanS)
hx : x ∈ interior ((convexHull ℝ) S')
hS'Fin : Set.Finite S'
hS'eq : (convexHull ℝ) S' = ⇑(AffineIsometryEquiv.VSubconst ℝ s') '' (Subtype.val ⁻¹' (convexHull ℝ) S)
hS' : Set.Nonempty (interior (Vpolytope hS'Fin))
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl.intro.intro.intro.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
s' : ↥SpanS := { val := s, property := hsaff }
x : ↥(AffineSubspace.direction (affineSpan ℝ S))
S' : Set ↥(AffineSubspace.direction SpanS)
hx : x ∈ interior ((convexHull ℝ) S')
hS'Fin : Set.Finite S'
hS'eq : (convexHull ℝ) S' = ⇑(AffineIsometryEquiv.VSubconst ℝ s') '' (Subtype.val ⁻¹' (convexHull ℝ) S)
hS' : Set.Nonempty (interior (Vpolytope hS'Fin))
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
rcases @Hpolytope_of_Vpolytope_interior SpanS.direction _ _ _ _ _ hS'Fin hS' with ⟨ H_''1, hH''1, hHV ⟩
Proof state after:
case left.inl.intro.intro.intro.intro.intro.intro
E✝ : Type
inst✝¹⁰ : NormedAddCommGroup E✝
inst✝⁹ : InnerProductSpace ℝ E✝
inst✝⁸ : CompleteSpace E✝
E P : Type
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : CompleteSpace E
inst✝⁴ : PseudoMetricSpace P
inst✝³ : NormedAddTorsor E P
inst✝² inst✝¹ : FiniteDimensional ℝ E
inst✝ : Nontrivial E
S : Set E
hS : Set.Finite S
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
hsaff : s ∈ affineSpan ℝ S
SpanS : AffineSubspace ℝ E := affineSpan ℝ S
s' : ↥SpanS := { val := s, property := hsaff }
x : ↥(AffineSubspace.direction (affineSpan ℝ S))
S' : Set ↥(AffineSubspace.direction SpanS)
hx : x ∈ interior ((convexHull ℝ) S')
hS'Fin : Set.Finite S'
hS'eq : (convexHull ℝ) S' = ⇑(AffineIsometryEquiv.VSubconst ℝ s') '' (Subtype.val ⁻¹' (convexHull ℝ) S)
hS' : Set.Nonempty (interior (Vpolytope hS'Fin))
H_''1 : Set (Halfspace ↥(AffineSubspace.direction SpanS))
hH''1 : Set.Finite H_''1
hHV : Hpolytope hH''1 = Vpolytope hS'Fin
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS