internlm/Lean-Github huggingface dataset:
Theorem: empty_Hpolytope
Proof state before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
h2 : 1 ≤ ↑f x
⊢ False
Tactic:
change f.1 x ≤ -1 at h1
Proof state after:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h2 : 1 ≤ ↑f x
h1 : ↑f x ≤ -1
⊢ False
Theorem: empty_Hpolytope
Proof state before:
case intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h2 : 1 ≤ ↑f x
h1 : ↑f x ≤ -1
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: empty_Hpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
⊢ ‖fval‖ = 1
Tactic:
change norm (innerSL ℝ ((norm x)⁻¹ • x)) = 1
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Theorem: empty_Hpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Tactic:
have := @norm_smul_inv_norm ℝ _ E _ _ x hx
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
this : ‖(↑‖x‖)⁻¹ • x‖ = 1
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Theorem: empty_Hpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
this : ‖(↑‖x‖)⁻¹ • x‖ = 1
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Tactic:
rw [IsROrC.ofReal_real_eq_id, id_eq] at this
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
this : ‖‖x‖⁻¹ • x‖ = 1
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Theorem: empty_Hpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
this : ‖‖x‖⁻¹ • x‖ = 1
⊢ ‖(innerSL ℝ) (‖x‖⁻¹ • x)‖ = 1
Tactic:
rw [innerSL_apply_norm, this]
Proof state after:
no goals
Theorem: empty_Hpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x : E
hx : x ≠ 0
xhat : E := ‖x‖⁻¹ • x
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
⊢ Set.Finite {{ f := f, α := -1 }, { f := -f, α := -1 }}
Tactic:
simp only [Set.mem_singleton_iff, Halfspace.mk.injEq, Set.finite_singleton, Set.Finite.insert]
Proof state after:
no goals
Theorem: empty_Hpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
⊢ { f := f, α := -1 } ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}
Tactic:
simp
Proof state after:
no goals
Theorem: empty_Hpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : Nontrivial E
x✝ : E
hx : x✝ ≠ 0
xhat : E := ‖x✝‖⁻¹ • x✝
fval : NormedSpace.Dual ℝ E := (InnerProductSpace.toDualMap ℝ E) xhat
f : { f // ‖f‖ = 1 } := { val := fval, property := ⋯ }
x : E
h : ∀ Hi ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := -1 }.f x ≤ { f := f, α := -1 }.α
⊢ { f := -f, α := -1 } ∈ {{ f := f, α := -1 }, { f := -f, α := -1 }}
Tactic:
simp
Proof state after:
no goals
Theorem: origin_Hpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = {0}
Tactic:
refine ⟨ ⋃₀ (orthoHyperplane '' (Subtype.val ⁻¹' Set.range (FiniteDimensional.finBasis ℝ E))), ?_, ?_ ⟩
Proof state after:
case refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (⋃₀ (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E))))

case refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Hpolytope ?refine_1 = {0}
Theorem: origin_Hpolytope
Proof state before:
case refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (⋃₀ (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E))))
Tactic:
apply Set.Finite.sUnion ?_ (fun t ht => by
  rcases ht with ⟨ x, _, rfl ⟩
  exact orthoHyperplane.Finite _)
Proof state after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)))
Theorem: origin_Hpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)))
Tactic:
apply Set.Finite.image
Proof state after:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E))
Theorem: origin_Hpolytope
Proof state before:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E))
Tactic:
apply Set.Finite.preimage (Set.injOn_of_injective Subtype.val_injective _)
Proof state after:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (Set.range ⇑(FiniteDimensional.finBasis ℝ E))
Theorem: origin_Hpolytope
Proof state before:
case hs
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Set.Finite (Set.range ⇑(FiniteDimensional.finBasis ℝ E))
Tactic:
exact Set.finite_range _
Proof state after:
no goals
Theorem: origin_Hpolytope
Proof state before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
t : Set (Halfspace E)
ht : t ∈ orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E))
⊢ Set.Finite t
Tactic:
rcases ht with ⟨ x, _, rfl ⟩
Proof state after:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : { x // x ≠ 0 }
left✝ : x ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)
⊢ Set.Finite (orthoHyperplane x)
Theorem: origin_Hpolytope
Proof state before:
case intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : { x // x ≠ 0 }
left✝ : x ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)
⊢ Set.Finite (orthoHyperplane x)
Tactic:
exact orthoHyperplane.Finite _
Proof state after:
no goals
Theorem: origin_Hpolytope
Proof state before:
case refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
⊢ Hpolytope ⋯ = {0}
Tactic:
ext x
Proof state after:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x ∈ {0}
Theorem: origin_Hpolytope
Proof state before:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x ∈ {0}
Tactic:
rw [Set.mem_singleton_iff]
Proof state after:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x = 0
Theorem: origin_Hpolytope
Proof state before:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x = 0
Tactic:
change x ∈ cutSpace ( (⋃₀ (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ↑(FiniteDimensional.finBasis ℝ E))))) ↔ x = 0
Proof state after:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x ∈ cutSpace (⋃₀ (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)))) ↔ x = 0
Theorem: origin_Hpolytope
Proof state before:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x ∈ cutSpace (⋃₀ (orthoHyperplane '' (Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)))) ↔ x = 0
Tactic:
rw [orthoHyperplanes_mem]
Proof state after:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0) ↔ x = 0
Theorem: origin_Hpolytope
Proof state before:
case refine_2.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0) ↔ x = 0
Tactic:
constructor
Proof state after:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0) → x = 0

case refine_2.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x = 0 → ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
Theorem: origin_Hpolytope
Proof state before:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ (∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0) → x = 0
Tactic:
intro h
Proof state after:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
⊢ x = 0
Theorem: origin_Hpolytope
Proof state before:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
⊢ x = 0
Tactic:
apply InnerProductSpace.ext_inner_left_basis (FiniteDimensional.finBasis ℝ E)
Proof state after:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
⊢ ∀ (i : Fin (FiniteDimensional.finrank ℝ E)),
    ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = ⟪(FiniteDimensional.finBasis ℝ E) i, 0⟫_ℝ
Theorem: origin_Hpolytope
Proof state before:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
⊢ ∀ (i : Fin (FiniteDimensional.finrank ℝ E)),
    ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = ⟪(FiniteDimensional.finBasis ℝ E) i, 0⟫_ℝ
Tactic:
intro i
Proof state after:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
i : Fin (FiniteDimensional.finrank ℝ E)
⊢ ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = ⟪(FiniteDimensional.finBasis ℝ E) i, 0⟫_ℝ
Theorem: origin_Hpolytope
Proof state before:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
i : Fin (FiniteDimensional.finrank ℝ E)
⊢ ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = ⟪(FiniteDimensional.finBasis ℝ E) i, 0⟫_ℝ
Tactic:
rw [inner_zero_right]
Proof state after:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
i : Fin (FiniteDimensional.finrank ℝ E)
⊢ ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = 0
Theorem: origin_Hpolytope
Proof state before:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
h : ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
i : Fin (FiniteDimensional.finrank ℝ E)
⊢ ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = 0
Tactic:
simp only [Set.mem_preimage, Set.mem_range, forall_exists_index, Subtype.forall] at h
Proof state after:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
i : Fin (FiniteDimensional.finrank ℝ E)
h :
  ∀ (a : E),
    a ≠ 0 → ∀ (x_1 : Fin (FiniteDimensional.finrank ℝ E)), (FiniteDimensional.finBasis ℝ E) x_1 = a → ⟪a, x⟫_ℝ = 0
⊢ ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = 0
Theorem: origin_Hpolytope
Proof state before:
case refine_2.h.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
i : Fin (FiniteDimensional.finrank ℝ E)
h :
  ∀ (a : E),
    a ≠ 0 → ∀ (x_1 : Fin (FiniteDimensional.finrank ℝ E)), (FiniteDimensional.finBasis ℝ E) x_1 = a → ⟪a, x⟫_ℝ = 0
⊢ ⟪(FiniteDimensional.finBasis ℝ E) i, x⟫_ℝ = 0
Tactic:
exact h (FiniteDimensional.finBasis ℝ E i) (Basis.ne_zero (FiniteDimensional.finBasis ℝ E) i) i rfl
Proof state after:
no goals
Theorem: origin_Hpolytope
Proof state before:
case refine_2.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : E
⊢ x = 0 → ∀ x_1 ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E), ⟪↑x_1, x⟫_ℝ = 0
Tactic:
rintro rfl x _
Proof state after:
case refine_2.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : { x // x ≠ 0 }
a✝ : x ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)
⊢ ⟪↑x, 0⟫_ℝ = 0
Theorem: origin_Hpolytope
Proof state before:
case refine_2.h.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
x : { x // x ≠ 0 }
a✝ : x ∈ Subtype.val ⁻¹' Set.range ⇑(FiniteDimensional.finBasis ℝ E)
⊢ ⟪↑x, 0⟫_ℝ = 0
Tactic:
rw [inner_zero_right]
Proof state after:
no goals
Theorem: hyperplane_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
⊢ ∀ (f : { f // ‖f‖ = 1 }) (c : ℝ), ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = {x | ↑f x = c}
Tactic:
intro f c
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = {x | ↑f x = c}
Theorem: hyperplane_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
⊢ ∃ H_, ∃ (hH_ : Set.Finite H_), Hpolytope hH_ = {x | ↑f x = c}
Tactic:
refine ⟨ {Halfspace.mk f c, Halfspace.mk (-f) (-c)},
  (by simp only [Set.mem_singleton_iff, Halfspace.mk.injEq, Set.finite_singleton, Set.Finite.insert]) , ?_ ⟩
Proof state after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
⊢ Hpolytope ⋯ = {x | ↑f x = c}
Theorem: hyperplane_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
⊢ Hpolytope ⋯ = {x | ↑f x = c}
Tactic:
ext x
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x ∈ {x | ↑f x = c}
Theorem: hyperplane_Hpolytope
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ x ∈ Hpolytope ⋯ ↔ x ∈ {x | ↑f x = c}
Tactic:
rw [mem_Hpolytope, Set.mem_setOf]
Proof state after:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ (∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α) ↔ ↑f x = c
Theorem: hyperplane_Hpolytope
Proof state before:
case h
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ (∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α) ↔ ↑f x = c
Tactic:
constructor
Proof state after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ (∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α) → ↑f x = c

case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ ↑f x = c → ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
Theorem: hyperplane_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
⊢ Set.Finite {{ f := f, α := c }, { f := -f, α := -c }}
Tactic:
simp only [Set.mem_singleton_iff, Halfspace.mk.injEq, Set.finite_singleton, Set.Finite.insert]
Proof state after:
no goals
Theorem: hyperplane_Hpolytope
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
⊢ (∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α) → ↑f x = c
Tactic:
intro h
Proof state after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
⊢ ↑f x = c
Theorem: hyperplane_Hpolytope
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
⊢ ↑f x = c
Tactic:
have h1 := h (Halfspace.mk f c) (by simp)
Proof state after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := c }.f x ≤ { f := f, α := c }.α
⊢ ↑f x = c
Theorem: hyperplane_Hpolytope
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := c }.f x ≤ { f := f, α := c }.α
⊢ ↑f x = c
Tactic:
have h2 := h (Halfspace.mk (-f) (-c)) (by simp)
Proof state after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := c }.f x ≤ { f := f, α := c }.α
h2 : ↑{ f := -f, α := -c }.f x ≤ { f := -f, α := -c }.α
⊢ ↑f x = c
Theorem: hyperplane_Hpolytope
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := c }.f x ≤ { f := f, α := c }.α
h2 : ↑{ f := -f, α := -c }.f x ≤ { f := -f, α := -c }.α
⊢ ↑f x = c
Tactic:
rw [unitSphereDual_neg, ContinuousLinearMap.neg_apply, neg_le, neg_neg] at h2
Proof state after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := c }.f x ≤ { f := f, α := c }.α
h2 : c ≤ ↑f x
⊢ ↑f x = c
Theorem: hyperplane_Hpolytope
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
h1 : ↑{ f := f, α := c }.f x ≤ { f := f, α := c }.α
h2 : c ≤ ↑f x
⊢ ↑f x = c
Tactic:
change f.1 x ≤ c at h1
Proof state after:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
h2 : c ≤ ↑f x
h1 : ↑f x ≤ c
⊢ ↑f x = c
Theorem: hyperplane_Hpolytope
Proof state before:
case h.mp
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
h2 : c ≤ ↑f x
h1 : ↑f x ≤ c
⊢ ↑f x = c
Tactic:
exact le_antisymm h1 h2
Proof state after:
no goals
Theorem: hyperplane_Hpolytope
Proof state before:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ∀ Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}, ↑Hi.f x ≤ Hi.α
⊢ { f := f, α := c } ∈ {{ f := f, α := c }, { f := -f, α := -c }}
Tactic:
simp
Proof state after:
no goals