α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a b : α
hab : a ∣ b
hba : b ∣ a
✝ : Nontrivial α
⊢ ↑normalize a = ↑normalize b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a b : α
hab : a ∣ b
hba : b ∣ a
⊢ ↑normalize a = ↑normalize b
nontriviality α
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
⊢ ↑normalize a = ↑normalize (a * ↑u)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a b : α
hab : a ∣ b
hba : b ∣ a
✝ : Nontrivial α
⊢ ↑normalize a = ↑normalize b
rcases associated_of_dvd_dvd hab hba with ⟨u, rfl⟩
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
ha : a ≠ 0
⊢ ↑normalize a = ↑normalize (a * ↑u)
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
⊢ ↑normalize a = ↑normalize (a * ↑u)
refine' by_cases (by rintro rfl; simp only [zero_mul]) fun ha : a ≠ 0 => _
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
ha : a ≠ 0
⊢ a * ↑(normUnit a) = a * ↑u * ↑(normUnit a) * ↑u⁻¹
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
ha : a ≠ 0
⊢ ↑normalize a = ↑normalize (a * ↑u)
suffices a * ↑(normUnit a) = a * ↑u * ↑(normUnit a) * ↑u⁻¹ by
  simpa only [normalize_apply, mul_assoc, normUnit_mul ha u.ne_zero, normUnit_coe_units]
no goals
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
ha : a ≠ 0
⊢ a * ↑(normUnit a) = a * ↑u * ↑(normUnit a) * ↑u⁻¹
calc
  a * ↑(normUnit a) = a * ↑(normUnit a) * ↑u * ↑u⁻¹ := (Units.mul_inv_cancel_right _ _).symm
  _ = a * ↑u * ↑(normUnit a) * ↑u⁻¹ := by rw [mul_right_comm a]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
✝ : Nontrivial α
u : αˣ
hab : 0 ∣ 0 * ↑u
hba : 0 * ↑u ∣ 0
⊢ ↑normalize 0 = ↑normalize (0 * ↑u)
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
⊢ a = 0 → ↑normalize a = ↑normalize (a * ↑u)
rintro rfl
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
✝ : Nontrivial α
u : αˣ
hab : 0 ∣ 0 * ↑u
hba : 0 * ↑u ∣ 0
⊢ ↑normalize 0 = ↑normalize (0 * ↑u)
simp only [zero_mul]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
ha : a ≠ 0
this : a * ↑(normUnit a) = a * ↑u * ↑(normUnit a) * ↑u⁻¹
⊢ ↑normalize a = ↑normalize (a * ↑u)
simpa only [normalize_apply, mul_assoc, normUnit_mul ha u.ne_zero, normUnit_coe_units]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
ha : a ≠ 0
⊢ a * ↑(normUnit a) * ↑u * ↑u⁻¹ = a * ↑u * ↑(normUnit a) * ↑u⁻¹
rw [mul_right_comm a]