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

State before:
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
⊢ ∃ p, a = p ^ 3
Tactic:
obtain ⟨f, hf⟩ := step5' a r hcoprime hcube
State after:
case intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
⊢ ∃ p, a = p ^ 3

State before:
case intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
⊢ ∃ p, a = p ^ 3
Tactic:
obtain ⟨h1, -⟩ := factorization'_prop hcoprime
State after:
case intro.intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = (factorization' hcoprime).prod ∨ a = -(factorization' hcoprime).prod
⊢ ∃ p, a = p ^ 3

State before:
case intro.intro
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = (factorization' hcoprime).prod ∨ a = -(factorization' hcoprime).prod
⊢ ∃ p, a = p ^ 3
Tactic:
cases h1 with
| inl h1 =>
  use f.prod
  rw [h1, hf, Multiset.prod_nsmul]
| inr h1 =>
  use -f.prod
  rw [h1, hf, Multiset.prod_nsmul, Odd.neg_pow]
  norm_num; decide
State after:
no goals

State before:
case intro.intro.inl
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = (factorization' hcoprime).prod
⊢ ∃ p, a = p ^ 3
Tactic:
use f.prod
State after:
case h
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = (factorization' hcoprime).prod
⊢ a = f.prod ^ 3

State before:
case h
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = (factorization' hcoprime).prod
⊢ a = f.prod ^ 3
Tactic:
rw [h1, hf, Multiset.prod_nsmul]
State after:
no goals

State before:
case intro.intro.inr
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = -(factorization' hcoprime).prod
⊢ ∃ p, a = p ^ 3
Tactic:
use -f.prod
State after:
case h
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = -(factorization' hcoprime).prod
⊢ a = (-f.prod) ^ 3

State before:
case h
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = -(factorization' hcoprime).prod
⊢ a = (-f.prod) ^ 3
Tactic:
rw [h1, hf, Multiset.prod_nsmul, Odd.neg_pow]
State after:
case h.a
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = -(factorization' hcoprime).prod
⊢ Odd 3

State before:
case h.a
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = -(factorization' hcoprime).prod
⊢ Odd 3
Tactic:
norm_num
State after:
case h.a
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = -(factorization' hcoprime).prod
⊢ ¬Even 3

State before:
case h.a
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = -(factorization' hcoprime).prod
⊢ ¬Even 3
Tactic:
decide
State after:
no goals