case h
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
⊢ gauge (ball p 0 1) x = ↑p x
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
⊢ gauge (ball p 0 1) = ↑p
ext x
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
⊢ gauge (ball p 0 1) x = ↑p x

case h.inr
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : Set.Nonempty {r | 0 < r ∧ x ∈ r • ball p 0 1}
⊢ gauge (ball p 0 1) x = ↑p x
case h
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
⊢ gauge (ball p 0 1) x = ↑p x
obtain hp | hp := { r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1 }.eq_empty_or_nonempty
case h.inr.refine'_1
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : Set.Nonempty {r | 0 < r ∧ x ∈ r • ball p 0 1}
r : ℝ
⊢ r ∈ {r | 0 < r ∧ x ∈ r • ball p 0 1} → ↑p x ≤ r

case h.inr.refine'_2
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : Set.Nonempty {r | 0 < r ∧ x ∈ r • ball p 0 1}
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • ball p 0 1}
ε : ℝ
hε : 0 < ε
⊢ r ≤ ↑p x + ε
case h.inr
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : Set.Nonempty {r | 0 < r ∧ x ∈ r • ball p 0 1}
⊢ gauge (ball p 0 1) x = ↑p x
refine' IsGLB.csInf_eq ⟨fun r => _, fun r hr => le_of_forall_pos_le_add fun ε hε => _⟩ hp
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
⊢ 0 = ↑p x
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
⊢ gauge (ball p 0 1) x = ↑p x
rw [gauge, hp, Real.sInf_empty]
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
h : ¬0 = ↑p x
⊢ False
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
⊢ 0 = ↑p x
by_contra h
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
h : ¬0 = ↑p x
hpx : 0 < ↑p x
⊢ False
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
h : ¬0 = ↑p x
⊢ False
have hpx : 0 < p x := (map_nonneg _ _).lt_of_ne h
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
h : ¬0 = ↑p x
hpx : 0 < ↑p x
hpx₂ : 0 < 2 * ↑p x
⊢ False
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
h : ¬0 = ↑p x
hpx : 0 < ↑p x
⊢ False
have hpx₂ : 0 < 2 * p x := mul_pos zero_lt_two hpx
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
h : ¬0 = ↑p x
hpx : 0 < ↑p x
hpx₂ : 0 < 2 * ↑p x
⊢ (2 * ↑p x)⁻¹ • x ∈ ball p 0 1
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
h : ¬0 = ↑p x
hpx : 0 < ↑p x
hpx₂ : 0 < 2 * ↑p x
⊢ False
refine' hp.subset ⟨hpx₂, (2 * p x)⁻¹ • x, _, smul_inv_smul₀ hpx₂.ne' _⟩
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
h : ¬0 = ↑p x
hpx : 0 < ↑p x
hpx₂ : 0 < 2 * ↑p x
⊢ ↑p x < 2 * ↑p x
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
h : ¬0 = ↑p x
hpx : 0 < ↑p x
hpx₂ : 0 < 2 * ↑p x
⊢ (2 * ↑p x)⁻¹ • x ∈ ball p 0 1
rw [p.mem_ball_zero, map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hpx₂),
  inv_mul_lt_iff hpx₂, mul_one]
no goals
case h.inl
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • ball p 0 1} = ∅
h : ¬0 = ↑p x
hpx : 0 < ↑p x
hpx₂ : 0 < 2 * ↑p x
⊢ ↑p x < 2 * ↑p x
exact lt_mul_of_one_lt_left hpx one_lt_two
case h.inr.refine'_1.intro.intro.intro
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : y ∈ ball p 0 1
hp : Set.Nonempty {r_1 | 0 < r_1 ∧ (fun x => r • x) y ∈ r_1 • ball p 0 1}
⊢ ↑p ((fun x => r • x) y) ≤ r
case h.inr.refine'_1
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : Set.Nonempty {r | 0 < r ∧ x ∈ r • ball p 0 1}
r : ℝ
⊢ r ∈ {r | 0 < r ∧ x ∈ r • ball p 0 1} → ↑p x ≤ r
rintro ⟨hr, y, hy, rfl⟩
case h.inr.refine'_1.intro.intro.intro
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : ↑p y < 1
hp : Set.Nonempty {r_1 | 0 < r_1 ∧ (fun x => r • x) y ∈ r_1 • ball p 0 1}
⊢ ↑p ((fun x => r • x) y) ≤ r
case h.inr.refine'_1.intro.intro.intro
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : y ∈ ball p 0 1
hp : Set.Nonempty {r_1 | 0 < r_1 ∧ (fun x => r • x) y ∈ r_1 • ball p 0 1}
⊢ ↑p ((fun x => r • x) y) ≤ r
rw [p.mem_ball_zero] at hy
case h.inr.refine'_1.intro.intro.intro
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : ↑p y < 1
hp : Set.Nonempty {r_1 | 0 < r_1 ∧ (fun x => r • x) y ∈ r_1 • ball p 0 1}
⊢ r * ↑p y ≤ r
case h.inr.refine'_1.intro.intro.intro
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : ↑p y < 1
hp : Set.Nonempty {r_1 | 0 < r_1 ∧ (fun x => r • x) y ∈ r_1 • ball p 0 1}
⊢ ↑p ((fun x => r • x) y) ≤ r
rw [map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos hr]
no goals
case h.inr.refine'_1.intro.intro.intro
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : ↑p y < 1
hp : Set.Nonempty {r_1 | 0 < r_1 ∧ (fun x => r • x) y ∈ r_1 • ball p 0 1}
⊢ r * ↑p y ≤ r
exact mul_le_of_le_one_right hr.le hy.le
case h.inr.refine'_2
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : Set.Nonempty {r | 0 < r ∧ x ∈ r • ball p 0 1}
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • ball p 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < ↑p x + ε
⊢ r ≤ ↑p x + ε
case h.inr.refine'_2
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : Set.Nonempty {r | 0 < r ∧ x ∈ r • ball p 0 1}
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • ball p 0 1}
ε : ℝ
hε : 0 < ε
⊢ r ≤ ↑p x + ε
have hpε : 0 < p x + ε :=
  add_pos_of_nonneg_of_pos (map_nonneg _ _) hε
case h.inr.refine'_2
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : Set.Nonempty {r | 0 < r ∧ x ∈ r • ball p 0 1}
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • ball p 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < ↑p x + ε
⊢ (↑p x + ε)⁻¹ • x ∈ ball p 0 1
case h.inr.refine'_2
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : Set.Nonempty {r | 0 < r ∧ x ∈ r • ball p 0 1}
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • ball p 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < ↑p x + ε
⊢ r ≤ ↑p x + ε
refine' hr ⟨hpε, (p x + ε)⁻¹ • x, _, smul_inv_smul₀ hpε.ne' _⟩
case h.inr.refine'_2
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : Set.Nonempty {r | 0 < r ∧ x ∈ r • ball p 0 1}
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • ball p 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < ↑p x + ε
⊢ ↑p x < ↑p x + ε
case h.inr.refine'_2
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : Set.Nonempty {r | 0 < r ∧ x ∈ r • ball p 0 1}
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • ball p 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < ↑p x + ε
⊢ (↑p x + ε)⁻¹ • x ∈ ball p 0 1
rw [p.mem_ball_zero, map_smul_eq_mul, Real.norm_eq_abs, abs_of_pos (inv_pos.2 hpε),
  inv_mul_lt_iff hpε, mul_one]
no goals
case h.inr.refine'_2
𝕜 : Type ?u.260696
E : Type u_1
F : Type ?u.260702
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s t : Set E
a : ℝ
p : Seminorm ℝ E
x : E
hp : Set.Nonempty {r | 0 < r ∧ x ∈ r • ball p 0 1}
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • ball p 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < ↑p x + ε
⊢ ↑p x < ↑p x + ε
exact lt_add_of_pos_right _ hε