Theorem: step5 (Flt/Edwards.lean)

State before:
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
⊢ ∃ 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 = Zsqrtd.norm a
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 = Zsqrtd.norm a
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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = Multiset.prod (factorization' hcoprime) ∨ a = -Multiset.prod (factorization' hcoprime)
⊢ ∃ p, a = p ^ 3

State before:
case intro.intro
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = Multiset.prod (factorization' hcoprime) ∨ a = -Multiset.prod (factorization' hcoprime)
⊢ ∃ 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
State after:
no goals

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

State before:
case intro.intro.inl
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = Multiset.prod (factorization' hcoprime)
⊢ a = Multiset.prod f ^ 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 = Zsqrtd.norm a
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = -Multiset.prod (factorization' hcoprime)
⊢ ∃ p, a = p ^ 3
Tactic:
use -f.prod
State after:
case intro.intro.inr
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = -Multiset.prod (factorization' hcoprime)
⊢ a = (-Multiset.prod f) ^ 3

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

State before:
case intro.intro.inr.a
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3))
hf : factorization' hcoprime = 3 • f
h1 : a = -Multiset.prod (factorization' hcoprime)
⊢ Odd 3
Tactic:
norm_num
State after:
no goals