α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
✝ : Nontrivial α
⊢ normUnit (a * ↑(normUnit a)) = 1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
⊢ normUnit (a * ↑(normUnit a)) = 1
nontriviality α using Subsingleton.elim a 0
case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
✝ : Nontrivial α
⊢ normUnit (0 * ↑(normUnit 0)) = 1

case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
✝ : Nontrivial α
h : a ≠ 0
⊢ normUnit (a * ↑(normUnit a)) = 1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
✝ : Nontrivial α
⊢ normUnit (a * ↑(normUnit a)) = 1
obtain rfl | h := eq_or_ne a 0
no goals
case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
✝ : Nontrivial α
⊢ normUnit (0 * ↑(normUnit 0)) = 1
rw [normUnit_zero, zero_mul, normUnit_zero]
no goals
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
✝ : Nontrivial α
h : a ≠ 0
⊢ normUnit (a * ↑(normUnit a)) = 1
rw [normUnit_mul h (Units.ne_zero _), normUnit_coe_units, mul_inv_eq_one]