Theorem: Spts.mul_of_dvd'' (FltRegular/FltThree/Spts.lean)

State before:
a p : ℤ√(-3)
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
⊢ ∃ u, (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
Tactic:
obtain ⟨u, hu⟩ := Spts.mul_of_dvd' hdvd hpprime
State after:
case intro
a p : ℤ√(-3)
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
u : ℤ√(-3)
hu : a = p * u ∨ a = star p * u
⊢ ∃ u, (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm

State before:
case intro
a p : ℤ√(-3)
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
u : ℤ√(-3)
hu : a = p * u ∨ a = star p * u
⊢ ∃ u, (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
Tactic:
refine' ⟨u, hu, _⟩
State after:
case intro
a p : ℤ√(-3)
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
u : ℤ√(-3)
hu : a = p * u ∨ a = star p * u
⊢ a.norm = p.norm * u.norm

State before:
case intro
a p : ℤ√(-3)
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
u : ℤ√(-3)
hu : a = p * u ∨ a = star p * u
⊢ a.norm = p.norm * u.norm
Tactic:
obtain rfl | rfl := hu
State after:
case intro.inl
p : ℤ√(-3)
hpprime : Prime p.norm
u : ℤ√(-3)
hdvd : p.norm ∣ (p * u).norm
⊢ (p * u).norm = p.norm * u.norm

case intro.inr
p : ℤ√(-3)
hpprime : Prime p.norm
u : ℤ√(-3)
hdvd : p.norm ∣ (star p * u).norm
⊢ (star p * u).norm = p.norm * u.norm

State before:
case intro.inl
p : ℤ√(-3)
hpprime : Prime p.norm
u : ℤ√(-3)
hdvd : p.norm ∣ (p * u).norm
⊢ (p * u).norm = p.norm * u.norm
Tactic:
rw [Zsqrtd.norm_mul]
State after:
no goals

State before:
case intro.inr
p : ℤ√(-3)
hpprime : Prime p.norm
u : ℤ√(-3)
hdvd : p.norm ∣ (star p * u).norm
⊢ (star p * u).norm = p.norm * u.norm
Tactic:
rw [Zsqrtd.norm_mul, Zsqrtd.norm_conj]
State after:
no goals