mathlib-initiative/mathlib-tactics huggingface dataset:
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)
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j > n
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
⊢ ↑(xn a1 n) - ↑(xn a1 (2 * n - j)) < ↑(xn a1 n) - ↑(xn a1 (2 * n - (j + 1)))

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)
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j > n
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
⊢ ↑(xn a1 n) - ↑(xn a1 (2 * n - j)) < ↑(xn a1 n) - ↑(xn a1 (2 * n - (j + 1)))
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)
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j > n
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
⊢ (2 * n - j).pred < 2 * n - j

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)
lem2 : ∀ k > n, k ≤ 2 * n → ↑(xn a1 k % xn a1 n) = ↑(xn a1 n) - ↑(xn a1 (2 * n - k))
o : j = n ∨ n < j
jn : j > n
lem1 : j ≠ n → xn a1 j % xn a1 n < xn a1 (j + 1) % xn a1 n → xn a1 i % xn a1 n < xn a1 (j + 1) % xn a1 n
⊢ (2 * n - j).pred < 2 * n - j
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
⊢ 0 < xn a1 i % xn a1 n

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
⊢ 0 < xn a1 i % xn a1 n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
⊢ 0 < xn a1 0

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ij : i ≤ j
j2n : j ≤ 2 * n
h : xn a1 i ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i = 0 ∧ j = 2)
npos : ¬n = 0
ij' : i < j
jn : j = n
⊢ 0 < xn a1 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case succ
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : i + 1 < n
⊢ 0 < xn a1 (i + 1) % xn a1 n

Tactic:
]

Goal state after:
case succ
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : i + 1 < n
⊢ 0 < xn a1 (i + 1) % xn a1 n
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
m_pos : 0 < ↑m
q' : ℚ
hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)
hden : q'.den ≤ m
den_pos : 0 < ↑q'.den
md_pos : 0 < (↑m + 1) * ↑q'.den
⊢ ↑q'.den < ↑m + 1

Tactic:
]

Goal state after:
ξ : ℝ
hξ : Irrational ξ
q : ℚ
h : 0 < |ξ - ↑q|
m : ℕ
hm : 1 / |ξ - ↑q| < ↑m
m_pos : 0 < ↑m
q' : ℚ
hbd : |ξ - ↑q'| ≤ 1 / ((↑m + 1) * ↑q'.den)
hden : q'.den ≤ m
den_pos : 0 < ↑q'.den
md_pos : 0 < (↑m + 1) * ↑q'.den
⊢ ↑q'.den < ↑m + 1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : 2 < 1
x✝ : a = 2 ∧ n = 1 ∧ 0 = 0 ∧ i + 1 = 2
left✝¹ : a = 2
n1 : n = 1
left✝ : 0 = 0
i2 : i + 1 = 2
⊢ False

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
j n : ℕ
j2n : j ≤ 2 * n
npos : ¬n = 0
jn : j = n
x0 : 0 < xn a1 0 % xn a1 n
i : ℕ
ij : i + 1 ≤ j
h : xn a1 (i + 1) ≡ xn a1 j [MOD xn a1 n]
ntriv : ¬(a = 2 ∧ n = 1 ∧ i + 1 = 0 ∧ j = 2)
ij' : 2 < 1
x✝ : a = 2 ∧ n = 1 ∧ 0 = 0 ∧ i + 1 = 2
left✝¹ : a = 2
n1 : n = 1
left✝ : 0 = 0
i2 : i + 1 = 2
⊢ False
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ q : ℚ
h : |ξ - q| * ↑q.den < 1 / ↑q.den ^ 2 * ↑q.den
hq₀ : 0 < ↑q.den
⊢ |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den

Tactic:
]

Goal state after:
ξ q : ℚ
h : |ξ - q| * ↑q.den < 1 / ↑q.den ^ 2 * ↑q.den
hq₀ : 0 < ↑q.den
⊢ |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
⊢ n ≤ n + n

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
⊢ n ≤ n + n
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : 2 ≤ 1
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
x✝¹ : a = 2
n1 : n = 1
x✝ : j = 0
i2 : i = 2
⊢ False

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : 2 ≤ 1
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : j ≤ 2 * n
x✝¹ : a = 2
n1 : n = 1
x✝ : j = 0
i2 : i = 2
⊢ False
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ q : ℚ
h : |ξ - q| * ↑q.den < 1 / ↑q.den ^ 2 * ↑q.den
hq₀ : 0 < ↑q.den
| |ξ - q| * |↑q.den|

Tactic:
← abs_mul,

Goal state after:
ξ q : ℚ
h : |ξ - q| * ↑q.den < 1 / ↑q.den ^ 2 * ↑q.den
hq₀ : 0 < ↑q.den
| |(ξ - q) * ↑q.den|
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
j42n : 4 * n - j ≤ 2 * n
t : xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]
⊢ xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
j42n : 4 * n - j ≤ 2 * n
t : xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]
⊢ xn a1 j ≡ xn a1 (4 * n - j) [MOD xn a1 n]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
j4n : j ≤ 4 * n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
i2n : i ≤ 2 * n
j2n : 2 * n < j
this : i = 4 * n - j
⊢ 4 * n = 4 * n

Tactic:
]

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

Goal state before:
pp: ξ q : ℚ
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
hq₀ : 0 < ↑q.den
⊢ |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den

Tactic:
]

Goal state after:
ξ q : ℚ
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
hq₀ : 0 < ↑q.den
⊢ |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
⊢ j % (4 * n) = j'

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : p (t none ::ₒ v ⊗ t ∘ some) = 0
⊢ p (t none ::ₒ v ⊗ t ∘ some) = 0

Tactic:
]

Goal state after:
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map (inr none ::ₒ inl ⊗ inr ∘ some) p) (v ⊗ t) = 0
t : Option β → ℕ
ht : p (t none ::ₒ v ⊗ t ∘ some) = 0
⊢ p (t none ::ₒ v ⊗ t ∘ some) = 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case succ
a : ℕ
a1 : 1 < a
i j✝ n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j✝ ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j✝ % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j✝ ≡ j' [MOD 4 * n]
j q : ℕ
IH : xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (4 * n + (j + 4 * n * q)) ≡ xn a1 j [MOD xn a1 n]

Tactic:
]

Goal state after:
case succ
a : ℕ
a1 : 1 < a
i j✝ n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j✝ ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j✝ % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j✝ ≡ j' [MOD 4 * n]
j q : ℕ
IH : xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (4 * n + (j + 4 * n * q)) ≡ xn a1 j [MOD xn a1 n]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
ji : j' = i
⊢ j ≡ j' [MOD 4 * n]

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
ji : j' = i
⊢ j ≡ j' [MOD 4 * n]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
ji : j' + i = 4 * n
⊢ 4 * n ≡ 0 [MOD 4 * n]

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
ji : j' + i = 4 * n
⊢ 4 * n ≡ 0 [MOD 4 * n]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (j % (4 * n) + 4 * n * (j / (4 * n))) ≡ xn a1 j' [MOD xn a1 n]

Tactic:
]

Goal state after:
a : ℕ
a1 : 1 < a
i j n : ℕ
ipos : 0 < i
hin : i ≤ n
h : xn a1 j ≡ xn a1 i [MOD xn a1 n]
j' : ℕ := j % (4 * n)
n4 : 0 < 4 * n
jl : j' < 4 * n
jj : j ≡ j' [MOD 4 * n]
this : ∀ (j q : ℕ), xn a1 (j + 4 * n * q) ≡ xn a1 j [MOD xn a1 n]
⊢ xn a1 (j % (4 * n) + 4 * n * (j / (4 * n))) ≡ xn a1 j' [MOD xn a1 n]
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| < ↑ξ.den / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ q.den ≤ ξ.den

Tactic:
]

Goal state after:
case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| < ↑ξ.den / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ q.den ≤ ξ.den
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * xn a1 (n + 1) ≡ 2 * b * xn b1 (n + 1) [MOD c]

Tactic:
]

Goal state after:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * xn a1 (n + 1) ≡ 2 * b * xn b1 (n + 1) [MOD c]
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | (v ∘ some, v none) ∈ f.graph}}
x : ℕ
hS : x ::ₒ v ∈ S
h : ∃ (h : (f (v, (x ::ₒ v) none).1).Dom), (f (v, (x ::ₒ v) none).1).get h = (v, (x ::ₒ v) none).2
⊢ v ∈ {v | ∃ (h : v ∈ f.Dom), f.fn v h ::ₒ v ∈ S}

Tactic:
]

Goal state after:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | (v ∘ some, v none) ∈ f.graph}}
x : ℕ
hS : x ::ₒ v ∈ S
h : ∃ (h : (f (v, (x ::ₒ v) none).1).Dom), (f (v, (x ::ₒ v) none).1).get h = (v, (x ::ₒ v) none).2
⊢ v ∈ {v | ∃ (h : v ∈ f.Dom), f.fn v h ::ₒ v ∈ S}
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ 2 * b * yn b1 (n + 1) [MOD c]

Tactic:
]

Goal state after:
a b c : ℕ
a1 : 1 < a
b1 : 1 < b
h : a ≡ b [MOD c]
n : ℕ
⊢ 2 * a * yn a1 (n + 1) ≡ 2 * b * yn b1 (n + 1) [MOD c]
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| < ↑ξ.den / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ 1 ≤ |ξ.num * ↑q.den - q.num * ↑ξ.den|

Tactic:
]

Goal state after:
case left.inr
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |↑ξ.num * ↑q.den - ↑ξ.den * ↑q.num| < ↑ξ.den / ↑q.den
H : ξ ≠ q
hξ₀ : 0 < ↑ξ.den
⊢ 1 ≤ |ξ.num * ↑q.den - q.num * ↑ξ.den|
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
⊢ 1 < a ∧
    k ≤ yn a1 k ∧
      (xn a1 k = 1 ∧ yn a1 k = 0 ∨
        ∃ u v s t b,
          xn a1 k * xn a1 k - (a * a - 1) * yn a1 k * yn a1 k = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 k] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 k * yn a1 k ∣ v ∧ s ≡ xn a1 k [MOD u] ∧ t ≡ k [MOD 4 * yn a1 k])

Tactic:
]

Goal state after:
a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
⊢ 1 < a ∧
    k ≤ yn a1 k ∧
      (xn a1 k = 1 ∧ yn a1 k = 0 ∨
        ∃ u v s t b,
          xn a1 k * xn a1 k - (a * a - 1) * yn a1 k * yn a1 k = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧
                  b ≡ 1 [MOD 4 * yn a1 k] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 k * yn a1 k ∣ v ∧ s ≡ xn a1 k [MOD u] ∧ t ≡ k [MOD 4 * yn a1 k])
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
k0 : k = 0
⊢ 0 ≤ yn a1 0 ∧
    (xn a1 0 = 1 ∧ yn a1 0 = 0 ∨
      ∃ u v s t b,
        xn a1 0 * xn a1 0 - (a * a - 1) * yn a1 0 * yn a1 0 = 1 ∧
          u * u - (a * a - 1) * v * v = 1 ∧
            s * s - (b * b - 1) * t * t = 1 ∧
              1 < b ∧
                b ≡ 1 [MOD 4 * yn a1 0] ∧
                  b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 0 * yn a1 0 ∣ v ∧ s ≡ xn a1 0 [MOD u] ∧ t ≡ 0 [MOD 4 * yn a1 0])

Tactic:
]

Goal state after:
a k x y : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x ∧ yn a1 k = y
a1 : 1 < a
hx : xn a1 k = x
hy : yn a1 k = y
k0 : k = 0
⊢ 0 ≤ yn a1 0 ∧
    (xn a1 0 = 1 ∧ yn a1 0 = 0 ∨
      ∃ u v s t b,
        xn a1 0 * xn a1 0 - (a * a - 1) * yn a1 0 * yn a1 0 = 1 ∧
          u * u - (a * a - 1) * v * v = 1 ∧
            s * s - (b * b - 1) * t * t = 1 ∧
              1 < b ∧
                b ≡ 1 [MOD 4 * yn a1 0] ∧
                  b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 0 * yn a1 0 ∣ v ∧ s ≡ xn a1 0 [MOD u] ∧ t ≡ 0 [MOD 4 * yn a1 0])
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case right
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
h₁ : ξ * ↑q.den < ↑q.num + 1
h₂ : ↑q.num < ξ * ↑q.den + 1
⊢ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1

Tactic:
]

Goal state after:
case right
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
h₁ : ξ * ↑q.den < ↑q.num + 1
h₂ : ↑q.num < ξ * ↑q.den + 1
⊢ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case right
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
h₁ : ξ * ↑q.den < ↑q.num + 1
h₂ : ↑q.num - 1 < ξ * ↑q.den
⊢ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1

Tactic:
]

Goal state after:
case right
ξ q : ℚ
hq₀ : 0 < ↑q.den
h : |ξ * ↑q.den - ↑q.num| < 1 / ↑q.den
h₁ : ξ * ↑q.den < ↑q.num + 1
h₂ : ↑q.num - 1 < ξ * ↑q.den
⊢ ⌈ξ * ↑q.den⌉ - 1 ≤ q.num ∧ q.num ≤ ⌊ξ * ↑q.den⌋ + 1
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | (v ∘ some, v none) ∈ f.graph}}
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ (v, (x ::ₒ v) none).2 ::ₒ v ∈ S

Tactic:
]

Goal state after:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S ∩ {v | (v ∘ some, v none) ∈ f.graph}}
x : ℕ
hS : x ::ₒ v ∈ S
hf : (f (v, (x ::ₒ v) none).1).Dom
h : (f (v, (x ::ₒ v) none).1).get hf = (v, (x ::ₒ v) none).2
⊢ (v, (x ::ₒ v) none).2 ::ₒ v ∈ S
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
a b : ℚ
hab : a.num = b.num ∧ a.den = b.den
⊢ ↑b.num / ↑b.den = ↑b.num / ↑b.den

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x✝¹ y✝ : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x✝¹ ∧ yn a1 k = y✝
a1 : 1 < a
hx : xn a1 k = x✝¹
hy : yn a1 k = y✝
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this✝ : xn a1 1 < u
this : a < u
⊢ a ≤ b

Tactic:
]

Goal state after:
a k x✝¹ y✝ : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x✝¹ ∧ yn a1 k = y✝
a1 : 1 < a
hx : xn a1 k = x✝¹
hy : yn a1 k = y✝
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this✝ : xn a1 1 < u
this : a < u
⊢ a ≤ b
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x✝¹ y✝ : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x✝¹ ∧ yn a1 k = y✝
a1 : 1 < a
hx : xn a1 k = x✝¹
hy : yn a1 k = y✝
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this✝ : xn a1 1 < u
this : a < u
⊢ b % u ≤ b

Tactic:
]

Goal state after:
a k x✝¹ y✝ : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x✝¹ ∧ yn a1 k = y✝
a1 : 1 < a
hx : xn a1 k = x✝¹
hy : yn a1 k = y✝
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b % u = a
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
this✝ : xn a1 1 < u
this : a < u
⊢ b % u ≤ b
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ (h : v ∈ f.Dom), f.fn v h ::ₒ v ∈ S}
x : v ∈ f.Dom
hS : f.fn v x ::ₒ v ∈ S
⊢ ∃ (h : (f (v, (f.fn v x ::ₒ v) none).1).Dom), (f (v, (f.fn v x ::ₒ v) none).1).get h = (v, (f.fn v x ::ₒ v) none).2

Tactic:
]

Goal state after:
α : Type u
S : Set (Option α → ℕ)
d : Dioph S
f : (α → ℕ) →. ℕ
df : DiophPFun f
v : α → ℕ
x✝ : v ∈ {v | ∃ (h : v ∈ f.Dom), f.fn v h ::ₒ v ∈ S}
x : v ∈ f.Dom
hS : f.fn v x ::ₒ v ∈ S
⊢ ∃ (h : (f (v, (f.fn v x ::ₒ v) none).1).Dom), (f (v, (f.fn v x ::ₒ v) none).1).get h = (v, (f.fn v x ::ₒ v) none).2
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x✝¹ y✝ : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x✝¹ ∧ yn a1 k = y✝
a1 : 1 < a
hx : xn a1 k = x✝¹
hy : yn a1 k = y✝
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b ≡ a [MOD u]
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
b1 : 1 < b
s : ℕ := xn b1 k
t : ℕ := yn b1 k
sx : s ≡ x [MOD u]
⊢ ↑(4 * y) ∣ ↑b - ↑1

Tactic:
]

Goal state after:
a k x✝¹ y✝ : ℕ
x✝ : ∃ (a1 : 1 < a), xn a1 k = x✝¹ ∧ yn a1 k = y✝
a1 : 1 < a
hx : xn a1 k = x✝¹
hy : yn a1 k = y✝
kpos : k > 0
x : ℕ := xn a1 k
y : ℕ := yn a1 k
m : ℕ := 2 * (k * y)
u : ℕ := xn a1 m
v : ℕ := yn a1 m
ky : k ≤ y
yv : y * y ∣ v
uco : u.Coprime (4 * y)
b : ℕ
ba : b ≡ a [MOD u]
bm1 : b ≡ 1 [MOD 4 * y]
m1 : 1 < m
vp : 0 < v
b1 : 1 < b
s : ℕ := xn b1 k
t : ℕ := yn b1 k
sx : s ≡ x [MOD u]
⊢ ↑(4 * y) ∣ ↑b - ↑1
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
x✝ :
  1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
a1 : 1 < a
ky : k ≤ 0
o :
  x = 1 ∧ y = 0 ∨
    ∃ u v s t b,
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
x1 : x = 1
y0 : y = 0
⊢ xn a1 k = x ∧ yn a1 k = y

Tactic:
]

Goal state after:
a k x y : ℕ
x✝ :
  1 < a ∧
    k ≤ y ∧
      (x = 1 ∧ y = 0 ∨
        ∃ u v s t b,
          x * x - (a * a - 1) * y * y = 1 ∧
            u * u - (a * a - 1) * v * v = 1 ∧
              s * s - (b * b - 1) * t * t = 1 ∧
                1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
a1 : 1 < a
ky : k ≤ 0
o :
  x = 1 ∧ y = 0 ∨
    ∃ u v s t b,
      x * x - (a * a - 1) * y * y = 1 ∧
        u * u - (a * a - 1) * v * v = 1 ∧
          s * s - (b * b - 1) * t * t = 1 ∧
            1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
x1 : x = 1
y0 : y = 0
⊢ xn a1 k = x ∧ yn a1 k = y
Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
⊢ Nat.card (DirichletCharacter R n) = Nat.card (ZMod n)ˣ

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
⊢ Nat.card (DirichletCharacter R n) = Nat.card (ZMod n)ˣ
Module: Mathlib.NumberTheory.DirichletCharacter.Orthogonality

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : NeZero n
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
⊢ Nat.card (DirichletCharacter R n) = n.totient

Tactic:
by
  rw [← ZMod.card_units_eq_totient n, ← Nat.card_eq_fintype_card]
  exact Nat.card_congr (mulEquiv_units R n).some.toEquiv

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: n : ℕ
S : Set (Vector3 ℕ n.succ)
d : Dioph S
v : Fin2 n → ℕ
x : ℕ
⊢ (x :: v) ∈ S ↔ (x :: v) ∈ S

Tactic:
]

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

Goal state before:
pp: ξ : ℝ
a b : ℤ
x✝ : b ≠ 0
h : ξ = ↑a / ↑b
q : ℚ
⊢ |↑a / ↑b - ↑q| < ↑(1 / ↑q.den ^ 2) ↔ |↑a / ↑b - q| < 1 / ↑q.den ^ 2

Tactic:
]

Goal state after:
ξ : ℝ
a b : ℤ
x✝ : b ≠ 0
h : ξ = ↑a / ↑b
q : ℚ
⊢ |↑a / ↑b - ↑q| < ↑(1 / ↑q.den ^ 2) ↔ |↑a / ↑b - q| < 1 / ↑q.den ^ 2