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'
z : ℤ
hz : y = ↑g ^ 2 * z
hgnezero : ↑g ≠ 0
⊢ ↑g ^ 2 * (x * z) = ↑g ^ 2 * Zsqrtd.norm C'
Tactic:
rw [← h5, hz, mul_left_comm]
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
h6 : x * z = Zsqrtd.norm C'
⊢ z ≠ 0
Tactic:
apply right_ne_zero_of_mul
Proof state after:
case a
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
h6 : x * z = Zsqrtd.norm C'
⊢ ?a * z ≠ 0

case a
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
h6 : x * z = Zsqrtd.norm C'
⊢ ℤ
Theorem: factors
Proof state before:
case a.a
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
h6 : x * z = Zsqrtd.norm C'
⊢ ?a.a✝ * (?a * z) ≠ 0

case a.a
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
h6 : x * z = Zsqrtd.norm C'
⊢ ℤ

case a
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
h6 : x * z = Zsqrtd.norm C'
⊢ ℤ
Tactic:
rwa [h6, ← h5, ← hy]
Proof state after:
no goals
Theorem: factors
Proof state before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
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
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ Int.natAbs w < Int.natAbs x
Tactic:
calc
  w.natAbs ≤ z.natAbs :=
    Nat.le_of_dvd (Int.natAbs_pos.mpr h8) (Int.natAbs_dvd_natAbs.mpr hwdvd)
  _ ≤ y.natAbs := by
    rw [hz, Int.natAbs_mul]
    exact Nat.le_mul_of_pos_left (pow_pos hgpos 2)
  _ < x.natAbs := h3
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
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ Int.natAbs z ≤ Int.natAbs y
Tactic:
rw [hz, Int.natAbs_mul]
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
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ Int.natAbs z ≤ Int.natAbs (↑g ^ 2) * Int.natAbs z
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
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ Int.natAbs z ≤ Int.natAbs (↑g ^ 2) * Int.natAbs z
Tactic:
exact Nat.le_mul_of_pos_left (pow_pos hgpos 2)
Proof state after:
no goals
Theorem: factors
Proof state before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ w ∣ Zsqrtd.norm C'
Tactic:
rw [← h6]
Proof state after:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ w ∣ x * z
Theorem: factors
Proof state before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
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
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ w ∣ x * z
Tactic:
exact dvd_mul_of_dvd_right hwdvd x
Proof state after:
no goals
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
⊢ abs a.re = 1 ∧ a.im = 0
Tactic:
suffices H : abs a.re = 1
Proof state after:
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
H : abs a.re = 1
⊢ abs a.re = 1 ∧ a.im = 0

case H
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
⊢ abs a.re = 1
Theorem: Spts.eq_one
Proof state before:
case H
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
⊢ abs a.re = 1
Tactic:
contrapose! h
Proof state after:
case H
a : ℤ√(-3)
h : abs a.re ≠ 1
⊢ Zsqrtd.norm a ≠ 1
Theorem: Spts.eq_one
Proof state before:
case H
a : ℤ√(-3)
h : abs a.re ≠ 1
⊢ Zsqrtd.norm a ≠ 1
Tactic:
cases' lt_or_gt_of_ne h with H H
Proof state after:
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
⊢ Zsqrtd.norm a ≠ 1

case H.inr
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ Zsqrtd.norm a ≠ 1
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
H : abs a.re = 1
⊢ abs a.re = 1 ∧ a.im = 0
Tactic:
refine' ⟨H, _⟩
Proof state after:
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
H : abs a.re = 1
⊢ a.im = 0
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
H : abs a.re = 1
⊢ a.im = 0
Tactic:
rw [Zsqrtd.norm_def, mul_assoc, ← Int.natAbs_mul_self' a.re, ← Int.abs_eq_natAbs, H, one_mul,
  neg_mul, sub_neg_eq_add, add_right_eq_self, mul_eq_zero, mul_self_eq_zero] at h
Proof state after:
a : ℤ√(-3)
h : 3 = 0 ∨ a.im = 0
H : abs a.re = 1
⊢ a.im = 0
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : 3 = 0 ∨ a.im = 0
H : abs a.re = 1
⊢ a.im = 0
Tactic:
exact h.resolve_left three_ne_zero
Proof state after:
no goals
Theorem: Spts.eq_one
Proof state before:
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
⊢ Zsqrtd.norm a ≠ 1
Tactic:
have : a.re = 0 := by rwa [← Int.abs_lt_one_iff]
Proof state after:
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
⊢ Zsqrtd.norm a ≠ 1
Theorem: Spts.eq_one
Proof state before:
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
⊢ Zsqrtd.norm a ≠ 1
Tactic:
simp only [Zsqrtd.norm_def, this, MulZeroClass.zero_mul, zero_sub, neg_mul, neg_neg]
Proof state after:
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
⊢ 3 * a.im * a.im ≠ 1
Theorem: Spts.eq_one
Proof state before:
case H.inl
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
⊢ 3 * a.im * a.im ≠ 1
Tactic:
by_cases hb : a.im = 0
Proof state after:
case pos
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
hb : a.im = 0
⊢ 3 * a.im * a.im ≠ 1

case neg
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
hb : ¬a.im = 0
⊢ 3 * a.im * a.im ≠ 1
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
⊢ a.re = 0
Tactic:
rwa [← Int.abs_lt_one_iff]
Proof state after:
no goals
Theorem: Spts.eq_one
Proof state before:
case pos
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
hb : a.im = 0
⊢ 3 * a.im * a.im ≠ 1
Tactic:
simp only [hb, not_false_iff, zero_ne_one, MulZeroClass.mul_zero]
Proof state after:
no goals
Theorem: Spts.eq_one
Proof state before:
case neg
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
hb : ¬a.im = 0
⊢ 3 * a.im * a.im ≠ 1
Tactic:
have : 1 ≤ abs a.im := by rwa [← Int.abs_lt_one_iff, not_lt] at hb
Proof state after:
case neg
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ abs a.im
⊢ 3 * a.im * a.im ≠ 1
Theorem: Spts.eq_one
Proof state before:
case neg
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ abs a.im
⊢ 3 * a.im * a.im ≠ 1
Tactic:
have : 1 ≤ a.im ^ 2 := by
  rw [← sq_abs]
  exact pow_le_pow_of_le_left zero_le_one this 2
Proof state after:
case neg
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝¹ : a.re = 0
hb : ¬a.im = 0
this✝ : 1 ≤ abs a.im
this : 1 ≤ a.im ^ 2
⊢ 3 * a.im * a.im ≠ 1
Theorem: Spts.eq_one
Proof state before:
case neg
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝¹ : a.re = 0
hb : ¬a.im = 0
this✝ : 1 ≤ abs a.im
this : 1 ≤ a.im ^ 2
⊢ 3 * a.im * a.im ≠ 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this : a.re = 0
hb : ¬a.im = 0
⊢ 1 ≤ abs a.im
Tactic:
rwa [← Int.abs_lt_one_iff, not_lt] at hb
Proof state after:
no goals
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ abs a.im
⊢ 1 ≤ a.im ^ 2
Tactic:
rw [← sq_abs]
Proof state after:
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ abs a.im
⊢ 1 ≤ abs a.im ^ 2
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ abs a.im
⊢ 1 ≤ abs a.im ^ 2
Tactic:
exact pow_le_pow_of_le_left zero_le_one this 2
Proof state after:
no goals
Theorem: Spts.eq_one
Proof state before:
case H.inr
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ Zsqrtd.norm a ≠ 1
Tactic:
apply ne_of_gt
Proof state after:
case H.inr.h
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < Zsqrtd.norm a
Theorem: Spts.eq_one
Proof state before:
case H.inr.h
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < Zsqrtd.norm a
Tactic:
rw [Zsqrtd.norm_def, neg_mul, neg_mul, sub_neg_eq_add]
Proof state after:
case H.inr.h
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < a.re * a.re + 3 * a.im * a.im
Theorem: Spts.eq_one
Proof state before:
case H.inr.h
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < a.re * a.re + 3 * a.im * a.im
Tactic:
apply lt_add_of_lt_of_nonneg
Proof state after:
case H.inr.h.hbc
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < a.re * a.re

case H.inr.h.ha
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 0 ≤ 3 * a.im * a.im
Theorem: Spts.eq_one
Proof state before:
case H.inr.h.hbc
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < a.re * a.re
Tactic:
rw [← sq, ← sq_abs]
Proof state after:
case H.inr.h.hbc
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < abs a.re ^ 2
Theorem: Spts.eq_one
Proof state before:
case H.inr.h.hbc
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 1 < abs a.re ^ 2
Tactic:
exact pow_lt_pow_of_lt_left H zero_le_one zero_lt_two
Proof state after:
no goals
Theorem: Spts.eq_one
Proof state before:
case H.inr.h.ha
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 0 ≤ 3 * a.im * a.im
Tactic:
rw [mul_assoc]
Proof state after:
case H.inr.h.ha
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 0 ≤ 3 * (a.im * a.im)
Theorem: Spts.eq_one
Proof state before:
case H.inr.h.ha
a : ℤ√(-3)
h : abs a.re ≠ 1
H : abs a.re > 1
⊢ 0 ≤ 3 * (a.im * a.im)
Tactic:
exact mul_nonneg zero_lt_three.le (mul_self_nonneg _)
Proof state after:
no goals
Theorem: Spts.eq_one'
Proof state before:
a : ℤ√(-3)
h : Zsqrtd.norm a = 1
⊢ a = 1 ∨ a = -1
Tactic:
simp only [Zsqrtd.ext, Zsqrtd.one_re, Zsqrtd.one_im, Zsqrtd.neg_im, Zsqrtd.neg_re, neg_zero, ←
  or_and_right, ← abs_eq (zero_le_one' ℤ), Spts.eq_one h, eq_self_iff_true, and_self_iff]
Proof state after:
no goals
Theorem: Spts.ne_zero_of_coprime'
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ Zsqrtd.norm a ≠ 0
Tactic:
contrapose! hcoprime with H
Proof state after:
a : ℤ√(-3)
H : Zsqrtd.norm a = 0
⊢ ¬IsCoprime a.re a.im
Theorem: Spts.ne_zero_of_coprime'
Proof state before:
a : ℤ√(-3)
H : Zsqrtd.norm a = 0
⊢ ¬IsCoprime a.re a.im
Tactic:
obtain ⟨rfl, rfl⟩ := (Zsqrtd.norm_eq_zero_iff (by norm_num) _).mp H
Proof state after:
case refl
H : Zsqrtd.norm 0 = 0
⊢ ¬IsCoprime 0.re 0.im
Theorem: Spts.ne_zero_of_coprime'
Proof state before:
case refl
H : Zsqrtd.norm 0 = 0
⊢ ¬IsCoprime 0.re 0.im
Tactic:
exact not_isCoprime_zero_zero
Proof state after:
no goals
Theorem: Spts.ne_zero_of_coprime'
Proof state before:
a : ℤ√(-3)
H : Zsqrtd.norm a = 0
⊢ -3 < 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Spts.pos_of_coprime'
Proof state before:
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 < Zsqrtd.norm a
Tactic:
apply lt_of_le_of_ne
Proof state after:
case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≤ Zsqrtd.norm a

case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≠ Zsqrtd.norm a
Theorem: Spts.pos_of_coprime'
Proof state before:
case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≤ Zsqrtd.norm a
Tactic:
apply Zsqrtd.norm_nonneg
Proof state after:
case a.hd
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ -3 ≤ 0
Theorem: Spts.pos_of_coprime'
Proof state before:
case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≠ Zsqrtd.norm a
Tactic:
apply Ne.symm
Proof state after:
case a.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ Zsqrtd.norm a ≠ 0
Theorem: Spts.pos_of_coprime'
Proof state before:
case a.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ Zsqrtd.norm a ≠ 0
Tactic:
exact Spts.ne_zero_of_coprime' _ hcoprime
Proof state after:
no goals
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 1 < Zsqrtd.norm a
Tactic:
apply lt_of_le_of_ne
Proof state after:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 1 ≤ Zsqrtd.norm a

case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 1 ≠ Zsqrtd.norm a
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 1 ≤ Zsqrtd.norm a
Tactic:
rw [← Int.sub_one_lt_iff, sub_self]
Proof state after:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 0 < Zsqrtd.norm a
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 0 < Zsqrtd.norm a
Tactic:
apply lt_of_le_of_ne (Zsqrtd.norm_nonneg (by norm_num) a)
Proof state after:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 0 ≠ Zsqrtd.norm a
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 0 ≠ Zsqrtd.norm a
Tactic:
contrapose! hb
Proof state after:
case a
a : ℤ√(-3)
hb : 0 = Zsqrtd.norm a
⊢ a.im = 0
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
case a
a : ℤ√(-3)
hb : 0 = Zsqrtd.norm a
⊢ a.im = 0
Tactic:
rw [eq_comm, Zsqrtd.norm_eq_zero_iff (by norm_num) a] at hb
Proof state after:
case a
a : ℤ√(-3)
hb : a = 0
⊢ a.im = 0
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
a : ℤ√(-3)
hb : Zsqrtd.norm a = 0
⊢ -3 < 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 1 ≠ Zsqrtd.norm a
Tactic:
intro H
Proof state after:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
H : 1 = Zsqrtd.norm a
⊢ False
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
H : 1 = Zsqrtd.norm a
⊢ False
Tactic:
exact hb (Spts.eq_one H.symm).2
Proof state after:
no goals