Theorem: factorsOddPrimeOrFour.unique (FltRegular/FltThree/Edwards.lean)

State before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ factorsOddPrimeOrFour a.norm.natAbs = f
Tactic:
rw [← hassoc]
State after:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ factorsOddPrimeOrFour f.prod = f

State before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ factorsOddPrimeOrFour f.prod = f
Tactic:
refine factorsOddPrimeOrFour.unique' hf ?_ ?_
State after:
case refine_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ 0 < f.prod

case refine_2
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ Even (evenFactorExp f.prod)

State before:
case refine_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ 0 < f.prod
Tactic:
rw [hassoc, Int.natAbs_pos]
State after:
case refine_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ a.norm ≠ 0

State before:
case refine_1
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ a.norm ≠ 0
Tactic:
exact Spts.ne_zero_of_coprime' _ hcoprime
State after:
no goals

State before:
case refine_2
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ Even (evenFactorExp f.prod)
Tactic:
rw [hassoc]
State after:
case refine_2
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ Even (evenFactorExp a.norm.natAbs)

State before:
case refine_2
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
f : Multiset ℕ
hf : ∀ x ∈ f, OddPrimeOrFour x
hassoc : f.prod = a.norm.natAbs
⊢ Even (evenFactorExp a.norm.natAbs)
Tactic:
exact factors_2_even' hcoprime
State after:
no goals