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

Goal state before:
pp: m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ ((↑m)⁻¹ • ∫ (x : ℝ) in ↑m * 0..↑m * (↑m)⁻¹, bernoulliFun (k + 1) x) -
      ∫ (x : ℝ) in 0..(↑m)⁻¹, ↑m ^ (k + 1) / ↑m * ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m) =
    0

pp: case hf
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ IntervalIntegrable (fun x ↦ bernoulliFun (k + 1) (↑m * x)) volume 0 (↑m)⁻¹

pp: case hg
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ IntervalIntegrable (fun x ↦ ↑m ^ (k + 1) / ↑m * ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m)) volume 0
    (↑m)⁻¹

Tactic:
mul_zero,

Goal state after:
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ ((↑m)⁻¹ • ∫ (x : ℝ) in 0..↑m * (↑m)⁻¹, bernoulliFun (k + 1) x) -
      ∫ (x : ℝ) in 0..(↑m)⁻¹, ↑m ^ (k + 1) / ↑m * ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m) =
    0

case hf
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ IntervalIntegrable (fun x ↦ bernoulliFun (k + 1) (↑m * x)) volume 0 (↑m)⁻¹

case hg
m : ℕ
m0 : m ≠ 0
x : ℝ
m0' : ↑m ≠ 0
f : ℕ → ℝ → ℝ := fun k x ↦ bernoulliFun k (↑m * x) - ↑m ^ k / ↑m * ∑ i ∈ Finset.range m, bernoulliFun k (x + ↑i / ↑m)
k : ℕ
h : ∀ (x : ℝ), f k x = 0
d : ∀ (x : ℝ), HasDerivAt (f (k + 1)) 0 x
c : ℝ
fc : ∀ (x : ℝ), f (k + 1) x = c
⊢ IntervalIntegrable (fun x ↦ ↑m ^ (k + 1) / ↑m * ∑ i ∈ Finset.range m, bernoulliFun (k + 1) (x + ↑i / ↑m)) volume 0
    (↑m)⁻¹
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: x : ℝ
hx : x ∈ Icc 0 1
k : ℕ
hk : k.succ ≠ 0
⊢ hurwitzZetaOdd (↑x) (1 - 2 * ↑k.succ) = 0

Tactic:
Nat.cast_succ,

Goal state after:
x : ℝ
hx : x ∈ Icc 0 1
k : ℕ
hk : k.succ ≠ 0
⊢ hurwitzZetaOdd (↑x) (1 - 2 * (↑k + 1)) = 0
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
this : ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s = 0
⊢ ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s + ↑N ^ (-s) * 0 =
    ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s

Tactic:
mul_zero,

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
this : ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s = 0
⊢ ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s + 0 =
    ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
⊢ completedLFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s

Tactic:
by
  suffices ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s = 0 by
    rw [completedLFunction, this, mul_zero, add_zero]
  refine (hΦ.mul_odd fun j ↦ ?_).sum_eq_zero
  rw [map_neg, completedHurwitzZetaOdd_neg]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case inl
k : ℕ
hk : k ≠ 0
⊢ 0 = -↑k ! / (2 * ↑π * I * 0) ^ k

Tactic:
mul_zero,

Goal state after:
case inl
k : ℕ
hk : k ≠ 0
⊢ 0 = -↑k ! / 0 ^ k
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
this : ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0
⊢ ↑N ^ (-s) * 0 + ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s =
    ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s

Tactic:
mul_zero,

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
this : ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0
⊢ 0 + ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s =
    ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x / ↑m ^ ↑x = ((↑m / (↑n + 1)) ^ ↑x)⁻¹

Tactic:
simp_rw [div_eq_mul_inv]

Goal state after:
case e_a
m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ (↑n + 1) ^ ↑x * (↑m ^ ↑x)⁻¹ = ((↑m * (↑n + 1)⁻¹) ^ ↑x)⁻¹
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
⊢ Tendsto (fun x ↦ (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))

Tactic:
obtain ⟨y, hay, hyt⟩ := exists_between ha

Goal state after:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : EReal
hay : abscissaOfAbsConv f < y
hyt : y < ⊤
⊢ Tendsto (fun x ↦ (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x) =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * (fourier (-↑n)) ↑x

Tactic:
mul_add,

Goal state after:
case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (fourier ↑n) ↑x + 1 / ↑n ^ k * ((-1) ^ k * (fourier (-↑n)) ↑x) =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * (fourier (-↑n)) ↑x
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * ((fourier ↑n) ↑x + (-1) ^ k * (fourier (-↑n)) ↑x) =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / ↑(-↑n) ^ k * (fourier (-↑n)) ↑x

Tactic:
rw [Int.cast_neg, mul_add, ← mul_assoc]

Goal state after:
case e'_5
k : ℕ
hk : 2 ≤ k
x : ℝ
hx : x ∈ Icc 0 1
n : ℕ
⊢ 1 / ↑n ^ k * (fourier ↑n) ↑x + 1 / ↑n ^ k * (-1) ^ k * (fourier (-↑n)) ↑x =
    1 / ↑↑n ^ k * (fourier ↑n) ↑x + 1 / (-↑↑n) ^ k * (fourier (-↑n)) ↑x
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: case inl
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
⊢ (1 / 0) ^ 3 * 0 * 1 = 0

Tactic:
mul_zero,

Goal state after:
case inl
N : ℕ
χ : DirichletCharacter ℂ N
inst✝ : NeZero N
t : ℝ
h : χ ^ 2 ≠ 1 ∨ t ≠ 0
Hz : LFunction χ (1 + I * ↑t) = 0
hz₁ : t ≠ 0 ∨ χ ≠ 1
hz₂ : 2 * t ≠ 0 ∨ χ ^ 2 ≠ 1
⊢ 0 * 1 = 0
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_5
k : ℕ
hk : k ≠ 0
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * 0)

Tactic:
mul_zero,

Goal state after:
case e'_5
k : ℕ
hk : k ≠ 0
n : ℕ
⊢ 1 / ↑n ^ (2 * k) = 1 / ↑n ^ (2 * k) * Real.cos 0
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ LSeries f s = s * ∫ (t : ℝ) in Set.Ioi 1, (∑ k ∈ Icc 1 ⌊t⌋₊, f k) * ↑t ^ (-(s + 1))

Tactic:
rw [← integral_const_mul]

Goal state after:
f : ℕ → ℂ
hf : f 0 = 0
r : ℝ
hr : 0 ≤ r
s : ℂ
hs : r < s.re
hS : LSeriesSummable f s
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
h₄ : ∀ (n : ℕ), ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k
hO : (fun n ↦ ∑ k ∈ Icc 0 n, f k) =O[atTop] fun n ↦ ↑n ^ r
⊢ LSeries f s = ∫ (a : ℝ) in Set.Ioi 1, s * ((∑ k ∈ Icc 1 ⌊a⌋₊, f k) * ↑a ^ (-(s + 1)))
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑((∏ x ∈ Ico 1 (p / 2).succ, a) * ↑(p / 2)!)

Tactic:
prod_const,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ ↑a ^ (p / 2) * ↑(p / 2)! = ↑(a ^ #(Ico 1 (p / 2).succ) * ↑(p / 2)!)
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : Nontrivial (ValueGroupWithZero R)ˣ
H : Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))
⊢ IsDiscrete R

Tactic:
nonempty_orderIso_withZeroMul_int_iff

Goal state after:
case neg
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : Nontrivial (ValueGroupWithZero R)ˣ
H : IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R)
⊢ IsDiscrete R
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_3
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
⊢ ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)

Tactic:
have ht' : 0 < t := hT₀.trans ht

Goal state after:
case refine_3
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
t : ℝ
ht : t ∈ Set.Ioi T
ht' : 0 < t
⊢ ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε * t ^ (-s)
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
⊢ legendreSym p ↑a = (-1) ^ ∑ x ∈ Ico 1 (p / 2).succ, x * a / p

Tactic:
by
  have hp' : Fact (p % 2 = 1) := ⟨(Nat.Prime.mod_two_eq_one_iff_ne_two Fact.out).mpr hp⟩
  have ha0' : ((a : ℤ) : ZMod p) ≠ 0 := by norm_cast
  rw [neg_one_pow_eq_pow_mod_two, gauss_lemma hp ha0', neg_one_pow_eq_pow_mod_two,
    (by norm_cast : ((a : ℤ) : ZMod p) = (a : ZMod p)),
    show _ = _ from eisenstein_lemma_aux p ha1 ha0]

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x : R
hx : x * ϖ ^ n ∈ I * I ^ n
⊢ x ∈ I

Tactic:
· rw [← pow_succ', hI, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx
      obtain ⟨y, hy⟩ := hx
      rw [mul_comm, pow_succ, mul_assoc, mul_right_inj' (pow_ne_zero _ _)] at hy
      · rw [hI, Ideal.mem_span_singleton]
        exact ⟨y, hy⟩
      · contrapose h'
        rw [hI, h', Ideal.span_singleton_eq_bot]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: m₁ m₂ n : ℕ
⊢ qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n

Tactic:
simp_rw [qrSign, Nat.cast_mul, map_mul, jacobiSym.mul_left]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a x y : ℕ
⊢ qrSign (x * y) a * J(↑(x * y) | a) = qrSign x a * J(↑x | a) * (qrSign y a * J(↑y | a))

Tactic:
simp_rw [qrSign.mul_left x y a, Nat.cast_mul, mul_left, mul_mul_mul_comm]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
b : ℕ
hb : Odd b
⊢ J(↑0 | b) = J(↑0 | b % (4 * 0))

Tactic:
mul_zero,

Goal state after:
case inl
b : ℕ
hb : Odd b
⊢ J(↑0 | b) = J(↑0 | b % 0)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : v ↑p < 1
n : ℕ
hn : ‖↑p‖ ^ n < ε
hF : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
⊢ Set.univ ⊆ ⋃ y ∈ Quotient.out '' Set.univ, Metric.ball y ε

Tactic:
have : {y : 𝒪[K] | v (y : K) ≤ v (p : K) ^ n} = Metric.closedBall 0 (‖p‖ ^ n) := by
      ext
      simp [← norm_pow]

Goal state after:
case mpr
K : Type u_1
Γ₀ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ₀
inst✝² : Valued K Γ₀
inst✝¹ : v.RankOne
inst✝ : IsDiscreteValuationRing ↥𝒪[K]
H : Finite 𝓀[K]
ε : ℝ
εpos : ε > 0
p : ↥𝒪[K]
hp : Irreducible p
hp' : v ↑p < 1
n : ℕ
hn : ‖↑p‖ ^ n < ε
hF : Finite (↥𝒪[K] ⧸ 𝓂[K] ^ n)
this : {y | v ↑y ≤ v ↑p ^ n} = Metric.closedBall 0 (‖p‖ ^ n)
⊢ Set.univ ⊆ ⋃ y ∈ Quotient.out '' Set.univ, Metric.ball y ε
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : ValuativeRel K
inst✝² : UniformSpace K
inst✝¹ : IsUniformAddGroup K
inst✝ : IsNonarchimedeanLocalField K
f : ℕ → ↥𝒪[K]
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD 𝓂[K] ^ m • ⊤]
S : ℕ → Set ↥𝒪[K] := fun n ↦ f n +ᵥ ↑(𝓂[K] ^ n)
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
L : ↥𝒪[K]
hL : L ∈ ⋂ i, S i
⊢ ∃ L, ∀ (n : ℕ), f n ≡ L [SMOD 𝓂[K] ^ n • ⊤]

Tactic:
refine ⟨L, fun n ↦ ?_⟩

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : ValuativeRel K
inst✝² : UniformSpace K
inst✝¹ : IsUniformAddGroup K
inst✝ : IsNonarchimedeanLocalField K
f : ℕ → ↥𝒪[K]
hf : ∀ {m n : ℕ}, m ≤ n → f m ≡ f n [SMOD 𝓂[K] ^ m • ⊤]
S : ℕ → Set ↥𝒪[K] := fun n ↦ f n +ᵥ ↑(𝓂[K] ^ n)
hS : ∀ (n : ℕ), S (n + 1) ⊆ S n
h : ∀ (n : ℕ), IsClosed (S n)
L : ↥𝒪[K]
hL : L ∈ ⋂ i, S i
n : ℕ
⊢ f n ≡ L [SMOD 𝓂[K] ^ n • ⊤]
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ (s - 1) * s * (Cs + ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1)) ≤
    (s - 1) * s * C + s * ((s - 1) * ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1))

Tactic:
mul_add,

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ (s - 1) * s * Cs + (s - 1) * s * ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤
    (s - 1) * s * C + s * ((s - 1) * ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1))
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' * (ω ^ 2 ^ p' + ωb ^ 2 ^ p') = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1

Tactic:
mul_add,

Goal state after:
case h
p' : ℕ
k : ℤ
h : ω ^ 2 ^ p' * ω ^ 2 ^ p' + ω ^ 2 ^ p' * ωb ^ 2 ^ p' = ω ^ 2 ^ p' * ↑((2 ^ (p' + 2) - 1) * k)
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_2
inst✝ : Ring R
𝒢 : Subgroup (GL n R)
⊢ 𝒢.adjoinNegOne.relIndex 𝒢 ≠ 0

Tactic:
by simp [Subgroup.relIndex_eq_one.mpr 𝒢.le_adjoinNegOne]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
⊢ 𝒢.adjoinNegOne.HasDetPlusMinusOne ↔ 𝒢.HasDetPlusMinusOne

Tactic:
refine ⟨fun _ ↦ ⟨fun {g} hg ↦ HasDetPlusMinusOne.det_eq (𝒢.le_adjoinNegOne hg)⟩, fun _ ↦ ⟨?_⟩⟩

Goal state after:
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
⊢ ∀ {g : GL n R}, g ∈ 𝒢.adjoinNegOne → GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k : ℤ
A : GL (Fin 2) ℝ
f : ℍ → ℂ
c : ℂ
τ : ℍ
⊢ ((c • f) ∣[k] A) τ = ((σ A) c • f ∣[k] A) τ

Tactic:
simp only [slash_apply, Pi.smul_apply, smul_eq_mul, map_mul, mul_assoc]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case coe
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : DecidableEq K
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsPrincipalIdealRing A
q : K
g : SL(2, A)
hg0 : ↑g 0 0 = IsFractionRing.num A q
hg1 : ↑g 1 0 = ↑(IsFractionRing.den A q)
⊢ ∃ g, (mapGL K) g • ∞ = ↑q

Tactic:
exact ⟨g, by simp [hg0, hg1, smul_infty_eq_ite]⟩

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
a b : SL(2, ℤ)
hab : a⁻¹ * b ∈ Subgroup.comap (mapGL ℝ) 𝒢
⊢ (fun m ↦ m • ⟨(mapGL ℝ) b⁻¹ • ∞, ⋯⟩) ⟨(mapGL ℝ) (a⁻¹ * b), hab⟩ = ⟨(mapGL ℝ) a⁻¹ • ∞, ⋯⟩

Tactic:
simp [mul_smul]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
this : GeneralLinearGroup.upperRightHom h • τ = h +ᵥ τ
⊢ f (h +ᵥ τ) = (⇑f ∣[k] GeneralLinearGroup.upperRightHom h) τ

Tactic:
slash_def,

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
this : GeneralLinearGroup.upperRightHom h • τ = h +ᵥ τ
⊢ f (h +ᵥ τ) =
    (σ (GeneralLinearGroup.upperRightHom h)) (f (GeneralLinearGroup.upperRightHom h • τ)) *
        ↑|↑(GeneralLinearGroup.det (GeneralLinearGroup.upperRightHom h))| ^ (k - 1) *
      denom (GeneralLinearGroup.upperRightHom h) ↑τ ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
inst✝ : SlashInvariantFormClass F Γ k
f : F
τ : ℍ
h : ℝ
hH : h ∈ Γ.strictPeriods
⊢ ↑(GeneralLinearGroup.upperRightHom h • τ) = ↑(h +ᵥ τ)

Tactic:
simp [σ, num, denom, coe_vadd, UpperHalfPlane.coe_smul, num, add_comm]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «1»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ * (↑z * ((starRingEnd ℂ) ↑(c 0) * (starRingEnd ℂ) ↑z + (starRingEnd ℂ) ↑(c 1))).im = c 1

Tactic:
mul_add,

Goal state after:
case «1»
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := Pi.normedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := π₀.smulRight ↑z + π₁.smulRight 1
f_def : ⇑f = fun p ↦ ↑(p 0) * ↑z + ↑(p 1)
this : (fun p ↦ normSq (↑(p 0) * ↑z + ↑(p 1))) = ⇑normSq ∘ ⇑f ∘ fun p ↦ Int.cast ∘ p
g : ℂ →ₗ[ℝ] Fin 2 → ℝ := LinearMap.pi ![imLm, imLm ∘ₗ (↑z • ↑↑conjAe)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ * (↑z * ((starRingEnd ℂ) ↑(c 0) * (starRingEnd ℂ) ↑z) + ↑z * (starRingEnd ℂ) ↑(c 1)).im = c 1
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
hfeq : f = fun τ ↦ update (cuspFunction h f) 0 (c 0) (𝕢 h ↑τ)
⊢ Tendsto f atImInfty (𝓝 (c 0))

Tactic:
hfeq

Goal state after:
h : ℝ
f : ℍ → ℂ
c : ℕ → ℂ
hh : 0 < h
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
hfeq : f = fun τ ↦ update (cuspFunction h f) 0 (c 0) (𝕢 h ↑τ)
⊢ Tendsto (fun τ ↦ update (cuspFunction h f) 0 (c 0) (𝕢 h ↑τ)) atImInfty (𝓝 (c 0))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
| ↑g

Tactic:
rw [(g : Matrix _ _ ℤ).eta_fin_two]

Goal state after:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
| !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1]
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : ∀ (g : SL(2, ℤ)), (fun τ ↦ f (g • τ)) =O[atImInfty] fun z ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst✝ : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
τ : ℍ
g h : SL(2, ℤ)
hgh : g ≈ h
⊢ f (g⁻¹ • τ) = f (h⁻¹ • τ)

Tactic:
by
    obtain ⟨j, hj, hj'⟩ : ∃ j ∈ Γ, h = g * j := by
      rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hgh
      exact ⟨g⁻¹ * h, hgh, (mul_inv_cancel_left g h).symm⟩
    simp [-sl_moeb, hj', mul_smul, hf_inv j⁻¹ (inv_mem hj)]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: τ : ℍ
h : τ ∈ 𝒟
⊢ 3 ≤ 4 * τ.im ^ 2

Tactic:
have : 1 ≤ τ.re * τ.re + τ.im * τ.im := by simpa [Complex.normSq_apply] using h.1
  cases abs_cases τ.re <;> nlinarith [h.2]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable

Goal state before:
pp: case h
k : ℤ
a : Fin 2 → ℤ
ha : a ≠ 0
⊢ (∀ x ∈ {z | 0 < z.im}, ↑(a 0) * x + ↑(a 1) ≠ 0) ∨ 0 ≤ -k

Tactic:
· left
      exact fun z hz ↦ linear_ne_zero ⟨z, hz⟩
        ((comp_ne_zero_iff _ Int.cast_injective Int.cast_zero).mpr ha)

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: α : Type u_1
f : ℤ → α
inst✝² : CommGroup α
inst✝¹ : TopologicalSpace α
inst✝ : ContinuousMul α
a : α
hf2 : Tendsto (fun N ↦ (f ↑N)⁻¹) atTop (𝓝 1)
hf : Tendsto ((fun s ↦ ∏ b ∈ s, f b) ∘ fun N ↦ Icc (-↑N) ↑N) atTop (𝓝 a)
⊢ Tendsto (((fun s ↦ ∏ b ∈ s, f b) ∘ fun N ↦ Ico (-N) N) ∘ Nat.cast / (fun s ↦ ∏ b ∈ s, f b) ∘ fun N ↦ Icc (-↑N) ↑N)
    atTop (𝓝 1)

Tactic:
simpa [Pi.div_def, fun N : ℕ ↦ prod_Icc_eq_prod_Ico_mul f (show (-N : ℤ) ≤ N by lia)]
    using hf2

Goal state after: