[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
⊢ ‖x‖ = infDist 0 {m | ↑m = x}
[PROOFSTEP]
simp only [AddSubgroup.quotient_norm_eq, infDist_eq_iInf, sInf_image', dist_zero_left]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M
⊢ ‖↑x‖ = infDist x ↑S
[PROOFSTEP]
rw [norm_eq_infDist, ← infDist_image (IsometryEquiv.subLeft x).isometry, IsometryEquiv.subLeft_apply, sub_zero, ←
  IsometryEquiv.preimage_symm]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M
⊢ infDist x (↑(IsometryEquiv.symm (IsometryEquiv.subLeft x)) ⁻¹' {m | ↑m = ↑x}) = infDist x ↑S
[PROOFSTEP]
congr 1 with y
[GOAL]
case e_s.h
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
⊢ y ∈ ↑(IsometryEquiv.symm (IsometryEquiv.subLeft x)) ⁻¹' {m | ↑m = ↑x} ↔ y ∈ ↑S
[PROOFSTEP]
simp only [mem_preimage, IsometryEquiv.subLeft_symm_apply, mem_setOf_eq, QuotientAddGroup.eq, neg_add, neg_neg,
  neg_add_cancel_right, SetLike.mem_coe]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
⊢ ‖-x‖ = ‖x‖
[PROOFSTEP]
simp only [AddSubgroup.quotient_norm_eq]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
⊢ sInf (norm '' {m | ↑m = -x}) = sInf (norm '' {m | ↑m = x})
[PROOFSTEP]
congr 1 with r
[GOAL]
case e_a.h
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ r ∈ norm '' {m | ↑m = -x} ↔ r ∈ norm '' {m | ↑m = x}
[PROOFSTEP]
constructor
[GOAL]
case e_a.h.mp
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ r ∈ norm '' {m | ↑m = -x} → r ∈ norm '' {m | ↑m = x}
[PROOFSTEP]
{rintro ⟨m, hm, rfl⟩; use-m; simpa [neg_eq_iff_eq_neg] using hm
}
[GOAL]
case e_a.h.mp
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ r ∈ norm '' {m | ↑m = -x} → r ∈ norm '' {m | ↑m = x}
[PROOFSTEP]
rintro ⟨m, hm, rfl⟩
[GOAL]
case e_a.h.mp.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
m : M
hm : m ∈ {m | ↑m = -x}
⊢ ‖m‖ ∈ norm '' {m | ↑m = x}
[PROOFSTEP]
use-m
[GOAL]
case h
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
m : M
hm : m ∈ {m | ↑m = -x}
⊢ -m ∈ {m | ↑m = x} ∧ ‖-m‖ = ‖m‖
[PROOFSTEP]
simpa [neg_eq_iff_eq_neg] using hm
[GOAL]
case e_a.h.mpr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ r ∈ norm '' {m | ↑m = x} → r ∈ norm '' {m | ↑m = -x}
[PROOFSTEP]
{rintro ⟨m, hm, rfl⟩; use-m; simpa [neg_eq_iff_eq_neg] using hm
}
[GOAL]
case e_a.h.mpr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ r ∈ norm '' {m | ↑m = x} → r ∈ norm '' {m | ↑m = -x}
[PROOFSTEP]
rintro ⟨m, hm, rfl⟩
[GOAL]
case e_a.h.mpr.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
m : M
hm : m ∈ {m | ↑m = x}
⊢ ‖m‖ ∈ norm '' {m | ↑m = -x}
[PROOFSTEP]
use-m
[GOAL]
case h
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
m : M
hm : m ∈ {m | ↑m = x}
⊢ -m ∈ {m | ↑m = -x} ∧ ‖-m‖ = ‖m‖
[PROOFSTEP]
simpa [neg_eq_iff_eq_neg] using hm
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M ⧸ S
⊢ ‖x - y‖ = ‖y - x‖
[PROOFSTEP]
rw [← neg_sub, quotient_norm_neg]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖↑(mk' S) m‖ = sInf ((fun x => ‖m + x‖) '' ↑S)
[PROOFSTEP]
rw [mk'_apply, norm_mk, sInf_image', ← infDist_image isometry_neg, image_neg, neg_coe_set (H := S), infDist_eq_iInf]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ⨅ (y : ↑↑S), dist (-m) ↑y = ⨅ (a : ↑↑S), ‖m + ↑a‖
[PROOFSTEP]
simp only [dist_eq_norm', sub_neg_eq_add, add_comm]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖↑(mk' S) m‖ = 0 ↔ m ∈ closure ↑S
[PROOFSTEP]
rw [mk'_apply, norm_mk, ← mem_closure_iff_infDist_zero]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ Set.Nonempty ↑S
[PROOFSTEP]
exact ⟨0, S.zero_mem⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ ‖x‖ < r ↔ ∃ m, ↑m = x ∧ ‖m‖ < r
[PROOFSTEP]
rw [isGLB_lt_iff (isGLB_quotient_norm _), bex_image_iff]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ (∃ x_1, x_1 ∈ {m | ↑(mk' S) m = x} ∧ ‖x_1‖ < r) ↔ ∃ m, ↑m = x ∧ ‖m‖ < r
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
⊢ ∃ s, s ∈ S ∧ ‖m + s‖ < ‖↑(mk' S) m‖ + ε
[PROOFSTEP]
obtain ⟨n : M, hn : mk' S n = mk' S m, hn' : ‖n‖ < ‖mk' S m‖ + ε⟩ := norm_mk_lt (QuotientAddGroup.mk' S m) hε
[GOAL]
case intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : ↑(mk' S) n = ↑(mk' S) m
hn' : ‖n‖ < ‖↑(mk' S) m‖ + ε
⊢ ∃ s, s ∈ S ∧ ‖m + s‖ < ‖↑(mk' S) m‖ + ε
[PROOFSTEP]
erw [eq_comm, QuotientAddGroup.eq] at hn 
[GOAL]
case intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : -m + n ∈ S
hn' : ‖n‖ < ‖↑(mk' S) m‖ + ε
⊢ ∃ s, s ∈ S ∧ ‖m + s‖ < ‖↑(mk' S) m‖ + ε
[PROOFSTEP]
use-m + n, hn
[GOAL]
case right
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : -m + n ∈ S
hn' : ‖n‖ < ‖↑(mk' S) m‖ + ε
⊢ ‖m + (-m + n)‖ < ‖↑(mk' S) m‖ + ε
[PROOFSTEP]
rwa [add_neg_cancel_left]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M ⧸ S
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖
[PROOFSTEP]
rcases And.intro (mk_surjective x) (mk_surjective y) with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
[GOAL]
case intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
⊢ ‖↑x + ↑y‖ ≤ ‖↑x‖ + ‖↑y‖
[PROOFSTEP]
simp only [← mk'_apply, ← map_add, quotient_norm_mk_eq, sInf_image']
[GOAL]
case intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
⊢ ⨅ (a : ↑↑S), ‖x + y + ↑a‖ ≤ (⨅ (a : ↑↑S), ‖x + ↑a‖) + ⨅ (a : ↑↑S), ‖y + ↑a‖
[PROOFSTEP]
refine le_ciInf_add_ciInf fun a b ↦ ?_
[GOAL]
case intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
a b : ↑↑S
⊢ ⨅ (a : ↑↑S), ‖x + y + ↑a‖ ≤ ‖x + ↑a‖ + ‖y + ↑b‖
[PROOFSTEP]
refine ciInf_le_of_le ⟨0, forall_range_iff.2 fun _ ↦ norm_nonneg _⟩ (a + b) ?_
[GOAL]
case intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
a b : ↑↑S
⊢ ‖x + y + ↑(a + b)‖ ≤ ‖x + ↑a‖ + ‖y + ↑b‖
[PROOFSTEP]
exact (congr_arg norm (add_add_add_comm _ _ _ _)).trans_le (norm_add_le _ _)
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ ‖0‖ = 0
[PROOFSTEP]
erw [quotient_norm_eq_zero_iff]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ 0 ∈ closure ↑S
[PROOFSTEP]
exact subset_closure S.zero_mem
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
hS : IsClosed ↑S
m : M
h : ‖↑(mk' S) m‖ = 0
⊢ m ∈ S
[PROOFSTEP]
rwa [quotient_norm_eq_zero_iff, hS.closure_eq] at h 
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ Filter.HasBasis (𝓝 0) (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}
[PROOFSTEP]
have : ∀ ε : ℝ, mk '' ball (0 : M) ε = {x : M ⧸ S | ‖x‖ < ε}
[GOAL]
case this
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
[PROOFSTEP]
refine fun ε ↦ Set.ext <| forall_mk.2 fun x ↦ ?_
[GOAL]
case this
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
ε : ℝ
x : M
⊢ ↑x ∈ mk '' ball 0 ε ↔ ↑x ∈ {x | ‖x‖ < ε}
[PROOFSTEP]
rw [ball_zero_eq, mem_setOf_eq, norm_lt_iff, mem_image]
[GOAL]
case this
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
ε : ℝ
x : M
⊢ (∃ x_1, x_1 ∈ {x | ‖x‖ < ε} ∧ ↑x_1 = ↑x) ↔ ∃ m, ↑m = ↑x ∧ ‖m‖ < ε
[PROOFSTEP]
exact exists_congr fun _ ↦ and_comm
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
⊢ Filter.HasBasis (𝓝 0) (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}
[PROOFSTEP]
rw [← mk_zero, nhds_eq, ← funext this]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
⊢ Filter.HasBasis (Filter.map mk (𝓝 0)) (fun ε => 0 < ε) fun x => mk '' ball 0 x
[PROOFSTEP]
exact .map _ Metric.nhds_basis_ball
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
⊢ dist x x = 0
[PROOFSTEP]
simp only [norm_mk_zero, sub_self]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y z : M ⧸ S
⊢ dist x z ≤ dist x y + dist y z
[PROOFSTEP]
refine le_trans ?_ (quotient_norm_add_le _ _ _)
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y z : M ⧸ S
⊢ dist x z ≤ ‖x - y + (y - z)‖
[PROOFSTEP]
exact (congr_arg norm (sub_add_sub_cancel _ _ _).symm).le
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M ⧸ S
⊢ (fun x y => ↑{ val := ‖x - y‖, property := (_ : 0 ≤ ‖x - y‖) }) x y = ENNReal.ofReal (dist x y)
[PROOFSTEP]
exact ENNReal.coe_nnreal_eq _
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ uniformity (M ⧸ S) = ⨅ (ε : ℝ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
[PROOFSTEP]
rw [uniformity_eq_comap_nhds_zero', ((quotient_nhd_basis S).comap _).eq_biInf]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ ⨅ (i : ℝ) (_ : 0 < i), Filter.principal ((fun p => p.snd - p.fst) ⁻¹' {x | ‖x‖ < i}) =
    ⨅ (ε : ℝ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
[PROOFSTEP]
simp only [dist, quotient_norm_sub_rev (Prod.fst _), preimage_setOf_eq]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
src✝ : M →+ M ⧸ S := mk' S
m : M
⊢ ‖ZeroHom.toFun (↑src✝) m‖ ≤ 1 * ‖m‖
[PROOFSTEP]
simpa [one_mul] using quotient_norm_mk_le _ m
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖↑(normedMk S) m‖ ≤ 1 * ‖m‖
[PROOFSTEP]
simp [quotient_norm_mk_le']
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
[PROOFSTEP]
cases (norm_nonneg f).eq_or_gt with
| inl h =>
  rcases mk_surjective x with ⟨x, rfl⟩
  simpa [h] using le_opNorm f x
| inr h =>
  rw [← not_lt, ← _root_.lt_div_iff' h, norm_lt_iff]
  rintro ⟨x, rfl, hx⟩
  exact ((lt_div_iff' h).1 hx).not_le (le_opNorm f x)
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
x✝ : ‖f‖ = 0 ∨ 0 < ‖f‖
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
[PROOFSTEP]
cases (norm_nonneg f).eq_or_gt with
| inl h =>
  rcases mk_surjective x with ⟨x, rfl⟩
  simpa [h] using le_opNorm f x
| inr h =>
  rw [← not_lt, ← _root_.lt_div_iff' h, norm_lt_iff]
  rintro ⟨x, rfl, hx⟩
  exact ((lt_div_iff' h).1 hx).not_le (le_opNorm f x)
[GOAL]
case inl
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : ‖f‖ = 0
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
[PROOFSTEP]

| inl h =>
  rcases mk_surjective x with ⟨x, rfl⟩
  simpa [h] using le_opNorm f x
[GOAL]
case inl
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : ‖f‖ = 0
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
[PROOFSTEP]
rcases mk_surjective x with ⟨x, rfl⟩
[GOAL]
case inl.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
h : ‖f‖ = 0
x : M
⊢ ‖↑(lift S (toAddMonoidHom f) hf) ↑x‖ ≤ ‖f‖ * ‖↑x‖
[PROOFSTEP]
simpa [h] using le_opNorm f x
[GOAL]
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
[PROOFSTEP]

| inr h =>
  rw [← not_lt, ← _root_.lt_div_iff' h, norm_lt_iff]
  rintro ⟨x, rfl, hx⟩
  exact ((lt_div_iff' h).1 hx).not_le (le_opNorm f x)
[GOAL]
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
[PROOFSTEP]
rw [← not_lt, ← _root_.lt_div_iff' h, norm_lt_iff]
[GOAL]
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ¬∃ m, ↑m = x ∧ ‖m‖ < ‖↑(lift S (toAddMonoidHom f) hf) x‖ / ‖f‖
[PROOFSTEP]
rintro ⟨x, rfl, hx⟩
[GOAL]
case inr.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
h : 0 < ‖f‖
x : M
hx : ‖x‖ < ‖↑(lift S (toAddMonoidHom f) hf) ↑x‖ / ‖f‖
⊢ False
[PROOFSTEP]
exact ((lt_div_iff' h).1 hx).not_le (le_opNorm f x)
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
⊢ ‖normedMk S‖ = 1
[PROOFSTEP]
refine le_antisymm (norm_normedMk_le S) ?_
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
⊢ 1 ≤ ‖normedMk S‖
[PROOFSTEP]
obtain ⟨x, hx⟩ : ∃ x : M, 0 < ‖(x : M ⧸ S)‖
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
⊢ ∃ x, 0 < ‖↑x‖
[PROOFSTEP]
refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
x : M
hx : x ∈ (↑(topologicalClosure S))ᶜ
⊢ 0 < ‖↑x‖
[PROOFSTEP]
exact (norm_nonneg _).lt_of_ne' <| mt (quotient_norm_eq_zero_iff S x).1 hx
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ 1 ≤ ‖normedMk S‖
[PROOFSTEP]
refine (le_mul_iff_one_le_left hx).1 ?_
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ ‖↑x‖ ≤ ‖normedMk S‖ * ‖↑x‖
[PROOFSTEP]
exact norm_lift_apply_le S.normedMk (fun x ↦ (eq_zero_iff x).2) x
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
⊢ ‖normedMk S‖ = 0
[PROOFSTEP]
refine' le_antisymm (opNorm_le_bound _ le_rfl fun x => _) (norm_nonneg _)
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
⊢ ‖↑(normedMk S) x‖ ≤ 0 * ‖x‖
[PROOFSTEP]
have hker : x ∈ S.normedMk.ker.topologicalClosure :=
  by
  rw [S.ker_normedMk, ← SetLike.mem_coe, h]
  trivial
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
⊢ x ∈ topologicalClosure (ker (normedMk S))
[PROOFSTEP]
rw [S.ker_normedMk, ← SetLike.mem_coe, h]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
⊢ x ∈ univ
[PROOFSTEP]
trivial
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
hker : x ∈ topologicalClosure (ker (normedMk S))
⊢ ‖↑(normedMk S) x‖ ≤ 0 * ‖x‖
[PROOFSTEP]
rw [ker_normedMk] at hker 
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
hker : x ∈ topologicalClosure S
⊢ ‖↑(normedMk S) x‖ ≤ 0 * ‖x‖
[PROOFSTEP]
simp only [(quotient_norm_eq_zero_iff S x).mpr hker, normedMk.apply, zero_mul, le_rfl]
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
⊢ g = lift S f hf
[PROOFSTEP]
ext x
[GOAL]
case H
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M ⧸ S
⊢ ↑g x = ↑(lift S f hf) x
[PROOFSTEP]
rcases AddSubgroup.surjective_normedMk _ x with ⟨x, rfl⟩
[GOAL]
case H.intro
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M
⊢ ↑g (↑(AddSubgroup.normedMk S) x) = ↑(lift S f hf) (↑(AddSubgroup.normedMk S) x)
[PROOFSTEP]
change g.comp S.normedMk x = _
[GOAL]
case H.intro
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M
⊢ ↑(NormedAddGroupHom.comp g (AddSubgroup.normedMk S)) x = ↑(lift S f hf) (↑(AddSubgroup.normedMk S) x)
[PROOFSTEP]
simp only [h]
[GOAL]
case H.intro
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M
⊢ ↑f x = ↑(lift S f hf) (↑(AddSubgroup.normedMk S) x)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖↑(AddSubgroup.normedMk S) m‖ = sInf ((fun m_1 => ‖m + m_1‖) '' ↑(ker (AddSubgroup.normedMk S)))
[PROOFSTEP]
simpa [S.ker_normedMk] using quotient_norm_mk_eq _ m
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
n : N
⊢ ∃ m, ↑f m = n ∧ ‖m‖ < ‖n‖ + ε
[PROOFSTEP]
obtain ⟨m, rfl⟩ := hquot.surjective n
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
⊢ ∃ m_1, ↑f m_1 = ↑f m ∧ ‖m_1‖ < ‖↑f m‖ + ε
[PROOFSTEP]
have nonemp : ((fun m' => ‖m + m'‖) '' f.ker).Nonempty :=
  by
  rw [Set.nonempty_image_iff]
  exact ⟨0, f.ker.zero_mem⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
⊢ Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
[PROOFSTEP]
rw [Set.nonempty_image_iff]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
⊢ Set.Nonempty ↑(ker f)
[PROOFSTEP]
exact ⟨0, f.ker.zero_mem⟩
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
⊢ ∃ m_1, ↑f m_1 = ↑f m ∧ ‖m_1‖ < ‖↑f m‖ + ε
[PROOFSTEP]
rcases Real.lt_sInf_add_pos nonemp hε with
  ⟨_, ⟨⟨x, hx, rfl⟩, H : ‖m + x‖ < sInf ((fun m' : M => ‖m + m'‖) '' f.ker) + ε⟩⟩
[GOAL]
case intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
x : M
hx : x ∈ ↑(ker f)
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑(ker f)) + ε
⊢ ∃ m_1, ↑f m_1 = ↑f m ∧ ‖m_1‖ < ‖↑f m‖ + ε
[PROOFSTEP]
exact ⟨m + x, by rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero], by rwa [hquot.norm]⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
x : M
hx : x ∈ ↑(ker f)
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑(ker f)) + ε
⊢ ↑f (m + x) = ↑f m
[PROOFSTEP]
rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
x : M
hx : x ∈ ↑(ker f)
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑(ker f)) + ε
⊢ ‖m + x‖ < ‖↑f m‖ + ε
[PROOFSTEP]
rwa [hquot.norm]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ ‖↑f m‖ ≤ ‖m‖
[PROOFSTEP]
rw [hquot.norm]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ sInf ((fun m_1 => ‖m + m_1‖) '' ↑(ker f)) ≤ ‖m‖
[PROOFSTEP]
apply csInf_le
[GOAL]
case h₁
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ BddBelow ((fun m_1 => ‖m + m_1‖) '' ↑(ker f))
[PROOFSTEP]
use 0
[GOAL]
case h
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ 0 ∈ lowerBounds ((fun m_1 => ‖m + m_1‖) '' ↑(ker f))
[PROOFSTEP]
rintro _ ⟨m', -, rfl⟩
[GOAL]
case h.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m m' : M
⊢ 0 ≤ (fun m_1 => ‖m + m_1‖) m'
[PROOFSTEP]
apply norm_nonneg
[GOAL]
case h₂
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ ‖m‖ ∈ (fun m_1 => ‖m + m_1‖) '' ↑(ker f)
[PROOFSTEP]
exact ⟨0, f.ker.zero_mem, by simp⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ (fun m_1 => ‖m + m_1‖) 0 = ‖m‖
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
fb : NormNoninc f
x : M ⧸ S
⊢ ‖↑(lift S f hf) x‖ ≤ ‖x‖
[PROOFSTEP]
have fb' : ‖f‖ ≤ (1 : ℝ≥0) := NormNoninc.normNoninc_iff_norm_le_one.mp fb
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
fb : NormNoninc f
x : M ⧸ S
fb' : ‖f‖ ≤ ↑1
⊢ ‖↑(lift S f hf) x‖ ≤ ‖x‖
[PROOFSTEP]
simpa using le_of_opNorm_le _ (f.lift_norm_le _ _ fb') _
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
[PROOFSTEP]
have :=
  (nhds_basis_ball.tendsto_iff nhds_basis_ball).mp ((@Real.uniformContinuous_const_mul ‖k‖).continuous.tendsto ‖x‖) ε hε
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
this :
  ∃ ia,
    0 < ia ∧ ∀ (x_1 : ℝ), x_1 ∈ ball ‖x‖ ia → (fun x x_2 => x * x_2) ‖k‖ x_1 ∈ ball ((fun x x_2 => x * x_2) ‖k‖ ‖x‖) ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
[PROOFSTEP]
simp only [mem_ball, exists_prop, dist, abs_sub_lt_iff] at this 
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
this :
  ∃ ia, 0 < ia ∧ ∀ (x_1 : ℝ), x_1 - ‖x‖ < ia ∧ ‖x‖ - x_1 < ia → ‖k‖ * x_1 - ‖k‖ * ‖x‖ < ε ∧ ‖k‖ * ‖x‖ - ‖k‖ * x_1 < ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
[PROOFSTEP]
rcases this with ⟨δ, hδ, h⟩
[GOAL]
case intro.intro
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
h : ∀ (x_1 : ℝ), x_1 - ‖x‖ < δ ∧ ‖x‖ - x_1 < δ → ‖k‖ * x_1 - ‖k‖ * ‖x‖ < ε ∧ ‖k‖ * ‖x‖ - ‖k‖ * x_1 < ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
[PROOFSTEP]
obtain ⟨a, rfl, ha⟩ := Submodule.Quotient.norm_mk_lt x hδ
[GOAL]
case intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h : ∀ (x : ℝ), x - ‖mk a‖ < δ ∧ ‖mk a‖ - x < δ → ‖k‖ * x - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * x < ε
ha : ‖a‖ < ‖mk a‖ + δ
⊢ ‖k • mk a‖ ≤ ‖k‖ * ‖mk a‖ + ε
[PROOFSTEP]
specialize h ‖a‖ ⟨by linarith, by linarith [Submodule.Quotient.norm_mk_le S a]⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h : ∀ (x : ℝ), x - ‖mk a‖ < δ ∧ ‖mk a‖ - x < δ → ‖k‖ * x - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * x < ε
ha : ‖a‖ < ‖mk a‖ + δ
⊢ ‖a‖ - ‖mk a‖ < δ
[PROOFSTEP]
linarith
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h : ∀ (x : ℝ), x - ‖mk a‖ < δ ∧ ‖mk a‖ - x < δ → ‖k‖ * x - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * x < ε
ha : ‖a‖ < ‖mk a‖ + δ
⊢ ‖mk a‖ - ‖a‖ < δ
[PROOFSTEP]
linarith [Submodule.Quotient.norm_mk_le S a]
[GOAL]
case intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
ha : ‖a‖ < ‖mk a‖ + δ
h : ‖k‖ * ‖a‖ - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * ‖a‖ < ε
⊢ ‖k • mk a‖ ≤ ‖k‖ * ‖mk a‖ + ε
[PROOFSTEP]
calc
  _ ≤ ‖k‖ * ‖a‖ := (quotient_norm_mk_le S.toAddSubgroup (k • a)).trans_eq (norm_smul k a)
  _ ≤ _ := (sub_lt_iff_lt_add'.mp h.1).le
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
[PROOFSTEP]
have :=
  ((nhds_basis_ball.prod_nhds nhds_basis_ball).tendsto_iff nhds_basis_ball).mp (continuous_mul.tendsto (‖x‖, ‖y‖)) ε hε
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
this :
  ∃ ia,
    (0 < ia.fst ∧ 0 < ia.snd) ∧
      ∀ (x_1 : ℝ × ℝ),
        x_1 ∈ ball ‖x‖ ia.fst ×ˢ ball ‖y‖ ia.snd → x_1.fst * x_1.snd ∈ ball ((‖x‖, ‖y‖).fst * (‖x‖, ‖y‖).snd) ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
[PROOFSTEP]
simp only [Set.mem_prod, mem_ball, and_imp, Prod.forall, exists_prop, Prod.exists] at this 
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
this : ∃ a b, (0 < a ∧ 0 < b) ∧ ∀ (a_1 b_1 : ℝ), dist a_1 ‖x‖ < a → dist b_1 ‖y‖ < b → dist (a_1 * b_1) (‖x‖ * ‖y‖) < ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
[PROOFSTEP]
rcases this with ⟨ε₁, ε₂, ⟨h₁, h₂⟩, h⟩
[GOAL]
case intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h : ∀ (a b : ℝ), dist a ‖x‖ < ε₁ → dist b ‖y‖ < ε₂ → dist (a * b) (‖x‖ * ‖y‖) < ε
h₁ : 0 < ε₁
h₂ : 0 < ε₂
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
[PROOFSTEP]
obtain ⟨⟨a, rfl, ha⟩, ⟨b, rfl, hb⟩⟩ := Ideal.Quotient.norm_mk_lt x h₁, Ideal.Quotient.norm_mk_lt y h₂
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
h :
  ∀ (a_1 b_1 : ℝ),
    dist a_1 ‖↑(mk I) a‖ < ε₁ → dist b_1 ‖↑(mk I) b‖ < ε₂ → dist (a_1 * b_1) (‖↑(mk I) a‖ * ‖↑(mk I) b‖) < ε
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
⊢ ‖↑(mk I) a * ↑(mk I) b‖ ≤ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ + ε
[PROOFSTEP]
simp only [dist, abs_sub_lt_iff] at h 
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖↑(mk I) a‖ < ε₁ ∧ ‖↑(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖↑(mk I) b‖ < ε₂ ∧ ‖↑(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖↑(mk I) a‖ * ‖↑(mk I) b‖ < ε ∧ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖↑(mk I) a * ↑(mk I) b‖ ≤ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ + ε
[PROOFSTEP]
specialize
  h ‖a‖ ‖b‖ ⟨by linarith, by linarith [Ideal.Quotient.norm_mk_le I a]⟩
    ⟨by linarith, by linarith [Ideal.Quotient.norm_mk_le I b]⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖↑(mk I) a‖ < ε₁ ∧ ‖↑(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖↑(mk I) b‖ < ε₂ ∧ ‖↑(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖↑(mk I) a‖ * ‖↑(mk I) b‖ < ε ∧ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖a‖ - ‖↑(mk I) a‖ < ε₁
[PROOFSTEP]
linarith
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖↑(mk I) a‖ < ε₁ ∧ ‖↑(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖↑(mk I) b‖ < ε₂ ∧ ‖↑(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖↑(mk I) a‖ * ‖↑(mk I) b‖ < ε ∧ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖↑(mk I) a‖ - ‖a‖ < ε₁
[PROOFSTEP]
linarith [Ideal.Quotient.norm_mk_le I a]
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖↑(mk I) a‖ < ε₁ ∧ ‖↑(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖↑(mk I) b‖ < ε₂ ∧ ‖↑(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖↑(mk I) a‖ * ‖↑(mk I) b‖ < ε ∧ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖b‖ - ‖↑(mk I) b‖ < ε₂
[PROOFSTEP]
linarith
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖↑(mk I) a‖ < ε₁ ∧ ‖↑(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖↑(mk I) b‖ < ε₂ ∧ ‖↑(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖↑(mk I) a‖ * ‖↑(mk I) b‖ < ε ∧ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖↑(mk I) b‖ - ‖b‖ < ε₂
[PROOFSTEP]
linarith [Ideal.Quotient.norm_mk_le I b]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
h : ‖a‖ * ‖b‖ - ‖↑(mk I) a‖ * ‖↑(mk I) b‖ < ε ∧ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ - ‖a‖ * ‖b‖ < ε
⊢ ‖↑(mk I) a * ↑(mk I) b‖ ≤ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ + ε
[PROOFSTEP]
calc
  _ ≤ ‖a‖ * ‖b‖ := (Ideal.Quotient.norm_mk_le I (a * b)).trans (norm_mul_le a b)
  _ ≤ _ := (sub_lt_iff_lt_add'.mp h.1).le
