-- Module: Mathlib.Analysis.Normed.Affine.Convex
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s t : Set E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht : t ∈ 𝓝ˢ s
rcases :
  ∀ (U : Set E) (hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (hU₂ : s ⊆ U) (hU₃ : U ⊆ t),
    ∃ (u : Finset E),
      s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
        (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
rcases₁ :
  ∀ (U : Set E) (hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (hU₂ : s ⊆ U) (hU₃ : U ⊆ t)
    (V : Set E) (hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V) (hV₂ : V + s ⊆ U),
    ∃ (u : Finset E),
      s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
        (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
rcases₂ :
  ∀ (U : Set E) (hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (hU₂ : s ⊆ U) (hU₃ : U ⊆ t)
    (V : Set E) (hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V) (hV₂ : V + s ⊆ U)
    (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E)
    (hb₁ :
      Membership.mem (γ := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        0)
    (hb₂ :
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        V),
    ∃ (u : Finset E),
      s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
        (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
rcases₃ :
  ∀ (U : Set E) (hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (hU₂ : s ⊆ U) (hU₃ : U ⊆ t)
    (V : Set E) (hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V) (hV₂ : V + s ⊆ U)
    (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E)
    (hb₁ :
      Membership.mem (γ := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        0)
    (hb₂ :
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        V)
    (u : Set E) (hu₁ : u ⊆ s) (hu₂ : u.Finite)
    (hu₃ :
      s ⊆
        ⋃ i ∈ u,
          HAdd.hAdd (α := Set E)
            (interior
              ((convexHull ℝ : (a : Set E) → Set E)
                (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
            {i}),
    ∃ (u : Finset E),
      s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
        (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
rcases₄ :
  ∀ (U : Set E) (hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (hU₂ : s ⊆ U) (hU₃ : U ⊆ t)
    (V : Set E) (hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V) (hV₂ : V + s ⊆ U)
    (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E)
    (hb₁ :
      Membership.mem (γ := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        0)
    (hb₂ :
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        V)
    (u : Finset E) (hu₁ : (↑u : Set E) ⊆ s)
    (hu₃ :
      s ⊆
        ⋃ i ∈ (↑u : Set E),
          HAdd.hAdd (α := Set E)
            (interior
              ((convexHull ℝ : (a : Set E) → Set E)
                (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
            {i}),
    ∃ (u : Finset E),
      s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
        (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t
refine_1 :
  ∀ (U : Set E) (hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (hU₂ : s ⊆ U) (hU₃ : U ⊆ t)
    (V : Set E) (hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V) (hV₂ : V + s ⊆ U)
    (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E)
    (hb₁ :
      Membership.mem (γ := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        0)
    (hb₂ :
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        V)
    (u : Finset E) (hu₁ : (↑u : Set E) ⊆ s)
    (hu₃ :
      s ⊆
        ⋃ i ∈ (↑u : Set E),
          HAdd.hAdd (α := Set E)
            (interior
              ((convexHull ℝ : (a : Set E) → Set E)
                (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
            {i}),
    s ⊆
      interior
        ((convexHull ℝ : (a : Set E) → Set E)
          (↑(Finset.image (α := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E) Finset.univ + u) : Set E))
refine_2 :
  ∀ (U : Set E) (hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (hU₂ : s ⊆ U) (hU₃ : U ⊆ t)
    (V : Set E) (hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V) (hV₂ : V + s ⊆ U)
    (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E)
    (hb₁ :
      Membership.mem (γ := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        0)
    (hb₂ :
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        V)
    (u : Finset E) (hu₁ : (↑u : Set E) ⊆ s)
    (hu₃ :
      s ⊆
        ⋃ i ∈ (↑u : Set E),
          HAdd.hAdd (α := Set E)
            (interior
              ((convexHull ℝ : (a : Set E) → Set E)
                (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
            {i}),
    (convexHull ℝ : (a : Set E) → Set E)
        (↑(Finset.image (α := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E) Finset.univ + u) : Set E) ⊆
      t
refine_1₁ :
  ∀ (U : Set E) (hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (hU₂ : s ⊆ U) (hU₃ : U ⊆ t)
    (V : Set E) (hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V) (hV₂ : V + s ⊆ U)
    (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E)
    (hb₁ :
      Membership.mem (γ := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        0)
    (hb₂ :
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        V)
    (u : Finset E) (hu₁ : (↑u : Set E) ⊆ s)
    (hu₃ :
      s ⊆
        ⋃ i ∈ (↑u : Set E),
          HAdd.hAdd (α := Set E)
            (interior
              ((convexHull ℝ : (a : Set E) → Set E)
                (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
            {i}),
    s ⊆
      interior
        (HAdd.hAdd (α := Set E) (β := Set E)
          ((convexHull ℝ : (a : Set E) → Set E)
              (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) :
            Set E)
          ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) : Set E))
refine_2₁ refine_2₂ :
  ∀ (U : Set E) (hU₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U) (hU₂ : s ⊆ U) (hU₃ : U ⊆ t)
    (V : Set E) (hV₁ : Membership.mem (γ := Filter E) (𝓝 0) V) (hV₂ : V + s ⊆ U)
    (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E)
    (hb₁ :
      Membership.mem (γ := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        0)
    (hb₂ :
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        V)
    (u : Finset E) (hu₁ : (↑u : Set E) ⊆ s)
    (hu₃ :
      s ⊆
        ⋃ i ∈ (↑u : Set E),
          HAdd.hAdd (α := Set E)
            (interior
              ((convexHull ℝ : (a : Set E) → Set E)
                (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
            {i}),
    HAdd.hAdd (α := Set E) (β := Set E)
        ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) :
          Set E)
        ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) : Set E) ⊆
      t
⊢ ∃ (u : Finset E),
    s ⊆ interior ((convexHull ℝ : (a : Set E) → Set E) (↑u : Set E)) ∧
      (convexHull ℝ : (a : Set E) → Set E) (↑u : Set E) ⊆ t

Tactic:
classical
  rcases mem_nhdsSet_iff_exists.1 ht with ⟨U, hU₁, hU₂, hU₃⟩
  rcases compact_open_separated_add_left hs₂ hU₁ hU₂ with ⟨V, hV₁, hV₂⟩
  rcases exists_mem_interior_convexHull_affineBasis hV₁ with ⟨b, hb₁, hb₂⟩
  rcases hs₂.elim_finite_subcover_image (b := s)
      (c := fun x => interior (convexHull ℝ (Set.range b)) + {x})
      (fun _ _ => isOpen_interior.add_right)
      (fun x hx => Set.mem_iUnion₂_of_mem hx <| by simpa using hb₁)
    with ⟨u, hu₁, hu₂, hu₃⟩
  lift u to Finset E using hu₂
  refine ⟨Finset.univ.image b + u, ?_, ?_⟩
  all_goals rw [Finset.coe_add, Finset.coe_image, Finset.coe_univ, Set.image_univ, convexHull_add]
  · grw [hu₃, ← subset_interior_add_left, Set.iUnion₂_subset_iff, ← subset_convexHull _ (u : Set E)]
    intros
    gcongr
    simpa
  · grw [hu₁, hs₁.convexHull_eq, hb₂, hV₂, hU₃]

Premises used: Set.image_univ, Finset.coe_univ, Finset, subset_interior_add_left, convexHull_add, Finset.coe_image, mem_nhdsSet_iff_exists, Iff.mp, Convex.convexHull_eq, Finset.coe_add, Set.iUnion₂_subset_iff