-- Mathlib/Analysis/Convex/Gauge.lean
theorem Seminorm.gauge_ball (p : Seminorm ℝ E) : gauge (p.ball 0 1) = p

Proof state:
case h.inr.refine_1.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : y ∈ p.ball 0 1
hp : {r_1 | 0 < r_1 ∧ (fun x => r • x) y ∈ r_1 • p.ball 0 1}.Nonempty
⊢ p ((fun x => r • x) y) ≤ r

Tactic:
rw [p.mem_ball_zero] at hy

Result:
case h.inr.refine_1.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : p y < 1
hp : {r_1 | 0 < r_1 ∧ (fun x => r • x) y ∈ r_1 • p.ball 0 1}.Nonempty
⊢ p ((fun x => r • x) y) ≤ r

Proof state:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
⊢ gauge (p.ball 0 1) x = p x

Tactic:
obtain hp | hp := { r : ℝ | 0 < r ∧ x ∈ r • p.ball 0 1 }.eq_empty_or_nonempty

Result:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
⊢ gauge (p.ball 0 1) x = p x

case h.inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
⊢ gauge (p.ball 0 1) x = p x

Proof state:
case h.inr.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < p x + ε
⊢ r ≤ p x + ε

Tactic:
refine hr ⟨hpε, (p x + ε)⁻¹ • x, ?_, smul_inv_smul₀ hpε.ne' _⟩

Result:
case h.inr.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < p x + ε
⊢ (p x + ε)⁻¹ • x ∈ p.ball 0 1

Proof state:
case h.inr.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < p x + ε
⊢ p x < p x + ε

Tactic:
exact lt_add_of_pos_right _ hε

Result:
no goals

Proof state:
case h.inr.refine_1.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : p y < 1
hp : {r_1 | 0 < r_1 ∧ (fun x => r • x) y ∈ r_1 • p.ball 0 1}.Nonempty
⊢ r * p y ≤ r

Tactic:
exact mul_le_of_le_one_right hr.le hy.le

Result:
no goals

Proof state:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
hpx : 0 < p x
hpx₂ : 0 < 2 * p x
⊢ False

Tactic:
refine hp.subset ⟨hpx₂, (2 * p x)⁻¹ • x, ?_, smul_inv_smul₀ hpx₂.ne' _⟩

Result:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
hpx : 0 < p x
hpx₂ : 0 < 2 * p x
⊢ (2 * p x)⁻¹ • x ∈ p.ball 0 1

Proof state:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
hpx : 0 < p x
hpx₂ : 0 < 2 * p x
⊢ p x < 2 * p x

Tactic:
exact lt_mul_of_one_lt_left hpx one_lt_two

Result:
no goals

Proof state:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
⊢ False

Tactic:
have hpx : 0 < p x := (apply_nonneg _ _).lt_of_ne h

Result:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
hpx : 0 < p x
⊢ False

Proof state:
case h.inr
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
⊢ gauge (p.ball 0 1) x = p x

Tactic:
refine IsGLB.csInf_eq ⟨fun r => ?_, fun r hr => le_of_forall_pos_le_add fun ε hε => ?_⟩ hp

Result:
case h.inr.refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
⊢ r ∈ {r | 0 < r ∧ x ∈ r • p.ball 0 1} → p x ≤ r

case h.inr.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}
ε : ℝ
hε : 0 < ε
⊢ r ≤ p x + ε

Proof state:
case h.inr.refine_1
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
⊢ r ∈ {r | 0 < r ∧ x ∈ r • p.ball 0 1} → p x ≤ r

Tactic:
rintro ⟨hr, y, hy, rfl⟩

Result:
case h.inr.refine_1.intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
r : ℝ
hr : 0 < r
y : E
hy : y ∈ p.ball 0 1
hp : {r_1 | 0 < r_1 ∧ (fun x => r • x) y ∈ r_1 • p.ball 0 1}.Nonempty
⊢ p ((fun x => r • x) y) ≤ r

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
⊢ gauge (p.ball 0 1) = ⇑p

Tactic:
ext x

Result:
case h
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
⊢ gauge (p.ball 0 1) x = p x

Proof state:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
⊢ 0 = p x

Tactic:
by_contra h

Result:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
⊢ False

Proof state:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
⊢ gauge (p.ball 0 1) x = p x

Tactic:
rw [gauge, hp, Real.sInf_empty]

Result:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
⊢ 0 = p x

Proof state:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
hpx : 0 < p x
⊢ False

Tactic:
have hpx₂ : 0 < 2 * p x := mul_pos zero_lt_two hpx

Result:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
hpx : 0 < p x
hpx₂ : 0 < 2 * p x
⊢ False

Proof state:
case h.inr.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}
ε : ℝ
hε : 0 < ε
⊢ r ≤ p x + ε

Tactic:
have hpε : 0 < p x + ε :=
  add_pos_of_nonneg_of_pos (apply_nonneg _ _) hε

Result:
case h.inr.refine_2
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1}.Nonempty
r : ℝ
hr : r ∈ lowerBounds {r | 0 < r ∧ x ∈ r • p.ball 0 1}
ε : ℝ
hε : 0 < ε
hpε : 0 < p x + ε
⊢ r ≤ p x + ε

Proof state:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
hpx : 0 < p x
hpx₂ : 0 < 2 * p x
⊢ (2 * p x)⁻¹ • x ∈ p.ball 0 1

Tactic:
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]

Result:
case h.inl
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
p : Seminorm ℝ E
x : E
hp : {r | 0 < r ∧ x ∈ r • p.ball 0 1} = ∅
h : ¬0 = p x
hpx : 0 < p x
hpx₂ : 0 < 2 * p x
⊢ p x < 2 * p x