internlm/Lean-Github huggingface dataset:
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : ¬Even a.norm
p : ℤ
pprime : Prime p
this✝ : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
pdvd' : A.norm ∣ a.norm
c : ℤ√(-3)
hcd : a.norm = A.norm * c.norm
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (p * q).natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
h : ¬(p * q).natAbs = 1
hqpos : q ≠ 0
this : (p.sign * q).natAbs = q.natAbs
⊢ ∀ (f' : ℤ), f' ∣ p.sign * q → Odd f' → ∃ p, |f'| = p.norm
Tactic:
intro f' hf'dvd hf'odd
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : ¬Even a.norm
p : ℤ
pprime : Prime p
this✝ : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
pdvd' : A.norm ∣ a.norm
c : ℤ√(-3)
hcd : a.norm = A.norm * c.norm
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (p * q).natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
h : ¬(p * q).natAbs = 1
hqpos : q ≠ 0
this : (p.sign * q).natAbs = q.natAbs
f' : ℤ
hf'dvd : f' ∣ p.sign * q
hf'odd : Odd f'
⊢ ∃ p, |f'| = p.norm
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : ¬Even a.norm
p : ℤ
pprime : Prime p
this✝ : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
pdvd' : A.norm ∣ a.norm
c : ℤ√(-3)
hcd : a.norm = A.norm * c.norm
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (p * q).natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
h : ¬(p * q).natAbs = 1
hqpos : q ≠ 0
this : (p.sign * q).natAbs = q.natAbs
f' : ℤ
hf'dvd : f' ∣ p.sign * q
hf'odd : Odd f'
⊢ ∃ p, |f'| = p.norm
Tactic:
refine' hnotform f' _ hf'odd
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : ¬Even a.norm
p : ℤ
pprime : Prime p
this✝ : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
pdvd' : A.norm ∣ a.norm
c : ℤ√(-3)
hcd : a.norm = A.norm * c.norm
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (p * q).natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
h : ¬(p * q).natAbs = 1
hqpos : q ≠ 0
this : (p.sign * q).natAbs = q.natAbs
f' : ℤ
hf'dvd : f' ∣ p.sign * q
hf'odd : Odd f'
⊢ f' ∣ p * q
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : ¬Even a.norm
p : ℤ
pprime : Prime p
this✝ : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
pdvd' : A.norm ∣ a.norm
c : ℤ√(-3)
hcd : a.norm = A.norm * c.norm
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (p * q).natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
h : ¬(p * q).natAbs = 1
hqpos : q ≠ 0
this : (p.sign * q).natAbs = q.natAbs
f' : ℤ
hf'dvd : f' ∣ p.sign * q
hf'odd : Odd f'
⊢ f' ∣ p * q
Tactic:
rw [← Int.dvd_natAbs, this, Int.dvd_natAbs] at hf'dvd
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : ¬Even a.norm
p : ℤ
pprime : Prime p
this✝ : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
pdvd' : A.norm ∣ a.norm
c : ℤ√(-3)
hcd : a.norm = A.norm * c.norm
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (p * q).natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
h : ¬(p * q).natAbs = 1
hqpos : q ≠ 0
this : (p.sign * q).natAbs = q.natAbs
f' : ℤ
hf'dvd : f' ∣ q
hf'odd : Odd f'
⊢ f' ∣ p * q
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : ¬Even a.norm
p : ℤ
pprime : Prime p
this✝ : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
pdvd' : A.norm ∣ a.norm
c : ℤ√(-3)
hcd : a.norm = A.norm * c.norm
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (p * q).natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
h : ¬(p * q).natAbs = 1
hqpos : q ≠ 0
this : (p.sign * q).natAbs = q.natAbs
f' : ℤ
hf'dvd : f' ∣ q
hf'odd : Odd f'
⊢ f' ∣ p * q
Tactic:
exact hf'dvd.mul_left _
Proof state after:
no goals
Theorem: Zqrtd.factor_div
Proof 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
Proof 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
Theorem: Zqrtd.factor_div
Proof 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
Proof 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
Theorem: Zqrtd.factor_div
Proof 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⟩
Proof 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
Theorem: Zqrtd.factor_div
Proof 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⟩, _, _⟩
Proof 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
Theorem: Zqrtd.factor_div
Proof 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]
Proof state after:
no goals
Theorem: Zqrtd.factor_div
Proof 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)]
Proof 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
Theorem: Zqrtd.factor_div
Proof 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
Proof 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
Theorem: Zqrtd.factor_div
Proof 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
Proof state after:
no goals
Theorem: Zqrtd.factor_div
Proof 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]
Proof 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
Theorem: Zqrtd.factor_div
Proof 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
Proof state after:
no goals
Theorem: Zqrtd.factor_div
Proof 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
Proof state after:
no goals
Theorem: Zqrtd.factor_div
Proof 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]
Proof 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
Theorem: Zqrtd.factor_div
Proof 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
Proof 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
Theorem: Zqrtd.factor_div
Proof 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
Proof state after:
no goals
Theorem: Zqrtd.factor_div
Proof 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)]
Proof 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
Theorem: Zqrtd.factor_div
Proof 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
Proof 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
Theorem: Zqrtd.factor_div
Proof 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
Proof state after:
no goals
Theorem: Zqrtd.factor_div
Proof 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
Proof state after:
no goals
Theorem: Zqrtd.factor_div'
Proof 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
Proof 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
Theorem: Zqrtd.factor_div'
Proof 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, _, _⟩
Proof 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
Theorem: Zqrtd.factor_div'
Proof 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
Proof 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
Theorem: Zqrtd.factor_div'
Proof 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'
Proof 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
Theorem: Zqrtd.factor_div'
Proof 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]
Proof 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
Theorem: Zqrtd.factor_div'
Proof 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]
Proof state after:
no goals
Theorem: Zqrtd.factor_div'
Proof 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
Proof 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
Theorem: Zqrtd.factor_div'
Proof 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, _⟩
Proof 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
Theorem: Zqrtd.factor_div'
Proof 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
Proof 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
Theorem: Zqrtd.factor_div'
Proof 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]
Proof 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
Theorem: Zqrtd.factor_div'
Proof 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
Proof 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
Theorem: Zqrtd.factor_div'
Proof 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)]
Proof state after:
no goals
Theorem: Zqrtd.factor_div'
Proof 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
Proof 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
Theorem: Zqrtd.factor_div'
Proof 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)
Proof 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