-- Mathlib/NumberTheory/Pell.lean
theorem exists_of_not_isSquare (h₀ : 0 < d) (hd : ¬IsSquare d) :
    ∃ a : Solution₁ d, IsFundamental a

Proof state:
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
⊢ ∃ a, IsFundamental a

Tactic:
obtain ⟨hx, y₁, hy₀, hy₁⟩ := Nat.find_spec P

Result:
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
⊢ ∃ a, IsFundamental a

Proof state:
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₂ : 0 < a.y
ax : ℕ
ha₁✝ : 1 < ↑ax
hax✝ hax : ↑ax ^ 2 - d * a.y ^ 2 = 1
ha₁ : 1 < ax
⊢ ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1

Tactic:
exact ⟨ax, ha₁, a.y, ha₂, hax⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < b.x
⊢ ↑x₁ ≤ b.x

Tactic:
have hb' := (Int.toNat_of_nonneg <| zero_le_one.trans hb.le).symm

Result:
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < b.x
hb' : b.x = ↑b.x.toNat
⊢ ↑x₁ ≤ b.x

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
hax : a.x ^ 2 - d * a.y ^ 2 = 1
⊢ ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1

Tactic:
lift a.x to ℕ using by positivity with ax

Result:
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₂ : 0 < a.y
ax : ℕ
ha₁✝ ha₁ : 1 < ↑ax
hax✝ hax : ↑ax ^ 2 - d * a.y ^ 2 = 1
⊢ ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1

Proof state:
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
hb : 1 < b.x.toNat
⊢ x₁ ≤ b.x.toNat

Tactic:
refine Nat.find_min' P ⟨hb, |b.y|, abs_pos.mpr <| y_ne_zero_of_one_lt_x hb'', ?_⟩

Result:
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
hb : 1 < b.x.toNat
⊢ ↑b.x.toNat ^ 2 - d * |b.y| ^ 2 = 1

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
⊢ ∃ a, IsFundamental a

Tactic:
obtain ⟨a, ha₁, ha₂⟩ := exists_pos_of_not_isSquare h₀ hd

Result:
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
⊢ ∃ a, IsFundamental a

Proof state:
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
hb : 1 < b.x.toNat
⊢ ↑b.x.toNat ^ 2 - d * |b.y| ^ 2 = 1

Tactic:
rw [← hb', sq_abs]

Result:
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
hb : 1 < b.x.toNat
⊢ b.x ^ 2 - d * b.y ^ 2 = 1

Proof state:
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < b.x
⊢ (Solution₁.mk (↑x₁) y₁ hy₁).x ≤ b.x

Tactic:
rw [x_mk]

Result:
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < b.x
⊢ ↑x₁ ≤ b.x

Proof state:
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₂ : 0 < a.y
ax : ℕ
ha₁✝ ha₁ : 1 < ↑ax
hax✝ hax : ↑ax ^ 2 - d * a.y ^ 2 = 1
⊢ ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1

Tactic:
norm_cast at ha₁

Result:
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₂ : 0 < a.y
ax : ℕ
ha₁✝ : 1 < ↑ax
hax✝ hax : ↑ax ^ 2 - d * a.y ^ 2 = 1
ha₁ : 1 < ax
⊢ ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1

Proof state:
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < b.x
hb' : b.x = ↑b.x.toNat
⊢ ↑x₁ ≤ b.x

Tactic:
have hb'' := hb

Result:
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < b.x
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
⊢ ↑x₁ ≤ b.x

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
⊢ ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1

Tactic:
have hax := a.prop

Result:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
hax : a.x ^ 2 - d * a.y ^ 2 = 1
⊢ ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
⊢ 1 < ↑x₁

Tactic:
exact mod_cast hx

Result:
no goals

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
⊢ 1 < (Solution₁.mk (↑x₁) y₁ hy₁).x

Tactic:
rw [x_mk]

Result:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
⊢ 1 < ↑x₁

Proof state:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
hax : a.x ^ 2 - d * a.y ^ 2 = 1
⊢ 0 ≤ a.x

Tactic:
positivity

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
hb : 1 < b.x.toNat
⊢ b.x ^ 2 - d * b.y ^ 2 = 1

Tactic:
exact b.prop

Result:
no goals