Theorem: step5' (Flt/Edwards.lean)

State before:
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
⊢ ∃ 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 = Zsqrtd.norm a
h1 : a = Multiset.prod (factorization' hcoprime) ∨ a = -Multiset.prod (factorization' hcoprime)
h2 : ∀ (pq : ℤ√(-3)), pq ∈ factorization' hcoprime → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
⊢ ∃ g, factorization' hcoprime = 3 • g

State before:
case intro
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
h1 : a = Multiset.prod (factorization' hcoprime) ∨ a = -Multiset.prod (factorization' hcoprime)
h2 : ∀ (pq : ℤ√(-3)), pq ∈ factorization' hcoprime → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
⊢ ∃ 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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
⊢ ∃ g, f = 3 • g

State before:
case intro
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
⊢ ∀ (a : ℤ√(-3)), a ∈ f → 3 ∣ Multiset.count a f

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

State before:
case h.e'_4
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ Multiset.count x f = 3 * Multiset.count (Zsqrtd.norm x) (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
  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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.count x f = 3 * Multiset.count (Zsqrtd.norm x) (factorsOddPrimeOrFour r)

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

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

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

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

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

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

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

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

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

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

State before:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
⊢ x = A ↔ Zsqrtd.norm x = Zsqrtd.norm A
Tactic:
refine' ⟨congr_arg _, fun h => _⟩
State after:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
⊢ x = A

State before:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
⊢ x = A
Tactic:
have hassoc := factorization'.associated'_of_norm_eq hcoprime hx HA h
State after:
case h.e'_4.calc_1
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ ¬IsUnit ?m.291656

case h.e'_4.calc_1.hcoprime
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ IsCoprime (Multiset.prod f).re (Multiset.prod f).im

case h.e'_4.calc_1.a
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ ?m.291656 ∈ f ∧ star ?m.291656 ∈ f

a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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
State after:
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ Even (evenFactorExp (Zsqrtd.norm a))

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

State before:
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even 3 ∨ Even (evenFactorExp r)
⊢ ¬Even 3
Tactic:
norm_num
State after:
no goals

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

State before:
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.count (Zsqrtd.norm x) (factorsOddPrimeOrFour (Zsqrtd.norm a)) =
    Multiset.count (Zsqrtd.norm x) (factorsOddPrimeOrFour (r ^ 3))
Tactic:
rw [hcube]
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.map Zsqrtd.norm f = factorsOddPrimeOrFour (Zsqrtd.norm a)
Tactic:
apply 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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ ∀ (x : ℤ), x ∈ Multiset.map Zsqrtd.norm f → OddPrimeOrFour x

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

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

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

State before:
case h.e'_4.calc_2.e_s.hf'
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ ∀ (x : ℤ), x ∈ Multiset.map Zsqrtd.norm f → 0 ≤ 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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x✝ : ℤ√(-3)
hx✝ : x✝ ∈ f
this : Even (evenFactorExp r)
x : ℤ
hx : x ∈ Multiset.map Zsqrtd.norm f
⊢ 0 ≤ x

State before:
case h.e'_4.calc_2.e_s.hf'
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x✝ : ℤ√(-3)
hx✝ : x✝ ∈ f
this : Even (evenFactorExp r)
x : ℤ
hx : x ∈ Multiset.map Zsqrtd.norm f
⊢ 0 ≤ x
Tactic:
obtain ⟨y, -, 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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx✝ : x ∈ f
this : Even (evenFactorExp r)
y : ℤ√(-3)
hx : Zsqrtd.norm y ∈ Multiset.map Zsqrtd.norm f
⊢ 0 ≤ 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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx✝ : x ∈ f
this : Even (evenFactorExp r)
y : ℤ√(-3)
hx : Zsqrtd.norm y ∈ Multiset.map Zsqrtd.norm f
⊢ 0 ≤ Zsqrtd.norm y
Tactic:
apply Zsqrtd.norm_nonneg
State after:
case h.e'_4.calc_2.e_s.hf'.intro.intro.hd
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx✝ : x ∈ f
this : Even (evenFactorExp r)
y : ℤ√(-3)
hx : Zsqrtd.norm y ∈ Multiset.map Zsqrtd.norm f
⊢ -3 ≤ 0

State before:
case h.e'_4.calc_2.e_s.hf'.intro.intro.hd
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx✝ : x ∈ f
this : Even (evenFactorExp r)
y : ℤ√(-3)
hx : Zsqrtd.norm y ∈ Multiset.map Zsqrtd.norm f
⊢ -3 ≤ 0
Tactic:
norm_num
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Associated (Multiset.prod (Multiset.map Zsqrtd.norm f)) (Zsqrtd.norm a)
Tactic:
rw [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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm a)

State before:
case h.e'_4.calc_2.e_s.hassoc
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm a)
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
h1 : a = -Multiset.prod f
⊢ Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (-Multiset.prod f))

State before:
case h.e'_4.calc_2.e_s.hassoc.inr
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
h1 : a = -Multiset.prod f
⊢ Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (-Multiset.prod f))
Tactic:
rw [Zsqrtd.norm_neg]
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ ¬IsUnit ?m.291656
Tactic:
intro HH
State after:
case h.e'_4.calc_1.hp
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
HH : IsUnit ?m.291656
⊢ False

State before:
case h.e'_4.calc_1.hp
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
HH : IsUnit ?m.291656
⊢ 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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
HH : IsUnit ?m.291656
⊢ x.im = 0

State before:
case h.e'_4.calc_1.hp
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
HH : IsUnit ?m.291656
⊢ 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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
HH : abs ?m.291680.re = 1 ∧ ?m.291680.im = 0
⊢ x.im = 0

a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
HH : abs ?m.291680.re = 1 ∧ ?m.291680.im = 0
⊢ x.im = 0

a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ IsCoprime (Multiset.prod f).re (Multiset.prod f).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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime✝
hcoprime : IsCoprime (Multiset.prod f).re (Multiset.prod f).im
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
h1 : a = Multiset.prod f
⊢ IsCoprime (Multiset.prod f).re (Multiset.prod f).im

case h.e'_4.calc_1.hcoprime.inr
a : ℤ√(-3)
r : ℤ
hcoprime✝ : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime✝
hcoprime : IsCoprime (-Multiset.prod f).re (-Multiset.prod f).im
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
h1 : a = -Multiset.prod f
⊢ IsCoprime (Multiset.prod f).re (Multiset.prod f).im

State before:
case h.e'_4.calc_1.hcoprime.inl
a : ℤ√(-3)
r : ℤ
hcoprime✝ : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime✝
hcoprime : IsCoprime (Multiset.prod f).re (Multiset.prod f).im
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
h1 : a = Multiset.prod f
⊢ IsCoprime (Multiset.prod f).re (Multiset.prod f).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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime✝
hcoprime : IsCoprime (-Multiset.prod f).re (-Multiset.prod f).im
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
h1 : a = -Multiset.prod f
⊢ IsCoprime (Multiset.prod f).re (Multiset.prod f).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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
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 (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
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