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

State before:
a : ℤ√(-3)
x : ℤ
hodd : Odd x
⊢ ∃ c m, a = c + m * ↑x ∧ Zsqrtd.norm c < x ^ 2
Tactic:
obtain ⟨m, c, ha, hc⟩ := Int.factor_div a.re x hodd
State after:
case intro.intro.intro
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
⊢ ∃ c m, a = c + m * ↑x ∧ Zsqrtd.norm c < x ^ 2

State before:
case intro.intro.intro
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
⊢ ∃ c m, a = c + m * ↑x ∧ Zsqrtd.norm c < x ^ 2
Tactic:
obtain ⟨n, d, hb, hd⟩ := Int.factor_div a.im x hodd
State after:
case intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
⊢ ∃ c m, a = c + m * ↑x ∧ Zsqrtd.norm c < x ^ 2

State before:
case intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
⊢ ∃ c m, a = c + m * ↑x ∧ Zsqrtd.norm c < x ^ 2
Tactic:
set c' : ℤ√(-3) := ⟨c, d⟩
State after:
case intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ ∃ c m, a = c + m * ↑x ∧ Zsqrtd.norm c < x ^ 2

State before:
case intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ ∃ c m, a = c + m * ↑x ∧ Zsqrtd.norm c < x ^ 2
Tactic:
refine' ⟨c', ⟨m, n⟩, _, _⟩
State after:
case intro.intro.intro.intro.intro.intro.refine'_1
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ a = c' + { re := m, im := n } * ↑x

case intro.intro.intro.intro.intro.intro.refine'_2
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ Zsqrtd.norm c' < x ^ 2

State before:
case intro.intro.intro.intro.intro.intro.refine'_1
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ a = c' + { re := m, im := n } * ↑x
Tactic:
simp only [Zsqrtd.ext, ha, hb, add_zero, Zsqrtd.coe_int_re, eq_self_iff_true, Zsqrtd.mul_im,
  zero_add, Zsqrtd.add_im, and_self_iff, Zsqrtd.mul_re, MulZeroClass.mul_zero, Zsqrtd.add_re,
  Zsqrtd.coe_int_im]
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.refine'_2
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ Zsqrtd.norm c' < x ^ 2
Tactic:
rw [← mul_lt_mul_left (by norm_num : (0 : ℤ) < 4)]
State after:
case intro.intro.intro.intro.intro.intro.refine'_2
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ 4 * Zsqrtd.norm c' < 4 * x ^ 2

State before:
case intro.intro.intro.intro.intro.intro.refine'_2
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ 4 * Zsqrtd.norm c' < 4 * x ^ 2
Tactic:
calc
  4 * c'.norm = (2 * c) ^ 2 + 3 * (2 * d) ^ 2 :=
    by
    rw [Zsqrtd.norm_def]
    ring
  _ < x ^ 2 + 3 * x ^ 2 := (add_lt_add ?_ ?_)
  _ = 4 * x ^ 2 := by ring
State after:
case intro.intro.intro.intro.intro.intro.refine'_2.calc_1
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * c) ^ 2 < x ^ 2

case intro.intro.intro.intro.intro.intro.refine'_2.calc_2
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ 3 * (2 * d) ^ 2 < 3 * x ^ 2

State before:
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ 0 < 4
Tactic:
norm_num
State after:
no goals

State before:
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ 4 * Zsqrtd.norm c' = (2 * c) ^ 2 + 3 * (2 * d) ^ 2
Tactic:
rw [Zsqrtd.norm_def]
State after:
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ 4 * (c'.re * c'.re - -3 * c'.im * c'.im) = (2 * c) ^ 2 + 3 * (2 * d) ^ 2

State before:
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ 4 * (c'.re * c'.re - -3 * c'.im * c'.im) = (2 * c) ^ 2 + 3 * (2 * d) ^ 2
Tactic:
ring
State after:
no goals

State before:
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ x ^ 2 + 3 * x ^ 2 = 4 * x ^ 2
Tactic:
ring
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.refine'_2.calc_1
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * c) ^ 2 < x ^ 2
Tactic:
rw [mul_pow, ← Int.natAbs_pow_two c, ← Int.natAbs_pow_two x, ← mul_pow]
State after:
case intro.intro.intro.intro.intro.intro.refine'_2.calc_1
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * ↑(Int.natAbs c)) ^ 2 < ↑(Int.natAbs x) ^ 2

State before:
case intro.intro.intro.intro.intro.intro.refine'_2.calc_1
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * ↑(Int.natAbs c)) ^ 2 < ↑(Int.natAbs x) ^ 2
Tactic:
norm_cast
State after:
case intro.intro.intro.intro.intro.intro.refine'_2.calc_1
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * Int.natAbs c) ^ 2 < Int.natAbs x ^ 2

State before:
case intro.intro.intro.intro.intro.intro.refine'_2.calc_1
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * Int.natAbs c) ^ 2 < Int.natAbs x ^ 2
Tactic:
exact Nat.pow_lt_pow_of_lt_left hc zero_lt_two
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro.refine'_2.calc_2
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ 3 * (2 * d) ^ 2 < 3 * x ^ 2
Tactic:
rw [mul_pow, ← Int.natAbs_pow_two d, ← Int.natAbs_pow_two x, ← mul_pow,
  mul_lt_mul_left (by norm_num : (0 : ℤ) < 3)]
State after:
case intro.intro.intro.intro.intro.intro.refine'_2.calc_2
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * ↑(Int.natAbs d)) ^ 2 < ↑(Int.natAbs x) ^ 2

State before:
case intro.intro.intro.intro.intro.intro.refine'_2.calc_2
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * ↑(Int.natAbs d)) ^ 2 < ↑(Int.natAbs x) ^ 2
Tactic:
norm_cast
State after:
case intro.intro.intro.intro.intro.intro.refine'_2.calc_2
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * Int.natAbs d) ^ 2 < Int.natAbs x ^ 2

State before:
case intro.intro.intro.intro.intro.intro.refine'_2.calc_2
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * Int.natAbs d) ^ 2 < Int.natAbs x ^ 2
Tactic:
exact Nat.pow_lt_pow_of_lt_left hd zero_lt_two
State after:
no goals

State before:
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * Int.natAbs c < Int.natAbs x
n d : ℤ
hb : d + n * x = a.im
hd : 2 * Int.natAbs d < Int.natAbs x
c' : ℤ√(-3) := { re := c, im := d }
⊢ 0 < 3
Tactic:
norm_num
State after:
no goals