-- Mathlib/Analysis/Convex/Body.lean
theorem iInter_smul_eq_self [T2Space V] {u : ℕ → ℝ≥0} (K : ConvexBody V) (h_zero : 0 ∈ K)
    (hu : Tendsto u atTop (𝓝 0)) :
    ⋂ n : ℕ, (1 + (u n : ℝ)) • (K : Set V) = K

Proof state:
case h.refine_1.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
y : V
hyK : y ∈ ↑K
h : (1 + ↑(u n)) • y ∈ ⋂ n, (1 + ↑(u n)) • ↑K
hn : ‖↑(u n) - ↑0‖ < ε / C
⊢ |↑(u n)| * ‖y‖ < ε

Tactic:
rw [lt_div_iff₀' hC_pos, mul_comm, NNReal.coe_zero, sub_zero, Real.norm_eq_abs] at hn

Result:
case h.refine_1.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
y : V
hyK : y ∈ ↑K
h : (1 + ↑(u n)) • y ∈ ⋂ n, (1 + ↑(u n)) • ↑K
hn : |↑(u n)| * C < ε
⊢ |↑(u n)| * ‖y‖ < ε

Proof state:
case h.refine_1.intro.intro.intro
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
x : V
h : x ∈ ⋂ n, (1 + ↑(u n)) • ↑K
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖↑(u n_1) - ↑0‖ < ε / C
⊢ ∃ b ∈ ↑K, ‖x - b‖ < ε

Tactic:
obtain ⟨y, hyK, rfl⟩ := Set.mem_smul_set.mp (Set.mem_iInter.mp h n)

Result:
case h.refine_1.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖↑(u n_1) - ↑0‖ < ε / C
y : V
hyK : y ∈ ↑K
h : (1 + ↑(u n)) • y ∈ ⋂ n, (1 + ↑(u n)) • ↑K
⊢ ∃ b ∈ ↑K, ‖(1 + ↑(u n)) • y - b‖ < ε

Proof state:
case h.refine_1.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖↑(u n_1) - ↑0‖ < ε / C
y : V
hyK : y ∈ ↑K
h : (1 + ↑(u n)) • y ∈ ⋂ n, (1 + ↑(u n)) • ↑K
⊢ ∃ b ∈ ↑K, ‖(1 + ↑(u n)) • y - b‖ < ε

Tactic:
refine ⟨y, hyK, ?_⟩

Result:
case h.refine_1.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
hn : ∀ (n_1 : ℕ), n ≤ n_1 → ‖↑(u n_1) - ↑0‖ < ε / C
y : V
hyK : y ∈ ↑K
h : (1 + ↑(u n)) • y ∈ ⋂ n, (1 + ↑(u n)) • ↑K
⊢ ‖(1 + ↑(u n)) • y - y‖ < ε

Proof state:
case h.refine_1.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
y : V
hyK : y ∈ ↑K
h : (1 + ↑(u n)) • y ∈ ⋂ n, (1 + ↑(u n)) • ↑K
hn : |↑(u n)| * C < ε
⊢ |↑(u n)| * ‖y‖ < ε

Tactic:
refine lt_of_le_of_lt ?_ hn

Result:
case h.refine_1.intro.intro.intro.intro.intro
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
n : ℕ
y : V
hyK : y ∈ ↑K
h : (1 + ↑(u n)) • y ∈ ⋂ n, (1 + ↑(u n)) • ↑K
hn : |↑(u n)| * C < ε
⊢ |↑(u n)| * ‖y‖ ≤ |↑(u n)| * C

Proof state:
case h.refine_2
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : x ∈ ↑K
⊢ x ∈ ⋂ n, (1 + ↑(u n)) • ↑K

Tactic:
refine Set.mem_iInter.mpr (fun n => Convex.mem_smul_of_zero_mem K.convex h_zero h ?_)

Result:
case h.refine_2
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : x ∈ ↑K
n : ℕ
⊢ 1 ≤ 1 + ↑(u n)

Proof state:
case h.refine_2
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : Tendsto u atTop (𝓝 0)
x : V
h : x ∈ ↑K
n : ℕ
⊢ 1 ≤ 1 + ↑(u n)

Tactic:
exact le_add_of_nonneg_right (by positivity)

Result:
no goals

Proof state:
case h.refine_1.intro.intro
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
x : V
h : x ∈ ⋂ n, (1 + ↑(u n)) • ↑K
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
⊢ ∀ (ε : ℝ), 0 < ε → ∃ b ∈ ↑K, ‖x - b‖ < ε

Tactic:
intro ε hε

Result:
case h.refine_1.intro.intro
V : Type u_1
inst✝² : SeminormedAddCommGroup V
inst✝¹ : NormedSpace ℝ V
inst✝ : T2Space V
u : ℕ → ℝ≥0
K : ConvexBody V
h_zero : 0 ∈ K
hu : ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ), N ≤ n → ‖↑(u n) - ↑0‖ < ε
x : V
h : x ∈ ⋂ n, (1 + ↑(u n)) • ↑K
C : ℝ
hC_pos : C > 0
hC_bdd : ∀ x ∈ ↑K, ‖x‖ ≤ C
ε : ℝ
hε : 0 < ε
⊢ ∃ b ∈ ↑K, ‖x - b‖ < ε