refine s.strongInductionOn ?_
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ (convexHull 𝕜) ↑s ⊆ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ∀ (s : Finset E),
    (∀ t ⊂ s, (convexHull 𝕜) ↑t ⊆ ⋃ t_1, ⋃ (_ : t_1 ⊆ t), combiInterior 𝕜 t_1) →
      (convexHull 𝕜) ↑s ⊆ ⋃ t, ⋃ (_ : t ⊆ s), combiInterior 𝕜 t