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

Goal state before:
pp: k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcast : ↑(∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = 0
T : ℤ
hT_int : (∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = ↑p * T
⊢ ∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + vonStaudtIndicator (2 * k) p = ↑p * ↑T

Tactic:
unfold vonStaudtIndicator

Goal state after:
k p : ℕ
hk : k > 0
inst✝ : Fact (Nat.Prime p)
hcast : ↑(∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = 0
T : ℤ
hT_int : (∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = ↑p * T
⊢ (∑ v ∈ Ico 1 p, ↑v ^ (2 * k) + if p - 1 ∣ 2 * k then 1 else 0) = ↑p * ↑T
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x x✝ : ℝ
| 1 / (x✝ * log x✝ ^ 2) * ∑ p ∈ Ioc 0 ⌊x✝⌋₊ with Nat.Prime p, log ↑p

Tactic:
sum_filter

Goal state after:
x x✝ : ℝ
| 1 / (x✝ * log x✝ ^ 2) * ∑ a ∈ Ioc 0 ⌊x✝⌋₊, if Nat.Prime a then log ↑a else 0
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ ↑(∑ x ∈ Icc 0 ⌊x⌋₊ with Nat.Prime x, 1) = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)

Tactic:
sum_filter

Goal state after:
x : ℝ
hx : 2 ≤ x
⊢ ↑(∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then 1 else 0) = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]ˣ
⊢ (↑x).zmodRepr ≠ 0

Tactic:
by
  rw [ne_eq, zmodRepr_eq_zero_iff_dvd]
  exact irreducible_p.not_dvd_isUnit x.isUnit

Goal state after:
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
⊢ ∑ p ∈ Icc 0 ⌊x⌋₊ with Nat.Prime p, log ↑p = ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t

Tactic:
sum_filter

Goal state after:
x : ℝ
hx : 2 ≤ x
⊢ (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log ↑a else 0) = ↑(π ⌊x⌋₊) * log x - ∫ (t : ℝ) in 2..x, ↑(π ⌊t⌋₊) / t
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ ↑(↑x.zmodRepr).val = ↑x.zmodRepr

Tactic:
rw [Nat.cast_inj]

Goal state after:
p' : ℕ
hp_prime : Fact (Nat.Prime (0 + p' + 1))
x : ℤ_[0 + p' + 1]
⊢ (↑x.zmodRepr).val = x.zmodRepr
Module: Mathlib.NumberTheory.Chebyshev

Goal state before:
pp: x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ IntegrableOn (deriv log) (Set.Icc 2 x) volume

Tactic:
deriv_log'

Goal state after:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (Set.ofPred Nat.Prime).indicator fun n ↦ 1
⊢ IntegrableOn Inv.inv (Set.Icc 2 x) volume
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case neg.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ (toZMod ↑(unitCoeff h) *
        0 ^
          match ↑(x - ↑(x.appr n)).valuation - ↑n with
          | Int.ofNat m => m
          | Int.negSucc m => m.succ).val ≤
    p - 1

Tactic:
apply le_pred_of_lt

Goal state after:
case neg.calc_1
p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
ih : ∀ (x : ℤ_[p]), x.appr n < p ^ n
x : ℤ_[p]
hp : p ^ n < p ^ (n + 1)
h : ¬x - ↑(x.appr n) = 0
⊢ (toZMod ↑(unitCoeff h) *
        0 ^
          match ↑(x - ↑(x.appr n)).valuation - ↑n with
          | Int.ofNat m => m
          | Int.negSucc m => m.succ).val <
    p.sub 0
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: p : ℕ
hp_prime : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
h : (toZModPow n) x = 0
this : x.appr n = 0
⊢ x ∈ Ideal.span {↑p ^ n}

Tactic:
convert! appr_spec n x
      simp only [this, sub_zero, cast_zero]

Goal state after:
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
j : ℕ
⊢ j ≥ k → padicNorm p ((fun n ↦ ↑(nthHom f r n)) j - (fun n ↦ ↑(nthHom f r n)) k) < ε

Tactic:
hj

Goal state after:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r : R
ε : ℚ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
j : ℕ
hj : j ≥ k
⊢ padicNorm p ((fun n ↦ ↑(nthHom f r n)) j - (fun n ↦ ↑(nthHom f r n)) k) < ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
⊢ j ≥ 1 → padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε

Tactic:
hj

Goal state after:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
ε : ℚ
hε : 0 < ε
j : ℕ
hj : j ≥ 1
⊢ padicNorm p (↑(nthHomSeq f_compat 1 - 1) j) < ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
⊢ j ≥ n → padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε

Tactic:
hj

Goal state after:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHomSeq f_compat (r + s) - (nthHomSeq f_compat r + nthHomSeq f_compat s)) j) < ε
Module: Mathlib.NumberTheory.Padics.RingHoms

Goal state before:
pp: case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
⊢ j ≥ n → padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε

Tactic:
hj

Goal state after:
case h
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
r s : R
ε : ℚ
hε : ε > 0
n : ℕ
hn : ↑p ^ (-↑n) < ε
j : ℕ
hj : j ≥ n
⊢ padicNorm p (↑(nthHomSeq f_compat (r * s) - nthHomSeq f_compat r * nthHomSeq f_compat s) j) < ε
Module: Mathlib.NumberTheory.Cyclotomic.Gal

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ✝ : IsPrimitiveRoot μ n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
h : Irreducible (cyclotomic n K)
hζ : IsPrimitiveRoot (zeta n K L) n := zeta_spec n K L
hμ : ∀ (t : (ZMod n)ˣ), IsPrimitiveRoot (zeta n K L ^ (↑t).val) n :=
  fun t ↦ IsPrimitiveRoot.pow_of_coprime hζ (↑t).val (ZMod.val_coe_unit_coprime t)
t : (ZMod n)ˣ
⊢ minpoly K (IsPrimitiveRoot.powerBasis K hζ).gen = minpoly K (IsPrimitiveRoot.powerBasis K ⋯).gen

Tactic:
by
          have := IsCyclotomicExtension.neZero' n K L
          simp only [IsPrimitiveRoot.powerBasis_gen]
          have hr :=
            IsPrimitiveRoot.minpoly_eq_cyclotomic_of_irreducible
              ((zeta_spec n K L).pow_of_coprime _ (ZMod.val_coe_unit_coprime t)) h
          exact ((zeta_spec n K L).minpoly_eq_cyclotomic_of_irreducible h).symm.trans hr

Goal state after:
Module: Mathlib.RingTheory.Discriminant

Goal state before:
pp: K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : (algebraMap R K) r = discr K ⇑B.basis • (B.basis.repr z) i
⊢ (discr K ⇑B.basis • (B.basis.repr z) i) • B.basis i ∈ R[B.gen]

Tactic:
← hr,

Goal state after:
K : Type u
L : Type v
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Module.Finite K L
R : Type z
inst✝⁶ : CommRing R
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R K L
inst✝² : Algebra.IsSeparable K L
inst✝¹ : IsIntegrallyClosed R
inst✝ : IsFractionRing R K
B : PowerBasis K L
hint : IsIntegral R B.gen
z : L
hz : IsIntegral R z
hinv : IsUnit (traceMatrix K ⇑B.basis).det
H :
  (traceMatrix K ⇑B.basis).det • traceMatrix K ⇑B.basis *ᵥ B.basis.equivFun z =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
cramer :
  (traceMatrix K ⇑B.basis *ᵥ (traceMatrix K ⇑B.basis).cramer fun i ↦ (trace K L) (z * B.basis i)) =
    (traceMatrix K ⇑B.basis).det • fun i ↦ (trace K L) (z * B.basis i)
i : Fin B.dim
x✝ : i ∈ univ
r : R
hr : (algebraMap R K) r = discr K ⇑B.basis • (B.basis.repr z) i
⊢ (algebraMap R K) r • B.basis i ∈ R[B.gen]
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
⊢ a ^ (n + 1) ≤ xn a1 (n + 1)

Tactic:
simp only [_root_.pow_succ, xn_succ]
    exact le_trans (Nat.mul_le_mul_right _ (xn_ge_a_pow n)) (Nat.le_add_right _ _)

Goal state after:
Module: Mathlib.NumberTheory.PellMatiyasevic

Goal state before:
pp: a : ℕ
a1 : 1 < a
n : ℕ
b : ℤ√↑(d a1)
h1 : 1 ≤ b
hp : IsPell b
h : b ≤ pellZd a1 (n + 1)
a1p : 0 ≤ { re := ↑a, im := 1 }
am1p : 0 ≤ { re := ↑a, im := -1 }
a1m : { re := ↑a, im := 1 } * { re := ↑a, im := -1 } = 1
ha : { re := ↑a, im := 1 } ≤ b
m : ℕ
e : b * { re := ↑a, im := -1 } = pellZd a1 m
⊢ b = pellZd a1 (m + 1)

Tactic:
rw [show b = b * ⟨a, -1⟩ * ⟨a, 1⟩ by rw [mul_assoc, Eq.trans (mul_comm _ _) a1m]; simp,
          pellZd_succ, e]

Goal state after:
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ 0 ≤ (sumsq (p :: ps)) x

Tactic:
rw [sumsq]

Goal state after:
α : Type u_1
x : α → ℕ
p : Poly α
ps : List (Poly α)
⊢ 0 ≤ (p * p + sumsq ps) x
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 := -↑x, im := ↑y } * { re := ↑z, im := ↑w }).Nonneg

Tactic:
rw [mul_comm]; exact nonneg_mul_lem ha

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
x✝ : { re := ↑z, im := ↑w }.Nonneg
⊢ ({ re := ↑x, im := -↑y } * { re := ↑z, im := ↑w }).Nonneg

Tactic:
rw [mul_comm]; exact nonneg_mul_lem ha

Goal state after:
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
⊢ m * m = d * (n * n)

Tactic:
refine mul_left_cancel₀ (mul_pos gpos gpos).ne' ?_

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
⊢ g * g * (m * m) = g * g * (d * (n * n))
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inl
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
a : α ⊕ β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl a) = ((v ⊗ x) ⊗ t) (inl a)

Tactic:
cases a

Goal state after:
case inl.inl
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
val✝ : α
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inl val✝)) = ((v ⊗ x) ⊗ t) (inl (inl val✝))

case inl.inr
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
val✝ : β
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inr val✝)) = ((v ⊗ x) ⊗ t) (inl (inr val✝))
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inr
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
b : γ
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ x) ⊗ t) (inr b)

Tactic:
cases a

Goal state after:
case inr
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, v ⊗ x ∈ S}
x : β → ℕ
hx : v ⊗ x ∈ S
t : γ → ℕ
ht : p ((v ⊗ x) ⊗ t) = 0
b : γ
⊢ ((v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inr b) = ((v ⊗ x) ⊗ t) (inr b)
Module: Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions

Goal state before:
pp: ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
⊢ ∃ n, (GenContFract.of ξ).convs n = ↑q

Tactic:
obtain ⟨n, hn⟩ := exists_rat_eq_convergent h

Goal state after:
ξ : ℝ
q : ℚ
h : |ξ - ↑q| < 1 / (2 * ↑q.den ^ 2)
n : ℕ
hn : q = ξ.convergent n
⊢ ∃ n, (GenContFract.of ξ).convs n = ↑q
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
cases a

Goal state after:
case inl.inl
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
val✝ : α
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inl val✝)) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl (inl val✝))

case inl.inr
α β : Type u
S : Set (α ⊕ β → ℕ)
γ : Type u
p : Poly ((α ⊕ β) ⊕ γ)
pe : ∀ (v : α ⊕ β → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : ∃ t, (Poly.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) p) (v ⊗ t) = 0
t : β ⊕ γ → ℕ
ht : p ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) = 0
val✝ : β
⊢ ((v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr)) (inl (inr val✝)) = ((v ⊗ t ∘ inl) ⊗ t ∘ inr) (inl (inr val✝))
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
cases a

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

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

Tactic:
cases a

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

case inl.some
α : Type u
S : Set (Option α → ℕ)
β : Type u
p : Poly (Option α ⊕ β)
pe : ∀ (v : Option α → ℕ), v ∈ S ↔ ∃ t, p (v ⊗ t) = 0
v : α → ℕ
x✝ : v ∈ {v | ∃ x, x ::ₒ v ∈ S}
x : ℕ
hx : x ::ₒ v ∈ S
t : β → ℕ
ht : p (x ::ₒ v ⊗ t) = 0
val✝ : α
⊢ ((v ⊗ x ::ₒ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl (some val✝)) = (x ::ₒ v ⊗ t) (inl (some val✝))
Module: Mathlib.NumberTheory.Dioph

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

Tactic:
cases a

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

Goal state before:
pp: case inl
α : 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 ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
a : Option α
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl a) = (t none ::ₒ v ⊗ t ∘ some) (inl a)

Tactic:
cases a

Goal state after:
case inl.none
α : 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 ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl none) = (t none ::ₒ v ⊗ t ∘ some) (inl none)

case inl.some
α : 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 ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
val✝ : α
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inl (some val✝)) = (t none ::ₒ v ⊗ t ∘ some) (inl (some val✝))
Module: Mathlib.NumberTheory.Dioph

Goal state before:
pp: case inr
α : 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 ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
b : β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (t none ::ₒ v ⊗ t ∘ some) (inr b)

Tactic:
cases a

Goal state after:
case inr
α : 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 ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) = 0
b : β
⊢ ((v ⊗ t) ∘ (inr none ::ₒ inl ⊗ inr ∘ some)) (inr b) = (t none ::ₒ v ⊗ t ∘ some) (inr b)
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
⊢ n = m ^ 2 * l.primeFactorsList.toFinset.prod id

Tactic:
← H₁

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.EulerProduct.Basic

Goal state before:
pp: 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 : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
N₀ : ℕ
hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ⊆ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
s : Finset ℕ
hs : s ⊇ range N₀
⊢ dist (∏ b ∈ s, {x | Nat.Prime x}.mulIndicator F b) (∑'[{ filter := Filter.atTop }] (n : ℕ), f n) < ε

Tactic:
have : ∏ p ∈ s, {p | Nat.Prime p}.mulIndicator F p = ∏ p ∈ s with p.Prime, F p :=
    prod_mulIndicator_eq_prod_filter s (fun _ ↦ F) _ id

Goal state after:
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 : Summable fun x ↦ ‖f x‖
hf₀ : f 0 = 0
F : ℕ → R := fun n ↦ ∑' (e : ℕ), f (n ^ e)
ε : ℝ
hε : ε > 0
N₀ : ℕ
hN₀ : ∀ (s : Finset ℕ), N₀.primesBelow ⊆ s → ‖∑' (m : ℕ), f m - ∑' (m : ↑(factoredNumbers s)), f ↑m‖ < ε
s : Finset ℕ
hs : s ⊇ range N₀
this : ∏ p ∈ s, {p | Nat.Prime p}.mulIndicator F p = ∏ p ∈ s with Nat.Prime p, F p
⊢ dist (∏ b ∈ s, {x | Nat.Prime x}.mulIndicator F b) (∑'[{ filter := Filter.atTop }] (n : ℕ), f n) < ε
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
x✝ : ℕ
⊢ (toArithmeticFunction f) x✝ = (toArithmeticFunction f') x✝

Tactic:
simp_all [toArithmeticFunction]

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

Goal state before:
pp: case h.inr.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
⊢ ∃ n, ↑u = ξ.convergent n

Tactic:
rcases le_or_gt (u : ℝ) ξ with ht | ht

Goal state after:
case h.inr.inl.inl
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ↑u ≤ ξ
⊢ ∃ n, ↑u = ξ.convergent n

case h.inr.inl.inr
ξ : ℝ
u : ℤ
ih : ∀ m < 1, ∀ {ξ : ℝ} {u : ℤ}, ContfracLegendre.Ass ξ u ↑m → ∃ n, ↑u / ↑m = ξ.convergent n
left✝ : IsCoprime u ↑1
h₁ : ↑1 = 1 → -(1 / 2) < ξ - ↑u
h₂ : |ξ - ↑u / ↑↑1| < (↑↑1 * (2 * ↑↑1 - 1))⁻¹
ht : ξ < ↑u
⊢ ∃ n, ↑u = ξ.convergent n
Module: Mathlib.NumberTheory.LSeries.MellinEqDirichlet

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)

Tactic:
have hs' : s ≠ 0 := fun h ↦ lt_irrefl _ (zero_re ▸ h ▸ hs)

Goal state after:
ι : Type u_1
inst✝ : Countable ι
a : ι → ℂ
p : ι → ℝ
F : ℝ → ℂ
s : ℂ
hp : ∀ (i : ι), 0 ≤ p i
hs : 0 < s.re
hF : ∀ t ∈ Ioi 0, HasSum (fun i ↦ if p i = 0 then 0 else a i * ↑(rexp (-π * p i * t))) (F t)
h_sum : Summable fun i ↦ ‖a i‖ / p i ^ s.re
hs' : s ≠ 0
⊢ HasSum (fun i ↦ ↑π ^ (-s) * Complex.Gamma s * a i / ↑(p i) ^ s) (mellin F s)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds

Goal state before:
pp: k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
⊢ F_int k (↑a) t = F_nat k a t + F_nat k (1 - a) t

Tactic:
simp only [F_int, F_nat, Function.Periodic.lift_coe]

Goal state after:
k : ℕ
a : ℝ
ha : a ∈ Icc 0 1
t : ℝ
ht : 0 < t
⊢ ∑' (n : ℤ), f_int k a t n = ∑' (n : ℕ), f_nat k a t n + ∑' (n : ℕ), f_nat k (1 - a) t n