awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ (x' : ℕ), 1 < x' ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑x' : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1
x₁ : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P
hx :
  1 <
    Nat.find (p := fun (n : ℕ) ↦
      1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ :
  HPow.hPow (α := ℤ) (β := ℕ)
        (↑(Nat.find (p := fun (n : ℕ) ↦
              1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
              P) :
          ℤ)
        2 -
      d * HPow.hPow (β := ℕ) y₁ 2 =
    1
b : Solution₁ d
hb' : b.x = (↑b.x.toNat : ℤ)
hb'' : 1 < b.x
hb : 1 < b.x.toNat
⊢ x₁ ≤ b.x.toNat

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

Premises used: Iff.mpr, abs, abs_pos, Pell.Solution₁.y, Nat.find_min', And.intro, Exists.intro, Pell.Solution₁.y_ne_zero_of_one_lt_x
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ (x' : ℕ), 1 < x' ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑x' : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1
x₁ : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P
hx :
  1 <
    Nat.find (p := fun (n : ℕ) ↦
      1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ :
  HPow.hPow (α := ℤ) (β := ℕ)
        (↑(Nat.find (p := fun (n : ℕ) ↦
              1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
              P) :
          ℤ)
        2 -
      d * HPow.hPow (β := ℕ) y₁ 2 =
    1
b : Solution₁ d
hb' : b.x = (↑b.x.toNat : ℤ)
hb'' : 1 < b.x
hb : 1 < b.x.toNat
refine : HPow.hPow (α := ℤ) (β := ℕ) (↑b.x.toNat : ℤ) 2 - d * HPow.hPow (β := ℕ) |b.y| 2 = 1
⊢ x₁ ≤ b.x.toNat

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

Premises used: Iff.mpr, abs, abs_pos, Pell.Solution₁.y, Nat.find_min', And.intro, Exists.intro, Pell.Solution₁.y_ne_zero_of_one_lt_x
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ (x' : ℕ), 1 < x' ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑x' : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1
x₁ : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P
hx :
  1 <
    Nat.find (p := fun (n : ℕ) ↦
      1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ :
  HPow.hPow (α := ℤ) (β := ℕ)
        (↑(Nat.find (p := fun (n : ℕ) ↦
              1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
              P) :
          ℤ)
        2 -
      d * HPow.hPow (β := ℕ) y₁ 2 =
    1
b : Solution₁ d
hb' : b.x = (↑b.x.toNat : ℤ)
hb'' : 1 < b.x
hb : 1 < b.x.toNat
rw : HPow.hPow (β := ℕ) b.x 2 - d * HPow.hPow (β := ℕ) b.y 2 = 1
⊢ HPow.hPow (α := ℤ) (β := ℕ) (↑b.x.toNat : ℤ) 2 - d * HPow.hPow (β := ℕ) |b.y| 2 = 1

Tactic:
rw [← hb', sq_abs]

Premises used: sq_abs
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ (x' : ℕ), 1 < x' ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑x' : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1
x₁ : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P
hx :
  1 <
    Nat.find (p := fun (n : ℕ) ↦
      1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ :
  HPow.hPow (α := ℤ) (β := ℕ)
        (↑(Nat.find (p := fun (n : ℕ) ↦
              1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
              P) :
          ℤ)
        2 -
      d * HPow.hPow (β := ℕ) y₁ 2 =
    1
b : Solution₁ d
hb' : b.x = (↑b.x.toNat : ℤ)
hb'' : 1 < b.x
hb : 1 < b.x.toNat
⊢ HPow.hPow (β := ℕ) b.x 2 - d * HPow.hPow (β := ℕ) b.y 2 = 1

Tactic:
b.prop

Premises used: Pell.Solution₁.prop
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ (x' : ℕ), 1 < x' ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑x' : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1
x₁ : ℕ :=
  Nat.find (p := fun (n : ℕ) ↦
    1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P
hx :
  1 <
    Nat.find (p := fun (n : ℕ) ↦
      1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1) P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ :
  HPow.hPow (α := ℤ) (β := ℕ)
        (↑(Nat.find (p := fun (n : ℕ) ↦
              1 < n ∧ ∃ (y' : ℤ), 0 < y' ∧ HPow.hPow (α := ℤ) (β := ℕ) (↑n : ℤ) 2 - d * HPow.hPow (β := ℕ) y' 2 = 1)
              P) :
          ℤ)
        2 -
      d * HPow.hPow (β := ℕ) y₁ 2 =
    1
b : Solution₁ d
hb' : b.x = (↑b.x.toNat : ℤ)
hb'' : 1 < b.x
hb : 1 < b.x.toNat
⊢ HPow.hPow (β := ℕ) b.x 2 - d * HPow.hPow (β := ℕ) b.y 2 = 1

Tactic:
exact b.prop

Premises used: Pell.Solution₁.prop
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
rw : 0 < (a ^ n).x * a.y + ((a ^ n).y * a.x - (a ^ n).y)
⊢ (a ^ n).y < (a ^ (n + 1)).y

Tactic:
rw [← sub_pos, zpow_add, zpow_one, y_mul, add_sub_assoc]

Premises used: sub_pos, add_sub_assoc, zpow_add, zpow_one, Pell.Solution₁.y_mul
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ (a ^ n).y * a.x - (a ^ n).y = (a ^ n).y * (a.x - 1)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
rw : 0 < (a ^ n).x * a.y + (a ^ n).y * (a.x - 1)
⊢ 0 < (a ^ n).x * a.y + ((a ^ n).y * a.x - (a ^ n).y)

Tactic:
rw [show (a ^ n).y * a.x - (a ^ n).y = (a ^ n).y * (a.x - 1) by ring]
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
rw : 1 ≤ a.x
⊢ 0 ≤ a.x - 1

Tactic:
rw [sub_nonneg]

Premises used: sub_nonneg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 1 ≤ a.x

Tactic:
h.1.le

Premises used: LT.lt.le, And.left
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 1 ≤ a.x

Tactic:
exact h.1.le

Premises used: LT.lt.le, And.left
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
add_pos_of_pos_of_nonneg : 0 ≤ (a ^ n).y
⊢ 0 < (a ^ n).x * a.y + (a ^ n).y * (a.x - 1)

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

Premises used: mul_nonneg, mul_pos, Pell.IsFundamental.x_pos, And.right, And.left, add_pos_of_pos_of_nonneg, Pell.Solution₁.x_zpow_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
inl : ∀ (hn : LE.le (α := ℤ) 0 0), 0 ≤ (HPow.hPow (β := ℤ) a 0).y
inr : ∀ (hn : 0 < n), 0 ≤ (a ^ n).y
⊢ 0 ≤ (a ^ n).y

Tactic:
rcases hn.eq_or_lt with (rfl | hn)

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
hn : LE.le (α := ℤ) 0 0
⊢ 0 ≤ (HPow.hPow (β := ℤ) a 0).y

Tactic:
simp only [zpow_zero, y_one, le_refl]

Premises used: le_refl, zpow_zero, Pell.Solution₁.y_one
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn_1 : 0 ≤ n
hn : 0 < n
⊢ 0 ≤ (a ^ n).y

Tactic:
(y_zpow_pos h.x_pos h.2.1 hn).le

Premises used: Pell.Solution₁.y_zpow_pos, LT.lt.le, Pell.IsFundamental.x_pos, And.right, And.left
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn_1 : 0 ≤ n
hn : 0 < n
⊢ 0 ≤ (a ^ n).y

Tactic:
exact (y_zpow_pos h.x_pos h.2.1 hn).le

Premises used: Pell.Solution₁.y_zpow_pos, LT.lt.le, Pell.IsFundamental.x_pos, And.right, And.left
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
⊢ ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y

Tactic:
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, le_refl]
    · exact (y_zpow_pos h.x_pos h.2.1 hn).le
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
⊢ StrictMono (β := ℤ) fun (n : ℤ) ↦ (a ^ n).y

Tactic:
strictMono_int_of_lt_succ fun n => ?_

Premises used: strictMono_int_of_lt_succ
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
refine : ∀ (n : ℤ), (a ^ n).y < (a ^ (n + 1)).y
⊢ StrictMono (β := ℤ) fun (n : ℤ) ↦ (a ^ n).y

Tactic:
refine strictMono_int_of_lt_succ fun n => ?_

Premises used: strictMono_int_of_lt_succ
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
inl : ∀ (hn : 0 ≤ n), (a ^ n).y < (a ^ (n + 1)).y
inr : ∀ (hn : n < 0), (a ^ n).y < (a ^ (n + 1)).y
⊢ (a ^ n).y < (a ^ (n + 1)).y

Tactic:
rcases le_or_gt 0 n with hn | hn

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
hn : 0 ≤ n
⊢ (a ^ n).y < (a ^ (n + 1)).y

Tactic:
H n hn
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
hn : 0 ≤ n
⊢ (a ^ n).y < (a ^ (n + 1)).y

Tactic:
exact H n hn
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
hn : n < 0
m : ℤ := -n - 1
⊢ n = -m - 1

Tactic:
simp only [m, neg_sub, sub_neg_eq_add, add_tsub_cancel_left]

Premises used: neg_sub, add_tsub_cancel_left, sub_neg_eq_add
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
hn : n < 0
m : ℤ := -n - 1
⊢ n = -m - 1

Tactic:
have hm : n = -m - 1 := by simp only [m, neg_sub, sub_neg_eq_add, add_tsub_cancel_left]
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
hn : n < 0
m : ℤ := -n - 1
hm : n = -m - 1
inr : (a ^ m).y < (a ^ (m + 1)).y
⊢ (a ^ n).y < (a ^ (n + 1)).y

Tactic:
rw [hm, sub_add_cancel, ← neg_add', zpow_neg, zpow_neg, y_inv, y_inv, neg_lt_neg_iff]

Premises used: neg_lt_neg_iff, Pell.Solution₁.y_inv, neg_add', zpow_neg, sub_add_cancel
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
hn : n < 0
m : ℤ := -n - 1
hm : n = -m - 1
⊢ 0 ≤ m

Tactic:
lia
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
hn : n < 0
m : ℤ := -n - 1
hm : n = -m - 1
⊢ (a ^ m).y < (a ^ (m + 1)).y

Tactic:
exact H _ (by lia)
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
⊢ (a ^ m).y < (a ^ n).y ↔ m < n

Tactic:
⟨fun H => ?_, fun H => h.y_strictMono H⟩

Premises used: Iff.intro, Pell.IsFundamental.y_strictMono
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
refine : ∀ (H : (a ^ m).y < (a ^ n).y), m < n
⊢ (a ^ m).y < (a ^ n).y ↔ m < n

Tactic:
refine ⟨fun H => ?_, fun H => h.y_strictMono H⟩
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
H : (a ^ m).y < (a ^ n).y
contrapose! : ∀ (H : n ≤ m), (a ^ n).y ≤ (a ^ m).y
⊢ m < n

Tactic:
contrapose! H
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
H : n ≤ m
⊢ (a ^ n).y ≤ (a ^ m).y

Tactic:
h.y_strictMono.monotone H

Premises used: StrictMono.monotone, Pell.IsFundamental.y_strictMono
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
m n : ℤ
H : n ≤ m
⊢ (a ^ n).y ≤ (a ^ m).y

Tactic:
exact h.y_strictMono.monotone H

Premises used: StrictMono.monotone, Pell.IsFundamental.y_strictMono
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
⊢ a ^ n = HPow.hPow (β := ℤ) a 0 ↔ n = 0

Tactic:
⟨fun H => h.y_strictMono.injective (congr_arg Solution₁.y H), fun H => H ▸ rfl⟩

Premises used: Eq.rec, congr_arg, StrictMono.injective, Pell.Solution₁.y, Iff.intro, Pell.IsFundamental.y_strictMono, rfl
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
⊢ a ^ n = HPow.hPow (β := ℤ) a 0 ↔ n = 0

Tactic:
exact ⟨fun H => h.y_strictMono.injective (congr_arg Solution₁.y H), fun H => H ▸ rfl⟩
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : a ^ n = -a ^ n'
⊢ (a ^ n).x = (-a ^ n').x

Tactic:
apply_fun Solution₁.x at hf

Premises used: Pell.Solution₁.x
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
⊢ 0 < (a ^ n).x

Tactic:
have H := x_zpow_pos h.x_pos n
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
H : 0 < (a ^ n).x
⊢ (a ^ n').x < 0

Tactic:
rw [hf, x_neg, lt_neg, neg_zero] at H

Premises used: lt_neg, Pell.Solution₁.x_neg, neg_zero
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
H : (a ^ n').x < 0
⊢ False

Tactic:
lt_irrefl _ ((x_zpow_pos h.x_pos n').trans H)

Premises used: lt_irrefl, Pell.IsFundamental.x_pos, LT.lt.trans, Pell.Solution₁.x_zpow_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n n' : ℤ
hf : (a ^ n).x = (-a ^ n').x
H : (a ^ n').x < 0
⊢ False

Tactic:
exact lt_irrefl _ ((x_zpow_pos h.x_pos n').trans H)

Premises used: lt_irrefl, Pell.IsFundamental.x_pos, LT.lt.trans, Pell.Solution₁.x_zpow_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
⊢ a₁.x ≤ a.x

Tactic:
h.2.2 hax

Premises used: And.right
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
rw :
  d * (HPow.hPow (β := ℕ) a₁.y 2 - HPow.hPow (β := ℕ) a.y 2) =
    1 + d * HPow.hPow (β := ℕ) a₁.y 2 - (1 + d * HPow.hPow (β := ℕ) a.y 2)
⊢ d * (HPow.hPow (β := ℕ) a₁.y 2 - HPow.hPow (β := ℕ) a.y 2) = HPow.hPow (β := ℕ) a₁.x 2 - HPow.hPow (β := ℕ) a.x 2

Tactic:
rw [a.prop_x, a₁.prop_x]

Premises used: Pell.Solution₁.prop_x
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * (HPow.hPow (β := ℕ) a₁.y 2 - HPow.hPow (β := ℕ) a.y 2) =
    1 + d * HPow.hPow (β := ℕ) a₁.y 2 - (1 + d * HPow.hPow (β := ℕ) a.y 2)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * (HPow.hPow (β := ℕ) a₁.y 2 - HPow.hPow (β := ℕ) a.y 2) = HPow.hPow (β := ℕ) a₁.x 2 - HPow.hPow (β := ℕ) a.x 2

Tactic:
have H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2 := by rw [a.prop_x, a₁.prop_x]; ring
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (HPow.hPow (β := ℕ) a₁.y 2 - HPow.hPow (β := ℕ) a.y 2) = HPow.hPow (β := ℕ) a₁.x 2 - HPow.hPow (β := ℕ) a.x 2
rw : a₁.x ≤ a.x
⊢ a₁.y ≤ a.y

Tactic:
rw [← abs_of_pos hay, ← abs_of_pos h.2.1, ← sq_le_sq, ← mul_le_mul_iff_right₀ 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)]

Premises used: mul_sub, sq_le_sq, zero_lt_one, Pell.IsFundamental.d_pos, And.right, And.left, LT.lt.trans, abs_of_pos, sub_nonpos, mul_le_mul_iff_right₀
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (HPow.hPow (β := ℕ) a₁.y 2 - HPow.hPow (β := ℕ) a.y 2) = HPow.hPow (β := ℕ) a₁.x 2 - HPow.hPow (β := ℕ) a.x 2
⊢ a₁.x ≤ a.x

Tactic:
h.x_le_x hax

Premises used: Pell.IsFundamental.x_le_x
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (HPow.hPow (β := ℕ) a₁.y 2 - HPow.hPow (β := ℕ) a.y 2) = HPow.hPow (β := ℕ) a₁.x 2 - HPow.hPow (β := ℕ) a.x 2
⊢ a₁.x ≤ a.x

Tactic:
exact h.x_le_x hax

Premises used: Pell.IsFundamental.x_le_x
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
rw :
  0 ≤
    HPow.hPow (β := ℕ) a.y 2 * (1 + d * HPow.hPow (β := ℕ) a₁.y 2) -
      (1 + d * HPow.hPow (β := ℕ) a.y 2) * HPow.hPow (β := ℕ) a₁.y 2
⊢ a.x * a₁.y ≤ a.y * a₁.x

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

Premises used: sq_le_sq, abs_mul, zero_lt_one, Pell.IsFundamental.x_pos, Pell.Solution₁.prop_x, And.right, And.left, LT.lt.trans, abs_of_pos, mul_pow, sub_nonneg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
ring_nf : 0 ≤ HPow.hPow (β := ℕ) a.y 2 - HPow.hPow (β := ℕ) a₁.y 2
⊢ 0 ≤
    HPow.hPow (β := ℕ) a.y 2 * (1 + d * HPow.hPow (β := ℕ) a₁.y 2) -
      (1 + d * HPow.hPow (β := ℕ) a.y 2) * HPow.hPow (β := ℕ) a₁.y 2

Tactic:
ring_nf
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
rw : a₁.y ≤ a.y
⊢ 0 ≤ HPow.hPow (β := ℕ) a.y 2 - HPow.hPow (β := ℕ) a₁.y 2

Tactic:
rw [sub_nonneg, sq_le_sq, abs_of_pos hay, abs_of_pos h.2.1]

Premises used: sq_le_sq, And.right, And.left, abs_of_pos, sub_nonneg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a₁.y ≤ a.y

Tactic:
h.y_le_y hax hay

Premises used: Pell.IsFundamental.y_le_y
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a₁.y ≤ a.y

Tactic:
exact h.y_le_y hax hay

Premises used: Pell.IsFundamental.y_le_y
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ 0 ≤ (a * a₁⁻¹).y

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

Premises used: Pell.IsFundamental.x_mul_y_le_y_mul_x, Pell.Solution₁.y_inv, Pell.Solution₁.y_mul, add_zero, le_neg_add_iff_add_le, mul_neg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
simp : d * (a.y * a₁.y) < a.x * a₁.x
⊢ 0 < (a * a₁⁻¹).x

Tactic:
simp only [x_mul, x_inv, y_inv, mul_neg, lt_add_neg_iff_add_lt, zero_add]

Premises used: lt_add_neg_iff_add_lt, Pell.Solution₁.x_mul, Pell.Solution₁.y_inv, zero_add, Pell.Solution₁.x_inv, mul_neg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * (a.y * a₁.y) < a.x * a₁.x

Tactic:
lt_of_mul_lt_mul_left ?_ <| zero_le_one.trans hax.le

Premises used: lt_of_mul_lt_mul_left, LT.lt.le, zero_le_one, LE.le.trans
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
refine : a.x * (d * (a.y * a₁.y)) < a.x * (a.x * a₁.x)
⊢ d * (a.y * a₁.y) < a.x * a₁.x

Tactic:
refine lt_of_mul_lt_mul_left ?_ <| zero_le_one.trans hax.le

Premises used: lt_of_mul_lt_mul_left, LT.lt.le, zero_le_one, LE.le.trans
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x * (d * (a.y * a₁.y)) = d * a.y * (a.x * a₁.y)

Tactic:
ring
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x * a₁.y ≤ a.y * a₁.x

Tactic:
have := x_mul_y_le_y_mul_x h hax hay
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
this : a.x * a₁.y ≤ a.y * a₁.x
⊢ 0 < d

Tactic:
have := h.d_pos
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
this_1 : a.x * a₁.y ≤ a.y * a₁.x
this : 0 < d
ha : 0 ≤ d * a.y
⊢ d * a.y * (a.x * a₁.y) ≤ d * a.y * (a.y * a₁.x)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
rw : d * a.y * (a.y * a₁.x) = d * HPow.hPow (β := ℕ) a.y 2 * a₁.x
⊢ d * a.y * (a.y * a₁.x) = (HPow.hPow (β := ℕ) a.x 2 - 1) * a₁.x

Tactic:
rw [← a.prop_y]

Premises used: Pell.Solution₁.prop_y
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * a.y * (a.y * a₁.x) = d * HPow.hPow (β := ℕ) a.y 2 * a₁.x

Tactic:
ring
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
linarith :
  a.x * (a.x * a₁.x) ≤ (HPow.hPow (β := ℕ) a.x 2 - 1) * a₁.x →
    HMul.hMul (α := ℤ) 2 (-1) + (a.x * (a.x * a₁.x) - (HPow.hPow (β := ℕ) a.x 2 - 1) * a₁.x) +
        (HAdd.hAdd (α := ℤ) 1 1 - a₁.x) =
      0
linarith₁ : a.x * (a.x * a₁.x) ≤ (HPow.hPow (β := ℕ) a.x 2 - 1) * a₁.x → GT.gt (α := ℤ) 2 0
⊢ (HPow.hPow (β := ℕ) a.x 2 - 1) * a₁.x < a.x * (a.x * a₁.x)

Tactic:
linarith [h.1]

Premises used: And.left
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
calc : a.x * (d * (a.y * a₁.y)) = d * a.y * (a.x * a₁.y)
calc₁ : d * a.y * (a.x * a₁.y) ≤ d * a.y * (a.y * a₁.x)
calc₂ : d * a.y * (a.y * a₁.x) = (HPow.hPow (β := ℕ) a.x 2 - 1) * a₁.x
calc₃ : (HPow.hPow (β := ℕ) a.x 2 - 1) * a₁.x < a.x * (a.x * a₁.x)
⊢ a.x * (d * (a.y * a₁.y)) < a.x * (a.x * a₁.x)

Tactic:
calc a.x * (d * (a.y * a₁.y))
    _ = d * a.y * (a.x * a₁.y) := by ring
    _ ≤ d * a.y * (a.y * a₁.x) := by have := x_mul_y_le_y_mul_x h hax hay; have := h.d_pos; gcongr
    _ = (a.x ^ 2 - 1) * a₁.x := by rw [← a.prop_y]; ring
    _ < a.x * (a.x * a₁.x) := by linarith [h.1]

Premises used: HMul.hMul, Pell.Solution₁.x, HSub.hSub, Pell.Solution₁.y, HPow.hPow, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
simp : a.x * a₁.x < d * (a.y * a₁.y) + a.x
⊢ (a * a₁⁻¹).x < a.x

Tactic:
simp only [x_mul, x_inv, y_inv, mul_neg, add_neg_lt_iff_le_add']

Premises used: Pell.Solution₁.x_mul, Pell.Solution₁.y_inv, add_neg_lt_iff_le_add', Pell.Solution₁.x_inv, mul_neg
-- Module: Mathlib.NumberTheory.Pell
Goal:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x * a₁.x < d * (a.y * a₁.y) + a.x

Tactic:
lt_of_mul_lt_mul_left ?_ h.2.1.le

Premises used: lt_of_mul_lt_mul_left, LT.lt.le, And.right, And.left