-- Mathlib/Analysis/Convex/StrictConvexSpace.lean
theorem StrictConvexSpace.of_norm_combo_lt_one
    (h : ∀ x y : E, ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b : ℝ, a + b = 1 ∧ ‖a • x + b • y‖ < 1) :
    StrictConvexSpace ℝ E

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1
⊢ StrictConvexSpace ℝ E

Tactic:
refine
  StrictConvexSpace.of_strictConvex_unitClosedBall ℝ
    ((convex_closedBall _ _).strictConvex' fun x hx y hy hne => ?_)

Result:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : x ∈ closedBall 0 1 \ interior (closedBall 0 1)
y : E
hy : y ∈ closedBall 0 1 \ interior (closedBall 0 1)
hne : x ≠ y
⊢ (fun x y => ∃ c, (AffineMap.lineMap x y) c ∈ interior (closedBall 0 1)) x y

Proof state:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
hab : a + b = 1
hlt : ‖a • x + b • y‖ < 1
⊢ (AffineMap.lineMap x y) b ∈ interior (closedBall 0 1)

Tactic:
rwa [AffineMap.lineMap_apply_module, interior_closedBall (0 : E) one_ne_zero, mem_ball_zero_iff,
  sub_eq_iff_eq_add.2 hab.symm]

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
⊢ ∃ c, (AffineMap.lineMap x y) c ∈ interior (closedBall 0 1)

Tactic:
rcases h x y hx hy hne with ⟨a, b, hab, hlt⟩

Result:
case intro.intro.intro
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
hab : a + b = 1
hlt : ‖a • x + b • y‖ < 1
⊢ ∃ c, (AffineMap.lineMap x y) c ∈ interior (closedBall 0 1)

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : x ∈ closedBall 0 1 \ interior (closedBall 0 1)
y : E
hy : y ∈ closedBall 0 1 \ interior (closedBall 0 1)
hne : x ≠ y
⊢ (fun x y => ∃ c, (AffineMap.lineMap x y) c ∈ interior (closedBall 0 1)) x y

Tactic:
rw [interior_closedBall (0 : E) one_ne_zero, closedBall_diff_ball,
  mem_sphere_zero_iff_norm] at hx hy

Result:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
⊢ ∃ c, (AffineMap.lineMap x y) c ∈ interior (closedBall 0 1)

Proof state:
case intro.intro.intro
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
hab : a + b = 1
hlt : ‖a • x + b • y‖ < 1
⊢ ∃ c, (AffineMap.lineMap x y) c ∈ interior (closedBall 0 1)

Tactic:
use b

Result:
case h
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
h : ∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, a + b = 1 ∧ ‖a • x + b • y‖ < 1
x : E
hx : ‖x‖ = 1
y : E
hy : ‖y‖ = 1
hne : x ≠ y
a b : ℝ
hab : a + b = 1
hlt : ‖a • x + b • y‖ < 1
⊢ (AffineMap.lineMap x y) b ∈ interior (closedBall 0 1)