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

State before:
x y : ℤ√(-3)
hre : abs x.re = abs y.re
him : abs x.im = abs y.im
⊢ Associated' x y
Tactic:
rw [abs_eq_abs] at hre him
State after:
x y : ℤ√(-3)
hre : x.re = y.re ∨ x.re = -y.re
him : x.im = y.im ∨ x.im = -y.im
⊢ Associated' x y

State before:
x y : ℤ√(-3)
hre : x.re = y.re ∨ x.re = -y.re
him : x.im = y.im ∨ x.im = -y.im
⊢ Associated' x y
Tactic:
cases' hre with h1 h1 <;> cases' him with h2 h2 <;>
  [
    (left; use 1),
    (right; use 1),
    (right; use -1),
    (left; use -1)
  ] <;>
  simp [Zsqrtd.ext, h1, h2]
State after:
no goals

State before:
case inl.inl
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = y.im
⊢ Associated' x y
Tactic:
left
State after:
case inl.inl.h
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = y.im
⊢ Associated x y

State before:
case inl.inl.h
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = y.im
⊢ Associated x y
Tactic:
use 1
State after:
case inl.inl.h
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = y.im
⊢ x * ↑1 = y

State before:
case inl.inr
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = -y.im
⊢ Associated' x y
Tactic:
right
State after:
case inl.inr.h
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = -y.im
⊢ Associated x (star y)

State before:
case inl.inr.h
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = -y.im
⊢ Associated x (star y)
Tactic:
use 1
State after:
case inl.inr.h
x y : ℤ√(-3)
h1 : x.re = y.re
h2 : x.im = -y.im
⊢ x * ↑1 = star y

State before:
case inr.inl
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = y.im
⊢ Associated' x y
Tactic:
right
State after:
case inr.inl.h
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = y.im
⊢ Associated x (star y)

State before:
case inr.inl.h
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = y.im
⊢ Associated x (star y)
Tactic:
use -1
State after:
case inr.inl.h
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = y.im
⊢ x * ↑(-1) = star y

State before:
case inr.inr
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = -y.im
⊢ Associated' x y
Tactic:
left
State after:
case inr.inr.h
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = -y.im
⊢ Associated x y

State before:
case inr.inr.h
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = -y.im
⊢ Associated x y
Tactic:
use -1
State after:
case inr.inr.h
x y : ℤ√(-3)
h1 : x.re = -y.re
h2 : x.im = -y.im
⊢ x * ↑(-1) = y