internlm/Lean-Github huggingface dataset:
Theorem: gcd3_coprime
Proof state before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ 2 * v
⊢ k ∣ v
Tactic:
exact Int.dvd_mul_cancel_prime' haddodd hkdvdleft Int.prime_two hkdvdright
Proof state after:
no goals
Theorem: gcd3_coprime
Proof state before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
⊢ IsCoprime (u - v) (2 * v)
Tactic:
apply isCoprime_of_prime_dvd
Proof state after:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
⊢ ¬(u - v = 0 ∧ 2 * v = 0)

case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
⊢ ∀ (z : ℤ), Prime z → z ∣ u - v → ¬z ∣ 2 * v
Theorem: gcd3_coprime
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
⊢ ∀ (z : ℤ), Prime z → z ∣ u - v → ¬z ∣ 2 * v
Tactic:
intro k hkprime hkdvdleft hkdvdright
Proof state after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ False
Theorem: gcd3_coprime
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ False
Tactic:
apply hkprime.not_unit
Proof state after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ IsUnit k
Theorem: gcd3_coprime
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ IsUnit k
Tactic:
have hkdvdright' : k ∣ v := by
  rw [even_iff_two_dvd] at hsubodd
  exact Int.dvd_mul_cancel_prime' hsubodd hkdvdleft Int.prime_two hkdvdright
Proof state after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ IsUnit k
Theorem: gcd3_coprime
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ IsUnit k
Tactic:
apply huvcoprime.isUnit_of_dvd' _ hkdvdright'
Proof state after:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ k ∣ u
Theorem: gcd3_coprime
Proof state before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ k ∣ u
Tactic:
rw [← sub_add_cancel u v]
Proof state after:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ k ∣ u - v + v
Theorem: gcd3_coprime
Proof state before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
hkdvdright' : k ∣ v
⊢ k ∣ u - v + v
Tactic:
exact dvd_add hkdvdleft hkdvdright'
Proof state after:
no goals
Theorem: gcd3_coprime
Proof state before:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
⊢ ¬(u - v = 0 ∧ 2 * v = 0)
Tactic:
rintro ⟨h1, -⟩
Proof state after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
h1 : u - v = 0
⊢ False
Theorem: gcd3_coprime
Proof state before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
h1 : u - v = 0
⊢ False
Tactic:
rw [h1] at hsubodd
Proof state after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even 0
haddcoprime : IsCoprime (u + v) (2 * v)
h1 : u - v = 0
⊢ False
Theorem: gcd3_coprime
Proof state before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even 0
haddcoprime : IsCoprime (u + v) (2 * v)
h1 : u - v = 0
⊢ False
Tactic:
norm_num at hsubodd
Proof state after:
no goals
Theorem: gcd3_coprime
Proof state before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ k ∣ v
Tactic:
rw [even_iff_two_dvd] at hsubodd
Proof state after:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬2 ∣ u - v
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ k ∣ v
Theorem: gcd3_coprime
Proof state before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬2 ∣ u - v
haddcoprime : IsCoprime (u + v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - v
hkdvdright : k ∣ 2 * v
⊢ k ∣ v
Tactic:
exact Int.dvd_mul_cancel_prime' hsubodd hkdvdleft Int.prime_two hkdvdright
Proof state after:
no goals
Theorem: gcd3_coprime
Proof state before:
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
⊢ IsCoprime (u + v) (u - v)
Tactic:
apply isCoprime_of_prime_dvd
Proof state after:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
⊢ ¬(u + v = 0 ∧ u - v = 0)

case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
⊢ ∀ (z : ℤ), Prime z → z ∣ u + v → ¬z ∣ u - v
Theorem: gcd3_coprime
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
⊢ ∀ (z : ℤ), Prime z → z ∣ u + v → ¬z ∣ u - v
Tactic:
intro k hkprime hkdvdleft hkdvdright
Proof state after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ False
Theorem: gcd3_coprime
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ False
Tactic:
apply hkprime.not_unit
Proof state after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ IsUnit k
Theorem: gcd3_coprime
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ IsUnit k
Tactic:
rw [even_iff_two_dvd] at haddodd
Proof state after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ IsUnit k
Theorem: gcd3_coprime
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ IsUnit k
Tactic:
apply huvcoprime.isUnit_of_dvd' <;>
  apply Int.dvd_mul_cancel_prime' haddodd hkdvdleft Int.prime_two
Proof state after:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ k ∣ 2 * u

case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ k ∣ 2 * v
Theorem: gcd3_coprime
Proof state before:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
⊢ ¬(u + v = 0 ∧ u - v = 0)
Tactic:
rintro ⟨h1, -⟩
Proof state after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
h1 : u + v = 0
⊢ False
Theorem: gcd3_coprime
Proof state before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even (u + v)
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
h1 : u + v = 0
⊢ False
Tactic:
rw [h1] at haddodd
Proof state after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even 0
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
h1 : u + v = 0
⊢ False
Theorem: gcd3_coprime
Proof state before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬Even 0
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
h1 : u + v = 0
⊢ False
Tactic:
norm_num at haddodd
Proof state after:
no goals
Theorem: gcd3_coprime
Proof state before:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ k ∣ 2 * u
Tactic:
convert dvd_add hkdvdleft hkdvdright using 1
Proof state after:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ 2 * u = u + v + (u - v)
Theorem: gcd3_coprime
Proof state before:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ 2 * u = u + v + (u - v)
Tactic:
ring
Proof state after:
no goals
Theorem: gcd3_coprime
Proof state before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ k ∣ 2 * v
Tactic:
convert dvd_sub hkdvdleft hkdvdright using 1
Proof state after:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ 2 * v = u + v - (u - v)
Theorem: gcd3_coprime
Proof state before:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
haddodd : ¬2 ∣ u + v
hsubodd : ¬Even (u - v)
haddcoprime : IsCoprime (u + v) (2 * v)
hsubcoprime : IsCoprime (u - v) (2 * v)
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u + v
hkdvdright : k ∣ u - v
⊢ 2 * v = u + v - (u - v)
Tactic:
ring
Proof state after:
no goals
Theorem: descent_gcd3_coprime
Proof 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]
Proof 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)
Theorem: descent_gcd3_coprime
Proof 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
Proof 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)
Theorem: descent_gcd3_coprime
Proof 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
Proof 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
Theorem: descent_gcd3_coprime
Proof 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
Proof 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
Theorem: descent_gcd3_coprime
Proof 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
Proof 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
Theorem: descent_gcd3_coprime
Proof 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
Proof 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
Theorem: descent_gcd3_coprime
Proof 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
Proof 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
Theorem: descent_gcd3_coprime
Proof 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
Proof 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
⊢ ℕ
Theorem: descent_gcd3_coprime
Proof 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 _)]
Proof 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
⊢ ℕ
Theorem: descent_gcd3_coprime
Proof 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
Proof state after:
no goals
Theorem: descent_gcd3_coprime
Proof 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]
Proof 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)
Theorem: descent_gcd3_coprime
Proof 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
Proof 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)
Theorem: descent_gcd3_coprime
Proof 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]
Proof state after:
no goals
Theorem: descent_gcd3_coprime
Proof 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
Proof state after:
no goals
Theorem: descent_gcd3_coprime
Proof 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
Proof 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
Theorem: descent_gcd3_coprime
Proof 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
Proof 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