-- Lean 4 proof step from Mathlib.Analysis.Normed.Affine.Convex (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
hs : s ∈ 𝓝 x
inr :
  ∀
    (this :
      ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
        {x : E} (hs : s ∈ 𝓝 x) (hx : x = 0),
        ∃ (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
          Membership.mem (γ := Set E)
              (interior
                ((convexHull ℝ : (a : Set E) → Set E)
                  (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
              x ∧
            (convexHull ℝ : (a : Set E) → Set E)
                (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
              s)
    (hx : ¬x = 0),
    ∃ (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
      Membership.mem (γ := Set E)
          (interior
            ((convexHull ℝ : (a : Set E) → Set E)
              (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
          x ∧
        (convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
          s
By By₁ :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E} {x : E}
    (hs : s ∈ 𝓝 x) (hx : x = 0),
    ∃ (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
      Membership.mem (γ := Set E)
          (interior
            ((convexHull ℝ : (a : Set E) → Set E)
              (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
          x ∧
        (convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
          s
By₂ :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
    (hs : Membership.mem (γ := Filter E) (𝓝 0) s),
    ∃ (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
      Membership.mem (γ := Set E)
          (interior
            ((convexHull ℝ : (a : Set E) → Set E)
              (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
          0 ∧
        (convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
          s
By₃ By₄ :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
    (hs : Membership.mem (γ := Filter E) (𝓝 0) s) (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
    ∃ (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
      Membership.mem (γ := Set E)
          (interior
            ((convexHull ℝ : (a : Set E) → Set E)
              (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
          0 ∧
        (convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
          s
By₅ By₆ :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
    (hs : Membership.mem (γ := Filter E) (𝓝 0) s) (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
    let c :=
      HVAdd.hVAdd (α := E)
        (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b;
    ∀
      (hc₀ :
        Membership.mem (γ := Set E)
          (interior
            ((convexHull ℝ : (a : Set E) → Set E)
              (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
          0),
      ∃ (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
        Membership.mem (γ := Set E)
            (interior
              ((convexHull ℝ : (a : Set E) → Set E)
                (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
            0 ∧
          (convexHull ℝ : (a : Set E) → Set E)
              (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
            s
By₇ :
  ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
    (hs : Membership.mem (γ := Filter E) (𝓝 0) s) (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
    let c :=
      HVAdd.hVAdd (α := E)
        (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b;
    ∀
      (hc₀ :
        Membership.mem (γ := Set E)
          (interior
            ((convexHull ℝ : (a : Set E) → Set E)
              (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
          0),
      let cnorm : ℝ :=
        Finset.sup' Finset.univ ⋯ fun (i : Fin (finrank ℝ E + 1)) ↦
          norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E);
      ∀
        (hcnorm :
          Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
            (closedBall 0 (cnorm + 1))),
        ∃ (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
          Membership.mem (γ := Set E)
              (interior
                ((convexHull ℝ : (a : Set E) → Set E)
                  (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
              0 ∧
            (convexHull ℝ : (a : Set E) → Set E)
                (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
              s
⊢ ∃ (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
    Membership.mem (γ := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
        x ∧
      (convexHull ℝ : (a : Set E) → Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
        s
have By₈ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  (hs : Membership.mem (γ := Filter E) (𝓝 0) s) (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
  let c :=
    HVAdd.hVAdd (α := E)
      (-Finset.centroid ℝ (ι := Fin (finrank ℝ E + 1)) Finset.univ (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) b;
  ∀
    (hc₀ :
      Membership.mem (γ := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))))
        0),
    let cnorm : ℝ :=
      Finset.sup' Finset.univ sorry fun (i : Fin (finrank ℝ E + 1)) ↦
        norm (E := E) ((c : (a : Fin (finrank ℝ E + 1)) → E) i : E);
    ∀
      (hcnorm :
        Subset (α := Set E) (range (ι := Fin (finrank ℝ E + 1)) (⇑c : (a : Fin (finrank ℝ E + 1)) → E))
          (closedBall 0 (cnorm + 1)))
      (ε : ℝ) (hε : ε > 0) (hεs : ball 0 ε ⊆ s),
      ∃ (b : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E),
        Membership.mem (γ := Set E)
            (interior
              ((convexHull ℝ : (a : Set E) → Set E)
                (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E))))
            0 ∧
          (convexHull ℝ : (a : Set E) → Set E)
              (range (ι := Fin (finrank ℝ E + 1)) (⇑b : (a : Fin (finrank ℝ E + 1)) → E)) ⊆
            s
Tactic: classical
  -- By translating, WLOG `x` is the origin.
  wlog hx : x = 0
  · obtain ⟨b, hb⟩ := this (s := -x +ᵥ s) (by simpa using vadd_mem_nhds_vadd (-x) hs) rfl
    use x +ᵥ b
    simpa [subset_vadd_set_iff, mem_vadd_set_iff_neg_vadd_mem, convexHull_vadd, interior_vadd,
      Pi.vadd_def, -vadd_eq_add, vadd_eq_add (a := -x), ← Set.vadd_set_range] using hb
  subst hx
  -- The strategy is now to find an arbitrary maximal spanning simplex (aka an affine basis)...
  obtain ⟨b⟩ := exists_affineBasis_of_finiteDimensional
    (ι := Fin (finrank ℝ E + 1)) (k := ℝ) (P := E) (by simp)
  -- ... translate it to contain the origin...
  set c : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := -Finset.univ.centroid ℝ b +ᵥ b
  have hc₀ : 0 ∈ interior (convexHull ℝ (range c) : Set E) := by
    simpa [c, convexHull_vadd, interior_vadd, range_add, Pi.vadd_def, mem_vadd_set_iff_neg_vadd_mem]
      using b.centroid_mem_interior_convexHull
  set cnorm := Finset.univ.sup' Finset.univ_nonempty (fun i ↦ ‖c i‖)
  have hcnorm : range c ⊆ closedBall 0 (cnorm + 1) := by
    simpa only [cnorm, subset_def, Finset.mem_coe, mem_closedBall, dist_zero_right,
      ← sub_le_iff_le_add, Finset.le_sup'_iff, forall_mem_range] using fun i ↦ ⟨i, by simp⟩
  -- ... and finally scale it to fit inside the neighborhood `s`.
  obtain ⟨ε, hε, hεs⟩ := Metric.mem_nhds_iff.1 hs
  set ε' : ℝ := ε / 2 / (cnorm + 1)
  have hc' : 0 < cnorm + 1 := by
    have : 0 ≤ cnorm := Finset.le_sup'_of_le _ (Finset.mem_univ 0) (norm_nonneg _)
    positivity
  have hε' : 0 < ε' := by positivity
  set d : AffineBasis (Fin (finrank ℝ E + 1)) ℝ E := Units.mk0 ε' hε'.ne' • c
  have hε₀ : 0 < ε / 2 := by positivity
  have hdnorm : (range d : Set E) ⊆ closedBall 0 (ε / 2) := by
    simp [d, abs_of_nonneg hε'.le, range_subset_iff, norm_smul]
    simpa [ε', hε₀.ne', range_subset_iff, ← mul_div_right_comm (ε / 2), div_le_iff₀ hc', hε₀]
      using hcnorm
  refine ⟨d, ?_, ?_⟩
  · simpa [d, Pi.smul_def, range_smul, interior_smul₀, convexHull_smul, zero_mem_smul_set_iff,
      hε'.ne']
  · calc
      convexHull ℝ (range d) ⊆ closedBall 0 (ε / 2) := convexHull_min hdnorm (convex_closedBall ..)
      _ ⊆ ball 0 ε := closedBall_subset_ball (by linarith)
      _ ⊆ s := hεs
Cleared hypotheses: inst_2, hs