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

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

State before:
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f = Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g
Tactic:
refine factors_unique_prod' ?_ ?_ ?_
State after:
case refine_1
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ ∀ x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f, OddPrimeOrFour x

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

case refine_3
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f).prod = (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g).prod

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

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

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

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

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

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

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

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

State before:
case refine_3
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f).prod = (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) g).prod
Tactic:
simp_rw [← Multiset.map_map, prod_map_natAbs, prod_map_norm, ← Int.associated_iff_natAbs]
State after:
case refine_3
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ Associated f.prod.norm g.prod.norm

State before:
case refine_3
f g : Multiset (ℤ√(-3))
hf : ∀ x ∈ f, OddPrimeOrFour x.norm.natAbs
hg : ∀ x ∈ g, OddPrimeOrFour x.norm.natAbs
hassoc : Associated f.prod.norm g.prod.norm
⊢ Associated f.prod.norm g.prod.norm
Tactic:
exact hassoc
State after:
no goals