internlm/Lean-Github huggingface dataset:
Theorem: gcd1or3
Proof state before:
case intro.intro.intro.hb.inr
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : Nat.Prime d
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
h000✝ : d ∣ 3 * Int.natAbs q ^ 2
h000 : d ∣ Int.natAbs q ^ 2
⊢ ↑d ∣ q
Tactic:
rw [Int.coe_nat_dvd_left]
Proof state after:
case intro.intro.intro.hb.inr
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : Nat.Prime d
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
h000✝ : d ∣ 3 * Int.natAbs q ^ 2
h000 : d ∣ Int.natAbs q ^ 2
⊢ d ∣ Int.natAbs q
Theorem: gcd1or3
Proof state before:
case intro.intro.intro.hb.inr
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : Nat.Prime d
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
Q : ℤ
hQ : p ^ 2 + 3 * q ^ 2 = ↑d * Q
H : ℤ
hH : P = 2 * H
hp : p = ↑d * H
h000✝ : d ∣ 3 * Int.natAbs q ^ 2
h000 : d ∣ Int.natAbs q ^ 2
⊢ d ∣ Int.natAbs q
Tactic:
exact Nat.Prime.dvd_of_dvd_pow hdprime h000
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ g = 3 ^ k
Tactic:
apply Nat.eq_prime_pow_of_unique_prime_dvd
Proof state after:
case hpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ g ≠ 0

case h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ ∀ {d : ℕ}, Nat.Prime d → d ∣ g → d = 3
Theorem: gcd1or3
Proof state before:
case h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ ∀ {d : ℕ}, Nat.Prime d → d ∣ g → d = 3
Tactic:
intro d hdprime hddvdg
Proof state after:
case h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
d : ℕ
hdprime : Nat.Prime d
hddvdg : d ∣ g
⊢ d = 3
Theorem: gcd1or3
Proof state before:
case h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
d : ℕ
hdprime : Nat.Prime d
hddvdg : d ∣ g
⊢ d = 3
Tactic:
rw [← Int.coe_nat_dvd] at hddvdg
Proof state after:
case h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
d : ℕ
hdprime : Nat.Prime d
hddvdg : ↑d ∣ ↑g
⊢ d = 3
Theorem: gcd1or3
Proof state before:
case h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
d : ℕ
hdprime : Nat.Prime d
hddvdg : ↑d ∣ ↑g
⊢ d = 3
Tactic:
apply basic _ hdprime <;> apply dvd_trans hddvdg <;> rw [hg']
Proof state after:
case h.a
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
d : ℕ
hdprime : Nat.Prime d
hddvdg : ↑d ∣ ↑g
⊢ ↑(Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)) ∣ 2 * p

case h.a
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
d : ℕ
hdprime : Nat.Prime d
hddvdg : ↑d ∣ ↑g
⊢ ↑(Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)) ∣ p ^ 2 + 3 * q ^ 2
Theorem: gcd1or3
Proof state before:
case h.a
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
d : ℕ
hdprime : Nat.Prime d
hddvdg : ↑d ∣ ↑g
⊢ ↑(Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)) ∣ 2 * p

case h.a
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
d : ℕ
hdprime : Nat.Prime d
hddvdg : ↑d ∣ ↑g
⊢ ↑(Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)) ∣ p ^ 2 + 3 * q ^ 2
Tactic:
exacts[Int.gcd_dvd_left _ _, Int.gcd_dvd_right _ _]
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
case hpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ g ≠ 0
Tactic:
apply ne_of_gt
Proof state after:
case hpos.h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ 0 < g
Theorem: gcd1or3
Proof state before:
case hpos.h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ 0 < g
Tactic:
apply Nat.gcd_pos_of_pos_left
Proof state after:
case hpos.h.mpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ 0 < Int.natAbs (2 * p)
Theorem: gcd1or3
Proof state before:
case hpos.h.mpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ 0 < Int.natAbs (2 * p)
Tactic:
rw [Int.natAbs_mul]
Proof state after:
case hpos.h.mpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ 0 < Int.natAbs 2 * Int.natAbs p
Theorem: gcd1or3
Proof state before:
case hpos.h.mpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ 0 < Int.natAbs 2 * Int.natAbs p
Tactic:
apply mul_pos zero_lt_two
Proof state after:
case hpos.h.mpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ 0 < Int.natAbs p
Theorem: gcd1or3
Proof state before:
case hpos.h.mpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
⊢ 0 < Int.natAbs p
Tactic:
rwa [pos_iff_ne_zero, Int.natAbs_ne_zero]
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
⊢ ¬IsUnit 3
Tactic:
rw [Int.isUnit_iff_natAbs_eq]
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
⊢ ¬Int.natAbs 3 = 1
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
⊢ ¬Int.natAbs 3 = 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
⊢ 3 ∣ p
Tactic:
suffices 3 ∣ 2 * p
  by
  apply Int.dvd_mul_cancel_prime' _ dvd_rfl Int.prime_two this
  norm_num
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
⊢ 3 ∣ 2 * p
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
⊢ 3 ∣ 2 * p
Tactic:
have : 3 ∣ (g : ℤ) := by
  rw [hg, pow_two, mul_assoc, Int.ofNat_mul]
  apply dvd_mul_right
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this✝ : ¬IsUnit 3
this : 3 ∣ ↑g
⊢ 3 ∣ 2 * p
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this✝ : ¬IsUnit 3
this : 3 ∣ ↑g
⊢ 3 ∣ 2 * p
Tactic:
exact dvd_trans this (Int.gcd_dvd_left _ _)
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this✝ : ¬IsUnit 3
this : 3 ∣ 2 * p
⊢ 3 ∣ p
Tactic:
apply Int.dvd_mul_cancel_prime' _ dvd_rfl Int.prime_two this
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this✝ : ¬IsUnit 3
this : 3 ∣ 2 * p
⊢ ¬2 ∣ 3
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this✝ : ¬IsUnit 3
this : 3 ∣ 2 * p
⊢ ¬2 ∣ 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
⊢ 3 ∣ ↑g
Tactic:
rw [hg, pow_two, mul_assoc, Int.ofNat_mul]
Proof state after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
⊢ 3 ∣ ↑3 * ↑(3 * 3 ^ (List.length (Nat.factors g) - 2))
Theorem: gcd1or3
Proof state before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
⊢ 3 ∣ ↑3 * ↑(3 * 3 ^ (List.length (Nat.factors g) - 2))
Tactic:
apply dvd_mul_right
Proof state after:
no goals
Theorem: gcd1or3
Proof state before:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ∣ p
⊢ 3 ∣ q
Tactic:
rw [← Int.pow_dvd_pow_iff zero_lt_two] at hdvdp
Proof state after:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ∣ q
Theorem: gcd1or3
Proof state before:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ∣ q
Tactic:
apply Prime.dvd_of_dvd_pow Int.prime_three
Proof state after:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ∣ q ^ ?m.67838

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ
Theorem: gcd1or3
Proof state before:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ∣ q ^ ?m.67838

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ
Tactic:
rw [← mul_dvd_mul_iff_left (three_ne_zero' ℤ), ← pow_two, dvd_add_iff_right hdvdp]
Proof state after:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ^ 2 ∣ p ^ 2 + 3 * q ^ ?m.67838

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ
Theorem: gcd1or3
Proof state before:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ^ 2 ∣ p ^ 2 + 3 * q ^ ?m.67838

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ
Tactic:
refine' dvd_trans _ (Int.gcd_dvd_right (2 * p) (p ^ 2 + 3 * q ^ 2))
Proof state after:
case H
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
hg' : g = Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), Nat.Prime f → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := List.length (Nat.factors g)
hg : g = 3 ^ 2 * 3 ^ (List.length (Nat.factors g) - 2)
H : 2 ≤ List.length (Nat.factors g)
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ^ 2 ∣ ↑(Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2))