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

Goal state before:
pp: case inl
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
N : ℕ
x : ι → K
hp : IsHomogeneous 0 N
⊢ v ((eval x) 0) ≤ (⨆ s, v (coeff (↑s) 0)) * (⨆ i, v (x i)) ^ N

pp: case inr
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
⊢ v ((eval x) p) ≤ (⨆ s, v (coeff (↑s) p)) * (⨆ i, v (x i)) ^ N

Tactic:
· simp_all

Goal state after:
case inr
K : Type u_4
inst✝¹ : Field K
ι : Type u_5
inst✝ : Finite ι
v : AbsoluteValue K ℝ
hv : IsNonarchimedean ⇑v
p : MvPolynomial ι K
N : ℕ
hp : p.IsHomogeneous N
x : ι → K
hp₀ : p ≠ 0
⊢ v ((eval x) p) ≤ (⨆ s, v (coeff (↑s) p)) * (⨆ i, v (x i)) ^ N
Module: Mathlib.NumberTheory.Height.MvPolynomial

Goal state before:
pp: case c0
K : Type u_4
inst✝² : Field K
ι : Type u_5
ι' : Type u_6
inst✝¹ : AdmissibleAbsValues K
inst✝ : Finite ι'
p : ι' → MvPolynomial ι K
h : (fun j ↦ constantCoeff (p j)) ≠ 0
⊢ 0 ≤ ∏ᶠ (v : ↑nonarchAbsVal), ⨆ i, ↑v (constantCoeff (p i))

Tactic:
exact finprod_nonneg fun v ↦ Real.iSup_nonneg_of_nonnegHomClass ..

Goal state after:
Module: Mathlib.NumberTheory.Height.Projectivization

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : Projectivization K (ι → K)
⊢ Height.logHeight x.rep = log (Height.mulHeight x.rep)

Tactic:
Height.logHeight

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : AdmissibleAbsValues K
ι : Type u_2
inst✝ : Finite ι
x : Projectivization K (ι → K)
⊢ log (Height.mulHeight x.rep) = log (Height.mulHeight x.rep)
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: h : Tendsto (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this : Tendsto ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
⊢ (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ =ᶠ[𝓝[≠] 1] fun s ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)

Tactic:
have : {z | 0 < re z} ∈ 𝓝 (1 : ℂ) := by
    apply (continuous_re.isOpen_preimage _ isOpen_Ioi).mem_nhds
    simp only [mem_preimage, one_re, mem_Ioi, zero_lt_one]

Goal state after:
h : Tendsto (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this✝ : Tendsto ((fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ) (𝓝[≠] 1) (𝓝 (-(↑γ + Complex.log (4 * ↑π)) / 2))
this : {z | 0 < z.re} ∈ 𝓝 1
⊢ (fun b ↦ (b.Gammaℝ - 1) / (b - 1)) / Gammaℝ =ᶠ[𝓝[≠] 1] fun s ↦ 1 / (s - 1) - 1 / s.Gammaℝ / (s - 1)
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
ι : Type u_2
inst✝¹ : Finite ι
x : ι → 𝓞 K
inst✝ : Nonempty ι
hx : ∀ (i : ι), x i ≠ 0
H : ∀ (j : ι), span {x j} ≠ ⊥
hx' : ⨆ i, span {x i} ≠ ⊥
⊢ Function.HasFiniteMulSupport fun x_1 ↦
    ↑(absNorm (x_1.maximalIdeal.asIdeal ^ multiplicity x_1.maximalIdeal.asIdeal (⨆ i, span {x i})))

Tactic:
simp only [map_pow, Nat.cast_pow]
    exact hasFiniteMulSupport_fun_pow_multiplicity hx' fun v ↦ (v.absNorm : ℝ)

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.ZetaAsymp

Goal state before:
pp: s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
n : ℕ
⊢ 1 / (starRingEnd ℂ) ↑n ^ z = 1 / ↑n ^ z

Tactic:
conj_natCast

Goal state after:
s : ℂ
hs : s ≠ 1
hg_an : AnalyticOnNhd ℂ (fun z ↦ (starRingEnd ℂ) (riemannZeta ((starRingEnd ℂ) z))) {1}ᶜ
z : ℂ
hz : 1 < z.re
n : ℕ
⊢ 1 / ↑n ^ z = 1 / ↑n ^ z
Module: Mathlib.NumberTheory.JacobiSum.Basic

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
| ∑ x, χ x * χ⁻¹ (1 - x) = -χ (-1)

Tactic:
enter [1, 2, x]; rw [MulChar.inv_apply', ← map_mul, ← div_eq_mul_inv]

Goal state after:
F : Type u_1
R : Type u_2
inst✝³ : Field F
inst✝² : Fintype F
inst✝¹ : CommRing R
inst✝ : IsDomain R
χ : MulChar F R
hχ : χ ≠ 1
x : F
| χ (x / (1 - x))
Module: Mathlib.NumberTheory.Height.NumberField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
hv : ∀ (i : Fin 2), ↑(![a, ↑n] i) = ![↑a, ↑n] i
this : ↑n ^ (totalWeight K - 1) * ∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i) = 1
⊢ ↑n ^ ∑ v, v.mult ≤ ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult

Tactic:
← prod_pow_eq_pow_sum univ

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
n : ℕ
hn : n ≠ 0
a : 𝓞 K
ha₁ : ↑n * x = ↑a
ha₂ : Ideal.absNorm (Ideal.span {↑n, a}) = n ^ (totalWeight K - 1)
hv : ∀ (i : Fin 2), ↑(![a, ↑n] i) = ![↑a, ↑n] i
this : ↑n ^ (totalWeight K - 1) * ∏ᶠ (v : FinitePlace K), ⨆ i, v (![↑a, ↑n] i) = 1
⊢ ∏ i, ↑n ^ i.mult ≤ ∏ v, (⨆ i, v (![↑a, ↑n] i)) ^ v.mult
Module: Mathlib.NumberTheory.LSeries.DirichletContinuation

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
H :
  (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
| ∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)

Tactic:
rw [← mul_one <| Finset.prod ..]

Goal state after:
N : ℕ
inst✝ : NeZero N
H :
  (fun s ↦ (s - 1) * LFunctionTrivChar N s) =ᶠ[𝓝[≠] 1] fun s ↦
    (∏ p ∈ N.primeFactors, (1 - ↑p ^ (-s))) * ((s - 1) * riemannZeta s)
| (∏ p ∈ N.primeFactors, (1 - (↑p)⁻¹)) * 1
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:
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.LSeries.Linearity

Goal state before:
pp: f g : ℕ → ℂ
s : ℂ
n : ℕ
⊢ term (f - g) s n = term f s n - term g s n

Tactic:
by
  rw [term_sub, Pi.sub_apply]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x))
    ((-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))))

Tactic:
convert! ((hasSum_iff _ _).mp (this.div_const 2)).1 with n

Goal state after:
case e'_5
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
n : ℕ
⊢ 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * x) = (1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x) / 2).re

case e'_6
k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
ofReal_two : ↑2 = 2
⊢ (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! *
      Polynomial.eval x (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k))) =
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x) / 2).re
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ Summable fun p ↦ -log (1 - χ ↑↑p * ↑↑p ^ (-s))

Tactic:
refine (Nat.Primes.summable_rpow.mpr ?_).of_nonneg_of_le (fun _ ↦ norm_nonneg _) this
    |>.of_norm.clog_one_sub.neg

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
this : ∀ (p : Nat.Primes), ‖χ ↑↑p * ↑↑p ^ (-s)‖ ≤ ↑↑p ^ (-s).re
⊢ (-s).re < -1
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: 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
⊢ (s - 1) * ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε

Tactic:
have h {t : ℝ} (ht : 0 < t) : t ^ (-s) = t * t ^ (-s - 1) := by
    rw [Real.rpow_sub ht, Real.rpow_one, mul_div_cancel₀ _ ht.ne']

Goal state after:
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)
⊢ (s - 1) * ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = 1
⊢ J(a | b) ^ 2 = 1

Tactic:
rw [h₁]

Goal state after:
case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = 1
⊢ 1 ^ 2 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = -1
⊢ J(a | b) ^ 2 = 1

Tactic:
rw [h₁]

Goal state after:
case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = -1
⊢ (-1) ^ 2 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
h : a.gcd ↑b = 1
⊢ J(a | b) ^ 2 = 1

Tactic:
by
  rcases eq_one_or_neg_one h with h₁ | h₁ <;> rw [h₁] <;> rfl

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

Goal state before:
pp: case cons
n✝ : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n✝) = (List.map (fun a ↦ J(a | n✝)) l').prod
⊢ J((n :: l').prod | n✝) = (List.map (fun a ↦ J(a | n✝)) (n :: l')).prod

Tactic:
| cons n l' ih =>

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

Goal state before:
pp: case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n ↦ J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
⊢ J(a | (n :: l').prod) = (List.map (fun n ↦ J(a | n)) (n :: l')).prod

Tactic:
| cons n l' ih =>

Goal state after:
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 < ε
⊢ ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, Metric.ball y ε

Tactic:
have hF := finite_quotient_maximalIdeal_pow_of_finite_residueField H n

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)
⊢ ∃ t, t.Finite ∧ Set.univ ⊆ ⋃ y ∈ t, Metric.ball y ε
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).re < -1

Tactic:
rwa [neg_re, ofReal_re, neg_lt_neg_iff]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case neg
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
this : (∀ (i : K), IsOpen (U i)) → ↑𝒪[K] ⊆ ⋃ i, U i → ∃ t, ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
w : K
hw : ¬v w ≤ ↑↑z
⊢ IsOpen {w_1 | v w_1 = v w}

Tactic:
simp_rw [← v.restrict_inj]
      refine Valued.isOpen_sphere _ ?_
      push Not at hw
      rw [← map_zero v.restrict, ne_eq, v.restrict_inj]
      refine (hw.trans' ?_).ne'
      simp [z0]

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr.refine_1
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
⊢ (i : K) → i ∈ ↑t → (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ

Tactic:
refine fun i hi ↦ if hi' : v i ≤ z then z else Units.mk0 ⟨(v i), by simp⟩ ?_
    push Not at hi'
    exact Subtype.coe_injective.ne_iff.mp (hi'.trans' z0).ne'

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

Goal state before:
pp: case neg
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ J(a | b) = fastJacobiSymAux (a % ↑b).natAbs b false ⋯

Tactic:
rw [fastJacobiSymAux.eq_jacobiSym, if_neg Bool.false_ne_true, mod_left a b,
      Int.natAbs_of_nonneg (a.emod_nonneg (mod_cast hb0))]

Goal state after:
case neg.hb2
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b % 2 = 1

case neg.hb1
a : ℤ
b : ℕ
IH : ∀ m < b, J(a | m) = fastJacobiSym a m
hb0 : ¬b = 0
hb2 : ¬b % 2 = 0
hb1 : ¬b = 1
hab : ¬a % ↑b = 0
⊢ b > 1
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
C ε : ℝ
⊢ Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)

Tactic:
rw [show 𝓝 ε = 𝓝 ((1 - 1) * 1 * C + 1 * ε) by congr; ring]

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
C ε : ℝ
⊢ Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ((1 - 1) * 1 * C + 1 * ε))
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case inl
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
h✝ : p = 0
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1

pp: case inr
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hp : p ≠ 0
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1

Tactic:
· simp_all

Goal state after:
case inr
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hp : p ≠ 0
⊢ ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ω ^ 2 ^ (p' + 2) = (ω ^ 2 ^ (p' + 1)) ^ 2

Tactic:
by
      rw [← pow_mul, ← Nat.pow_succ]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case inr.mpr
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
n : ℤ
⊢ ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ {1} → ⟨(fun x ↦ g ^ x) n, ⋯⟩ ∈ Subtype.val ⁻¹' Set.Ioo (g ^ (-1)) (g ^ 1)

Tactic:
· simp_all

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
g : GL (Fin 2) K
⊢ g • ∞ = if ↑g 1 0 = 0 then ∞ else ↑(↑g 0 0 / ↑g 1 0)

Tactic:
by
  by_cases h : g 1 0 = 0 <;>
  simp [h, div_eq_inv_mul, smul_infty_def]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
⊢ (g ^ n).parabolicFixedPoint = g.parabolicFixedPoint

Tactic:
by
  rw [eq_comm, ← IsParabolic.smul_eq_self_iff (hg.pow hn)]
  clear hn
  induction n with
  | zero => simp
  | succ n IH => rw [pow_succ, mul_smul, hg.smul_eq_self_iff.mpr rfl, IH]

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

Goal state before:
pp: g : GL (Fin 2) ℚ
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • (mapGL ℝ).range).IsArithmetic

Tactic:
constructor
  rw [MonoidHom.range_eq_map]
  constructor
  · rw [← Subgroup.relIndex_comap, Subgroup.relIndex_top_right]
    exact (finiteIndex_conjGL g⁻¹).index_ne_zero
  · rw [← Subgroup.relIndex_pointwise_smul (toConjAct (g.map (Rat.castHom ℝ)))⁻¹,
      inv_smul_smul, ← Subgroup.relIndex_comap, Subgroup.relIndex_top_right]
    exact (finiteIndex_conjGL g).index_ne_zero

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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)
x✝ : Fin 2 → ℤ
⊢ normSq (↑(x✝ 0) * ↑z + ↑(x✝ 1)) = normSq (↑↑(x✝ 0) * ↑z + ↑↑(x✝ 1))

Tactic:
rw [ofReal_intCast, ofReal_intCast]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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)]
⊢ ((↑z).im⁻¹ • g) ∘ₗ f = LinearMap.id

Tactic:
apply LinearMap.ext

Goal state after:
z : ℍ
this✝ : Module ℝ (Fin 2 → ℝ) := ⋯
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := ⋯
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := ⋯
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := ⋯
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 → ℝ := ⋯
⊢ ∀ (x : Fin 2 → ℝ), (((↑z).im⁻¹ • g) ∘ₗ f) x = LinearMap.id x
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: case refine_3.inr
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖UpperHalfPlane.cuspFunction 1 (⇑f) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f) w‖

Tactic:
obtain ⟨ξ, hξ, hξ₂⟩ := exists_one_half_le_im_and_norm_le hk f
        ⟨_, im_invQParam_pos_of_norm_lt_one Real.zero_lt_one (mem_ball_zero_iff.mp hq) hq'⟩

Goal state after:
case refine_3.inr
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
ξ : ℍ
hξ : 1 / 2 ≤ ξ.im
hξ₂ : ‖f { coe := invQParam 1 q, coe_im_pos := ⋯ }‖ ≤ ‖f ξ‖
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖UpperHalfPlane.cuspFunction 1 (⇑f) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f) w‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
this : g = -T ^ (-↑g 0 1)
⊢ ∀ (z : ℍ), g • z = T ^ (-↑g 0 1) • z

Tactic:
intro z; conv_lhs => rw [this, SL_neg_smul]

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
this : (f ∘ ↑ofComplex) =O[I∞] (1 ∘ ↑ofComplex)
⊢ (fun τ ↦ f τ - valueAtInfty f) =O[atImInfty] fun τ ↦ rexp (-2 * π * τ.im / h)

Tactic:
convert!
    (hfper.exp_decay_sub_of_bounded_at_inf hh
          (eventually_of_mem (preimage_mem_comap (Ioi_mem_atTop 0)) fun z hz ↦ by
            simpa using (UpperHalfPlane.mdifferentiableAt_iff.mp <| hfhol ⟨z, hz⟩))
          this).comp_tendsto
      tendsto_coe_atImInfty

Goal state after:
case e'_7
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
this : (f ∘ ↑ofComplex) =O[I∞] (1 ∘ ↑ofComplex)
x✝ : ℍ
⊢ f x✝ - valueAtInfty f =
    ((fun z ↦ (f ∘ ↑ofComplex) z - Periodic.cuspFunction h (f ∘ ↑ofComplex) 0) ∘ UpperHalfPlane.coe) x✝
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
⊢ qExpansion h 0 = 0

Tactic:
by
  suffices cuspFunction h 0 = 0 by ext; simp [qExpansion_coeff, this]
  simpa [cuspFunction, Periodic.cuspFunction]
    using! (tendsto_const_nhds.mono_left nhdsWithin_le_nhds).limUnder_eq

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

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ c.IsZeroAt (⇑f) k

Tactic:
rw [isZeroAt_iff_forall_SL2Z hc]

Goal state after:
k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ ∀ (γ : SL(2, ℤ)), (Matrix.SpecialLinearGroup.mapGL ℝ) γ • ∞ = c → IsZeroAtImInfty (⇑f ∣[k] γ)
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
⊢ C * max 1 (1 / τ.im ^ k) = C * ‖τ.im ^ (-k)‖

Tactic:
max_eq_right,

Goal state after:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
⊢ C * (1 / τ.im ^ k) = C * ‖τ.im ^ (-k)‖

k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
τ : ℍ
hτ : τ.im ≤ 1
⊢ 1 ≤ 1 / τ.im ^ k
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
⊢ ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-(↑k / 2))

Tactic:
obtain ⟨C, hC⟩ := exists_bound f

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C / τ.im ^ (↑k / 2)
⊢ ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-(↑k / 2))
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
⊢ (-↑ρ)⁻¹ * 1 = ↑1 + ↑ρ

Tactic:
inv_mul_eq_iff_eq_mul₀ (neg_ne_zero.mpr ρ.ne_zero)

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
⊢ 1 = -↑ρ * (↑1 + ↑ρ)