Theorem: compact_polarDual_iff (src/Polar.lean)

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Tactic:
cases' (em (X \ {0}).Nonempty) with hXnonempty hXempty
State after:
case inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X

case inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : ¬Set.Nonempty (X \ {0})
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X

State before:
case inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Tactic:
constructor <;> rw [Metric.isCompact_iff_isClosed_bounded, isBounded_iff_forall_norm_le]
State after:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ 0 ∈ interior (polarDual X) → IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C

case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ (IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C) → 0 ∈ interior (polarDual X)

State before:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ 0 ∈ interior (polarDual X) → IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Tactic:
intro h
State after:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C

State before:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Tactic:
have : IsOpen (interior (polarDual X)) := isOpen_interior
State after:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
this : IsOpen (interior (polarDual X))
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C

State before:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
this : IsOpen (interior (polarDual X))
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Tactic:
rw [Metric.isOpen_iff] at this
State after:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
this : ∀ x ∈ interior (polarDual X), ∃ ε > 0, Metric.ball x ε ⊆ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C

State before:
case inl.mp
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
this : ∀ x ∈ interior (polarDual X), ∃ ε > 0, Metric.ball x ε ⊆ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Tactic:
rcases this 0 h with ⟨ ε, hε, hball ⟩
State after:
case inl.mp.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
this : ∀ x ∈ interior (polarDual X), ∃ ε > 0, Metric.ball x ε ⊆ interior (polarDual X)
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C

State before:
case inl.mp.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : 0 ∈ interior (polarDual X)
this : ∀ x ∈ interior (polarDual X), ∃ ε > 0, Metric.ball x ε ⊆ interior (polarDual X)
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Tactic:
clear this h
State after:
case inl.mp.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C

State before:
case inl.mp.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
⊢ IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
Tactic:
refine ⟨ hXcl, 2/ε, fun x hx => ?_ ⟩
State after:
case inl.mp.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
⊢ ‖x‖ ≤ 2 / ε

State before:
case inl.mp.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
⊢ ‖x‖ ≤ 2 / ε
Tactic:
cases' em (x = 0) with hx0 hx0
State after:
case inl.mp.intro.intro.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : x = 0
⊢ ‖x‖ ≤ 2 / ε

case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ‖x‖ ≤ 2 / ε

State before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
⊢ ‖x‖ ≤ 2 / ε
Tactic:
let u : E := (ε/2/(norm x)) • x
State after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
⊢ ‖x‖ ≤ 2 / ε

State before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
⊢ ‖x‖ ≤ 2 / ε
Tactic:
have hnormu : ‖u‖ = ε/2 := by
  rw [norm_smul, Real.norm_eq_abs, abs_of_pos (div_pos (half_pos hε) (norm_pos_iff.mpr hx0)),
    div_mul_cancel _ (norm_ne_zero_iff.mpr hx0)]
  done
State after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
⊢ ‖x‖ ≤ 2 / ε

State before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
⊢ ‖x‖ ≤ 2 / ε
Tactic:
have hu : u ∈ Metric.ball (0:E) ε := by
  rw [Metric.mem_ball, dist_zero_right, hnormu]
  exact half_lt_self hε
State after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
⊢ ‖x‖ ≤ 2 / ε

State before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
⊢ ‖x‖ ≤ 2 / ε
Tactic:
have h := interior_subset <| hball hu
State after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : u ∈ polarDual X
⊢ ‖x‖ ≤ 2 / ε

State before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : u ∈ polarDual X
⊢ ‖x‖ ≤ 2 / ε
Tactic:
rw [mem_polarDual] at h
State after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : ∀ x ∈ X, ⟪x, u⟫_ℝ ≤ 1
⊢ ‖x‖ ≤ 2 / ε

State before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : ∀ x ∈ X, ⟪x, u⟫_ℝ ≤ 1
⊢ ‖x‖ ≤ 2 / ε
Tactic:
specialize h x hx
State after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : ⟪x, u⟫_ℝ ≤ 1
⊢ ‖x‖ ≤ 2 / ε

State before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : ⟪x, u⟫_ℝ ≤ 1
⊢ ‖x‖ ≤ 2 / ε
Tactic:
rw [real_inner_smul_right, real_inner_self_eq_norm_mul_norm, ←mul_assoc,
  div_mul_cancel _ (norm_ne_zero_iff.mpr hx0), mul_comm, ← div_le_div_right (div_pos hε zero_lt_two),
  mul_div_cancel _ (Ne.symm <| ne_of_lt (div_pos hε zero_lt_two)), one_div_div] at h
State after:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : ‖x‖ ≤ 2 / ε
⊢ ‖x‖ ≤ 2 / ε

State before:
case inl.mp.intro.intro.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
hu : u ∈ Metric.ball 0 ε
h : ‖x‖ ≤ 2 / ε
⊢ ‖x‖ ≤ 2 / ε
Tactic:
exact h
State after:
no goals

State before:
case inl.mp.intro.intro.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : x = 0
⊢ ‖x‖ ≤ 2 / ε
Tactic:
rw [hx0, norm_zero]
State after:
case inl.mp.intro.intro.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : x = 0
⊢ 0 ≤ 2 / ε

State before:
case inl.mp.intro.intro.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : x = 0
⊢ 0 ≤ 2 / ε
Tactic:
exact div_nonneg zero_le_two (le_of_lt hε)
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
⊢ ‖u‖ = ε / 2
Tactic:
rw [norm_smul, Real.norm_eq_abs, abs_of_pos (div_pos (half_pos hε) (norm_pos_iff.mpr hx0)),
  div_mul_cancel _ (norm_ne_zero_iff.mpr hx0)]
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
⊢ u ∈ Metric.ball 0 ε
Tactic:
rw [Metric.mem_ball, dist_zero_right, hnormu]
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
⊢ ε / 2 < ε

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
ε : ℝ
hε : ε > 0
hball : Metric.ball 0 ε ⊆ interior (polarDual X)
x : E
hx : x ∈ X
hx0 : ¬x = 0
u : E := (ε / 2 / ‖x‖) • x
hnormu : ‖u‖ = ε / 2
⊢ ε / 2 < ε
Tactic:
exact half_lt_self hε
State after:
no goals

State before:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ (IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C) → 0 ∈ interior (polarDual X)
Tactic:
rw [interior_eq_compl_closure_compl, Set.mem_compl_iff, Metric.mem_closure_iff, dist_zero_left]
State after:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ (IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C) → ¬∀ ε > 0, ∃ b ∈ (polarDual X)ᶜ, ‖b‖ < ε

State before:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ (IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C) → ¬∀ ε > 0, ∃ b ∈ (polarDual X)ᶜ, ‖b‖ < ε
Tactic:
push_neg
State after:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ (IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C) → ∃ ε > 0, ∀ b ∈ (polarDual X)ᶜ, ε ≤ ‖b‖

State before:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
⊢ (IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C) → ∃ ε > 0, ∀ b ∈ (polarDual X)ᶜ, ε ≤ ‖b‖
Tactic:
intro h
State after:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
⊢ ∃ ε > 0, ∀ b ∈ (polarDual X)ᶜ, ε ≤ ‖b‖

State before:
case inl.mpr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
h : IsClosed X ∧ ∃ C, ∀ x ∈ X, ‖x‖ ≤ C
⊢ ∃ ε > 0, ∀ b ∈ (polarDual X)ᶜ, ε ≤ ‖b‖
Tactic:
rcases h with ⟨ _, M, hM ⟩
State after:
case inl.mpr.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ ∃ ε > 0, ∀ b ∈ (polarDual X)ᶜ, ε ≤ ‖b‖

State before:
case inl.mpr.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ ∃ ε > 0, ∀ b ∈ (polarDual X)ᶜ, ε ≤ ‖b‖
Tactic:
use 1/M
State after:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ 1 / M > 0 ∧ ∀ b ∈ (polarDual X)ᶜ, 1 / M ≤ ‖b‖

State before:
case h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ 1 / M > 0 ∧ ∀ b ∈ (polarDual X)ᶜ, 1 / M ≤ ‖b‖
Tactic:
refine ⟨ ?_, ?_ ⟩
State after:
case h.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ 1 / M > 0

case h.refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ ∀ b ∈ (polarDual X)ᶜ, 1 / M ≤ ‖b‖

State before:
case h.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ 1 / M > 0
Tactic:
rw [gt_iff_lt, one_div]
State after:
case h.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ 0 < M⁻¹

State before:
case h.refine_1
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ 0 < M⁻¹
Tactic:
exact inv_pos.mpr <| lt_of_lt_of_le (norm_pos_iff.mpr hXnonempty.some_mem.2) (hM hXnonempty.some hXnonempty.some_mem.1)
State after:
no goals

State before:
case h.refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
⊢ ∀ b ∈ (polarDual X)ᶜ, 1 / M ≤ ‖b‖
Tactic:
intro b hb
State after:
case h.refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
b : E
hb : b ∈ (polarDual X)ᶜ
⊢ 1 / M ≤ ‖b‖

State before:
case h.refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
b : E
hb : b ∈ (polarDual X)ᶜ
⊢ 1 / M ≤ ‖b‖
Tactic:
rw [Set.mem_compl_iff, mem_polarDual] at hb
State after:
case h.refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
b : E
hb : ¬∀ x ∈ X, ⟪x, b⟫_ℝ ≤ 1
⊢ 1 / M ≤ ‖b‖

State before:
case h.refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
b : E
hb : ¬∀ x ∈ X, ⟪x, b⟫_ℝ ≤ 1
⊢ 1 / M ≤ ‖b‖
Tactic:
push_neg at hb
State after:
case h.refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
b : E
hb : ∃ x ∈ X, 1 < ⟪x, b⟫_ℝ
⊢ 1 / M ≤ ‖b‖

State before:
case h.refine_2
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
b : E
hb : ∃ x ∈ X, 1 < ⟪x, b⟫_ℝ
⊢ 1 / M ≤ ‖b‖
Tactic:
rcases hb with ⟨ y, hy, hb ⟩
State after:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
⊢ 1 / M ≤ ‖b‖

State before:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
hM : ∀ x ∈ X, ‖x‖ ≤ M
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
⊢ 1 / M ≤ ‖b‖
Tactic:
specialize hM y hy
State after:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
⊢ 1 / M ≤ ‖b‖

State before:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
⊢ 1 / M ≤ ‖b‖
Tactic:
have hnorminner: |inner y b| ≤ ‖y‖ * ‖b‖ := by
  exact abs_real_inner_le_norm y b
State after:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : |⟪y, b⟫_ℝ| ≤ ‖y‖ * ‖b‖
⊢ 1 / M ≤ ‖b‖

State before:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : |⟪y, b⟫_ℝ| ≤ ‖y‖ * ‖b‖
⊢ 1 / M ≤ ‖b‖
Tactic:
rw [abs_of_pos (lt_trans zero_lt_one hb)] at hnorminner
State after:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
⊢ 1 / M ≤ ‖b‖

State before:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
⊢ 1 / M ≤ ‖b‖
Tactic:
have : (1:ℝ) ≤ ‖y‖ * ‖b‖ := le_trans (le_of_lt hb) hnorminner
State after:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
⊢ 1 / M ≤ ‖b‖

State before:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
⊢ 1 / M ≤ ‖b‖
Tactic:
have hynezero: y ≠ 0 := by
  rintro rfl
  rw [norm_zero, zero_mul] at this
  exact not_lt_of_le this zero_lt_one
State after:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : y ≠ 0
⊢ 1 / M ≤ ‖b‖

State before:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : y ≠ 0
⊢ 1 / M ≤ ‖b‖
Tactic:
rw [← norm_pos_iff] at hynezero
State after:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ 1 / M ≤ ‖b‖

State before:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ 1 / M ≤ ‖b‖
Tactic:
apply le_trans (div_le_div (le_of_lt <| lt_trans zero_lt_one hb) (le_of_lt hb) hynezero hM)
State after:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ / ‖y‖ ≤ ‖b‖

State before:
case h.refine_2.intro.intro
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ / ‖y‖ ≤ ‖b‖
Tactic:
apply div_le_of_nonneg_of_le_mul (le_of_lt hynezero)
State after:
case h.refine_2.intro.intro.hc
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ 0 ≤ ‖b‖

case h.refine_2.intro.intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ ≤ ‖b‖ * ‖y‖

State before:
case h.refine_2.intro.intro.hc
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ 0 ≤ ‖b‖

case h.refine_2.intro.intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ ≤ ‖b‖ * ‖y‖
Tactic:
apply (mul_nonneg_iff_of_pos_left hynezero).mp (le_trans (zero_le_one) this)
State after:
case h.refine_2.intro.intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ ≤ ‖b‖ * ‖y‖

State before:
case h.refine_2.intro.intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ ≤ ‖b‖ * ‖y‖
Tactic:
rw [mul_comm]
State after:
case h.refine_2.intro.intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖

State before:
case h.refine_2.intro.intro.h
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
hynezero : 0 < ‖y‖
⊢ ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
Tactic:
exact hnorminner
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
⊢ |⟪y, b⟫_ℝ| ≤ ‖y‖ * ‖b‖
Tactic:
exact abs_real_inner_le_norm y b
State after:
no goals

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b y : E
hy : y ∈ X
hb : 1 < ⟪y, b⟫_ℝ
hM : ‖y‖ ≤ M
hnorminner : ⟪y, b⟫_ℝ ≤ ‖y‖ * ‖b‖
this : 1 ≤ ‖y‖ * ‖b‖
⊢ y ≠ 0
Tactic:
rintro rfl
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b : E
hy : 0 ∈ X
hb : 1 < ⟪0, b⟫_ℝ
hM : ‖0‖ ≤ M
hnorminner : ⟪0, b⟫_ℝ ≤ ‖0‖ * ‖b‖
this : 1 ≤ ‖0‖ * ‖b‖
⊢ False

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b : E
hy : 0 ∈ X
hb : 1 < ⟪0, b⟫_ℝ
hM : ‖0‖ ≤ M
hnorminner : ⟪0, b⟫_ℝ ≤ ‖0‖ * ‖b‖
this : 1 ≤ ‖0‖ * ‖b‖
⊢ False
Tactic:
rw [norm_zero, zero_mul] at this
State after:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b : E
hy : 0 ∈ X
hb : 1 < ⟪0, b⟫_ℝ
hM : ‖0‖ ≤ M
hnorminner : ⟪0, b⟫_ℝ ≤ ‖0‖ * ‖b‖
this : 1 ≤ 0
⊢ False

State before:
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXnonempty : Set.Nonempty (X \ {0})
left✝ : IsClosed X
M : ℝ
b : E
hy : 0 ∈ X
hb : 1 < ⟪0, b⟫_ℝ
hM : ‖0‖ ≤ M
hnorminner : ⟪0, b⟫_ℝ ≤ ‖0‖ * ‖b‖
this : 1 ≤ 0
⊢ False
Tactic:
exact not_lt_of_le this zero_lt_one
State after:
no goals

State before:
case inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : ¬Set.Nonempty (X \ {0})
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Tactic:
rw [Set.not_nonempty_iff_eq_empty, Set.diff_eq_empty, Set.subset_singleton_iff_eq] at hXempty
State after:
case inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : X = ∅ ∨ X = {0}
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X

State before:
case inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : X = ∅ ∨ X = {0}
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Tactic:
cases' hXempty with hXempty hX0
State after:
case inr.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : X = ∅
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X

case inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hX0 : X = {0}
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X

State before:
case inr.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : X = ∅
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Tactic:
rw [hXempty, polarDual_empty, interior_univ]
State after:
case inr.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : X = ∅
⊢ 0 ∈ Set.univ ↔ IsCompact ∅

State before:
case inr.inl
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hXempty : X = ∅
⊢ 0 ∈ Set.univ ↔ IsCompact ∅
Tactic:
exact ⟨ fun _ => isCompact_empty, fun _ => trivial ⟩
State after:
no goals

State before:
case inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hX0 : X = {0}
⊢ 0 ∈ interior (polarDual X) ↔ IsCompact X
Tactic:
rw [hX0, polarDual_zero, interior_univ]
State after:
case inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hX0 : X = {0}
⊢ 0 ∈ Set.univ ↔ IsCompact {0}

State before:
case inr.inr
E : Type
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : FiniteDimensional ℝ E
X : Set E
hXcl : IsClosed X
hX0 : X = {0}
⊢ 0 ∈ Set.univ ↔ IsCompact {0}
Tactic:
exact ⟨ fun _ => isCompact_singleton, fun _ => trivial ⟩
State after:
no goals