-- Mathlib/Analysis/Convex/Gauge.lean
theorem mem_closure_of_gauge_le_one (hc : Convex ℝ s) (hs₀ : 0 ∈ s) (ha : Absorbent ℝ s)
    (h : gauge s x ≤ 1) : x ∈ closure s

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
⊢ Tendsto (fun x_1 => x_1 • x) (𝓝[<] 1) (𝓝 x)

Tactic:
exact Filter.Tendsto.mono_left (Continuous.tendsto' (by fun_prop) _ _ (one_smul _ _))
  inf_le_left

Result:
no goals

Proof state:
case h.a
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
hr₀ : 0 ≤ r
hr₁ : r < 1
⊢ r • x ∈ {x | gauge s x < 1}

Tactic:
rw [mem_setOf_eq, gauge_smul_of_nonneg hr₀]

Result:
case h.a
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
hr₀ : 0 ≤ r
hr₁ : r < 1
⊢ r • gauge s x < 1

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
⊢ Continuous fun x_1 => x_1 • x

Tactic:
fun_prop

Result:
no goals

Proof state:
case h.a
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
hr₀ : 0 ≤ r
hr₁ : r < 1
⊢ r • gauge s x < 1

Tactic:
exact mul_lt_one_of_nonneg_of_lt_one_left hr₀ hr₁ h

Result:
no goals

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
⊢ x ∈ closure s

Tactic:
have : ∀ᶠ r : ℝ in 𝓝[<] 1, r • x ∈ s := by
  filter_upwards [Ico_mem_nhdsLT one_pos] with r ⟨hr₀, hr₁⟩
  apply gauge_lt_one_subset_self hc hs₀ ha
  rw [mem_setOf_eq, gauge_smul_of_nonneg hr₀]
  exact mul_lt_one_of_nonneg_of_lt_one_left hr₀ hr₁ h

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
⊢ x ∈ closure s

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
⊢ x ∈ closure s

Tactic:
refine mem_closure_of_tendsto ?_ this

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
this : ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s
⊢ Tendsto (fun x_1 => x_1 • x) (𝓝[<] 1) (𝓝 x)

Proof state:
case h
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
hr₀ : 0 ≤ r
hr₁ : r < 1
⊢ r • x ∈ s

Tactic:
apply gauge_lt_one_subset_self hc hs₀ ha

Result:
case h.a
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
hr₀ : 0 ≤ r
hr₁ : r < 1
⊢ r • x ∈ {x | gauge s x < 1}

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] 1, r • x ∈ s

Tactic:
filter_upwards [Ico_mem_nhdsLT one_pos] with r ⟨hr₀, hr₁⟩

Result:
case h
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
s : Set E
x : E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
hc : Convex ℝ s
hs₀ : 0 ∈ s
ha : Absorbent ℝ s
h : gauge s x ≤ 1
r : ℝ
hr₀ : 0 ≤ r
hr₁ : r < 1
⊢ r • x ∈ s