case inl
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Subsingleton ι
⊢ interior (↑(convexHull ℝ).toOrderHom (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b 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 ℝ).toOrderHom (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
⊢ interior (↑(convexHull ℝ).toOrderHom (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
cases subsingleton_or_nontrivial ι
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 ℝ).toOrderHom (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
case inl
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Subsingleton ι
⊢ interior (↑(convexHull ℝ).toOrderHom (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
have : range b = univ :=
  AffineSubspace.eq_univ_of_subsingleton_span_eq_top (subsingleton_range _) b.tot
no goals
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 ℝ).toOrderHom (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
simp [this]
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 ℝ).toOrderHom (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b 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 ℝ).toOrderHom (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
haveI : FiniteDimensional ℝ E := b.finiteDimensional
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 ℝ).toOrderHom (range ↑b) = ⋂ (i : ι), ↑(coord b i) ⁻¹' Ici 0
⊢ interior (↑(convexHull ℝ).toOrderHom (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
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 ℝ).toOrderHom (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
have : convexHull ℝ (range b) = ⋂ i, b.coord i ⁻¹' Ici 0 := by
  rw [b.convexHull_eq_nonneg_coord, setOf_forall]; rfl
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 ℝ).toOrderHom (range ↑b) = ⋂ (i : ι), ↑(coord b i) ⁻¹' Ici 0
x✝ : E
⊢ x✝ ∈ interior (↑(convexHull ℝ).toOrderHom (range ↑b)) ↔ x✝ ∈ {x | ∀ (i : ι), 0 < ↑(coord b i) x}
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 ℝ).toOrderHom (range ↑b) = ⋂ (i : ι), ↑(coord b i) ⁻¹' Ici 0
⊢ interior (↑(convexHull ℝ).toOrderHom (range ↑b)) = {x | ∀ (i : ι), 0 < ↑(coord b i) x}
ext
no goals
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 ℝ).toOrderHom (range ↑b) = ⋂ (i : ι), ↑(coord b i) ⁻¹' Ici 0
x✝ : E
⊢ x✝ ∈ interior (↑(convexHull ℝ).toOrderHom (range ↑b)) ↔ x✝ ∈ {x | ∀ (i : ι), 0 < ↑(coord b i) x}
simp only [this, interior_iInter, ←
  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]
ι : 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 ≤ ↑(coord b i) x}) = ⋂ (i : ι), ↑(coord b i) ⁻¹' Ici 0
ι : Type u_1
E : Type u_2
inst✝² : Finite ι
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
b : AffineBasis ι ℝ E
h✝ : Nontrivial ι
this : FiniteDimensional ℝ E
⊢ ↑(convexHull ℝ).toOrderHom (range ↑b) = ⋂ (i : ι), ↑(coord b i) ⁻¹' Ici 0
rw [b.convexHull_eq_nonneg_coord, setOf_forall]
no goals
ι : 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 ≤ ↑(coord b i) x}) = ⋂ (i : ι), ↑(coord b i) ⁻¹' Ici 0
rfl