Theorem: OddPrimeOrFour.im_ne_zero (FltRegular/FltThree/Edwards.lean)

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

State before:
p : ℤ√(-3)
h : OddPrimeOrFour p.norm.natAbs
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).natAbs
hcoprime : IsCoprime p.re p.im
H : p.im = 0
⊢ False

State before:
p : ℤ√(-3)
h : OddPrimeOrFour (p.re ^ 2).natAbs
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).natAbs = 4
⊢ False

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

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

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

State before:
case inl
p : ℤ√(-3)
hcoprime : |p.re| = 1
H : p.im = 0
h : (1 ^ 2).natAbs = 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 : (p.re ^ 2).natAbs.Prime
⊢ False
Tactic:
rw [Int.natAbs_pow] at hp
State after:
case inr.intro
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
H : p.im = 0
hp : (p.re.natAbs ^ 2).Prime
⊢ False

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