-- Mathlib/Analysis/Convex/Cone/Proper.lean
theorem hyperplane_separation (K : ProperCone ℝ E) {f : E →L[ℝ] F} {b : F} :
    b ∈ K.map f ↔ ∀ y : F, adjoint f y ∈ K.dual → 0 ≤ ⟪y, b⟫_ℝ :=
  Iff.intro
    (by
      -- suppose `b ∈ K.map f`
      simp_rw [mem_map, PointedCone.mem_closure, PointedCone.coe_map, coe_coe,
        mem_closure_iff_seq_limit, mem_image, SetLike.mem_coe, mem_coe, mem_dual,
        adjoint_inner_right, forall_exists_index, and_imp]

      -- there is a sequence `seq : ℕ → F` in the image of `f` that converges to `b`
      rintro seq hmem htends y hinner
      suffices h : ∀ n, 0 ≤ ⟪y, seq n⟫_ℝ from
        ge_of_tendsto'
          (Continuous.seqContinuous (Continuous.inner (@continuous_const _ _ _ _ y) continuous_id)
            htends)
          h
      intro n
      obtain ⟨_, h, hseq⟩ := hmem n
      simpa only [← hseq, real_inner_comm] using hinner h)
    (by
      -- proof by contradiction
      -- suppose `b ∉ K.map f`
      intro h
      contrapose! h

      -- as `b ∉ K.map f`, there is a hyperplane `y` separating `b` from `K.map f`
      let C := @PointedCone.toConvexCone ℝ F _ _ _ (K.map f)
      obtain ⟨y, hxy, hyb⟩ :=
        @ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem
        _ _ _ _ C (K.map f).nonempty (K.map f).isClosed b h

      -- the rest of the proof is a straightforward algebraic manipulation
      refine ⟨y, ?_, hyb⟩
      simp_rw [ProperCone.mem_dual, adjoint_inner_right]
      intro x hxK
      apply hxy (f x)
      simp_rw [C, coe_map]
      apply subset_closure
      simp_rw [PointedCone.toConvexCone_map, ConvexCone.coe_map, coe_coe, mem_image,
        SetLike.mem_coe]
      exact ⟨x, hxK, rfl⟩)

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f K
C : ConvexCone ℝ F := ↑↑(map f K)
⊢ ∃ y, (adjoint f) y ∈ K.dual ∧ ⟪y, b⟫_ℝ < 0

Tactic:
obtain ⟨y, hxy, hyb⟩ :=
  @ConvexCone.hyperplane_separation_of_nonempty_of_isClosed_of_nmem
  _ _ _ _ C (K.map f).nonempty (K.map f).isClosed b h

Result:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f K
C : ConvexCone ℝ F := ↑↑(map f K)
y : F
hxy : ∀ x ∈ C, 0 ≤ ⟪x, y⟫_ℝ
hyb : ⟪y, b⟫_ℝ < 0
⊢ ∃ y, (adjoint f) y ∈ K.dual ∧ ⟪y, b⟫_ℝ < 0

Proof state:
case intro.intro.a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f K
C : ConvexCone ℝ F := ↑↑(map f K)
y : F
hxy : ∀ x ∈ C, 0 ≤ ⟪x, y⟫_ℝ
hyb : ⟪y, b⟫_ℝ < 0
x : E
hxK : x ∈ K
⊢ ∃ x_1 ∈ ↑↑K, f x_1 = f x

Tactic:
exact ⟨x, hxK, rfl⟩

Result:
no goals

Proof state:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f K
C : ConvexCone ℝ F := ↑↑(map f K)
y : F
hxy : ∀ x ∈ C, 0 ≤ ⟪x, y⟫_ℝ
hyb : ⟪y, b⟫_ℝ < 0
⊢ (adjoint f) y ∈ K.dual

Tactic:
simp_rw [ProperCone.mem_dual, adjoint_inner_right]

Result:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f K
C : ConvexCone ℝ F := ↑↑(map f K)
y : F
hxy : ∀ x ∈ C, 0 ≤ ⟪x, y⟫_ℝ
hyb : ⟪y, b⟫_ℝ < 0
⊢ ∀ ⦃x : E⦄, x ∈ K → 0 ≤ ⟪f x, y⟫_ℝ

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), ∃ x ∈ K, f x = seq n
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ ⟪f x, y⟫_ℝ
⊢ ∀ (n : ℕ), 0 ≤ ⟪y, seq n⟫_ℝ

Tactic:
intro n

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), ∃ x ∈ K, f x = seq n
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ ⟪f x, y⟫_ℝ
n : ℕ
⊢ 0 ≤ ⟪y, seq n⟫_ℝ

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
⊢ ∀ (x : ℕ → F),
    (∀ (n : ℕ), ∃ x_1 ∈ K, f x_1 = x n) →
      Tendsto x atTop (nhds b) → ∀ (y : F), (∀ ⦃x : E⦄, x ∈ K → 0 ≤ ⟪f x, y⟫_ℝ) → 0 ≤ ⟪y, b⟫_ℝ

Tactic:
rintro seq hmem htends y hinner

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), ∃ x ∈ K, f x = seq n
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ ⟪f x, y⟫_ℝ
⊢ 0 ≤ ⟪y, b⟫_ℝ

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f K
⊢ ∃ y, (adjoint f) y ∈ K.dual ∧ ⟪y, b⟫_ℝ < 0

Tactic:
let C := @PointedCone.toConvexCone ℝ F _ _ _ (K.map f)

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f K
C : ConvexCone ℝ F := ↑↑(map f K)
⊢ ∃ y, (adjoint f) y ∈ K.dual ∧ ⟪y, b⟫_ℝ < 0

Proof state:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
seq : ℕ → F
hmem : ∀ (n : ℕ), ∃ x ∈ K, f x = seq n
htends : Tendsto seq atTop (nhds b)
y : F
hinner : ∀ ⦃x : E⦄, x ∈ K → 0 ≤ ⟪f x, y⟫_ℝ
n : ℕ
w✝ : E
h : w✝ ∈ K
hseq : f w✝ = seq n
⊢ 0 ≤ ⟪y, seq n⟫_ℝ

Tactic:
simpa only [← hseq, real_inner_comm] using hinner h

Result:
no goals

Proof state:
case intro.intro
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f K
C : ConvexCone ℝ F := ↑↑(map f K)
y : F
hxy : ∀ x ∈ C, 0 ≤ ⟪x, y⟫_ℝ
hyb : ⟪y, b⟫_ℝ < 0
x : E
hxK : x ∈ K
⊢ f x ∈ ↑(PointedCone.map ↑f ↑K).closure

Tactic:
apply subset_closure

Result:
case intro.intro.a
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace ℝ E
inst✝³ : CompleteSpace E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace ℝ F
inst✝ : CompleteSpace F
K : ProperCone ℝ E
f : E →L[ℝ] F
b : F
h : b ∉ map f K
C : ConvexCone ℝ F := ↑↑(map f K)
y : F
hxy : ∀ x ∈ C, 0 ≤ ⟪x, y⟫_ℝ
hyb : ⟪y, b⟫_ℝ < 0
x : E
hxK : x ∈ K
⊢ f x ∈ ↑↑(PointedCone.map ↑f ↑K)