Theorem: Zsqrtd.associated_norm_of_associated (FltRegular/FltThree/Edwards.lean)

State before:
d : ℤ
f g : ℤ√d
h : Associated f g
⊢ Associated f.norm g.norm
Tactic:
obtain ⟨u, rfl⟩ := h
State after:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
⊢ Associated f.norm (f * ↑u).norm

State before:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
⊢ Associated f.norm (f * ↑u).norm
Tactic:
have := (Zsqrtd.isUnit_iff_norm_isUnit u).mp u.isUnit
State after:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (↑u).norm
⊢ Associated f.norm (f * ↑u).norm

State before:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (↑u).norm
⊢ Associated f.norm (f * ↑u).norm
Tactic:
rw [Zsqrtd.norm_mul]
State after:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (↑u).norm
⊢ Associated f.norm (f.norm * (↑u).norm)

State before:
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (↑u).norm
⊢ Associated f.norm (f.norm * (↑u).norm)
Tactic:
exact associated_mul_unit_right (Zsqrtd.norm f) _ this
State after:
no goals