-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem le_arch (a : ℤ√d) : ∃ n : ℕ, a ≤ n

Proof state:
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ { re := ↑x, im := ↑y } ≤ ↑(x + d * y)

Tactic:
change Nonneg ⟨↑x + d * y - ↑x, 0 - ↑y⟩

Result:
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ { re := ↑x + ↑d * ↑y - ↑x, im := 0 - ↑y }.Nonneg

Proof state:
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ { re := ↑x + ↑d * ↑y - ↑x, im := 0 - ↑y }.Nonneg

Tactic:
rcases y with - | y

Result:
case intro.intro.zero
d : ℕ
a : ℤ√↑d
x : ℕ
h : a ≤ { re := ↑x, im := ↑0 }
⊢ { re := ↑x + ↑d * ↑0 - ↑x, im := 0 - ↑0 }.Nonneg

case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑(y + 1) }
⊢ { re := ↑x + ↑d * ↑(y + 1) - ↑x, im := 0 - ↑(y + 1) }.Nonneg

Proof state:
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ ∃ n, a ≤ ↑n

Tactic:
refine ⟨x + d * y, h.trans ?_⟩

Result:
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ { re := ↑x, im := ↑y } ≤ ↑(x + d * y)

Proof state:
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(y + 1) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ ↑x + ↑d * ↑y.succ - ↑x = ↑d * ↑y.succ

Tactic:
simp

Result:
no goals

Proof state:
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ { re := 0, im := 0 }.Nonneg

Tactic:
trivial

Result:
no goals

Proof state:
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ ({ re := ↑0, im := ↑(y + 1) } + { re := ofNat x, im := -[y+1] }).Nonneg

Tactic:
simp [add_def, Int.negSucc_coe, add_assoc]

Result:
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ { re := ↑x, im := 0 }.Nonneg

Proof state:
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ ({ re := ↑0, im := ↑0 } + { re := ofNat x, im := ofNat y }).Nonneg

Tactic:
trivial

Result:
no goals

Proof state:
case intro.intro.zero
d : ℕ
a : ℤ√↑d
x : ℕ
h : a ≤ { re := ↑x, im := ↑0 }
⊢ { re := ↑x + ↑d * ↑0 - ↑x, im := 0 - ↑0 }.Nonneg

Tactic:
simp

Result:
case intro.intro.zero
d : ℕ
a : ℤ√↑d
x : ℕ
h : a ≤ { re := ↑x, im := ↑0 }
⊢ { re := 0, im := 0 }.Nonneg

Proof state:
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ { re := ↑x, im := 0 }.Nonneg

Tactic:
trivial

Result:
no goals

Proof state:
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ ({ re := ↑(x + 1), im := ↑(y + 1) } + { re := -[x+1], im := -[y+1] }).Nonneg

Tactic:
simp [Int.negSucc_coe, add_assoc]

Result:
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ { re := 0, im := 0 }.Nonneg

Proof state:
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ { re := 0, im := ↑y }.Nonneg

Tactic:
trivial

Result:
no goals

Proof state:
case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(y + 1) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ { re := ↑x + ↑d * ↑(y + 1) - ↑x, im := 0 - ↑(y + 1) }.Nonneg

Tactic:
rw [show (x : ℤ) + d * Nat.succ y - x = d * Nat.succ y by simp]

Result:
case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(y + 1) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ { re := ↑d * ↑y.succ, im := 0 - ↑(y + 1) }.Nonneg

Proof state:
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ ({ re := ↑(x + 1), im := ↑0 } + { re := -[x+1], im := ofNat y }).Nonneg

Tactic:
simp [Int.negSucc_coe, add_assoc]

Result:
d : ℕ
a : ℤ√↑d
x y : ℕ
⊢ { re := 0, im := ↑y }.Nonneg

Proof state:
case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑(y + 1) }
⊢ { re := ↑x + ↑d * ↑(y + 1) - ↑x, im := 0 - ↑(y + 1) }.Nonneg

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

Result:
case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(y + 1) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ { re := ↑x + ↑d * ↑(y + 1) - ↑x, im := 0 - ↑(y + 1) }.Nonneg

Proof state:
case intro.intro.succ
d : ℕ
a : ℤ√↑d
x y : ℕ
h✝ : a ≤ { re := ↑x, im := ↑(y + 1) }
h : ∀ (y : ℕ), SqLe y d (d * y) 1
⊢ { re := ↑d * ↑y.succ, im := 0 - ↑(y + 1) }.Nonneg

Tactic:
exact h (y + 1)

Result:
no goals

Proof state:
d : ℕ
a : ℤ√↑d
x y✝ : ℕ
h : a ≤ { re := ↑x, im := ↑(y✝ + 1) }
y : ℕ
⊢ SqLe y d (d * y) 1

Tactic:
simpa [SqLe, mul_comm, mul_left_comm] using Nat.mul_le_mul_right (y * y) (Nat.le_mul_self d)

Result:
no goals

Proof state:
d : ℕ
a : ℤ√↑d
⊢ ∃ n, a ≤ ↑n

Tactic:
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⟩

Result:
case intro.intro
d : ℕ
a : ℤ√↑d
x y : ℕ
h : a ≤ { re := ↑x, im := ↑y }
⊢ ∃ n, a ≤ ↑n

Proof state:
case intro.intro.zero
d : ℕ
a : ℤ√↑d
x : ℕ
h : a ≤ { re := ↑x, im := ↑0 }
⊢ { re := 0, im := 0 }.Nonneg

Tactic:
trivial

Result:
no goals