-- 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
⊢ ⟪z - b, b⟫_ℝ < 0

Tactic:
have hinner₀ := hinner 0 (K.pointed_of_nonempty_of_isClosed ne hc)

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₀ : ⟪b - z, 0 - z⟫_ℝ ≤ 0
⊢ ⟪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
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
⊢ ⟪b - z, b - z + z⟫_ℝ = ⟪b - z, b⟫_ℝ

Tactic:
rw [sub_add_cancel]

Result:
no goals

Proof state:
case h
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
⊢ (∀ x ∈ K, 0 ≤ ⟪x, z - b⟫_ℝ) ∧ ⟪z - b, b⟫_ℝ < 0

Tactic:
constructor

Result:
case h.left
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
⊢ ∀ x ∈ K, 0 ≤ ⟪x, z - b⟫_ℝ

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
⊢ ⟪z - b, b⟫_ℝ < 0

Proof state:
case h.left
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
⊢ ∀ x ∈ K, 0 ≤ ⟪x, z - b⟫_ℝ

Tactic:
rintro x hxK

Result:
case h.left
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
x : H
hxK : x ∈ K
⊢ 0 ≤ ⟪x, z - b⟫_ℝ

Proof state:
case h.left
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
x : H
hxK : x ∈ K
⊢ 0 ≤ ⟪x, z - b⟫_ℝ

Tactic:
specialize hinner _ (K.add_mem hxK hzK)

Result:
case h.left
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‖
x : H
hxK : x ∈ K
hinner : ⟪b - z, x + z - z⟫_ℝ ≤ 0
⊢ 0 ≤ ⟪x, z - b⟫_ℝ

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
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖
hinner : ∀ w ∈ ↑K, ⟪b - z, w - z⟫_ℝ ≤ 0
hinner₀ : 0 ≤ ⟪b - z, z⟫_ℝ
⊢ b - z ≠ 0

Tactic:
rw [sub_ne_zero]

Result:
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⟫_ℝ
⊢ b ≠ z

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
z : H
infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖
hinner : ∀ w ∈ ↑K, ⟪b - z, w - z⟫_ℝ ≤ 0
hinner₀ : 0 ≤ ⟪b - z, z⟫_ℝ
hzK : b = z
⊢ z ∉ ↑K

Tactic:
rwa [← hzK]

Result:
no goals

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
z : H
hzK : z ∈ ↑K
infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖
hinner : ∀ w ∈ ↑K, ⟪b - z, w - z⟫_ℝ ≤ 0
hinner₀ : 0 ≤ ⟪b - z, z⟫_ℝ
⊢ b ≠ z

Tactic:
contrapose! hzK

Result:
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
infi : ‖b - z‖ = ⨅ w, ‖b - ↑w‖
hinner : ∀ w ∈ ↑K, ⟪b - z, w - z⟫_ℝ ≤ 0
hinner₀ : 0 ≤ ⟪b - z, z⟫_ℝ
hzK : b = z
⊢ z ∉ ↑K

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
⊢ ⟪z - b, b⟫_ℝ < 0

Tactic:
rw [← neg_zero, lt_neg, ← neg_one_mul, ← real_inner_smul_left, smul_sub, neg_smul, one_smul,
  neg_smul, neg_sub_neg, one_smul]

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
⊢ 0 < ⟪b - z, b⟫_ℝ

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‖
hinner : ∀ w ∈ ↑K, ⟪b - z, w - z⟫_ℝ ≤ 0
⊢ ∃ y, (∀ x ∈ K, 0 ≤ ⟪x, y⟫_ℝ) ∧ ⟪y, b⟫_ℝ < 0

Tactic:
use z - b

Result:
case h
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
⊢ (∀ x ∈ K, 0 ≤ ⟪x, z - b⟫_ℝ) ∧ ⟪z - b, b⟫_ℝ < 0

Proof state:
case h.left
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‖
x : H
hxK : x ∈ K
hinner : ⟪b - z, x + z - z⟫_ℝ ≤ 0
⊢ 0 ≤ ⟪x, z - b⟫_ℝ

Tactic:
rwa [add_sub_cancel_right, real_inner_comm, ← neg_nonneg, neg_eq_neg_one_mul,
  ← real_inner_smul_right, neg_smul, one_smul, neg_sub] at hinner

Result:
no goals