internlm/Lean-Github huggingface dataset:
Theorem: factors'
Proof state before:
case neg
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
obtain ⟨p, pprime, pdvd⟩ := Int.exists_prime_and_dvd h
Proof state after:
case neg.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case neg.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
have : p ∣ a.norm := by
  rw [← hfactor]
  exact pdvd.mul_left _
Proof state after:
case neg.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case neg.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
have podd : Odd p :=
  Int.odd_iff_not_even.mpr
    (by
      intro X
      apply H
      apply even_iff_two_dvd.mpr
      apply dvd_trans _ this
      apply even_iff_two_dvd.mp X)
Proof state after:
case neg.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case neg.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
obtain ⟨A, HA⟩ := hnotform p pdvd podd
Proof state after:
case neg.intro.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case neg.intro.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
have pprime' := pprime.abs
Proof state after:
case neg.intro.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (abs p)
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case neg.intro.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (abs p)
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
rw [HA] at pprime'
Proof state after:
case neg.intro.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case neg.intro.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
⊢ ∃ p, abs f = Zsqrtd.norm p
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
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
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
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case neg.intro.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
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
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
obtain ⟨c, -, hcd⟩ := Spts.mul_of_dvd'' pdvd' pprime'
Proof state after:
case neg.intro.intro.intro.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
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
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
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
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
obtain ⟨q, rfl⟩ := pdvd
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
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
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
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
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
have hqpos : q ≠ 0 := right_ne_zero_of_mul hgpos
Proof state after:
case neg.intro.intro.intro.intro.intro.intro
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
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
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
⊢ ∃ p, abs f = Zsqrtd.norm p
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
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
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
⊢ p ∣ Zsqrtd.norm a
Tactic:
rw [← hfactor]
Proof state after:
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
⊢ p ∣ f * g
Theorem: factors'
Proof state before:
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 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:
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
⊢ ¬Even p
Tactic:
intro X
Proof state after:
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
X : Even p
⊢ False