Theorem: obscure' (FltRegular/FltThree/FltThree.lean)

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
hcube : ∃ r, p ^ 2 + 3 * q ^ 2 = r ^ 3
⊢ ∃ a b, p = a * (a - 3 * b) * (a + 3 * b) ∧ q = 3 * b * (a - b) * (a + b) ∧ IsCoprime a b ∧ (Even a ↔ ¬Even b)
Tactic:
obtain ⟨u, hu⟩ := hcube
State after:
case intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
⊢ ∃ a b, p = a * (a - 3 * b) * (a + 3 * b) ∧ q = 3 * b * (a - b) * (a + b) ∧ IsCoprime a b ∧ (Even a ↔ ¬Even b)

State before:
case intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
⊢ ∃ a b, p = a * (a - 3 * b) * (a + 3 * b) ∧ q = 3 * b * (a - b) * (a + b) ∧ IsCoprime a b ∧ (Even a ↔ ¬Even b)
Tactic:
obtain ⟨a, b, hp', hq'⟩ := step6 p q u hcoprime hu.symm
State after:
case intro.intro.intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ ∃ a b, p = a * (a - 3 * b) * (a + 3 * b) ∧ q = 3 * b * (a - b) * (a + b) ∧ IsCoprime a b ∧ (Even a ↔ ¬Even b)

State before:
case intro.intro.intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ ∃ a b, p = a * (a - 3 * b) * (a + 3 * b) ∧ q = 3 * b * (a - b) * (a + b) ∧ IsCoprime a b ∧ (Even a ↔ ¬Even b)
Tactic:
refine' ⟨a, b, _, _, _, _⟩
State after:
case intro.intro.intro.intro.refine'_1
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ p = a * (a - 3 * b) * (a + 3 * b)

case intro.intro.intro.intro.refine'_2
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ q = 3 * b * (a - b) * (a + b)

case intro.intro.intro.intro.refine'_3
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ IsCoprime a b

case intro.intro.intro.intro.refine'_4
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ Even a ↔ ¬Even b

State before:
case intro.intro.intro.intro.refine'_1
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ p = a * (a - 3 * b) * (a + 3 * b)
Tactic:
rw [hp']
State after:
case intro.intro.intro.intro.refine'_1
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ a ^ 3 - 9 * a * b ^ 2 = a * (a - 3 * b) * (a + 3 * b)

State before:
case intro.intro.intro.intro.refine'_1
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ a ^ 3 - 9 * a * b ^ 2 = a * (a - 3 * b) * (a + 3 * b)
Tactic:
ring
State after:
no goals

State before:
case intro.intro.intro.intro.refine'_2
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ q = 3 * b * (a - b) * (a + b)
Tactic:
rw [hq']
State after:
case intro.intro.intro.intro.refine'_2
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ 3 * a ^ 2 * b - 3 * b ^ 3 = 3 * b * (a - b) * (a + b)

State before:
case intro.intro.intro.intro.refine'_2
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ 3 * a ^ 2 * b - 3 * b ^ 3 = 3 * b * (a - b) * (a + b)
Tactic:
ring
State after:
no goals

State before:
case intro.intro.intro.intro.refine'_3
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ IsCoprime a b
Tactic:
apply isCoprime_of_dvd
State after:
case intro.intro.intro.intro.refine'_3.nonzero
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ ¬(a = 0 ∧ b = 0)

case intro.intro.intro.intro.refine'_3.H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ ∀ z ∈ nonunits ℤ, z ≠ 0 → z ∣ a → ¬z ∣ b

State before:
case intro.intro.intro.intro.refine'_3.H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ ∀ z ∈ nonunits ℤ, z ≠ 0 → z ∣ a → ¬z ∣ b
Tactic:
rintro k hknu - hkdvdleft hkdvdright
State after:
case intro.intro.intro.intro.refine'_3.H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ False

State before:
case intro.intro.intro.intro.refine'_3.H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ False
Tactic:
apply hknu
State after:
case intro.intro.intro.intro.refine'_3.H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ IsUnit k

State before:
case intro.intro.intro.intro.refine'_3.H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ IsUnit k
Tactic:
apply hcoprime.isUnit_of_dvd'
State after:
case intro.intro.intro.intro.refine'_3.H.ha
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ p

case intro.intro.intro.intro.refine'_3.H.hb
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ q

State before:
case intro.intro.intro.intro.refine'_3.nonzero
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
⊢ ¬(a = 0 ∧ b = 0)
Tactic:
rintro ⟨rfl, rfl⟩
State after:
case intro.intro.intro.intro.refine'_3.nonzero.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
hp' : p = 0 ^ 3 - 9 * 0 * 0 ^ 2
hq' : q = 3 * 0 ^ 2 * 0 - 3 * 0 ^ 3
⊢ False

State before:
case intro.intro.intro.intro.refine'_3.nonzero.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
hp' : p = 0 ^ 3 - 9 * 0 * 0 ^ 2
hq' : q = 3 * 0 ^ 2 * 0 - 3 * 0 ^ 3
⊢ False
Tactic:
norm_num at hp'
State after:
case intro.intro.intro.intro.refine'_3.nonzero.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
hq' : q = 3 * 0 ^ 2 * 0 - 3 * 0 ^ 3
hp' : p = 0
⊢ False

State before:
case intro.intro.intro.intro.refine'_3.nonzero.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
hq' : q = 3 * 0 ^ 2 * 0 - 3 * 0 ^ 3
hp' : p = 0
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case intro.intro.intro.intro.refine'_3.H.ha
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ p
Tactic:
rw [hp']
State after:
case intro.intro.intro.intro.refine'_3.H.ha
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ a ^ 3 - 9 * a * b ^ 2

State before:
case intro.intro.intro.intro.refine'_3.H.ha
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ a ^ 3 - 9 * a * b ^ 2
Tactic:
apply dvd_sub
State after:
case intro.intro.intro.intro.refine'_3.H.ha.h₁
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ a ^ 3

case intro.intro.intro.intro.refine'_3.H.ha.h₂
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ 9 * a * b ^ 2

State before:
case intro.intro.intro.intro.refine'_3.H.ha.h₁
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ a ^ 3
Tactic:
exact dvd_pow hkdvdleft (by norm_num)
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ 3 ≠ 0
Tactic:
norm_num
State after:
no goals

State before:
case intro.intro.intro.intro.refine'_3.H.ha.h₂
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ 9 * a * b ^ 2
Tactic:
rw [mul_comm (9 : ℤ), mul_assoc]
State after:
case intro.intro.intro.intro.refine'_3.H.ha.h₂
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ a * (9 * b ^ 2)

State before:
case intro.intro.intro.intro.refine'_3.H.ha.h₂
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ a * (9 * b ^ 2)
Tactic:
exact hkdvdleft.mul_right _
State after:
no goals

State before:
case intro.intro.intro.intro.refine'_3.H.hb
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ q
Tactic:
rw [hq']
State after:
case intro.intro.intro.intro.refine'_3.H.hb
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ 3 * a ^ 2 * b - 3 * b ^ 3

State before:
case intro.intro.intro.intro.refine'_3.H.hb
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ 3 * a ^ 2 * b - 3 * b ^ 3
Tactic:
apply dvd_sub
State after:
case intro.intro.intro.intro.refine'_3.H.hb.h₁
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ 3 * a ^ 2 * b

case intro.intro.intro.intro.refine'_3.H.hb.h₂
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ 3 * b ^ 3

State before:
case intro.intro.intro.intro.refine'_3.H.hb.h₁
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ 3 * a ^ 2 * b
Tactic:
exact hkdvdright.mul_left _
State after:
no goals

State before:
case intro.intro.intro.intro.refine'_3.H.hb.h₂
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
k : ℤ
hknu : k ∈ nonunits ℤ
hkdvdleft : k ∣ a
hkdvdright : k ∣ b
⊢ k ∣ 3 * b ^ 3
Tactic:
exact (hkdvdright.pow (by norm_num)).mul_left _
State after:
no goals

State before:
case neg
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
⊢ Even a ↔ ¬Even b
Tactic:
exfalso
State after:
case neg
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
⊢ False

State before:
case neg
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
⊢ False
Tactic:
have : Even p := by
  rw [hp']
  have : ¬ Even (9 : ℤ) := by decide
  simp [this, haparity, hbparity, three_ne_zero, parity_simps]
State after:
case neg
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
this : Even p
⊢ False

State before:
case neg
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
this : Even p
⊢ False
Tactic:
have : Even q := by
  rw [hq']
  simp [haparity, hbparity, three_ne_zero, parity_simps]
State after:
case neg
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
this✝ : Even p
this : Even q
⊢ False

State before:
case neg
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
this✝ : Even p
this : Even q
⊢ False
Tactic:
tauto
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
⊢ Even p
Tactic:
rw [hp']
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
⊢ Even (a ^ 3 - 9 * a * b ^ 2)

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
⊢ Even (a ^ 3 - 9 * a * b ^ 2)
Tactic:
have : ¬ Even (9 : ℤ) := by decide
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
this : ¬Even 9
⊢ Even (a ^ 3 - 9 * a * b ^ 2)

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
this : ¬Even 9
⊢ Even (a ^ 3 - 9 * a * b ^ 2)
Tactic:
simp [this, haparity, hbparity, three_ne_zero, parity_simps]
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
⊢ ¬Even 9
Tactic:
decide
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
this : Even p
⊢ Even q
Tactic:
rw [hq']
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
this : Even p
⊢ Even (3 * a ^ 2 * b - 3 * b ^ 3)

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
u : ℤ
hu : p ^ 2 + 3 * q ^ 2 = u ^ 3
a b : ℤ
hp' : p = a ^ 3 - 9 * a * b ^ 2
hq' : q = 3 * a ^ 2 * b - 3 * b ^ 3
haparity : ¬Even a
hbparity : ¬Even b
this : Even p
⊢ Even (3 * a ^ 2 * b - 3 * b ^ 3)
Tactic:
simp [haparity, hbparity, three_ne_zero, parity_simps]
State after:
no goals