awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
a1p : LE.le (α := ℤ√(↑(d a1) : ℤ)) 0 { re := (↑a : ℤ), im := 1 }
am1p : LE.le (α := ℤ√(↑(d a1) : ℤ)) 0 { re := (↑a : ℤ), im := -1 }
a1m :
  HMul.hMul (α := ℤ√(↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) }
      { re := (↑a : ℤ), im := -1 : ℤ√(↑(d a1) : ℤ) } =
    1
x y : ℤ
h1 : LE.le (α := ℤ√(↑(d a1) : ℤ)) 1 { re := x, im := y }
hp : IsPell (d := (↑(d a1) : ℤ)) { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬LE.le (α := ℤ√(↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 } { re := x, im := y }
h1l : LT.lt (α := ℤ√(↑(d a1) : ℤ)) 1 { re := x, im := y }
bm :
  HMul.hMul (α := ℤ√(↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) }
      { re := Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) },
        im := -Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) } : ℤ√(↑(d a1) : ℤ) } =
    1
y0l : LT.lt (α := ℤ√(↑(d a1) : ℤ)) 0 { re := x - x, im := y - -y }
⊢ LT.lt (α := ℤ√(↑(d a1) : ℤ))
    {
      re :=
        Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) } +
          Zsqrtd.re (d := (↑(d a1) : ℤ)) (-{ re := x, im := -y : ℤ√(↑(d a1) : ℤ) }),
      im :=
        Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) } +
          Zsqrtd.im (d := (↑(d a1) : ℤ)) (-{ re := x, im := -y : ℤ√(↑(d a1) : ℤ) }) }
    {
      re :=
        Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) } +
          Zsqrtd.re (d := (↑(d a1) : ℤ)) (-{ re := (↑a : ℤ), im := -1 : ℤ√(↑(d a1) : ℤ) }),
      im :=
        Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) } +
          Zsqrtd.im (d := (↑(d a1) : ℤ)) (-{ re := (↑a : ℤ), im := -1 : ℤ√(↑(d a1) : ℤ) }) }

Tactic:
have yl2 : (⟨_, _⟩ : ℤ√_) < ⟨_, _⟩ :=
          show (⟨x, y⟩ - ⟨x, -y⟩ : ℤ√d a1) < ⟨a, 1⟩ - ⟨a, -1⟩ from
            sub_lt_sub ha fun hn : (⟨x, -y⟩ : ℤ√d a1) ≤ ⟨a, -1⟩ => by
              have t := mul_le_mul_of_nonneg_right
                      (mul_le_mul_of_nonneg_left hn (le_trans zero_le_one h1)) a1p
              rw [bm, one_mul, mul_assoc, Eq.trans (mul_comm _ _) a1m, mul_one] at t
              exact ha t
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
a1p : LE.le (α := ℤ√(↑(d a1) : ℤ)) 0 { re := (↑a : ℤ), im := 1 }
am1p : LE.le (α := ℤ√(↑(d a1) : ℤ)) 0 { re := (↑a : ℤ), im := -1 }
a1m :
  HMul.hMul (α := ℤ√(↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) }
      { re := (↑a : ℤ), im := -1 : ℤ√(↑(d a1) : ℤ) } =
    1
x y : ℤ
h1 : LE.le (α := ℤ√(↑(d a1) : ℤ)) 1 { re := x, im := y }
hp : IsPell (d := (↑(d a1) : ℤ)) { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬LE.le (α := ℤ√(↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 } { re := x, im := y }
h1l : LT.lt (α := ℤ√(↑(d a1) : ℤ)) 1 { re := x, im := y }
bm :
  HMul.hMul (α := ℤ√(↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) }
      { re := Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) },
        im := -Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) } : ℤ√(↑(d a1) : ℤ) } =
    1
y0l : LT.lt (α := ℤ√(↑(d a1) : ℤ)) 0 { re := x - x, im := y - -y }
yl2 :
  LT.lt (α := ℤ√(↑(d a1) : ℤ))
    {
      re :=
        Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) } +
          Zsqrtd.re (d := (↑(d a1) : ℤ)) (-{ re := x, im := -y : ℤ√(↑(d a1) : ℤ) }),
      im :=
        Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) } +
          Zsqrtd.im (d := (↑(d a1) : ℤ)) (-{ re := x, im := -y : ℤ√(↑(d a1) : ℤ) }) }
    {
      re :=
        Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) } +
          Zsqrtd.re (d := (↑(d a1) : ℤ)) (-{ re := (↑a : ℤ), im := -1 : ℤ√(↑(d a1) : ℤ) }),
      im :=
        Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) } +
          Zsqrtd.im (d := (↑(d a1) : ℤ)) (-{ re := (↑a : ℤ), im := -1 : ℤ√(↑(d a1) : ℤ) }) }
⊢ LT.lt (α := ℤ√(↑(d a1) : ℤ)) 0 { re := 0, im := y + y }

Tactic:
simp only [sub_self, sub_neg_eq_add] at y0l

Premises used: sub_self, sub_neg_eq_add
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
a1p : LE.le (α := ℤ√(↑(d a1) : ℤ)) 0 { re := (↑a : ℤ), im := 1 }
am1p : LE.le (α := ℤ√(↑(d a1) : ℤ)) 0 { re := (↑a : ℤ), im := -1 }
a1m :
  HMul.hMul (α := ℤ√(↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) }
      { re := (↑a : ℤ), im := -1 : ℤ√(↑(d a1) : ℤ) } =
    1
x y : ℤ
h1 : LE.le (α := ℤ√(↑(d a1) : ℤ)) 1 { re := x, im := y }
hp : IsPell (d := (↑(d a1) : ℤ)) { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬LE.le (α := ℤ√(↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 } { re := x, im := y }
h1l : LT.lt (α := ℤ√(↑(d a1) : ℤ)) 1 { re := x, im := y }
bm :
  HMul.hMul (α := ℤ√(↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) }
      { re := Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) },
        im := -Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) } : ℤ√(↑(d a1) : ℤ) } =
    1
yl2 :
  LT.lt (α := ℤ√(↑(d a1) : ℤ))
    {
      re :=
        Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) } +
          Zsqrtd.re (d := (↑(d a1) : ℤ)) (-{ re := x, im := -y : ℤ√(↑(d a1) : ℤ) }),
      im :=
        Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) } +
          Zsqrtd.im (d := (↑(d a1) : ℤ)) (-{ re := x, im := -y : ℤ√(↑(d a1) : ℤ) }) }
    {
      re :=
        Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) } +
          Zsqrtd.re (d := (↑(d a1) : ℤ)) (-{ re := (↑a : ℤ), im := -1 : ℤ√(↑(d a1) : ℤ) }),
      im :=
        Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) } +
          Zsqrtd.im (d := (↑(d a1) : ℤ)) (-{ re := (↑a : ℤ), im := -1 : ℤ√(↑(d a1) : ℤ) }) }
y0l : LT.lt (α := ℤ√(↑(d a1) : ℤ)) 0 { re := 0, im := y + y }
⊢ LT.lt (α := ℤ√(↑(d a1) : ℤ)) { re := 0, im := y + y } { re := 0, im := HAdd.hAdd (α := ℤ) 1 1 }

Tactic:
simp only [Zsqrtd.re_neg, add_neg_cancel,
          Zsqrtd.im_neg, neg_neg] at yl2

Premises used: add_neg_cancel, Zsqrtd.re_neg, neg_neg, Zsqrtd.im_neg
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
a1p : LE.le (α := ℤ√(↑(d a1) : ℤ)) 0 { re := (↑a : ℤ), im := 1 }
am1p : LE.le (α := ℤ√(↑(d a1) : ℤ)) 0 { re := (↑a : ℤ), im := -1 }
a1m :
  HMul.hMul (α := ℤ√(↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) }
      { re := (↑a : ℤ), im := -1 : ℤ√(↑(d a1) : ℤ) } =
    1
x y_1 : ℤ
y0l : LT.lt (α := ℤ√(↑(d a1) : ℤ)) 0 { re := 0, im := y_1 + y_1 }
yl2_1 : LT.lt (α := ℤ√(↑(d a1) : ℤ)) { re := 0, im := y_1 + y_1 } { re := 0, im := HAdd.hAdd (α := ℤ) 1 1 }
y : ℕ
h_1 : LT.lt (α := ℤ√(↑(d a1) : ℤ)) 0 { re := 0, im := HAdd.hAdd (α := ℤ) (↑(y + 1) : ℤ) (↑(y + 1) : ℤ) }
yl2 :
  LT.lt (α := ℤ√(↑(d a1) : ℤ)) { re := 0, im := HAdd.hAdd (α := ℤ) (↑(y + 1) : ℤ) (↑(y + 1) : ℤ) }
    { re := 0, im := HAdd.hAdd (α := ℤ) 1 1 }
h1 : LE.le (α := ℤ√(↑(d a1) : ℤ)) 1 { re := x, im := (↑(y + 1) : ℤ) }
hp : IsPell (d := (↑(d a1) : ℤ)) { re := x, im := (↑(y + 1) : ℤ) }
h : { re := x, im := (↑(y + 1) : ℤ) } ≤ pellZd a1 (n + 1)
ha : ¬LE.le (α := ℤ√(↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 } { re := x, im := (↑(y + 1) : ℤ) }
h1l : LT.lt (α := ℤ√(↑(d a1) : ℤ)) 1 { re := x, im := (↑(y + 1) : ℤ) }
bm :
  HMul.hMul (α := ℤ√(↑(d a1) : ℤ)) { re := x, im := (↑(y + 1) : ℤ) : ℤ√(↑(d a1) : ℤ) }
      { re := Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := x, im := (↑(y + 1) : ℤ) : ℤ√(↑(d a1) : ℤ) },
        im := -Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := x, im := (↑(y + 1) : ℤ) : ℤ√(↑(d a1) : ℤ) } : ℤ√(↑(d a1) : ℤ) } =
    1
⊢ LE.le (α := ℤ) 0 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n : ℕ
a1p : LE.le (α := ℤ√(↑(d a1) : ℤ)) 0 { re := (↑a : ℤ), im := 1 }
am1p : LE.le (α := ℤ√(↑(d a1) : ℤ)) 0 { re := (↑a : ℤ), im := -1 }
a1m :
  HMul.hMul (α := ℤ√(↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) }
      { re := (↑a : ℤ), im := -1 : ℤ√(↑(d a1) : ℤ) } =
    1
x y : ℤ
h1 : LE.le (α := ℤ√(↑(d a1) : ℤ)) 1 { re := x, im := y }
hp : IsPell (d := (↑(d a1) : ℤ)) { re := x, im := y }
h : { re := x, im := y } ≤ pellZd a1 (n + 1)
ha : ¬LE.le (α := ℤ√(↑(d a1) : ℤ)) { re := (↑a : ℤ), im := 1 } { re := x, im := y }
h1l : LT.lt (α := ℤ√(↑(d a1) : ℤ)) 1 { re := x, im := y }
bm :
  HMul.hMul (α := ℤ√(↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) }
      { re := Zsqrtd.re (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) },
        im := -Zsqrtd.im (d := (↑(d a1) : ℤ)) { re := x, im := y : ℤ√(↑(d a1) : ℤ) } : ℤ√(↑(d a1) : ℤ) } =
    1
y0l : LT.lt (α := ℤ√(↑(d a1) : ℤ)) 0 { re := 0, im := y + y }
yl2 : LT.lt (α := ℤ√(↑(d a1) : ℤ)) { re := 0, im := y + y } { re := 0, im := HAdd.hAdd (α := ℤ) 1 1 }
⊢ False

Tactic:
exact
          match y, y0l, (yl2 : (⟨_, _⟩ : ℤ√_) < ⟨_, _⟩) with
          | 0, y0l, _ => y0l (le_refl 0)
          | (y + 1 : ℕ), _, yl2 =>
            yl2
              (Zsqrtd.le_of_le_le (by simp)
                (let t := Int.ofNat_le_ofNat_of_le (Nat.succ_pos y)
                add_le_add t t))
          | Int.negSucc _, y0l, _ => y0l trivial
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
b : ℤ√(↑(d a1) : ℤ)
b1 : 1 ≤ b
hp : IsPell b
n : ℕ
h : b ≤ (↑n : ℤ√(↑(d a1) : ℤ))
⊢ { re := (↑n : ℤ), im := 0 } ≤ pellZd a1 n

Tactic:
Zsqrtd.le_of_le_le (Int.ofNat_le_ofNat_of_le <| le_of_lt <| n_lt_xn _ _)
          (Int.natCast_nonneg _)

Premises used: le_of_lt, Pell.n_lt_xn, Int.ofNat_le_ofNat_of_le, Zsqrtd.le_of_le_le, Int.natCast_nonneg
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
b : ℤ√(↑(d a1) : ℤ)
b1 : 1 ≤ b
hp : IsPell b
n : ℕ
h : b ≤ (↑n : ℤ√(↑(d a1) : ℤ))
⊢ { re := (↑n : ℤ), im := 0 } ≤ pellZd a1 n

Tactic:
exact
        Zsqrtd.le_of_le_le (Int.ofNat_le_ofNat_of_le <| le_of_lt <| n_lt_xn _ _)
          (Int.natCast_nonneg _)

Premises used: le_of_lt, Pell.n_lt_xn, Int.ofNat_le_ofNat_of_le, Zsqrtd.le_of_le_le, Int.natCast_nonneg
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
x y : ℕ
hp_1 : x * x - d a1 * y * y = 1
hp : 0 - d a1 * y * y = 1
⊢ Eq (α := ℕ) 0 1

Tactic:
rw [zero_tsub] at hp

Premises used: zero_tsub
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
x y : ℕ
hp_1 : x * x - d a1 * y * y = 1
hp : Eq (α := ℕ) 0 1
⊢ LE.le (α := ℤ√(↑(d a1) : ℤ)) 1 { re := (↑0 : ℤ), im := (↑y : ℤ) }

Tactic:
contradiction
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
rw : pellZd a1 (m + n + 1) = pellZd a1 m * pellZd a1 (n + 1)
rw₁ : pellZd a1 (m + n) * { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) } = pellZd a1 m * pellZd a1 (n + 1)
rw₂ :
  pellZd a1 (m + n) * { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) } =
    pellZd a1 m * (pellZd a1 n * { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) })
rw₃ :
  pellZd a1 m * pellZd a1 n * { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) } =
    pellZd a1 m * (pellZd a1 n * { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) })
rw₄ rw₅ :
  pellZd a1 m * pellZd a1 n * { re := (↑a : ℤ), im := 1 : ℤ√(↑(d a1) : ℤ) } =
    pellZd a1 m * pellZd a1 n * { re := (↑a : ℤ), im := 1 }
⊢ pellZd a1 (m + (n + 1)) = pellZd a1 m * pellZd a1 (n + 1)

Tactic:
rw [← add_assoc, pellZd_succ, pellZd_succ, pellZd_add _ n, ← mul_assoc]

Premises used: add_assoc, mul_assoc, Pell.pellZd_succ
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
⊢ (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im

Tactic:
injection pellZd_add a1 m n with h _

Premises used: Pell.pellZd_add
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
⊢ (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re

Tactic:
injection pellZd_add a1 m n with h _

Premises used: Pell.pellZd_add
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
im_eq : (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
zify :
  (↑(xn a1 (m + n)) : ℤ) =
    HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(xn a1 n) : ℤ) +
      HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 m) : ℤ) * (↑(yn a1 n) : ℤ)
⊢ xn a1 (m + n) = xn a1 m * xn a1 n + d a1 * yn a1 m * yn a1 n

Tactic:
zify
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
im_eq : (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
rw :
  (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im =
    HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(xn a1 n) : ℤ) +
      HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 m) : ℤ) * (↑(yn a1 n) : ℤ)
⊢ (↑(xn a1 (m + n)) : ℤ) =
    HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(xn a1 n) : ℤ) +
      HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 m) : ℤ) * (↑(yn a1 n) : ℤ)

Tactic:
rw [h]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
im_eq : (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im =
    HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(xn a1 n) : ℤ) +
      HMul.hMul (α := ℤ) (↑(d a1) : ℤ) (↑(yn a1 m) : ℤ) * (↑(yn a1 n) : ℤ)

Tactic:
simp [pellZd]

Premises used: Pell.pellZd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
⊢ (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im

Tactic:
injection pellZd_add a1 m n with _ h

Premises used: Pell.pellZd_add
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq :
  (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
⊢ (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re

Tactic:
injection pellZd_add a1 m n with _ h

Premises used: Pell.pellZd_add
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq :
  (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
h : (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
zify :
  (↑(yn a1 (m + n)) : ℤ) =
    HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(yn a1 n) : ℤ) + HMul.hMul (α := ℤ) (↑(yn a1 m) : ℤ) (↑(xn a1 n) : ℤ)
⊢ yn a1 (m + n) = xn a1 m * yn a1 n + yn a1 m * xn a1 n

Tactic:
zify
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq :
  (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
h : (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
rw :
  (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re =
    HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(yn a1 n) : ℤ) + HMul.hMul (α := ℤ) (↑(yn a1 m) : ℤ) (↑(xn a1 n) : ℤ)
⊢ (↑(yn a1 (m + n)) : ℤ) =
    HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(yn a1 n) : ℤ) + HMul.hMul (α := ℤ) (↑(yn a1 m) : ℤ) (↑(xn a1 n) : ℤ)

Tactic:
rw [h]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
re_eq :
  (↑(xn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).re + (↑(d a1) : ℤ) * (pellZd a1 m).im * (pellZd a1 n).im
h : (↑(yn a1 (m + n)) : ℤ) = (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re
⊢ (pellZd a1 m).re * (pellZd a1 n).im + (pellZd a1 m).im * (pellZd a1 n).re =
    HMul.hMul (α := ℤ) (↑(xn a1 m) : ℤ) (↑(yn a1 n) : ℤ) + HMul.hMul (α := ℤ) (↑(yn a1 m) : ℤ) (↑(xn a1 n) : ℤ)

Tactic:
simp [pellZd]

Premises used: Pell.pellZd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 (n + (m - n)) = pellZd a1 n * pellZd a1 (m - n) := ⋯
⊢ pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)

Tactic:
rw [add_tsub_cancel_of_le h] at t

Premises used: add_tsub_cancel_of_le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
t : pellZd a1 m = pellZd a1 n * pellZd a1 (m - n)
rw : pellZd a1 (m - n) = pellZd a1 n * pellZd a1 (m - n) * star (pellZd a1 n)
rw₁ : pellZd a1 (m - n) = pellZd a1 (m - n) * pellZd a1 n * star (pellZd a1 n)
rw₂ : pellZd a1 (m - n) = pellZd a1 (m - n) * (pellZd a1 n * star (pellZd a1 n))
rw₃ : pellZd a1 (m - n) = pellZd a1 (m - n) * 1
rw₄ rw₅ : pellZd a1 (m - n) = pellZd a1 (m - n)
⊢ pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n)

Tactic:
rw [t, mul_comm (pellZd _ n) _, mul_assoc, isPell_norm.1 (isPell_pellZd _ _), mul_one]

Premises used: Pell.isPell_norm, mul_assoc, Iff.mp, mul_comm, Pell.pellZd, mul_one, Pell.isPell_pellZd
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
rw : xz a1 (m - n) = xz a1 m * xz a1 n + (↑(d a1) : ℤ) * yz a1 m * -yz a1 n
⊢ xz a1 (m - n) = xz a1 m * xz a1 n - (↑(d a1) : ℤ) * yz a1 m * yz a1 n

Tactic:
rw [sub_eq_add_neg, ← mul_neg]

Premises used: sub_eq_add_neg, mul_neg
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ xz a1 (m - n) = xz a1 m * xz a1 n + (↑(d a1) : ℤ) * yz a1 m * -yz a1 n

Tactic:
congr_arg Zsqrtd.re (pellZd_sub a1 h)

Premises used: Zsqrtd.re, Pell.pellZd_sub, Pell.yz, Pell.xz, congr_arg
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ xz a1 (m - n) = xz a1 m * xz a1 n + (↑(d a1) : ℤ) * yz a1 m * -yz a1 n

Tactic:
exact congr_arg Zsqrtd.re (pellZd_sub a1 h)

Premises used: Zsqrtd.re, Pell.pellZd_sub, congr_arg
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
rw : yz a1 (m - n) = xz a1 m * -yz a1 n + yz a1 m * xz a1 n
⊢ yz a1 (m - n) = xz a1 n * yz a1 m - xz a1 m * yz a1 n

Tactic:
rw [sub_eq_add_neg, ← mul_neg, mul_comm, add_comm]

Premises used: sub_eq_add_neg, add_comm, mul_comm, mul_neg
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ yz a1 (m - n) = xz a1 m * -yz a1 n + yz a1 m * xz a1 n

Tactic:
congr_arg Zsqrtd.im (pellZd_sub a1 h)

Premises used: Pell.pellZd_sub, Pell.yz, Pell.xz, congr_arg, Zsqrtd.im
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : n ≤ m
⊢ yz a1 (m - n) = xz a1 m * -yz a1 n + yz a1 m * xz a1 n

Tactic:
exact congr_arg Zsqrtd.im (pellZd_sub a1 h)

Premises used: Pell.pellZd_sub, congr_arg, Zsqrtd.im
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
h : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
p : xn a1 n * xn a1 n - d a1 * yn a1 n * yn a1 n = 1 := ⋯
rw : k ∣ xn a1 n * xn a1 n - d a1 * yn a1 n * yn a1 n
⊢ k ∣ 1

Tactic:
rw [← p]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
h : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
p : xn a1 n * xn a1 n - d a1 * yn a1 n * yn a1 n = 1 := ⋯
⊢ k ∣ xn a1 n * xn a1 n - d a1 * yn a1 n * yn a1 n

Tactic:
Nat.dvd_sub (kx.mul_left _) (ky.mul_left _)

Premises used: Dvd.dvd.mul_left, Nat.dvd_sub
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
h : Nat.Prime k
kx : k ∣ xn a1 n
ky : k ∣ yn a1 n
p : xn a1 n * xn a1 n - d a1 * yn a1 n * yn a1 n = 1 := ⋯
⊢ k ∣ xn a1 n * xn a1 n - d a1 * yn a1 n * yn a1 n

Tactic:
exact Nat.dvd_sub (kx.mul_left _) (ky.mul_left _)

Premises used: Dvd.dvd.mul_left, Nat.dvd_sub
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
e : m = n
rw rw₁ : yn a1 n ≤ yn a1 n
⊢ yn a1 m ≤ yn a1 n

Tactic:
rw [e]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
⊢ yn a1 m ≤ yn a1 n

Tactic:
have : yn a1 m ≤ yn a1 n :=
      Or.elim (lt_or_eq_of_le <| Nat.le_of_succ_le_succ h) (fun hl => le_of_lt <| strictMono_y hl)
        fun e => by rw [e]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m < xn a1 n + yn a1 n * a

Tactic:
lt_of_le_of_lt ?_ (Nat.lt_add_of_pos_left <| x_pos a1 n)

Premises used: lt_of_le_of_lt, Nat.lt_add_of_pos_left, Pell.x_pos
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
refine : yn a1 m ≤ yn a1 n * a
⊢ yn a1 m < xn a1 n + yn a1 n * a

Tactic:
refine lt_of_le_of_lt ?_ (Nat.lt_add_of_pos_left <| x_pos a1 n)

Premises used: lt_of_le_of_lt, Nat.lt_add_of_pos_left, Pell.x_pos
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
rw : yn a1 m * 1 ≤ yn a1 n * a
⊢ yn a1 m ≤ yn a1 n * a

Tactic:
rw [← mul_one (yn a1 m)]

Premises used: Pell.yn, mul_one
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m * 1 ≤ yn a1 n * a

Tactic:
mul_le_mul this (le_of_lt a1) (Nat.zero_le _) (Nat.zero_le _)

Premises used: Nat.zero_le, le_of_lt, mul_le_mul
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : yn a1 m ≤ yn a1 n
⊢ yn a1 m * 1 ≤ yn a1 n * a

Tactic:
exact mul_le_mul this (le_of_lt a1) (Nat.zero_le _) (Nat.zero_le _)

Premises used: Nat.zero_le, le_of_lt, mul_le_mul
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
e : m = n
rw rw₁ : xn a1 n ≤ xn a1 n
⊢ xn a1 m ≤ xn a1 n

Tactic:
rw [e]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
⊢ xn a1 m ≤ xn a1 n

Tactic:
have : xn a1 m ≤ xn a1 n :=
      Or.elim (lt_or_eq_of_le <| Nat.le_of_succ_le_succ h) (fun hl => le_of_lt <| strictMono_x hl)
        fun e => by rw [e]
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
⊢ xn a1 m < xn a1 n * a + d a1 * yn a1 n

Tactic:
lt_of_lt_of_le (lt_of_le_of_lt this ?_) (Nat.le_add_right _ _)

Premises used: lt_of_le_of_lt, Nat.le_add_right, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
refine : xn a1 n < xn a1 n * a
⊢ xn a1 m < xn a1 n * a + d a1 * yn a1 n

Tactic:
refine lt_of_lt_of_le (lt_of_le_of_lt this ?_) (Nat.le_add_right _ _)

Premises used: lt_of_le_of_lt, Nat.le_add_right, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
⊢ xn a1 n * 1 < xn a1 n * a

Tactic:
have t := Nat.mul_lt_mul_of_pos_left a1 (x_pos a1 n)
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : m < n + 1
this : xn a1 m ≤ xn a1 n
t : xn a1 n * 1 < xn a1 n * a
rwa rwa₁ rwa₂ rwa₃ : ∀ (t : xn a1 n < xn a1 n * a), xn a1 n < xn a1 n * a
⊢ xn a1 n < xn a1 n * a

Tactic:
rwa [mul_one] at t

Premises used: mul_one
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
rw : yn a1 n ∣ xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n
⊢ yn a1 n ∣ yn a1 (n * (k + 1))

Tactic:
rw [Nat.mul_succ, yn_add]

Premises used: Nat.mul_succ, Pell.yn_add
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
⊢ yn a1 n ∣ xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n

Tactic:
dvd_add (dvd_mul_left _ _) ((y_mul_dvd _ k).mul_right _)

Premises used: Dvd.dvd.mul_right, dvd_mul_left, dvd_add
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
n k : ℕ
⊢ yn a1 n ∣ xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n

Tactic:
exact dvd_add (dvd_mul_left _ _) ((y_mul_dvd _ k).mul_right _)

Premises used: Dvd.dvd.mul_right, dvd_mul_left, dvd_add
-- Module: Mathlib.NumberTheory.PellMatiyasevic
Goal:
a : ℕ
a1 : 1 < a
m n : ℕ
h : yn a1 m ∣ yn a1 n
hp : n % m > 0
⊢ (yn a1 m).Coprime (xn a1 (m * (n / m)))

Tactic:
have co : Nat.Coprime (yn a1 m) (xn a1 (m * (n / m))) :=
          Nat.Coprime.symm <| (xy_coprime a1 _).coprime_dvd_right (y_mul_dvd a1 m (n / m))