Theorem: Zqrtd.factor_div' (FltRegular/FltThree/Spts.lean)

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

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

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

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

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

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

State before:
case intro.intro.intro.refine'_1
x : ℤ
hodd : Odd x
h : 1 < |x|
m : ℤ√(-3)
h2 : Zsqrtd.norm 0 < x ^ 2
hcoprime : IsCoprime (0 + m * ↑x).re (0 + m * ↑x).im
hfactor : x ∣ (0 + m * ↑x).norm
⊢ 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 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
⊢ ∃ y, c.norm = x * y ∧ y.natAbs < x.natAbs
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.intCast_re, Zsqrtd.mul_im, Zsqrtd.add_im, Zsqrtd.mul_re, Zsqrtd.add_re,
    Zsqrtd.intCast_im]
  ring
State after:
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
y : ℤ
hy : c.norm = x * y
⊢ ∃ y, c.norm = x * y ∧ y.natAbs < x.natAbs

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

State before:
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
y : ℤ
hy : c.norm = x * y
⊢ y.natAbs < x.natAbs
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 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
y : ℤ
hy : c.norm = x * y
h0'' : 0 < x.natAbs
⊢ y.natAbs < x.natAbs

State before:
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
y : ℤ
hy : c.norm = x * y
h0'' : 0 < x.natAbs
⊢ y.natAbs < x.natAbs
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 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
y : ℤ
hy : c.norm = x * y
h0'' : 0 < x.natAbs
⊢ c.norm.natAbs < x.natAbs ^ 2

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

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

State before:
x : ℤ
hodd : Odd x
h : 1 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
⊢ x ∣ c.norm
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 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
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 ∣ c.norm

State before:
x : ℤ
hodd : Odd x
h : 1 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
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 ∣ c.norm
Tactic:
convert dvd_sub hfactor (dvd_mul_right x e)
State after:
case h.e'_4
x : ℤ
hodd : Odd x
h : 1 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
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.norm = (c + m * ↑x).norm - x * e

State before:
case h.e'_4
x : ℤ
hodd : Odd x
h : 1 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
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.norm = (c + m * ↑x).norm - x * e
Tactic:
rw [he, Zsqrtd.norm_def, Zsqrtd.norm_def]
State after:
case h.e'_4
x : ℤ
hodd : Odd x
h : 1 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
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 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
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.intCast_re, Zsqrtd.mul_im, Zsqrtd.add_im, Zsqrtd.mul_re, Zsqrtd.add_re,
  Zsqrtd.intCast_im]
State after:
case h.e'_4
x : ℤ
hodd : Odd x
h : 1 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
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 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
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 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
y : ℤ
hy : c.norm = x * y
⊢ 0 < x.natAbs
Tactic:
zify
State after:
x : ℤ
hodd : Odd x
h : 1 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
y : ℤ
hy : c.norm = x * y
⊢ 0 < |x|

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

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