apply associated'_of_associated_norm hxy
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hf' : ∀ (x : ℤ√(-3)), x ∈ f → IsCoprime x.re x.im
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hg' : ∀ (x : ℤ√(-3)), x ∈ g → IsCoprime x.re x.im
h : Associated (Multiset.prod f) (Multiset.prod g)
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
⊢ Associated' x y
case hx
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hf' : ∀ (x : ℤ√(-3)), x ∈ f → IsCoprime x.re x.im
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hg' : ∀ (x : ℤ√(-3)), x ∈ g → IsCoprime x.re x.im
h : Associated (Multiset.prod f) (Multiset.prod g)
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
⊢ IsCoprime x.re x.im

case hy
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hf' : ∀ (x : ℤ√(-3)), x ∈ f → IsCoprime x.re x.im
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hg' : ∀ (x : ℤ√(-3)), x ∈ g → IsCoprime x.re x.im
h : Associated (Multiset.prod f) (Multiset.prod g)
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
⊢ IsCoprime y.re y.im

case h'
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hf' : ∀ (x : ℤ√(-3)), x ∈ f → IsCoprime x.re x.im
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hg' : ∀ (x : ℤ√(-3)), x ∈ g → IsCoprime x.re x.im
h : Associated (Multiset.prod f) (Multiset.prod g)
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)
⊢ OddPrimeOrFour (Zsqrtd.norm x)