-- Mathlib/NumberTheory/Pell.lean
theorem y_strictMono {a : Solution₁ d} (h : IsFundamental a) :
    StrictMono fun n : ℤ => (a ^ n).y

Proof state:
case inl
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

Result:
no goals

Proof state:
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]

Result:
no goals

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 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]

Result:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 < (a ^ n).x * a.y + (a ^ n).y * (a.x - 1)

Proof state:
case inr
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
⊢ (a ^ n).y < (a ^ (n + 1)).y

Tactic:
have hm : n = -m - 1 := by simp only [m, neg_sub, sub_neg_eq_add, add_tsub_cancel_left]

Result:
case inr
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 ^ n).y < (a ^ (n + 1)).y

Proof state:
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:
omega

Result:
no goals

Proof state:
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

Result:
no goals

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 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))

Result:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 ≤ (a ^ n).y

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 ≤ a.x - 1

Tactic:
rw [sub_nonneg]

Result:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 1 ≤ a.x

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 ≤ (a ^ n).y

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

Result:
case inl
d : ℤ
a : Solution₁ d
h : IsFundamental a
hn : 0 ≤ 0
⊢ 0 ≤ (a ^ 0).y

case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn✝ : 0 ≤ n
hn : 0 < n
⊢ 0 ≤ (a ^ n).y

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
⊢ (a ^ n).y < (a ^ (n + 1)).y

Tactic:
rcases le_or_lt 0 n with hn | hn

Result:
case inl
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

case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
hn : n < 0
⊢ (a ^ n).y < (a ^ (n + 1)).y

Proof state:
case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
hn : n < 0
⊢ (a ^ n).y < (a ^ (n + 1)).y

Tactic:
let m : ℤ := -n - 1

Result:
case inr
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
⊢ (a ^ n).y < (a ^ (n + 1)).y

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 1 ≤ a.x

Tactic:
exact h.1.le

Result:
no goals

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
⊢ ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y

Tactic:
intro n hn

Result:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ (a ^ n).y < (a ^ (n + 1)).y

Proof state:
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:
refine strictMono_int_of_lt_succ fun n => ?_

Result:
d : ℤ
a : Solution₁ d
h : IsFundamental a
H : ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y
n : ℤ
⊢ (a ^ n).y < (a ^ (n + 1)).y

Proof state:
case inr
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn✝ : 0 ≤ n
hn : 0 < n
⊢ 0 ≤ (a ^ n).y

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

Result:
no goals

Proof state:
case inr
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 ^ 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]

Result:
case inr
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

Proof state:
case inr
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 omega)

Result:
no goals

Proof state:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ (a ^ n).y < (a ^ (n + 1)).y

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

Result:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 < (a ^ n).x * a.y + ((a ^ n).y * a.x - (a ^ n).y)

Proof state:
case inl
d : ℤ
a : Solution₁ d
h : IsFundamental a
hn : 0 ≤ 0
⊢ 0 ≤ (a ^ 0).y

Tactic:
simp only [zpow_zero, y_one, le_refl]

Result:
no goals