a : ℕ
a1 : 1 < a
n : ℕ
h : xn a1 n * 2 = xn a1 n * a + Pell.d a1 * yn a1 n
⊢ a = 2 ∧ n = 0
a : ℕ
a1 : 1 < a
n : ℕ
h : 2 * xn a1 n = xn a1 (n + 1)
⊢ a = 2 ∧ n = 0
rw [xn_succ, mul_comm] at h
a : ℕ
a1 : 1 < a
n : ℕ
h : xn a1 n * 2 = xn a1 n * a + Pell.d a1 * yn a1 n
this : n = 0
⊢ a = 2 ∧ n = 0
a : ℕ
a1 : 1 < a
n : ℕ
h : xn a1 n * 2 = xn a1 n * a + Pell.d a1 * yn a1 n
⊢ a = 2 ∧ n = 0
have : n = 0 :=
  n.eq_zero_or_pos.resolve_right fun np =>
    _root_.ne_of_lt
      (lt_of_le_of_lt (Nat.mul_le_mul_left _ a1)
        (Nat.lt_add_of_pos_right <| mul_pos (d_pos a1) (strictMono_y a1 np)))
      h
case refl
a : ℕ
a1 : 1 < a
h : xn a1 0 * 2 = xn a1 0 * a + Pell.d a1 * yn a1 0
⊢ a = 2 ∧ 0 = 0
a : ℕ
a1 : 1 < a
n : ℕ
h : xn a1 n * 2 = xn a1 n * a + Pell.d a1 * yn a1 n
this : n = 0
⊢ a = 2 ∧ n = 0
cases this
case refl
a : ℕ
a1 : 1 < a
h : 2 = a
⊢ a = 2 ∧ 0 = 0
case refl
a : ℕ
a1 : 1 < a
h : xn a1 0 * 2 = xn a1 0 * a + Pell.d a1 * yn a1 0
⊢ a = 2 ∧ 0 = 0
simp at h
no goals
case refl
a : ℕ
a1 : 1 < a
h : 2 = a
⊢ a = 2 ∧ 0 = 0
exact ⟨h.symm, rfl⟩