mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
a b : ℤ√d
⊢ star (a * b) = star b * star a

Tactic:
ext

Goal state after:
case re
d : ℤ
a b : ℤ√d
⊢ (star (a * b)).re = (star b * star a).re

case im
d : ℤ
a b : ℤ√d
⊢ (star (a * b)).im = (star b * star a).im
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ 0 * x✝ = 0

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (0 * x✝¹) x✝ = 0 x✝
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d n : ℤ
⊢ ↑n = { re := n, im := 0 }

Tactic:
ext

Goal state after:
case re
d n : ℤ
⊢ (↑n).re = { re := n, im := 0 }.re

case im
d n : ℤ
⊢ (↑n).im = { re := n, im := 0 }.im
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ : Poly α
⊢ x✝ * 0 = 0

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝¹ * 0) x✝ = 0 x✝
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d n : ℤ
⊢ ofInt n = ↑n

Tactic:
ext

Goal state after:
case re
d n : ℤ
⊢ (ofInt n).re = (↑n).re

case im
d n : ℤ
⊢ (ofInt n).im = (↑n).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
n : ℕ
x y : ℤ
⊢ ↑n * { re := x, im := y } = { re := ↑n * x, im := ↑n * y }

Tactic:
ext

Goal state after:
case re
d : ℤ
n : ℕ
x y : ℤ
⊢ (↑n * { re := x, im := y }).re = { re := ↑n * x, im := ↑n * y }.re

case im
d : ℤ
n : ℕ
x y : ℤ
⊢ (↑n * { re := x, im := y }).im = { re := ↑n * x, im := ↑n * y }.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d n x y : ℤ
⊢ ↑n * { re := x, im := y } = { re := n * x, im := n * y }

Tactic:
ext

Goal state after:
case re
d n x y : ℤ
⊢ (↑n * { re := x, im := y }).re = { re := n * x, im := n * y }.re

case im
d n x y : ℤ
⊢ (↑n * { re := x, im := y }).im = { re := n * x, im := n * y }.im
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝² x✝¹ x✝ : Poly α
⊢ x✝² * (x✝¹ + x✝) = x✝² * x✝¹ + x✝² * x✝

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝³ * (x✝² + x✝¹)) x✝ = (x✝³ * x✝² + x✝³ * x✝¹) x✝
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y : ℤ
⊢ sqrtd * { re := x, im := y } = { re := d * y, im := x }

Tactic:
ext

Goal state after:
case re
d x y : ℤ
⊢ (sqrtd * { re := x, im := y }).re = { re := d * y, im := x }.re

case im
d x y : ℤ
⊢ (sqrtd * { re := x, im := y }).im = { re := d * y, im := x }.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
⊢ sqrtd * sqrtd = ↑d

Tactic:
ext

Goal state after:
case re
d : ℤ
⊢ (sqrtd * sqrtd).re = (↑d).re

case im
d : ℤ
⊢ (sqrtd * sqrtd).im = (↑d).im
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝² x✝¹ x✝ : Poly α
⊢ (x✝² + x✝¹) * x✝ = x✝² * x✝ + x✝¹ * x✝

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝³ x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ ((x✝³ + x✝²) * x✝¹) x✝ = (x✝³ * x✝¹ + x✝² * x✝¹) x✝
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d n x y : ℤ
⊢ sqrtd * ↑n * { re := x, im := y } = { re := d * n * y, im := n * x }

Tactic:
ext

Goal state after:
case re
d n x y : ℤ
⊢ (sqrtd * ↑n * { re := x, im := y }).re = { re := d * n * y, im := n * x }.re

case im
d n x y : ℤ
⊢ (sqrtd * ↑n * { re := x, im := y }).im = { re := d * n * y, im := n * x }.im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y : ℤ
⊢ { re := x, im := y } = ↑x + sqrtd * ↑y

Tactic:
ext

Goal state after:
case re
d x y : ℤ
⊢ { re := x, im := y }.re = (↑x + sqrtd * ↑y).re

case im
d x y : ℤ
⊢ { re := x, im := y }.im = (↑x + sqrtd * ↑y).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d x y : ℤ
⊢ { re := x, im := y } * star { re := x, im := y } = ↑x * ↑x - ↑d * ↑y * ↑y

Tactic:
ext

Goal state after:
case re
d x y : ℤ
⊢ ({ re := x, im := y } * star { re := x, im := y }).re = (↑x * ↑x - ↑d * ↑y * ↑y).re

case im
d x y : ℤ
⊢ ({ re := x, im := y } * star { re := x, im := y }).im = (↑x * ↑x - ↑d * ↑y * ↑y).im
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝¹ x✝ : Poly α
⊢ x✝¹ * x✝ = x✝ * x✝¹

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
x✝² x✝¹ : Poly α
x✝ : α → ℕ
⊢ (x✝² * x✝¹) x✝ = (x✝¹ * x✝²) x✝
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d z : ℤ
a : ℤ√d
⊢ ↑z ∣ a ↔ z ∣ a.re ∧ z ∣ a.im

Tactic:
constructor

Goal state after:
case mp
d z : ℤ
a : ℤ√d
⊢ ↑z ∣ a → z ∣ a.re ∧ z ∣ a.im

case mpr
d z : ℤ
a : ℤ√d
⊢ z ∣ a.re ∧ z ∣ a.im → ↑z ∣ a
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_1
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
intro xy

Goal state after:
case refine_1
d x y z w : ℕ
xy : SqLe x 1 y d
⊢ SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_2
d x y z w : ℕ
⊢ SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d

Tactic:
intro xy

Goal state after:
case refine_2
d x y z w : ℕ
xy : SqLe x 1 y d
⊢ SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_3
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d

Tactic:
intro xy

Goal state after:
case refine_3
d x y z w : ℕ
xy : SqLe y d x 1
⊢ SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case refine_4
d x y z w : ℕ
⊢ SqLe y d x 1 → SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1

Tactic:
intro xy

Goal state after:
case refine_4
d x y z w : ℕ
xy : SqLe y d x 1
⊢ SqLe w d z 1 → SqLe (x * w + y * z) d (x * z + d * y * w) 1
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
n : ℤ√d
⊢ ↑n.norm = n * star n

Tactic:
ext

Goal state after:
case re
d : ℤ
n : ℤ√d
⊢ (↑n.norm).re = (n * star n).re

case im
d : ℤ
n : ℤ√d
⊢ (↑n.norm).im = (n * star n).im
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: d : ℤ
hd : d < 0
z : ℤ√d
⊢ z.norm = 0 ↔ z = 0

Tactic:
constructor

Goal state after:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
⊢ z.norm = 0 → z = 0

case mpr
d : ℤ
hd : d < 0
z : ℤ√d
⊢ z = 0 → z.norm = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.norm = 0
⊢ z = 0

Tactic:
rw [norm_def, sub_eq_add_neg, mul_assoc] at h

Goal state after:
case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
⊢ z = 0
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: case mp
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z = 0

Tactic:
ext

Goal state after:
case mp.re
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.re = re 0

case mp.im
d : ℤ
hd : d < 0
z : ℤ√d
h : z.re * z.re + -(d * (z.im * z.im)) = 0
left : 0 ≤ z.re * z.re
right : 0 ≤ -(d * (z.im * z.im))
ha : z.re * z.re = 0
hb : -(d * (z.im * z.im)) = 0
⊢ z.im = im 0
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ pellZd a1 (n + 2) + pellZd a1 n = ↑(2 * a) * pellZd a1 (n + 1)

Tactic:
ext

Goal state after:
case re
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 2) + pellZd a1 n).re = (↑(2 * a) * pellZd a1 (n + 1)).re

case im
a : ℕ
a1 : 1 < a
n : ℕ
⊢ (pellZd a1 (n + 2) + pellZd a1 n).im = (↑(2 * a) * pellZd a1 (n + 1)).im
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) * (↑(xn a1 j) * ↑(yn a1 n)) + ↑(xn a1 j)

Tactic:
rw [mul_comm (xn _ _ : ℤ)]

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
⊢ 0 ≤ a → 0 ≤ b → 0 ≤ a * b

Tactic:
simp_rw [← nonneg_iff_zero_le]
  exact nonneg_mul

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

Goal state before:
pp: case pos
p : ℕ
K : Type u
L : Type v
ζ : L
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
hp : Fact (Nat.Prime p)
k : ℕ
hcycl : IsCyclotomicExtension {p ^ (k + 1)} K L
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
hirr : Irreducible (cyclotomic (p ^ (k + 1)) K)
hk : p ^ (k + 1) = 2
⊢ discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
    (-1) ^ (φ (p ^ (k + 1)) / 2) * ↑p ^ (p ^ (k + 1 - 1) * ((p - 1) * (k + 1) - 1))

Tactic:
obtain rfl : p = 2 := by
        rw [← pow_one 2] at hk
        exact eq_of_prime_pow_eq (prime_iff.1 hp.out) (prime_iff.1 Nat.prime_two) (succ_pos _) hk
      nth_rw 2 [← pow_one 2] at hk
      replace hk := Nat.pow_right_injective rfl.le hk
      rw [add_eq_right] at hk
      subst hk
      rw [pow_one] at hζ hcycl
      have : natDegree (minpoly K ζ) = 1 := by
        rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp,
          minpoly.eq_X_sub_C_of_algebraMap_inj _ (FaithfulSMul.algebraMap_injective K L)]
        exact natDegree_X_sub_C (-1)
      rcases Fin.equiv_iff_eq.2 this with ⟨e⟩
      rw [← Algebra.discr_reindex K (hζ.powerBasis K).basis e, coe_basis, powerBasis_gen]
      simp only [powerBasis_dim,
        zero_add, pow_one, totient_two, reduceDiv, pow_zero, cast_ofNat, tsub_self,
        Nat.add_one_sub_one, mul_one, mul_zero]
      simp_rw [hζ.eq_neg_one_of_two_right, show (-1 : L) = algebraMap K L (-1) by simp]
      convert_to (discr K fun i : Fin 1 ↦ (algebraMap K L) (-1) ^ ↑i) = _
      · congr 1
        ext i
        simp only [map_neg, map_one, Function.comp_apply, Fin.val_eq_zero, _root_.pow_zero]
        suffices (e.symm i : ℕ) = 0 by simp [this]
        rw [← Nat.lt_one_iff]
        convert! (e.symm i).2
        rw [this]
      · simp only [discr, traceMatrix_apply, Matrix.det_unique, Fin.default_eq_zero, Fin.val_zero,
          _root_.pow_zero, traceForm_apply, mul_one]
        rw [← (algebraMap K L).map_one, trace_algebraMap, finrank _ hirr]; simp

Goal state after:
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:
Int.ofNat_sub xle

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
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))
Module: Mathlib.NumberTheory.Zsqrtd.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
d : ℤ
f : ℤ√d →+* R
⊢ (fun r ↦ { toFun := fun a ↦ ↑a.re + ↑a.im * ↑r, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
      ((fun f ↦ ⟨f sqrtd, ⋯⟩) f) =
    f

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : CommRing R
d : ℤ
f : ℤ√d →+* R
⊢ ((fun r ↦ { toFun := fun a ↦ ↑a.re + ↑a.im * ↑r, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ })
        ((fun f ↦ ⟨f sqrtd, ⋯⟩) f))
      sqrtd =
    f sqrtd
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

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

Tactic:
constructor

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

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

Goal state before:
pp: ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
⊢ f '' s ⊆ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}

Tactic:
intro xy

Goal state after:
ξ : ℚ
f : ℚ → ℤ × ℕ := fun q ↦ (q.num, q.den)
s : Set ℚ := {q | |ξ - q| < 1 / ↑q.den ^ 2}
hinj : Function.Injective f
xy : ℤ × ℕ
⊢ xy ∈ f '' s → xy ∈ ⋃ y ∈ Ioc 0 ξ.den, Icc (⌈ξ * ↑y⌉ - 1) (⌊ξ * ↑y⌋ + 1) ×ˢ {y}
Module: Mathlib.NumberTheory.SmoothNumbers

Goal state before:
pp: s : Finset ℕ
p : ℕ
hp : Prime p
hs : p ∉ s
e m : ℕ
hm₀ : m ≠ 0
hm : ∀ p ∈ m.primeFactorsList, p ∈ s
hpm : ¬p ∣ m
⊢ (p ^ e * m).factorization p = e ∧ (List.filter (fun x ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m

Tactic:
constructor

Goal state after:
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
⊢ (p ^ e * m).factorization p = e

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
⊢ (List.filter (fun x ↦ decide (x ∈ s)) (p ^ e * m).primeFactorsList).prod = m
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
⊢ l.primeFactorsList.toFinset ∈ k.primesBelow.powerset

Tactic:
simp only [toFinset_factors, Finset.mem_powerset]

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
⊢ l.primeFactors ⊆ k.primesBelow
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
⊢ x % y = z

Tactic:
by
              rw [← hc]; simp only [add_mul_mod_self_left]; rcases h with x0 | hl
              · rw [x0, mod_zero]
              exact mod_eq_of_lt hl

Goal state after:
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
⊢ i = k

Tactic:
clear o rem xy uv st

Goal state after:
a k x y : ℕ
a1 : 1 < a
ky✝ : k ≤ y
u v s t b : ℕ
b1 : 1 < b
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])
ipos : i > 0
⊢ i = k
Module: Mathlib.NumberTheory.EulerProduct.Basic

Goal state before:
pp: case pos
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)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))

Tactic:
constructor

Goal state after:
case pos.left
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)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ Summable fun m ↦ ‖f ↑m‖

case pos.right
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)‖
p : ℕ
s : Finset ℕ
hp : p ∉ s
ih : (Summable fun m ↦ ‖f ↑m‖) ∧ HasSum (fun m ↦ f ↑m) (∏ p ∈ s with Nat.Prime p, ∑' (n : ℕ), f (p ^ n))
hpp : Nat.Prime p
⊢ HasSum (fun m ↦ f ↑m) (∏ x ∈ insert p ({p ∈ s | Nat.Prime p}), ∑' (n : ℕ), f (x ^ n))
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: m n k : ℕ
⊢ n ^ k = m ↔
    k = 0 ∧ m = 1 ∨
      0 < k ∧
        (n = 0 ∧ m = 0 ∨
          0 < n ∧
            ∃ w a t z,
              ∃ (a1 : 1 < a),
                xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧
                  2 * a * n = t + (n * n + 1) ∧
                    m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)

Tactic:
constructor

Goal state after:
case mp
m n k : ℕ
⊢ n ^ k = m →
    k = 0 ∧ m = 1 ∨
      0 < k ∧
        (n = 0 ∧ m = 0 ∨
          0 < n ∧
            ∃ w a t z,
              ∃ (a1 : 1 < a),
                xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧
                  2 * a * n = t + (n * n + 1) ∧
                    m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1)

case mpr
m n k : ℕ
⊢ k = 0 ∧ m = 1 ∨
      0 < k ∧
        (n = 0 ∧ m = 0 ∨
          0 < n ∧
            ∃ w a t z,
              ∃ (a1 : 1 < a),
                xn a1 k ≡ yn a1 k * (a - n) + m [MOD t] ∧
                  2 * a * n = t + (n * n + 1) ∧
                    m < t ∧ n ≤ w ∧ k ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1) →
    n ^ k = m
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: R : Type u_1
inst✝ : Zero R
f f' : ℕ → R
h : ∀ {n : ℕ}, n ≠ 0 → f n = f' n
⊢ toArithmeticFunction f = toArithmeticFunction f'

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : Zero R
f f' : ℕ → R
h : ∀ {n : ℕ}, n ≠ 0 → f n = f' n
x✝ : ℕ
⊢ (toArithmeticFunction f) x✝ = (toArithmeticFunction f') x✝
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: case mpr.inr.inr
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w a t z : ℕ
a1 : 1 < a
tm : xn a1 k ≡ yn a1 k * (a - n) + m [MOD t]
ta : 2 * a * n = t + (n * n + 1)
mt : m < t
nw : n ≤ w
kw : k ≤ w
zp : a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
hw0 : 0 < w
hw1 : 1 < w + 1
⊢ n ^ k = m

Tactic:
rcases eq_pell hw1 zp with ⟨j, rfl, yj⟩

Goal state after:
case mpr.inr.inr
m n k : ℕ
hk0 : 0 < k
hn0 : 0 < n
w t z : ℕ
mt : m < t
nw : n ≤ w
kw : k ≤ w
hw0 : 0 < w
hw1 : 1 < w + 1
j : ℕ
yj : w * z = yn hw1 j
a1 : 1 < xn hw1 j
tm : xn a1 k ≡ yn a1 k * (xn hw1 j - n) + m [MOD t]
ta : 2 * xn hw1 j * n = t + (n * n + 1)
zp : xn hw1 j * xn hw1 j - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1
⊢ n ^ k = m
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f ⍟ g) s n = ∑ p ∈ n.divisorsAntidiagonal, term f s p.1 * term g s p.2

Tactic:
rcases eq_or_ne n 0 with rfl | hn
  · simp
  -- now `n ≠ 0`
  rw [term_of_ne_zero hn, convolution_def, Finset.sum_div]
  refine Finset.sum_congr rfl fun p hp ↦ ?_
  have ⟨hp₁, hp₂⟩ := ne_zero_of_mem_divisorsAntidiagonal hp
  rw [term_of_ne_zero hp₁, term_of_ne_zero hp₂, mul_comm_div, div_div, ← mul_div_assoc,
    ← natCast_mul_natCast_cpow, ← cast_mul, mul_comm p.2, (mem_divisorsAntidiagonal.mp hp).1]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
⊢ (fun p ↦ p.1 * p.2) ⁻¹' {0} = {0} ×ˢ univ ∪ univ ×ˢ {0}

Tactic:
ext

Goal state after:
f g : ℕ → ℂ
s : ℂ
x✝ : ℕ × ℕ
⊢ x✝ ∈ (fun p ↦ p.1 * p.2) ⁻¹' {0} ↔ x✝ ∈ {0} ×ˢ univ ∪ univ ×ˢ {0}
Module: Mathlib.NumberTheory.LSeries.Convolution

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
⊢ (fun p ↦ p.1 * p.2) ⁻¹' {n} = ↑n.divisorsAntidiagonal

Tactic:
ext

Goal state after:
f g : ℕ → ℂ
s : ℂ
n : ℕ
hn : n ≠ 0
x✝ : ℕ × ℕ
⊢ x✝ ∈ (fun p ↦ p.1 * p.2) ⁻¹' {n} ↔ x✝ ∈ ↑n.divisorsAntidiagonal
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
⊢ ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹

Tactic:
sub_eq_iff_eq_add'.mp huv

Goal state after:
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
⊢ ↑(⌊ξ⌋ * v + 1) / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

Goal state before:
pp: case refine_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : fract ξ < 2 / (2 * ↑v - 1)
⊢ (2 * ↑v - 1) / 2 < (fract ξ)⁻¹

Tactic:
lt_inv_comm₀ (div_pos hv₀' zero_lt_two) (aux₁ hv h),

Goal state after:
case refine_2
ξ : ℝ
u v : ℤ
hv : 2 ≤ v
h : ContfracLegendre.Ass ξ u v
huv : u - ⌊ξ⌋ * v = 1
hv₀' : 0 < 2 * ↑v - 1
Hv : (↑v * (2 * ↑v - 1))⁻¹ + (↑v)⁻¹ = 2 / (2 * ↑v - 1)
Huv : ↑u / ↑v = ↑⌊ξ⌋ + (↑v)⁻¹
h' : fract ξ < 2 / (2 * ↑v - 1)
⊢ fract ξ < ((2 * ↑v - 1) / 2)⁻¹
Module: Mathlib.NumberTheory.DiophantineApproximation.Basic

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

Tactic:
by norm_cast

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable

Goal state before:
pp: S T : ℝ
hT : 0 < T
z τ : ℂ
hz : |z.im| ≤ S
hτ : T ≤ τ.im
n : ℤ
⊢ ‖jacobiTheta₂_term n z τ‖ ≤ rexp (-π * (T * ↑n ^ 2 - 2 * S * ↑|n|))

Tactic:
simp_rw [norm_jacobiTheta₂_term, Real.exp_le_exp, sub_eq_add_neg, neg_mul, ← neg_add,
    neg_le_neg_iff, mul_comm (2 : ℝ), mul_assoc π, ← mul_add, mul_le_mul_iff_right₀ pi_pos,
    mul_comm T, mul_comm S]
  refine add_le_add (mul_le_mul le_rfl hτ hT.le (sq_nonneg _)) ?_
  rw [← mul_neg, mul_assoc, mul_assoc, mul_le_mul_iff_right₀ two_pos, mul_comm, neg_mul, ← mul_neg]
  refine le_trans ?_ (neg_abs_le _)
  rw [mul_neg, neg_le_neg_iff, abs_mul, Int.cast_abs]
  exact mul_le_mul_of_nonneg_left hz (abs_nonneg _)

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖↑n ^ k * rexp (-π * ((↑n + a) ^ 2 * t))‖ ≤
    ↑|↑n| ^ k * (rexp (-π * (t * ↑↑n ^ 2 - 2 * (|a| * (t * ↑|↑n|)))) * rexp (-π * (a ^ 2 * t)))

Tactic:
← Real.exp_add,

Goal state after:
k : ℕ
a t : ℝ
ht : 0 < t
n : ℕ
⊢ ‖↑n ^ k * rexp (-π * ((↑n + a) ^ 2 * t))‖ ≤
    ↑|↑n| ^ k * rexp (-π * (t * ↑↑n ^ 2 - 2 * (|a| * (t * ↑|↑n|))) + -π * (a ^ 2 * t))