Theorem: ℤθ.norm_divides (Mordell4/CubicRing.lean)

State before:
a✝ b c p a : ℤθ
h : p ∣ a
⊢ norm p ∣ norm a
Tactic:
cases' h with n hn
State after:
case intro
a✝ b c p a n : ℤθ
hn : a = p * n
⊢ norm p ∣ norm a

State before:
case intro
a✝ b c p a n : ℤθ
hn : a = p * n
⊢ norm p ∣ norm a
Tactic:
use norm n
State after:
case h
a✝ b c p a n : ℤθ
hn : a = p * n
⊢ norm a = norm p * norm n

State before:
case h
a✝ b c p a n : ℤθ
hn : a = p * n
⊢ norm a = norm p * norm n
Tactic:
rw [norm_hMul p n]
State after:
case h
a✝ b c p a n : ℤθ
hn : a = p * n
⊢ norm a = norm (p * n)

State before:
case h
a✝ b c p a n : ℤθ
hn : a = p * n
⊢ norm a = norm (p * n)
Tactic:
rw [hn]
State after:
no goals