Theorem: factorization'.associated'_of_norm_eq (Flt/Edwards.lean)

State before:
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ Associated' b c
Tactic:
apply associated'_of_associated_norm
State after:
case h
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ Associated (Zsqrtd.norm b) (Zsqrtd.norm c)

case hx
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ IsCoprime b.re b.im

case hy
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ IsCoprime c.re c.im

case h'
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ OddPrimeOrFour (Zsqrtd.norm b)

State before:
case h
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ Associated (Zsqrtd.norm b) (Zsqrtd.norm c)
Tactic:
rw [hnorm]
State after:
no goals

State before:
case hx
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ IsCoprime b.re b.im
Tactic:
exact factorization'.coprime_of_mem h hbmem
State after:
no goals

State before:
case hy
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ IsCoprime c.re c.im
Tactic:
exact factorization'.coprime_of_mem h hcmem
State after:
no goals

State before:
case h'
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Zsqrtd.norm b = Zsqrtd.norm c
⊢ OddPrimeOrFour (Zsqrtd.norm b)
Tactic:
exact ((factorization'_prop h).2 b hbmem).2.2
State after:
no goals