-- Mathlib/Analysis/Normed/Affine/AddTorsorBases.lean
theorem AffineBasis.interior_convexHull {ι E : Type*} [Finite ι] [NormedAddCommGroup E]
    [NormedSpace ℝ E] (b : AffineBasis ι ℝ E) :
    interior (convexHull ℝ (range b)) = {x | ∀ i, 0 < b.coord i x}

Proof state:
case inl
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Subsingleton ι
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Tactic:
have : range b = univ :=
  AffineSubspace.eq_univ_of_subsingleton_span_eq_top (subsingleton_range _) b.tot

Result:
case inl
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Subsingleton ι
this : range ⇑b = univ
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Proof state:
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Tactic:
cases subsingleton_or_nontrivial ι

Result:
case inl
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Subsingleton ι
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

case inr
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Proof state:
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ (convexHull ℝ) (range ⇑b) = ⋂ i, ⇑(b.coord i) ⁻¹' Ici 0

Tactic:
rw [b.convexHull_eq_nonneg_coord, setOf_forall]

Result:
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ ⋂ i, {x | 0 ≤ (b.coord i) x} = ⋂ i, ⇑(b.coord i) ⁻¹' Ici 0

Proof state:
case inl
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Subsingleton ι
this : range ⇑b = univ
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Tactic:
simp [this]

Result:
no goals

Proof state:
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ ⋂ i, {x | 0 ≤ (b.coord i) x} = ⋂ i, ⇑(b.coord i) ⁻¹' Ici 0

Tactic:
rfl

Result:
no goals

Proof state:
case inr
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Tactic:
have : convexHull ℝ (range b) = ⋂ i, b.coord i ⁻¹' Ici 0 := by
  rw [b.convexHull_eq_nonneg_coord, setOf_forall]; rfl

Result:
case inr
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this✝ : FiniteDimensional ℝ E
this : (convexHull ℝ) (range ⇑b) = ⋂ i, ⇑(b.coord i) ⁻¹' Ici 0
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Proof state:
case inr
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Tactic:
haveI : FiniteDimensional ℝ E := b.finiteDimensional

Result:
case inr
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Proof state:
case inr
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this✝ : FiniteDimensional ℝ E
this : (convexHull ℝ) (range ⇑b) = ⋂ i, ⇑(b.coord i) ⁻¹' Ici 0
⊢ interior ((convexHull ℝ) (range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}

Tactic:
ext

Result:
case inr.h
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this✝ : FiniteDimensional ℝ E
this : (convexHull ℝ) (range ⇑b) = ⋂ i, ⇑(b.coord i) ⁻¹' Ici 0
x✝ : E
⊢ x✝ ∈ interior ((convexHull ℝ) (range ⇑b)) ↔ x✝ ∈ {x | ∀ (i : ι), 0 < (b.coord i) x}

Proof state:
case inr.h
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this✝ : FiniteDimensional ℝ E
this : (convexHull ℝ) (range ⇑b) = ⋂ i, ⇑(b.coord i) ⁻¹' Ici 0
x✝ : E
⊢ x✝ ∈ interior ((convexHull ℝ) (range ⇑b)) ↔ x✝ ∈ {x | ∀ (i : ι), 0 < (b.coord i) x}

Tactic:
simp only [this, interior_iInter_of_finite, ←
  IsOpenMap.preimage_interior_eq_interior_preimage (isOpenMap_barycentric_coord b _)
    (continuous_barycentric_coord b _),
  interior_Ici, mem_iInter, mem_setOf_eq, mem_Ioi, mem_preimage]

Result:
no goals