Theorem: factors_unique_prod (Flt/Edwards.lean)

State before:
⊢ ∀ {f g : Multiset (ℤ√(-3))},
    (∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)) →
      (∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)) →
        Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g)) →
          Multiset.Rel Associated (Multiset.map Zsqrtd.norm f) (Multiset.map Zsqrtd.norm g)
Tactic:
intro f g hf hg hassoc
State after:
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
⊢ Multiset.Rel Associated (Multiset.map Zsqrtd.norm f) (Multiset.map Zsqrtd.norm g)

State before:
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
⊢ Multiset.Rel Associated (Multiset.map Zsqrtd.norm f) (Multiset.map Zsqrtd.norm g)
Tactic:
apply factors_unique_prod'
State after:
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
⊢ ∀ (x : ℤ), x ∈ Multiset.map Zsqrtd.norm f → OddPrimeOrFour x

case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
⊢ ∀ (x : ℤ), x ∈ Multiset.map Zsqrtd.norm g → OddPrimeOrFour x

case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
⊢ Associated (Multiset.prod (Multiset.map Zsqrtd.norm f)) (Multiset.prod (Multiset.map Zsqrtd.norm g))

State before:
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
⊢ ∀ (x : ℤ), x ∈ Multiset.map Zsqrtd.norm f → OddPrimeOrFour x
Tactic:
intro x hx
State after:
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
x : ℤ
hx : x ∈ Multiset.map Zsqrtd.norm f
⊢ OddPrimeOrFour x

State before:
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
x : ℤ
hx : x ∈ Multiset.map Zsqrtd.norm f
⊢ OddPrimeOrFour x
Tactic:
rw [Multiset.mem_map] at hx
State after:
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
x : ℤ
hx : ∃ a, a ∈ f ∧ Zsqrtd.norm a = x
⊢ OddPrimeOrFour x

State before:
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
x : ℤ
hx : ∃ a, a ∈ f ∧ Zsqrtd.norm a = x
⊢ OddPrimeOrFour x
Tactic:
obtain ⟨y, hy, rfl⟩ := hx
State after:
case a.intro.intro
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
y : ℤ√(-3)
hy : y ∈ f
⊢ OddPrimeOrFour (Zsqrtd.norm y)

State before:
case a.intro.intro
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
y : ℤ√(-3)
hy : y ∈ f
⊢ OddPrimeOrFour (Zsqrtd.norm y)
Tactic:
exact hf y hy
State after:
no goals

State before:
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
⊢ ∀ (x : ℤ), x ∈ Multiset.map Zsqrtd.norm g → OddPrimeOrFour x
Tactic:
intro x hx
State after:
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
x : ℤ
hx : x ∈ Multiset.map Zsqrtd.norm g
⊢ OddPrimeOrFour x

State before:
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
x : ℤ
hx : x ∈ Multiset.map Zsqrtd.norm g
⊢ OddPrimeOrFour x
Tactic:
rw [Multiset.mem_map] at hx
State after:
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
x : ℤ
hx : ∃ a, a ∈ g ∧ Zsqrtd.norm a = x
⊢ OddPrimeOrFour x

State before:
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
x : ℤ
hx : ∃ a, a ∈ g ∧ Zsqrtd.norm a = x
⊢ OddPrimeOrFour x
Tactic:
obtain ⟨y, hy, rfl⟩ := hx
State after:
case a.intro.intro
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
y : ℤ√(-3)
hy : y ∈ g
⊢ OddPrimeOrFour (Zsqrtd.norm y)

State before:
case a.intro.intro
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
y : ℤ√(-3)
hy : y ∈ g
⊢ OddPrimeOrFour (Zsqrtd.norm y)
Tactic:
exact hg y hy
State after:
no goals

State before:
case a
f g : Multiset (ℤ√(-3))
hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)
hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)
hassoc : Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g))
⊢ Associated (Multiset.prod (Multiset.map Zsqrtd.norm f)) (Multiset.prod (Multiset.map Zsqrtd.norm g))
Tactic:
rwa [prod_map_norm, prod_map_norm]
State after:
no goals