internlm/Lean-Github huggingface dataset:
Theorem: factors'
Proof state before:
case neg.intro.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
⊢ ∃ p, |f| = p.norm
Tactic:
have pprime' := pprime.abs
Proof state after:
case neg.intro.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime |p|
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case neg.intro.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime |p|
⊢ ∃ p, |f| = p.norm
Tactic:
rw [HA] at pprime'
Proof state after:
case neg.intro.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case neg.intro.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
⊢ ∃ p, |f| = p.norm
Tactic:
have pdvd' : A.norm ∣ a.norm := by
  rw [← hfactor, ← HA, abs_dvd]
  exact dvd_mul_of_dvd_right pdvd _
Proof state after:
case neg.intro.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
pdvd' : A.norm ∣ a.norm
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case neg.intro.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
pdvd' : A.norm ∣ a.norm
⊢ ∃ p, |f| = p.norm
Tactic:
obtain ⟨c, -, hcd⟩ := Spts.mul_of_dvd'' pdvd' pprime'
Proof state after:
case neg.intro.intro.intro.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
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
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
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
⊢ ∃ p, |f| = p.norm
Tactic:
obtain ⟨q, rfl⟩ := pdvd
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
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
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
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
⊢ ∃ p, |f| = p.norm
Tactic:
have hqpos : q ≠ 0 := right_ne_zero_of_mul hgpos
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
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
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
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
⊢ ∃ p, |f| = p.norm
Tactic:
have : (p.sign * q).natAbs = q.natAbs := by
  rw [Int.natAbs_mul, Int.natAbs_sign_of_nonzero pprime.ne_zero, one_mul]
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
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
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
⊢ p ∣ a.norm
Tactic:
rw [← hfactor]
Proof state after:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
⊢ p ∣ f * g
Theorem: factors'
Proof state before:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
⊢ p ∣ f * g
Tactic:
exact pdvd.mul_left _
Proof state after:
no goals
Theorem: factors'
Proof state before:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
⊢ ¬Even p
Tactic:
intro X
Proof state after:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
X : Even p
⊢ False
Theorem: factors'
Proof state before:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
X : Even p
⊢ False
Tactic:
apply H
Proof state after:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
X : Even p
⊢ Even a.norm
Theorem: factors'
Proof state before:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
X : Even p
⊢ Even a.norm
Tactic:
apply even_iff_two_dvd.mpr
Proof state after:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
X : Even p
⊢ 2 ∣ a.norm
Theorem: factors'
Proof state before:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
X : Even p
⊢ 2 ∣ a.norm
Tactic:
apply dvd_trans _ this
Proof state after:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
X : Even p
⊢ 2 ∣ p
Theorem: factors'
Proof state before:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
X : Even p
⊢ 2 ∣ p
Tactic:
apply even_iff_two_dvd.mp X
Proof state after:
no goals
Theorem: factors'
Proof state before:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
⊢ A.norm ∣ a.norm
Tactic:
rw [← hfactor, ← HA, abs_dvd]
Proof state after:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
⊢ p ∣ f * g
Theorem: factors'
Proof state before:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < g.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 : ¬Even a.norm
h : ¬g.natAbs = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
⊢ p ∣ f * g
Tactic:
exact dvd_mul_of_dvd_right pdvd _
Proof state after:
no goals
Theorem: factors'
Proof state before:
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
⊢ (p.sign * q).natAbs = q.natAbs
Tactic:
rw [Int.natAbs_mul, Int.natAbs_sign_of_nonzero pprime.ne_zero, one_mul]
Proof state after:
no goals
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.refine'_1
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
⊢ q.natAbs < (p * q).natAbs
Tactic:
rw [Int.natAbs_mul]
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.refine'_1
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
⊢ q.natAbs < p.natAbs * q.natAbs
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.refine'_1
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
⊢ q.natAbs < p.natAbs * q.natAbs
Tactic:
apply lt_mul_of_one_lt_left (Int.natAbs_pos.mpr hqpos)
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.refine'_1
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
⊢ 1 < p.natAbs
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.refine'_1
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
⊢ 1 < p.natAbs
Tactic:
rw [Int.prime_iff_natAbs_prime] at pprime
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.refine'_1
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : ¬Even a.norm
p : ℤ
pprime : p.natAbs.Prime
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
⊢ 1 < p.natAbs
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.refine'_1
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : ¬Even a.norm
p : ℤ
pprime : p.natAbs.Prime
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
⊢ 1 < p.natAbs
Tactic:
exact pprime.one_lt
Proof state after:
no goals
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.refine'_2
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
⊢ ¬p.sign * q = 0
Tactic:
rwa [← Int.natAbs_eq_zero, this, Int.natAbs_eq_zero]
Proof state after:
no goals
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro.refine'_3
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 * (p.sign * q) = c.norm
Tactic:
rw [← mul_right_inj' pprime'.ne_zero, ← hcd, mul_left_comm, ← hfactor, ← HA, ←
  mul_assoc (|p|), mul_comm (|p|), Int.sign_mul_abs]
Proof state after:
no goals