Theorem: factors'
Proof state before:
case neg.intro.intro.intro.intro.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : ¬Even a.norm
p : ℤ
pprime : Prime p
this✝ : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
pdvd' : A.norm ∣ a.norm
c : ℤ√(-3)
hcd : a.norm = A.norm * c.norm
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (p * q).natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
h : ¬(p * q).natAbs = 1
hqpos : q ≠ 0
this : (p.sign * q).natAbs = q.natAbs
⊢ ∃ p, |f| = p.norm
Tactic:
refine' IH q.natAbs _ c (p.sign * q) _ _ _ this
Proof state after:
case neg.intro.intro.intro.intro.intro.intro.refine'_1
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : ¬Even a.norm
p : ℤ
pprime : Prime p
this✝ : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
pdvd' : A.norm ∣ a.norm
c : ℤ√(-3)
hcd : a.norm = A.norm * c.norm
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (p * q).natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
h : ¬(p * q).natAbs = 1
hqpos : q ≠ 0
this : (p.sign * q).natAbs = q.natAbs
⊢ q.natAbs < (p * q).natAbs

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

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

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