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