Theorem: associated'_of_associated_norm (Flt/Edwards.lean)

State before:
x y : ℤ√(-3)
h : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour (Zsqrtd.norm x)
⊢ 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 (Zsqrtd.norm x) (Zsqrtd.norm y)
hx : IsCoprime x.re x.im
hy : IsCoprime y.re y.im
h' : OddPrimeOrFour (Zsqrtd.norm x)
heq : Zsqrtd.norm x = Zsqrtd.norm y
⊢ Associated' x y

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

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

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