-- Mathlib/NumberTheory/Pell.lean
theorem exists_of_not_isSquare (h₀ : 0 < d) (hd : ¬IsSquare d) :
    ∃ x y : ℤ, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |√↑d + ↑q| * |√↑d - ↑q| < ↑M * (1 / ↑q.den ^ 2)

Tactic:
refine mul_lt_mul'' (((abs_add ξ q).trans ?_).trans_lt hM₁) h (abs_nonneg _) (abs_nonneg _)

Result:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |ξ| + |↑q| ≤ 2 * |ξ| + 1

Proof state:
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
x : ℤ
hx : ξ = ↑x
⊢ ↑d = ↑(x * x)

Tactic:
rw [← sq_sqrt <| Int.cast_nonneg.mpr h₀.le, Int.cast_mul, ← hx, sq]

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.refine_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q => (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
hd₂ : m ∣ q₁.num * ↑q₂.den - q₂.num * ↑q₁.den
hm₀ : ↑m ≠ 0
⊢ ↑q₁.num * ↑q₂.den - ↑q₂.num * ↑q₁.den ≠ 0

Tactic:
exact mod_cast mt sub_eq_zero.mp (mt Rat.eq_iff_mul_eq_mul.mpr hne)

Result:
no goals

Proof state:
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
hm₀ : m ≠ 0
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

Tactic:
haveI := neZero_iff.mpr (Int.natAbs_ne_zero.mpr hm₀)

Result:
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
hm₀ : m ≠ 0
this : NeZero m.natAbs
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : |↑q - ξ| < 1 / ↑q.den ^ 2
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ 1 / ↑q.den ^ 2 ≤ 1

Tactic:
rw [div_le_one h0, one_le_sq_iff_one_le_abs, Nat.abs_cast, Nat.one_le_cast]

Result:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : |↑q - ξ| < 1 / ↑q.den ^ 2
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ 1 ≤ q.den

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
⊢ ∃ m, {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite

Tactic:
contrapose! hM

Result:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : ∀ (m : ℤ), ¬{q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
⊢ ¬{q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
⊢ {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite

Tactic:
refine Infinite.mono (fun q h => ?_) (infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational hξ)

Result:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
⊢ q ∈ {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
⊢ Irrational ξ

Tactic:
refine irrational_nrt_of_notint_nrt 2 d (sq_sqrt <| Int.cast_nonneg.mpr h₀.le) ?_ two_pos

Result:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
⊢ ¬∃ y, ξ = ↑y

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : |↑q - ξ| < 1 / ↑q.den ^ 2
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |↑q| - |ξ| ≤ 1

Tactic:
refine (abs_sub_abs_le_abs_sub (q : ℝ) ξ).trans (h.le.trans ?_)

Result:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : |↑q - ξ| < 1 / ↑q.den ^ 2
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ 1 / ↑q.den ^ 2 ≤ 1

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ q ∈ {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}

Tactic:
rw [mem_setOf, abs_sub_comm, ← @Int.cast_lt ℝ,
  ← div_lt_div_iff_of_pos_right (abs_pos_of_pos h0)]

Result:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ ↑|d * ↑q.den ^ 2 - q.num ^ 2| / |↑q.den ^ 2| < ↑M / |↑q.den ^ 2|

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.refine_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q => (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
hd₂ : m ∣ q₁.num * ↑q₂.den - q₂.num * ↑q₁.den
hm₀ : ↑m ≠ 0
⊢ (q₁.num * q₂.num - d * ↑(q₁.den * q₂.den)) ^ 2 - d * (q₁.num * ↑q₂.den - q₂.num * ↑q₁.den) ^ 2 =
    (q₁.num ^ 2 - d * ↑q₁.den ^ 2) * (q₂.num ^ 2 - d * ↑q₂.den ^ 2)

Tactic:
push_cast

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.refine_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q => (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
hd₂ : m ∣ q₁.num * ↑q₂.den - q₂.num * ↑q₁.den
hm₀ : ↑m ≠ 0
⊢ (q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)) ^ 2 - d * (q₁.num * ↑q₂.den - q₂.num * ↑q₁.den) ^ 2 =
    (q₁.num ^ 2 - d * ↑q₁.den ^ 2) * (q₂.num ^ 2 - d * ↑q₂.den ^ 2)