Theorem: Zqrtd.factor_div' (Flt/Spts.lean)

State before:
a : ℤ√(-3)
x : ℤ
hodd : Odd x
h : 1 < abs x
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ Zsqrtd.norm a
⊢ ∃ c m, a = c + m * ↑x ∧ Zsqrtd.norm c < x ^ 2 ∧ c ≠ 0 ∧ ∃ y, Zsqrtd.norm c = x * y ∧ Int.natAbs y < Int.natAbs x
Tactic:
obtain ⟨c, m, rfl, h2⟩ := Zqrtd.factor_div a hodd
State after:
case intro.intro.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
⊢ ∃ c_1 m_1,
    c + m * ↑x = c_1 + m_1 * ↑x ∧
      Zsqrtd.norm c_1 < x ^ 2 ∧ c_1 ≠ 0 ∧ ∃ y, Zsqrtd.norm c_1 = x * y ∧ Int.natAbs y < Int.natAbs x

State before:
case intro.intro.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
⊢ ∃ c_1 m_1,
    c + m * ↑x = c_1 + m_1 * ↑x ∧
      Zsqrtd.norm c_1 < x ^ 2 ∧ c_1 ≠ 0 ∧ ∃ y, Zsqrtd.norm c_1 = x * y ∧ Int.natAbs y < Int.natAbs x
Tactic:
refine' ⟨c, m, rfl, h2, _, _⟩
State after:
case intro.intro.intro.refine'_1
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
⊢ c ≠ 0

case intro.intro.intro.refine'_2
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
⊢ ∃ y, Zsqrtd.norm c = x * y ∧ Int.natAbs y < Int.natAbs x

State before:
case intro.intro.intro.refine'_1
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
⊢ c ≠ 0
Tactic:
rintro rfl
State after:
case intro.intro.intro.refine'_1
x : ℤ
hodd : Odd x
h : 1 < abs x
m : ℤ√(-3)
h2 : Zsqrtd.norm 0 < x ^ 2
hcoprime : IsCoprime (0 + m * ↑x).re (0 + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (0 + m * ↑x)
⊢ False

State before:
case intro.intro.intro.refine'_1
x : ℤ
hodd : Odd x
h : 1 < abs x
m : ℤ√(-3)
h2 : Zsqrtd.norm 0 < x ^ 2
hcoprime : IsCoprime (0 + m * ↑x).re (0 + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (0 + m * ↑x)
⊢ False
Tactic:
apply h.ne'
State after:
case intro.intro.intro.refine'_1
x : ℤ
hodd : Odd x
h : 1 < abs x
m : ℤ√(-3)
h2 : Zsqrtd.norm 0 < x ^ 2
hcoprime : IsCoprime (0 + m * ↑x).re (0 + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (0 + m * ↑x)
⊢ abs x = 1

State before:
case intro.intro.intro.refine'_1
x : ℤ
hodd : Odd x
h : 1 < abs x
m : ℤ√(-3)
h2 : Zsqrtd.norm 0 < x ^ 2
hcoprime : IsCoprime (0 + m * ↑x).re (0 + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (0 + m * ↑x)
⊢ abs x = 1
Tactic:
rw [← Int.isUnit_iff_abs_eq]
State after:
case intro.intro.intro.refine'_1
x : ℤ
hodd : Odd x
h : 1 < abs x
m : ℤ√(-3)
h2 : Zsqrtd.norm 0 < x ^ 2
hcoprime : IsCoprime (0 + m * ↑x).re (0 + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (0 + m * ↑x)
⊢ IsUnit x

State before:
case intro.intro.intro.refine'_1
x : ℤ
hodd : Odd x
h : 1 < abs x
m : ℤ√(-3)
h2 : Zsqrtd.norm 0 < x ^ 2
hcoprime : IsCoprime (0 + m * ↑x).re (0 + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (0 + m * ↑x)
⊢ IsUnit x
Tactic:
apply hcoprime.isUnit_of_dvd' <;>
  simp only [zero_add, mul_comm m, Zsqrtd.smul_re, Zsqrtd.smul_im, dvd_mul_right]
State after:
no goals

State before:
case intro.intro.intro.refine'_2
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
⊢ ∃ y, Zsqrtd.norm c = x * y ∧ Int.natAbs y < Int.natAbs x
Tactic:
obtain ⟨y, hy⟩ : x ∣ c.norm :=
  by
  set e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im with he
  convert dvd_sub hfactor (dvd_mul_right x e)
  rw [he, Zsqrtd.norm_def, Zsqrtd.norm_def]
  simp only [Zsqrtd.coe_int_re, Zsqrtd.mul_im, Zsqrtd.add_im, Zsqrtd.mul_re, Zsqrtd.add_re,
    Zsqrtd.coe_int_im]
  ring
State after:
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
⊢ ∃ y, Zsqrtd.norm c = x * y ∧ Int.natAbs y < Int.natAbs x

State before:
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
⊢ ∃ y, Zsqrtd.norm c = x * y ∧ Int.natAbs y < Int.natAbs x
Tactic:
refine' ⟨y, hy, _⟩
State after:
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
⊢ Int.natAbs y < Int.natAbs x

State before:
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
⊢ Int.natAbs y < Int.natAbs x
Tactic:
have h0'' : 0 < x.natAbs := by
  zify
  exact zero_lt_one.trans h
State after:
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
h0'' : 0 < Int.natAbs x
⊢ Int.natAbs y < Int.natAbs x

State before:
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
h0'' : 0 < Int.natAbs x
⊢ Int.natAbs y < Int.natAbs x
Tactic:
rw [← mul_lt_mul_left h0'', ← pow_two, ← Int.natAbs_mul, ← hy]
State after:
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
h0'' : 0 < Int.natAbs x
⊢ Int.natAbs (Zsqrtd.norm c) < Int.natAbs x ^ 2

State before:
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
h0'' : 0 < Int.natAbs x
⊢ Int.natAbs (Zsqrtd.norm c) < Int.natAbs x ^ 2
Tactic:
zify
State after:
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
h0'' : 0 < Int.natAbs x
⊢ abs (Zsqrtd.norm c) < abs x ^ 2

State before:
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
h0'' : 0 < Int.natAbs x
⊢ abs (Zsqrtd.norm c) < abs x ^ 2
Tactic:
rwa [← Int.coe_natAbs x, Int.natAbs_pow_two x, ← Int.coe_natAbs,
  Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) c)]
State after:
no goals

State before:
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
⊢ x ∣ Zsqrtd.norm c
Tactic:
set e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im with he
State after:
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
he : e = m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
⊢ x ∣ Zsqrtd.norm c

State before:
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
he : e = m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
⊢ x ∣ Zsqrtd.norm c
Tactic:
convert dvd_sub hfactor (dvd_mul_right x e)
State after:
case h.e'_4
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
he : e = m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
⊢ Zsqrtd.norm c = Zsqrtd.norm (c + m * ↑x) - x * e

State before:
case h.e'_4
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
he : e = m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
⊢ Zsqrtd.norm c = Zsqrtd.norm (c + m * ↑x) - x * e
Tactic:
rw [he, Zsqrtd.norm_def, Zsqrtd.norm_def]
State after:
case h.e'_4
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
he : e = m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
⊢ c.re * c.re - -3 * c.im * c.im =
    (c + m * ↑x).re * (c + m * ↑x).re - -3 * (c + m * ↑x).im * (c + m * ↑x).im -
      x * (m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im)

State before:
case h.e'_4
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
he : e = m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
⊢ c.re * c.re - -3 * c.im * c.im =
    (c + m * ↑x).re * (c + m * ↑x).re - -3 * (c + m * ↑x).im * (c + m * ↑x).im -
      x * (m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im)
Tactic:
simp only [Zsqrtd.coe_int_re, Zsqrtd.mul_im, Zsqrtd.add_im, Zsqrtd.mul_re, Zsqrtd.add_re,
  Zsqrtd.coe_int_im]
State after:
case h.e'_4
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
he : e = m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
⊢ c.re * c.re - -3 * c.im * c.im =
    (c.re + (m.re * x + -3 * m.im * 0)) * (c.re + (m.re * x + -3 * m.im * 0)) -
        -3 * (c.im + (m.re * 0 + m.im * x)) * (c.im + (m.re * 0 + m.im * x)) -
      x * (m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im)

State before:
case h.e'_4
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
he : e = m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im
⊢ c.re * c.re - -3 * c.im * c.im =
    (c.re + (m.re * x + -3 * m.im * 0)) * (c.re + (m.re * x + -3 * m.im * 0)) -
        -3 * (c.im + (m.re * 0 + m.im * x)) * (c.im + (m.re * 0 + m.im * x)) -
      x * (m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im)
Tactic:
ring
State after:
no goals

State before:
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
⊢ 0 < Int.natAbs x
Tactic:
zify
State after:
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
⊢ 0 < abs x

State before:
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
⊢ 0 < abs x
Tactic:
exact zero_lt_one.trans h
State after:
no goals

State before:
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
h0'' : 0 < Int.natAbs x
⊢ -3 ≤ 0
Tactic:
norm_num
State after:
no goals