-- Mathlib/Analysis/Convex/Gauge.lean
theorem comap_gauge_nhds_zero_le (ha : Absorbent ℝ s) (hb : Bornology.IsVonNBounded ℝ s) :
    comap (gauge s) (𝓝 0) ≤ 𝓝 0 := fun u hu ↦ by
  rcases (hb hu).exists_pos with ⟨r, hr₀, hr⟩
  filter_upwards [preimage_mem_comap (gt_mem_nhds (inv_pos.2 hr₀))] with x (hx : gauge s x < r⁻¹)
  rcases exists_lt_of_gauge_lt ha hx with ⟨c, hc₀, hcr, y, hy, rfl⟩
  have hrc := (lt_inv_comm₀ hr₀ hc₀).2 hcr
  rcases hr c⁻¹ (hrc.le.trans (le_abs_self _)) hy with ⟨z, hz, rfl⟩
  simpa only [smul_inv_smul₀ hc₀.ne']

Proof state:
case intro.intro
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
⊢ u ∈ comap (gauge s) (𝓝 0)

Tactic:
filter_upwards [preimage_mem_comap (gt_mem_nhds (inv_pos.2 hr₀))] with x (hx : gauge s x < r⁻¹)

Result:
case h
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
x : E
hx : gauge s x < r⁻¹
⊢ x ∈ u

Proof state:
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
⊢ u ∈ comap (gauge s) (𝓝 0)

Tactic:
rcases (hb hu).exists_pos with ⟨r, hr₀, hr⟩

Result:
case intro.intro
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
⊢ u ∈ comap (gauge s) (𝓝 0)

Proof state:
case h.intro.intro.intro.intro.intro.intro.intro
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
hrc : r < c⁻¹
z : E
hz : z ∈ u
hy : (fun x => c⁻¹ • x) z ∈ s
hx : gauge s ((fun x => c • x) ((fun x => c⁻¹ • x) z)) < r⁻¹
⊢ (fun x => c • x) ((fun x => c⁻¹ • x) z) ∈ u

Tactic:
simpa only [smul_inv_smul₀ hc₀.ne']

Result:
no goals

Proof state:
case h
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
x : E
hx : gauge s x < r⁻¹
⊢ x ∈ u

Tactic:
rcases exists_lt_of_gauge_lt ha hx with ⟨c, hc₀, hcr, y, hy, rfl⟩

Result:
case h.intro.intro.intro.intro.intro
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
y : E
hy : y ∈ s
hx : gauge s ((fun x => c • x) y) < r⁻¹
⊢ (fun x => c • x) y ∈ u

Proof state:
case h.intro.intro.intro.intro.intro
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
y : E
hy : y ∈ s
hx : gauge s ((fun x => c • x) y) < r⁻¹
⊢ (fun x => c • x) y ∈ u

Tactic:
have hrc := (lt_inv_comm₀ hr₀ hc₀).2 hcr

Result:
case h.intro.intro.intro.intro.intro
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
y : E
hy : y ∈ s
hx : gauge s ((fun x => c • x) y) < r⁻¹
hrc : r < c⁻¹
⊢ (fun x => c • x) y ∈ u

Proof state:
case h.intro.intro.intro.intro.intro
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
y : E
hy : y ∈ s
hx : gauge s ((fun x => c • x) y) < r⁻¹
hrc : r < c⁻¹
⊢ (fun x => c • x) y ∈ u

Tactic:
rcases hr c⁻¹ (hrc.le.trans (le_abs_self _)) hy with ⟨z, hz, rfl⟩

Result:
case h.intro.intro.intro.intro.intro.intro.intro
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
s : Set E
inst✝ : TopologicalSpace E
ha : Absorbent ℝ s
hb : Bornology.IsVonNBounded ℝ s
u : Set E
hu : u ∈ 𝓝 0
r : ℝ
hr₀ : r > 0
hr : ∀ (c : ℝ), r ≤ ‖c‖ → s ⊆ c • u
c : ℝ
hc₀ : 0 < c
hcr : c < r⁻¹
hrc : r < c⁻¹
z : E
hz : z ∈ u
hy : (fun x => c⁻¹ • x) z ∈ s
hx : gauge s ((fun x => c • x) ((fun x => c⁻¹ • x) z)) < r⁻¹
⊢ (fun x => c • x) ((fun x => c⁻¹ • x) z) ∈ u