Theorem: step2 (FltRegular/FltThree/Edwards.lean)

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

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

State before:
case intro.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
u' : ℤ√(-3)
h : a = p * u' ∨ a = star p * u'
h' : a.norm = p.norm * u'.norm
⊢ IsCoprime u'.re u'.im
Tactic:
apply Zsqrtd.coprime_of_dvd_coprime hcoprime
State after:
case intro.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
u' : ℤ√(-3)
h : a = p * u' ∨ a = star p * u'
h' : a.norm = p.norm * u'.norm
⊢ u' ∣ a

State before:
case intro.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hpprime : Prime p.norm
u' : ℤ√(-3)
h : a = p * u' ∨ a = star p * u'
h' : a.norm = p.norm * u'.norm
⊢ u' ∣ a
Tactic:
obtain rfl | rfl := h <;> apply dvd_mul_left
State after:
no goals