Theorem: factors_unique (FltRegular/FltThree/Edwards.lean)

State before:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
p : ∀ x ∈ f, ∀ y ∈ g, (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y → Associated' x y
⊢ Multiset.Rel Associated' f g
Tactic:
refine' Multiset.Rel.mono _ p
State after:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
p : ∀ x ∈ f, ∀ y ∈ g, (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y → Associated' x y
⊢ Multiset.Rel (fun a b => (Int.natAbs ∘ Zsqrtd.norm) a = (Int.natAbs ∘ Zsqrtd.norm) b) f g

State before:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
p : ∀ x ∈ f, ∀ y ∈ g, (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y → Associated' x y
⊢ Multiset.Rel (fun a b => (Int.natAbs ∘ Zsqrtd.norm) a = (Int.natAbs ∘ Zsqrtd.norm) b) f g
Tactic:
rw [← Multiset.rel_map, factors_unique_prod hf hg <| Zsqrtd.associated_norm_of_associated h,
  Multiset.rel_eq]
State after:
no goals

State before:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
⊢ ∀ x ∈ f, ∀ y ∈ g, (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y → Associated' x y
Tactic:
intro x hx y hy hxy
State after:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y
⊢ Associated' x y

State before:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : (Int.natAbs ∘ Zsqrtd.norm) x = (Int.natAbs ∘ Zsqrtd.norm) y
⊢ Associated' x y
Tactic:
rw [Function.comp_apply, Function.comp_apply, ← Int.associated_iff_natAbs] at hxy
State after:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated x.norm y.norm
⊢ Associated' x y

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

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

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

State before:
case hx
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated x.norm y.norm
⊢ IsCoprime x.re x.im
Tactic:
exact hf' x hx
State after:
no goals

State before:
case hy
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated x.norm y.norm
⊢ IsCoprime y.re y.im
Tactic:
exact hg' y hy
State after:
no goals

State before:
case h'
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hf' : ∀ x ∈ f, IsCoprime x.re x.im
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hg' : ∀ x ∈ g, IsCoprime x.re x.im
h : Associated f.prod g.prod
x : ℤ√(-3)
hx : x ∈ f
y : ℤ√(-3)
hy : y ∈ g
hxy : Associated x.norm y.norm
⊢ OddPrimeOrFour x.norm.natAbs
Tactic:
exact hf x hx
State after:
no goals