Theorem: Spts.four_of_coprime (Flt/Spts.lean)

State before:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : Zsqrtd.norm p = 4
⊢ abs p.re = 1 ∧ abs p.im = 1
Tactic:
apply Spts.four hfour
State after:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : Zsqrtd.norm p = 4
⊢ p.im ≠ 0

State before:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : Zsqrtd.norm p = 4
⊢ p.im ≠ 0
Tactic:
rintro him
State after:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : Zsqrtd.norm p = 4
him : p.im = 0
⊢ False

State before:
p : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hfour : Zsqrtd.norm p = 4
him : p.im = 0
⊢ False
Tactic:
rw [him, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime
State after:
p : ℤ√(-3)
hcoprime : abs p.re = 1
hfour : Zsqrtd.norm p = 4
him : p.im = 0
⊢ False

State before:
p : ℤ√(-3)
hcoprime : abs p.re = 1
hfour : Zsqrtd.norm p = 4
him : p.im = 0
⊢ False
Tactic:
rw [Zsqrtd.norm_def, him, MulZeroClass.mul_zero, sub_zero, ← sq, ← sq_abs, hcoprime] at hfour
State after:
p : ℤ√(-3)
hcoprime : abs p.re = 1
hfour : 1 ^ 2 = 4
him : p.im = 0
⊢ False

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