Theorem: hyperplane_Hpolytope (src/Polytope.lean)

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
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}

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]) , ?_ ⟩
State after:
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
⊢ Hpolytope ⋯ = {x | ↑f x = c}

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
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}

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]
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

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
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.α

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]
State after:
no goals

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
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

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)
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

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)
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

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
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

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
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

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
State after:
no goals

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
State after:
no goals

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.α
h1 : ↑{ f := f, α := c }.f x ≤ { f := f, α := c }.α
⊢ { f := -f, α := -c } ∈ {{ f := f, α := c }, { f := -f, α := -c }}
Tactic:
simp
State after:
no goals

State before:
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.α
Tactic:
intro h Hi hHi
State after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
Hi : Halfspace E
hHi : Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}
⊢ ↑Hi.f x ≤ Hi.α

State before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
Hi : Halfspace E
hHi : Hi ∈ {{ f := f, α := c }, { f := -f, α := -c }}
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
simp only [Set.mem_singleton_iff, Halfspace.mk.injEq, Set.mem_insert_iff] at hHi
State after:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
Hi : Halfspace E
hHi : Hi = { f := f, α := c } ∨ Hi = { f := -f, α := -c }
⊢ ↑Hi.f x ≤ Hi.α

State before:
case h.mpr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
Hi : Halfspace E
hHi : Hi = { f := f, α := c } ∨ Hi = { f := -f, α := -c }
⊢ ↑Hi.f x ≤ Hi.α
Tactic:
rcases hHi with rfl | rfl
State after:
case h.mpr.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
⊢ ↑{ f := f, α := c }.f x ≤ { f := f, α := c }.α

case h.mpr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
⊢ ↑{ f := -f, α := -c }.f x ≤ { f := -f, α := -c }.α

State before:
case h.mpr.inl
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
⊢ ↑{ f := f, α := c }.f x ≤ { f := f, α := c }.α
Tactic:
exact le_of_eq h
State after:
no goals

State before:
case h.mpr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
⊢ ↑{ f := -f, α := -c }.f x ≤ { f := -f, α := -c }.α
Tactic:
rw [unitSphereDual_neg, ContinuousLinearMap.neg_apply, neg_le, neg_neg]
State after:
case h.mpr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
⊢ c ≤ ↑f x

State before:
case h.mpr.inr
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : CompleteSpace E
f : { f // ‖f‖ = 1 }
c : ℝ
x : E
h : ↑f x = c
⊢ c ≤ ↑f x
Tactic:
exact le_of_eq h.symm
State after:
no goals