case h
𝕜 : Type ?u.66870
E : Type u_1
F : Type ?u.66876
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ x✝ ∈ {x | gauge s x < a} ↔ x✝ ∈ ⋃ (r : ℝ) (_ : r ∈ Ioo 0 a), r • s
𝕜 : Type ?u.66870
E : Type u_1
F : Type ?u.66876
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
absorbs : Absorbent ℝ s
a : ℝ
⊢ {x | gauge s x < a} = ⋃ (r : ℝ) (_ : r ∈ Ioo 0 a), r • s
ext
case h
𝕜 : Type ?u.66870
E : Type u_1
F : Type ?u.66876
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ gauge s x✝ < a ↔ ∃ i, 0 < i ∧ i < a ∧ x✝ ∈ i • s
case h
𝕜 : Type ?u.66870
E : Type u_1
F : Type ?u.66876
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ x✝ ∈ {x | gauge s x < a} ↔ x✝ ∈ ⋃ (r : ℝ) (_ : r ∈ Ioo 0 a), r • s
simp_rw [mem_setOf, mem_iUnion, exists_prop, mem_Ioo, and_assoc]
no goals
case h
𝕜 : Type ?u.66870
E : Type u_1
F : Type ?u.66876
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a✝ : ℝ
absorbs : Absorbent ℝ s
a : ℝ
x✝ : E
⊢ gauge s x✝ < a ↔ ∃ i, 0 < i ∧ i < a ∧ x✝ ∈ i • s
exact
  ⟨exists_lt_of_gauge_lt absorbs, fun ⟨r, hr₀, hr₁, hx⟩ =>
    (gauge_le_of_mem hr₀.le hx).trans_lt hr₁⟩