Theorem: step5' (FltRegular/FltThree/Edwards.lean)

State before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
⊢ ∃ g, factorization' hcoprime = 3 • g
Tactic:
obtain ⟨h1, h2⟩ := factorization'_prop hcoprime
State after:
case intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
h1 : a = (factorization' hcoprime).prod ∨ a = -(factorization' hcoprime).prod
h2 : ∀ pq ∈ factorization' hcoprime, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
⊢ ∃ g, factorization' hcoprime = 3 • g

State before:
case intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
h1 : a = (factorization' hcoprime).prod ∨ a = -(factorization' hcoprime).prod
h2 : ∀ pq ∈ factorization' hcoprime, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
⊢ ∃ g, factorization' hcoprime = 3 • g
Tactic:
set f := factorization' hcoprime with hf
State after:
case intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
⊢ ∃ g, f = 3 • g

State before:
case intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
⊢ ∃ g, f = 3 • g
Tactic:
apply Multiset.exists_smul_of_dvd_count
State after:
case intro.h
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
⊢ ∀ a ∈ f, 3 ∣ Multiset.count a f

State before:
case intro.h
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
⊢ ∀ a ∈ f, 3 ∣ Multiset.count a f
Tactic:
intro x hx
State after:
case intro.h
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ 3 ∣ Multiset.count x f

State before:
case intro.h
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ 3 ∣ Multiset.count x f
Tactic:
convert dvd_mul_right 3 (Multiset.count x.norm.natAbs (factorsOddPrimeOrFour r))
State after:
case h.e'_4
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ Multiset.count x f = 3 * Multiset.count x.norm.natAbs (factorsOddPrimeOrFour r)

State before:
case h.e'_4
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ Multiset.count x f = 3 * Multiset.count x.norm.natAbs (factorsOddPrimeOrFour r)
Tactic:
have : Even (evenFactorExp r) :=
  by
  suffices Even (3 * evenFactorExp r)
    by
    rw [Nat.even_mul] at this
    apply this.resolve_left
    norm_num; decide
  rw [← evenFactorExp.pow r 3, hcube]
  exact factors_2_even' hcoprime
State after:
case h.e'_4
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.count x f = 3 * Multiset.count x.norm.natAbs (factorsOddPrimeOrFour r)

State before:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
⊢ x = A ↔ x.norm.natAbs = A.norm.natAbs

case h.e'_4.calc_2
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.countP (fun x_1 => x.norm.natAbs = x_1) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) =
    Multiset.countP (fun x_1 => x.norm.natAbs = x_1) (factorsOddPrimeOrFour a.norm.natAbs)
Tactic:
swap
State after:
case h.e'_4.calc_2
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.countP (fun x_1 => x.norm.natAbs = x_1) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) =
    Multiset.countP (fun x_1 => x.norm.natAbs = x_1) (factorsOddPrimeOrFour a.norm.natAbs)

case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
⊢ x = A ↔ x.norm.natAbs = A.norm.natAbs

State before:
case h.e'_4.calc_2
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.countP (fun x_1 => x.norm.natAbs = x_1) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) =
    Multiset.countP (fun x_1 => x.norm.natAbs = x_1) (factorsOddPrimeOrFour a.norm.natAbs)

case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
⊢ x = A ↔ x.norm.natAbs = A.norm.natAbs
Tactic:
show
  Multiset.countP (Eq x.norm.natAbs) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) =
    Multiset.countP (Eq x.norm.natAbs) ((factorsOddPrimeOrFour a.norm.natAbs))
State after:
case h.e'_4.calc_2
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.countP (Eq x.norm.natAbs) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) =
    Multiset.countP (Eq x.norm.natAbs) (factorsOddPrimeOrFour a.norm.natAbs)

case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
⊢ x = A ↔ x.norm.natAbs = A.norm.natAbs

State before:
case h.e'_4.calc_2
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.countP (Eq x.norm.natAbs) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) =
    Multiset.countP (Eq x.norm.natAbs) (factorsOddPrimeOrFour a.norm.natAbs)

case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
⊢ x = A ↔ x.norm.natAbs = A.norm.natAbs
Tactic:
congr 1
State after:
case h.e'_4.calc_2.e_s
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f = factorsOddPrimeOrFour a.norm.natAbs

case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
⊢ x = A ↔ x.norm.natAbs = A.norm.natAbs

State before:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
⊢ x = A ↔ x.norm.natAbs = A.norm.natAbs
Tactic:
have h2x := h2 x hx
State after:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
⊢ x = A ↔ x.norm.natAbs = A.norm.natAbs

State before:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
⊢ x = A ↔ x.norm.natAbs = A.norm.natAbs
Tactic:
refine' ⟨fun h => by rw [h], fun h => _⟩
State after:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : x.norm.natAbs = A.norm.natAbs
⊢ x = A

State before:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : x.norm.natAbs = A.norm.natAbs
⊢ x = A
Tactic:
rw [← Int.associated_iff_natAbs] at h
State after:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
⊢ x = A

State before:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
⊢ x = A
Tactic:
have hassoc := factorization'.associated'_of_norm_associated hcoprime hx HA h
State after:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
⊢ x = A

State before:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
⊢ x = A
Tactic:
have eq_or_eq_conj := (eq_or_eq_conj_iff_associated'_of_nonneg h2x.1 (h2 A HA).1).mp hassoc
State after:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
⊢ x = A

State before:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
⊢ x = A
Tactic:
refine' eq_or_eq_conj.resolve_right fun H => _
State after:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ False

State before:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ False
Tactic:
apply no_conj f
State after:
case h.e'_4.calc_1.hp
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ ¬IsUnit ?m.81883

case h.e'_4.calc_1.hcoprime
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ IsCoprime f.prod.re f.prod.im

case h.e'_4.calc_1.a
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ ?m.81883 ∈ f ∧ star ?m.81883 ∈ f

a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ ℤ√(-3)

State before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ Even (evenFactorExp r)
Tactic:
suffices Even (3 * evenFactorExp r)
  by
  rw [Nat.even_mul] at this
  apply this.resolve_left
  norm_num; decide
State after:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ Even (3 * evenFactorExp r)

State before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ Even (3 * evenFactorExp r)
Tactic:
rw [← evenFactorExp.pow r 3, hcube]
State after:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ Even (evenFactorExp a.norm.natAbs)

State before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ Even (evenFactorExp a.norm.natAbs)
Tactic:
exact factors_2_even' hcoprime
State after:
no goals

State before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (3 * evenFactorExp r)
⊢ Even (evenFactorExp r)
Tactic:
rw [Nat.even_mul] at this
State after:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even 3 ∨ Even (evenFactorExp r)
⊢ Even (evenFactorExp r)

State before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even 3 ∨ Even (evenFactorExp r)
⊢ Even (evenFactorExp r)
Tactic:
apply this.resolve_left
State after:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even 3 ∨ Even (evenFactorExp r)
⊢ ¬Even 3

State before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even 3 ∨ Even (evenFactorExp r)
⊢ ¬Even 3
Tactic:
decide
State after:
no goals

State before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.count x f = Multiset.card (Multiset.filter (fun x_1 => x = x_1) f)
Tactic:
rw [Multiset.count, Multiset.countP_eq_card_filter]
State after:
no goals

State before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.countP (fun x_1 => x.norm.natAbs = x_1) (factorsOddPrimeOrFour a.norm.natAbs) =
    Multiset.count x.norm.natAbs (factorsOddPrimeOrFour a.norm.natAbs)
Tactic:
rw [Multiset.count]
State after:
no goals

State before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.count x.norm.natAbs (factorsOddPrimeOrFour a.norm.natAbs) =
    Multiset.count x.norm.natAbs (factorsOddPrimeOrFour (r ^ 3))
Tactic:
rw [hcube]
State after:
no goals

State before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.count x.norm.natAbs (factorsOddPrimeOrFour (r ^ 3)) =
    Multiset.count x.norm.natAbs (3 • factorsOddPrimeOrFour r)
Tactic:
rw [factorsOddPrimeOrFour.pow _ _ this]
State after:
no goals

State before:
case h.e'_4.calc_2.e_s
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f = factorsOddPrimeOrFour a.norm.natAbs
Tactic:
rw [factorsOddPrimeOrFour.unique hcoprime]
State after:
case h.e'_4.calc_2.e_s.hf
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ ∀ x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f, OddPrimeOrFour x

case h.e'_4.calc_2.e_s.hassoc
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f).prod = a.norm.natAbs

State before:
case h.e'_4.calc_2.e_s.hf
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ ∀ x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f, OddPrimeOrFour x
Tactic:
intro x hx
State after:
case h.e'_4.calc_2.e_s.hf
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x✝ : ℤ√(-3)
hx✝ : x✝ ∈ f
this : Even (evenFactorExp r)
x : ℕ
hx : x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f
⊢ OddPrimeOrFour x

State before:
case h.e'_4.calc_2.e_s.hf
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x✝ : ℤ√(-3)
hx✝ : x✝ ∈ f
this : Even (evenFactorExp r)
x : ℕ
hx : x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f
⊢ OddPrimeOrFour x
Tactic:
obtain ⟨y, hy, rfl⟩ := Multiset.mem_map.mp hx
State after:
case h.e'_4.calc_2.e_s.hf.intro.intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx✝ : x ∈ f
this : Even (evenFactorExp r)
y : ℤ√(-3)
hy : y ∈ f
hx : (Int.natAbs ∘ Zsqrtd.norm) y ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f
⊢ OddPrimeOrFour ((Int.natAbs ∘ Zsqrtd.norm) y)

State before:
case h.e'_4.calc_2.e_s.hf.intro.intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx✝ : x ∈ f
this : Even (evenFactorExp r)
y : ℤ√(-3)
hy : y ∈ f
hx : (Int.natAbs ∘ Zsqrtd.norm) y ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f
⊢ OddPrimeOrFour ((Int.natAbs ∘ Zsqrtd.norm) y)
Tactic:
exact (h2 y hy).2.2
State after:
no goals

State before:
case h.e'_4.calc_2.e_s.hassoc
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f).prod = a.norm.natAbs
Tactic:
rw [← Multiset.map_map, prod_map_natAbs, prod_map_norm]
State after:
case h.e'_4.calc_2.e_s.hassoc
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ f.prod.norm.natAbs = a.norm.natAbs

State before:
case h.e'_4.calc_2.e_s.hassoc
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ f.prod.norm.natAbs = a.norm.natAbs
Tactic:
cases' h1 with h1 h1 <;> rw [h1]
State after:
case h.e'_4.calc_2.e_s.hassoc.inr
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
h1 : a = -f.prod
⊢ f.prod.norm.natAbs = (-f.prod).norm.natAbs

State before:
case h.e'_4.calc_2.e_s.hassoc.inr
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
h1 : a = -f.prod
⊢ f.prod.norm.natAbs = (-f.prod).norm.natAbs
Tactic:
rw [Zsqrtd.norm_neg]
State after:
no goals

State before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : x = A
⊢ x.norm.natAbs = A.norm.natAbs
Tactic:
rw [h]
State after:
no goals

State before:
case h.e'_4.calc_1.hp
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ ¬IsUnit ?m.81883
Tactic:
intro HH
State after:
case h.e'_4.calc_1.hp
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
HH : IsUnit ?m.81883
⊢ False

State before:
case h.e'_4.calc_1.hp
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
HH : IsUnit ?m.81883
⊢ False
Tactic:
apply h2x.2.1
State after:
case h.e'_4.calc_1.hp
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
HH : IsUnit ?m.81883
⊢ x.im = 0

State before:
case h.e'_4.calc_1.hp
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
HH : IsUnit ?m.81883
⊢ x.im = 0
Tactic:
rw [Zsqrt3.isUnit_iff] at HH
State after:
case h.e'_4.calc_1.hp
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
HH : |?m.81907.re| = 1 ∧ ?m.81907.im = 0
⊢ x.im = 0

a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ ℤ√(-3)

State before:
case h.e'_4.calc_1.hp
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
HH : |?m.81907.re| = 1 ∧ ?m.81907.im = 0
⊢ x.im = 0

a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ ℤ√(-3)
Tactic:
exact HH.2
State after:
no goals

State before:
case h.e'_4.calc_1.hcoprime
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ IsCoprime f.prod.re f.prod.im
Tactic:
cases' h1 with h1 h1 <;> rw [h1] at hcoprime
State after:
case h.e'_4.calc_1.hcoprime.inl
a : ℤ√(-3)
r : ℕ
hcoprime✝ : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime✝
hcoprime : IsCoprime f.prod.re f.prod.im
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime✝
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
h1 : a = f.prod
⊢ IsCoprime f.prod.re f.prod.im

case h.e'_4.calc_1.hcoprime.inr
a : ℤ√(-3)
r : ℕ
hcoprime✝ : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime✝
hcoprime : IsCoprime (-f.prod).re (-f.prod).im
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime✝
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
h1 : a = -f.prod
⊢ IsCoprime f.prod.re f.prod.im

State before:
case h.e'_4.calc_1.hcoprime.inl
a : ℤ√(-3)
r : ℕ
hcoprime✝ : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime✝
hcoprime : IsCoprime f.prod.re f.prod.im
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime✝
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
h1 : a = f.prod
⊢ IsCoprime f.prod.re f.prod.im
Tactic:
exact hcoprime
State after:
no goals

State before:
case h.e'_4.calc_1.hcoprime.inr
a : ℤ√(-3)
r : ℕ
hcoprime✝ : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime✝
hcoprime : IsCoprime (-f.prod).re (-f.prod).im
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime✝
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
h1 : a = -f.prod
⊢ IsCoprime f.prod.re f.prod.im
Tactic:
rwa [← IsCoprime.neg_neg_iff, ← Zsqrtd.neg_im, ← Zsqrtd.neg_re]
State after:
no goals

State before:
case h.e'_4.calc_1.a
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ x ∈ f ∧ star x ∈ f
Tactic:
refine' ⟨hx, _⟩
State after:
case h.e'_4.calc_1.a
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ star x ∈ f

State before:
case h.e'_4.calc_1.a
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ star x ∈ f
Tactic:
rwa [H, star_star]
State after:
no goals