Theorem: factors' (FltRegular/FltThree/Spts.lean)

State before:
a : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
⊢ ∃ p, |f| = p.norm
Tactic:
induction' hg : g.natAbs using Nat.strong_induction_on with g'' IH generalizing a g
State after:
case h
f : ℤ
hodd : Odd f
g'' : ℕ
IH :
  ∀ m < g'',
    ∀ (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
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
hg : g.natAbs = g''
⊢ ∃ p, |f| = p.norm

State before:
case h
f : ℤ
hodd : Odd f
g'' : ℕ
IH :
  ∀ m < g'',
    ∀ (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
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm
hg : g.natAbs = g''
⊢ ∃ p, |f| = p.norm
Tactic:
subst g''
State after:
case h
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
⊢ ∃ p, |f| = p.norm

State before:
case h
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
⊢ ∃ p, |f| = p.norm
Tactic:
dsimp at IH
State after:
case h
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
⊢ ∃ p, |f| = p.norm

State before:
case h
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
⊢ ∃ p, |f| = p.norm
Tactic:
by_cases H : Even (Zsqrtd.norm a)
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
⊢ ∃ 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
⊢ ∃ p, |f| = p.norm

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
⊢ ∃ p, |f| = p.norm
Tactic:
obtain ⟨c, hc⟩ := factors2 H
State after:
case pos.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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
⊢ ∃ p, |f| = p.norm

State before:
case pos.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
c : ℤ√(-3)
hc : a.norm = 4 * c.norm
this : 4 ∣ g
⊢ ∃ p, |f| = p.norm
Tactic:
obtain ⟨g', rfl⟩ := this
State after:
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
⊢ ∃ p, |f| = p.norm

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
⊢ ∃ p, |f| = p.norm
Tactic:
have hg'pos : g' ≠ 0 := right_ne_zero_of_mul hgpos
State after:
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

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
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

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
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
⊢ ℤ

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
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

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
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

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
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
⊢ ℕ

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]
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

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
State after:
no goals

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]
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

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 _ _
State after:
no goals

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]
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

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)
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

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
State after:
no goals

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]
State after:
no goals

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
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

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
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'

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 _
State after:
no goals

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
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

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
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

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
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

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⟩
State after:
no goals

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
State after:
no goals

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
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

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
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

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 _
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

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)
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

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
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

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
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

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'
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

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 _
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

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'
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

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
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

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
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

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]
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

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
this : (p.sign * q).natAbs = q.natAbs
⊢ ∃ p, |f| = p.norm
Tactic:
refine' IH q.natAbs _ c (p.sign * q) _ _ _ this
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 * q).natAbs

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

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

case neg.intro.intro.intro.intro.intro.intro.refine'_4
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' : ℤ), f' ∣ p.sign * q → Odd f' → ∃ p, |f'| = p.norm

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]
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

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 _
State after:
no goals

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
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

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
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

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
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

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
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

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
State after:
no goals

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]
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

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 _
State after:
no goals

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]
State after:
no goals

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]
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

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)
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

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
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

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals

State before:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
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' : ℤ), f' ∣ p.sign * q → Odd f' → ∃ p, |f'| = p.norm
Tactic:
intro f' hf'dvd hf'odd
State after:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
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' : ℤ
hf'dvd : f' ∣ p.sign * q
hf'odd : Odd f'
⊢ ∃ p, |f'| = p.norm

State before:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
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' : ℤ
hf'dvd : f' ∣ p.sign * q
hf'odd : Odd f'
⊢ ∃ p, |f'| = p.norm
Tactic:
refine' hnotform f' _ hf'odd
State after:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
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' : ℤ
hf'dvd : f' ∣ p.sign * q
hf'odd : Odd f'
⊢ f' ∣ p * q

State before:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
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' : ℤ
hf'dvd : f' ∣ p.sign * q
hf'odd : Odd f'
⊢ f' ∣ p * q
Tactic:
rw [← Int.dvd_natAbs, this, Int.dvd_natAbs] at hf'dvd
State after:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
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' : ℤ
hf'dvd : f' ∣ q
hf'odd : Odd f'
⊢ f' ∣ p * q

State before:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
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' : ℤ
hf'dvd : f' ∣ q
hf'odd : Odd f'
⊢ f' ∣ p * q
Tactic:
exact hf'dvd.mul_left _
State after:
no goals