Theorem: associated'_of_associated_norm (FltRegular/FltThree/Edwards.lean)

State before:
x y : ℤ√(-3)
h : Associated x.norm y.norm
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour x.norm.natAbs
⊢ Associated' x y
Tactic:
have heq : x.norm = y.norm :=
  haveI hd : (-3 : ℤ) ≤ 0 := by norm_num
  Int.eq_of_associated_of_nonneg h (Zsqrtd.norm_nonneg hd _) (Zsqrtd.norm_nonneg hd _)
State after:
x y : ℤ√(-3)
h : Associated x.norm y.norm
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour x.norm.natAbs
heq : x.norm = y.norm
⊢ Associated' x y

State before:
x y : ℤ√(-3)
h : Associated x.norm y.norm
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour x.norm.natAbs
heq : x.norm = y.norm
⊢ Associated' x y
Tactic:
obtain ⟨hre, him⟩ := step4_3 hx hy h' heq
State after:
case intro
x y : ℤ√(-3)
h : Associated x.norm y.norm
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour x.norm.natAbs
heq : x.norm = y.norm
hre : |x.re| = |y.re|
him : |x.im| = |y.im|
⊢ Associated' x y

State before:
case intro
x y : ℤ√(-3)
h : Associated x.norm y.norm
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour x.norm.natAbs
heq : x.norm = y.norm
hre : |x.re| = |y.re|
him : |x.im| = |y.im|
⊢ Associated' x y
Tactic:
exact associated'_of_abs_eq hre him
State after:
no goals

State before:
x y : ℤ√(-3)
h : Associated x.norm y.norm
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour x.norm.natAbs
⊢ -3 ≤ 0
Tactic:
norm_num
State after:
no goals