p x : ℝ
⊢ ‖↑(-1 * x)‖ = ‖↑x‖
p x : ℝ
⊢ ‖↑x‖ = ‖↑x‖
suffices ‖(↑(-1 * x) : AddCircle (-1 * p))‖ = ‖(x : AddCircle p)‖ by
  rw [← this, neg_one_mul]
  simp
no goals
p x : ℝ
⊢ ‖↑(-1 * x)‖ = ‖↑x‖
simp only [norm_coe_mul, abs_neg, abs_one, one_mul]
p x : ℝ
this : ‖↑(-1 * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = ‖↑(-1 * x)‖
p x : ℝ
this : ‖↑(-1 * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = ‖↑x‖
rw [← this, neg_one_mul]
no goals
p x : ℝ
this : ‖↑(-1 * x)‖ = ‖↑x‖
⊢ ‖↑x‖ = ‖↑(-1 * x)‖
simp