Theorem: step1' (Flt/Edwards.lean)

State before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
⊢ ∃ u, IsCoprime u.re u.im ∧ Zsqrtd.norm a = 4 * Zsqrtd.norm u
Tactic:
obtain ⟨u', hu'⟩ := step1 hcoprime heven
State after:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
u' : ℤ√(-3)
hu' : a = { re := 1, im := 1 } * u' ∨ a = { re := 1, im := -1 } * u'
⊢ ∃ u, IsCoprime u.re u.im ∧ Zsqrtd.norm a = 4 * Zsqrtd.norm u

State before:
case intro
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
u' : ℤ√(-3)
hu' : a = { re := 1, im := 1 } * u' ∨ a = { re := 1, im := -1 } * u'
⊢ ∃ u, IsCoprime u.re u.im ∧ Zsqrtd.norm a = 4 * Zsqrtd.norm u
Tactic:
refine' ⟨u', _, _⟩
State after:
case intro.refine'_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
u' : ℤ√(-3)
hu' : a = { re := 1, im := 1 } * u' ∨ a = { re := 1, im := -1 } * u'
⊢ IsCoprime u'.re u'.im

case intro.refine'_2
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
u' : ℤ√(-3)
hu' : a = { re := 1, im := 1 } * u' ∨ a = { re := 1, im := -1 } * u'
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm u'

State before:
case intro.refine'_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
u' : ℤ√(-3)
hu' : a = { re := 1, im := 1 } * u' ∨ a = { re := 1, im := -1 } * u'
⊢ IsCoprime u'.re u'.im
Tactic:
apply Zsqrtd.coprime_of_dvd_coprime hcoprime
State after:
case intro.refine'_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
u' : ℤ√(-3)
hu' : a = { re := 1, im := 1 } * u' ∨ a = { re := 1, im := -1 } * u'
⊢ u' ∣ a

State before:
case intro.refine'_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
u' : ℤ√(-3)
hu' : a = { re := 1, im := 1 } * u' ∨ a = { re := 1, im := -1 } * u'
⊢ u' ∣ a
Tactic:
obtain rfl | rfl := hu' <;> apply dvd_mul_left
State after:
no goals

State before:
case intro.refine'_2.inr
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
u' : ℤ√(-3)
hu' : a = { re := 1, im := -1 } * u'
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm u'
Tactic:
rw [hu', Zsqrtd.norm_mul]
State after:
case intro.refine'_2.inr
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
u' : ℤ√(-3)
hu' : a = { re := 1, im := -1 } * u'
⊢ Zsqrtd.norm { re := 1, im := -1 } * Zsqrtd.norm u' = 4 * Zsqrtd.norm u'

State before:
case intro.refine'_2.inr
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
u' : ℤ√(-3)
hu' : a = { re := 1, im := -1 } * u'
⊢ Zsqrtd.norm { re := 1, im := -1 } * Zsqrtd.norm u' = 4 * Zsqrtd.norm u'
Tactic:
congr
State after:
no goals