[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : UniformSpace α
inst✝³ : MonoidWithZero M
inst✝² : Zero α
inst✝¹ : MulActionWithZero M α
inst✝ : UniformContinuousConstSMul M α
src✝ : MulAction M (Completion α) := inferInstance
r : M
⊢ r • 0 = 0
[PROOFSTEP]
rw [← coe_zero, ← coe_smul, MulActionWithZero.smul_zero r]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁴ : UniformSpace α
inst✝³ : MonoidWithZero M
inst✝² : Zero α
inst✝¹ : MulActionWithZero M α
inst✝ : UniformContinuousConstSMul M α
src✝ : MulAction M (Completion α) := inferInstance
a : α
⊢ 0 • ↑α a = 0
[PROOFSTEP]
rw [← coe_smul, zero_smul, coe_zero]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝¹ : Zero (Completion α) := inferInstance
src✝ : Add (Completion α) := inferInstance
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑α a + ↑α b + ↑α c = ↑α a + (↑α b + ↑α c)
[PROOFSTEP]
repeat' rw_mod_cast [add_assoc]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝¹ : Zero (Completion α) := inferInstance
src✝ : Add (Completion α) := inferInstance
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑α a + ↑α b + ↑α c = ↑α a + (↑α b + ↑α c)
[PROOFSTEP]
rw_mod_cast [add_assoc]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝¹ : Zero (Completion α) := inferInstance
src✝ : Add (Completion α) := inferInstance
a✝ : Completion α
a : α
⊢ 0 + ↑α a = ↑α a
[PROOFSTEP]
rw [← coe_zero, ← coe_add, zero_add]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝¹ : Zero (Completion α) := inferInstance
src✝ : Add (Completion α) := inferInstance
a✝ : Completion α
a : α
⊢ ↑α a + 0 = ↑α a
[PROOFSTEP]
rw [← coe_zero, ← coe_add, add_zero]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝¹ : Zero (Completion α) := inferInstance
src✝ : Add (Completion α) := inferInstance
a✝ : Completion α
a : α
⊢ 0 • ↑α a = 0
[PROOFSTEP]
rw [← coe_smul, ← coe_zero, zero_smul]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝¹ : Zero (Completion α) := inferInstance
src✝ : Add (Completion α) := inferInstance
n : ℕ
a✝ : Completion α
a : α
⊢ (n + 1) • ↑α a = ↑α a + n • ↑α a
[PROOFSTEP]
rw [← coe_smul, succ_nsmul, coe_add, coe_smul]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝² : AddMonoid (Completion α) := inferInstance
src✝¹ : Neg (Completion α) := inferInstance
src✝ : Sub (Completion α) := inferInstance
a✝ b✝ : Completion α
a b : α
⊢ ↑α a - ↑α b = ↑α a + -↑α b
[PROOFSTEP]
exact_mod_cast congr_arg ((↑) : α → Completion α) (sub_eq_add_neg a b)
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝² : AddMonoid (Completion α) := inferInstance
src✝¹ : Neg (Completion α) := inferInstance
src✝ : Sub (Completion α) := inferInstance
a✝ : Completion α
a : α
⊢ 0 • ↑α a = 0
[PROOFSTEP]
rw [← coe_smul, ← coe_zero, zero_smul]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝² : AddMonoid (Completion α) := inferInstance
src✝¹ : Neg (Completion α) := inferInstance
src✝ : Sub (Completion α) := inferInstance
n : ℕ
a✝ : Completion α
a : α
⊢ Int.ofNat (Nat.succ n) • ↑α a = ↑α a + (fun x x_1 => x • x_1) (Int.ofNat n) (↑α a)
[PROOFSTEP]
rw [← coe_smul, show Int.ofNat n.succ • a = a + Int.ofNat n • a from SubNegMonoid.zsmul_succ' n a, coe_add, coe_smul]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝² : AddMonoid (Completion α) := inferInstance
src✝¹ : Neg (Completion α) := inferInstance
src✝ : Sub (Completion α) := inferInstance
n : ℕ
a✝ : Completion α
a : α
⊢ Int.negSucc n • ↑α a = -(fun x x_1 => x • x_1) (↑(Nat.succ n)) (↑α a)
[PROOFSTEP]
rw [← coe_smul, show (Int.negSucc n) • a = -((n.succ : ℤ) • a) from SubNegMonoid.zsmul_neg' n a, coe_neg, coe_smul]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝ : SubNegMonoid (Completion α) := inferInstance
a✝ : Completion α
a : α
⊢ -↑α a + ↑α a = 0
[PROOFSTEP]
rw_mod_cast [add_left_neg]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddGroup α
inst✝ : UniformAddGroup α
src✝ : SubNegMonoid (Completion α) := inferInstance
a✝ : Completion α
a : α
⊢ ↑α 0 = 0
[PROOFSTEP]
rfl
[GOAL]
M✝ : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
M : Type ?u.31551
inst✝² : Monoid M
inst✝¹ : DistribMulAction M α
inst✝ : UniformContinuousConstSMul M α
src✝ : MulAction M (Completion α) := inferInstance
r : M
⊢ r • 0 = 0
[PROOFSTEP]
rw [← coe_zero, ← coe_smul, smul_zero r]
[GOAL]
M✝ : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
M : Type ?u.31551
inst✝² : Monoid M
inst✝¹ : DistribMulAction M α
inst✝ : UniformContinuousConstSMul M α
src✝ : MulAction M (Completion α) := inferInstance
r : M
x y : Completion α
a b : α
⊢ r • (↑α a + ↑α b) = r • ↑α a + r • ↑α b
[PROOFSTEP]
simp only [← coe_add, ← coe_smul, smul_add]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddCommGroup α
inst✝ : UniformAddGroup α
src✝ : AddGroup (Completion α) := inferInstance
a b : Completion α
x y : α
⊢ ↑α x + ↑α y = ↑α y + ↑α x
[PROOFSTEP]
change (x : Completion α) + ↑y = ↑y + ↑x
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝² : UniformSpace α
inst✝¹ : AddCommGroup α
inst✝ : UniformAddGroup α
src✝ : AddGroup (Completion α) := inferInstance
a b : Completion α
x y : α
⊢ ↑α x + ↑α y = ↑α y + ↑α x
[PROOFSTEP]
rw [← coe_add, ← coe_add, add_comm]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddCommGroup α
inst✝³ : UniformAddGroup α
inst✝² : Semiring R
inst✝¹ : Module R α
inst✝ : UniformContinuousConstSMul R α
src✝¹ : DistribMulAction R (Completion α) := inferInstance
src✝ : MulActionWithZero R (Completion α) := inferInstance
a b : R
x : α
⊢ (a + b) • ↑α x = a • ↑α x + b • ↑α x
[PROOFSTEP]
rw [← coe_smul, add_smul, coe_add, coe_smul, coe_smul]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : UniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : UniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
f : α →+ β
hf✝ : Continuous ↑f
hf : UniformContinuous ↑f
⊢ Completion.extension (↑f) 0 = 0
[PROOFSTEP]
rw [← coe_zero, extension_coe hf, f.map_zero]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : UniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : UniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
f : α →+ β
hf✝ : Continuous ↑f
hf : UniformContinuous ↑f
a✝ b✝ : Completion α
a b : α
⊢ Completion.extension (↑f) (↑α a + ↑α b) = Completion.extension (↑f) (↑α a) + Completion.extension (↑f) (↑α b)
[PROOFSTEP]
rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf, f.map_add]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
⊢ completion 0 (_ : Continuous fun x => AddZeroClass.toZero.1) = 0
[PROOFSTEP]
ext x
[GOAL]
case h
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ ↑(completion 0 (_ : Continuous fun x => AddZeroClass.toZero.1)) x = ↑0 x
[PROOFSTEP]
refine Completion.induction_on x ?_ ?_
[GOAL]
case h.refine_1
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ IsClosed {a | ↑(completion 0 (_ : Continuous fun x => AddZeroClass.toZero.1)) a = ↑0 a}
[PROOFSTEP]
apply isClosed_eq (AddMonoidHom.continuous_completion (0 : α →+ β) continuous_const)
[GOAL]
case h.refine_1
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ Continuous fun x => ↑0 x
[PROOFSTEP]
simp [continuous_const]
[GOAL]
case h.refine_2
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ ∀ (a : α), ↑(completion 0 (_ : Continuous fun x => AddZeroClass.toZero.1)) (↑α a) = ↑0 (↑α a)
[PROOFSTEP]
intro a
[GOAL]
case h.refine_2
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
a : α
⊢ ↑(completion 0 (_ : Continuous fun x => AddZeroClass.toZero.1)) (↑α a) = ↑0 (↑α a)
[PROOFSTEP]
simp [(0 : α →+ β).completion_coe continuous_const, coe_zero]
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁸ : UniformSpace α
inst✝⁷ : AddGroup α
inst✝⁶ : UniformAddGroup α
inst✝⁵ : UniformSpace β
inst✝⁴ : AddGroup β
inst✝³ : UniformAddGroup β
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ↑f
hg : Continuous ↑g
⊢ completion (f + g) (_ : Continuous fun x => ↑f x + ↑g x) = completion f hf + completion g hg
[PROOFSTEP]
have hfg := hf.add hg
[GOAL]
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁸ : UniformSpace α
inst✝⁷ : AddGroup α
inst✝⁶ : UniformAddGroup α
inst✝⁵ : UniformSpace β
inst✝⁴ : AddGroup β
inst✝³ : UniformAddGroup β
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ↑f
hg : Continuous ↑g
hfg : Continuous fun x => ↑f x + ↑g x
⊢ completion (f + g) (_ : Continuous fun x => ↑f x + ↑g x) = completion f hf + completion g hg
[PROOFSTEP]
ext x
[GOAL]
case h
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁸ : UniformSpace α
inst✝⁷ : AddGroup α
inst✝⁶ : UniformAddGroup α
inst✝⁵ : UniformSpace β
inst✝⁴ : AddGroup β
inst✝³ : UniformAddGroup β
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ↑f
hg : Continuous ↑g
hfg : Continuous fun x => ↑f x + ↑g x
x : Completion α
⊢ ↑(completion (f + g) (_ : Continuous fun x => ↑f x + ↑g x)) x = ↑(completion f hf + completion g hg) x
[PROOFSTEP]
refine Completion.induction_on x ?_ ?_
[GOAL]
case h.refine_1
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁸ : UniformSpace α
inst✝⁷ : AddGroup α
inst✝⁶ : UniformAddGroup α
inst✝⁵ : UniformSpace β
inst✝⁴ : AddGroup β
inst✝³ : UniformAddGroup β
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ↑f
hg : Continuous ↑g
hfg : Continuous fun x => ↑f x + ↑g x
x : Completion α
⊢ IsClosed {a | ↑(completion (f + g) (_ : Continuous fun x => ↑f x + ↑g x)) a = ↑(completion f hf + completion g hg) a}
[PROOFSTEP]
exact isClosed_eq ((f + g).continuous_completion hfg) ((f.continuous_completion hf).add (g.continuous_completion hg))
[GOAL]
case h.refine_2
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁸ : UniformSpace α
inst✝⁷ : AddGroup α
inst✝⁶ : UniformAddGroup α
inst✝⁵ : UniformSpace β
inst✝⁴ : AddGroup β
inst✝³ : UniformAddGroup β
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ↑f
hg : Continuous ↑g
hfg : Continuous fun x => ↑f x + ↑g x
x : Completion α
⊢ ∀ (a : α),
    ↑(completion (f + g) (_ : Continuous fun x => ↑f x + ↑g x)) (↑α a) = ↑(completion f hf + completion g hg) (↑α a)
[PROOFSTEP]
intro a
[GOAL]
case h.refine_2
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁸ : UniformSpace α
inst✝⁷ : AddGroup α
inst✝⁶ : UniformAddGroup α
inst✝⁵ : UniformSpace β
inst✝⁴ : AddGroup β
inst✝³ : UniformAddGroup β
γ : Type u_5
inst✝² : AddCommGroup γ
inst✝¹ : UniformSpace γ
inst✝ : UniformAddGroup γ
f g : α →+ γ
hf : Continuous ↑f
hg : Continuous ↑g
hfg : Continuous fun x => ↑f x + ↑g x
x : Completion α
a : α
⊢ ↑(completion (f + g) (_ : Continuous fun x => ↑f x + ↑g x)) (↑α a) = ↑(completion f hf + completion g hg) (↑α a)
[PROOFSTEP]
simp [(f + g).completion_coe hfg, coe_add, f.completion_coe hf, g.completion_coe hg]
