Theorem: Zsqrtd.associated_norm_of_associated (Flt/Edwards.lean)

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

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

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

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