Theorem: MainTheoremOfPolytopes (src/MainTheorem.lean)

State before:
case refine_2.hs
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 - {s} ⊆ Set.range ⇑(LinearMap.toAffineMap (Submodule.subtype (AffineSubspace.direction SpanS)))
Tactic:
rw [LinearMap.coe_toAffineMap, Submodule.coeSubtype]
State after:
case refine_2.hs
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 - {s} ⊆ Set.range Subtype.val

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
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
⊢ Nontrivial ↥(AffineSubspace.direction SpanS)
Tactic:
apply AffineSubspace.direction_nontrivial_of_nontrivial
State after:
case a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
⊢ Nontrivial ↥SpanS

State before:
case a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
⊢ Nontrivial ↥SpanS
Tactic:
exact affineSpan_nontrivial ℝ (Set.nontrivial_coe_sort.mpr hSnontrivial)
State after:
no goals

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty (SetLike.coe '' H_'1)
Tactic:
(apply Set.Nonempty.image)
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty H_'1

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty (SetLike.coe '' H_'1)
Tactic:
apply Set.Nonempty.image
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty H_'1

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty H_'1
Tactic:
(try (change Set.Nonempty (Halfspace.val (AffineSubspace.direction SpanS) '' H_''1)))
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty (Halfspace.val (AffineSubspace.direction SpanS) '' H_''1)

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty H_'1
Tactic:
try (change Set.Nonempty (Halfspace.val (AffineSubspace.direction SpanS) '' H_''1))
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty (Halfspace.val (AffineSubspace.direction SpanS) '' H_''1)

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty H_'1
Tactic:
(change Set.Nonempty (Halfspace.val (AffineSubspace.direction SpanS) '' H_''1))
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty (Halfspace.val (AffineSubspace.direction SpanS) '' H_''1)

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty H_'1
Tactic:
change Set.Nonempty (Halfspace.val (AffineSubspace.direction SpanS) '' H_''1)
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty (Halfspace.val (AffineSubspace.direction SpanS) '' H_''1)

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty (Halfspace.val (AffineSubspace.direction SpanS) '' H_''1)
Tactic:
(try apply Set.Nonempty.image)
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty H_''1

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty (Halfspace.val (AffineSubspace.direction SpanS) '' H_''1)
Tactic:
try apply Set.Nonempty.image
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty H_''1

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty (Halfspace.val (AffineSubspace.direction SpanS) '' H_''1)
Tactic:
apply Set.Nonempty.image
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty H_''1

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty H_''1
Tactic:
(by_contra h)
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
h : ¬Set.Nonempty H_''1
⊢ False

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
⊢ Set.Nonempty H_''1
Tactic:
by_contra h
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
h : ¬Set.Nonempty H_''1
⊢ False

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
h : ¬Set.Nonempty H_''1
⊢ False
Tactic:
(rw [Set.not_nonempty_iff_eq_empty] at h)
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
h : H_''1 = ∅
⊢ False

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
h : ¬Set.Nonempty H_''1
⊢ False
Tactic:
rw [Set.not_nonempty_iff_eq_empty] at h
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
h : H_''1 = ∅
⊢ False

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
h : H_''1 = ∅
⊢ False
Tactic:
(rw [Hpolytope, h, Set.image_empty, Set.sInter_empty] at hHV)
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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 : Set.univ = Vpolytope hS'Fin
H_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
h : H_''1 = ∅
⊢ False

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
h : H_''1 = ∅
⊢ False
Tactic:
rw [Hpolytope, h, Set.image_empty, Set.sInter_empty] at hHV
State after:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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 : Set.univ = Vpolytope hS'Fin
H_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
h : H_''1 = ∅
⊢ False

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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 : Set.univ = Vpolytope hS'Fin
H_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
h : H_''1 = ∅
⊢ False
Tactic:
(exact IsCompact.ne_univ (Compact_Vpolytope hS'Fin) hHV.symm)
State after:
no goals

State before:
case left.inl.intro.intro.intro.intro.intro.intro.intro.intro.hs.a.a
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 : Set.univ = Vpolytope hS'Fin
H_'1 : Set (Halfspace E) := Halfspace.val (AffineSubspace.direction SpanS) '' H_''1
hH_'1 : Set.Finite H_'1
H_'2 : Set (Halfspace E)
hH_'2 : Set.Finite H_'2
hH_'2Span : Hpolytope hH_'2 = ↑(AffineSubspace.direction SpanS)
H_' : Set (Halfspace E) := Halfspace_translation s '' (H_'1 ∪ H_'2)
hH_' : Set.Finite H_'
hH_'12 : Hpolytope ⋯ = Hpolytope hH_'1 ∩ Hpolytope hH_'2
this : Nontrivial ↥(AffineSubspace.direction SpanS)
h : H_''1 = ∅
⊢ False
Tactic:
exact IsCompact.ne_univ (Compact_Vpolytope hS'Fin) hHV.symm
State after:
no goals

State before:
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
Tactic:
rw [Set.not_nontrivial_iff] at hStrivial
State after:
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.Subsingleton S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS

State before:
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.Subsingleton S
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
exact Hpolytope_of_Vpolytope_subsingleton _ hStrivial
State after:
no goals

State before:
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
Tactic:
exact Vpolytope_of_Hpolytope
State after:
no goals