[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
src✝ : Module 𝕜 (Completion E) := instModule
c : 𝕜
x : Completion E
y : E
⊢ ‖c • ↑E y‖ ≤ ‖c‖ * ‖↑E y‖
[PROOFSTEP]
simp only [← coe_smul, norm_coe, norm_smul, le_rfl]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : Completion A
⊢ dist x y = ‖x - y‖
[PROOFSTEP]
refine Completion.induction_on₂ x y ?_ ?_
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : Completion A
⊢ IsClosed {x | dist x.fst x.snd = ‖x.fst - x.snd‖}
[PROOFSTEP]
clear x y
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : Completion A
⊢ ∀ (a b : A), dist (↑A a) (↑A b) = ‖↑A a - ↑A b‖
[PROOFSTEP]
clear x y
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
⊢ IsClosed {x | dist x.fst x.snd = ‖x.fst - x.snd‖}
[PROOFSTEP]
refine' isClosed_eq (Completion.uniformContinuous_extension₂ _).continuous _
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
⊢ Continuous fun x => ‖x.fst - x.snd‖
[PROOFSTEP]
exact Continuous.comp Completion.continuous_extension continuous_sub
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
⊢ ∀ (a b : A), dist (↑A a) (↑A b) = ‖↑A a - ↑A b‖
[PROOFSTEP]
intro x y
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : A
⊢ dist (↑A x) (↑A y) = ‖↑A x - ↑A y‖
[PROOFSTEP]
rw [← Completion.coe_sub, norm_coe, Completion.dist_eq, dist_eq_norm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : Completion A
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖
[PROOFSTEP]
refine Completion.induction_on₂ x y ?_ ?_
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : Completion A
⊢ IsClosed {x | ‖x.fst * x.snd‖ ≤ ‖x.fst‖ * ‖x.snd‖}
[PROOFSTEP]
clear x y
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : Completion A
⊢ ∀ (a b : A), ‖↑A a * ↑A b‖ ≤ ‖↑A a‖ * ‖↑A b‖
[PROOFSTEP]
clear x y
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
⊢ IsClosed {x | ‖x.fst * x.snd‖ ≤ ‖x.fst‖ * ‖x.snd‖}
[PROOFSTEP]
exact
  isClosed_le (Continuous.comp continuous_norm continuous_mul)
    (Continuous.comp _root_.continuous_mul (Continuous.prod_map continuous_norm continuous_norm))
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
⊢ ∀ (a b : A), ‖↑A a * ↑A b‖ ≤ ‖↑A a‖ * ‖↑A b‖
[PROOFSTEP]
intro x y
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : A
⊢ ‖↑A x * ↑A y‖ ≤ ‖↑A x‖ * ‖↑A y‖
[PROOFSTEP]
simp only [← coe_mul, norm_coe]
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
A : Type u_3
inst✝ : SeminormedRing A
src✝¹ : Ring (Completion A) := ring
src✝ : MetricSpace (Completion A) := instMetricSpace
x y : A
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖
[PROOFSTEP]
exact norm_mul_le x y
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
x : Completion A
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
[PROOFSTEP]
refine Completion.induction_on x ?_ ?_
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
x : Completion A
⊢ IsClosed {a | ‖r • a‖ ≤ ‖r‖ * ‖a‖}
[PROOFSTEP]
clear x
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
x : Completion A
⊢ ∀ (a : A), ‖r • ↑A a‖ ≤ ‖r‖ * ‖↑A a‖
[PROOFSTEP]
clear x
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
⊢ IsClosed {a | ‖r • a‖ ≤ ‖r‖ * ‖a‖}
[PROOFSTEP]
exact
  isClosed_le (Continuous.comp continuous_norm (continuous_const_smul r))
    (Continuous.comp (continuous_mul_left _) continuous_norm)
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
⊢ ∀ (a : A), ‖r • ↑A a‖ ≤ ‖r‖ * ‖↑A a‖
[PROOFSTEP]
intro x
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
x : A
⊢ ‖r • ↑A x‖ ≤ ‖r‖ * ‖↑A x‖
[PROOFSTEP]
simp only [← coe_smul, norm_coe]
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : NormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
A : Type u_3
inst✝² : SeminormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : UniformContinuousConstSMul 𝕜 A
src✝ : Algebra 𝕜 (Completion A) := algebra A 𝕜
r : 𝕜
x : A
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
[PROOFSTEP]
exact norm_smul_le r x
