internlm/Lean-Github huggingface dataset:
Theorem: MainTheoremOfPolytopes
Proof state before:
case left.inl.intro.intro.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_'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_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = Vpolytope hS
Tactic:
refine ⟨ H_', hH_', ?_ ⟩
Proof state after:
case left.inl.intro.intro.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_'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)
⊢ Hpolytope hH_' = Vpolytope hS
Theorem: MainTheoremOfPolytopes
Proof 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 : 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

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:
all_goals (exact IsCompact.ne_univ (Compact_Vpolytope hS'Fin) hHV.symm)
Proof state after:
no goals
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
hSnontrivial : Set.Nontrivial S
this✝ : Nontrivial ↑S
hSnonempty : Set.Nonempty S
this : Nonempty ↑S
s : E
hs : s ∈ S
⊢ s ∈ affineSpan ℝ S
Tactic:
apply subset_affineSpan
Proof 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
⊢ s ∈ S
Theorem: MainTheoremOfPolytopes
Proof 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
⊢ s ∈ S
Tactic:
exact hs
Proof state after:
no goals
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
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.Finite S' ∧ (convexHull ℝ) S' = ⇑(AffineIsometryEquiv.VSubconst ℝ s') '' (Subtype.val ⁻¹' (convexHull ℝ) S)
Tactic:
rw [InDown_eq_DownIn, ← @convexHull_singleton ℝ, Set.vsub_eq_sub, ← convexHull_sub,
  ← Submodule.coeSubtype]
Proof state after:
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.Finite S' ∧
      (convexHull ℝ) S' = ⇑(Submodule.subtype (AffineSubspace.direction SpanS)) ⁻¹' (convexHull ℝ) (S - {↑s'})
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
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.Finite S' ∧
      (convexHull ℝ) S' = ⇑(Submodule.subtype (AffineSubspace.direction SpanS)) ⁻¹' (convexHull ℝ) (S - {↑s'})
Tactic:
refine ⟨ Subtype.val ⁻¹' (S - {s}), ?_, ?_ ⟩
Proof state after:
case refine_1
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))
⊢ Set.Finite (Subtype.val ⁻¹' (S - {s}))

case refine_2
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))
⊢ (convexHull ℝ) (Subtype.val ⁻¹' (S - {s})) =
    ⇑(Submodule.subtype (AffineSubspace.direction SpanS)) ⁻¹' (convexHull ℝ) (S - {↑s'})
Theorem: MainTheoremOfPolytopes
Proof state before:
case refine_1
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))
⊢ Set.Finite (Subtype.val ⁻¹' (S - {s}))
Tactic:
apply Set.Finite.preimage (Set.injOn_of_injective Subtype.val_injective _)
Proof state after:
case refine_1
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))
⊢ Set.Finite (S - {s})
Theorem: MainTheoremOfPolytopes
Proof state before:
case refine_1
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))
⊢ Set.Finite (S - {s})
Tactic:
rw [Set.sub_singleton]
Proof state after:
case refine_1
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))
⊢ Set.Finite ((fun x => x - s) '' S)
Theorem: MainTheoremOfPolytopes
Proof state before:
case refine_1
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))
⊢ Set.Finite ((fun x => x - s) '' S)
Tactic:
exact hS.image _
Proof state after:
no goals
Theorem: MainTheoremOfPolytopes
Proof state before:
case refine_2
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))
⊢ (convexHull ℝ) (Subtype.val ⁻¹' (S - {s})) =
    ⇑(Submodule.subtype (AffineSubspace.direction SpanS)) ⁻¹' (convexHull ℝ) (S - {↑s'})
Tactic:
rw [← Submodule.coeSubtype, ← LinearMap.coe_toAffineMap, ← AffineMap.preimage_convexHull]
Proof state after:
case refine_2.hf
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))
⊢ Function.Injective (LinearMap.toAffineMap (Submodule.subtype (AffineSubspace.direction SpanS))).toFun

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)))
Theorem: MainTheoremOfPolytopes
Proof state before:
case refine_2.hf
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))
⊢ Function.Injective Subtype.val

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
Tactic:
exact Subtype.val_injective
Proof 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
Theorem: MainTheoremOfPolytopes
Proof 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 Subtype.val
Tactic:
rw [Subtype.range_coe_subtype]
Proof 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} ⊆ {x | x ∈ AffineSubspace.direction SpanS}