-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem normalize_eq_normalize {a b : α} (hab : a ∣ b) (hba : b ∣ a) :
    normalize a = normalize b

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
⊢ a = 0 → normalize a = normalize (a * ↑u)

Tactic:
rintro rfl

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a✝ : Nontrivial α
u : αˣ
hab : 0 ∣ 0 * ↑u
hba : 0 * ↑u ∣ 0
⊢ normalize 0 = normalize (0 * ↑u)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a✝ : Nontrivial α
u : αˣ
hab : 0 ∣ 0 * ↑u
hba : 0 * ↑u ∣ 0
⊢ normalize 0 = normalize (0 * ↑u)

Tactic:
simp only [zero_mul]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a b : α
hab : a ∣ b
hba : b ∣ a
⊢ normalize a = normalize b

Tactic:
nontriviality α

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a b : α
hab : a ∣ b
hba : b ∣ a
a✝ : Nontrivial α
⊢ normalize a = normalize b

Proof state:
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
ha : a ≠ 0
⊢ normalize a = normalize (a * ↑u)

Tactic:
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]

Result:
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
ha : a ≠ 0
⊢ a * ↑(normUnit a) = a * ↑u * ↑(normUnit a) * ↑u⁻¹

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a b : α
hab : a ∣ b
hba : b ∣ a
a✝ : Nontrivial α
⊢ normalize a = normalize b

Tactic:
rcases associated_of_dvd_dvd hab hba with ⟨u, rfl⟩

Result:
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
⊢ normalize a = normalize (a * ↑u)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
ha : a ≠ 0
⊢ a * ↑(normUnit a) * ↑u * ↑u⁻¹ = a * ↑u * ↑(normUnit a) * ↑u⁻¹

Tactic:
rw [mul_right_comm a]

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
⊢ normalize a = normalize (a * ↑u)

Tactic:
refine by_cases (by rintro rfl; simp only [zero_mul]) fun ha : a ≠ 0 => ?_

Result:
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
ha : a ≠ 0
⊢ normalize a = normalize (a * ↑u)

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
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)

Tactic:
simpa only [normalize_apply, mul_assoc, normUnit_mul ha u.ne_zero, normUnit_coe_units]

Result:
no goals

Proof state:
case intro
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
u : αˣ
hab : a ∣ a * ↑u
hba : a * ↑u ∣ a
ha : a ≠ 0
⊢ a * ↑(normUnit a) = a * ↑u * ↑(normUnit a) * ↑u⁻¹

Tactic:
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]

Result:
no goals