Theorem: step2 (Flt/Edwards.lean)

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hpprime : Prime (Zsqrtd.norm p)
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u
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 : Zsqrtd.norm p ∣ Zsqrtd.norm a
hpprime : Prime (Zsqrtd.norm p)
u' : ℤ√(-3)
h : a = p * u' ∨ a = star p * u'
h' : Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u'
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u

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

State before:
case intro.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hpprime : Prime (Zsqrtd.norm p)
u' : ℤ√(-3)
h : a = p * u' ∨ a = star p * u'
h' : Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u'
⊢ 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 : Zsqrtd.norm p ∣ Zsqrtd.norm a
hpprime : Prime (Zsqrtd.norm p)
u' : ℤ√(-3)
h : a = p * u' ∨ a = star p * u'
h' : Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u'
⊢ u' ∣ a

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