internlm/Lean-Github huggingface dataset:
Theorem: factors'
Proof state before:
case pos.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
⊢ ∃ p, |f| = p.norm
Tactic:
refine' IH g'.natAbs _ c g' hg'pos _ _ rfl
Proof state after:
case pos.intro.intro.refine'_1
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
⊢ g'.natAbs < (4 * g').natAbs

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

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

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

case y
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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ ℤ
Theorem: factors'
Proof state before:
case H1
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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ IsCoprime 4 ?y
Tactic:
show IsCoprime _ f
Proof state after:
case H1
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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ IsCoprime 4 f
Theorem: factors'
Proof state before:
case H1
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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ 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
f : ℤ
hodd : IsCoprime 2 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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ IsCoprime 4 f
Theorem: factors'
Proof state before:
case H1
f : ℤ
hodd : IsCoprime 2 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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ IsCoprime 4 f
Tactic:
convert hodd.pow_left
Proof state after:
case h.e'_3
f : ℤ
hodd : IsCoprime 2 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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ 4 = 2 ^ ?H1

case H1
f : ℤ
hodd : IsCoprime 2 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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ ℕ
Theorem: factors'
Proof state before:
case h.e'_3
f : ℤ
hodd : IsCoprime 2 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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ 4 = 2 ^ ?H1

case H1
f : ℤ
hodd : IsCoprime 2 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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ ℕ
Tactic:
rw [sq]
Proof state after:
case h.e'_3
f : ℤ
hodd : IsCoprime 2 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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ 4 = 2 * 2
Theorem: factors'
Proof state before:
case h.e'_3
f : ℤ
hodd : IsCoprime 2 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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ 4 = 2 * 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: factors'
Proof state before:
case H2
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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ 4 ∣ f * g
Tactic:
rw [hfactor, hc]
Proof state after:
case H2
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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ 4 ∣ 4 * c.norm
Theorem: factors'
Proof state before:
case H2
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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ 4 ∣ 4 * c.norm
Tactic:
exact dvd_mul_right _ _
Proof state after:
no goals
Theorem: factors'
Proof state before:
case pos.intro.intro.refine'_1
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
⊢ g'.natAbs < (4 * g').natAbs
Tactic:
rw [Int.natAbs_mul]
Proof state after:
case pos.intro.intro.refine'_1
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
⊢ g'.natAbs < Int.natAbs 4 * g'.natAbs
Theorem: factors'
Proof state before:
case pos.intro.intro.refine'_1
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
⊢ g'.natAbs < Int.natAbs 4 * g'.natAbs
Tactic:
apply lt_mul_of_one_lt_left (Int.natAbs_pos.mpr hg'pos)
Proof state after:
case pos.intro.intro.refine'_1
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
⊢ 1 < Int.natAbs 4
Theorem: factors'
Proof state before:
case pos.intro.intro.refine'_1
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
⊢ 1 < Int.natAbs 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: factors'
Proof state before:
case pos.intro.intro.refine'_2
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
⊢ f * g' = c.norm
Tactic:
rw [← mul_right_inj' (four_ne_zero' ℤ), ← hc, ← hfactor, mul_left_comm]
Proof state after:
no goals
Theorem: factors'
Proof state before:
case pos.intro.intro.refine'_3
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
⊢ ∀ (f' : ℤ), f' ∣ g' → Odd f' → ∃ p, |f'| = p.norm
Tactic:
intro f' hf'dvd hf'odd
Proof state after:
case pos.intro.intro.refine'_3
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
f' : ℤ
hf'dvd : f' ∣ g'
hf'odd : Odd f'
⊢ ∃ p, |f'| = p.norm
Theorem: factors'
Proof state before:
case pos.intro.intro.refine'_3
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
f' : ℤ
hf'dvd : f' ∣ g'
hf'odd : Odd f'
⊢ ∃ p, |f'| = p.norm
Tactic:
refine' hnotform f' _ hf'odd
Proof state after:
case pos.intro.intro.refine'_3
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
f' : ℤ
hf'dvd : f' ∣ g'
hf'odd : Odd f'
⊢ f' ∣ 4 * g'
Theorem: factors'
Proof state before:
case pos.intro.intro.refine'_3
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : Even a.norm
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
g' : ℤ
hgpos : 4 * g' ≠ 0
hfactor : f * (4 * g') = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ 4 * g' → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (4 * 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
hg'pos : g' ≠ 0
f' : ℤ
hf'dvd : f' ∣ g'
hf'odd : Odd f'
⊢ f' ∣ 4 * g'
Tactic:
exact hf'dvd.mul_left _
Proof state after:
no goals
Theorem: factors'
Proof state before:
case neg
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
⊢ ∃ p, |f| = p.norm
Tactic:
by_cases h : |g| = 1
Proof state after:
case pos
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| = 1
⊢ ∃ p, |f| = p.norm

case neg
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| = 1
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case pos
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| = 1
⊢ ∃ p, |f| = p.norm
Tactic:
apply_fun abs  at hfactor
Proof state after:
case pos
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
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| = 1
hfactor : |f * g| = |a.norm|
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case pos
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
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| = 1
hfactor : |f * g| = |a.norm|
⊢ ∃ p, |f| = p.norm
Tactic:
rw [abs_mul, h, mul_one, abs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)] at hfactor
Proof state after:
case pos
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
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| = 1
hfactor : |f| = a.norm
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case pos
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
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| = 1
hfactor : |f| = a.norm
⊢ ∃ p, |f| = p.norm
Tactic:
exact ⟨_, hfactor⟩
Proof state after:
no goals
Theorem: factors'
Proof state before:
f : ℤ
hodd : Odd f
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
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| = 1
hfactor : |f| = |a.norm|
⊢ -3 ≤ 0
Tactic:
norm_num
Proof state after:
no goals
Theorem: factors'
Proof state before:
case neg
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| = 1
⊢ ∃ p, |f| = p.norm
Tactic:
rw [Int.abs_eq_natAbs, ← Int.ofNat_one, Int.natCast_inj] at h
Proof state after:
case neg
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, |f| = p.norm
Theorem: factors'
Proof state before:
case neg
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, |f| = p.norm
Tactic:
obtain ⟨p, pprime, pdvd⟩ := Int.exists_prime_and_dvd h
Proof state after:
case neg.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
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case neg.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
⊢ ∃ p, |f| = p.norm
Tactic:
have : p ∣ a.norm := by
  rw [← hfactor]
  exact pdvd.mul_left _
Proof state after:
case neg.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
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case neg.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
⊢ ∃ p, |f| = p.norm
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
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
⊢ ∃ p, |f| = p.norm
Theorem: factors'
Proof state before:
case neg.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
⊢ ∃ p, |f| = p.norm
Tactic:
obtain ⟨A, HA⟩ := hnotform p pdvd podd
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
⊢ ∃ p, |f| = p.norm