-- Mathlib/Analysis/Convex/Topology.lean
theorem Convex.strictConvex {s : Set E} (hs : Convex 𝕜 s)
    (h : (s \ interior s).Pairwise fun x y => ([x -[𝕜] y] \ frontier s).Nonempty) :
    StrictConvex 𝕜 s

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
⊢ (⇑(lineMap x y) '' Icc 0 1 \ frontier s).Nonempty → ∃ c, (lineMap x y) c ∈ s \ frontier s

Tactic:
rintro ⟨_, ⟨⟨c, hc, rfl⟩, hcs⟩⟩

Result:
case intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
c : 𝕜
hc : c ∈ Icc 0 1
hcs : (lineMap x y) c ∉ frontier s
⊢ ∃ c, (lineMap x y) c ∈ s \ frontier s

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
c : 𝕜
hc : c ∈ Icc 0 1
hcs : (lineMap x y) c ∉ frontier s
⊢ (lineMap x y) c ∈ [x-[𝕜]y]

Tactic:
exact (segment_eq_image_lineMap 𝕜 x y).symm ▸ mem_image_of_mem _ hc

Result:
no goals

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
⊢ fun ⦃a b⦄ => ([a-[𝕜]b] \ frontier s).Nonempty → ∃ c, (lineMap a b) c ∈ interior s

Tactic:
simp only [segment_eq_image_lineMap, ← self_diff_frontier]

Result:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
⊢ (⇑(lineMap x y) '' Icc 0 1 \ frontier s).Nonempty → ∃ c, (lineMap x y) c ∈ s \ frontier s

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
c : 𝕜
hc : c ∈ Icc 0 1
hcs : (lineMap x y) c ∉ frontier s
⊢ ∃ c, (lineMap x y) c ∈ s \ frontier s

Tactic:
refine ⟨c, hs.segment_subset hx.1 hy.1 ?_, hcs⟩

Result:
case intro.intro.intro.intro
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
c : 𝕜
hc : c ∈ Icc 0 1
hcs : (lineMap x y) c ∉ frontier s
⊢ (lineMap x y) c ∈ [x-[𝕜]y]

Proof state:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty
⊢ StrictConvex 𝕜 s

Tactic:
refine hs.strictConvex' <| h.imp_on fun x hx y hy _ => ?_

Result:
𝕜 : Type u_2
E : Type u_3
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalAddGroup E
inst✝ : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun x y => ([x-[𝕜]y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
x✝ : x ≠ y
⊢ fun ⦃a b⦄ => ([a-[𝕜]b] \ frontier s).Nonempty → ∃ c, (lineMap a b) c ∈ interior s