[GOAL]
e : ℤˣ
⊢ ‖↑e‖₊ = 1
[PROOFSTEP]
obtain rfl | rfl := units_eq_one_or e
[GOAL]
case inl
⊢ ‖↑1‖₊ = 1
[PROOFSTEP]
simp only [Units.coe_neg_one, Units.val_one, nnnorm_neg, nnnorm_one]
[GOAL]
case inr
⊢ ‖↑(-1)‖₊ = 1
[PROOFSTEP]
simp only [Units.coe_neg_one, Units.val_one, nnnorm_neg, nnnorm_one]
[GOAL]
e : ℤˣ
⊢ ‖↑e‖ = 1
[PROOFSTEP]
rw [← coe_nnnorm, nnnorm_coe_units, NNReal.coe_one]
[GOAL]
n : ℤ
⊢ ↑(toNat n) + ↑(toNat (-n)) = ‖n‖₊
[PROOFSTEP]
rw [← Nat.cast_add, toNat_add_toNat_neg_eq_natAbs, NNReal.coe_natAbs]
[GOAL]
n : ℤ
⊢ ↑(toNat n) + ↑(toNat (-n)) = ‖n‖
[PROOFSTEP]
simpa only [NNReal.coe_nat_cast, NNReal.coe_add] using congrArg NNReal.toReal (toNat_add_toNat_neg_eq_nnnorm n)
