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

State before:
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
⊢ ∃ p q, a = p ^ 3 - 9 * p * q ^ 2 ∧ b = 3 * p ^ 2 * q - 3 * q ^ 3
Tactic:
set A : ℤ√(-3) := ⟨a, b⟩ with hA
State after:
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
⊢ ∃ p q, a = p ^ 3 - 9 * p * q ^ 2 ∧ b = 3 * p ^ 2 * q - 3 * q ^ 3

State before:
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
⊢ ∃ p q, a = p ^ 3 - 9 * p * q ^ 2 ∧ b = 3 * p ^ 2 * q - 3 * q ^ 3
Tactic:
have hcube' : r.natAbs ^ 3 = A.norm.natAbs :=
  by
  rw [← Int.natAbs_pow]
  apply congr_arg
  simp only [hcube, Zsqrtd.norm_def, hA]
  ring
State after:
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
hcube' : r.natAbs ^ 3 = A.norm.natAbs
⊢ ∃ p q, a = p ^ 3 - 9 * p * q ^ 2 ∧ b = 3 * p ^ 2 * q - 3 * q ^ 3

State before:
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
hcube' : r.natAbs ^ 3 = A.norm.natAbs
⊢ ∃ p q, a = p ^ 3 - 9 * p * q ^ 2 ∧ b = 3 * p ^ 2 * q - 3 * q ^ 3
Tactic:
obtain ⟨p, hp⟩ := step5 A r.natAbs hcoprime hcube'
State after:
case intro
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
hcube' : r.natAbs ^ 3 = A.norm.natAbs
p : ℤ√(-3)
hp : A = p ^ 3
⊢ ∃ p q, a = p ^ 3 - 9 * p * q ^ 2 ∧ b = 3 * p ^ 2 * q - 3 * q ^ 3

State before:
case intro
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
hcube' : r.natAbs ^ 3 = A.norm.natAbs
p : ℤ√(-3)
hp : A = p ^ 3
⊢ ∃ p q, a = p ^ 3 - 9 * p * q ^ 2 ∧ b = 3 * p ^ 2 * q - 3 * q ^ 3
Tactic:
use p.re, p.im
State after:
case h
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
hcube' : r.natAbs ^ 3 = A.norm.natAbs
p : ℤ√(-3)
hp : A = p ^ 3
⊢ a = p.re ^ 3 - 9 * p.re * p.im ^ 2 ∧ b = 3 * p.re ^ 2 * p.im - 3 * p.im ^ 3

State before:
case h
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
hcube' : r.natAbs ^ 3 = A.norm.natAbs
p : ℤ√(-3)
hp : A = p ^ 3
⊢ a = p.re ^ 3 - 9 * p.re * p.im ^ 2 ∧ b = 3 * p.re ^ 2 * p.im - 3 * p.im ^ 3
Tactic:
simp only [Zsqrtd.ext_iff, pow_succ', pow_two, Zsqrtd.mul_re, Zsqrtd.mul_im] at hp
State after:
case h
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
hcube' : r.natAbs ^ 3 = A.norm.natAbs
p : ℤ√(-3)
hp :
  a =
      p.re *
          (p.re * (p.re * (p ^ 0).re + -3 * p.im * (p ^ 0).im) + -3 * p.im * (p.re * (p ^ 0).im + p.im * (p ^ 0).re)) +
        -3 * p.im *
          (p.re * (p.re * (p ^ 0).im + p.im * (p ^ 0).re) + p.im * (p.re * (p ^ 0).re + -3 * p.im * (p ^ 0).im)) ∧
    b =
      p.re * (p.re * (p.re * (p ^ 0).im + p.im * (p ^ 0).re) + p.im * (p.re * (p ^ 0).re + -3 * p.im * (p ^ 0).im)) +
        p.im *
          (p.re * (p.re * (p ^ 0).re + -3 * p.im * (p ^ 0).im) + -3 * p.im * (p.re * (p ^ 0).im + p.im * (p ^ 0).re))
⊢ a = p.re ^ 3 - 9 * p.re * p.im ^ 2 ∧ b = 3 * p.re ^ 2 * p.im - 3 * p.im ^ 3

State before:
case h
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
hcube' : r.natAbs ^ 3 = A.norm.natAbs
p : ℤ√(-3)
hp :
  a =
      p.re *
          (p.re * (p.re * (p ^ 0).re + -3 * p.im * (p ^ 0).im) + -3 * p.im * (p.re * (p ^ 0).im + p.im * (p ^ 0).re)) +
        -3 * p.im *
          (p.re * (p.re * (p ^ 0).im + p.im * (p ^ 0).re) + p.im * (p.re * (p ^ 0).re + -3 * p.im * (p ^ 0).im)) ∧
    b =
      p.re * (p.re * (p.re * (p ^ 0).im + p.im * (p ^ 0).re) + p.im * (p.re * (p ^ 0).re + -3 * p.im * (p ^ 0).im)) +
        p.im *
          (p.re * (p.re * (p ^ 0).re + -3 * p.im * (p ^ 0).im) + -3 * p.im * (p.re * (p ^ 0).im + p.im * (p ^ 0).re))
⊢ a = p.re ^ 3 - 9 * p.re * p.im ^ 2 ∧ b = 3 * p.re ^ 2 * p.im - 3 * p.im ^ 3
Tactic:
convert hp using 2 <;> simp <;> ring
State after:
no goals

State before:
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
⊢ r.natAbs ^ 3 = A.norm.natAbs
Tactic:
rw [← Int.natAbs_pow]
State after:
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
⊢ (r ^ 3).natAbs = A.norm.natAbs

State before:
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
⊢ (r ^ 3).natAbs = A.norm.natAbs
Tactic:
apply congr_arg
State after:
case h
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
⊢ r ^ 3 = A.norm

State before:
case h
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
⊢ r ^ 3 = A.norm
Tactic:
simp only [hcube, Zsqrtd.norm_def, hA]
State after:
case h
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
⊢ a ^ 2 + 3 * b ^ 2 = a * a - -3 * b * b

State before:
case h
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
⊢ a ^ 2 + 3 * b ^ 2 = a * a - -3 * b * b
Tactic:
ring
State after:
no goals