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

State before:
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Associated b.norm c.norm
⊢ 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 : Associated b.norm c.norm
⊢ Associated b.norm c.norm

case hx
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Associated b.norm c.norm
⊢ 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 : Associated b.norm c.norm
⊢ 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 : Associated b.norm c.norm
⊢ OddPrimeOrFour b.norm.natAbs

State before:
case h
a b c : ℤ√(-3)
h : IsCoprime a.re a.im
hbmem : b ∈ factorization' h
hcmem : c ∈ factorization' h
hnorm : Associated b.norm c.norm
⊢ Associated b.norm c.norm
Tactic:
exact 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 : Associated b.norm c.norm
⊢ 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 : Associated b.norm c.norm
⊢ 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 : Associated b.norm c.norm
⊢ OddPrimeOrFour b.norm.natAbs
Tactic:
exact ((factorization'_prop h).2 b hbmem).2.2
State after:
no goals