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

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
⊢ (2 * p).gcd (p ^ 2 + 3 * q ^ 2) = 1 ∨ (2 * p).gcd (p ^ 2 + 3 * q ^ 2) = 3
Tactic:
set g := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) with hg'
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
⊢ g = 1 ∨ g = 3

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
⊢ ∃ k, g = 3 ^ k ∧ k < 2
Tactic:
set k := g.factors.length
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ ∃ k, g = 3 ^ k ∧ k < 2

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ k
⊢ ∃ k, g = 3 ^ k ∧ k < 2
Tactic:
refine' ⟨k, hg, _⟩
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ k
⊢ k < 2

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ k
⊢ k < 2
Tactic:
by_contra! H
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ k
H : 2 ≤ k
⊢ False

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ k
H : 2 ≤ k
⊢ False
Tactic:
rw [← pow_mul_pow_sub _ H] at hg
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
⊢ False

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
⊢ False
Tactic:
have : ¬IsUnit (3 : ℤ) := by
  rw [Int.isUnit_iff_natAbs_eq]
  norm_num
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
⊢ False

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

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
⊢ IsUnit 3
Tactic:
have hdvdp : 3 ∣ p :=
  by
  suffices 3 ∣ 2 * p
    by
    apply Int.dvd_mul_cancel_prime' _ dvd_rfl Int.prime_two this
    norm_num
  have : 3 ∣ (g : ℤ) := by
    rw [hg, pow_two, mul_assoc, Int.ofNat_mul]
    apply dvd_mul_right
  exact dvd_trans this Int.gcd_dvd_left
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ∣ p
⊢ IsUnit 3

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

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
H : ∃ k, g = 3 ^ k ∧ k < 2
⊢ g = 1 ∨ g = 3
Tactic:
obtain ⟨k, hg, hk⟩ := H
State after:
case intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ k
hk : k < 2
⊢ g = 1 ∨ g = 3

State before:
case intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ k
hk : k < 2
⊢ g = 1 ∨ g = 3
Tactic:
interval_cases k
State after:
case intro.intro.«0»
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 0
hk : 0 < 2
⊢ g = 1 ∨ g = 3

case intro.intro.«1»
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 1
hk : 1 < 2
⊢ g = 1 ∨ g = 3

State before:
case intro.intro.«0»
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 0
hk : 0 < 2
⊢ g = 1 ∨ g = 3
Tactic:
left
State after:
case intro.intro.«0».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 0
hk : 0 < 2
⊢ g = 1

State before:
case intro.intro.«0».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 0
hk : 0 < 2
⊢ g = 1
Tactic:
rw [pow_zero] at hg
State after:
case intro.intro.«0».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 1
hk : 0 < 2
⊢ g = 1

State before:
case intro.intro.«0».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 1
hk : 0 < 2
⊢ g = 1
Tactic:
exact hg
State after:
no goals

State before:
case intro.intro.«1»
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 1
hk : 1 < 2
⊢ g = 1 ∨ g = 3
Tactic:
right
State after:
case intro.intro.«1».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 1
hk : 1 < 2
⊢ g = 3

State before:
case intro.intro.«1».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3 ^ 1
hk : 1 < 2
⊢ g = 3
Tactic:
rw [pow_one] at hg
State after:
case intro.intro.«1».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3
hk : 1 < 2
⊢ g = 3

State before:
case intro.intro.«1».h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
k : ℕ
hg : g = 3
hk : 1 < 2
⊢ g = 3
Tactic:
exact hg
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
⊢ ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
Tactic:
intro d hdprime hdleft hdright
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
⊢ d = 3

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
⊢ d = 3
Tactic:
by_contra hne3
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : ¬d = 3
⊢ False

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : ¬d = 3
⊢ False
Tactic:
rw [← Ne] at hne3
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
⊢ False

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
⊢ False
Tactic:
apply (Nat.prime_iff_prime_int.mp hdprime).not_unit
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
⊢ IsUnit ↑d

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
⊢ IsUnit ↑d
Tactic:
have hne2 : d ≠ 2 := by
  rintro rfl
  rw [Nat.cast_two, ← even_iff_two_dvd] at hdright
  have : ¬ Even (3 : ℤ) := by decide
  simp [this, hparity, two_ne_zero, parity_simps] at hdright
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
⊢ IsUnit ↑d

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
⊢ IsUnit ↑d
Tactic:
have : 2 < d := lt_of_le_of_ne hdprime.two_le hne2.symm
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
this : 2 < d
⊢ IsUnit ↑d

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
this : 2 < d
⊢ IsUnit ↑d
Tactic:
have : 3 < d := lt_of_le_of_ne this hne3.symm
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
⊢ IsUnit ↑d

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
⊢ IsUnit ↑d
Tactic:
obtain ⟨P, hP⟩ := hdleft
State after:
case intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
⊢ IsUnit ↑d

State before:
case intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
hne2 : d ≠ 2
this✝ : 2 < d
this : 3 < d
P : ℤ
hP : 2 * p = ↑d * P
⊢ IsUnit ↑d
Tactic:
obtain ⟨Q, hQ⟩ := hdright
State after:
case intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ IsUnit ↑d

State before:
case intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ IsUnit ↑d
Tactic:
obtain ⟨H, hH⟩ : 2 ∣ P := by
  have H := dvd_mul_right 2 p
  rw [hP] at H
  apply (Prime.dvd_or_dvd Int.prime_two H).resolve_left
  rw [Int.dvd_natCast]
  change ¬2 ∣ d
  rw [Nat.prime_dvd_prime_iff_eq Nat.prime_two hdprime]
  exact hne2.symm
State after:
case intro.intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ IsUnit ↑d

State before:
case intro.intro.intro
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ IsUnit ↑d
Tactic:
have hp : p = d * H := by rw [← mul_right_inj' (two_ne_zero' ℤ), hP, hH, mul_left_comm]
State after:
case intro.intro.intro
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ IsUnit ↑d

State before:
case intro.intro.intro
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ IsUnit ↑d
Tactic:
apply hcoprime.isUnit_of_dvd'
State after:
case intro.intro.intro.ha
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ ↑d ∣ p

case intro.intro.intro.hb
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ ↑d ∣ q

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
hdleft : ↑d ∣ 2 * p
hdright : ↑d ∣ p ^ 2 + 3 * q ^ 2
hne3 : d ≠ 3
⊢ d ≠ 2
Tactic:
rintro rfl
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : ↑2 ∣ p ^ 2 + 3 * q ^ 2
hne3 : 2 ≠ 3
⊢ False

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : ↑2 ∣ p ^ 2 + 3 * q ^ 2
hne3 : 2 ≠ 3
⊢ False
Tactic:
rw [Nat.cast_two, ← even_iff_two_dvd] at hdright
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : Even (p ^ 2 + 3 * q ^ 2)
hne3 : 2 ≠ 3
⊢ False

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : Even (p ^ 2 + 3 * q ^ 2)
hne3 : 2 ≠ 3
⊢ False
Tactic:
have : ¬ Even (3 : ℤ) := by decide
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : Even (p ^ 2 + 3 * q ^ 2)
hne3 : 2 ≠ 3
this : ¬Even 3
⊢ False

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : Even (p ^ 2 + 3 * q ^ 2)
hne3 : 2 ≠ 3
this : ¬Even 3
⊢ False
Tactic:
simp [this, hparity, two_ne_zero, parity_simps] at hdright
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hdprime : Nat.Prime 2
hdleft : ↑2 ∣ 2 * p
hdright : Even (p ^ 2 + 3 * q ^ 2)
hne3 : 2 ≠ 3
⊢ ¬Even 3
Tactic:
decide
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ 2 ∣ P
Tactic:
have H := dvd_mul_right 2 p
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 : 2 ∣ 2 * p
⊢ 2 ∣ P

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 : 2 ∣ 2 * p
⊢ 2 ∣ P
Tactic:
rw [hP] at H
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 : 2 ∣ ↑d * P
⊢ 2 ∣ P

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 : 2 ∣ ↑d * P
⊢ 2 ∣ P
Tactic:
apply (Prime.dvd_or_dvd Int.prime_two H).resolve_left
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 : 2 ∣ ↑d * P
⊢ ¬2 ∣ ↑d

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 : 2 ∣ ↑d * P
⊢ ¬2 ∣ ↑d
Tactic:
rw [Int.dvd_natCast]
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 : 2 ∣ ↑d * P
⊢ ¬Int.natAbs 2 ∣ d

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 : 2 ∣ ↑d * P
⊢ ¬Int.natAbs 2 ∣ d
Tactic:
change ¬2 ∣ d
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 : 2 ∣ ↑d * P
⊢ ¬2 ∣ d

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 : 2 ∣ ↑d * P
⊢ ¬2 ∣ d
Tactic:
rw [Nat.prime_dvd_prime_iff_eq Nat.prime_two hdprime]
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 : 2 ∣ ↑d * P
⊢ ¬2 = d

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 : 2 ∣ ↑d * P
⊢ ¬2 = d
Tactic:
exact hne2.symm
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ p = ↑d * H
Tactic:
rw [← mul_right_inj' (two_ne_zero' ℤ), hP, hH, mul_left_comm]
State after:
no goals

State before:
case intro.intro.intro.ha
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ ↑d ∣ p
Tactic:
rw [hp]
State after:
case intro.intro.intro.ha
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ ↑d ∣ ↑d * H

State before:
case intro.intro.intro.ha
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ ↑d ∣ ↑d * H
Tactic:
exact dvd_mul_right _ _
State after:
no goals

State before:
case intro.intro.intro.hb
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ ↑d ∣ q
Tactic:
have h000 : d ∣ 3 * q.natAbs ^ 2 :=
  by
  rw [← Int.natCast_dvd_natCast, Int.ofNat_mul, Int.natCast_pow, Int.natAbs_sq, Nat.cast_three]
  use Q - d * H ^ 2
  rw [mul_sub, ← hQ, hp]
  ring
State after:
case intro.intro.intro.hb
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 * q.natAbs ^ 2
⊢ ↑d ∣ q

State before:
case intro.intro.intro.hb
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 * q.natAbs ^ 2
⊢ ↑d ∣ q
Tactic:
cases' (Nat.Prime.dvd_mul hdprime).mp h000 with h000 h000
State after:
case intro.intro.intro.hb.inl
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 * q.natAbs ^ 2
h000 : d ∣ 3
⊢ ↑d ∣ q

case intro.intro.intro.hb.inr
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 * q.natAbs ^ 2
h000 : d ∣ q.natAbs ^ 2
⊢ ↑d ∣ q

State before:
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ d ∣ 3 * q.natAbs ^ 2
Tactic:
rw [← Int.natCast_dvd_natCast, Int.ofNat_mul, Int.natCast_pow, Int.natAbs_sq, Nat.cast_three]
State after:
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ ↑d ∣ 3 * q ^ 2

State before:
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ ↑d ∣ 3 * q ^ 2
Tactic:
use Q - d * H ^ 2
State after:
case h
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ 3 * q ^ 2 = ↑d * (Q - ↑d * H ^ 2)

State before:
case h
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ 3 * q ^ 2 = ↑d * (Q - ↑d * H ^ 2)
Tactic:
rw [mul_sub, ← hQ, hp]
State after:
case h
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ 3 * q ^ 2 = (↑d * H) ^ 2 + 3 * q ^ 2 - ↑d * (↑d * H ^ 2)

State before:
case h
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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
⊢ 3 * q ^ 2 = (↑d * H) ^ 2 + 3 * q ^ 2 - ↑d * (↑d * H ^ 2)
Tactic:
ring
State after:
no goals

State before:
case intro.intro.intro.hb.inl
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 * q.natAbs ^ 2
h000 : d ∣ 3
⊢ ↑d ∣ q
Tactic:
rw [Nat.prime_dvd_prime_iff_eq hdprime Nat.prime_three] at h000
State after:
case intro.intro.intro.hb.inl
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 * q.natAbs ^ 2
h000 : d = 3
⊢ ↑d ∣ q

State before:
case intro.intro.intro.hb.inl
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 * q.natAbs ^ 2
h000 : d = 3
⊢ ↑d ∣ q
Tactic:
exact absurd h000 hne3
State after:
no goals

State before:
case intro.intro.intro.hb.inr
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 * q.natAbs ^ 2
h000 : d ∣ q.natAbs ^ 2
⊢ ↑d ∣ q
Tactic:
rw [Int.natCast_dvd]
State after:
case intro.intro.intro.hb.inr
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 * q.natAbs ^ 2
h000 : d ∣ q.natAbs ^ 2
⊢ d ∣ q.natAbs

State before:
case intro.intro.intro.hb.inr
p q : ℤ
hp✝ : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
d : ℕ
hdprime : d.Prime
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 * q.natAbs ^ 2
h000 : d ∣ q.natAbs ^ 2
⊢ d ∣ q.natAbs
Tactic:
exact Nat.Prime.dvd_of_dvd_pow hdprime h000
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ g = 3 ^ k
Tactic:
apply Nat.eq_prime_pow_of_unique_prime_dvd
State after:
case hpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ g ≠ 0

case h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ ∀ {d : ℕ}, d.Prime → d ∣ g → d = 3

State before:
case h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ ∀ {d : ℕ}, d.Prime → d ∣ g → d = 3
Tactic:
intro d hdprime hddvdg
State after:
case h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
d : ℕ
hdprime : d.Prime
hddvdg : d ∣ g
⊢ d = 3

State before:
case h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
d : ℕ
hdprime : d.Prime
hddvdg : d ∣ g
⊢ d = 3
Tactic:
rw [← Int.natCast_dvd_natCast] at hddvdg
State after:
case h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
d : ℕ
hdprime : d.Prime
hddvdg : ↑d ∣ ↑g
⊢ d = 3

State before:
case h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
d : ℕ
hdprime : d.Prime
hddvdg : ↑d ∣ ↑g
⊢ d = 3
Tactic:
apply basic _ hdprime <;> apply dvd_trans hddvdg <;> rw [hg']
State after:
case h.a
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
d : ℕ
hdprime : d.Prime
hddvdg : ↑d ∣ ↑g
⊢ ↑((2 * p).gcd (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 : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
d : ℕ
hdprime : d.Prime
hddvdg : ↑d ∣ ↑g
⊢ ↑((2 * p).gcd (p ^ 2 + 3 * q ^ 2)) ∣ p ^ 2 + 3 * q ^ 2

State before:
case h.a
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
d : ℕ
hdprime : d.Prime
hddvdg : ↑d ∣ ↑g
⊢ ↑((2 * p).gcd (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 : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
d : ℕ
hdprime : d.Prime
hddvdg : ↑d ∣ ↑g
⊢ ↑((2 * p).gcd (p ^ 2 + 3 * q ^ 2)) ∣ p ^ 2 + 3 * q ^ 2
Tactic:
exacts[Int.gcd_dvd_left, Int.gcd_dvd_right]
State after:
no goals

State before:
case hpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ g ≠ 0
Tactic:
apply ne_of_gt
State after:
case hpos.h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ 0 < g

State before:
case hpos.h
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ 0 < g
Tactic:
apply Nat.gcd_pos_of_pos_left
State after:
case hpos.h.mpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ 0 < (2 * p).natAbs

State before:
case hpos.h.mpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ 0 < (2 * p).natAbs
Tactic:
rw [Int.natAbs_mul]
State after:
case hpos.h.mpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ 0 < Int.natAbs 2 * p.natAbs

State before:
case hpos.h.mpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ 0 < Int.natAbs 2 * p.natAbs
Tactic:
apply mul_pos zero_lt_two
State after:
case hpos.h.mpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ 0 < p.natAbs

State before:
case hpos.h.mpos
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
⊢ 0 < p.natAbs
Tactic:
rwa [pos_iff_ne_zero, Int.natAbs_ne_zero]
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
⊢ ¬IsUnit 3
Tactic:
rw [Int.isUnit_iff_natAbs_eq]
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
⊢ ¬Int.natAbs 3 = 1

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
⊢ ¬Int.natAbs 3 = 1
Tactic:
norm_num
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
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
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
⊢ 3 ∣ 2 * p

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
⊢ 3 ∣ 2 * p
Tactic:
have : 3 ∣ (g : ℤ) := by
  rw [hg, pow_two, mul_assoc, Int.ofNat_mul]
  apply dvd_mul_right
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this✝ : ¬IsUnit 3
this : 3 ∣ ↑g
⊢ 3 ∣ 2 * p

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this✝ : ¬IsUnit 3
this : 3 ∣ ↑g
⊢ 3 ∣ 2 * p
Tactic:
exact dvd_trans this Int.gcd_dvd_left
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this✝ : ¬IsUnit 3
this : 3 ∣ 2 * p
⊢ 3 ∣ p
Tactic:
apply Int.dvd_mul_cancel_prime' _ dvd_rfl Int.prime_two this
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this✝ : ¬IsUnit 3
this : 3 ∣ 2 * p
⊢ ¬2 ∣ 3

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this✝ : ¬IsUnit 3
this : 3 ∣ 2 * p
⊢ ¬2 ∣ 3
Tactic:
norm_num
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
⊢ 3 ∣ ↑g
Tactic:
rw [hg, pow_two, mul_assoc, Int.ofNat_mul]
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
⊢ 3 ∣ ↑3 * ↑(3 * 3 ^ (k - 2))

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
⊢ 3 ∣ ↑3 * ↑(3 * 3 ^ (k - 2))
Tactic:
apply dvd_mul_right
State after:
no goals

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ∣ p
⊢ 3 ∣ q
Tactic:
rw [← Int.pow_dvd_pow_iff two_ne_zero] at hdvdp
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ∣ q

State before:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ∣ q
Tactic:
apply Prime.dvd_of_dvd_pow Int.prime_three
State after:
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ∣ q ^ ?m.72510

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

State before:
case refine'_1
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ^ 2 ∣ ↑(?refine'_2.gcd (p ^ 2 + 3 * q ^ ?m.72510))

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

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

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

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

p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ ℕ
Tactic:
rw [← hg', hg, Int.ofNat_mul]
State after:
case refine'_1
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ^ 2 ∣ ↑(3 ^ 2) * ↑(3 ^ (k - 2))

State before:
case refine'_1
p q : ℤ
hp : p ≠ 0
hcoprime : IsCoprime p q
hparity : Even p ↔ ¬Even q
g : ℕ := (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
hg' : g = (2 * p).gcd (p ^ 2 + 3 * q ^ 2)
basic : ∀ (f : ℕ), f.Prime → ↑f ∣ 2 * p → ↑f ∣ p ^ 2 + 3 * q ^ 2 → f = 3
k : ℕ := g.factors.length
hg : g = 3 ^ 2 * 3 ^ (k - 2)
H : 2 ≤ k
this : ¬IsUnit 3
hdvdp : 3 ^ 2 ∣ p ^ 2
⊢ 3 ^ 2 ∣ ↑(3 ^ 2) * ↑(3 ^ (k - 2))
Tactic:
apply dvd_mul_right
State after:
no goals