case intro.intro.intro
𝕜 : Type ?u.17621
E : Type u_1
F : Type ?u.17627
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
absorbs : Absorbent ℝ s
h : gauge s x < a
b : ℝ
hba : b < a
hb : 0 < b
hx : x ∈ b • s
⊢ ∃ b, 0 < b ∧ b < a ∧ x ∈ b • s
𝕜 : Type ?u.17621
E : Type u_1
F : Type ?u.17627
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
absorbs : Absorbent ℝ s
h : gauge s x < a
⊢ ∃ b, 0 < b ∧ b < a ∧ x ∈ b • s
obtain ⟨b, ⟨hb, hx⟩, hba⟩ := exists_lt_of_csInf_lt absorbs.gauge_set_nonempty h
no goals
case intro.intro.intro
𝕜 : Type ?u.17621
E : Type u_1
F : Type ?u.17627
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
x : E
absorbs : Absorbent ℝ s
h : gauge s x < a
b : ℝ
hba : b < a
hb : 0 < b
hx : x ∈ b • s
⊢ ∃ b, 0 < b ∧ b < a ∧ x ∈ b • s
exact ⟨b, hb, hba, hx⟩