internlm/Lean-Github huggingface dataset:
Theorem: Spts.mul_of_dvd'
Proof state before:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
this : a = { re := p.re, im := -↑A * p.im } * U
⊢ a = p * U ∨ a = star p * U
Tactic:
apply Or.imp _ _ (Int.units_eq_one_or A).symm <;> rintro rfl <;> simpa [Zsqrtd.ext] using this
Proof state after:
no goals
Theorem: Spts.mul_of_dvd'
Proof state before:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
⊢ Zsqrtd.norm p = p.re ^ 2 + 3 * ↑A ^ 2 * p.im ^ 2
Tactic:
rw [Zsqrtd.norm_def, HAsq]
Proof state after:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
⊢ p.re * p.re - -3 * p.im * p.im = p.re ^ 2 + 3 * 1 * p.im ^ 2
Theorem: Spts.mul_of_dvd'
Proof state before:
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
X : ℤ√(-3) := { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
HX : X = { re := p.re * a.re - ↑A * 3 * p.im * a.im, im := p.re * a.im + ↑A * a.re * p.im }
U : ℤ√(-3)
HU : X = ↑(Zsqrtd.norm p) * U
⊢ p.re * p.re - -3 * p.im * p.im = p.re ^ 2 + 3 * 1 * p.im ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: Spts.mul_of_dvd''
Proof state before:
a p : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hpprime : Prime (Zsqrtd.norm p)
⊢ ∃ u, (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u
Tactic:
obtain ⟨u, hu⟩ := Spts.mul_of_dvd' hdvd hpprime
Proof state after:
case intro
a p : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hpprime : Prime (Zsqrtd.norm p)
u : ℤ√(-3)
hu : a = p * u ∨ a = star p * u
⊢ ∃ u, (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u
Theorem: Spts.mul_of_dvd''
Proof state before:
case intro
a p : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hpprime : Prime (Zsqrtd.norm p)
u : ℤ√(-3)
hu : a = p * u ∨ a = star p * u
⊢ ∃ u, (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u
Tactic:
refine' ⟨u, hu, _⟩
Proof state after:
case intro
a p : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hpprime : Prime (Zsqrtd.norm p)
u : ℤ√(-3)
hu : a = p * u ∨ a = star p * u
⊢ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u
Theorem: Spts.mul_of_dvd''
Proof state before:
case intro
a p : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a
hpprime : Prime (Zsqrtd.norm p)
u : ℤ√(-3)
hu : a = p * u ∨ a = star p * u
⊢ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u
Tactic:
obtain rfl | rfl := hu
Proof state after:
case intro.inl
p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
u : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm (p * u)
⊢ Zsqrtd.norm (p * u) = Zsqrtd.norm p * Zsqrtd.norm u

case intro.inr
p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
u : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm (star p * u)
⊢ Zsqrtd.norm (star p * u) = Zsqrtd.norm p * Zsqrtd.norm u
Theorem: Spts.mul_of_dvd''
Proof state before:
case intro.inl
p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
u : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm (p * u)
⊢ Zsqrtd.norm (p * u) = Zsqrtd.norm p * Zsqrtd.norm u
Tactic:
rw [Zsqrtd.norm_mul]
Proof state after:
no goals
Theorem: Spts.mul_of_dvd''
Proof state before:
case intro.inr
p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
u : ℤ√(-3)
hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm (star p * u)
⊢ Zsqrtd.norm (star p * u) = Zsqrtd.norm p * Zsqrtd.norm u
Tactic:
rw [Zsqrtd.norm_mul, Zsqrtd.norm_conj]
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
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
induction' hg : g.natAbs using Nat.strong_induction_on with g'' IH generalizing a g
Proof state after:
case h
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✝
g'' : ℕ
IH :
  ∀ (m : ℕ),
    m < 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
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
hg : Int.natAbs g = g''
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case h
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✝
g'' : ℕ
IH :
  ∀ (m : ℕ),
    m < 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
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
hg : Int.natAbs g = g''
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
subst g''
Proof state after:
case h
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
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case h
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
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
dsimp at IH
Proof state after:
case h
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
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case h
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
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
by_cases H : Even (Zsqrtd.norm a)
Proof state after:
case pos
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)
⊢ ∃ p, abs f = Zsqrtd.norm p

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)
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case pos
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)
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
obtain ⟨c, hc⟩ := factors2 H
Proof state after:
case pos.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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case pos.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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
this : 4 ∣ g
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
obtain ⟨g', rfl⟩ := this
Proof state after:
case pos.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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (4 * 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
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case pos.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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (4 * 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
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
have hg'pos : g' ≠ 0 := right_ne_zero_of_mul hgpos
Proof state after:
case pos.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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (4 * 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
hg'pos : g' ≠ 0
⊢ ∃ p, abs f = Zsqrtd.norm p
Theorem: factors'
Proof state before:
case pos.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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (4 * 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
hg'pos : g' ≠ 0
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
refine' IH g'.natAbs _ c g' hg'pos _ _ rfl
Proof state after:
case pos.intro.intro.refine'_1
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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (4 * 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
hg'pos : g' ≠ 0
⊢ Int.natAbs g' < Int.natAbs (4 * g')

case pos.intro.intro.refine'_2
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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (4 * 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
hg'pos : g' ≠ 0
⊢ f * g' = Zsqrtd.norm c

case pos.intro.intro.refine'_3
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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (4 * 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
hg'pos : g' ≠ 0
⊢ ∀ (f' : ℤ), f' ∣ g' → Odd f' → ∃ 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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
⊢ 4 ∣ g
Tactic:
apply IsCoprime.dvd_of_dvd_mul_left
Proof state after:
case H1
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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
⊢ IsCoprime 4 ?y

case H2
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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
⊢ 4 ∣ ?y * g

case y
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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
⊢ ℤ
Theorem: factors'
Proof state before:
case H1
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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
⊢ IsCoprime 4 ?y
Tactic:
show IsCoprime _ f
Proof state after:
case H1
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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
⊢ IsCoprime 4 f
Theorem: factors'
Proof state before:
case H1
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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
⊢ IsCoprime 4 f
Tactic:
rw [Int.odd_iff_not_even, even_iff_two_dvd, ← Int.prime_two.coprime_iff_not_dvd] at hodd
Proof state after:
case H1
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : IsCoprime 2 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)
c : ℤ√(-3)
hc : Zsqrtd.norm a = 4 * Zsqrtd.norm c
⊢ IsCoprime 4 f