case h
α : Type ?u.206596
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_1
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion ((fun x => A) r)
⊢ Completion.map ((fun x x_1 => x • x_1) r) x = (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r)) x
α : Type ?u.206596
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_1
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
⊢ Completion.map ((fun x x_1 => x • x_1) r) = (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r))
ext x
case h.refine'_1
α : Type ?u.206596
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_1
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion ((fun x => A) r)
⊢ IsClosed
    {a |
      Completion.map ((fun x x_1 => x • x_1) r) a = (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r)) a}

case h.refine'_2
α : Type ?u.206596
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_1
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion ((fun x => A) r)
a : (fun x => A) r
⊢ Completion.map ((fun x x_1 => x • x_1) r) (↑((fun x => A) r) a) =
    (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r)) (↑((fun x => A) r) a)
case h
α : Type ?u.206596
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_1
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion ((fun x => A) r)
⊢ Completion.map ((fun x x_1 => x • x_1) r) x = (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r)) x
refine' Completion.induction_on x _ fun a => _
no goals
case h.refine'_1
α : Type ?u.206596
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_1
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion ((fun x => A) r)
⊢ IsClosed
    {a |
      Completion.map ((fun x x_1 => x • x_1) r) a = (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r)) a}
exact isClosed_eq Completion.continuous_map (continuous_mul_left _)
no goals
case h.refine'_2
α : Type ?u.206596
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_1
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion ((fun x => A) r)
a : (fun x => A) r
⊢ Completion.map ((fun x x_1 => x • x_1) r) (↑((fun x => A) r) a) =
    (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r)) (↑((fun x => A) r) a)
simp_rw [map_coe (uniformContinuous_const_smul r) a, Algebra.smul_def, coe_mul]