internlm/Lean-Github huggingface dataset:
Theorem: factors
Proof state before:
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
this : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
⊢ ↑p ∣ ↑↑(c'.re.gcd c'.im) * C' + m * ↑x
Tactic:
exact
  dvd_add
    (dvd_mul_of_dvd_left
      ((Zsqrtd.intCast_dvd_intCast _ _).mpr (hpprime.dvd_of_dvd_pow hpdvdleft)) _)
    (dvd_mul_of_dvd_right ((Zsqrtd.intCast_dvd_intCast _ _).mpr hpdvdright) _)
Proof state after:
no goals
Theorem: factors
Proof state before:
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
⊢ x * z = C'.norm
Tactic:
apply Int.eq_of_mul_eq_mul_left (pow_ne_zero 2 <| Int.natCast_ne_zero_iff_pos.mpr hgpos)
Proof state after:
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
⊢ ↑g ^ 2 * (x * z) = ↑g ^ 2 * C'.norm
Theorem: factors
Proof state before:
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
⊢ ↑g ^ 2 * (x * z) = ↑g ^ 2 * C'.norm
Tactic:
rw [← h5, hz, mul_left_comm]
Proof state after:
no goals
Theorem: factors
Proof state before:
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
⊢ z ≠ 0
Tactic:
apply right_ne_zero_of_mul
Proof state after:
case a
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
⊢ ?a * z ≠ 0

case a
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
⊢ ℤ
Theorem: factors
Proof state before:
case a.a
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
⊢ ?a.a✝ * (?a * z) ≠ 0

case a.a
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
⊢ ℤ

case a
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
⊢ ℤ
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
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ w.natAbs < x.natAbs
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:
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ z.natAbs ≤ y.natAbs
Tactic:
rw [hz, Int.natAbs_mul]
Proof state after:
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ z.natAbs ≤ (↑g ^ 2).natAbs * z.natAbs
Theorem: factors
Proof state before:
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ z.natAbs ≤ (↑g ^ 2).natAbs * z.natAbs
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
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ w ∣ C'.norm
Tactic:
rw [← h6]
Proof state after:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
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
x : ℤ
hodd : Odd x
IH : ∀ m < x.natAbs, ∀ (a : ℤ√(-3)) (x : ℤ), IsCoprime a.re a.im → Odd x → x ∣ a.norm → x.natAbs = m → ∃ c, |x| = c.norm
h0 : x ≠ 0
h0' : 1 ≤ |x|
h : 1 < |x|
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ (c' + m * ↑x).norm
hneg1 : 1 ≤ (c' + m * ↑x).norm
h1 : c' ≠ 0
y : ℤ
hy : c'.norm = x * y
h3 : y.natAbs < x.natAbs
h4 : c'.norm ≠ 0
g : ℕ := c'.re.gcd c'.im
hg : g = c'.re.gcd c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(c'.re.gcd c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * C'.norm
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = C'.norm
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 : a.norm = 1
⊢ |a.re| = 1 ∧ a.im = 0
Tactic:
suffices H : abs a.re = 1 by
  refine' ⟨H, _⟩
  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
  exact h.resolve_left three_ne_zero
Proof state after:
a : ℤ√(-3)
h : a.norm = 1
⊢ |a.re| = 1
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : a.norm = 1
⊢ |a.re| = 1
Tactic:
contrapose! h
Proof state after:
a : ℤ√(-3)
h : |a.re| ≠ 1
⊢ a.norm ≠ 1
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : |a.re| ≠ 1
⊢ a.norm ≠ 1
Tactic:
cases' lt_or_gt_of_ne h with H H
Proof state after:
case inl
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| < 1
⊢ a.norm ≠ 1

case inr
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| > 1
⊢ a.norm ≠ 1
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : a.norm = 1
H : |a.re| = 1
⊢ |a.re| = 1 ∧ a.im = 0
Tactic:
refine' ⟨H, _⟩
Proof state after:
a : ℤ√(-3)
h : a.norm = 1
H : |a.re| = 1
⊢ a.im = 0
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : a.norm = 1
H : |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 : |a.re| = 1
⊢ a.im = 0
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : 3 = 0 ∨ a.im = 0
H : |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 inl
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| < 1
⊢ a.norm ≠ 1
Tactic:
have : a.re = 0 := by rwa [← Int.abs_lt_one_iff]
Proof state after:
case inl
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| < 1
this : a.re = 0
⊢ a.norm ≠ 1
Theorem: Spts.eq_one
Proof state before:
case inl
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| < 1
this : a.re = 0
⊢ a.norm ≠ 1
Tactic:
simp only [Zsqrtd.norm_def, this, MulZeroClass.zero_mul, zero_sub, neg_mul, neg_neg]
Proof state after:
case inl
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| < 1
this : a.re = 0
⊢ 3 * a.im * a.im ≠ 1
Theorem: Spts.eq_one
Proof state before:
case inl
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |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 : |a.re| ≠ 1
H : |a.re| < 1
this : a.re = 0
hb : a.im = 0
⊢ 3 * a.im * a.im ≠ 1

case neg
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |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 : |a.re| ≠ 1
H : |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 : |a.re| ≠ 1
H : |a.re| < 1
this : a.re = 0
hb : a.im = 0
⊢ 3 * a.im * a.im ≠ 1
Tactic:
simp [hb]
Proof state after:
no goals
Theorem: Spts.eq_one
Proof state before:
case neg
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |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 : |a.re| ≠ 1
H : |a.re| < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ |a.im|
⊢ 3 * a.im * a.im ≠ 1
Theorem: Spts.eq_one
Proof state before:
case neg
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ |a.im|
⊢ 3 * a.im * a.im ≠ 1
Tactic:
have : 1 ≤ a.im ^ 2 := by
  rw [← sq_abs]
  exact pow_le_pow_left zero_le_one this 2
Proof state after:
case neg
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| < 1
this✝¹ : a.re = 0
hb : ¬a.im = 0
this✝ : 1 ≤ |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 : |a.re| ≠ 1
H : |a.re| < 1
this✝¹ : a.re = 0
hb : ¬a.im = 0
this✝ : 1 ≤ |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 : |a.re| ≠ 1
H : |a.re| < 1
this : a.re = 0
hb : ¬a.im = 0
⊢ 1 ≤ |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 : |a.re| ≠ 1
H : |a.re| < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ |a.im|
⊢ 1 ≤ a.im ^ 2
Tactic:
rw [← sq_abs]
Proof state after:
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ |a.im|
⊢ 1 ≤ |a.im| ^ 2
Theorem: Spts.eq_one
Proof state before:
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| < 1
this✝ : a.re = 0
hb : ¬a.im = 0
this : 1 ≤ |a.im|
⊢ 1 ≤ |a.im| ^ 2
Tactic:
exact pow_le_pow_left zero_le_one this 2
Proof state after:
no goals
Theorem: Spts.eq_one
Proof state before:
case inr
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| > 1
⊢ a.norm ≠ 1
Tactic:
apply ne_of_gt
Proof state after:
case inr.h
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| > 1
⊢ 1 < a.norm
Theorem: Spts.eq_one
Proof state before:
case inr.h
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| > 1
⊢ 1 < a.norm
Tactic:
rw [Zsqrtd.norm_def, neg_mul, neg_mul, sub_neg_eq_add]
Proof state after:
case inr.h
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| > 1
⊢ 1 < a.re * a.re + 3 * a.im * a.im
Theorem: Spts.eq_one
Proof state before:
case inr.h
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |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 inr.h.hbc
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| > 1
⊢ 1 < a.re * a.re

case inr.h.ha
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| > 1
⊢ 0 ≤ 3 * a.im * a.im
Theorem: Spts.eq_one
Proof state before:
case inr.h.hbc
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| > 1
⊢ 1 < a.re * a.re
Tactic:
rw [← sq, ← sq_abs]
Proof state after:
case inr.h.hbc
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| > 1
⊢ 1 < |a.re| ^ 2
Theorem: Spts.eq_one
Proof state before:
case inr.h.hbc
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| > 1
⊢ 1 < |a.re| ^ 2
Tactic:
exact pow_lt_pow_left H zero_le_one two_ne_zero
Proof state after:
no goals
Theorem: Spts.eq_one
Proof state before:
case inr.h.ha
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| > 1
⊢ 0 ≤ 3 * a.im * a.im
Tactic:
rw [mul_assoc]
Proof state after:
case inr.h.ha
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |a.re| > 1
⊢ 0 ≤ 3 * (a.im * a.im)
Theorem: Spts.eq_one
Proof state before:
case inr.h.ha
a : ℤ√(-3)
h : |a.re| ≠ 1
H : |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 : a.norm = 1
⊢ a = 1 ∨ a = -1
Tactic:
simp only [Zsqrtd.ext_iff, 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
⊢ a.norm ≠ 0
Tactic:
contrapose! hcoprime with H
Proof state after:
a : ℤ√(-3)
H : a.norm = 0
⊢ ¬IsCoprime a.re a.im
Theorem: Spts.ne_zero_of_coprime'
Proof state before:
a : ℤ√(-3)
H : a.norm = 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 (Zsqrtd.re 0) (Zsqrtd.im 0)
Theorem: Spts.ne_zero_of_coprime'
Proof state before:
case refl
H : Zsqrtd.norm 0 = 0
⊢ ¬IsCoprime (Zsqrtd.re 0) (Zsqrtd.im 0)
Tactic:
exact not_isCoprime_zero_zero
Proof state after:
no goals
Theorem: Spts.ne_zero_of_coprime'
Proof state before:
a : ℤ√(-3)
H : a.norm = 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 < a.norm
Tactic:
apply lt_of_le_of_ne
Proof state after:
case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≤ a.norm

case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≠ a.norm
Theorem: Spts.pos_of_coprime'
Proof state before:
case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≤ a.norm
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.hd
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ -3 ≤ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Spts.pos_of_coprime'
Proof state before:
case a
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ 0 ≠ a.norm
Tactic:
apply Ne.symm
Proof state after:
case a.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ a.norm ≠ 0
Theorem: Spts.pos_of_coprime'
Proof state before:
case a.h
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
⊢ a.norm ≠ 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 < a.norm
Tactic:
apply lt_of_le_of_ne
Proof state after:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 1 ≤ a.norm

case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 1 ≠ a.norm
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 1 ≤ a.norm
Tactic:
rw [← Int.sub_one_lt_iff, sub_self]
Proof state after:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 0 < a.norm
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 0 < a.norm
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 ≠ a.norm
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ 0 ≠ a.norm
Tactic:
contrapose! hb
Proof state after:
case a
a : ℤ√(-3)
hb : 0 = a.norm
⊢ a.im = 0
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
case a
a : ℤ√(-3)
hb : 0 = a.norm
⊢ 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:
case a
a : ℤ√(-3)
hb : a = 0
⊢ a.im = 0
Tactic:
rw [hb, Zsqrtd.zero_im]
Proof state after:
no goals
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
a : ℤ√(-3)
hb : a.im ≠ 0
⊢ -3 ≤ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
a : ℤ√(-3)
hb : a.norm = 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 ≠ a.norm
Tactic:
intro H
Proof state after:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
H : 1 = a.norm
⊢ False
Theorem: Spts.one_lt_of_im_ne_zero
Proof state before:
case a
a : ℤ√(-3)
hb : a.im ≠ 0
H : 1 = a.norm
⊢ False
Tactic:
exact hb (Spts.eq_one H.symm).2
Proof state after:
no goals
Theorem: Spts.not_two
Proof state before:
a : ℤ√(-3)
⊢ a.norm ≠ 2
Tactic:
rw [Zsqrtd.norm_def]
Proof state after:
a : ℤ√(-3)
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2
Theorem: Spts.not_two
Proof state before:
a : ℤ√(-3)
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2
Tactic:
obtain him | him := eq_or_ne a.im 0
Proof state after:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2

case inr
a : ℤ√(-3)
him : a.im ≠ 0
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2
Theorem: Spts.not_two
Proof state before:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ a.re * a.re - -3 * a.im * a.im ≠ 2
Tactic:
rw [him, MulZeroClass.mul_zero, sub_zero, ← Int.natAbs_mul_self, ← sq]
Proof state after:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ ↑(a.re.natAbs ^ 2) ≠ 2
Theorem: Spts.not_two
Proof state before:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ ↑(a.re.natAbs ^ 2) ≠ 2
Tactic:
norm_cast
Proof state after:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ ¬a.re.natAbs ^ 2 = 2
Theorem: Spts.not_two
Proof state before:
case inl
a : ℤ√(-3)
him : a.im = 0
⊢ ¬a.re.natAbs ^ 2 = 2
Tactic:
apply (Nat.pow_left_strictMono two_ne_zero).monotone.ne_of_lt_of_lt_nat 1 <;> norm_num
Proof state after:
no goals