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