internlm/Lean-Github huggingface dataset:
Theorem: Int.gcd1_coprime12
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u - 3 * v
⊢ IsUnit k
Tactic:
apply huvcoprime.isUnit_of_dvd'
Proof state after:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u - 3 * v
⊢ k ∣ u

case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u - 3 * v
⊢ k ∣ v
Theorem: Int.gcd1_coprime12
Proof state before:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
⊢ ¬(2 * u = 0 ∧ u - 3 * v = 0)
Tactic:
rintro ⟨-, h2⟩
Proof state after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
h2 : u - 3 * v = 0
⊢ False
Theorem: Int.gcd1_coprime12
Proof state before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
h2 : u - 3 * v = 0
⊢ False
Tactic:
rw [h2] at notdvd_2_2
Proof state after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ 0
not_3_dvd_2 : ¬3 ∣ u - 3 * v
h2 : u - 3 * v = 0
⊢ False
Theorem: Int.gcd1_coprime12
Proof state before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ 0
not_3_dvd_2 : ¬3 ∣ u - 3 * v
h2 : u - 3 * v = 0
⊢ False
Tactic:
norm_num at notdvd_2_2
Proof state after:
no goals
Theorem: Int.gcd1_coprime12
Proof state before:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u - 3 * v
⊢ k ∣ u
Tactic:
exact Int.dvd_mul_cancel_prime' notdvd_2_2 hkdvdright Int.prime_two hkdvdleft
Proof state after:
no goals
Theorem: Int.gcd1_coprime12
Proof state before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u - 3 * v
⊢ k ∣ v
Tactic:
apply Int.dvd_mul_cancel_prime' not_3_dvd_2 hkdvdright Int.prime_three
Proof state after:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u - 3 * v
⊢ k ∣ 3 * v
Theorem: Int.gcd1_coprime12
Proof state before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u - 3 * v
⊢ k ∣ 3 * v
Tactic:
apply Int.dvd_mul_cancel_prime' notdvd_2_2 hkdvdright Int.prime_two
Proof state after:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u - 3 * v
⊢ k ∣ 2 * (3 * v)
Theorem: Int.gcd1_coprime12
Proof state before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u - 3 * v
⊢ k ∣ 2 * (3 * v)
Tactic:
convert dvd_sub hkdvdleft (hkdvdright.mul_left 2) using 1
Proof state after:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u - 3 * v
⊢ 2 * (3 * v) = 2 * u - 2 * (u - 3 * v)
Theorem: Int.gcd1_coprime12
Proof state before:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
not_3_dvd_2 : ¬3 ∣ u - 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u - 3 * v
⊢ 2 * (3 * v) = 2 * u - 2 * (u - 3 * v)
Tactic:
ring
Proof state after:
no goals
Theorem: Int.gcd1_coprime13
Proof state before:
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬Even (u + 3 * v)
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ IsCoprime (2 * u) (u + 3 * v)
Tactic:
rw [even_iff_two_dvd] at this'
Proof state after:
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ IsCoprime (2 * u) (u + 3 * v)
Theorem: Int.gcd1_coprime13
Proof state before:
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ IsCoprime (2 * u) (u + 3 * v)
Tactic:
apply isCoprime_of_prime_dvd
Proof state after:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ ¬(2 * u = 0 ∧ u + 3 * v = 0)

case H
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ ∀ (z : ℤ), Prime z → z ∣ 2 * u → ¬z ∣ u + 3 * v
Theorem: Int.gcd1_coprime13
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ ∀ (z : ℤ), Prime z → z ∣ 2 * u → ¬z ∣ u + 3 * v
Tactic:
intro k hkprime hkdvdleft hkdvdright
Proof state after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ False
Theorem: Int.gcd1_coprime13
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ False
Tactic:
apply hkprime.not_unit
Proof state after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ IsUnit k
Theorem: Int.gcd1_coprime13
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ IsUnit k
Tactic:
apply huvcoprime.isUnit_of_dvd'
Proof state after:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ u

case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ v
Theorem: Int.gcd1_coprime13
Proof state before:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ ¬(2 * u = 0 ∧ u + 3 * v = 0)
Tactic:
rintro ⟨-, h2⟩
Proof state after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
h2 : u + 3 * v = 0
⊢ False
Theorem: Int.gcd1_coprime13
Proof state before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
h2 : u + 3 * v = 0
⊢ False
Tactic:
rw [h2] at this'
Proof state after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ 0
notdvd_3_3 : ¬3 ∣ u + 3 * v
h2 : u + 3 * v = 0
⊢ False
Theorem: Int.gcd1_coprime13
Proof state before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ 0
notdvd_3_3 : ¬3 ∣ u + 3 * v
h2 : u + 3 * v = 0
⊢ False
Tactic:
norm_num at this'
Proof state after:
no goals
Theorem: Int.gcd1_coprime13
Proof state before:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ u
Tactic:
exact Int.dvd_mul_cancel_prime' this' hkdvdright Int.prime_two hkdvdleft
Proof state after:
no goals
Theorem: Int.gcd1_coprime13
Proof state before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ v
Tactic:
apply Int.dvd_mul_cancel_prime' notdvd_3_3 hkdvdright Int.prime_three
Proof state after:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 3 * v
Theorem: Int.gcd1_coprime13
Proof state before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 3 * v
Tactic:
apply Int.dvd_mul_cancel_prime' this' hkdvdright Int.prime_two
Proof state after:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 2 * (3 * v)
Theorem: Int.gcd1_coprime13
Proof state before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 2 * (3 * v)
Tactic:
convert dvd_sub (hkdvdright.mul_left 2) hkdvdleft using 1
Proof state after:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ 2 * (3 * v) = 2 * (u + 3 * v) - 2 * u
Theorem: Int.gcd1_coprime13
Proof state before:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
this' : ¬2 ∣ u + 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ 2 * u
hkdvdright : k ∣ u + 3 * v
⊢ 2 * (3 * v) = 2 * (u + 3 * v) - 2 * u
Tactic:
ring
Proof state after:
no goals
Theorem: Int.gcd1_coprime23
Proof state before:
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ IsCoprime (u - 3 * v) (u + 3 * v)
Tactic:
apply isCoprime_of_prime_dvd
Proof state after:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ ¬(u - 3 * v = 0 ∧ u + 3 * v = 0)

case H
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ ∀ (z : ℤ), Prime z → z ∣ u - 3 * v → ¬z ∣ u + 3 * v
Theorem: Int.gcd1_coprime23
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ ∀ (z : ℤ), Prime z → z ∣ u - 3 * v → ¬z ∣ u + 3 * v
Tactic:
intro k hkprime hkdvdleft hkdvdright
Proof state after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ False
Theorem: Int.gcd1_coprime23
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ False
Tactic:
apply hkprime.not_unit
Proof state after:
case H
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ IsUnit k
Theorem: Int.gcd1_coprime23
Proof state before:
case H
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ IsUnit k
Tactic:
apply huvcoprime.isUnit_of_dvd'
Proof state after:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ u

case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ v
Theorem: Int.gcd1_coprime23
Proof state before:
case nonzero
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
⊢ ¬(u - 3 * v = 0 ∧ u + 3 * v = 0)
Tactic:
rintro ⟨h1, -⟩
Proof state after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
h1 : u - 3 * v = 0
⊢ False
Theorem: Int.gcd1_coprime23
Proof state before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
h1 : u - 3 * v = 0
⊢ False
Tactic:
rw [h1] at notdvd_2_2
Proof state after:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ 0
notdvd_3_3 : ¬3 ∣ u + 3 * v
h1 : u - 3 * v = 0
⊢ False
Theorem: Int.gcd1_coprime23
Proof state before:
case nonzero.intro
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ 0
notdvd_3_3 : ¬3 ∣ u + 3 * v
h1 : u - 3 * v = 0
⊢ False
Tactic:
norm_num at notdvd_2_2
Proof state after:
no goals
Theorem: Int.gcd1_coprime23
Proof state before:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ u
Tactic:
apply Int.dvd_mul_cancel_prime' notdvd_2_2 hkdvdleft Int.prime_two
Proof state after:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 2 * u
Theorem: Int.gcd1_coprime23
Proof state before:
case H.ha
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * 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
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ 2 * u = u - 3 * v + (u + 3 * v)
Theorem: Int.gcd1_coprime23
Proof state before:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ 2 * u = u - 3 * v + (u + 3 * v)
Tactic:
ring
Proof state after:
no goals
Theorem: Int.gcd1_coprime23
Proof state before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ v
Tactic:
apply Int.dvd_mul_cancel_prime' notdvd_3_3 hkdvdright Int.prime_three
Proof state after:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 3 * v
Theorem: Int.gcd1_coprime23
Proof state before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 3 * v
Tactic:
apply Int.dvd_mul_cancel_prime' notdvd_2_2 hkdvdleft Int.prime_two
Proof state after:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 2 * (3 * v)
Theorem: Int.gcd1_coprime23
Proof state before:
case H.hb
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ k ∣ 2 * (3 * v)
Tactic:
convert dvd_sub hkdvdright hkdvdleft using 1
Proof state after:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ 2 * (3 * v) = u + 3 * v - (u - 3 * v)
Theorem: Int.gcd1_coprime23
Proof state before:
case h.e'_4
u v : ℤ
huvcoprime : IsCoprime u v
notdvd_2_2 : ¬2 ∣ u - 3 * v
notdvd_3_3 : ¬3 ∣ u + 3 * v
k : ℤ
hkprime : Prime k
hkdvdleft : k ∣ u - 3 * v
hkdvdright : k ∣ u + 3 * v
⊢ 2 * (3 * v) = u + 3 * v - (u - 3 * v)
Tactic:
ring
Proof state after:
no goals
Theorem: descent_gcd1
Proof state before:
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
obtain ⟨r, hr⟩ : ∃ r, 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3 := by
  rcases hcube with (hcube | hcube | hcube) <;> [(use a); (use b); (use c)]
Proof state after:
case intro
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Theorem: descent_gcd1
Proof state before:
case intro
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
have : Odd 3 := by decide
Proof state after:
case intro
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
this : Odd 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Theorem: descent_gcd1
Proof state before:
case intro
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
this : Odd 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
obtain ⟨hcubeleft, hcuberight⟩ := Int.eq_pow_of_mul_eq_pow_odd hgcd this hr
Proof state after:
case intro.intro
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
this : Odd 3
hcubeleft : ∃ d, 2 * p = d ^ 3
hcuberight : ∃ e, p ^ 2 + 3 * q ^ 2 = e ^ 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Theorem: descent_gcd1
Proof state before:
case intro.intro
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
this : Odd 3
hcubeleft : ∃ d, 2 * p = d ^ 3
hcuberight : ∃ e, p ^ 2 + 3 * q ^ 2 = e ^ 3
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
obtain ⟨u, v, hpfactor, hq, huvcoprime, huvodd⟩ := obscure' p q hp hcoprime hodd hcuberight
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
this : Odd 3
hcubeleft : ∃ d, 2 * p = d ^ 3
hcuberight : ∃ e, p ^ 2 + 3 * q ^ 2 = e ^ 3
u v : ℤ
hpfactor : p = u * (u - 3 * v) * (u + 3 * v)
hq : q = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Theorem: descent_gcd1
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
this : Odd 3
hcubeleft : ∃ d, 2 * p = d ^ 3
hcuberight : ∃ e, p ^ 2 + 3 * q ^ 2 = e ^ 3
u v : ℤ
hpfactor : p = u * (u - 3 * v) * (u + 3 * v)
hq : q = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
have u_ne_zero : u ≠ 0 := by
  rintro rfl
  rw [MulZeroClass.zero_mul, MulZeroClass.zero_mul] at hpfactor
  contradiction
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
this : Odd 3
hcubeleft : ∃ d, 2 * p = d ^ 3
hcuberight : ∃ e, p ^ 2 + 3 * q ^ 2 = e ^ 3
u v : ℤ
hpfactor : p = u * (u - 3 * v) * (u + 3 * v)
hq : q = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
u_ne_zero : u ≠ 0
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Theorem: descent_gcd1
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
this : Odd 3
hcubeleft : ∃ d, 2 * p = d ^ 3
hcuberight : ∃ e, p ^ 2 + 3 * q ^ 2 = e ^ 3
u v : ℤ
hpfactor : p = u * (u - 3 * v) * (u + 3 * v)
hq : q = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
u_ne_zero : u ≠ 0
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3
Tactic:
have haaa : 2 * p = 2 * u * (u - 3 * v) * (u + 3 * v) :=
  by
  rw [hpfactor]
  ring
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
a b c p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hodd : Even p ↔ ¬Even q
hcube : 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3
hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)
r : ℤ
hr : 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3
this : Odd 3
hcubeleft : ∃ d, 2 * p = d ^ 3
hcuberight : ∃ e, p ^ 2 + 3 * q ^ 2 = e ^ 3
u v : ℤ
hpfactor : p = u * (u - 3 * v) * (u + 3 * v)
hq : q = 3 * v * (u - v) * (u + v)
huvcoprime : IsCoprime u v
huvodd : Even u ↔ ¬Even v
u_ne_zero : u ≠ 0
haaa : 2 * p = 2 * u * (u - 3 * v) * (u + 3 * v)
⊢ ∃ a' b' c', a' ≠ 0 ∧ b' ≠ 0 ∧ c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3