mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ discr K ((fun i ↦ ζ ^ ↑i) ∘ ⇑e.symm) = (-1) ^ (φ (2 ^ (0 + 1)) / 2) * ↑2 ^ (2 ^ (0 + 1 - 1) * ((2 - 1) * (0 + 1) - 1))

Tactic:
]

Goal state after:
case pos
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ discr K ((fun i ↦ ζ ^ ↑i) ∘ ⇑e.symm) = (-1) ^ (φ (2 ^ (0 + 1)) / 2) * ↑2 ^ (2 ^ (0 + 1 - 1) * ((2 - 1) * (0 + 1) - 1))
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
⊢ d a1 * yn a1 n * (xn a1 n * yn a1 j) + (d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j) ≡ 0 + 0 [MOD xn a1 n]

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ d a1 * yn a1 n * (xn a1 n * yn a1 j) + (d a1 * yn a1 n * (yn a1 n * xn a1 j) + xn a1 j) ≡ 0 + 0 [MOD xn a1 n]
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
⊢ ↑x * a + sqrtd * (↑y * a) = ↑x * a + sqrtd * (↑y * a)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ (↑x * a + sqrtd * (↑y * a)).Nonneg

Tactic:
]

Goal state after:
d x y : ℕ
a : ℤ√↑d
ha : a.Nonneg
this : { re := ↑x, im := ↑y } * a = ↑x * a + sqrtd * (↑y * a)
⊢ (↑x * a + sqrtd * (↑y * a)).Nonneg
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(d a1) * yz a1 n * (xz a1 j * yz a1 n) + xz a1 j - ↑(d a1) * yz a1 n * (xz a1 n * yz a1 j)

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ xz a1 n ∣ ↑(d a1) * yz a1 n * (xz a1 j * yz a1 n) + xz a1 j - ↑(d a1) * yz a1 n * (xz a1 n * yz a1 j)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
x✝ : { re := ↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑z, im := ↑w } * { re := -↑x, im := ↑y }).Nonneg

Tactic:
]

Goal state after:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
x✝ : { re := ↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑z, im := ↑w } * { re := -↑x, im := ↑y }).Nonneg
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(d a1) * ↑(yn a1 n) * (↑(yn a1 n) * ↑(xn a1 j)) + ↑(xn a1 j)

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
⊢ ↑(xn a1 n) ∣ ↑(d a1) * ↑(yn a1 n) * (↑(yn a1 n) * ↑(xn a1 j)) + ↑(xn a1 j)
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
x✝ : { re := ↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑z, im := ↑w } * { re := ↑x, im := -↑y }).Nonneg

Tactic:
]

Goal state after:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
x✝ : { re := ↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑z, im := ↑w } * { re := ↑x, im := -↑y }).Nonneg
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }.Nonneg

Tactic:
]

Goal state after:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }.Nonneg
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ xn a1 n * xn a1 (n - j) + (d a1 * yn a1 n * yn a1 (n - j) + xn a1 j) ≡ 0 + 0 [MOD xn a1 n]

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ n
h1 : xz a1 n ∣ ↑(d a1) * yz a1 n * yz a1 (n - j) + xz a1 j
⊢ xn a1 n * xn a1 (n - j) + (d a1 * yn a1 n * yn a1 (n - j) + xn a1 j) ≡ 0 + 0 [MOD xn a1 n]
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : p (v ⊗ t ∘ inl) = 0
hr : List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
⊢ p (v ⊗ t ∘ inl) = 0

Tactic:
]

Goal state after:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : p (v ⊗ t ∘ inl) = 0
hr : List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
⊢ p (v ⊗ t ∘ inl) = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg

Tactic:
]

Goal state after:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := -↑x, im := ↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
⊢ n + n ≤ n + j

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
⊢ n + n ≤ n + j
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
this : 2 * n - j + j ≤ n + j
t : xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
this : 2 * n - j + j ≤ n + j
t : xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg

Tactic:
]

Goal state after:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := -↑z, im := ↑w }.Nonneg
⊢ { re := -(↑x * ↑z + ↑d * ↑y * ↑w), im := ↑x * ↑w + ↑y * ↑z }.Nonneg
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
jn : n ≤ j
this : 2 * n - j + j ≤ n + j
t : xn a1 (2 * n - (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n] :=
  xn_modEq_x2n_sub_lem a1 (Nat.le_of_add_le_add_right this)
⊢ xn a1 (2 * n - j) + xn a1 j ≡ 0 [MOD xn a1 n]

Tactic:
rwa [tsub_tsub_cancel_of_le h, add_comm] at t

Goal state after:
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case e'_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
i : Fin 1
⊢ ↑(e.symm i) < 1

Tactic:
]

Goal state after:
case e'_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
i : Fin 1
⊢ ↑(e.symm i) < 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
⊢ 0 ≡ xn a1 (2 * n + j) + xn a1 j [MOD xn a1 n]

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ 0 ≡ xn a1 (2 * n + j) + xn a1 j [MOD xn a1 n]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (2 * n + (2 * n + j)) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
⊢ xn a1 (2 * n + (2 * n + j)) + xn a1 (2 * n + j) ≡ 0 [MOD xn a1 n]
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
i : Fin 1
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }.Nonneg

Tactic:
]

Goal state after:
d : ℕ
a b : ℤ√↑d
ha✝ : a.Nonneg
hb✝ : b.Nonneg
x y z w : ℕ
ha : { re := ↑x, im := -↑y }.Nonneg
hb : { re := ↑z, im := -↑w }.Nonneg
⊢ { re := ↑x * ↑z + ↑d * ↑y * ↑w, im := -(↑x * ↑w + ↑y * ↑z) }.Nonneg
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h : j ≤ 2 * n
⊢ 1 * n + n ≤ 1 * n + n

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ 0 ≡ xn a1 (2 * n - j) + xn a1 j [MOD xn a1 n]

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ 0 ≡ xn a1 (2 * n - j) + xn a1 j [MOD xn a1 n]
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ False

Tactic:
]

Goal state after:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
⊢ False
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (2 * n + (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
n j : ℕ
h h' : j ≤ 2 * n
⊢ xn a1 (2 * n + (2 * n - j)) + xn a1 (2 * n - j) ≡ 0 [MOD xn a1 n]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
this : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
this : xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
h : i = j
⊢ xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: case pos.convert_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ φ (2 ^ (0 + 1)) • 1 = 1

Tactic:
]

Goal state after:
case pos.convert_2
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime 2)
hcycl✝ : IsCyclotomicExtension {2 ^ (0 + 1)} K L
hcycl : IsCyclotomicExtension {2} K L
hζ✝ : IsPrimitiveRoot ζ (2 ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
hirr : Irreducible (cyclotomic (2 ^ (0 + 1)) K)
this : (minpoly K ζ).natDegree = 1
e : Fin (minpoly K ζ).natDegree ≃ Fin 1
⊢ φ (2 ^ (0 + 1)) • 1 = 1
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ d ∣ d * (n * n)

Tactic:
]

Goal state after:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
g : ℕ := x.gcd y
gpos : g > 0
m n : ℕ
h : m * g * (m * g) = d * (n * g) * (n * g)
co : m.Coprime n
hx : x = m * g
hy : y = n * g
this : m * m = d * (n * n)
co2 : (m * m).Coprime (n * n)
⊢ d ∣ d * (n * n)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j < xn a1 (j + 1)

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
i n j : ℕ
ij : i < j + 1
jn : j + 1 < n
⊢ xn a1 j < xn a1 (j + 1)
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
h : xn a1 n * 2 = xn a1 n * a + d a1 * yn a1 n
⊢ a = 2 ∧ n = 0

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
n : ℕ
h : xn a1 n * 2 = xn a1 n * a + d a1 * yn a1 n
⊢ a = 2 ∧ n = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : ↑(x.natAbs * x.natAbs) = ↑(d * y.natAbs * y.natAbs)
⊢ x = 0 ∧ y = 0

Tactic:
]

Goal state after:
d : ℕ
dnsq : Nonsquare d
x y : ℤ
h : ↑(x.natAbs * x.natAbs) = ↑(d * y.natAbs * y.natAbs)
⊢ x = 0 ∧ y = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
t : (x + 1) * (x + 1) = d * y.succ * y.succ
⊢ { re := ↑(x + 1), im := -[y+1] } = 0

Tactic:
]

Goal state after:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (y + 1) d (x + 1) 1
yx : SqLe (x + 1) 1 y.succ d
t : (x + 1) * (x + 1) = d * y.succ * y.succ
⊢ { re := ↑(x + 1), im := -[y+1] } = 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := eq_of_xn_modEq_lem3._proof_1_5 npos k kn
xle : xn a1 (2 * n - k) ≤ xn a1 n
this : xn a1 k % xn a1 n = xn a1 n - xn a1 (2 * n - k)
⊢ ↑(xn a1 n) - ↑(xn a1 (2 * n - k)) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
t : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ { re := -[x+1], im := ↑(y + 1) } = 0

Tactic:
]

Goal state after:
d : ℕ
dnsq : Nonsquare d
x y : ℕ
xy : SqLe (x + 1) 1 (y + 1) d
yx : SqLe (y + 1) d x.succ 1
t : (x + 1) * (x + 1) = d * (y + 1) * (y + 1)
⊢ { re := -[x+1], im := ↑(y + 1) } = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
a b : ℤ√↑d
ab : a ≤ b
ba : b ≤ a
⊢ (b - a).Nonneg

Tactic:
]

Goal state after:
d : ℕ
dnsq : Nonsquare d
a b : ℤ√↑d
ab : a ≤ b
ba : b ≤ a
⊢ (b - a).Nonneg
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
x✝¹ x✝ : ℤ√↑d
ab : x✝¹ ≤ x✝
ba : x✝ ≤ x✝¹
⊢ (x✝ - x✝¹).Nonneg

Tactic:
]

Goal state after:
d : ℕ
dnsq : Nonsquare d
x✝¹ x✝ : ℤ√↑d
ab : x✝¹ ≤ x✝
ba : x✝ ≤ x✝¹
⊢ (x✝ - x✝¹).Nonneg
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
⊢ ∃ u n, (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑u * ↑p ^ n

Tactic:
]

Goal state after:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
⊢ ∃ u n, (-1) ^ (φ (p ^ k) / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑u * ↑p ^ n
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
a b : ℤ√↑d
t : (b - a).Nonneg ∨ (a - b).Nonneg
⊢ a ≤ b ∨ b ≤ a

Tactic:
]

Goal state after:
d : ℕ
dnsq : Nonsquare d
a b : ℤ√↑d
t : (b - a).Nonneg ∨ (a - b).Nonneg
⊢ a ≤ b ∨ b ≤ a
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := eq_of_xn_modEq_lem3._proof_1_5 npos k kn
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k % xn a1 n = (xn a1 n - xn a1 (2 * n - k)) % xn a1 n

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := eq_of_xn_modEq_lem3._proof_1_5 npos k kn
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k % xn a1 n = (xn a1 n - xn a1 (2 * n - k)) % xn a1 n
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
heven : Even (φ (p ^ k) / 2)
⊢ 1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
]

Goal state after:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
heven : Even (φ (p ^ k) / 2)
⊢ 1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
q : Poly (α ⊕ γ)
hq : q (v ⊗ t ∘ inr) = 0
⊢ q (v ⊗ t ∘ inr) = 0

Tactic:
]

Goal state after:
α : Type u
S : Set (α → ℕ)
l : List (Set (α → ℕ))
IH :
  List.Forall Dioph l →
    ∃ β pl, ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
d : List.Forall Dioph (S :: l)
dl : List.Forall Dioph l
β : Type u
p : Poly (α ⊕ β)
pe : ∀ (v : α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
γ : Type u
pl : List (Poly (α ⊕ γ))
ple : ∀ (v : α → ℕ), List.Forall (fun S ↦ v ∈ S) l ↔ ∃ t, List.Forall (fun p ↦ p (v ⊗ t) = 0) pl
v : α → ℕ
x✝ :
  ∃ t,
    p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0 ∧
      List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
t : β ⊕ γ → ℕ
hl : p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl)) = 0
hr : List.Forall ((fun p ↦ p (v ⊗ t) = 0) ∘ fun q ↦ Poly.map (inl ⊗ inr ∘ inr) q) pl
q : Poly (α ⊕ γ)
hq : q (v ⊗ t ∘ inr) = 0
⊢ q (v ⊗ t ∘ inr) = 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := eq_of_xn_modEq_lem3._proof_1_5 npos k kn
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := eq_of_xn_modEq_lem3._proof_1_5 npos k kn
xle : xn a1 (2 * n - k) ≤ xn a1 n
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := eq_of_xn_modEq_lem3._proof_1_5 npos k kn
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 k + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
i n : ℕ
npos : 0 < n
j : ℕ
ij : i < j + 1
j2n : j + 1 ≤ 2 * n
jnn : j + 1 ≠ n
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j + 1 = 2)
k : ℕ
kn : k > n
k2n : k ≤ 2 * n
k2nl : 2 * n - k < n := eq_of_xn_modEq_lem3._proof_1_5 npos k kn
xle : xn a1 (2 * n - k) ≤ xn a1 n
t : xn a1 k + xn a1 (2 * n - k) ≡ 0 [MOD xn a1 n]
⊢ xn a1 k + xn a1 (2 * n - k) ≡ xn a1 n [MOD xn a1 n]
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℕ
dnsq : Nonsquare d
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ (b - a).Nonneg

Tactic:
]

Goal state after:
d : ℕ
dnsq : Nonsquare d
a b : ℤ√↑d
ab : a ≤ b
c : ℤ√↑d
⊢ (b - a).Nonneg
Module: Mathlib.NumberTheory.Cyclotomic.Discriminant

Goal state before:
pp: p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
heven : ¬Even (φ (p ^ k) / 2)
⊢ -1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑(-1) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))

Tactic:
]

Goal state after:
p k : ℕ
K : Type u
L : Type v
ζ : L
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {p ^ k} K L
hp : Fact (Nat.Prime p)
hζ : IsPrimitiveRoot ζ (p ^ k)
hirr : Irreducible (cyclotomic (p ^ k) K)
heven : ¬Even (φ (p ^ k) / 2)
⊢ -1 * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1)) = ↑↑(-1) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
h : a = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
⊢ a.re = re 0 ∧ a.im = im 0

Tactic:
]

Goal state after:
d : ℤ
h_nonsquare : ∀ (n : ℤ), d ≠ n * n
a : ℤ√d
ha : a.re * a.re = d * a.im * a.im
⊢ a.re = re 0 ∧ a.im = im 0