Theorem: Spts.mul_of_dvd'' (Flt/Spts.lean)

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

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

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

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

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

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