-- Mathlib/Analysis/Convex/Cone/InnerDual.lean
theorem ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem (K : ConvexCone ℝ H)
    (ne : (K : Set H).Nonempty) (hc : IsClosed (K : Set H)) {b : H} (disj : b ∉ K) :
    ∃ y : H, (∀ x : H, x ∈ K → 0 ≤ ⟪x, y⟫_ℝ) ∧ ⟪y, b⟫_ℝ < 0

Proof state:
case h.right
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
b : H
disj : b ∉ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖
hinner : ∀ w ∈ ↑K, ⟪b - z, w - z⟫_ℝ ≤ 0
hinner₀ : ⟪b - z, 0 - z⟫_ℝ ≤ 0
⊢ ⟪z - b, b⟫_ℝ < 0

Tactic:
rw [zero_sub, inner_neg_right, Right.neg_nonpos_iff] at hinner₀

Result:
case h.right
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
b : H
disj : b ∉ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖
hinner : ∀ w ∈ ↑K, ⟪b - z, w - z⟫_ℝ ≤ 0
hinner₀ : 0 ≤ ⟪b - z, z⟫_ℝ
⊢ ⟪z - b, b⟫_ℝ < 0

Proof state:
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
b : H
disj : b ∉ K
⊢ ∃ y, (∀ x ∈ K, 0 ≤ ⟪x, y⟫_ℝ) ∧ ⟪y, b⟫_ℝ < 0

Tactic:
obtain ⟨z, hzK, infi⟩ := exists_norm_eq_iInf_of_complete_convex ne hc.isComplete K.convex b

Result:
case intro.intro
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
b : H
disj : b ∉ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖
⊢ ∃ y, (∀ x ∈ K, 0 ≤ ⟪x, y⟫_ℝ) ∧ ⟪y, b⟫_ℝ < 0

Proof state:
case h.right
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
b : H
disj : b ∉ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖
hinner : ∀ w ∈ ↑K, ⟪b - z, w - z⟫_ℝ ≤ 0
hinner₀ : 0 ≤ ⟪b - z, z⟫_ℝ
⊢ ⟪z - b, b⟫_ℝ < 0

Tactic:
have hbz : b - z ≠ 0 := by
  rw [sub_ne_zero]
  contrapose! hzK
  rwa [← hzK]

Result:
case h.right
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
b : H
disj : b ∉ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖
hinner : ∀ w ∈ ↑K, ⟪b - z, w - z⟫_ℝ ≤ 0
hinner₀ : 0 ≤ ⟪b - z, z⟫_ℝ
hbz : b - z ≠ 0
⊢ ⟪z - b, b⟫_ℝ < 0

Proof state:
case h.right
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
b : H
disj : b ∉ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖
hinner : ∀ w ∈ ↑K, ⟪b - z, w - z⟫_ℝ ≤ 0
hinner₀ : 0 ≤ ⟪b - z, z⟫_ℝ
hbz : b - z ≠ 0
⊢ 0 < ⟪b - z, b⟫_ℝ

Tactic:
calc
  0 < ⟪b - z, b - z⟫_ℝ := lt_of_not_le ((Iff.not real_inner_self_nonpos).2 hbz)
  _ = ⟪b - z, b - z⟫_ℝ + 0 := (add_zero _).symm
  _ ≤ ⟪b - z, b - z⟫_ℝ + ⟪b - z, z⟫_ℝ := add_le_add rfl.ge hinner₀
  _ = ⟪b - z, b - z + z⟫_ℝ := (inner_add_right _ _ _).symm
  _ = ⟪b - z, b⟫_ℝ := by rw [sub_add_cancel]

Result:
no goals

Proof state:
case intro.intro
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
b : H
disj : b ∉ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖
⊢ ∃ y, (∀ x ∈ K, 0 ≤ ⟪x, y⟫_ℝ) ∧ ⟪y, b⟫_ℝ < 0

Tactic:
have hinner := (norm_eq_iInf_iff_real_inner_le_zero K.convex hzK).1 infi

Result:
case intro.intro
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
b : H
disj : b ∉ K
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖
hinner : ∀ w ∈ ↑K, ⟪b - z, w - z⟫_ℝ ≤ 0
⊢ ∃ y, (∀ x ∈ K, 0 ≤ ⟪x, y⟫_ℝ) ∧ ⟪y, b⟫_ℝ < 0