-- Mathlib/Analysis/Normed/Affine/AddTorsorBases.lean
theorem interior_convexHull_nonempty_iff_affineSpan_eq_top [FiniteDimensional ℝ V] {s : Set V} :
    (interior (convexHull ℝ s)).Nonempty ↔ affineSpan ℝ s = ⊤

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
⊢ (interior ((convexHull ℝ) s)).Nonempty

Tactic:
obtain ⟨t, hts, b, hb⟩ := AffineBasis.exists_affine_subbasis h

Result:
case intro.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
⊢ (interior ((convexHull ℝ) s)).Nonempty

Proof state:
case intro.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
⊢ (interior ((convexHull ℝ) s)).Nonempty

Tactic:
suffices (interior (convexHull ℝ (range b))).Nonempty by
  rw [hb, Subtype.range_coe_subtype, setOf_mem_eq] at this
  refine this.mono (by gcongr)

Result:
case intro.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
⊢ (interior ((convexHull ℝ) (range ⇑b))).Nonempty

Proof state:
case intro.intro.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Finset V
hts : ↑t ⊆ s
b : AffineBasis ↑↑t ℝ V
hb : ⇑b = Subtype.val
⊢ (interior ((convexHull ℝ) (range ⇑b))).Nonempty

Tactic:
exact ⟨_, b.centroid_mem_interior_convexHull⟩

Result:
no goals

Proof state:
case intro.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
⊢ (interior ((convexHull ℝ) (range ⇑b))).Nonempty

Tactic:
lift t to Finset V using b.finite_set

Result:
case intro.intro.intro.intro
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Finset V
hts : ↑t ⊆ s
b : AffineBasis ↑↑t ℝ V
hb : ⇑b = Subtype.val
⊢ (interior ((convexHull ℝ) (range ⇑b))).Nonempty

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
this : (interior ((convexHull ℝ) t)).Nonempty
⊢ (interior ((convexHull ℝ) s)).Nonempty

Tactic:
refine this.mono (by gcongr)

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
this : (interior ((convexHull ℝ) (range ⇑b))).Nonempty
⊢ (interior ((convexHull ℝ) s)).Nonempty

Tactic:
rw [hb, Subtype.range_coe_subtype, setOf_mem_eq] at this

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
this : (interior ((convexHull ℝ) t)).Nonempty
⊢ (interior ((convexHull ℝ) s)).Nonempty

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
t : Set V
hts : t ⊆ s
b : AffineBasis ↑t ℝ V
hb : ⇑b = Subtype.val
this : (interior ((convexHull ℝ) t)).Nonempty
⊢ interior ((convexHull ℝ) t) ⊆ interior ((convexHull ℝ) s)

Tactic:
gcongr

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
⊢ (interior ((convexHull ℝ) s)).Nonempty ↔ affineSpan ℝ s = ⊤

Tactic:
refine ⟨affineSpan_eq_top_of_nonempty_interior, fun h => ?_⟩

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : FiniteDimensional ℝ V
s : Set V
h : affineSpan ℝ s = ⊤
⊢ (interior ((convexHull ℝ) s)).Nonempty