-- Mathlib/Analysis/Convex/Gauge.lean
theorem interior_subset_gauge_lt_one (s : Set E) : interior s ⊆ { x | gauge s x < 1 }

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
⊢ interior s ⊆ {x | gauge s x < 1}

Tactic:
intro x hx

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
⊢ x ∈ {x | gauge s x < 1}

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
H₂ : ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1
⊢ x ∈ {x | gauge s x < 1}

Tactic:
rcases H₂.exists with ⟨r, hxr, hr₀, hr₁⟩

Result:
case intro.intro.intro
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
H₂ : ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1
r : ℝ
hxr : x ∈ r • s
hr₀ : 0 < r
hr₁ : r < 1
⊢ x ∈ {x | gauge s x < 1}

Proof state:
case h
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
r : ℝ
h₁ : r ∈ (fun r => r⁻¹ • x) ⁻¹' s
h₂ : r ∈ Ioo 0 1
⊢ x ∈ r • s ∧ 0 < r ∧ r < 1

Tactic:
exact ⟨(mem_smul_set_iff_inv_smul_mem₀ h₂.1.ne' _ _).2 h₁, h₂⟩

Result:
no goals

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
⊢ x ∈ {x | gauge s x < 1}

Tactic:
have H₁ : Tendsto (fun r : ℝ ↦ r⁻¹ • x) (𝓝[<] 1) (𝓝 ((1 : ℝ)⁻¹ • x)) :=
  ((tendsto_id.inv₀ one_ne_zero).smul tendsto_const_nhds).mono_left inf_le_left

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 (1⁻¹ • x))
⊢ x ∈ {x | gauge s x < 1}

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
⊢ x ∈ {x | gauge s x < 1}

Tactic:
have H₂ : ∀ᶠ r in 𝓝[<] (1 : ℝ), x ∈ r • s ∧ 0 < r ∧ r < 1 := by
  filter_upwards [H₁ (mem_interior_iff_mem_nhds.1 hx), Ioo_mem_nhdsLT one_pos] with r h₁ h₂
  exact ⟨(mem_smul_set_iff_inv_smul_mem₀ h₂.1.ne' _ _).2 h₁, h₂⟩

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
H₂ : ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1
⊢ x ∈ {x | gauge s x < 1}

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
⊢ ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1

Tactic:
filter_upwards [H₁ (mem_interior_iff_mem_nhds.1 hx), Ioo_mem_nhdsLT one_pos] with r h₁ h₂

Result:
case h
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
r : ℝ
h₁ : r ∈ (fun r => r⁻¹ • x) ⁻¹' s
h₂ : r ∈ Ioo 0 1
⊢ x ∈ r • s ∧ 0 < r ∧ r < 1

Proof state:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 (1⁻¹ • x))
⊢ x ∈ {x | gauge s x < 1}

Tactic:
rw [inv_one, one_smul] at H₁

Result:
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
⊢ x ∈ {x | gauge s x < 1}

Proof state:
case intro.intro.intro
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module ℝ E
inst✝¹ : TopologicalSpace E
inst✝ : ContinuousSMul ℝ E
s : Set E
x : E
hx : x ∈ interior s
H₁ : Tendsto (fun r => r⁻¹ • x) (𝓝[<] 1) (𝓝 x)
H₂ : ∀ᶠ (r : ℝ) in 𝓝[<] 1, x ∈ r • s ∧ 0 < r ∧ r < 1
r : ℝ
hxr : x ∈ r • s
hr₀ : 0 < r
hr₁ : r < 1
⊢ x ∈ {x | gauge s x < 1}

Tactic:
exact (gauge_le_of_mem hr₀.le hxr).trans_lt hr₁

Result:
no goals