mathlib-initiative/mathlib-tactics huggingface dataset:
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 0 = 1 ∧ yn a1 0 = 0

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 0 = 1 ∧ yn a1 0 = 0
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : Prime p ∧ p ∣ k
⊢ Prime p ∧ p ∣ m

Tactic:
]

Goal state after:
s : Finset ℕ
m k : ℕ
h' : k ∣ m
h₁ : m ≠ 0
h₂ : ∀ p ∈ m.primeFactorsList, p ∈ s
hk : k ≠ 0
p : ℕ
hp : Prime p ∧ p ∣ k
⊢ Prime p ∧ p ∣ m
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
⊢ False

Tactic:
]

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
⊢ False
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
⊢ (m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s) ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s

Tactic:
]

Goal state after:
s : Finset ℕ
m p : ℕ
hp₁ : 1 + s.sup id ≤ p
hp₂ : Prime p
⊢ (m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p ∈ s) ↔ ∀ (p : ℕ), Prime p → p ∣ m → p ∈ s
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m : ℕ
hm : m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ m.primeFactors ⊆ s

Tactic:
]

Goal state after:
s : Finset ℕ
m : ℕ
hm : m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
⊢ m.primeFactors ⊆ s
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
m : ℕ
hm : m ≠ 0
hp : m.primeFactors ⊆ s
⊢ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s

Tactic:
]

Goal state after:
s : Finset ℕ
m : ℕ
hm : m ≠ 0
hp : m.primeFactors ⊆ s
⊢ m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p ∈ s
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
h' : ↑⌊ξ⌋ - ↑u / ↑v = (↑⌊ξ⌋ * ↑v - ↑u) / ↑v
⊢ 1 ≤ |↑⌊ξ⌋ * ↑v - ↑u|

Tactic:
]

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
h' : ↑⌊ξ⌋ - ↑u / ↑v = (↑⌊ξ⌋ * ↑v - ↑u) / ↑v
⊢ 1 ≤ |↑⌊ξ⌋ * ↑v - ↑u|
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
rem : b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 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 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
o :
  xn a1 i = 1 ∧ yn a1 i = 0 ∨
    ∃ u v s t b,
      xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 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 i] ∧
                b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i]
xy : xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1
uv : xn a1 n * xn a1 n - (a * a - 1) * yn a1 n * yn a1 n = 1
st : xn b1 j * xn b1 j - (b * b - 1) * yn b1 j * yn b1 j = 1
i0 : i = 0
ky : k = 0
⊢ xn a1 0 = xn a1 0 ∧ yn a1 0 = yn a1 0

Tactic:
]

Goal state after:
a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
rem : b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 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 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
o :
  xn a1 i = 1 ∧ yn a1 i = 0 ∨
    ∃ u v s t b,
      xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 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 i] ∧
                b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i]
xy : xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1
uv : xn a1 n * xn a1 n - (a * a - 1) * yn a1 n * yn a1 n = 1
st : xn b1 j * xn b1 j - (b * b - 1) * yn b1 j * yn b1 j = 1
i0 : i = 0
ky : k = 0
⊢ xn a1 0 = xn a1 0 ∧ yn a1 0 = yn a1 0
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case inl
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ q ∈ insert p s

Tactic:
]

Goal state after:
case inl
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ q ∈ insert p s
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case inl
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ p ∈ insert p s

Tactic:
]

Goal state after:
case inl
s : Finset ℕ
p n : ℕ
hp : Prime p
e : ℕ
hn : n ∈ factoredNumbers s
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ p ∈ insert p s
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ p ∉ n.primeFactorsList

Tactic:
]

Goal state after:
s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ p ∉ n.primeFactorsList
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case left
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ e = e

Tactic:
]

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
h' : ↑⌊ξ⌋ - ↑u / ↑v = (↑⌊ξ⌋ * ↑v - ↑u) / ↑v
⊢ ⌊ξ⌋ * v ≠ u

Tactic:
]

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hv₀ hv₁ : 0 < ↑v
hv₂ : 0 < 2 * ↑v - 1
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |↑⌊ξ⌋ - ↑u / ↑v| < (↑v * (2 * ↑v - 1))⁻¹
hf : ξ = ↑⌊ξ⌋
h' : ↑⌊ξ⌋ - ↑u / ↑v = (↑⌊ξ⌋ * ↑v - ↑u) / ↑v
⊢ ⌊ξ⌋ * v ≠ u
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case right
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ m.primeFactorsList ~ m.primeFactorsList

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
⊢ (replicate (List.count p m.primeFactorsList) p ++ List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod = m

Tactic:
]

Goal state after:
s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
m : ℕ
hm₀ : m ≠ 0
hm : ∀ p_1 ∈ m.primeFactorsList, p_1 ∈ insert p s
⊢ (replicate (List.count p m.primeFactorsList) p ++ List.filter (fun x ↦ decide (x ∈ s)) m.primeFactorsList).prod = m
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: n : ℕ
⊢ factoredNumbers (Finset.range n) = factoredNumbers n.primesBelow

Tactic:
]

Goal state after:
n : ℕ
⊢ factoredNumbers (Finset.range n) = factoredNumbers n.primesBelow
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: m₁ m₂ n : ℕ
hm1 : m₁ ∈ factoredNumbers (Finset.range n)
hm2 : m₂ ∈ factoredNumbers (Finset.range n)
⊢ m₁ * m₂ ∈ factoredNumbers (Finset.range n)

Tactic:
]

Goal state after:
m₁ m₂ n : ℕ
hm1 : m₁ ∈ factoredNumbers (Finset.range n)
hm2 : m₂ ∈ factoredNumbers (Finset.range n)
⊢ m₁ * m₂ ∈ factoredNumbers (Finset.range n)
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1}
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ (z + y * c) % y = z

Tactic:
]

Goal state after:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1}
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
h : y = 0 ∨ z < y
c : ℕ
hc : z + y * c = x
⊢ (z + y * c) % y = z
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |ξ - ↑u / ↑v| * |↑v * (2 * ↑v - 1)| < 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v

Tactic:
← abs_mul,

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : |(ξ - ↑u / ↑v) * (↑v * (2 * ↑v - 1))| < 1
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case inl
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ q < p.succ

Tactic:
]

Goal state after:
case inl
p n : ℕ
hp : p ≠ 0
e : ℕ
hn : n ∈ p.smoothNumbers
this : NoZeroDivisors ℕ
hp' : p ^ e ≠ 0
q : ℕ
hq : q ∈ (p ^ e * n).primeFactorsList
H : Prime q ∧ q ∣ p ^ e
⊢ q < p.succ
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
rem : b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 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 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
o :
  xn a1 i = 1 ∧ yn a1 i = 0 ∨
    ∃ u v s t b,
      xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 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 i] ∧
                b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i]
xy : xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1
uv : xn a1 n * xn a1 n - (a * a - 1) * yn a1 n * yn a1 n = 1
st : xn b1 j * xn b1 j - (b * b - 1) * yn b1 j * yn b1 j = 1
ipos : i > 0
this : i = k
⊢ xn a1 k = xn a1 k ∧ yn a1 k = yn a1 k

Tactic:
]

Goal state after:
a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
rem : b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y]
i n j : ℕ
bm1 : b ≡ 1 [MOD 4 * yn a1 i]
ba : b ≡ a [MOD xn a1 n]
vp : 0 < yn a1 n
yv : yn a1 i * yn a1 i ∣ yn a1 n
sx : xn b1 j ≡ xn a1 i [MOD xn a1 n]
tk : yn b1 j ≡ k [MOD 4 * yn a1 i]
ky : k ≤ yn a1 i
x✝ :
  1 < a ∧
    k ≤ yn a1 i ∧
      (xn a1 i = 1 ∧ yn a1 i = 0 ∨
        ∃ u v s t b,
          xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 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 i] ∧
                    b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i])
o :
  xn a1 i = 1 ∧ yn a1 i = 0 ∨
    ∃ u v s t b,
      xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 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 i] ∧
                b ≡ a [MOD u] ∧ 0 < v ∧ yn a1 i * yn a1 i ∣ v ∧ s ≡ xn a1 i [MOD u] ∧ t ≡ k [MOD 4 * yn a1 i]
xy : xn a1 i * xn a1 i - (a * a - 1) * yn a1 i * yn a1 i = 1
uv : xn a1 n * xn a1 n - (a * a - 1) * yn a1 n * yn a1 n = 1
st : xn b1 j * xn b1 j - (b * b - 1) * yn b1 j * yn b1 j = 1
ipos : i > 0
this : i = k
⊢ xn a1 k = xn a1 k ∧ yn a1 k = yn a1 k
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ #({x ∈ Finset.range (N + 1) | x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers}) = N

Tactic:
]

Goal state after:
N k : ℕ
⊢ #({x ∈ Finset.range (N + 1) | x ∈ k.smoothNumbers ∨ x ≠ 0 ∧ x ∉ k.smoothNumbers}) = N
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v

Tactic:
]

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ 0 < u - ⌊ξ⌋ * v ∧ u - ⌊ξ⌋ * v < v
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
this : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
hn' : ∀ (n : ℕ), n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0
⊢ #({n ∈ Finset.range N.succ | n ≠ 0}) = N

Tactic:
]

Goal state after:
N k : ℕ
this : #({x ∈ Finset.range (N + 1) | x ≠ 0}) = N
hn' : ∀ (n : ℕ), n ∈ k.smoothNumbers ∨ n ≠ 0 ∧ n ∉ k.smoothNumbers ↔ n ≠ 0
⊢ #({n ∈ Finset.range N.succ | n ≠ 0}) = N
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ #(Finset.range N.succ) - 1 = N

Tactic:
]

Goal state after:
N k : ℕ
⊢ #(Finset.range N.succ) - 1 = N
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case refine_1
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
p : ℕ
hp : Prime p ∧ p ∣ l ∧ l ≠ 0
⊢ p < k

Tactic:
]

Goal state after:
case refine_1
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
p : ℕ
hp : Prime p ∧ p ∣ l ∧ l ≠ 0
⊢ p < k
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)

Tactic:
]

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
h : -1 + ξ * (↑v * (2 * ↑v - 1)) < ↑u * (2 * ↑v - 1) ∧ ↑u * (2 * ↑v - 1) < 1 + ξ * (↑v * (2 * ↑v - 1))
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inl
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1}
z x y : ℕ
x✝ : (y = 0 ∨ z < y) ∧ ∃ c, z + y * c = x
c : ℕ
hc : z + y * c = x
x0 : y = 0
⊢ z = z

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case refine_2
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ m ^ 2 * l = m ^ 2 * l.primeFactorsList.toFinset.prod id

Tactic:
]

Goal state after:
case refine_2
n k : ℕ
h : n ∈ k.smoothNumbers
l m : ℕ
H₁ : m ^ 2 * l = n
H₂ : Squarefree l
hl : l ∈ k.smoothNumbers
⊢ m ^ 2 * l = m ^ 2 * l.primeFactorsList.toFinset.prod id
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1}
z x y : ℕ
e : x % y = z
⊢ (y = 0 ∨ x % y < y) ∧ ∃ c, x % y + y * c = x

Tactic:
]

Goal state after:
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | (v &2 = 0 ∨ v &0 < v &2) ∧ ∃ x, v &0 + v &2 * x = v &1}
z x y : ℕ
e : x % y = z
⊢ (y = 0 ∨ x % y < y) ∧ ∃ c, x % y + y * c = x
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
h : -1 < (↑u - ξ * ↑v) * (2 * ↑v - 1)
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)

Tactic:
]

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
h : -1 < (↑u - ξ * ↑v) * (2 * ↑v - 1)
⊢ -1 < (u - ⌊ξ⌋ * v) * (2 * v - 1)
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ^ 2 ≤ N

Tactic:
]

Goal state after:
case refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ^ 2 ≤ N
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ^ 2 * 1 ≤ m ^ 2 * s.prod id

Tactic:
]

Goal state after:
case refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m ^ 2 * 1 ≤ m ^ 2 * s.prod id
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case refine_2
N k n : ℕ
hn : n ∈ N.smoothNumbersUpTo k
hn₁ : n ≤ N
hn₂ : n ∈ k.smoothNumbers
s : Finset ℕ
hs : s ∈ k.primesBelow.powerset
m : ℕ
hm : n = m ^ 2 * s.prod id
⊢ m < N.sqrt + 1

Tactic:
rw [Nat.lt_succ_iff, le_sqrt']
    refine LE.le.trans ?_ (hm ▸ hn₁)
    nth_rw 1 [← mul_one (m ^ 2)]
    gcongr
    exact Finset.one_le_prod' fun p hp ↦
      (prime_of_mem_primesBelow <| Finset.mem_powerset.mp hs hp).one_le

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: case e'_4
N k : ℕ
⊢ 2 ^ #k.primesBelow * N.sqrt = #(k.primesBelow.powerset ×ˢ (Finset.range (N.sqrt + 1)).erase 0)

Tactic:
simp only [Finset.card_product, Finset.card_powerset, Finset.mem_range, zero_lt_succ,
    Finset.card_erase_of_mem, Finset.card_range, succ_sub_succ_eq_sub, Nat.sub_zero]

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

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1) < ↑v * (2 * ↑v - 1) + 1
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1

Tactic:
]

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
hcop : IsCoprime u v
left✝ : v = 1 → -(1 / 2) < ξ - ↑u
hv₀ : 0 < ↑v
hv₀' : 0 < 2 * ↑v - 1
hv₁ : 0 < 2 * v - 1
hu₀ : 0 ≤ u - ⌊ξ⌋ * v
h : (↑u - ξ * ↑v) * (2 * ↑v - 1) + ↑v * (2 * ↑v - 1) < ↑v * (2 * ↑v - 1) + 1
⊢ (u - ⌊ξ⌋ * v) * (2 * v - 1) < v * (2 * v - 1) + 1
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ N.roughNumbersUpTo k =
    ((N + 1).primesBelow \ k.primesBelow).biUnion fun p ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}

Tactic:
by
  ext m
  simp only [roughNumbersUpTo, mem_smoothNumbers_iff_forall_le, not_and, not_forall,
    not_lt, exists_prop, Finset.mem_range, Finset.mem_filter,
    Finset.mem_biUnion, Finset.mem_sdiff, mem_primesBelow,
    show ∀ P Q : Prop, P ∧ (P → Q) ↔ P ∧ Q by tauto]
  simp_rw [← exists_and_left, ← not_lt]
  refine exists_congr fun p ↦ ?_
  have H : m ≠ 0 → p ∣ m → ¬ m < p :=
    fun h₁ h₂ ↦ not_lt.mpr <| le_of_dvd (Nat.pos_of_ne_zero h₁) h₂
  grind

Goal state after:
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: N k : ℕ
⊢ #(((N + 1).primesBelow \ k.primesBelow).biUnion fun p ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}) ≤
    ∑ p ∈ (N + 1).primesBelow \ k.primesBelow, N / p

Tactic:
]

Goal state after:
N k : ℕ
⊢ #(((N + 1).primesBelow \ k.primesBelow).biUnion fun p ↦ {m ∈ Finset.range (N + 1) | m ≠ 0 ∧ p ∣ m}) ≤
    ∑ p ∈ (N + 1).primesBelow \ k.primesBelow, N / p
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inr
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2}
z x y : ℕ
hy : y > 0
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < z * y + y ↔ z * y ≤ x ∧ x ≤ z * y + y - 1

Tactic:
]

Goal state after:
case inr
α : Type
f g : (α → ℕ) → ℕ
df : DiophFn f
dg : DiophFn g
this : Dioph {v | v &2 = 0 ∧ v &0 = 0 ∨ v &0 * v &2 ≤ v &1 ∧ v &1 < (v &0 + 1) * v &2}
z x y : ℕ
hy : y > 0
⊢ y = 0 ∧ z = 0 ∨ z * y ≤ x ∧ x < z * y + y ↔ z * y ≤ x ∧ x ≤ z * y + y - 1
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: case empty
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ ∅ with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))

Tactic:
]

Goal state after:
case empty
R : Type u_1
inst✝¹ : NormedCommRing R
f : ℕ → R
inst✝ : CompleteSpace R
hf₁ : f 1 = 1
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
hsum : ∀ {p : ℕ}, Nat.Prime p → Summable fun n ↦ ‖f (p ^ n)‖
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ ∅ with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))