[GOAL]
d : ℤ
a : ℤ√d
⊢ a.re ^ 2 - d * a.im ^ 2 = 1 ↔ a ∈ unitary (ℤ√d)
[PROOFSTEP]
rw [← norm_eq_one_iff_mem_unitary, norm_def, sq, sq, ← mul_assoc]
[GOAL]
d : ℤ
a : Solution₁ d
⊢ Solution₁.x a ^ 2 = 1 + d * Solution₁.y a ^ 2
[PROOFSTEP]
rw [← a.prop]
[GOAL]
d : ℤ
a : Solution₁ d
⊢ Solution₁.x a ^ 2 = Solution₁.x a ^ 2 - d * Solution₁.y a ^ 2 + d * Solution₁.y a ^ 2
[PROOFSTEP]
ring
[GOAL]
d : ℤ
a : Solution₁ d
⊢ d * Solution₁.y a ^ 2 = Solution₁.x a ^ 2 - 1
[PROOFSTEP]
rw [← a.prop]
[GOAL]
d : ℤ
a : Solution₁ d
⊢ d * Solution₁.y a ^ 2 = Solution₁.x a ^ 2 - (Solution₁.x a ^ 2 - d * Solution₁.y a ^ 2)
[PROOFSTEP]
ring
[GOAL]
d : ℤ
a b : Solution₁ d
⊢ Solution₁.x (a * b) = Solution₁.x a * Solution₁.x b + d * (Solution₁.y a * Solution₁.y b)
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
d : ℤ
a b : Solution₁ d
⊢ Solution₁.x (a * b) = Solution₁.x a * Solution₁.x b + d * Solution₁.y a * Solution₁.y b
[PROOFSTEP]
rfl
[GOAL]
d : ℤ
h₀ : d < 0
a : Solution₁ d
⊢ Solution₁.x a = 0 ∨ Solution₁.y a = 0
[PROOFSTEP]
have h := a.prop
[GOAL]
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : Solution₁.x a ^ 2 - d * Solution₁.y a ^ 2 = 1
⊢ Solution₁.x a = 0 ∨ Solution₁.y a = 0
[PROOFSTEP]
contrapose! h
[GOAL]
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : Solution₁.x a ≠ 0 ∧ Solution₁.y a ≠ 0
⊢ Solution₁.x a ^ 2 - d * Solution₁.y a ^ 2 ≠ 1
[PROOFSTEP]
have h1 := sq_pos_of_ne_zero a.x h.1
[GOAL]
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : Solution₁.x a ≠ 0 ∧ Solution₁.y a ≠ 0
h1 : 0 < Solution₁.x a ^ 2
⊢ Solution₁.x a ^ 2 - d * Solution₁.y a ^ 2 ≠ 1
[PROOFSTEP]
have h2 :=
  sq_pos_of_ne_zero a.y
    h.2
      -- Porting note: added this to help `nlinarith`
[GOAL]
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : Solution₁.x a ≠ 0 ∧ Solution₁.y a ≠ 0
h1 : 0 < Solution₁.x a ^ 2
h2 : 0 < Solution₁.y a ^ 2
⊢ Solution₁.x a ^ 2 - d * Solution₁.y a ^ 2 ≠ 1
[PROOFSTEP]
obtain ⟨d', rfl⟩ : ∃ d', d = -d' := ⟨-d, by exact Iff.mp neg_eq_iff_eq_neg rfl⟩
[GOAL]
d : ℤ
h₀ : d < 0
a : Solution₁ d
h : Solution₁.x a ≠ 0 ∧ Solution₁.y a ≠ 0
h1 : 0 < Solution₁.x a ^ 2
h2 : 0 < Solution₁.y a ^ 2
⊢ d = - -d
[PROOFSTEP]
exact Iff.mp neg_eq_iff_eq_neg rfl
[GOAL]
case intro
d' : ℤ
h₀ : -d' < 0
a : Solution₁ (-d')
h : Solution₁.x a ≠ 0 ∧ Solution₁.y a ≠ 0
h1 : 0 < Solution₁.x a ^ 2
h2 : 0 < Solution₁.y a ^ 2
⊢ Solution₁.x a ^ 2 - -d' * Solution₁.y a ^ 2 ≠ 1
[PROOFSTEP]
nlinarith
[GOAL]
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
⊢ Solution₁.x a ≠ 0
[PROOFSTEP]
intro hx
[GOAL]
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : Solution₁.x a = 0
⊢ False
[PROOFSTEP]
have h : 0 ≤ d * a.y ^ 2 := mul_nonneg h₀ (sq_nonneg _)
[GOAL]
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : Solution₁.x a = 0
h : 0 ≤ d * Solution₁.y a ^ 2
⊢ False
[PROOFSTEP]
rw [a.prop_y, hx, sq, zero_mul, zero_sub] at h
[GOAL]
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : Solution₁.x a = 0
h : 0 ≤ -1
⊢ False
[PROOFSTEP]
exact not_le.mpr (neg_one_lt_zero : (-1 : ℤ) < 0) h
[GOAL]
d : ℤ
a : Solution₁ d
ha : 1 < Solution₁.x a
⊢ Solution₁.y a ≠ 0
[PROOFSTEP]
intro hy
[GOAL]
d : ℤ
a : Solution₁ d
ha : 1 < Solution₁.x a
hy : Solution₁.y a = 0
⊢ False
[PROOFSTEP]
have prop := a.prop
[GOAL]
d : ℤ
a : Solution₁ d
ha : 1 < Solution₁.x a
hy : Solution₁.y a = 0
prop : Solution₁.x a ^ 2 - d * Solution₁.y a ^ 2 = 1
⊢ False
[PROOFSTEP]
rw [hy, sq (0 : ℤ), zero_mul, mul_zero, sub_zero] at prop
[GOAL]
d : ℤ
a : Solution₁ d
ha : 1 < Solution₁.x a
hy : Solution₁.y a = 0
prop : Solution₁.x a ^ 2 = 1
⊢ False
[PROOFSTEP]
exact lt_irrefl _ (((one_lt_sq_iff <| zero_le_one.trans ha.le).mpr ha).trans_eq prop)
[GOAL]
d : ℤ
a : Solution₁ d
ha : 1 < Solution₁.x a
⊢ 0 < d
[PROOFSTEP]
refine' pos_of_mul_pos_left _ (sq_nonneg a.y)
[GOAL]
d : ℤ
a : Solution₁ d
ha : 1 < Solution₁.x a
⊢ 0 < d * Solution₁.y a ^ 2
[PROOFSTEP]
rw [a.prop_y, sub_pos]
[GOAL]
d : ℤ
a : Solution₁ d
ha : 1 < Solution₁.x a
⊢ 1 < Solution₁.x a ^ 2
[PROOFSTEP]
exact one_lt_pow ha two_ne_zero
[GOAL]
d : ℤ
a : Solution₁ d
ha : 1 < Solution₁.x a
⊢ ¬IsSquare d
[PROOFSTEP]
have hp := a.prop
[GOAL]
d : ℤ
a : Solution₁ d
ha : 1 < Solution₁.x a
hp : Solution₁.x a ^ 2 - d * Solution₁.y a ^ 2 = 1
⊢ ¬IsSquare d
[PROOFSTEP]
rintro ⟨b, rfl⟩
[GOAL]
case intro
b : ℤ
a : Solution₁ (b * b)
ha : 1 < Solution₁.x a
hp : Solution₁.x a ^ 2 - b * b * Solution₁.y a ^ 2 = 1
⊢ False
[PROOFSTEP]
simp_rw [← sq, ← mul_pow, sq_sub_sq, Int.mul_eq_one_iff_eq_one_or_neg_one] at hp
[GOAL]
case intro
b : ℤ
a : Solution₁ (b * b)
ha : 1 < Solution₁.x a
hp :
  Solution₁.x a + b * Solution₁.y a = 1 ∧ Solution₁.x a - b * Solution₁.y a = 1 ∨
    Solution₁.x a + b * Solution₁.y a = -1 ∧ Solution₁.x a - b * Solution₁.y a = -1
⊢ False
[PROOFSTEP]
rcases hp with (⟨hp₁, hp₂⟩ | ⟨hp₁, hp₂⟩)
[GOAL]
case intro.inl.intro
b : ℤ
a : Solution₁ (b * b)
ha : 1 < Solution₁.x a
hp₁ : Solution₁.x a + b * Solution₁.y a = 1
hp₂ : Solution₁.x a - b * Solution₁.y a = 1
⊢ False
[PROOFSTEP]
linarith [ha, hp₁, hp₂]
[GOAL]
case intro.inr.intro
b : ℤ
a : Solution₁ (b * b)
ha : 1 < Solution₁.x a
hp₁ : Solution₁.x a + b * Solution₁.y a = -1
hp₂ : Solution₁.x a - b * Solution₁.y a = -1
⊢ False
[PROOFSTEP]
linarith [ha, hp₁, hp₂]
[GOAL]
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : Solution₁.x a = 1
⊢ a = 1
[PROOFSTEP]
have prop := a.prop_y
[GOAL]
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : Solution₁.x a = 1
prop : d * Solution₁.y a ^ 2 = Solution₁.x a ^ 2 - 1
⊢ a = 1
[PROOFSTEP]
rw [ha, one_pow, sub_self, mul_eq_zero, or_iff_right h₀, sq_eq_zero_iff] at prop
[GOAL]
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : Solution₁.x a = 1
prop : Solution₁.y a = 0
⊢ a = 1
[PROOFSTEP]
exact ext ha prop
[GOAL]
d : ℤ
a : Solution₁ d
⊢ a = 1 ∨ a = -1 ↔ Solution₁.y a = 0
[PROOFSTEP]
refine' ⟨fun H => H.elim (fun h => by simp [h]) fun h => by simp [h], fun H => _⟩
[GOAL]
d : ℤ
a : Solution₁ d
H : a = 1 ∨ a = -1
h : a = 1
⊢ Solution₁.y a = 0
[PROOFSTEP]
simp [h]
[GOAL]
d : ℤ
a : Solution₁ d
H : a = 1 ∨ a = -1
h : a = -1
⊢ Solution₁.y a = 0
[PROOFSTEP]
simp [h]
[GOAL]
d : ℤ
a : Solution₁ d
H : Solution₁.y a = 0
⊢ a = 1 ∨ a = -1
[PROOFSTEP]
have prop := a.prop
[GOAL]
d : ℤ
a : Solution₁ d
H : Solution₁.y a = 0
prop : Solution₁.x a ^ 2 - d * Solution₁.y a ^ 2 = 1
⊢ a = 1 ∨ a = -1
[PROOFSTEP]
rw [H, sq (0 : ℤ), mul_zero, mul_zero, sub_zero, sq_eq_one_iff] at prop
[GOAL]
d : ℤ
a : Solution₁ d
H : Solution₁.y a = 0
prop : Solution₁.x a = 1 ∨ Solution₁.x a = -1
⊢ a = 1 ∨ a = -1
[PROOFSTEP]
exact prop.imp (fun h => ext h H) fun h => ext h H
[GOAL]
d : ℤ
a b : Solution₁ d
ha : 0 < Solution₁.x a
hb : 0 < Solution₁.x b
⊢ 0 < Solution₁.x (a * b)
[PROOFSTEP]
simp only [x_mul]
[GOAL]
d : ℤ
a b : Solution₁ d
ha : 0 < Solution₁.x a
hb : 0 < Solution₁.x b
⊢ 0 < Solution₁.x a * Solution₁.x b + d * (Solution₁.y a * Solution₁.y b)
[PROOFSTEP]
refine' neg_lt_iff_pos_add'.mp (abs_lt.mp _).1
[GOAL]
d : ℤ
a b : Solution₁ d
ha : 0 < Solution₁.x a
hb : 0 < Solution₁.x b
⊢ |d * (Solution₁.y a * Solution₁.y b)| < Solution₁.x a * Solution₁.x b
[PROOFSTEP]
rw [← abs_of_pos ha, ← abs_of_pos hb, ← abs_mul, ← sq_lt_sq, mul_pow a.x, a.prop_x, b.prop_x, ← sub_pos]
[GOAL]
d : ℤ
a b : Solution₁ d
ha : 0 < Solution₁.x a
hb : 0 < Solution₁.x b
⊢ 0 < (1 + d * Solution₁.y a ^ 2) * (1 + d * Solution₁.y b ^ 2) - (d * (Solution₁.y a * Solution₁.y b)) ^ 2
[PROOFSTEP]
ring_nf
[GOAL]
d : ℤ
a b : Solution₁ d
ha : 0 < Solution₁.x a
hb : 0 < Solution₁.x b
⊢ 0 < 1 + d * Solution₁.y a ^ 2 + d * Solution₁.y b ^ 2
[PROOFSTEP]
cases' le_or_lt 0 d with h h
[GOAL]
case inl
d : ℤ
a b : Solution₁ d
ha : 0 < Solution₁.x a
hb : 0 < Solution₁.x b
h : 0 ≤ d
⊢ 0 < 1 + d * Solution₁.y a ^ 2 + d * Solution₁.y b ^ 2
[PROOFSTEP]
positivity
[GOAL]
case inr
d : ℤ
a b : Solution₁ d
ha : 0 < Solution₁.x a
hb : 0 < Solution₁.x b
h : d < 0
⊢ 0 < 1 + d * Solution₁.y a ^ 2 + d * Solution₁.y b ^ 2
[PROOFSTEP]
rw [(eq_zero_of_d_neg h a).resolve_left ha.ne', (eq_zero_of_d_neg h b).resolve_left hb.ne']
  -- Porting note: was
      -- rw [zero_pow two_pos, zero_add, zero_mul, zero_add]
      -- exact one_pos
      -- but this relied on the exact output of `ring_nf`
[GOAL]
case inr
d : ℤ
a b : Solution₁ d
ha : 0 < Solution₁.x a
hb : 0 < Solution₁.x b
h : d < 0
⊢ 0 < 1 + d * 0 ^ 2 + d * 0 ^ 2
[PROOFSTEP]
simp
[GOAL]
d : ℤ
a b : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
hbx : 0 < Solution₁.x b
hby : 0 < Solution₁.y b
⊢ 0 < Solution₁.y (a * b)
[PROOFSTEP]
simp only [y_mul]
[GOAL]
d : ℤ
a b : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
hbx : 0 < Solution₁.x b
hby : 0 < Solution₁.y b
⊢ 0 < Solution₁.x a * Solution₁.y b + Solution₁.y a * Solution₁.x b
[PROOFSTEP]
positivity
[GOAL]
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
n : ℕ
⊢ 0 < Solution₁.x (a ^ n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
⊢ 0 < Solution₁.x (a ^ Nat.zero)
[PROOFSTEP]
simp only [Nat.zero_eq, pow_zero, x_one, zero_lt_one]
[GOAL]
case succ
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
n : ℕ
ih : 0 < Solution₁.x (a ^ n)
⊢ 0 < Solution₁.x (a ^ Nat.succ n)
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
n : ℕ
ih : 0 < Solution₁.x (a ^ n)
⊢ 0 < Solution₁.x (a * a ^ n)
[PROOFSTEP]
exact x_mul_pos hax ih
[GOAL]
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
n : ℕ
⊢ 0 < Solution₁.y (a ^ Nat.succ n)
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ 0 < Solution₁.y (a ^ Nat.succ Nat.zero)
[PROOFSTEP]
simp only [Nat.zero_eq, ← Nat.one_eq_succ_zero, hay, pow_one]
[GOAL]
case succ
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
n : ℕ
ih : 0 < Solution₁.y (a ^ Nat.succ n)
⊢ 0 < Solution₁.y (a ^ Nat.succ (Nat.succ n))
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
n : ℕ
ih : 0 < Solution₁.y (a ^ Nat.succ n)
⊢ 0 < Solution₁.y (a * a ^ (n + 1))
[PROOFSTEP]
exact y_mul_pos hax hay (x_pow_pos hax _) ih
[GOAL]
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
n : ℤ
hn : 0 < n
⊢ 0 < Solution₁.y (a ^ n)
[PROOFSTEP]
lift n to ℕ using hn.le
[GOAL]
case intro
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
n : ℕ
hn : 0 < ↑n
⊢ 0 < Solution₁.y (a ^ ↑n)
[PROOFSTEP]
norm_cast at hn ⊢
[GOAL]
case intro
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
n : ℕ
hn : 0 < n
⊢ 0 < Solution₁.y (a ^ n)
[PROOFSTEP]
rw [← Nat.succ_pred_eq_of_pos hn]
[GOAL]
case intro
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
n : ℕ
hn : 0 < n
⊢ 0 < Solution₁.y (a ^ Nat.succ (Nat.pred n))
[PROOFSTEP]
exact y_pow_succ_pos hax hay _
[GOAL]
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
n : ℤ
⊢ 0 < Solution₁.x (a ^ n)
[PROOFSTEP]
cases n with
| ofNat n =>
  rw [Int.ofNat_eq_coe, zpow_ofNat]
  exact x_pow_pos hax n
| negSucc n =>
  rw [zpow_negSucc]
  exact x_pow_pos hax (n + 1)
[GOAL]
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
n : ℤ
⊢ 0 < Solution₁.x (a ^ n)
[PROOFSTEP]
cases n with
| ofNat n =>
  rw [Int.ofNat_eq_coe, zpow_ofNat]
  exact x_pow_pos hax n
| negSucc n =>
  rw [zpow_negSucc]
  exact x_pow_pos hax (n + 1)
[GOAL]
case ofNat
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
n : ℕ
⊢ 0 < Solution₁.x (a ^ Int.ofNat n)
[PROOFSTEP]

| ofNat n =>
  rw [Int.ofNat_eq_coe, zpow_ofNat]
  exact x_pow_pos hax n
[GOAL]
case ofNat
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
n : ℕ
⊢ 0 < Solution₁.x (a ^ Int.ofNat n)
[PROOFSTEP]
rw [Int.ofNat_eq_coe, zpow_ofNat]
[GOAL]
case ofNat
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
n : ℕ
⊢ 0 < Solution₁.x (a ^ n)
[PROOFSTEP]
exact x_pow_pos hax n
[GOAL]
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
n : ℕ
⊢ 0 < Solution₁.x (a ^ Int.negSucc n)
[PROOFSTEP]

| negSucc n =>
  rw [zpow_negSucc]
  exact x_pow_pos hax (n + 1)
[GOAL]
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
n : ℕ
⊢ 0 < Solution₁.x (a ^ Int.negSucc n)
[PROOFSTEP]
rw [zpow_negSucc]
[GOAL]
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
n : ℕ
⊢ 0 < Solution₁.x (a ^ (n + 1))⁻¹
[PROOFSTEP]
exact x_pow_pos hax (n + 1)
[GOAL]
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
n : ℤ
⊢ Int.sign (Solution₁.y (a ^ n)) = Int.sign n
[PROOFSTEP]
rcases n with ((_ | n) | n)
[GOAL]
case ofNat.zero
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Int.sign (Solution₁.y (a ^ Int.ofNat Nat.zero)) = Int.sign (Int.ofNat Nat.zero)
[PROOFSTEP]
rfl
[GOAL]
case ofNat.succ
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
n : ℕ
⊢ Int.sign (Solution₁.y (a ^ Int.ofNat (Nat.succ n))) = Int.sign (Int.ofNat (Nat.succ n))
[PROOFSTEP]
rw [Int.ofNat_eq_coe, zpow_ofNat]
[GOAL]
case ofNat.succ
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
n : ℕ
⊢ Int.sign (Solution₁.y (a ^ Nat.succ n)) = Int.sign ↑(Nat.succ n)
[PROOFSTEP]
exact Int.sign_eq_one_of_pos (y_pow_succ_pos hax hay n)
[GOAL]
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
n : ℕ
⊢ Int.sign (Solution₁.y (a ^ Int.negSucc n)) = Int.sign (Int.negSucc n)
[PROOFSTEP]
rw [zpow_negSucc]
[GOAL]
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 < Solution₁.y a
n : ℕ
⊢ Int.sign (Solution₁.y (a ^ (n + 1))⁻¹) = Int.sign (Int.negSucc n)
[PROOFSTEP]
exact Int.sign_eq_neg_one_of_neg (neg_neg_of_pos (y_pow_succ_pos hax hay n))
[GOAL]
d : ℤ
h₀ : 0 < d
a : Solution₁ d
⊢ ∃ b, 0 < Solution₁.x b ∧ 0 ≤ Solution₁.y b ∧ a ∈ {b, b⁻¹, -b, -b⁻¹}
[PROOFSTEP]
refine'
  (lt_or_gt_of_ne (a.x_ne_zero h₀.le)).elim
    ((le_total 0 a.y).elim (fun hy hx => ⟨-a⁻¹, _, _, _⟩) fun hy hx => ⟨-a, _, _, _⟩)
    ((le_total 0 a.y).elim (fun hy hx => ⟨a, hx, hy, _⟩) fun hy hx => ⟨a⁻¹, hx, _, _⟩)
[GOAL]
case refine'_1
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ Solution₁.y a
hx : Solution₁.x a < 0
⊢ 0 < Solution₁.x (-a⁻¹)
[PROOFSTEP]
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or_iff, eq_self_iff_true, x_neg,
  x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true_iff]
[GOAL]
case refine'_2
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ Solution₁.y a
hx : Solution₁.x a < 0
⊢ 0 ≤ Solution₁.y (-a⁻¹)
[PROOFSTEP]
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or_iff, eq_self_iff_true, x_neg,
  x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true_iff]
[GOAL]
case refine'_3
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ Solution₁.y a
hx : Solution₁.x a < 0
⊢ a ∈ {-a⁻¹, (-a⁻¹)⁻¹, - -a⁻¹, -(-a⁻¹)⁻¹}
[PROOFSTEP]
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or_iff, eq_self_iff_true, x_neg,
  x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true_iff]
[GOAL]
case refine'_4
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : Solution₁.y a ≤ 0
hx : Solution₁.x a < 0
⊢ 0 < Solution₁.x (-a)
[PROOFSTEP]
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or_iff, eq_self_iff_true, x_neg,
  x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true_iff]
[GOAL]
case refine'_5
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : Solution₁.y a ≤ 0
hx : Solution₁.x a < 0
⊢ 0 ≤ Solution₁.y (-a)
[PROOFSTEP]
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or_iff, eq_self_iff_true, x_neg,
  x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true_iff]
[GOAL]
case refine'_6
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : Solution₁.y a ≤ 0
hx : Solution₁.x a < 0
⊢ a ∈ {-a, (-a)⁻¹, - -a, -(-a)⁻¹}
[PROOFSTEP]
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or_iff, eq_self_iff_true, x_neg,
  x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true_iff]
[GOAL]
case refine'_7
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ Solution₁.y a
hx : Solution₁.x a > 0
⊢ a ∈ {a, a⁻¹, -a, -a⁻¹}
[PROOFSTEP]
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or_iff, eq_self_iff_true, x_neg,
  x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true_iff]
[GOAL]
case refine'_8
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : Solution₁.y a ≤ 0
hx : Solution₁.x a > 0
⊢ 0 ≤ Solution₁.y a⁻¹
[PROOFSTEP]
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or_iff, eq_self_iff_true, x_neg,
  x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true_iff]
[GOAL]
case refine'_9
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : Solution₁.y a ≤ 0
hx : Solution₁.x a > 0
⊢ a ∈ {a⁻¹, a⁻¹⁻¹, -a⁻¹, -a⁻¹⁻¹}
[PROOFSTEP]
simp only [neg_neg, inv_inv, neg_inv, Set.mem_insert_iff, Set.mem_singleton_iff, true_or_iff, eq_self_iff_true, x_neg,
  x_inv, y_neg, y_inv, neg_pos, neg_nonneg, or_true_iff]
[GOAL]
case refine'_1
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ Solution₁.y a
hx : Solution₁.x a < 0
⊢ Solution₁.x a < 0
[PROOFSTEP]
assumption
[GOAL]
case refine'_2
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ Solution₁.y a
hx : Solution₁.x a < 0
⊢ 0 ≤ Solution₁.y a
[PROOFSTEP]
assumption
[GOAL]
case refine'_4
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : Solution₁.y a ≤ 0
hx : Solution₁.x a < 0
⊢ Solution₁.x a < 0
[PROOFSTEP]
assumption
[GOAL]
case refine'_5
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : Solution₁.y a ≤ 0
hx : Solution₁.x a < 0
⊢ Solution₁.y a ≤ 0
[PROOFSTEP]
assumption
[GOAL]
case refine'_8
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : Solution₁.y a ≤ 0
hx : Solution₁.x a > 0
⊢ Solution₁.y a ≤ 0
[PROOFSTEP]
assumption
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
let ξ : ℝ := sqrt d
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
have hξ : Irrational ξ :=
  by
  refine' irrational_nrt_of_notint_nrt 2 d (sq_sqrt <| Int.cast_nonneg.mpr h₀.le) _ two_pos
  rintro ⟨x, hx⟩
  refine' hd ⟨x, @Int.cast_injective ℝ _ _ d (x * x) _⟩
  rw [← sq_sqrt <| Int.cast_nonneg.mpr h₀.le, Int.cast_mul, ← hx, sq]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
⊢ Irrational ξ
[PROOFSTEP]
refine' irrational_nrt_of_notint_nrt 2 d (sq_sqrt <| Int.cast_nonneg.mpr h₀.le) _ two_pos
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
⊢ ¬∃ y, ξ = ↑y
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
x : ℤ
hx : ξ = ↑x
⊢ False
[PROOFSTEP]
refine' hd ⟨x, @Int.cast_injective ℝ _ _ d (x * x) _⟩
[GOAL]
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
x : ℤ
hx : ξ = ↑x
⊢ ↑d = ↑(x * x)
[PROOFSTEP]
rw [← sq_sqrt <| Int.cast_nonneg.mpr h₀.le, Int.cast_mul, ← hx, sq]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
obtain ⟨M, hM₁⟩ := exists_int_gt (2 * |ξ| + 1)
[GOAL]
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
have hM : {q : ℚ | |q.1 ^ 2 - d * (q.2 : ℤ) ^ 2| < M}.Infinite :=
  by
  refine' Infinite.mono (fun q h => _) (infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational hξ)
  have h0 : 0 < (q.2 : ℝ) ^ 2 := pow_pos (Nat.cast_pos.mpr q.pos) 2
  have h1 : (q.num : ℝ) / (q.den : ℝ) = q := by exact_mod_cast q.num_div_den
  rw [mem_setOf, abs_sub_comm, ← @Int.cast_lt ℝ, ← div_lt_div_right (abs_pos_of_pos h0)]
  push_cast
  rw [← abs_div, abs_sq, sub_div, mul_div_cancel _ h0.ne', ← div_pow, h1, ← sq_sqrt (Int.cast_pos.mpr h₀).le, sq_sub_sq,
    abs_mul, ← mul_one_div]
  refine' mul_lt_mul'' (((abs_add ξ q).trans _).trans_lt hM₁) h (abs_nonneg _) (abs_nonneg _)
  rw [two_mul, add_assoc, add_le_add_iff_left, ← sub_le_iff_le_add']
  rw [mem_setOf, abs_sub_comm] at h
  refine' (abs_sub_abs_le_abs_sub (q : ℝ) ξ).trans (h.le.trans _)
  rw [div_le_one h0, one_le_sq_iff_one_le_abs, Nat.abs_cast, Nat.one_le_cast]
  exact q.pos
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
⊢ Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
[PROOFSTEP]
refine' Infinite.mono (fun q h => _) (infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational hξ)
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑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}
[PROOFSTEP]
have h0 : 0 < (q.2 : ℝ) ^ 2 := pow_pos (Nat.cast_pos.mpr q.pos) 2
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
⊢ q ∈ {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
[PROOFSTEP]
have h1 : (q.num : ℝ) / (q.den : ℝ) = q := by exact_mod_cast q.num_div_den
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
⊢ ↑q.num / ↑q.den = ↑q
[PROOFSTEP]
exact_mod_cast q.num_div_den
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑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}
[PROOFSTEP]
rw [mem_setOf, abs_sub_comm, ← @Int.cast_lt ℝ, ← div_lt_div_right (abs_pos_of_pos h0)]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑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|
[PROOFSTEP]
push_cast
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑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|
[PROOFSTEP]
rw [← abs_div, abs_sq, sub_div, mul_div_cancel _ h0.ne', ← div_pow, h1, ← sq_sqrt (Int.cast_pos.mpr h₀).le, sq_sub_sq,
  abs_mul, ← mul_one_div]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑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
⊢ |sqrt ↑d + ↑q| * |sqrt ↑d - ↑q| < ↑M * (1 / ↑q.den ^ 2)
[PROOFSTEP]
refine' mul_lt_mul'' (((abs_add ξ q).trans _).trans_lt hM₁) h (abs_nonneg _) (abs_nonneg _)
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑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
[PROOFSTEP]
rw [two_mul, add_assoc, add_le_add_iff_left, ← sub_le_iff_le_add']
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑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| - |ξ| ≤ 1
[PROOFSTEP]
rw [mem_setOf, abs_sub_comm] at h
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑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
[PROOFSTEP]
refine' (abs_sub_abs_le_abs_sub (q : ℝ) ξ).trans (h.le.trans _)
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑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
[PROOFSTEP]
rw [div_le_one h0, one_le_sq_iff_one_le_abs, Nat.abs_cast, Nat.one_le_cast]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑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
[PROOFSTEP]
exact q.pos
[GOAL]
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
obtain ⟨m, hm⟩ : ∃ m : ℤ, {q : ℚ | q.1 ^ 2 - d * (q.den : ℤ) ^ 2 = m}.Infinite :=
  by
  contrapose! hM
  simp only [not_infinite] at hM ⊢
  refine' (congr_arg _ (ext fun x => _)).mp (Finite.biUnion (finite_Ioo (-M) M) fun m _ => hM m)
  simp only [abs_lt, mem_setOf, mem_Ioo, mem_iUnion, exists_prop, exists_eq_right']
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
⊢ ∃ m, Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
[PROOFSTEP]
contrapose! hM
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : ∀ (m : ℤ), ¬Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
⊢ ¬Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
[PROOFSTEP]
simp only [not_infinite] at hM ⊢
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : ∀ (m : ℤ), Set.Finite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
⊢ Set.Finite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
[PROOFSTEP]
refine' (congr_arg _ (ext fun x => _)).mp (Finite.biUnion (finite_Ioo (-M) M) fun m _ => hM m)
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : ∀ (m : ℤ), Set.Finite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
x : ℚ
⊢ x ∈ ⋃ (i : ℤ) (_ : i ∈ Ioo (-M) M), {q | q.num ^ 2 - d * ↑q.den ^ 2 = i} ↔ x ∈ {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
[PROOFSTEP]
simp only [abs_lt, mem_setOf, mem_Ioo, mem_iUnion, exists_prop, exists_eq_right']
[GOAL]
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
have hm₀ : m ≠ 0 := by
  rintro rfl
  obtain ⟨q, hq⟩ := hm.nonempty
  rw [mem_setOf, sub_eq_zero, mul_comm] at hq
  obtain ⟨a, ha⟩ := (Int.pow_dvd_pow_iff two_pos).mp ⟨d, hq⟩
  rw [ha, mul_pow, mul_right_inj' (pow_pos (Int.coe_nat_pos.mpr q.pos) 2).ne'] at hq
  exact hd ⟨a, sq a ▸ hq.symm⟩
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
⊢ m ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}
⊢ False
[PROOFSTEP]
obtain ⟨q, hq⟩ := hm.nonempty
[GOAL]
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}
q : ℚ
hq : q ∈ {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}
⊢ False
[PROOFSTEP]
rw [mem_setOf, sub_eq_zero, mul_comm] at hq
[GOAL]
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}
q : ℚ
hq : q.num ^ 2 = ↑q.den ^ 2 * d
⊢ False
[PROOFSTEP]
obtain ⟨a, ha⟩ := (Int.pow_dvd_pow_iff two_pos).mp ⟨d, hq⟩
[GOAL]
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}
q : ℚ
hq : q.num ^ 2 = ↑q.den ^ 2 * d
a : ℤ
ha : q.num = ↑q.den * a
⊢ False
[PROOFSTEP]
rw [ha, mul_pow, mul_right_inj' (pow_pos (Int.coe_nat_pos.mpr q.pos) 2).ne'] at hq
[GOAL]
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}
q : ℚ
a : ℤ
hq : a ^ 2 = d
ha : q.num = ↑q.den * a
⊢ False
[PROOFSTEP]
exact hd ⟨a, sq a ▸ hq.symm⟩
[GOAL]
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
haveI := neZero_iff.mpr (Int.natAbs_ne_zero.mpr hm₀)
[GOAL]
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
let f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q => (q.num, q.den)
[GOAL]
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := fun q => (↑q.num, ↑q.den)
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
obtain ⟨q₁, h₁ : q₁.num ^ 2 - d * (q₁.den : ℤ) ^ 2 = m, q₂, h₂ : q₂.num ^ 2 - d * (q₂.den : ℤ) ^ 2 = m, hne, hqf⟩ :=
  hm.exists_ne_map_eq_of_mapsTo (mapsTo_univ f _) finite_univ
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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₂
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
obtain ⟨hq1 : (q₁.num : ZMod m.natAbs) = q₂.num, hq2 : (q₁.den : ZMod m.natAbs) = q₂.den⟩ := Prod.ext_iff.mp hqf
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
have hd₁ : m ∣ q₁.num * q₂.num - d * (q₁.den * q₂.den) :=
  by
  rw [← Int.natAbs_dvd, ← ZMod.int_cast_zmod_eq_zero_iff_dvd]
  push_cast
  rw [hq1, hq2, ← sq, ← sq]
  norm_cast
  rw [ZMod.int_cast_zmod_eq_zero_iff_dvd, Int.natAbs_dvd, Nat.cast_pow, ← h₂]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
⊢ m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
[PROOFSTEP]
rw [← Int.natAbs_dvd, ← ZMod.int_cast_zmod_eq_zero_iff_dvd]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
⊢ ↑(q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)) = 0
[PROOFSTEP]
push_cast
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
⊢ ↑q₁.num * ↑q₂.num - ↑d * (↑q₁.den * ↑q₂.den) = 0
[PROOFSTEP]
rw [hq1, hq2, ← sq, ← sq]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
⊢ ↑q₂.num ^ 2 - ↑d * ↑q₂.den ^ 2 = 0
[PROOFSTEP]
norm_cast
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
⊢ ↑(q₂.num ^ 2 - d * ↑(q₂.den ^ 2)) = 0
[PROOFSTEP]
rw [ZMod.int_cast_zmod_eq_zero_iff_dvd, Int.natAbs_dvd, Nat.cast_pow, ← h₂]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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)
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
have hd₂ : m ∣ q₁.num * q₂.den - q₂.num * q₁.den :=
  by
  rw [← Int.natAbs_dvd, ← ZMod.int_cast_eq_int_cast_iff_dvd_sub]
  push_cast
  rw [hq1, hq2]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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)
⊢ m ∣ q₁.num * ↑q₂.den - q₂.num * ↑q₁.den
[PROOFSTEP]
rw [← Int.natAbs_dvd, ← ZMod.int_cast_eq_int_cast_iff_dvd_sub]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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)
⊢ ↑(q₂.num * ↑q₁.den) = ↑(q₁.num * ↑q₂.den)
[PROOFSTEP]
push_cast
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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)
⊢ ↑q₂.num * ↑q₁.den = ↑q₁.num * ↑q₂.den
[PROOFSTEP]
rw [hq1, hq2]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
hm₀ : m ≠ 0
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
replace hm₀ : (m : ℚ) ≠ 0 := Int.cast_ne_zero.mpr hm₀
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
⊢ ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
[PROOFSTEP]
refine' ⟨(q₁.num * q₂.num - d * (q₁.den * q₂.den)) / m, (q₁.num * q₂.den - q₂.num * q₁.den) / m, _, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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)) / m) ^ 2 - d * ((q₁.num * ↑q₂.den - q₂.num * ↑q₁.den) / m) ^ 2 = 1
[PROOFSTEP]
qify [hd₁, hd₂]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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)) / ↑m) ^ 2 - ↑d * ((↑q₁.num * ↑q₂.den - ↑q₂.num * ↑q₁.den) / ↑m) ^ 2 =
    1
[PROOFSTEP]
field_simp [hm₀]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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 = ↑m ^ 2
[PROOFSTEP]
norm_cast
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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 = m ^ 2
[PROOFSTEP]
conv_rhs =>
  rw [sq]
  congr
  ·rw [← h₁]
  ·rw [← h₂]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
| m ^ 2
[PROOFSTEP]
  rw [sq]
  congr
  ·rw [← h₁]
  ·rw [← h₂]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
| m ^ 2
[PROOFSTEP]
  rw [sq]
  congr
  ·rw [← h₁]
  ·rw [← h₂]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
| m ^ 2
[PROOFSTEP]
rw [sq]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
| m * m
[PROOFSTEP]
congr
[GOAL]
case a
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
| m
case a
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
| m
[PROOFSTEP]
·rw [← h₁]
[GOAL]
case a
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
| m
[PROOFSTEP]
rw [← h₁]
[GOAL]
case a
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
| m
[PROOFSTEP]
rw [← h₁]
[GOAL]
case a
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
| m
[PROOFSTEP]
rw [← h₁]
[GOAL]
case a
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
| m
[PROOFSTEP]
·rw [← h₂]
[GOAL]
case a
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
| m
[PROOFSTEP]
rw [← h₂]
[GOAL]
case a
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
| m
[PROOFSTEP]
rw [← h₂]
[GOAL]
case a
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
| m
[PROOFSTEP]
rw [← h₂]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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)
[PROOFSTEP]
push_cast
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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)
[PROOFSTEP]
ring
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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) / m ≠ 0
[PROOFSTEP]
qify [hd₂]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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) / ↑m ≠ 0
[PROOFSTEP]
refine' div_ne_zero_iff.mpr ⟨_, hm₀⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro.refine'_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := sqrt ↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : Set.Infinite {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}
m : ℤ
hm : Set.Infinite {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}
this : NeZero (Int.natAbs m)
f : ℚ → ZMod (Int.natAbs m) × ZMod (Int.natAbs m) := 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
[PROOFSTEP]
exact_mod_cast mt sub_eq_zero.mp (mt Rat.eq_iff_mul_eq_mul.mpr hne)
[GOAL]
d : ℤ
h₀ : 0 < d
⊢ (∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) ↔ ¬IsSquare d
[PROOFSTEP]
refine' ⟨_, exists_of_not_isSquare h₀⟩
[GOAL]
d : ℤ
h₀ : 0 < d
⊢ (∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) → ¬IsSquare d
[PROOFSTEP]
rintro ⟨x, y, hxy, hy⟩ ⟨a, rfl⟩
[GOAL]
case intro.intro.intro.intro
x y : ℤ
hy : y ≠ 0
a : ℤ
h₀ : 0 < a * a
hxy : x ^ 2 - a * a * y ^ 2 = 1
⊢ False
[PROOFSTEP]
rw [← sq, ← mul_pow, sq_sub_sq] at hxy
[GOAL]
case intro.intro.intro.intro
x y : ℤ
hy : y ≠ 0
a : ℤ
h₀ : 0 < a * a
hxy : (x + a * y) * (x - a * y) = 1
⊢ False
[PROOFSTEP]
simpa [hy, mul_self_pos.mp h₀, sub_eq_add_neg, eq_neg_self_iff] using Int.eq_of_mul_eq_one hxy
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
⊢ ∃ a, a ≠ 1 ∧ a ≠ -1
[PROOFSTEP]
obtain ⟨x, y, prop, hy⟩ := exists_of_not_isSquare h₀ hd
[GOAL]
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ ∃ a, a ≠ 1 ∧ a ≠ -1
[PROOFSTEP]
refine' ⟨mk x y prop, fun H => _, fun H => _⟩
[GOAL]
case intro.intro.intro.refine'_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : mk x y prop = 1
⊢ False
[PROOFSTEP]
apply_fun Solution₁.y at H
[GOAL]
case intro.intro.intro.refine'_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : mk x y prop = -1
⊢ False
[PROOFSTEP]
apply_fun Solution₁.y at H
[GOAL]
case intro.intro.intro.refine'_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : Solution₁.y (mk x y prop) = Solution₁.y 1
⊢ False
[PROOFSTEP]
simp [hy] at H
[GOAL]
case intro.intro.intro.refine'_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : Solution₁.y (mk x y prop) = Solution₁.y (-1)
⊢ False
[PROOFSTEP]
simp [hy] at H
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
⊢ ∃ a, 1 < Solution₁.x a ∧ 0 < Solution₁.y a
[PROOFSTEP]
obtain ⟨x, y, h, hy⟩ := exists_of_not_isSquare h₀ hd
[GOAL]
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ ∃ a, 1 < Solution₁.x a ∧ 0 < Solution₁.y a
[PROOFSTEP]
refine' ⟨mk |x| |y| (by rwa [sq_abs, sq_abs]), _, abs_pos.mpr hy⟩
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ |x| ^ 2 - d * |y| ^ 2 = 1
[PROOFSTEP]
rwa [sq_abs, sq_abs]
[GOAL]
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ 1 < Solution₁.x (mk |x| |y| (_ : |x| ^ 2 - d * |y| ^ 2 = 1))
[PROOFSTEP]
rw [x_mk, ← one_lt_sq_iff_one_lt_abs, eq_add_of_sub_eq h, lt_add_iff_pos_right]
[GOAL]
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
h : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ 0 < d * y ^ 2
[PROOFSTEP]
exact mul_pos h₀ (sq_pos_of_ne_zero y hy)
[GOAL]
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
⊢ a = b
[PROOFSTEP]
have hx := le_antisymm (ha.2.2 hb.1) (hb.2.2 ha.1)
[GOAL]
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : Solution₁.x a = Solution₁.x b
⊢ a = b
[PROOFSTEP]
refine' Solution₁.ext hx _
[GOAL]
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : Solution₁.x a = Solution₁.x b
⊢ Solution₁.y a = Solution₁.y b
[PROOFSTEP]
have : d * a.y ^ 2 = d * b.y ^ 2 := by rw [a.prop_y, b.prop_y, hx]
[GOAL]
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : Solution₁.x a = Solution₁.x b
⊢ d * Solution₁.y a ^ 2 = d * Solution₁.y b ^ 2
[PROOFSTEP]
rw [a.prop_y, b.prop_y, hx]
[GOAL]
d : ℤ
a b : Solution₁ d
ha : IsFundamental a
hb : IsFundamental b
hx : Solution₁.x a = Solution₁.x b
this : d * Solution₁.y a ^ 2 = d * Solution₁.y b ^ 2
⊢ Solution₁.y a = Solution₁.y b
[PROOFSTEP]
exact (sq_eq_sq ha.2.1.le hb.2.1.le).mp (Int.eq_of_mul_eq_mul_left ha.d_pos.ne' this)
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
⊢ ∃ a, IsFundamental a
[PROOFSTEP]
obtain ⟨a, ha₁, ha₂⟩ := exists_pos_of_not_isSquare h₀ hd
[GOAL]
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
⊢ ∃ a, IsFundamental a
[PROOFSTEP]
have P : ∃ x' : ℕ, 1 < x' ∧ ∃ y' : ℤ, 0 < y' ∧ (x' : ℤ) ^ 2 - d * y' ^ 2 = 1 :=
  by
  have hax := a.prop
  lift a.x to ℕ using by positivity with ax
  norm_cast at ha₁
  exact ⟨ax, ha₁, a.y, ha₂, hax⟩
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
⊢ ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
[PROOFSTEP]
have hax := a.prop
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
hax : Solution₁.x a ^ 2 - d * Solution₁.y a ^ 2 = 1
⊢ ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
[PROOFSTEP]
lift a.x to ℕ using by positivity with ax
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
hax : Solution₁.x a ^ 2 - d * Solution₁.y a ^ 2 = 1
⊢ 0 ≤ Solution₁.x a
[PROOFSTEP]
positivity
[GOAL]
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₂ : 0 < Solution₁.y a
ax : ℕ
ha₁✝ ha₁ : 1 < ↑ax
hax✝ hax : ↑ax ^ 2 - d * Solution₁.y a ^ 2 = 1
⊢ ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
[PROOFSTEP]
norm_cast at ha₁
[GOAL]
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₂ : 0 < Solution₁.y a
ax : ℕ
ha₁✝ : 1 < ↑ax
hax✝ hax : ↑ax ^ 2 - d * Solution₁.y a ^ 2 = 1
ha₁ : 1 < ax
⊢ ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
[PROOFSTEP]
exact ⟨ax, ha₁, a.y, ha₂, hax⟩
[GOAL]
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
⊢ ∃ a, IsFundamental a
[PROOFSTEP]
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
[GOAL]
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
⊢ ∃ a, IsFundamental a
[PROOFSTEP]
let x₁ := Nat.find P
[GOAL]
case intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
⊢ ∃ a, IsFundamental a
[PROOFSTEP]
obtain ⟨hx, y₁, hy₀, hy₁⟩ := Nat.find_spec P
[GOAL]
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
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
[PROOFSTEP]
refine' ⟨mk x₁ y₁ hy₁, by rw [x_mk]; exact_mod_cast hx, hy₀, fun {b} hb => _⟩
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
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₁.x (Solution₁.mk (↑x₁) y₁ hy₁)
[PROOFSTEP]
rw [x_mk]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
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₁
[PROOFSTEP]
exact_mod_cast hx
[GOAL]
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
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 < Solution₁.x b
⊢ Solution₁.x (Solution₁.mk (↑x₁) y₁ hy₁) ≤ Solution₁.x b
[PROOFSTEP]
rw [x_mk]
[GOAL]
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
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 < Solution₁.x b
⊢ ↑x₁ ≤ Solution₁.x b
[PROOFSTEP]
have hb' := (Int.toNat_of_nonneg <| zero_le_one.trans hb.le).symm
[GOAL]
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
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 < Solution₁.x b
hb' : Solution₁.x b = ↑(Int.toNat (Solution₁.x b))
⊢ ↑x₁ ≤ Solution₁.x b
[PROOFSTEP]
have hb'' := hb
[GOAL]
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
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 < Solution₁.x b
hb' : Solution₁.x b = ↑(Int.toNat (Solution₁.x b))
hb'' : 1 < Solution₁.x b
⊢ ↑x₁ ≤ Solution₁.x b
[PROOFSTEP]
rw [hb'] at hb ⊢
[GOAL]
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
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 < ↑(Int.toNat (Solution₁.x b))
hb' : Solution₁.x b = ↑(Int.toNat (Solution₁.x b))
hb'' : 1 < Solution₁.x b
⊢ ↑x₁ ≤ ↑(Int.toNat (Solution₁.x b))
[PROOFSTEP]
norm_cast at hb ⊢
[GOAL]
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
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' : Solution₁.x b = ↑(Int.toNat (Solution₁.x b))
hb'' : 1 < Solution₁.x b
hb : 1 < Int.toNat (Solution₁.x b)
⊢ x₁ ≤ Int.toNat (Solution₁.x b)
[PROOFSTEP]
refine' Nat.find_min' P ⟨hb, |b.y|, abs_pos.mpr <| y_ne_zero_of_one_lt_x hb'', _⟩
[GOAL]
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
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' : Solution₁.x b = ↑(Int.toNat (Solution₁.x b))
hb'' : 1 < Solution₁.x b
hb : 1 < Int.toNat (Solution₁.x b)
⊢ ↑(Int.toNat (Solution₁.x b)) ^ 2 - d * |Solution₁.y b| ^ 2 = 1
[PROOFSTEP]
rw [← hb', sq_abs]
[GOAL]
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < Solution₁.x a
ha₂ : 0 < Solution₁.y a
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' : Solution₁.x b = ↑(Int.toNat (Solution₁.x b))
hb'' : 1 < Solution₁.x b
hb : 1 < Int.toNat (Solution₁.x b)
⊢ Solution₁.x b ^ 2 - d * Solution₁.y b ^ 2 = 1
[PROOFSTEP]
exact b.prop
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
⊢ StrictMono fun n => Solution₁.y (a ^ n)
[PROOFSTEP]
have H : ∀ n : ℤ, 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y :=
  by
  intro n hn
  rw [← sub_pos, zpow_add, zpow_one, y_mul, add_sub_assoc]
  rw [show (a ^ n).y * a.x - (a ^ n).y = (a ^ n).y * (a.x - 1) by ring]
  refine'
    add_pos_of_pos_of_nonneg (mul_pos (x_zpow_pos h.x_pos _) h.2.1) (mul_nonneg _ (by rw [sub_nonneg]; exact h.1.le))
  rcases hn.eq_or_lt with (rfl | hn)
  · simp only [zpow_zero, y_one]
  · exact (y_zpow_pos h.x_pos h.2.1 hn).le
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
⊢ ∀ (n : ℤ), 0 ≤ n → Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
[PROOFSTEP]
intro n hn
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
[PROOFSTEP]
rw [← sub_pos, zpow_add, zpow_one, y_mul, add_sub_assoc]
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 < Solution₁.x (a ^ n) * Solution₁.y a + (Solution₁.y (a ^ n) * Solution₁.x a - Solution₁.y (a ^ n))
[PROOFSTEP]
rw [show (a ^ n).y * a.x - (a ^ n).y = (a ^ n).y * (a.x - 1) by ring]
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ Solution₁.y (a ^ n) * Solution₁.x a - Solution₁.y (a ^ n) = Solution₁.y (a ^ n) * (Solution₁.x a - 1)
[PROOFSTEP]
ring
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 < Solution₁.x (a ^ n) * Solution₁.y a + Solution₁.y (a ^ n) * (Solution₁.x a - 1)
[PROOFSTEP]
refine'
  add_pos_of_pos_of_nonneg (mul_pos (x_zpow_pos h.x_pos _) h.2.1) (mul_nonneg _ (by rw [sub_nonneg]; exact h.1.le))
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 ≤ Solution₁.x a - 1
[PROOFSTEP]
rw [sub_nonneg]
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 1 ≤ Solution₁.x a
[PROOFSTEP]
exact h.1.le
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 ≤ Solution₁.y (a ^ n)
[PROOFSTEP]
rcases hn.eq_or_lt with (rfl | hn)
[GOAL]
case inl
d : ℤ
a : Solution₁ d
h : IsFundamental a
hn : 0 ≤ 0
⊢ 0 ≤ Solution₁.y (a ^ 0)
[PROOFSTEP]
simp only [zpow_zero, y_one]
[GOAL]
case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn✝ : 0 ≤ n
hn : 0 < n
⊢ 0 ≤ Solution₁.y (a ^ n)
[PROOFSTEP]
exact (y_zpow_pos h.x_pos h.2.1 hn).le
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
⊢ StrictMono fun n => Solution₁.y (a ^ n)
[PROOFSTEP]
refine' strictMono_int_of_lt_succ fun n => _
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
n : ℤ
⊢ Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
[PROOFSTEP]
cases' le_or_lt 0 n with hn hn
[GOAL]
case inl
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
n : ℤ
hn : 0 ≤ n
⊢ Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
[PROOFSTEP]
exact H n hn
[GOAL]
case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
n : ℤ
hn : n < 0
⊢ Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
[PROOFSTEP]
let m : ℤ := -n - 1
[GOAL]
case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
n : ℤ
hn : n < 0
m : ℤ := -n - 1
⊢ Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
[PROOFSTEP]
have hm : n = -m - 1 := by simp only [neg_sub, sub_neg_eq_add, add_tsub_cancel_left]
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
n : ℤ
hn : n < 0
m : ℤ := -n - 1
⊢ n = -m - 1
[PROOFSTEP]
simp only [neg_sub, sub_neg_eq_add, add_tsub_cancel_left]
[GOAL]
case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
n : ℤ
hn : n < 0
m : ℤ := -n - 1
hm : n = -m - 1
⊢ Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
[PROOFSTEP]
rw [hm, sub_add_cancel, ← neg_add', zpow_neg, zpow_neg, y_inv, y_inv, neg_lt_neg_iff]
[GOAL]
case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
n : ℤ
hn : n < 0
m : ℤ := -n - 1
hm : n = -m - 1
⊢ Solution₁.y (a ^ m) < Solution₁.y (a ^ (m + 1))
[PROOFSTEP]
exact H _ (by linarith [hn])
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → Solution₁.y (a ^ n) < Solution₁.y (a ^ (n + 1))
n : ℤ
hn : n < 0
m : ℤ := -n - 1
hm : n = -m - 1
⊢ 0 ≤ m
[PROOFSTEP]
linarith [hn]
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
⊢ Solution₁.y (a ^ m) < Solution₁.y (a ^ n) ↔ m < n
[PROOFSTEP]
refine' ⟨fun H => _, fun H => h.y_strictMono H⟩
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
H : Solution₁.y (a ^ m) < Solution₁.y (a ^ n)
⊢ m < n
[PROOFSTEP]
contrapose! H
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
H : n ≤ m
⊢ Solution₁.y (a ^ n) ≤ Solution₁.y (a ^ m)
[PROOFSTEP]
exact h.y_strictMono.monotone H
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
⊢ a ^ n = 1 ↔ n = 0
[PROOFSTEP]
rw [← zpow_zero a]
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
⊢ a ^ n = a ^ 0 ↔ n = 0
[PROOFSTEP]
exact ⟨fun H => h.y_strictMono.injective (congr_arg Solution₁.y H), fun H => H ▸ rfl⟩
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
⊢ a ^ n ≠ -a ^ n'
[PROOFSTEP]
intro hf
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : a ^ n = -a ^ n'
⊢ False
[PROOFSTEP]
apply_fun Solution₁.x at hf
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : Solution₁.x (a ^ n) = Solution₁.x (-a ^ n')
⊢ False
[PROOFSTEP]
have H := x_zpow_pos h.x_pos n
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : Solution₁.x (a ^ n) = Solution₁.x (-a ^ n')
H : 0 < Solution₁.x (a ^ n)
⊢ False
[PROOFSTEP]
rw [hf, x_neg, lt_neg, neg_zero] at H
[GOAL]
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : Solution₁.x (a ^ n) = Solution₁.x (-a ^ n')
H : Solution₁.x (a ^ n') < 0
⊢ False
[PROOFSTEP]
exact lt_irrefl _ ((x_zpow_pos h.x_pos n').trans H)
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.y a₁ ≤ Solution₁.y a
[PROOFSTEP]
have H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2 := by rw [a.prop_x, a₁.prop_x]; ring
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ d * (Solution₁.y a₁ ^ 2 - Solution₁.y a ^ 2) = Solution₁.x a₁ ^ 2 - Solution₁.x a ^ 2
[PROOFSTEP]
rw [a.prop_x, a₁.prop_x]
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ d * (Solution₁.y a₁ ^ 2 - Solution₁.y a ^ 2) = 1 + d * Solution₁.y a₁ ^ 2 - (1 + d * Solution₁.y a ^ 2)
[PROOFSTEP]
ring
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
H : d * (Solution₁.y a₁ ^ 2 - Solution₁.y a ^ 2) = Solution₁.x a₁ ^ 2 - Solution₁.x a ^ 2
⊢ Solution₁.y a₁ ≤ Solution₁.y a
[PROOFSTEP]
rw [← abs_of_pos hay, ← abs_of_pos h.2.1, ← sq_le_sq, ← mul_le_mul_left h.d_pos, ← sub_nonpos, ← mul_sub, H, sub_nonpos,
  sq_le_sq, abs_of_pos (zero_lt_one.trans h.1), abs_of_pos (zero_lt_one.trans hax)]
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
H : d * (Solution₁.y a₁ ^ 2 - Solution₁.y a ^ 2) = Solution₁.x a₁ ^ 2 - Solution₁.x a ^ 2
⊢ Solution₁.x a₁ ≤ Solution₁.x a
[PROOFSTEP]
exact h.x_le_x hax
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.x a * Solution₁.y a₁ ≤ Solution₁.y a * Solution₁.x a₁
[PROOFSTEP]
rw [← abs_of_pos <| zero_lt_one.trans hax, ← abs_of_pos hay, ← abs_of_pos h.x_pos, ← abs_of_pos h.2.1, ← abs_mul, ←
  abs_mul, ← sq_le_sq, mul_pow, mul_pow, a.prop_x, a₁.prop_x, ← sub_nonneg]
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ 0 ≤ Solution₁.y a ^ 2 * (1 + d * Solution₁.y a₁ ^ 2) - (1 + d * Solution₁.y a ^ 2) * Solution₁.y a₁ ^ 2
[PROOFSTEP]
ring_nf
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ 0 ≤ Solution₁.y a ^ 2 - Solution₁.y a₁ ^ 2
[PROOFSTEP]
rw [sub_nonneg, sq_le_sq, abs_of_pos hay, abs_of_pos h.2.1]
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.y a₁ ≤ Solution₁.y a
[PROOFSTEP]
exact h.y_le_y hax hay
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ 0 ≤ Solution₁.y (a * a₁⁻¹)
[PROOFSTEP]
simpa only [y_inv, mul_neg, y_mul, le_neg_add_iff_add_le, add_zero] using h.x_mul_y_le_y_mul_x hax hay
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ 0 < Solution₁.x (a * a₁⁻¹)
[PROOFSTEP]
simp only [x_mul, x_inv, y_inv, mul_neg, lt_add_neg_iff_add_lt, zero_add]
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ d * (Solution₁.y a * Solution₁.y a₁) < Solution₁.x a * Solution₁.x a₁
[PROOFSTEP]
refine' (mul_lt_mul_left <| zero_lt_one.trans hax).mp _
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.x a * (d * (Solution₁.y a * Solution₁.y a₁)) < Solution₁.x a * (Solution₁.x a * Solution₁.x a₁)
[PROOFSTEP]
rw [(by ring : a.x * (d * (a.y * a₁.y)) = d * a.y * (a.x * a₁.y))]
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.x a * (d * (Solution₁.y a * Solution₁.y a₁)) = d * Solution₁.y a * (Solution₁.x a * Solution₁.y a₁)
[PROOFSTEP]
ring
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ d * Solution₁.y a * (Solution₁.x a * Solution₁.y a₁) < Solution₁.x a * (Solution₁.x a * Solution₁.x a₁)
[PROOFSTEP]
refine' ((mul_le_mul_left <| mul_pos h.d_pos hay).mpr <| x_mul_y_le_y_mul_x h hax hay).trans_lt _
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ d * Solution₁.y a * (Solution₁.y a * Solution₁.x a₁) < Solution₁.x a * (Solution₁.x a * Solution₁.x a₁)
[PROOFSTEP]
rw [← mul_assoc, mul_assoc d, ← sq, a.prop_y, ← sub_pos]
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ 0 < Solution₁.x a * (Solution₁.x a * Solution₁.x a₁) - (Solution₁.x a ^ 2 - 1) * Solution₁.x a₁
[PROOFSTEP]
ring_nf
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ 0 < Solution₁.x a₁
[PROOFSTEP]
exact zero_lt_one.trans h.1
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.x (a * a₁⁻¹) < Solution₁.x a
[PROOFSTEP]
simp only [x_mul, x_inv, y_inv, mul_neg, add_neg_lt_iff_le_add']
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.x a * Solution₁.x a₁ < d * (Solution₁.y a * Solution₁.y a₁) + Solution₁.x a
[PROOFSTEP]
refine' (mul_lt_mul_left h.2.1).mp _
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.y a₁ * (Solution₁.x a * Solution₁.x a₁) <
    Solution₁.y a₁ * (d * (Solution₁.y a * Solution₁.y a₁) + Solution₁.x a)
[PROOFSTEP]
rw [(by ring : a₁.y * (a.x * a₁.x) = a.x * a₁.y * a₁.x)]
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.y a₁ * (Solution₁.x a * Solution₁.x a₁) = Solution₁.x a * Solution₁.y a₁ * Solution₁.x a₁
[PROOFSTEP]
ring
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.x a * Solution₁.y a₁ * Solution₁.x a₁ <
    Solution₁.y a₁ * (d * (Solution₁.y a * Solution₁.y a₁) + Solution₁.x a)
[PROOFSTEP]
refine' ((mul_le_mul_right <| zero_lt_one.trans h.1).mpr <| x_mul_y_le_y_mul_x h hax hay).trans_lt _
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.y a * Solution₁.x a₁ * Solution₁.x a₁ <
    Solution₁.y a₁ * (d * (Solution₁.y a * Solution₁.y a₁) + Solution₁.x a)
[PROOFSTEP]
rw [mul_assoc, ← sq, a₁.prop_x, ← sub_neg]
  -- Porting note: was `ring_nf`
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.y a * (1 + d * Solution₁.y a₁ ^ 2) -
      Solution₁.y a₁ * (d * (Solution₁.y a * Solution₁.y a₁) + Solution₁.x a) <
    0
[PROOFSTEP]
suffices a.y - a.x * a₁.y < 0 by convert this using 1; ring
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
this : Solution₁.y a - Solution₁.x a * Solution₁.y a₁ < 0
⊢ Solution₁.y a * (1 + d * Solution₁.y a₁ ^ 2) -
      Solution₁.y a₁ * (d * (Solution₁.y a * Solution₁.y a₁) + Solution₁.x a) <
    0
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_3
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
this : Solution₁.y a - Solution₁.x a * Solution₁.y a₁ < 0
⊢ Solution₁.y a * (1 + d * Solution₁.y a₁ ^ 2) -
      Solution₁.y a₁ * (d * (Solution₁.y a * Solution₁.y a₁) + Solution₁.x a) =
    Solution₁.y a - Solution₁.x a * Solution₁.y a₁
[PROOFSTEP]
ring
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.y a - Solution₁.x a * Solution₁.y a₁ < 0
[PROOFSTEP]
rw [sub_neg, ← abs_of_pos hay, ← abs_of_pos h.2.1, ← abs_of_pos <| zero_lt_one.trans hax, ← abs_mul, ← sq_lt_sq,
  mul_pow, a.prop_x]
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ Solution₁.y a ^ 2 < (1 + d * Solution₁.y a ^ 2) * Solution₁.y a₁ ^ 2
[PROOFSTEP]
calc
  a.y ^ 2 = 1 * a.y ^ 2 := (one_mul _).symm
  _ ≤ d * a.y ^ 2 := ((mul_le_mul_right <| sq_pos_of_pos hay).mpr h.d_pos)
  _ < d * a.y ^ 2 + 1 := (lt_add_one _)
  _ = (1 + d * a.y ^ 2) * 1 := by rw [add_comm, mul_one]
  _ ≤ (1 + d * a.y ^ 2) * a₁.y ^ 2 := (mul_le_mul_left (by have := h.d_pos; positivity)).mpr (sq_pos_of_pos h.2.1)
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ d * Solution₁.y a ^ 2 + 1 = (1 + d * Solution₁.y a ^ 2) * 1
[PROOFSTEP]
rw [add_comm, mul_one]
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
⊢ 0 < 1 + d * Solution₁.y a ^ 2
[PROOFSTEP]
have := h.d_pos
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < Solution₁.x a
hay : 0 < Solution₁.y a
this : 0 < d
⊢ 0 < 1 + d * Solution₁.y a ^ 2
[PROOFSTEP]
positivity
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 0 < Solution₁.x a
hay : 0 ≤ Solution₁.y a
⊢ ∃ n, a = a₁ ^ n
[PROOFSTEP]
lift a.x to ℕ using hax.le with ax hax'
[GOAL]
case intro
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
ax : ℕ
hax' : ↑ax = Solution₁.x a
hax✝ hax : 0 < ↑ax
⊢ ∃ n, a = a₁ ^ n
[PROOFSTEP]
clear hax
[GOAL]
case intro
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
ax : ℕ
hax' : ↑ax = Solution₁.x a
hax : 0 < ↑ax
⊢ ∃ n, a = a₁ ^ n
[PROOFSTEP]
induction' ax using Nat.strong_induction_on with x ih generalizing a
[GOAL]
case intro.h
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
⊢ ∃ n, a = a₁ ^ n
[PROOFSTEP]
cases' hay.eq_or_lt with hy hy
[GOAL]
case intro.h.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 = Solution₁.y a
⊢ ∃ n, a = a₁ ^ n
[PROOFSTEP]
refine' ⟨0, _⟩
[GOAL]
case intro.h.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 = Solution₁.y a
⊢ a = a₁ ^ 0
[PROOFSTEP]
simp only [pow_zero]
[GOAL]
case intro.h.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 = Solution₁.y a
⊢ a = 1
[PROOFSTEP]
ext
[GOAL]
case intro.h.inl.hx
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 = Solution₁.y a
⊢ Solution₁.x a = Solution₁.x 1
[PROOFSTEP]
simp only [x_one, y_one]
[GOAL]
case intro.h.inl.hy
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 = Solution₁.y a
⊢ Solution₁.y a = Solution₁.y 1
[PROOFSTEP]
simp only [x_one, y_one]
[GOAL]
case intro.h.inl.hx
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 = Solution₁.y a
⊢ Solution₁.x a = 1
[PROOFSTEP]
have prop := a.prop
[GOAL]
case intro.h.inl.hx
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 = Solution₁.y a
prop : Solution₁.x a ^ 2 - d * Solution₁.y a ^ 2 = 1
⊢ Solution₁.x a = 1
[PROOFSTEP]
rw [← hy, sq (0 : ℤ), zero_mul, mul_zero, sub_zero, sq_eq_one_iff] at prop
[GOAL]
case intro.h.inl.hx
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 = Solution₁.y a
prop : Solution₁.x a = 1 ∨ Solution₁.x a = -1
⊢ Solution₁.x a = 1
[PROOFSTEP]
refine' prop.resolve_right fun hf => _
[GOAL]
case intro.h.inl.hx
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 = Solution₁.y a
prop : Solution₁.x a = 1 ∨ Solution₁.x a = -1
hf : Solution₁.x a = -1
⊢ False
[PROOFSTEP]
have := (hax.trans_eq hax').le.trans_eq hf
[GOAL]
case intro.h.inl.hx
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 = Solution₁.y a
prop : Solution₁.x a = 1 ∨ Solution₁.x a = -1
hf : Solution₁.x a = -1
this : 0 ≤ -1
⊢ False
[PROOFSTEP]
norm_num at this
[GOAL]
case intro.h.inl.hy
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 = Solution₁.y a
⊢ Solution₁.y a = 0
[PROOFSTEP]
exact hy.symm
[GOAL]
case intro.h.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 < Solution₁.y a
⊢ ∃ n, a = a₁ ^ n
[PROOFSTEP]
have hx₁ : 1 < a.x := by nlinarith [a.prop, h.d_pos]
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 < Solution₁.y a
⊢ 1 < Solution₁.x a
[PROOFSTEP]
nlinarith [a.prop, h.d_pos]
[GOAL]
case intro.h.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 < Solution₁.y a
hx₁ : 1 < Solution₁.x a
⊢ ∃ n, a = a₁ ^ n
[PROOFSTEP]
have hxx₁ := h.mul_inv_x_pos hx₁ hy
[GOAL]
case intro.h.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 < Solution₁.y a
hx₁ : 1 < Solution₁.x a
hxx₁ : 0 < Solution₁.x (a * a₁⁻¹)
⊢ ∃ n, a = a₁ ^ n
[PROOFSTEP]
have hxx₂ := h.mul_inv_x_lt_x hx₁ hy
[GOAL]
case intro.h.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 < Solution₁.y a
hx₁ : 1 < Solution₁.x a
hxx₁ : 0 < Solution₁.x (a * a₁⁻¹)
hxx₂ : Solution₁.x (a * a₁⁻¹) < Solution₁.x a
⊢ ∃ n, a = a₁ ^ n
[PROOFSTEP]
have hyy := h.mul_inv_y_nonneg hx₁ hy
[GOAL]
case intro.h.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 < Solution₁.y a
hx₁ : 1 < Solution₁.x a
hxx₁ : 0 < Solution₁.x (a * a₁⁻¹)
hxx₂ : Solution₁.x (a * a₁⁻¹) < Solution₁.x a
hyy : 0 ≤ Solution₁.y (a * a₁⁻¹)
⊢ ∃ n, a = a₁ ^ n
[PROOFSTEP]
lift (a * a₁⁻¹).x to ℕ using hxx₁.le with x' hx'
[GOAL]
case intro.h.inr.intro
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 < Solution₁.y a
hx₁ : 1 < Solution₁.x a
hyy : 0 ≤ Solution₁.y (a * a₁⁻¹)
x' : ℕ
hx' : ↑x' = Solution₁.x (a * a₁⁻¹)
hxx₁✝ hxx₁ : 0 < ↑x'
hxx₂✝ hxx₂ : ↑x' < Solution₁.x a
⊢ ∃ n, a = a₁ ^ n
[PROOFSTEP]
obtain ⟨n, hn⟩ := ih x' (by exact_mod_cast hxx₂.trans_eq hax'.symm) hyy hx' hxx₁
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 < Solution₁.y a
hx₁ : 1 < Solution₁.x a
hyy : 0 ≤ Solution₁.y (a * a₁⁻¹)
x' : ℕ
hx' : ↑x' = Solution₁.x (a * a₁⁻¹)
hxx₁✝ hxx₁ : 0 < ↑x'
hxx₂✝ hxx₂ : ↑x' < Solution₁.x a
⊢ x' < x
[PROOFSTEP]
exact_mod_cast hxx₂.trans_eq hax'.symm
[GOAL]
case intro.h.inr.intro.intro
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 < Solution₁.y a
hx₁ : 1 < Solution₁.x a
hyy : 0 ≤ Solution₁.y (a * a₁⁻¹)
x' : ℕ
hx' : ↑x' = Solution₁.x (a * a₁⁻¹)
hxx₁✝ hxx₁ : 0 < ↑x'
hxx₂✝ hxx₂ : ↑x' < Solution₁.x a
n : ℕ
hn : a * a₁⁻¹ = a₁ ^ n
⊢ ∃ n, a = a₁ ^ n
[PROOFSTEP]
exact ⟨n + 1, by rw [pow_succ, ← hn, mul_comm a, ← mul_assoc, mul_inv_self, one_mul]⟩
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a✝ : Solution₁ d
hay✝ : 0 ≤ Solution₁.y a✝
ax : ℕ
hax'✝ : ↑ax = Solution₁.x a✝
hax✝ : 0 < ↑ax
x : ℕ
ih : ∀ (m : ℕ), m < x → ∀ {a : Solution₁ d}, 0 ≤ Solution₁.y a → ↑m = Solution₁.x a → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ Solution₁.y a
hax' : ↑x = Solution₁.x a
hax : 0 < ↑x
hy : 0 < Solution₁.y a
hx₁ : 1 < Solution₁.x a
hyy : 0 ≤ Solution₁.y (a * a₁⁻¹)
x' : ℕ
hx' : ↑x' = Solution₁.x (a * a₁⁻¹)
hxx₁✝ hxx₁ : 0 < ↑x'
hxx₂✝ hxx₂ : ↑x' < Solution₁.x a
n : ℕ
hn : a * a₁⁻¹ = a₁ ^ n
⊢ a = a₁ ^ (n + 1)
[PROOFSTEP]
rw [pow_succ, ← hn, mul_comm a, ← mul_assoc, mul_inv_self, one_mul]
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
[PROOFSTEP]
obtain ⟨b, hbx, hby, hb⟩ := exists_pos_variant h.d_pos a
[GOAL]
case intro.intro.intro
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < Solution₁.x b
hby : 0 ≤ Solution₁.y b
hb : a ∈ {b, b⁻¹, -b, -b⁻¹}
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
[PROOFSTEP]
obtain ⟨n, hn⟩ := h.eq_pow_of_nonneg hbx hby
[GOAL]
case intro.intro.intro.intro
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < Solution₁.x b
hby : 0 ≤ Solution₁.y b
hb : a ∈ {b, b⁻¹, -b, -b⁻¹}
n : ℕ
hn : b = a₁ ^ n
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
[PROOFSTEP]
rcases hb with (rfl | rfl | rfl | hb)
[GOAL]
case intro.intro.intro.intro.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
n : ℕ
hbx : 0 < Solution₁.x a
hby : 0 ≤ Solution₁.y a
hn : a = a₁ ^ n
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
[PROOFSTEP]
exact ⟨n, Or.inl (by exact_mod_cast hn)⟩
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
n : ℕ
hbx : 0 < Solution₁.x a
hby : 0 ≤ Solution₁.y a
hn : a = a₁ ^ n
⊢ a = a₁ ^ ↑n
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
case intro.intro.intro.intro.inr.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < Solution₁.x b
hby : 0 ≤ Solution₁.y b
n : ℕ
hn : b = a₁ ^ n
⊢ ∃ n, b⁻¹ = a₁ ^ n ∨ b⁻¹ = -a₁ ^ n
[PROOFSTEP]
exact ⟨-n, Or.inl (by simp [hn])⟩
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < Solution₁.x b
hby : 0 ≤ Solution₁.y b
n : ℕ
hn : b = a₁ ^ n
⊢ b⁻¹ = a₁ ^ (-↑n)
[PROOFSTEP]
simp [hn]
[GOAL]
case intro.intro.intro.intro.inr.inr.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < Solution₁.x b
hby : 0 ≤ Solution₁.y b
n : ℕ
hn : b = a₁ ^ n
⊢ ∃ n, -b = a₁ ^ n ∨ -b = -a₁ ^ n
[PROOFSTEP]
exact ⟨n, Or.inr (by simp [hn])⟩
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
b : Solution₁ d
hbx : 0 < Solution₁.x b
hby : 0 ≤ Solution₁.y b
n : ℕ
hn : b = a₁ ^ n
⊢ -b = -a₁ ^ ↑n
[PROOFSTEP]
simp [hn]
[GOAL]
case intro.intro.intro.intro.inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < Solution₁.x b
hby : 0 ≤ Solution₁.y b
n : ℕ
hn : b = a₁ ^ n
hb : a ∈ {-b⁻¹}
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
[PROOFSTEP]
rw [Set.mem_singleton_iff] at hb
[GOAL]
case intro.intro.intro.intro.inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < Solution₁.x b
hby : 0 ≤ Solution₁.y b
n : ℕ
hn : b = a₁ ^ n
hb : a = -b⁻¹
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
[PROOFSTEP]
rw [hb]
[GOAL]
case intro.intro.intro.intro.inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < Solution₁.x b
hby : 0 ≤ Solution₁.y b
n : ℕ
hn : b = a₁ ^ n
hb : a = -b⁻¹
⊢ ∃ n, -b⁻¹ = a₁ ^ n ∨ -b⁻¹ = -a₁ ^ n
[PROOFSTEP]
exact ⟨-n, Or.inr (by simp [hn])⟩
[GOAL]
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < Solution₁.x b
hby : 0 ≤ Solution₁.y b
n : ℕ
hn : b = a₁ ^ n
hb : a = -b⁻¹
⊢ -b⁻¹ = -a₁ ^ (-↑n)
[PROOFSTEP]
simp [hn]
[GOAL]
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
⊢ ∃! a₁, 1 < Solution₁.x a₁ ∧ 0 < Solution₁.y a₁ ∧ ∀ (a : Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
[PROOFSTEP]
obtain ⟨a₁, ha₁⟩ := IsFundamental.exists_of_not_isSquare h₀ hd
[GOAL]
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
⊢ ∃! a₁, 1 < Solution₁.x a₁ ∧ 0 < Solution₁.y a₁ ∧ ∀ (a : Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
[PROOFSTEP]
refine' ⟨a₁, ⟨ha₁.1, ha₁.2.1, ha₁.eq_zpow_or_neg_zpow⟩, fun a (H : 1 < _ ∧ _) => _⟩
[GOAL]
case intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
a : Solution₁ d
H : 1 < Solution₁.x a ∧ 0 < Solution₁.y a ∧ ∀ (a_1 : Solution₁ d), ∃ n, a_1 = a ^ n ∨ a_1 = -a ^ n
⊢ a = a₁
[PROOFSTEP]
obtain ⟨Hx, Hy, H⟩ := H
[GOAL]
case intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
a : Solution₁ d
Hx : 1 < Solution₁.x a
Hy : 0 < Solution₁.y a
H : ∀ (a_1 : Solution₁ d), ∃ n, a_1 = a ^ n ∨ a_1 = -a ^ n
⊢ a = a₁
[PROOFSTEP]
obtain ⟨n₁, hn₁⟩ := H a₁
[GOAL]
case intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
a : Solution₁ d
Hx : 1 < Solution₁.x a
Hy : 0 < Solution₁.y a
H : ∀ (a_1 : Solution₁ d), ∃ n, a_1 = a ^ n ∨ a_1 = -a ^ n
n₁ : ℤ
hn₁ : a₁ = a ^ n₁ ∨ a₁ = -a ^ n₁
⊢ a = a₁
[PROOFSTEP]
obtain ⟨n₂, hn₂⟩ := ha₁.eq_zpow_or_neg_zpow a
[GOAL]
case intro.intro.intro.intro.intro
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
a : Solution₁ d
Hx : 1 < Solution₁.x a
Hy : 0 < Solution₁.y a
H : ∀ (a_1 : Solution₁ d), ∃ n, a_1 = a ^ n ∨ a_1 = -a ^ n
n₁ : ℤ
hn₁ : a₁ = a ^ n₁ ∨ a₁ = -a ^ n₁
n₂ : ℤ
hn₂ : a = a₁ ^ n₂ ∨ a = -a₁ ^ n₂
⊢ a = a₁
[PROOFSTEP]
rcases hn₂ with (rfl | rfl)
[GOAL]
case intro.intro.intro.intro.intro.inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < Solution₁.x (a₁ ^ n₂)
Hy : 0 < Solution₁.y (a₁ ^ n₂)
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ = (a₁ ^ n₂) ^ n₁ ∨ a₁ = -(a₁ ^ n₂) ^ n₁
⊢ a₁ ^ n₂ = a₁
[PROOFSTEP]
rw [← zpow_mul, eq_comm, @eq_comm _ a₁, ← mul_inv_eq_one, ← @mul_inv_eq_one _ _ _ a₁, ← zpow_neg_one, neg_mul, ←
  zpow_add, ← sub_eq_add_neg] at hn₁
[GOAL]
case intro.intro.intro.intro.intro.inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < Solution₁.x (a₁ ^ n₂)
Hy : 0 < Solution₁.y (a₁ ^ n₂)
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁✝ : a₁ ^ (n₂ * n₁) = a₁ ∨ -a₁ ^ (n₂ * n₁) = a₁
hn₁ : a₁ ^ (n₂ * n₁ - 1) = 1 ∨ -a₁ ^ (n₂ * n₁ - 1) = 1
⊢ a₁ ^ n₂ = a₁
[PROOFSTEP]
cases' hn₁ with hn₁ hn₁
[GOAL]
case intro.intro.intro.intro.intro.inl.inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < Solution₁.x (a₁ ^ n₂)
Hy : 0 < Solution₁.y (a₁ ^ n₂)
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁✝ : a₁ ^ (n₂ * n₁) = a₁ ∨ -a₁ ^ (n₂ * n₁) = a₁
hn₁ : a₁ ^ (n₂ * n₁ - 1) = 1
⊢ a₁ ^ n₂ = a₁
[PROOFSTEP]
rcases Int.isUnit_iff.mp (isUnit_of_mul_eq_one _ _ <| sub_eq_zero.mp <| (ha₁.zpow_eq_one_iff (n₂ * n₁ - 1)).mp hn₁) with
  (rfl | rfl)
[GOAL]
case intro.intro.intro.intro.intro.inl.inl.inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < Solution₁.x (a₁ ^ 1)
Hy : 0 < Solution₁.y (a₁ ^ 1)
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ 1) ^ n ∨ a = -(a₁ ^ 1) ^ n
hn₁✝ : a₁ ^ (1 * n₁) = a₁ ∨ -a₁ ^ (1 * n₁) = a₁
hn₁ : a₁ ^ (1 * n₁ - 1) = 1
⊢ a₁ ^ 1 = a₁
[PROOFSTEP]
rw [zpow_one]
[GOAL]
case intro.intro.intro.intro.intro.inl.inl.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < Solution₁.x (a₁ ^ (-1))
Hy : 0 < Solution₁.y (a₁ ^ (-1))
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ (-1)) ^ n ∨ a = -(a₁ ^ (-1)) ^ n
hn₁✝ : a₁ ^ (-1 * n₁) = a₁ ∨ -a₁ ^ (-1 * n₁) = a₁
hn₁ : a₁ ^ (-1 * n₁ - 1) = 1
⊢ a₁ ^ (-1) = a₁
[PROOFSTEP]
rw [zpow_neg_one, y_inv, lt_neg, neg_zero] at Hy
[GOAL]
case intro.intro.intro.intro.intro.inl.inl.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < Solution₁.x (a₁ ^ (-1))
Hy : Solution₁.y a₁ < 0
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ (-1)) ^ n ∨ a = -(a₁ ^ (-1)) ^ n
hn₁✝ : a₁ ^ (-1 * n₁) = a₁ ∨ -a₁ ^ (-1 * n₁) = a₁
hn₁ : a₁ ^ (-1 * n₁ - 1) = 1
⊢ a₁ ^ (-1) = a₁
[PROOFSTEP]
exact False.elim (lt_irrefl _ <| ha₁.2.1.trans Hy)
[GOAL]
case intro.intro.intro.intro.intro.inl.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < Solution₁.x (a₁ ^ n₂)
Hy : 0 < Solution₁.y (a₁ ^ n₂)
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁✝ : a₁ ^ (n₂ * n₁) = a₁ ∨ -a₁ ^ (n₂ * n₁) = a₁
hn₁ : -a₁ ^ (n₂ * n₁ - 1) = 1
⊢ a₁ ^ n₂ = a₁
[PROOFSTEP]
rw [← zpow_zero a₁, eq_comm] at hn₁
[GOAL]
case intro.intro.intro.intro.intro.inl.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < Solution₁.x (a₁ ^ n₂)
Hy : 0 < Solution₁.y (a₁ ^ n₂)
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁✝ : a₁ ^ (n₂ * n₁) = a₁ ∨ -a₁ ^ (n₂ * n₁) = a₁
hn₁ : a₁ ^ 0 = -a₁ ^ (n₂ * n₁ - 1)
⊢ a₁ ^ n₂ = a₁
[PROOFSTEP]
exact False.elim (ha₁.zpow_ne_neg_zpow hn₁)
[GOAL]
case intro.intro.intro.intro.intro.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < Solution₁.x (-a₁ ^ n₂)
Hy : 0 < Solution₁.y (-a₁ ^ n₂)
H : ∀ (a : Solution₁ d), ∃ n, a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ -a₁ ^ n₂ = a₁
[PROOFSTEP]
rw [x_neg, lt_neg] at Hx
[GOAL]
case intro.intro.intro.intro.intro.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : Solution₁.x (a₁ ^ n₂) < -1
Hy : 0 < Solution₁.y (-a₁ ^ n₂)
H : ∀ (a : Solution₁ d), ∃ n, a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ -a₁ ^ n₂ = a₁
[PROOFSTEP]
have := (x_zpow_pos (zero_lt_one.trans ha₁.1) n₂).trans Hx
[GOAL]
case intro.intro.intro.intro.intro.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : Solution₁.x (a₁ ^ n₂) < -1
Hy : 0 < Solution₁.y (-a₁ ^ n₂)
H : ∀ (a : Solution₁ d), ∃ n, a = (-a₁ ^ n₂) ^ n ∨ a = -(-a₁ ^ n₂) ^ n
hn₁ : a₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
this : 0 < -1
⊢ -a₁ ^ n₂ = a₁
[PROOFSTEP]
norm_num at this
[GOAL]
d : ℤ
a : Solution₁ d
⊢ (1 < Solution₁.x a ∧ 0 < Solution₁.y a ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n) ↔ IsFundamental a
[PROOFSTEP]
refine' ⟨fun h => _, fun H => ⟨H.1, H.2.1, H.eq_zpow_or_neg_zpow⟩⟩
[GOAL]
d : ℤ
a : Solution₁ d
h : 1 < Solution₁.x a ∧ 0 < Solution₁.y a ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
⊢ IsFundamental a
[PROOFSTEP]
have h₀ := d_pos_of_one_lt_x h.1
[GOAL]
d : ℤ
a : Solution₁ d
h : 1 < Solution₁.x a ∧ 0 < Solution₁.y a ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
⊢ IsFundamental a
[PROOFSTEP]
have hd := d_nonsquare_of_one_lt_x h.1
[GOAL]
d : ℤ
a : Solution₁ d
h : 1 < Solution₁.x a ∧ 0 < Solution₁.y a ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
⊢ IsFundamental a
[PROOFSTEP]
obtain ⟨a₁, ha₁⟩ := IsFundamental.exists_of_not_isSquare h₀ hd
[GOAL]
case intro
d : ℤ
a : Solution₁ d
h : 1 < Solution₁.x a ∧ 0 < Solution₁.y a ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
⊢ IsFundamental a
[PROOFSTEP]
obtain ⟨b, -, hb₂⟩ := existsUnique_pos_generator h₀ hd
[GOAL]
case intro.intro.intro
d : ℤ
a : Solution₁ d
h : 1 < Solution₁.x a ∧ 0 < Solution₁.y a ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
b : Solution₁ d
hb₂ :
  ∀ (y : Solution₁ d),
    (fun a₁ => 1 < Solution₁.x a₁ ∧ 0 < Solution₁.y a₁ ∧ ∀ (a : Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n) y → y = b
⊢ IsFundamental a
[PROOFSTEP]
rwa [hb₂ a h, ← hb₂ a₁ ⟨ha₁.1, ha₁.2.1, ha₁.eq_zpow_or_neg_zpow⟩]