[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
src✝¹ : NormedAddCommGroup PUnit := normedAddCommGroup
src✝ : CommRing PUnit := commRing
x✝¹ x✝ : PUnit
⊢ ‖x✝¹ * x✝‖ ≤ ‖x✝¹‖ * ‖x✝‖
[PROOFSTEP]
simp
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
α : Type u_5
inst✝² : SeminormedAddCommGroup α
inst✝¹ : One α
inst✝ : NormOneClass α
⊢ ‖0‖ ≠ ‖1‖
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : SeminormedAddCommGroup α
inst✝¹ : One α
inst✝ : NormOneClass α
⊢ ‖1‖ = 1
[PROOFSTEP]
simp [ULift.norm_def]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝⁵ : SeminormedAddCommGroup α
inst✝⁴ : One α
inst✝³ : NormOneClass α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : One β
inst✝ : NormOneClass β
⊢ ‖1‖ = 1
[PROOFSTEP]
simp [Prod.norm_def]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι : Type u_5
α : ι → Type u_6
inst✝⁴ : Nonempty ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedAddCommGroup (α i)
inst✝¹ : (i : ι) → One (α i)
inst✝ : ∀ (i : ι), NormOneClass (α i)
⊢ ‖1‖ = 1
[PROOFSTEP]
simp [Pi.norm_def]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι✝ : Type u_4
ι : Type u_5
α : ι → Type u_6
inst✝⁴ : Nonempty ι
inst✝³ : Fintype ι
inst✝² : (i : ι) → SeminormedAddCommGroup (α i)
inst✝¹ : (i : ι) → One (α i)
inst✝ : ∀ (i : ι), NormOneClass (α i)
⊢ (Finset.sup Finset.univ fun b => 1) = 1
[PROOFSTEP]
exact Finset.sup_const Finset.univ_nonempty 1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
a b : α
⊢ ‖a * b‖₊ ≤ ‖a‖₊ * ‖b‖₊
[PROOFSTEP]
simpa only [← norm_toNNReal, ← Real.toNNReal_mul (norm_nonneg _)] using Real.toNNReal_mono (norm_mul_le _ _)
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : NonUnitalSeminormedRing α
β : Type u_5
inst✝¹ : NormedRing β
inst✝ : Nontrivial β
⊢ ‖1‖ ≤ ‖1‖ * ‖1‖
[PROOFSTEP]
simpa only [mul_one] using norm_mul_le (1 : β) 1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x y : α
⊢ ‖↑(AddMonoidHom.mulRight x) y‖ ≤ ‖x‖ * ‖y‖
[PROOFSTEP]
rw [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x y : α
⊢ ‖↑(AddMonoidHom.mulRight x) y‖ ≤ ‖y‖ * ‖x‖
[PROOFSTEP]
exact norm_mul_le y x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
inst✝ : NonUnitalSeminormedRing β
src✝¹ : SeminormedAddCommGroup (α × β) := seminormedAddCommGroup
src✝ : NonUnitalRing (α × β) := instNonUnitalRing
x y : α × β
⊢ max (‖x.fst‖ * ‖y.fst‖) (‖x.snd‖ * ‖y.snd‖) = max (‖x.fst‖ * ‖y.fst‖) (‖y.snd‖ * ‖x.snd‖)
[PROOFSTEP]
simp [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
inst✝ : NonUnitalSeminormedRing β
src✝¹ : SeminormedAddCommGroup (α × β) := seminormedAddCommGroup
src✝ : NonUnitalRing (α × β) := instNonUnitalRing
x y : α × β
⊢ max (‖x.fst‖ * ‖y.fst‖) (‖y.snd‖ * ‖x.snd‖) ≤ max ‖x.fst‖ ‖x.snd‖ * max ‖y.snd‖ ‖y.fst‖
[PROOFSTEP]
apply max_mul_mul_le_max_mul_max
[GOAL]
case ha
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
inst✝ : NonUnitalSeminormedRing β
src✝¹ : SeminormedAddCommGroup (α × β) := seminormedAddCommGroup
src✝ : NonUnitalRing (α × β) := instNonUnitalRing
x y : α × β
⊢ 0 ≤ ‖x.fst‖
[PROOFSTEP]
simp [norm_nonneg]
[GOAL]
case hd
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
inst✝ : NonUnitalSeminormedRing β
src✝¹ : SeminormedAddCommGroup (α × β) := seminormedAddCommGroup
src✝ : NonUnitalRing (α × β) := instNonUnitalRing
x y : α × β
⊢ 0 ≤ ‖y.snd‖
[PROOFSTEP]
simp [norm_nonneg]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NonUnitalSeminormedRing α
inst✝ : NonUnitalSeminormedRing β
src✝¹ : SeminormedAddCommGroup (α × β) := seminormedAddCommGroup
src✝ : NonUnitalRing (α × β) := instNonUnitalRing
x y : α × β
⊢ max ‖x.fst‖ ‖x.snd‖ * max ‖y.snd‖ ‖y.fst‖ = max ‖x.fst‖ ‖x.snd‖ * max ‖y.fst‖ ‖y.snd‖
[PROOFSTEP]
simp [max_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
⊢ ‖↑0‖ ≤ ↑0 * ‖1‖
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑(n + 1)‖ ≤ ↑(n + 1) * ‖1‖
[PROOFSTEP]
rw [n.cast_succ, n.cast_succ, add_mul, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
n : ℕ
⊢ ‖↑n + 1‖ ≤ ↑n * ‖1‖ + ‖1‖
[PROOFSTEP]
exact norm_add_le_of_le (Nat.norm_cast_le n) le_rfl
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a : α
x✝ : [a] ≠ []
⊢ ‖prod [a]‖ ≤ prod (map norm [a])
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖prod (a :: b :: l)‖ ≤ prod (map norm (a :: b :: l))
[PROOFSTEP]
rw [List.map_cons, List.prod_cons, @List.prod_cons _ _ _ ‖a‖]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖a * prod (b :: l)‖ ≤ ‖a‖ * prod (map norm (b :: l))
[PROOFSTEP]
refine' le_trans (norm_mul_le _ _) (mul_le_mul_of_nonneg_left _ (norm_nonneg _))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a b : α
l : List α
x✝ : a :: b :: l ≠ []
⊢ ‖prod (b :: l)‖ ≤ prod (map norm (b :: l))
[PROOFSTEP]
exact List.norm_prod_le' (List.cons_ne_nil b l)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
l : List α
hl : l ≠ []
⊢ prod (map norm l) = (fun a => ↑a) (prod (map nnnorm l))
[PROOFSTEP]
simp [NNReal.coe_list_prod, List.map_map]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
⊢ ‖prod []‖ ≤ prod (map norm [])
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
l : List α
⊢ prod (map norm l) = (fun a => ↑a) (prod (map nnnorm l))
[PROOFSTEP]
simp [NNReal.coe_list_prod, List.map_map]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α✝
α : Type u_5
inst✝ : NormedCommRing α
s : Finset ι
hs : Finset.Nonempty s
f : ι → α
⊢ ‖∏ i in s, f i‖ ≤ ∏ i in s, ‖f i‖
[PROOFSTEP]
rcases s with ⟨⟨l⟩, hl⟩
[GOAL]
case mk.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α✝
α : Type u_5
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
hs : Finset.Nonempty { val := Quot.mk Setoid.r l, nodup := hl }
⊢ ‖∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, f i‖ ≤ ∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, ‖f i‖
[PROOFSTEP]
have : l.map f ≠ [] := by simpa using hs
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α✝
α : Type u_5
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
hs : Finset.Nonempty { val := Quot.mk Setoid.r l, nodup := hl }
⊢ List.map f l ≠ []
[PROOFSTEP]
simpa using hs
[GOAL]
case mk.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α✝
α : Type u_5
inst✝ : NormedCommRing α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
hs : Finset.Nonempty { val := Quot.mk Setoid.r l, nodup := hl }
this : List.map f l ≠ []
⊢ ‖∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, f i‖ ≤ ∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, ‖f i‖
[PROOFSTEP]
simpa using List.norm_prod_le' this
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α✝
α : Type u_5
inst✝ : NormedCommRing α
s : Finset ι
hs : Finset.Nonempty s
f : ι → α
⊢ ∏ i in s, ‖f i‖ = (fun a => ↑a) (∏ i in s, ‖f i‖₊)
[PROOFSTEP]
simp [NNReal.coe_prod]
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : SeminormedRing α✝
α : Type u_5
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
s : Finset ι
f : ι → α
⊢ ‖∏ i in s, f i‖ ≤ ∏ i in s, ‖f i‖
[PROOFSTEP]
rcases s with ⟨⟨l⟩, hl⟩
[GOAL]
case mk.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : SeminormedRing α✝
α : Type u_5
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
f : ι → α
val✝ : Multiset ι
l : List ι
hl : Multiset.Nodup (Quot.mk Setoid.r l)
⊢ ‖∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, f i‖ ≤ ∏ i in { val := Quot.mk Setoid.r l, nodup := hl }, ‖f i‖
[PROOFSTEP]
simpa using (l.map f).norm_prod_le
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : SeminormedRing α✝
α : Type u_5
inst✝¹ : NormedCommRing α
inst✝ : NormOneClass α
s : Finset ι
f : ι → α
⊢ ∏ i in s, ‖f i‖ = (fun a => ↑a) (∏ i in s, ‖f i‖₊)
[PROOFSTEP]
simp [NNReal.coe_prod]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a : α
x✝ : 0 < 1
⊢ ‖a ^ 1‖₊ ≤ ‖a‖₊ ^ 1
[PROOFSTEP]
simp only [pow_one, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a : α
n : ℕ
x✝ : 0 < n + 2
⊢ ‖a ^ (n + 2)‖₊ ≤ ‖a‖₊ ^ (n + 2)
[PROOFSTEP]
simpa only [pow_succ _ (n + 1)] using le_trans (nnnorm_mul_le _ _) (mul_le_mul_left' (nnnorm_pow_le' a n.succ_pos) _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
a : α
n : ℕ
⊢ ‖a ^ Nat.zero‖₊ ≤ ‖a‖₊ ^ Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, pow_zero, nnnorm_one, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedRing α
a : α
n : ℕ
h : 0 < n
⊢ ‖a ^ n‖ ≤ ‖a‖ ^ n
[PROOFSTEP]
simpa only [NNReal.coe_pow, coe_nnnorm] using NNReal.coe_mono (nnnorm_pow_le' a h)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : SeminormedRing α
inst✝ : NormOneClass α
a : α
n : ℕ
⊢ ‖a ^ Nat.zero‖ ≤ ‖a‖ ^ Nat.zero
[PROOFSTEP]
simp only [Nat.zero_eq, pow_zero, norm_one, le_rfl]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
⊢ Tendsto (fun e => ‖e.fst * e.snd - (fun p => p.fst * p.snd) x‖) (𝓝 x) (𝓝 0)
[PROOFSTEP]
have : ∀ e : α × α, ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ :=
  by
  intro e
  calc
    ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
      rw [_root_.mul_sub, _root_.sub_mul, sub_add_sub_cancel]
        -- porting note: `ENNReal.{mul_sub, sub_mul}` should be protected
    _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ := norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
⊢ ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
[PROOFSTEP]
intro e
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
[PROOFSTEP]
calc
  ‖e.1 * e.2 - x.1 * x.2‖ ≤ ‖e.1 * (e.2 - x.2) + (e.1 - x.1) * x.2‖ := by
    rw [_root_.mul_sub, _root_.sub_mul, sub_add_sub_cancel]
      -- porting note: `ENNReal.{mul_sub, sub_mul}` should be protected
  _ ≤ ‖e.1‖ * ‖e.2 - x.2‖ + ‖e.1 - x.1‖ * ‖x.2‖ := norm_add_le_of_le (norm_mul_le _ _) (norm_mul_le _ _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x e : α × α
⊢ ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst * (e.snd - x.snd) + (e.fst - x.fst) * x.snd‖
[PROOFSTEP]
rw [_root_.mul_sub, _root_.sub_mul, sub_add_sub_cancel]
  -- porting note: `ENNReal.{mul_sub, sub_mul}` should be protected
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ Tendsto (fun e => ‖e.fst * e.snd - (fun p => p.fst * p.snd) x‖) (𝓝 x) (𝓝 0)
[PROOFSTEP]
refine squeeze_zero (fun e => norm_nonneg _) this ?_
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ Tendsto (fun t => ‖t.fst‖ * ‖t.snd - x.snd‖ + ‖t.fst - x.fst‖ * ‖x.snd‖) (𝓝 x) (𝓝 0)
[PROOFSTEP]
convert
  ((continuous_fst.tendsto x).norm.mul ((continuous_snd.tendsto x).sub tendsto_const_nhds).norm).add
    (((continuous_fst.tendsto x).sub tendsto_const_nhds).norm.mul _)
      -- Porting note: `show` used to select a goal to work on
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ 0 = ‖x.fst‖ * ‖x.snd - x.snd‖ + ‖x.fst - x.fst‖ * ?convert_4
case convert_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ ℝ
case convert_5
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ Tendsto (fun t => ‖x.snd‖) (𝓝 x) (𝓝 ?convert_4)
[PROOFSTEP]
rotate_right
[GOAL]
case convert_5
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ Tendsto (fun t => ‖x.snd‖) (𝓝 x) (𝓝 ?convert_4)
case h.e'_5.h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ 0 = ‖x.fst‖ * ‖x.snd - x.snd‖ + ‖x.fst - x.fst‖ * ?convert_4
case convert_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ ℝ
[PROOFSTEP]
show Tendsto _ _ _
[GOAL]
case convert_5
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ Tendsto (fun t => ‖x.snd‖) (𝓝 x) (𝓝 ?convert_4)
case h.e'_5.h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ 0 = ‖x.fst‖ * ‖x.snd - x.snd‖ + ‖x.fst - x.fst‖ * ?convert_4
case convert_4
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ ℝ
[PROOFSTEP]
exact tendsto_const_nhds
[GOAL]
case h.e'_5.h.e'_3
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NonUnitalSeminormedRing α
x : α × α
this : ∀ (e : α × α), ‖e.fst * e.snd - x.fst * x.snd‖ ≤ ‖e.fst‖ * ‖e.snd - x.snd‖ + ‖e.fst - x.fst‖ * ‖x.snd‖
⊢ 0 = ‖x.fst‖ * ‖x.snd - x.snd‖ + ‖x.fst - x.fst‖ * ‖x.snd‖
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
⊢ ‖1‖ * ‖1‖ = ‖1‖ * 1
[PROOFSTEP]
rw [← norm_mul, mul_one, mul_one]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
a : α
⊢ ↑‖a⁻¹‖₊ = ↑‖a‖₊⁻¹
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ dist z⁻¹ w⁻¹ = dist z w / (‖z‖ * ‖w‖)
[PROOFSTEP]
rw [dist_eq_norm, inv_sub_inv' hz hw, norm_mul, norm_mul, norm_inv, norm_inv, mul_comm ‖z‖⁻¹, mul_assoc, dist_eq_norm',
  div_eq_mul_inv, mul_inv]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ nndist z⁻¹ w⁻¹ = nndist z w / (‖z‖₊ * ‖w‖₊)
[PROOFSTEP]
rw [← NNReal.coe_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
z w : α
hz : z ≠ 0
hw : w ≠ 0
⊢ ↑(nndist z⁻¹ w⁻¹) = ↑(nndist z w / (‖z‖₊ * ‖w‖₊))
[PROOFSTEP]
simp [-NNReal.coe_eq, dist_inv_inv₀ hz hw]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
a : α
ha : a ≠ 0
⊢ Tendsto ((fun x x_1 => x * x_1) a) (comap norm atTop) (comap norm atTop)
[PROOFSTEP]
simpa only [tendsto_comap_iff, (· ∘ ·), norm_mul] using tendsto_const_nhds.mul_atTop (norm_pos_iff.2 ha) tendsto_comap
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
a : α
ha : a ≠ 0
⊢ Tendsto (fun x => x * a) (comap norm atTop) (comap norm atTop)
[PROOFSTEP]
simpa only [tendsto_comap_iff, (· ∘ ·), norm_mul] using tendsto_comap.atTop_mul (norm_pos_iff.2 ha) tendsto_const_nhds
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
⊢ HasContinuousInv₀ α
[PROOFSTEP]
refine' ⟨fun r r0 => tendsto_iff_norm_tendsto_zero.2 _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
⊢ Tendsto (fun e => ‖e⁻¹ - r⁻¹‖) (𝓝 r) (𝓝 0)
[PROOFSTEP]
have r0' : 0 < ‖r‖ := norm_pos_iff.2 r0
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
⊢ Tendsto (fun e => ‖e⁻¹ - r⁻¹‖) (𝓝 r) (𝓝 0)
[PROOFSTEP]
rcases exists_between r0' with ⟨ε, ε0, εr⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
⊢ Tendsto (fun e => ‖e⁻¹ - r⁻¹‖) (𝓝 r) (𝓝 0)
[PROOFSTEP]
have : ∀ᶠ e in 𝓝 r, ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε :=
  by
  filter_upwards [(isOpen_lt continuous_const continuous_norm).eventually_mem εr] with e he
  have e0 : e ≠ 0 := norm_pos_iff.1 (ε0.trans he)
  calc
    ‖e⁻¹ - r⁻¹‖ = ‖r‖⁻¹ * ‖r - e‖ * ‖e‖⁻¹ := by
      rw [← norm_inv, ← norm_inv, ← norm_mul, ← norm_mul, _root_.mul_sub, _root_.sub_mul, mul_assoc _ e,
        inv_mul_cancel r0, mul_inv_cancel e0, one_mul, mul_one]
        -- porting note: `ENNReal.{mul_sub, sub_mul}` should be `protected`
    _ = ‖r - e‖ / ‖r‖ / ‖e‖ := by field_simp [mul_comm]
    _ ≤ ‖r - e‖ / ‖r‖ / ε := by gcongr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
⊢ ∀ᶠ (e : α) in 𝓝 r, ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε
[PROOFSTEP]
filter_upwards [(isOpen_lt continuous_const continuous_norm).eventually_mem εr] with e he
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
e : α
he : ε < ‖e‖
⊢ ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε
[PROOFSTEP]
have e0 : e ≠ 0 := norm_pos_iff.1 (ε0.trans he)
[GOAL]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
e : α
he : ε < ‖e‖
e0 : e ≠ 0
⊢ ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε
[PROOFSTEP]
calc
  ‖e⁻¹ - r⁻¹‖ = ‖r‖⁻¹ * ‖r - e‖ * ‖e‖⁻¹ := by
    rw [← norm_inv, ← norm_inv, ← norm_mul, ← norm_mul, _root_.mul_sub, _root_.sub_mul, mul_assoc _ e,
      inv_mul_cancel r0, mul_inv_cancel e0, one_mul, mul_one]
      -- porting note: `ENNReal.{mul_sub, sub_mul}` should be `protected`
  _ = ‖r - e‖ / ‖r‖ / ‖e‖ := by field_simp [mul_comm]
  _ ≤ ‖r - e‖ / ‖r‖ / ε := by gcongr
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
e : α
he : ε < ‖e‖
e0 : e ≠ 0
⊢ ‖e⁻¹ - r⁻¹‖ = ‖r‖⁻¹ * ‖r - e‖ * ‖e‖⁻¹
[PROOFSTEP]
rw [← norm_inv, ← norm_inv, ← norm_mul, ← norm_mul, _root_.mul_sub, _root_.sub_mul, mul_assoc _ e, inv_mul_cancel r0,
  mul_inv_cancel e0, one_mul, mul_one]
  -- porting note: `ENNReal.{mul_sub, sub_mul}` should be `protected`
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
e : α
he : ε < ‖e‖
e0 : e ≠ 0
⊢ ‖r‖⁻¹ * ‖r - e‖ * ‖e‖⁻¹ = ‖r - e‖ / ‖r‖ / ‖e‖
[PROOFSTEP]
field_simp [mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
e : α
he : ε < ‖e‖
e0 : e ≠ 0
⊢ ‖r - e‖ / ‖r‖ / ‖e‖ ≤ ‖r - e‖ / ‖r‖ / ε
[PROOFSTEP]
gcongr
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
this : ∀ᶠ (e : α) in 𝓝 r, ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε
⊢ Tendsto (fun e => ‖e⁻¹ - r⁻¹‖) (𝓝 r) (𝓝 0)
[PROOFSTEP]
refine' squeeze_zero' (eventually_of_forall fun _ => norm_nonneg _) this _
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
this : ∀ᶠ (e : α) in 𝓝 r, ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε
⊢ Tendsto (fun t => ‖r - t‖ / ‖r‖ / ε) (𝓝 r) (𝓝 0)
[PROOFSTEP]
refine' (((continuous_const.sub continuous_id).norm.div_const _).div_const _).tendsto' _ _ _
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NormedDivisionRing α
r : α
r0 : r ≠ 0
r0' : 0 < ‖r‖
ε : ℝ
ε0 : 0 < ε
εr : ε < ‖r‖
this : ∀ᶠ (e : α) in 𝓝 r, ‖e⁻¹ - r⁻¹‖ ≤ ‖r - e‖ / ‖r‖ / ε
⊢ ‖r - id r‖ / ‖r‖ / ε = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ ‖↑φ x‖ = 1
[PROOFSTEP]
rw [← pow_left_inj, ← norm_pow, ← map_pow, h, map_one, norm_one, one_pow]
[GOAL]
case Hxpos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ 0 ≤ ‖↑φ x‖
case Hypos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ 0 ≤ 1
case Hnpos
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : NormedDivisionRing α
inst✝ : Monoid β
φ : β →* α
x : β
k : ℕ+
h : x ^ ↑k = 1
⊢ 0 < ↑k
[PROOFSTEP]
exacts [norm_nonneg _, zero_le_one, k.pos]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
r : ℝ
w : α
hw : 1 < ‖w‖
n : ℕ
hn : r < ‖w‖ ^ n
⊢ r < ‖w ^ n‖
[PROOFSTEP]
rwa [norm_pow]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
r : ℝ
hr : 0 < r
w : α
hw : r⁻¹ < ‖w‖
⊢ 0 < ‖w⁻¹‖ ∧ ‖w⁻¹‖ < r
[PROOFSTEP]
rwa [← Set.mem_Ioo, norm_inv, ← Set.mem_inv, Set.inv_Ioo_0_left hr]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
x : α
⊢ NeBot (𝓝[{x}ᶜ] x)
[PROOFSTEP]
rw [← mem_closure_iff_nhdsWithin_neBot, Metric.mem_closure_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
x : α
⊢ ∀ (ε : ℝ), ε > 0 → ∃ b, b ∈ {x}ᶜ ∧ dist x b < ε
[PROOFSTEP]
rintro ε ε0
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
⊢ ∃ b, b ∈ {x}ᶜ ∧ dist x b < ε
[PROOFSTEP]
rcases exists_norm_lt α ε0 with ⟨b, hb0, hbε⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ ∃ b, b ∈ {x}ᶜ ∧ dist x b < ε
[PROOFSTEP]
refine' ⟨x + b, mt (Set.mem_singleton_iff.trans add_right_eq_self).1 <| norm_pos_iff.1 hb0, _⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ dist x (x + b) < ε
[PROOFSTEP]
rwa [dist_comm, dist_eq_norm, add_sub_cancel']
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : NontriviallyNormedField α
⊢ NeBot (𝓝[{x | IsUnit x}] 0)
[PROOFSTEP]
simpa only [isUnit_iff_ne_zero] using punctured_nhds_neBot (0 : α)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
r₁ r₂ : ℝ≥0
h : r₁ < r₂
⊢ ∃ x, r₁ < ‖x‖₊ ∧ ‖x‖₊ < r₂
[PROOFSTEP]
exact_mod_cast exists_lt_norm_lt α r₁.prop h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
⊢ ∀ (a₁ a₂ : ↑(Set.range norm)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨-, x, rfl⟩ ⟨-, y, rfl⟩ hxy
[GOAL]
case mk.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
x y : α
hxy : { val := ‖x‖, property := (_ : ∃ y, ‖y‖ = ‖x‖) } < { val := ‖y‖, property := (_ : ∃ y_1, ‖y_1‖ = ‖y‖) }
⊢ ∃ a, { val := ‖x‖, property := (_ : ∃ y, ‖y‖ = ‖x‖) } < a ∧ a < { val := ‖y‖, property := (_ : ∃ y_1, ‖y_1‖ = ‖y‖) }
[PROOFSTEP]
let ⟨z, h⟩ := exists_lt_norm_lt α (norm_nonneg _) hxy
[GOAL]
case mk.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
x y : α
hxy : { val := ‖x‖, property := (_ : ∃ y, ‖y‖ = ‖x‖) } < { val := ‖y‖, property := (_ : ∃ y_1, ‖y_1‖ = ‖y‖) }
z : α
h : ‖x‖ < ‖z‖ ∧ ‖z‖ < ↑{ val := ‖y‖, property := (_ : ∃ y_1, ‖y_1‖ = ‖y‖) }
⊢ ∃ a, { val := ‖x‖, property := (_ : ∃ y, ‖y‖ = ‖x‖) } < a ∧ a < { val := ‖y‖, property := (_ : ∃ y_1, ‖y_1‖ = ‖y‖) }
[PROOFSTEP]
exact ⟨⟨‖z‖, z, rfl⟩, h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
⊢ ∀ (a₁ a₂ : ↑(Set.range nnnorm)), a₁ < a₂ → ∃ a, a₁ < a ∧ a < a₂
[PROOFSTEP]
rintro ⟨-, x, rfl⟩ ⟨-, y, rfl⟩ hxy
[GOAL]
case mk.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
x y : α
hxy : { val := ‖x‖₊, property := (_ : ∃ y, ‖y‖₊ = ‖x‖₊) } < { val := ‖y‖₊, property := (_ : ∃ y_1, ‖y_1‖₊ = ‖y‖₊) }
⊢ ∃ a,
    { val := ‖x‖₊, property := (_ : ∃ y, ‖y‖₊ = ‖x‖₊) } < a ∧
      a < { val := ‖y‖₊, property := (_ : ∃ y_1, ‖y_1‖₊ = ‖y‖₊) }
[PROOFSTEP]
let ⟨z, h⟩ := exists_lt_nnnorm_lt α hxy
[GOAL]
case mk.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : DenselyNormedField α
x y : α
hxy : { val := ‖x‖₊, property := (_ : ∃ y, ‖y‖₊ = ‖x‖₊) } < { val := ‖y‖₊, property := (_ : ∃ y_1, ‖y_1‖₊ = ‖y‖₊) }
z : α
h :
  ↑{ val := ‖x‖₊, property := (_ : ∃ y, ‖y‖₊ = ‖x‖₊) } < ‖z‖₊ ∧
    ‖z‖₊ < ↑{ val := ‖y‖₊, property := (_ : ∃ y_1, ‖y_1‖₊ = ‖y‖₊) }
⊢ ∃ a,
    { val := ‖x‖₊, property := (_ : ∃ y, ‖y‖₊ = ‖x‖₊) } < a ∧
      a < { val := ‖y‖₊, property := (_ : ∃ y_1, ‖y_1‖₊ = ‖y‖₊) }
[PROOFSTEP]
exact ⟨⟨‖z‖₊, z, rfl⟩, h⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
x✝¹ x✝ : ℝ
h₀ : 0 ≤ x✝¹
hr : x✝¹ < x✝
x : ℝ
h : x✝¹ < x ∧ x < x✝
⊢ x✝¹ < ‖x‖ ∧ ‖x‖ < x✝
[PROOFSTEP]
rwa [Real.norm_eq_abs, abs_of_nonneg (h₀.trans h.1.le)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
x y : ℝ
hx : 0 ≤ x
⊢ toNNReal x * ‖y‖₊ = ‖x * y‖₊
[PROOFSTEP]
ext
[GOAL]
case a
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
x y : ℝ
hx : 0 ≤ x
⊢ ↑(toNNReal x * ‖y‖₊) = ↑‖x * y‖₊
[PROOFSTEP]
simp only [NNReal.coe_mul, nnnorm_mul, coe_nnnorm, Real.toNNReal_of_nonneg, norm_of_nonneg, hx, coe_mk]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
x y : ℝ
hy : 0 ≤ y
⊢ ‖x‖₊ * toNNReal y = ‖x * y‖₊
[PROOFSTEP]
rw [mul_comm, mul_comm x, toNNReal_mul_nnnorm x hy]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
x : ℝ≥0
⊢ ‖↑x‖ = ↑x
[PROOFSTEP]
rw [Real.norm_eq_abs, x.abs_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedAddCommGroup α
a : α
⊢ ‖‖a‖‖₊ = ‖a‖₊
[PROOFSTEP]
rw [Real.nnnorm_of_nonneg (norm_nonneg a)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : SeminormedAddCommGroup α
a : α
⊢ { val := ‖a‖, property := (_ : 0 ≤ ‖a‖) } = ‖a‖₊
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : Nonempty α
inst✝¹ : SemilatticeSup α
β : Type u_5
inst✝ : SeminormedAddCommGroup β
f : α → β
b : β
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ (x : α), x ∈ Set.Ici ia → f x ∈ ball b ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → ‖f n - b‖ < ε
[PROOFSTEP]
simp [dist_eq_norm]
[GOAL]
α : Type u_1
β✝ : Type u_2
γ : Type u_3
ι : Type u_4
inst✝³ : Nonempty α
inst✝² : SemilatticeSup α
inst✝¹ : NoMaxOrder α
β : Type u_5
inst✝ : SeminormedAddCommGroup β
f : α → β
b : β
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ (x : α), x ∈ Set.Ioi ia → f x ∈ ball b ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N < n → ‖f n - b‖ < ε
[PROOFSTEP]
simp [dist_eq_norm]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
src✝¹ : NormedAddCommGroup ℤ := normedAddCommGroup
src✝ : Ring ℤ := instRingInt
m n : ℤ
⊢ ‖m * n‖ = ‖m‖ * ‖n‖
[PROOFSTEP]
simp only [norm, Int.cast_mul, abs_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
⊢ ‖1‖ = 1
[PROOFSTEP]
simp [← Int.norm_cast_real]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
src✝¹ : NormedAddCommGroup ℚ := normedAddCommGroup
src✝ : Field ℚ := field
r₁ r₂ : ℚ
⊢ ‖r₁ * r₂‖ = ‖r₁‖ * ‖r₂‖
[PROOFSTEP]
simp only [norm, Rat.cast_mul, abs_mul]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
r₁ r₂ : ℝ
h₀ : 0 ≤ r₁
hr : r₁ < r₂
q : ℚ
h : r₁ < ↑q ∧ ↑q < r₂
⊢ r₁ < ‖q‖ ∧ ‖q‖ < r₂
[PROOFSTEP]
rwa [← Rat.norm_cast_real, Real.norm_eq_abs, abs_of_pos (h₀.trans_lt h.1)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
F : Type u_5
R : Type u_6
S : Type u_7
inst✝² : NonUnitalRing R
inst✝¹ : NonUnitalSeminormedRing S
inst✝ : NonUnitalRingHomClass F R S
f : F
src✝¹ : SeminormedAddCommGroup R := SeminormedAddCommGroup.induced R S f
src✝ : NonUnitalRing R := inst✝²
x y : R
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖
[PROOFSTEP]
show ‖f (x * y)‖ ≤ ‖f x‖ * ‖f y‖
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
F : Type u_5
R : Type u_6
S : Type u_7
inst✝² : NonUnitalRing R
inst✝¹ : NonUnitalSeminormedRing S
inst✝ : NonUnitalRingHomClass F R S
f : F
src✝¹ : SeminormedAddCommGroup R := SeminormedAddCommGroup.induced R S f
src✝ : NonUnitalRing R := inst✝²
x y : R
⊢ ‖↑f (x * y)‖ ≤ ‖↑f x‖ * ‖↑f y‖
[PROOFSTEP]
exact (map_mul f x y).symm ▸ norm_mul_le (f x) (f y)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
F : Type u_5
R : Type u_6
S : Type u_7
inst✝² : DivisionRing R
inst✝¹ : NormedDivisionRing S
inst✝ : NonUnitalRingHomClass F R S
f : F
hf : Function.Injective ↑f
src✝¹ : NormedAddCommGroup R := NormedAddCommGroup.induced R S f hf
src✝ : DivisionRing R := inst✝²
x y : R
⊢ ‖x * y‖ = ‖x‖ * ‖y‖
[PROOFSTEP]
show ‖f (x * y)‖ = ‖f x‖ * ‖f y‖
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
F : Type u_5
R : Type u_6
S : Type u_7
inst✝² : DivisionRing R
inst✝¹ : NormedDivisionRing S
inst✝ : NonUnitalRingHomClass F R S
f : F
hf : Function.Injective ↑f
src✝¹ : NormedAddCommGroup R := NormedAddCommGroup.induced R S f hf
src✝ : DivisionRing R := inst✝²
x y : R
⊢ ‖↑f (x * y)‖ = ‖↑f x‖ * ‖↑f y‖
[PROOFSTEP]
exact (map_mul f x y).symm ▸ norm_mul (f x) (f y)
