case h
M : Type ?u.263181
R : Type ?u.263184
α : Type u_1
β : Type u_2
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
M : Type ?u.263181
R : Type ?u.263184
α : Type u_1
β : Type u_2
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
⊢ completion 0 (_ : Continuous fun x => AddZeroClass.toZero.1) = 0
ext x
case h.refine_1
M : Type ?u.263181
R : Type ?u.263184
α : Type u_1
β : Type u_2
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}

case h.refine_2
M : Type ?u.263181
R : Type ?u.263184
α : Type u_1
β : Type u_2
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)
case h
M : Type ?u.263181
R : Type ?u.263184
α : Type u_1
β : Type u_2
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
refine Completion.induction_on x ?_ ?_
case h.refine_1
M : Type ?u.263181
R : Type ?u.263184
α : Type u_1
β : Type u_2
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ Continuous fun x => ↑0 x
case h.refine_1
M : Type ?u.263181
R : Type ?u.263184
α : Type u_1
β : Type u_2
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}
apply isClosed_eq (AddMonoidHom.continuous_completion (0 : α →+ β) continuous_const)
no goals
case h.refine_1
M : Type ?u.263181
R : Type ?u.263184
α : Type u_1
β : Type u_2
inst✝⁵ : UniformSpace α
inst✝⁴ : AddGroup α
inst✝³ : UniformAddGroup α
inst✝² : UniformSpace β
inst✝¹ : AddGroup β
inst✝ : UniformAddGroup β
x : Completion α
⊢ Continuous fun x => ↑0 x
simp [continuous_const]
case h.refine_2
M : Type ?u.263181
R : Type ?u.263184
α : Type u_1
β : Type u_2
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)
case h.refine_2
M : Type ?u.263181
R : Type ?u.263184
α : Type u_1
β : Type u_2
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)
intro a
no goals
case h.refine_2
M : Type ?u.263181
R : Type ?u.263184
α : Type u_1
β : Type u_2
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)
simp [(0 : α →+ β).completion_coe continuous_const, coe_zero]