[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e e₁ e₂ : ENorm 𝕜 V
h : ↑e₁ = ↑e₂
⊢ e₁ = e₂
[PROOFSTEP]
cases e₁
[GOAL]
case mk
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e e₂ : ENorm 𝕜 V
toFun✝ : V → ℝ≥0∞
eq_zero'✝ : ∀ (x : V), toFun✝ x = 0 → x = 0
map_add_le'✝ : ∀ (x y : V), toFun✝ (x + y) ≤ toFun✝ x + toFun✝ y
map_smul_le'✝ : ∀ (c : 𝕜) (x : V), toFun✝ (c • x) ≤ ↑‖c‖₊ * toFun✝ x
h : ↑{ toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ } = ↑e₂
⊢ { toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ } = e₂
[PROOFSTEP]
cases e₂
[GOAL]
case mk.mk
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
toFun✝¹ : V → ℝ≥0∞
eq_zero'✝¹ : ∀ (x : V), toFun✝¹ x = 0 → x = 0
map_add_le'✝¹ : ∀ (x y : V), toFun✝¹ (x + y) ≤ toFun✝¹ x + toFun✝¹ y
map_smul_le'✝¹ : ∀ (c : 𝕜) (x : V), toFun✝¹ (c • x) ≤ ↑‖c‖₊ * toFun✝¹ x
toFun✝ : V → ℝ≥0∞
eq_zero'✝ : ∀ (x : V), toFun✝ x = 0 → x = 0
map_add_le'✝ : ∀ (x y : V), toFun✝ (x + y) ≤ toFun✝ x + toFun✝ y
map_smul_le'✝ : ∀ (c : 𝕜) (x : V), toFun✝ (c • x) ≤ ↑‖c‖₊ * toFun✝ x
h :
  ↑{ toFun := toFun✝¹, eq_zero' := eq_zero'✝¹, map_add_le' := map_add_le'✝¹, map_smul_le' := map_smul_le'✝¹ } =
    ↑{ toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ }
⊢ { toFun := toFun✝¹, eq_zero' := eq_zero'✝¹, map_add_le' := map_add_le'✝¹, map_smul_le' := map_smul_le'✝¹ } =
    { toFun := toFun✝, eq_zero' := eq_zero'✝, map_add_le' := map_add_le'✝, map_smul_le' := map_smul_le'✝ }
[PROOFSTEP]
congr
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
⊢ ↑e (c • x) = ↑‖c‖₊ * ↑e x
[PROOFSTEP]
apply le_antisymm (e.map_smul_le' c x)
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
⊢ ↑‖c‖₊ * ↑e x ≤ ↑e (c • x)
[PROOFSTEP]
by_cases hc : c = 0
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hc : c = 0
⊢ ↑‖c‖₊ * ↑e x ≤ ↑e (c • x)
[PROOFSTEP]
simp [hc]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ↑‖c‖₊ * ↑e x ≤ ↑e (c • x)
[PROOFSTEP]
calc
  (‖c‖₊ : ℝ≥0∞) * e x = ‖c‖₊ * e (c⁻¹ • c • x) := by rw [inv_smul_smul₀ hc]
  _ ≤ ‖c‖₊ * (‖c⁻¹‖₊ * e (c • x)) := (mul_le_mul_left' (e.map_smul_le' _ _) _)
  _ = e (c • x) := by
    rw [← mul_assoc, nnnorm_inv, ENNReal.coe_inv, ENNReal.mul_inv_cancel _ ENNReal.coe_ne_top, one_mul] <;> simp [hc]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ↑‖c‖₊ * ↑e x = ↑‖c‖₊ * ↑e (c⁻¹ • c • x)
[PROOFSTEP]
rw [inv_smul_smul₀ hc]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ↑‖c‖₊ * (↑‖c⁻¹‖₊ * ↑e (c • x)) = ↑e (c • x)
[PROOFSTEP]
rw [← mul_assoc, nnnorm_inv, ENNReal.coe_inv, ENNReal.mul_inv_cancel _ ENNReal.coe_ne_top, one_mul]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ↑‖c‖₊ ≠ 0
[PROOFSTEP]
simp [hc]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hc : ¬c = 0
⊢ ‖c‖₊ ≠ 0
[PROOFSTEP]
simp [hc]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
⊢ ↑e 0 = 0
[PROOFSTEP]
rw [← zero_smul 𝕜 (0 : V), e.map_smul]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
⊢ ↑‖0‖₊ * ↑e 0 = 0
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
⊢ ↑e (-x) = ↑‖-1‖₊ * ↑e x
[PROOFSTEP]
rw [← map_smul, neg_one_smul]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
⊢ ↑‖-1‖₊ * ↑e x = ↑e x
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ ↑e (x - y) = ↑e (y - x)
[PROOFSTEP]
rw [← neg_sub, e.map_neg]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ ↑e (x - y) = ↑e (x + -y)
[PROOFSTEP]
rw [sub_eq_add_neg]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ ↑e x + ↑e (-y) = ↑e x + ↑e y
[PROOFSTEP]
rw [e.map_neg]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
⊢ (fun x => if x = 0 then 0 else ⊤) x = 0 → x = 0
[PROOFSTEP]
simp only
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
⊢ (if x = 0 then 0 else ⊤) = 0 → x = 0
[PROOFSTEP]
split_ifs
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
h✝ : x = 0
⊢ 0 = 0 → x = 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
h✝ : ¬x = 0
⊢ ⊤ = 0 → x = 0
[PROOFSTEP]
simp [*]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ (fun x => if x = 0 then 0 else ⊤) (x + y) ≤ (fun x => if x = 0 then 0 else ⊤) x + (fun x => if x = 0 then 0 else ⊤) y
[PROOFSTEP]
simp only
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ (if x + y = 0 then 0 else ⊤) ≤ (if x = 0 then 0 else ⊤) + if y = 0 then 0 else ⊤
[PROOFSTEP]
split_ifs with hxy hx hy hy hx hy hy
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : x = 0
hy : y = 0
⊢ 0 ≤ 0 + 0
[PROOFSTEP]
try simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : x = 0
hy : y = 0
⊢ 0 ≤ 0 + 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : x = 0
hy : ¬y = 0
⊢ 0 ≤ 0 + ⊤
[PROOFSTEP]
try simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : x = 0
hy : ¬y = 0
⊢ 0 ≤ 0 + ⊤
[PROOFSTEP]
simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ 0 ≤ ⊤ + 0
[PROOFSTEP]
try simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ 0 ≤ ⊤ + 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ 0 ≤ ⊤ + ⊤
[PROOFSTEP]
try simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ 0 ≤ ⊤ + ⊤
[PROOFSTEP]
simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : x = 0
hy : y = 0
⊢ ⊤ ≤ 0 + 0
[PROOFSTEP]
try simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : x = 0
hy : y = 0
⊢ ⊤ ≤ 0 + 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : x = 0
hy : ¬y = 0
⊢ ⊤ ≤ 0 + ⊤
[PROOFSTEP]
try simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : x = 0
hy : ¬y = 0
⊢ ⊤ ≤ 0 + ⊤
[PROOFSTEP]
simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ ⊤ ≤ ⊤ + 0
[PROOFSTEP]
try simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : ¬x = 0
hy : y = 0
⊢ ⊤ ≤ ⊤ + 0
[PROOFSTEP]
simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ ⊤ ≤ ⊤ + ⊤
[PROOFSTEP]
try simp [*]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : ¬x = 0
hy : ¬y = 0
⊢ ⊤ ≤ ⊤ + ⊤
[PROOFSTEP]
simp [*]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
hxy : ¬x + y = 0
hx : x = 0
hy : y = 0
⊢ False
[PROOFSTEP]
simp [hx, hy] at hxy 
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
⊢ (fun x => if x = 0 then 0 else ⊤) (c • x) ≤ ↑‖c‖₊ * (fun x => if x = 0 then 0 else ⊤) x
[PROOFSTEP]
simp only
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
⊢ (if c • x = 0 then 0 else ⊤) ≤ ↑‖c‖₊ * if x = 0 then 0 else ⊤
[PROOFSTEP]
split_ifs with hcx hx hx
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hcx : c • x = 0
hx : x = 0
⊢ 0 ≤ ↑‖c‖₊ * 0
[PROOFSTEP]
simp only [smul_eq_zero, not_or] at hcx 
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hcx : c • x = 0
hx : ¬x = 0
⊢ 0 ≤ ↑‖c‖₊ * ⊤
[PROOFSTEP]
simp only [smul_eq_zero, not_or] at hcx 
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hcx : ¬c • x = 0
hx : x = 0
⊢ ⊤ ≤ ↑‖c‖₊ * 0
[PROOFSTEP]
simp only [smul_eq_zero, not_or] at hcx 
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hcx : ¬c • x = 0
hx : ¬x = 0
⊢ ⊤ ≤ ↑‖c‖₊ * ⊤
[PROOFSTEP]
simp only [smul_eq_zero, not_or] at hcx 
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hx : x = 0
hcx : c = 0 ∨ x = 0
⊢ 0 ≤ ↑‖c‖₊ * 0
[PROOFSTEP]
simp only [mul_zero, le_refl]
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hx : ¬x = 0
hcx : c = 0 ∨ x = 0
⊢ 0 ≤ ↑‖c‖₊ * ⊤
[PROOFSTEP]
have : c = 0 := by tauto
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hx : ¬x = 0
hcx : c = 0 ∨ x = 0
⊢ c = 0
[PROOFSTEP]
tauto
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hx : ¬x = 0
hcx : c = 0 ∨ x = 0
this : c = 0
⊢ 0 ≤ ↑‖c‖₊ * ⊤
[PROOFSTEP]
simp [this]
[GOAL]
case pos
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hx : x = 0
hcx : ¬c = 0 ∧ ¬x = 0
⊢ ⊤ ≤ ↑‖c‖₊ * 0
[PROOFSTEP]
tauto
[GOAL]
case neg
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : V
hx : ¬x = 0
hcx : ¬c = 0 ∧ ¬x = 0
⊢ ⊤ ≤ ↑‖c‖₊ * ⊤
[PROOFSTEP]
simpa [mul_top'] using hcx.1
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e✝ e : ENorm 𝕜 V
x : V
h : x = 0
⊢ ↑e x ≤ ↑⊤ x
[PROOFSTEP]
simp [h]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e✝ e : ENorm 𝕜 V
x : V
h : ¬x = 0
⊢ ↑e x ≤ ↑⊤ x
[PROOFSTEP]
simp [top_map h]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
src✝ : PartialOrder (ENorm 𝕜 V) := partialOrder
e₁ e₂ : ENorm 𝕜 V
c : 𝕜
x : V
⊢ (fun x => max (↑e₁ x) (↑e₂ x)) (c • x) = ↑‖c‖₊ * (fun x => max (↑e₁ x) (↑e₂ x)) x
[PROOFSTEP]
simp only [map_smul, ENNReal.mul_max]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x : V
⊢ edist x x = 0
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y z : V
⊢ ↑e (x - z) = ↑e (x - y + (y - z))
[PROOFSTEP]
rw [sub_add_sub_cancel]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
x y : V
⊢ edist x y = 0 → x = y
[PROOFSTEP]
simp [sub_eq_zero]
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
⊢ 0 ∈
    { carrier := {x | ↑e x < ⊤},
        add_mem' := (_ : ∀ {x y : V}, x ∈ {x | ↑e x < ⊤} → y ∈ {x | ↑e x < ⊤} → ↑e (x + y) < ⊤) }.carrier
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
⊢ MetricSpace { x // x ∈ finiteSubspace e }
[PROOFSTEP]
letI := e.emetricSpace
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
this : EMetricSpace V := emetricSpace e
⊢ MetricSpace { x // x ∈ finiteSubspace e }
[PROOFSTEP]
refine' EMetricSpace.toMetricSpace fun x y => _
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
this : EMetricSpace V := emetricSpace e
x y : { x // x ∈ finiteSubspace e }
⊢ edist x y ≠ ⊤
[PROOFSTEP]
change e (x - y) ≠ ⊤
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
this : EMetricSpace V := emetricSpace e
x y : { x // x ∈ finiteSubspace e }
⊢ ↑e (↑x - ↑y) ≠ ⊤
[PROOFSTEP]
exact ne_top_of_le_ne_top (ENNReal.add_lt_top.2 ⟨x.2, y.2⟩).ne (e.map_sub_le x y)
[GOAL]
𝕜 : Type u_1
V : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : AddCommGroup V
inst✝ : Module 𝕜 V
e : ENorm 𝕜 V
c : 𝕜
x : { x // x ∈ finiteSubspace e }
⊢ ‖c • x‖ = ‖c‖ * ‖x‖
[PROOFSTEP]
simp [finite_norm_eq, ENNReal.toReal_mul]
