Theorem: factors' (Flt/Spts.lean)

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

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

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

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

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

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

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

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

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

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

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

State before:
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
Tactic:
convert hodd.pow_left
State after:
case h.e'_3
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
⊢ 4 = 2 ^ ?H1

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

State before:
case h.e'_3
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
⊢ 4 = 2 ^ ?H1

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
⊢ ℕ
Tactic:
rw [sq]
State after:
case h.e'_3
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
⊢ 4 = 2 * 2

State before:
case h.e'_3
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
⊢ 4 = 2 * 2
Tactic:
norm_num
State after:
no goals

State before:
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 ∣ f * g
Tactic:
rw [hfactor, hc]
State after:
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 ∣ 4 * Zsqrtd.norm c

State before:
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 ∣ 4 * Zsqrtd.norm c
Tactic:
exact dvd_mul_right _ _
State after:
no goals

State before:
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')
Tactic:
rw [Int.natAbs_mul]
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 * Int.natAbs g'

State before:
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 * Int.natAbs g'
Tactic:
apply lt_mul_of_one_lt_left (Int.natAbs_pos.mpr hg'pos)
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
⊢ 1 < Int.natAbs 4

State before:
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
⊢ 1 < Int.natAbs 4
Tactic:
norm_num
State after:
no goals

State before:
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
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
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
Tactic:
intro f' hf'dvd hf'odd
State after:
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' : ℤ
hf'dvd : f' ∣ g'
hf'odd : Odd f'
⊢ ∃ p, abs f' = Zsqrtd.norm p

State before:
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' : ℤ
hf'dvd : f' ∣ g'
hf'odd : Odd f'
⊢ ∃ p, abs f' = Zsqrtd.norm p
Tactic:
refine' hnotform f' _ hf'odd
State after:
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' : ℤ
hf'dvd : f' ∣ g'
hf'odd : Odd f'
⊢ f' ∣ 4 * g'

State before:
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' : ℤ
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
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:
by_cases h : |g| = 1
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)
h : abs g = 1
⊢ ∃ 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)
h : ¬abs g = 1
⊢ ∃ p, abs f = Zsqrtd.norm p

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)
h : abs g = 1
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
apply_fun abs  at hfactor
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
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : abs g = 1
hfactor : abs (f * g) = abs (Zsqrtd.norm a)
⊢ ∃ p, abs f = Zsqrtd.norm p

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
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : abs g = 1
hfactor : abs (f * g) = abs (Zsqrtd.norm a)
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
rw [abs_mul, h, mul_one, abs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)] at hfactor
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
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : abs g = 1
hfactor : abs f = Zsqrtd.norm a
⊢ ∃ p, abs f = Zsqrtd.norm p

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
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : abs g = 1
hfactor : abs f = Zsqrtd.norm a
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
exact ⟨_, hfactor⟩
State after:
no goals

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
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : abs g = 1
hfactor : abs f = abs (Zsqrtd.norm a)
⊢ -3 ≤ 0
Tactic:
norm_num
State after:
no goals

State before:
case neg
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬abs g = 1
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
rw [Int.abs_eq_natAbs, ← Int.ofNat_one, Int.coe_nat_inj'] at h
State after:
case neg
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
⊢ ∃ p, abs f = Zsqrtd.norm p

State before:
case neg
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
obtain ⟨p, pprime, pdvd⟩ := Int.exists_prime_and_dvd h
State after:
case neg.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
⊢ ∃ p, abs f = Zsqrtd.norm p

State before:
case neg.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
have : p ∣ a.norm := by
  rw [← hfactor]
  exact pdvd.mul_left _
State after:
case neg.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
⊢ ∃ p, abs f = Zsqrtd.norm p

State before:
case neg.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
have podd : Odd p :=
  Int.odd_iff_not_even.mpr
    (by
      intro X
      apply H
      apply even_iff_two_dvd.mpr
      apply dvd_trans _ this
      apply even_iff_two_dvd.mp X)
State after:
case neg.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
⊢ ∃ p, abs f = Zsqrtd.norm p

State before:
case neg.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
obtain ⟨A, HA⟩ := hnotform p pdvd podd
State after:
case neg.intro.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
⊢ ∃ p, abs f = Zsqrtd.norm p

State before:
case neg.intro.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
have pprime' := pprime.abs
State after:
case neg.intro.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (abs p)
⊢ ∃ p, abs f = Zsqrtd.norm p

State before:
case neg.intro.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (abs p)
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
rw [HA] at pprime'
State after:
case neg.intro.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
⊢ ∃ p, abs f = Zsqrtd.norm p

State before:
case neg.intro.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
have pdvd' : A.norm ∣ a.norm := by
  rw [← hfactor, ← HA, abs_dvd]
  exact dvd_mul_of_dvd_right pdvd _
State after:
case neg.intro.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
⊢ ∃ p, abs f = Zsqrtd.norm p

State before:
case neg.intro.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
obtain ⟨c, -, hcd⟩ := Spts.mul_of_dvd'' pdvd' pprime'
State after:
case neg.intro.intro.intro.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
⊢ ∃ p, abs f = Zsqrtd.norm p

State before:
case neg.intro.intro.intro.intro.intro
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
obtain ⟨q, rfl⟩ := pdvd
State after:
case neg.intro.intro.intro.intro.intro.intro
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
⊢ ∃ p, abs f = Zsqrtd.norm p

State before:
case neg.intro.intro.intro.intro.intro.intro
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
have hqpos : q ≠ 0 := right_ne_zero_of_mul hgpos
State after:
case neg.intro.intro.intro.intro.intro.intro
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
⊢ ∃ p, abs f = Zsqrtd.norm p

State before:
case neg.intro.intro.intro.intro.intro.intro
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
have : (p.sign * q).natAbs = q.natAbs := by
  rw [Int.natAbs_mul, Int.natAbs_sign_of_nonzero pprime.ne_zero, one_mul]
State after:
case neg.intro.intro.intro.intro.intro.intro
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ ∃ p, abs f = Zsqrtd.norm p

State before:
case neg.intro.intro.intro.intro.intro.intro
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ ∃ p, abs f = Zsqrtd.norm p
Tactic:
refine' IH q.natAbs _ c (p.sign * q) _ _ _ this
State after:
case neg.intro.intro.intro.intro.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)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ Int.natAbs q < Int.natAbs (p * q)

case neg.intro.intro.intro.intro.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)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ ¬Int.sign p * q = 0

case neg.intro.intro.intro.intro.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)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ f * (Int.sign p * q) = Zsqrtd.norm c

case neg.intro.intro.intro.intro.intro.intro.refine'_4
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ ∀ (f' : ℤ), f' ∣ Int.sign p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p

State before:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
⊢ p ∣ Zsqrtd.norm a
Tactic:
rw [← hfactor]
State after:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
⊢ p ∣ f * g

State before:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
⊢ p ∣ f * g
Tactic:
exact pdvd.mul_left _
State after:
no goals

State before:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
⊢ ¬Even p
Tactic:
intro X
State after:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
X : Even p
⊢ False

State before:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
X : Even p
⊢ False
Tactic:
apply H
State after:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
X : Even p
⊢ Even (Zsqrtd.norm a)

State before:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
X : Even p
⊢ Even (Zsqrtd.norm a)
Tactic:
apply even_iff_two_dvd.mpr
State after:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
X : Even p
⊢ 2 ∣ Zsqrtd.norm a

State before:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
X : Even p
⊢ 2 ∣ Zsqrtd.norm a
Tactic:
apply dvd_trans _ this
State after:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
X : Even p
⊢ 2 ∣ p

State before:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
X : Even p
⊢ 2 ∣ p
Tactic:
apply even_iff_two_dvd.mp X
State after:
no goals

State before:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
⊢ Zsqrtd.norm A ∣ Zsqrtd.norm a
Tactic:
rw [← hfactor, ← HA, abs_dvd]
State after:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
⊢ p ∣ f * g

State before:
a✝ : ℤ√(-3)
f g✝ : ℤ
hodd : Odd f
hgpos✝ : g✝ ≠ 0
hfactor✝ : f * g✝ = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g✝ → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g✝ = x✝
a : ℤ√(-3)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
H : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
⊢ p ∣ f * g
Tactic:
exact dvd_mul_of_dvd_right pdvd _
State after:
no goals

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)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
⊢ Int.natAbs (Int.sign p * q) = Int.natAbs q
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
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ Int.natAbs q < Int.natAbs (p * q)
Tactic:
rw [Int.natAbs_mul]
State after:
case neg.intro.intro.intro.intro.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)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ Int.natAbs q < Int.natAbs p * Int.natAbs q

State before:
case neg.intro.intro.intro.intro.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)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ Int.natAbs q < Int.natAbs p * Int.natAbs q
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
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ 1 < Int.natAbs p

State before:
case neg.intro.intro.intro.intro.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)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ 1 < Int.natAbs p
Tactic:
rw [Int.prime_iff_natAbs_prime] at pprime
State after:
case neg.intro.intro.intro.intro.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)
p : ℤ
pprime : Nat.Prime (Int.natAbs p)
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ 1 < Int.natAbs p

State before:
case neg.intro.intro.intro.intro.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)
p : ℤ
pprime : Nat.Prime (Int.natAbs p)
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ 1 < Int.natAbs p
Tactic:
exact pprime.one_lt
State after:
no goals

State before:
case neg.intro.intro.intro.intro.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)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ ¬Int.sign p * 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
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ f * (Int.sign p * q) = Zsqrtd.norm c
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
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ ∀ (f' : ℤ), f' ∣ Int.sign p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
Tactic:
intro f' hf'dvd hf'odd
State after:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
f' : ℤ
hf'dvd : f' ∣ Int.sign p * q
hf'odd : Odd f'
⊢ ∃ p, abs f' = Zsqrtd.norm p

State before:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
f' : ℤ
hf'dvd : f' ∣ Int.sign p * q
hf'odd : Odd f'
⊢ ∃ p, abs f' = Zsqrtd.norm p
Tactic:
refine' hnotform f' _ hf'odd
State after:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
f' : ℤ
hf'dvd : f' ∣ Int.sign p * q
hf'odd : Odd f'
⊢ f' ∣ p * q

State before:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
f' : ℤ
hf'dvd : f' ∣ Int.sign p * 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
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
f' : ℤ
hf'dvd : f' ∣ q
hf'odd : Odd f'
⊢ f' ∣ p * q

State before:
case neg.intro.intro.intro.intro.intro.intro.refine'_4
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
f' : ℤ
hf'dvd : f' ∣ q
hf'odd : Odd f'
⊢ f' ∣ p * q
Tactic:
exact hf'dvd.mul_left _
State after:
no goals