-- Module: Mathlib.NumberTheory.Pell
Goal:
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' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑x' : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1
to to₁ to₂ : ∃ (a : Solution₁ d), IsFundamental a
to₃ :
  ∀
    (hx :
      1 <
        Nat.find (p := fun (n : ℕ) ↦
          1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P)
    (y₁ : ℤ) (hy₀ : 0 < y₁)
    (hy₁ :
      HPow.hPow (α := ℤ) (β := ℕ)
            (↑(Nat.find (p := fun (n : ℕ) ↦
                  1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
                  P) :
              ℤ)
            2 -
          d * HPow.hPow (β := ℕ) y₁ 2 =
        1),
    ∃ (a : Solution₁ d), IsFundamental a
to₄ :
  let x₁ :=
    Nat.find (p := fun (n : ℕ) ↦
      1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P;
  ∀
    (hx :
      1 <
        Nat.find (p := fun (n : ℕ) ↦
          1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P)
    (y₁ : ℤ) (hy₀ : 0 < y₁)
    (hy₁ :
      HPow.hPow (α := ℤ) (β := ℕ)
            (↑(Nat.find (p := fun (n : ℕ) ↦
                  1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
                  P) :
              ℤ)
            2 -
          d * HPow.hPow (β := ℕ) y₁ 2 =
        1)
    {b : Solution₁ d} (hb : 1 < b.x), (Solution₁.mk (↑x₁ : ℤ) y₁ hy₁).x ≤ b.x
to₅ :
  let x₁ :=
    Nat.find (p := fun (n : ℕ) ↦
      1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P;
  ∀
    (hx :
      1 <
        Nat.find (p := fun (n : ℕ) ↦
          1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P)
    (y₁ : ℤ) (hy₀ : 0 < y₁)
    (hy₁ :
      HPow.hPow (α := ℤ) (β := ℕ)
            (↑(Nat.find (p := fun (n : ℕ) ↦
                  1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
                  P) :
              ℤ)
            2 -
          d * HPow.hPow (β := ℕ) y₁ 2 =
        1)
    {b : Solution₁ d} (hb : 1 < b.x), (↑x₁ : ℤ) ≤ b.x
to₆ :
  let x₁ :=
    Nat.find (p := fun (n : ℕ) ↦
      1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P;
  ∀
    (hx :
      1 <
        Nat.find (p := fun (n : ℕ) ↦
          1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P)
    (y₁ : ℤ) (hy₀ : 0 < y₁)
    (hy₁ :
      HPow.hPow (α := ℤ) (β := ℕ)
            (↑(Nat.find (p := fun (n : ℕ) ↦
                  1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
                  P) :
              ℤ)
            2 -
          d * HPow.hPow (β := ℕ) y₁ 2 =
        1)
    {b : Solution₁ d} (hb : 1 < b.x) (hb' : b.x = (↑b.x.toNat : ℤ)), (↑x₁ : ℤ) ≤ b.x
to₇ :
  let x₁ :=
    Nat.find (p := fun (n : ℕ) ↦
      1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P;
  ∀
    (hx :
      1 <
        Nat.find (p := fun (n : ℕ) ↦
          1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P)
    (y₁ : ℤ) (hy₀ : 0 < y₁)
    (hy₁ :
      HPow.hPow (α := ℤ) (β := ℕ)
            (↑(Nat.find (p := fun (n : ℕ) ↦
                  1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
                  P) :
              ℤ)
            2 -
          d * HPow.hPow (β := ℕ) y₁ 2 =
        1)
    {b : Solution₁ d} (hb : 1 < b.x) (hb' : b.x = (↑b.x.toNat : ℤ)) (hb'' : 1 < b.x), (↑x₁ : ℤ) ≤ b.x
to₈ :
  let x₁ :=
    Nat.find (p := fun (n : ℕ) ↦
      1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P;
  ∀
    (hx :
      1 <
        Nat.find (p := fun (n : ℕ) ↦
          1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P)
    (y₁ : ℤ) (hy₀ : 0 < y₁)
    (hy₁ :
      HPow.hPow (α := ℤ) (β := ℕ)
            (↑(Nat.find (p := fun (n : ℕ) ↦
                  1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
                  P) :
              ℤ)
            2 -
          d * HPow.hPow (β := ℕ) y₁ 2 =
        1)
    {b : Solution₁ d} (hb : LT.lt (α := ℤ) 1 (↑b.x.toNat : ℤ)) (hb' : b.x = (↑b.x.toNat : ℤ)) (hb'' : 1 < b.x),
    LE.le (α := ℤ) (↑x₁ : ℤ) (↑b.x.toNat : ℤ)
to₉ :
  let x₁ :=
    Nat.find (p := fun (n : ℕ) ↦
      1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P;
  ∀
    (hx :
      1 <
        Nat.find (p := fun (n : ℕ) ↦
          1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P)
    (y₁ : ℤ) (hy₀ : 0 < y₁)
    (hy₁ :
      HPow.hPow (α := ℤ) (β := ℕ)
            (↑(Nat.find (p := fun (n : ℕ) ↦
                  1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
                  P) :
              ℤ)
            2 -
          d * HPow.hPow (β := ℕ) 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
to₁₀ :
  ∀
    (hx :
      1 <
        Nat.find (p := fun (n : ℕ) ↦
          1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P)
    (y₁ : ℤ) (hy₀ : 0 < y₁)
    (hy₁ :
      HPow.hPow (α := ℤ) (β := ℕ)
            (↑(Nat.find (p := fun (n : ℕ) ↦
                  1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
                  P) :
              ℤ)
            2 -
          d * HPow.hPow (β := ℕ) y₁ 2 =
        1)
    {b : Solution₁ d} (hb' : b.x = (↑b.x.toNat : ℤ)) (hb'' : 1 < b.x) (hb : 1 < b.x.toNat),
    HPow.hPow (α := ℤ) (β := ℕ) (↑b.x.toNat : ℤ) 2 - d * HPow.hPow (β := ℕ) |b.y| 2 = 1
to₁₁ :
  ∀
    (hx :
      1 <
        Nat.find (p := fun (n : ℕ) ↦
          1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P)
    (y₁ : ℤ) (hy₀ : 0 < y₁)
    (hy₁ :
      HPow.hPow (α := ℤ) (β := ℕ)
            (↑(Nat.find (p := fun (n : ℕ) ↦
                  1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
                  P) :
              ℤ)
            2 -
          d * HPow.hPow (β := ℕ) y₁ 2 =
        1)
    {b : Solution₁ d} (hb' : b.x = (↑b.x.toNat : ℤ)) (hb'' : 1 < b.x) (hb : 1 < b.x.toNat),
    HPow.hPow (β := ℕ) b.x 2 - d * HPow.hPow (β := ℕ) b.y 2 = 1
⊢ ∃ (a : Solution₁ d), IsFundamental a

Tactic:
classical
  -- to avoid having to show that the predicate is decidable
  let x₁ := Nat.find P
  obtain ⟨hx, y₁, hy₀, hy₁⟩ := Nat.find_spec P
  refine ⟨mk x₁ y₁ hy₁, by rw [x_mk]; exact mod_cast hx, hy₀, fun {b} hb => ?_⟩
  rw [x_mk]
  have hb' := (Int.toNat_of_nonneg <| zero_le_one.trans hb.le).symm
  have hb'' := hb
  rw [hb'] at hb ⊢
  norm_cast at hb ⊢
  refine Nat.find_min' P ⟨hb, |b.y|, abs_pos.mpr <| y_ne_zero_of_one_lt_x hb'', ?_⟩
  rw [← hb', sq_abs]
  exact b.prop

Premises used: sq_abs, Pell.Solution₁.x_mk