Theorem: step1_2 (Flt/Edwards.lean)

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hp : OddPrimeOrFour (Zsqrtd.norm p)
hq : p.im ≠ 0
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u
Tactic:
obtain hp | ⟨hpprime, -⟩ := hp
State after:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hq : p.im ≠ 0
hp : Zsqrtd.norm p = 4
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u

case inr.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hq : p.im ≠ 0
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

State before:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hq : p.im ≠ 0
hp : Zsqrtd.norm p = 4
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u
Tactic:
rw [hp] at hdvd⊢
State after:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ Zsqrtd.norm a
hq : p.im ≠ 0
hp : Zsqrtd.norm p = 4
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = 4 * Zsqrtd.norm u

State before:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ Zsqrtd.norm a
hq : p.im ≠ 0
hp : Zsqrtd.norm p = 4
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = 4 * Zsqrtd.norm u
Tactic:
have heven : Even a.norm :=
  by
  apply even_iff_two_dvd.mpr (dvd_trans _ hdvd)
  norm_num
State after:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ Zsqrtd.norm a
hq : p.im ≠ 0
hp : Zsqrtd.norm p = 4
heven : Even (Zsqrtd.norm a)
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = 4 * Zsqrtd.norm u

State before:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ Zsqrtd.norm a
hq : p.im ≠ 0
hp : Zsqrtd.norm p = 4
heven : Even (Zsqrtd.norm a)
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = 4 * Zsqrtd.norm u
Tactic:
exact step1'' hcoprime hp hq heven
State after:
no goals

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ Zsqrtd.norm a
hq : p.im ≠ 0
hp : Zsqrtd.norm p = 4
⊢ Even (Zsqrtd.norm a)
Tactic:
apply even_iff_two_dvd.mpr (dvd_trans _ hdvd)
State after:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ Zsqrtd.norm a
hq : p.im ≠ 0
hp : Zsqrtd.norm p = 4
⊢ 2 ∣ 4

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ Zsqrtd.norm a
hq : p.im ≠ 0
hp : Zsqrtd.norm p = 4
⊢ 2 ∣ 4
Tactic:
norm_num
State after:
no goals

State before:
case inr.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hq : p.im ≠ 0
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:
apply step2 hcoprime hdvd hpprime
State after:
no goals