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

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

case inr.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hpprime : p.norm.natAbs.Prime
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm

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

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

State before:
case inl
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 4
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm
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 ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 4
heven : Even a.norm
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm

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

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hp : p.norm.natAbs = 4
⊢ p.norm = 4
Tactic:
rw [← Zsqrt3.norm_natAbs]
State after:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hp : p.norm.natAbs = 4
⊢ ↑p.norm.natAbs = 4

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

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

State before:
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : 4 ∣ a.norm
hq : p.im ≠ 0
hp : p.norm = 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 : p.norm ∣ a.norm
hq : p.im ≠ 0
hpprime : p.norm.natAbs.Prime
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
Tactic:
rw [← Int.prime_iff_natAbs_prime] at hpprime
State after:
case inr.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hpprime : Prime p.norm
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm

State before:
case inr.intro
a p : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hdvd : p.norm ∣ a.norm
hq : p.im ≠ 0
hpprime : Prime p.norm
⊢ ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm
Tactic:
apply step2 hcoprime hdvd hpprime
State after:
no goals