Theorem: descent_gcd3_coprime (FltRegular/FltThree/FltThree.lean)

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
⊢ IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
Tactic:
have h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2 :=
  by
  rw [← even_iff_two_dvd]
  have : ¬ Even (3 : ℤ) := by decide
  simp [this, two_ne_zero, hodd', parity_simps]
State after:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
⊢ IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
⊢ IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
Tactic:
have h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2 := by
  intro H
  apply h3_ndvd_q
  rw [dvd_add_left (dvd_mul_right _ _)] at H
  exact Prime.dvd_of_dvd_pow Int.prime_three H
State after:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
⊢ IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
⊢ IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2)
Tactic:
apply isCoprime_of_prime_dvd
State after:
case nonzero
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
⊢ ¬(3 ^ 2 * 2 * s = 0 ∧ q ^ 2 + 3 * s ^ 2 = 0)

case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
⊢ ∀ (z : ℤ), Prime z → z ∣ 3 ^ 2 * 2 * s → ¬z ∣ q ^ 2 + 3 * s ^ 2

State before:
case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
⊢ ∀ (z : ℤ), Prime z → z ∣ 3 ^ 2 * 2 * s → ¬z ∣ q ^ 2 + 3 * s ^ 2
Tactic:
intro k hkprime hkdvdleft hkdvdright
State after:
case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
⊢ False

State before:
case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
⊢ False
Tactic:
apply hkprime.not_unit
State after:
case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
⊢ IsUnit k

State before:
case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
⊢ IsUnit k
Tactic:
have : k ∣ s := by
  apply Int.dvd_mul_cancel_prime' h2ndvd hkdvdright Int.prime_two
  apply Int.dvd_mul_cancel_prime' h3ndvd hkdvdright Int.prime_three
  apply Int.dvd_mul_cancel_prime' h3ndvd hkdvdright Int.prime_three
  convert hkdvdleft using 1
  ring
State after:
case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ IsUnit k

State before:
case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ IsUnit k
Tactic:
apply hcoprime'.isUnit_of_dvd' this
State after:
case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ k ∣ q

State before:
case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ k ∣ q
Tactic:
apply hkprime.dvd_of_dvd_pow
State after:
case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ k ∣ q ^ ?m.131699

q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ ℕ

State before:
case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ k ∣ q ^ ?m.131699

q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ ℕ
Tactic:
rw [← dvd_add_left ((this.pow two_ne_zero).mul_left _)]
State after:
case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ k ∣ q ^ ?m.131699 + ?m.131972 * s ^ 2

q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ ℕ

q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ ℤ

q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ ℕ

State before:
case H
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ k ∣ q ^ ?m.131699 + ?m.131972 * s ^ 2

q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ ℕ

q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ ℤ

q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
this : k ∣ s
⊢ ℕ
Tactic:
exact hkdvdright
State after:
no goals

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
⊢ ¬2 ∣ q ^ 2 + 3 * s ^ 2
Tactic:
rw [← even_iff_two_dvd]
State after:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
⊢ ¬Even (q ^ 2 + 3 * s ^ 2)

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
⊢ ¬Even (q ^ 2 + 3 * s ^ 2)
Tactic:
have : ¬ Even (3 : ℤ) := by decide
State after:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
this : ¬Even 3
⊢ ¬Even (q ^ 2 + 3 * s ^ 2)

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
this : ¬Even 3
⊢ ¬Even (q ^ 2 + 3 * s ^ 2)
Tactic:
simp [this, two_ne_zero, hodd', parity_simps]
State after:
no goals

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
⊢ ¬Even 3
Tactic:
decide
State after:
no goals

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
⊢ ¬3 ∣ q ^ 2 + 3 * s ^ 2
Tactic:
intro H
State after:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
H : 3 ∣ q ^ 2 + 3 * s ^ 2
⊢ False

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
H : 3 ∣ q ^ 2 + 3 * s ^ 2
⊢ False
Tactic:
apply h3_ndvd_q
State after:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
H : 3 ∣ q ^ 2 + 3 * s ^ 2
⊢ 3 ∣ q

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
H : 3 ∣ q ^ 2 + 3 * s ^ 2
⊢ 3 ∣ q
Tactic:
rw [dvd_add_left (dvd_mul_right _ _)] at H
State after:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
H : 3 ∣ q ^ 2
⊢ 3 ∣ q

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
H : 3 ∣ q ^ 2
⊢ 3 ∣ q
Tactic:
exact Prime.dvd_of_dvd_pow Int.prime_three H
State after:
no goals

State before:
case nonzero
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
⊢ ¬(3 ^ 2 * 2 * s = 0 ∧ q ^ 2 + 3 * s ^ 2 = 0)
Tactic:
rintro ⟨h1, -⟩
State after:
case nonzero.intro
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
h1 : 3 ^ 2 * 2 * s = 0
⊢ False

State before:
case nonzero.intro
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
h1 : 3 ^ 2 * 2 * s = 0
⊢ False
Tactic:
rw [mul_eq_zero] at h1
State after:
case nonzero.intro
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
h1 : 3 ^ 2 * 2 = 0 ∨ s = 0
⊢ False

State before:
case nonzero.intro
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
h1 : 3 ^ 2 * 2 = 0 ∨ s = 0
⊢ False
Tactic:
exact hspos (h1.resolve_left (by norm_num))
State after:
no goals

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
h1 : 3 ^ 2 * 2 = 0 ∨ s = 0
⊢ ¬3 ^ 2 * 2 = 0
Tactic:
norm_num
State after:
no goals

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
⊢ k ∣ s
Tactic:
apply Int.dvd_mul_cancel_prime' h2ndvd hkdvdright Int.prime_two
State after:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
⊢ k ∣ 2 * s

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
⊢ k ∣ 2 * s
Tactic:
apply Int.dvd_mul_cancel_prime' h3ndvd hkdvdright Int.prime_three
State after:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
⊢ k ∣ 3 * (2 * s)

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
⊢ k ∣ 3 * (2 * s)
Tactic:
apply Int.dvd_mul_cancel_prime' h3ndvd hkdvdright Int.prime_three
State after:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
⊢ k ∣ 3 * (3 * (2 * s))

State before:
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
⊢ k ∣ 3 * (3 * (2 * s))
Tactic:
convert hkdvdleft using 1
State after:
case h.e'_4
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
⊢ 3 * (3 * (2 * s)) = 3 ^ 2 * 2 * s

State before:
case h.e'_4
q s : ℤ
h3_ndvd_q : ¬3 ∣ q
hspos : s ≠ 0
hcoprime' : IsCoprime s q
hodd' : Even q ↔ ¬Even s
h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2
h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 3 ^ 2 * 2 * s
hkdvdright : k ∣ q ^ 2 + 3 * s ^ 2
⊢ 3 * (3 * (2 * s)) = 3 ^ 2 * 2 * s
Tactic:
ring
State after:
no goals