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

State before:
a : ℤ√(-3)
x : ℤ
hodd : Odd x
⊢ ∃ c m, a = c + m * ↑x ∧ c.norm < 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 * c.natAbs < x.natAbs
⊢ ∃ c m, a = c + m * ↑x ∧ c.norm < x ^ 2

State before:
case intro.intro.intro
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * c.natAbs < x.natAbs
⊢ ∃ c m, a = c + m * ↑x ∧ c.norm < 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
⊢ ∃ c m, a = c + m * ↑x ∧ c.norm < 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
⊢ ∃ c m, a = c + m * ↑x ∧ c.norm < 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ ∃ c m, a = c + m * ↑x ∧ c.norm < 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ ∃ c m, a = c + m * ↑x ∧ c.norm < 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ c'.norm < 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ a = c' + { re := m, im := n } * ↑x
Tactic:
simp only [Zsqrtd.ext_iff, ha, hb, add_zero, Zsqrtd.intCast_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.intCast_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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ c'.norm < 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ 4 * c'.norm < 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ 4 * c'.norm < 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ 4 * c'.norm = (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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * ↑c.natAbs) ^ 2 < ↑x.natAbs ^ 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * ↑c.natAbs) ^ 2 < ↑x.natAbs ^ 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * c.natAbs) ^ 2 < x.natAbs ^ 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * c.natAbs) ^ 2 < x.natAbs ^ 2
Tactic:
exact Nat.pow_lt_pow_left hc two_ne_zero
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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * ↑d.natAbs) ^ 2 < ↑x.natAbs ^ 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * ↑d.natAbs) ^ 2 < ↑x.natAbs ^ 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * d.natAbs) ^ 2 < x.natAbs ^ 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 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ (2 * d.natAbs) ^ 2 < x.natAbs ^ 2
Tactic:
exact Nat.pow_lt_pow_left hd two_ne_zero
State after:
no goals

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