case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ ∃ n, a ≤ ↑n
d : ℕ
a : ℤ√↑d
⊢ ∃ n, a ≤ ↑n
obtain ⟨x, y, (h : a ≤ ⟨x, y⟩)⟩ : ∃ x y : ℕ, Nonneg (⟨x, y⟩ + -a) :=
  match -a with
  | ⟨Int.ofNat x, Int.ofNat y⟩ => ⟨0, 0, by trivial⟩
  | ⟨Int.ofNat x, -[y+1]⟩ => ⟨0, y + 1, by simp [add_def, Int.negSucc_coe, add_assoc]; trivial⟩
  | ⟨-[x+1], Int.ofNat y⟩ => ⟨x + 1, 0, by simp [Int.negSucc_coe, add_assoc]; trivial⟩
  | ⟨-[x+1], -[y+1]⟩ => ⟨x + 1, y + 1, by simp [Int.negSucc_coe, add_assoc]; trivial⟩
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ { re := ↑x, im := ↑y } ≤ ↑(x + d * y)
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ ∃ n, a ≤ ↑n
refine' ⟨x + d * y, h.trans _⟩
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ Nonneg { re := ↑x + ↑d * ↑y - ↑x, im := 0 - ↑y }
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ { re := ↑x, im := ↑y } ≤ ↑(x + d * y)
change Nonneg ⟨↑x + d * y - ↑x, 0 - ↑y⟩
case intro.intro.zero
d : ℕ
a : ℤ√↑d
x : ℕ
h : a ≤ { re := ↑x, im := ↑Nat.zero }
⊢ Nonneg { re := ↑x + ↑d * ↑Nat.zero - ↑x, im := 0 - ↑Nat.zero }

case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑(Nat.succ y) }
⊢ Nonneg { re := ↑x + ↑d * ↑(Nat.succ y) - ↑x, im := 0 - ↑(Nat.succ y) }
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ Nonneg { re := ↑x + ↑d * ↑y - ↑x, im := 0 - ↑y }
cases' y with y
case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(Nat.succ y) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ Nonneg { re := ↑x + ↑d * ↑(Nat.succ y) - ↑x, im := 0 - ↑(Nat.succ y) }
case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑(Nat.succ y) }
⊢ Nonneg { re := ↑x + ↑d * ↑(Nat.succ y) - ↑x, im := 0 - ↑(Nat.succ y) }
have h : ∀ y, SqLe y d (d * y) 1 := fun y => by
  simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_right (y * y) (Nat.le_mul_self d)
case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(Nat.succ y) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ Nonneg { re := ↑d * ↑(Nat.succ y), im := 0 - ↑(Nat.succ y) }
case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(Nat.succ y) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ Nonneg { re := ↑x + ↑d * ↑(Nat.succ y) - ↑x, im := 0 - ↑(Nat.succ y) }
rw [show (x : ℤ) + d * Nat.succ y - x = d * Nat.succ y by simp]
no goals
case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(Nat.succ y) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ Nonneg { re := ↑d * ↑(Nat.succ y), im := 0 - ↑(Nat.succ y) }
exact h (y + 1)
no goals
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg ({ re := ↑0, im := ↑0 } + { re := ofNat x, im := ofNat y })
trivial
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg { re := ↑x, im := 0 }
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg ({ re := ↑0, im := ↑(y + 1) } + { re := ofNat x, im := -[y+1] })
simp [add_def, Int.negSucc_coe, add_assoc]
no goals
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg { re := ↑x, im := 0 }
trivial
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg { re := 0, im := ↑y }
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg ({ re := ↑(x + 1), im := ↑0 } + { re := -[x+1], im := ofNat y })
simp [Int.negSucc_coe, add_assoc]
no goals
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg { re := 0, im := ↑y }
trivial
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg { re := 0, im := 0 }
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg ({ re := ↑(x + 1), im := ↑(y + 1) } + { re := -[x+1], im := -[y+1] })
simp [Int.negSucc_coe, add_assoc]
no goals
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ Nonneg { re := 0, im := 0 }
trivial
case intro.intro.zero
d : ℕ
a : ℤ√↑d
x : ℕ
h : a ≤ { re := ↑x, im := ↑Nat.zero }
⊢ Nonneg { re := 0, im := 0 }
case intro.intro.zero
d : ℕ
a : ℤ√↑d
x : ℕ
h : a ≤ { re := ↑x, im := ↑Nat.zero }
⊢ Nonneg { re := ↑x + ↑d * ↑Nat.zero - ↑x, im := 0 - ↑Nat.zero }
simp
no goals
case intro.intro.zero
d : ℕ
a : ℤ√↑d
x : ℕ
h : a ≤ { re := ↑x, im := ↑Nat.zero }
⊢ Nonneg { re := 0, im := 0 }
trivial
no goals
d : ℕ
a : ℤ√↑d
x y✝ : ℕ
h : a ≤ { re := ↑x, im := ↑(Nat.succ y✝) }
y : ℕ
⊢ SqLe y d (d * y) 1
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_right (y * y) (Nat.le_mul_self d)
no goals
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(Nat.succ y) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ ↑x + ↑d * ↑(Nat.succ y) - ↑x = ↑d * ↑(Nat.succ y)
simp