internlm/Lean-Github huggingface dataset:
Theorem: factors
Proof state before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ ↑g ^ 2 ∣ y
Tactic:
apply IsCoprime.dvd_of_dvd_mul_left _ this
Proof state after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ IsCoprime (↑g ^ 2) x
Theorem: factors
Proof state before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ IsCoprime (↑g ^ 2) x
Tactic:
apply isCoprime_of_prime_dvd
Proof state after:
case nonzero
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ ¬(↑g ^ 2 = 0 ∧ x = 0)

case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ ∀ (z : ℤ), Prime z → z ∣ ↑g ^ 2 → ¬z ∣ x
Theorem: factors
Proof state before:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ ∀ (z : ℤ), Prime z → z ∣ ↑g ^ 2 → ¬z ∣ x
Tactic:
intro p hpprime hpdvdleft hpdvdright
Proof state after:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
⊢ False
Theorem: factors
Proof state before:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
⊢ False
Tactic:
have : ↑p ∣ c' + m * x := by
  rw [HC']
  exact
    dvd_add
      (dvd_mul_of_dvd_left
        ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr (hpprime.dvd_of_dvd_pow hpdvdleft)) _)
      (dvd_mul_of_dvd_right ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr hpdvdright) _)
Proof state after:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this✝ : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
this : ↑p ∣ c' + m * ↑x
⊢ False
Theorem: factors
Proof state before:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this✝ : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
this : ↑p ∣ c' + m * ↑x
⊢ False
Tactic:
have := Zsqrtd.coprime_of_dvd_coprime hcoprime this
Proof state after:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this✝¹ : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
this✝ : ↑p ∣ c' + m * ↑x
this : IsCoprime (↑p).re (↑p).im
⊢ False
Theorem: factors
Proof state before:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this✝¹ : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
this✝ : ↑p ∣ c' + m * ↑x
this : IsCoprime (↑p).re (↑p).im
⊢ False
Tactic:
simp only [Zsqrtd.coe_int_re, isCoprime_zero_right, Zsqrtd.coe_int_im, hpprime.not_unit] at this
Proof state after:
no goals
Theorem: factors
Proof state before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
⊢ ↑g ^ 2 ∣ x * y
Tactic:
rw [h5]
Proof state after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
⊢ ↑g ^ 2 ∣ ↑g ^ 2 * Zsqrtd.norm C'
Theorem: factors
Proof state before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
⊢ ↑g ^ 2 ∣ ↑g ^ 2 * Zsqrtd.norm C'
Tactic:
exact dvd_mul_right _ _
Proof state after:
no goals
Theorem: factors
Proof state before:
case nonzero
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ ¬(↑g ^ 2 = 0 ∧ x = 0)
Tactic:
contrapose! h0
Proof state after:
case nonzero
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
h0 : ↑(Int.gcd c'.re c'.im) ^ 2 = 0 ∧ x = 0
⊢ x = 0
Theorem: factors
Proof state before:
case nonzero
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
h0 : ↑(Int.gcd c'.re c'.im) ^ 2 = 0 ∧ x = 0
⊢ x = 0
Tactic:
exact h0.2
Proof state after:
no goals
Theorem: factors
Proof state before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
⊢ ↑p ∣ c' + m * ↑x
Tactic:
rw [HC']
Proof state after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
⊢ ↑p ∣ ↑↑(Int.gcd c'.re c'.im) * C' + m * ↑x
Theorem: factors
Proof state before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
⊢ ↑p ∣ ↑↑(Int.gcd c'.re c'.im) * C' + m * ↑x
Tactic:
exact
  dvd_add
    (dvd_mul_of_dvd_left
      ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr (hpprime.dvd_of_dvd_pow hpdvdleft)) _)
    (dvd_mul_of_dvd_right ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr hpdvdright) _)
Proof state after:
no goals
Theorem: factors
Proof state before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
⊢ x * z = Zsqrtd.norm C'
Tactic:
have hgnezero := Int.coe_nat_ne_zero_iff_pos.mpr hgpos
Proof state after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
hgnezero : ↑g ≠ 0
⊢ x * z = Zsqrtd.norm C'
Theorem: factors
Proof state before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
hgnezero : ↑g ≠ 0
⊢ x * z = Zsqrtd.norm C'
Tactic:
apply Int.eq_of_mul_eq_mul_left (pow_ne_zero 2 hgnezero)
Proof state after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
hgnezero : ↑g ≠ 0
⊢ ↑g ^ 2 * (x * z) = ↑g ^ 2 * Zsqrtd.norm C'