Theorem: OddPrimeOrFour.im_ne_zero (Flt/Edwards.lean)

State before:
p : ℤ√(-3)
h : OddPrimeOrFour (Zsqrtd.norm p)
hcoprime : IsCoprime p.re p.im
⊢ p.im ≠ 0
Tactic:
intro H
State after:
p : ℤ√(-3)
h : OddPrimeOrFour (Zsqrtd.norm p)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
⊢ False

State before:
p : ℤ√(-3)
h : OddPrimeOrFour (Zsqrtd.norm p)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
⊢ False
Tactic:
rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two] at h
State after:
p : ℤ√(-3)
h : OddPrimeOrFour (p.re ^ 2)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
⊢ False

State before:
p : ℤ√(-3)
h : OddPrimeOrFour (p.re ^ 2)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
⊢ False
Tactic:
obtain h | ⟨hp, -⟩ := h
State after:
case inl
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
h : p.re ^ 2 = 4
⊢ False

case inr.intro
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
hp : Prime (p.re ^ 2)
⊢ False

State before:
case inl
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
h : p.re ^ 2 = 4
⊢ False
Tactic:
rw [H, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime
State after:
case inl
p : ℤ√(-3)
hcoprime : Abs.abs p.re = 1
H : p.im = 0
h : p.re ^ 2 = 4
⊢ False

State before:
case inl
p : ℤ√(-3)
hcoprime : Abs.abs p.re = 1
H : p.im = 0
h : p.re ^ 2 = 4
⊢ False
Tactic:
rw [← sq_abs, hcoprime] at h
State after:
case inl
p : ℤ√(-3)
hcoprime : Abs.abs p.re = 1
H : p.im = 0
h : 1 ^ 2 = 4
⊢ False

State before:
case inl
p : ℤ√(-3)
hcoprime : Abs.abs p.re = 1
H : p.im = 0
h : 1 ^ 2 = 4
⊢ False
Tactic:
norm_num at h
State after:
no goals

State before:
case inr.intro
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
hp : Prime (p.re ^ 2)
⊢ False
Tactic:
exact pow_not_prime one_lt_two.ne' hp
State after:
no goals