Theorem: factors (Flt/Spts.lean)

State before:
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
induction' hx' : x.natAbs using Nat.strong_induction_on with x' IH generalizing a x
State after:
case h
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx'✝ : Int.natAbs x✝¹ = x✝
x' : ℕ
IH :
  ∀ (m : ℕ),
    m < x' →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
hx' : Int.natAbs x = x'
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx'✝ : Int.natAbs x✝¹ = x✝
x' : ℕ
IH :
  ∀ (m : ℕ),
    m < x' →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
hx' : Int.natAbs x = x'
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
subst hx'
State after:
case h
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
have hneg1 : 1 ≤ a.norm := by
  rw [← Int.sub_one_lt_iff, sub_self]
  apply lt_of_le_of_ne (Zsqrtd.norm_nonneg (by norm_num) a)
  rw [Ne.def, eq_comm, Zsqrtd.norm_eq_zero_iff (by norm_num : (-3 : ℤ) < 0)]
  rintro rfl
  rw [Zsqrtd.zero_im, Zsqrtd.zero_re] at hcoprime
  exact not_isCoprime_zero_zero hcoprime
State after:
case h
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
have h0 : x ≠ 0 := by
  rintro rfl
  simp only [even_zero, not_true, Int.odd_iff_not_even] at hodd
State after:
case h
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
h0 : x ≠ 0
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
h0 : x ≠ 0
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
have h0' : 1 ≤ abs x := by rwa [← Int.sub_one_lt_iff, sub_self, abs_pos]
State after:
case h
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
h0 : x ≠ 0
h0' : 1 ≤ abs x
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
h0 : x ≠ 0
h0' : 1 ≤ abs x
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
cases' h0'.eq_or_lt with h h
State after:
case h.inl
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 = abs x
⊢ ∃ c, abs x = Zsqrtd.norm c

case h.inr
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h.inr
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
obtain ⟨c', m, rfl, -, h1, ⟨y, hy, h3⟩⟩ := Zqrtd.factor_div' a hodd h hcoprime hfactor
State after:
case h.inr.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h.inr.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
have h4 : c'.norm ≠ 0 := by rwa [Ne.def, Zsqrtd.norm_eq_zero_iff (by norm_num) c']
State after:
case h.inr.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h.inr.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
set g := Int.gcd c'.re c'.im with hg
State after:
case h.inr.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h.inr.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
have hgpos : 0 < g := by rwa [hg, Zsqrtd.gcd_pos_iff]
State after:
case h.inr.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h.inr.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
obtain ⟨C', HC', HCDcoprime⟩ := Zsqrtd.exists_coprime_of_gcd_pos hgpos
State after:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
have h5 : x * y = (g : ℤ) ^ 2 * C'.norm := by
  rw [← hy, HC', Zsqrtd.norm_mul, Zsqrtd.norm_int_cast, ← pow_two]
State after:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
have h6 : x * z = C'.norm :=
  by
  have hgnezero := Int.coe_nat_ne_zero_iff_pos.mpr hgpos
  apply Int.eq_of_mul_eq_mul_left (pow_ne_zero 2 hgnezero)
  rw [← h5, hz, mul_left_comm]
State after:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
have h8 : z ≠ 0 := by
  apply right_ne_zero_of_mul
  apply right_ne_zero_of_mul
  rwa [h6, ← h5, ← hy]
State after:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
⊢ ∃ c, abs x = Zsqrtd.norm c

State before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
refine' factors' _ x z hodd h8 h6 _
State after:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
⊢ ∀ (f' : ℤ), f' ∣ z → Odd f' → ∃ p, abs f' = Zsqrtd.norm p

State before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
⊢ ∀ (f' : ℤ), f' ∣ z → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
Tactic:
intro w hwdvd hwodd
State after:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ ∃ p, abs w = Zsqrtd.norm p

State before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ ∃ p, abs w = Zsqrtd.norm p
Tactic:
refine' IH w.natAbs _ C' w HCDcoprime hwodd _ rfl
State after:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ Int.natAbs w < Int.natAbs x

case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ w ∣ Zsqrtd.norm C'

State before:
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ 1 ≤ Zsqrtd.norm a
Tactic:
rw [← Int.sub_one_lt_iff, sub_self]
State after:
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ 0 < Zsqrtd.norm a

State before:
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ 0 < Zsqrtd.norm a
Tactic:
apply lt_of_le_of_ne (Zsqrtd.norm_nonneg (by norm_num) a)
State after:
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ 0 ≠ Zsqrtd.norm a

State before:
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ 0 ≠ Zsqrtd.norm a
Tactic:
rw [Ne.def, eq_comm, Zsqrtd.norm_eq_zero_iff (by norm_num : (-3 : ℤ) < 0)]
State after:
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ ¬a = 0

State before:
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ ¬a = 0
Tactic:
rintro rfl
State after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hcoprime : IsCoprime 0.re 0.im
hfactor : x ∣ Zsqrtd.norm 0
⊢ False

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hcoprime : IsCoprime 0.re 0.im
hfactor : x ∣ Zsqrtd.norm 0
⊢ False
Tactic:
rw [Zsqrtd.zero_im, Zsqrtd.zero_re] at hcoprime
State after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hcoprime : IsCoprime 0 0
hfactor : x ∣ Zsqrtd.norm 0
⊢ False

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hcoprime : IsCoprime 0 0
hfactor : x ∣ Zsqrtd.norm 0
⊢ False
Tactic:
exact not_isCoprime_zero_zero hcoprime
State after:
no goals

State before:
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ -3 ≤ 0
Tactic:
norm_num
State after:
no goals

State before:
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ -3 < 0
Tactic:
norm_num
State after:
no goals

State before:
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
⊢ x ≠ 0
Tactic:
rintro rfl
State after:
a✝ : ℤ√(-3)
x : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x
hfactor✝ : x ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x = x✝
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hneg1 : 1 ≤ Zsqrtd.norm a
hodd : Odd 0
hfactor : 0 ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs 0 →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ False

State before:
a✝ : ℤ√(-3)
x : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x
hfactor✝ : x ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x = x✝
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hneg1 : 1 ≤ Zsqrtd.norm a
hodd : Odd 0
hfactor : 0 ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs 0 →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
⊢ False
Tactic:
simp only [even_zero, not_true, Int.odd_iff_not_even] at hodd
State after:
no goals

State before:
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
h0 : x ≠ 0
⊢ 1 ≤ abs x
Tactic:
rwa [← Int.sub_one_lt_iff, sub_self, abs_pos]
State after:
no goals

State before:
case h.inl
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 = abs x
⊢ ∃ c, abs x = Zsqrtd.norm c
Tactic:
rw [← h]
State after:
case h.inl
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 = abs x
⊢ ∃ c, 1 = Zsqrtd.norm c

State before:
case h.inl
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 = abs x
⊢ ∃ c, 1 = Zsqrtd.norm c
Tactic:
refine' ⟨⟨1, 0⟩, _⟩
State after:
case h.inl
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 = abs x
⊢ 1 = Zsqrtd.norm { re := 1, im := 0 }

State before:
case h.inl
a✝ : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a✝.re a✝.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a✝
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hodd : Odd x
hfactor : x ∣ Zsqrtd.norm a
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
hneg1 : 1 ≤ Zsqrtd.norm a
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 = abs x
⊢ 1 = Zsqrtd.norm { re := 1, im := 0 }
Tactic:
norm_num [Zsqrtd.norm_def]
State after:
no goals

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
⊢ Zsqrtd.norm c' ≠ 0
Tactic:
rwa [Ne.def, Zsqrtd.norm_eq_zero_iff (by norm_num) c']
State after:
no goals

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
⊢ -3 < 0
Tactic:
norm_num
State after:
no goals

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
⊢ 0 < g
Tactic:
rwa [hg, Zsqrtd.gcd_pos_iff]
State after:
no goals

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
⊢ x * y = ↑g ^ 2 * Zsqrtd.norm C'
Tactic:
rw [← hy, HC', Zsqrtd.norm_mul, Zsqrtd.norm_int_cast, ← pow_two]
State after:
no goals

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
⊢ ↑g ^ 2 ∣ y
Tactic:
have : (g : ℤ) ^ 2 ∣ x * y := by
  rw [h5]
  exact dvd_mul_right _ _
State after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ ↑g ^ 2 ∣ y

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ ↑g ^ 2 ∣ y
Tactic:
apply IsCoprime.dvd_of_dvd_mul_left _ this
State after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ IsCoprime (↑g ^ 2) x

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ IsCoprime (↑g ^ 2) x
Tactic:
apply isCoprime_of_prime_dvd
State after:
case nonzero
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ ¬(↑g ^ 2 = 0 ∧ x = 0)

case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ ∀ (z : ℤ), Prime z → z ∣ ↑g ^ 2 → ¬z ∣ x

State before:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ ∀ (z : ℤ), Prime z → z ∣ ↑g ^ 2 → ¬z ∣ x
Tactic:
intro p hpprime hpdvdleft hpdvdright
State after:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
⊢ False

State before:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
⊢ False
Tactic:
have : ↑p ∣ c' + m * x := by
  rw [HC']
  exact
    dvd_add
      (dvd_mul_of_dvd_left
        ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr (hpprime.dvd_of_dvd_pow hpdvdleft)) _)
      (dvd_mul_of_dvd_right ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr hpdvdright) _)
State after:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this✝ : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
this : ↑p ∣ c' + m * ↑x
⊢ False

State before:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this✝ : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
this : ↑p ∣ c' + m * ↑x
⊢ False
Tactic:
have := Zsqrtd.coprime_of_dvd_coprime hcoprime this
State after:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this✝¹ : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
this✝ : ↑p ∣ c' + m * ↑x
this : IsCoprime (↑p).re (↑p).im
⊢ False

State before:
case H
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this✝¹ : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
this✝ : ↑p ∣ c' + m * ↑x
this : IsCoprime (↑p).re (↑p).im
⊢ False
Tactic:
simp only [Zsqrtd.coe_int_re, isCoprime_zero_right, Zsqrtd.coe_int_im, hpprime.not_unit] at this
State after:
no goals

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
⊢ ↑g ^ 2 ∣ x * y
Tactic:
rw [h5]
State after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
⊢ ↑g ^ 2 ∣ ↑g ^ 2 * Zsqrtd.norm C'

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
⊢ ↑g ^ 2 ∣ ↑g ^ 2 * Zsqrtd.norm C'
Tactic:
exact dvd_mul_right _ _
State after:
no goals

State before:
case nonzero
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
⊢ ¬(↑g ^ 2 = 0 ∧ x = 0)
Tactic:
contrapose! h0
State after:
case nonzero
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
h0 : ↑(Int.gcd c'.re c'.im) ^ 2 = 0 ∧ x = 0
⊢ x = 0

State before:
case nonzero
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
h0 : ↑(Int.gcd c'.re c'.im) ^ 2 = 0 ∧ x = 0
⊢ x = 0
Tactic:
exact h0.2
State after:
no goals

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
⊢ ↑p ∣ c' + m * ↑x
Tactic:
rw [HC']
State after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
⊢ ↑p ∣ ↑↑(Int.gcd c'.re c'.im) * C' + m * ↑x

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
this : ↑g ^ 2 ∣ x * y
p : ℤ
hpprime : Prime p
hpdvdleft : p ∣ ↑g ^ 2
hpdvdright : p ∣ x
⊢ ↑p ∣ ↑↑(Int.gcd c'.re c'.im) * C' + m * ↑x
Tactic:
exact
  dvd_add
    (dvd_mul_of_dvd_left
      ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr (hpprime.dvd_of_dvd_pow hpdvdleft)) _)
    (dvd_mul_of_dvd_right ((Zsqrtd.coe_int_dvd_coe_int _ _).mpr hpdvdright) _)
State after:
no goals

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
⊢ x * z = Zsqrtd.norm C'
Tactic:
have hgnezero := Int.coe_nat_ne_zero_iff_pos.mpr hgpos
State after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
hgnezero : ↑g ≠ 0
⊢ x * z = Zsqrtd.norm C'

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
hgnezero : ↑g ≠ 0
⊢ x * z = Zsqrtd.norm C'
Tactic:
apply Int.eq_of_mul_eq_mul_left (pow_ne_zero 2 hgnezero)
State after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
hgnezero : ↑g ≠ 0
⊢ ↑g ^ 2 * (x * z) = ↑g ^ 2 * Zsqrtd.norm C'

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
hgnezero : ↑g ≠ 0
⊢ ↑g ^ 2 * (x * z) = ↑g ^ 2 * Zsqrtd.norm C'
Tactic:
rw [← h5, hz, mul_left_comm]
State after:
no goals

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
⊢ z ≠ 0
Tactic:
apply right_ne_zero_of_mul
State after:
case a
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
⊢ ?a * z ≠ 0

case a
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
⊢ ℤ

State before:
case a
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
⊢ ?a * z ≠ 0

case a
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
⊢ ℤ
Tactic:
apply right_ne_zero_of_mul
State after:
case a.a
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
⊢ ?a.a✝ * (?a * z) ≠ 0

case a.a
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
⊢ ℤ

case a
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
⊢ ℤ

State before:
case a.a
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
⊢ ?a.a✝ * (?a * z) ≠ 0

case a.a
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
⊢ ℤ

case a
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
⊢ ℤ
Tactic:
rwa [h6, ← h5, ← hy]
State after:
no goals

State before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ Int.natAbs w < Int.natAbs x
Tactic:
calc
  w.natAbs ≤ z.natAbs :=
    Nat.le_of_dvd (Int.natAbs_pos.mpr h8) (Int.natAbs_dvd_natAbs.mpr hwdvd)
  _ ≤ y.natAbs := by
    rw [hz, Int.natAbs_mul]
    exact Nat.le_mul_of_pos_left (pow_pos hgpos 2)
  _ < x.natAbs := h3
State after:
no goals

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ Int.natAbs z ≤ Int.natAbs y
Tactic:
rw [hz, Int.natAbs_mul]
State after:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ Int.natAbs z ≤ Int.natAbs (↑g ^ 2) * Int.natAbs z

State before:
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ Int.natAbs z ≤ Int.natAbs (↑g ^ 2) * Int.natAbs z
Tactic:
exact Nat.le_mul_of_pos_left (pow_pos hgpos 2)
State after:
no goals

State before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ w ∣ Zsqrtd.norm C'
Tactic:
rw [← h6]
State after:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ w ∣ x * z

State before:
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
a : ℤ√(-3)
x✝¹ : ℤ
hcoprime✝ : IsCoprime a.re a.im
hodd✝ : Odd x✝¹
hfactor✝ : x✝¹ ∣ Zsqrtd.norm a
x✝ : ℕ
hx' : Int.natAbs x✝¹ = x✝
x : ℤ
hodd : Odd x
IH :
  ∀ (m : ℕ),
    m < Int.natAbs x →
      ∀ (a : ℤ√(-3)) (x : ℤ),
        IsCoprime a.re a.im → Odd x → x ∣ Zsqrtd.norm a → Int.natAbs x = m → ∃ c, abs x = Zsqrtd.norm c
h0 : x ≠ 0
h0' : 1 ≤ abs x
h : 1 < abs x
c' m : ℤ√(-3)
hcoprime : IsCoprime (c' + m * ↑x).re (c' + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c' + m * ↑x)
hneg1 : 1 ≤ Zsqrtd.norm (c' + m * ↑x)
h1 : c' ≠ 0
y : ℤ
hy : Zsqrtd.norm c' = x * y
h3 : Int.natAbs y < Int.natAbs x
h4 : Zsqrtd.norm c' ≠ 0
g : ℕ := Int.gcd c'.re c'.im
hg : g = Int.gcd c'.re c'.im
hgpos : 0 < g
C' : ℤ√(-3)
HC' : c' = ↑↑(Int.gcd c'.re c'.im) * C'
HCDcoprime : IsCoprime C'.re C'.im
h5 : x * y = ↑g ^ 2 * Zsqrtd.norm C'
z : ℤ
hz : y = ↑g ^ 2 * z
h6 : x * z = Zsqrtd.norm C'
h8 : z ≠ 0
w : ℤ
hwdvd : w ∣ z
hwodd : Odd w
⊢ w ∣ x * z
Tactic:
exact dvd_mul_of_dvd_right hwdvd x
State after:
no goals