-- Mathlib/Analysis/Convex/Cone/InnerDual.lean
theorem ConvexCone.innerDualCone_of_innerDualCone_eq_self (K : ConvexCone ℝ H)
    (ne : (K : Set H).Nonempty) (hc : IsClosed (K : Set H)) :
    ((K : Set H).innerDualCone : Set H).innerDualCone = K

Proof state:
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
⊢ (↑(↑K).innerDualCone).innerDualCone = K

Tactic:
ext x

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
x : H
⊢ x ∈ (↑(↑K).innerDualCone).innerDualCone ↔ x ∈ K

Proof state:
case h.mp
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
x : H
⊢ (∀ x_1 ∈ ↑(↑K).innerDualCone, 0 ≤ inner x_1 x) → x ∈ ↑K

Tactic:
contrapose!

Result:
case h.mp
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
x : H
⊢ x ∉ ↑K → ∃ x_1 ∈ ↑(↑K).innerDualCone, inner x_1 x < 0

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
x : H
⊢ x ∈ (↑(↑K).innerDualCone).innerDualCone ↔ x ∈ K

Tactic:
constructor

Result:
case h.mp
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
x : H
⊢ x ∈ (↑(↑K).innerDualCone).innerDualCone → x ∈ K

case h.mpr
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
x : H
⊢ x ∈ K → x ∈ (↑(↑K).innerDualCone).innerDualCone

Proof state:
case h.mpr
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
x : H
hxK : x ∈ K
y : H
h : y ∈ ↑(↑K).innerDualCone
⊢ 0 ≤ inner y x

Tactic:
specialize h x hxK

Result:
case h.mpr
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
x : H
hxK : x ∈ K
y : H
h : 0 ≤ inner x y
⊢ 0 ≤ inner y x

Proof state:
case h.mp
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
x : H
⊢ x ∈ (↑(↑K).innerDualCone).innerDualCone → x ∈ K

Tactic:
rw [mem_innerDualCone, ← SetLike.mem_coe]

Result:
case h.mp
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
x : H
⊢ (∀ x_1 ∈ ↑(↑K).innerDualCone, 0 ≤ inner x_1 x) → x ∈ ↑K

Proof state:
case h.mpr
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
x : H
hxK : x ∈ K
y : H
h : 0 ≤ inner x y
⊢ 0 ≤ inner y x

Tactic:
rwa [real_inner_comm]

Result:
no goals

Proof state:
case h.mpr
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
x : H
⊢ x ∈ K → x ∈ (↑(↑K).innerDualCone).innerDualCone

Tactic:
rintro hxK y h

Result:
case h.mpr
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
x : H
hxK : x ∈ K
y : H
h : y ∈ ↑(↑K).innerDualCone
⊢ 0 ≤ inner y x

Proof state:
case h.mp
H : Type u_1
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℝ H
inst✝ : CompleteSpace H
K : ConvexCone ℝ H
ne : (↑K).Nonempty
hc : IsClosed ↑K
x : H
⊢ x ∉ ↑K → ∃ x_1 ∈ ↑(↑K).innerDualCone, inner x_1 x < 0

Tactic:
exact K.hyperplane_separation_of_nonempty_of_isClosed_of_nmem ne hc

Result:
no goals