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

Goal state before:
pp: f : ℕ → ℂ
r : ℝ
s : ℂ
hf : f 0 = 0
hO : (fun n ↦ ∑ k ∈ Icc 1 n, ‖f k‖) =O[atTop] fun n ↦ ↑n ^ r
hr : 0 ≤ r
hs : r < s.re
h₁ : -s ≠ 0
h₂ : (-s).re + r ≤ 0
⊢ LSeriesSummable f s

Tactic:
have h₃ (t : ℝ) (ht : t ∈ Set.Ici 1) : DifferentiableAt ℝ (fun x : ℝ ↦ ‖(x : ℂ) ^ (-s)‖) t :=
    have ht' : t ≠ 0 := (zero_lt_one.trans_le ht).ne'
    (differentiableAt_id.ofReal_cpow_const ht' h₁).norm ℝ <|
      (cpow_ne_zero_iff_of_exponent_ne_zero h₁).mpr <| ofReal_ne_zero.mpr ht'

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

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
⊢ False

Tactic:
have H₁ {x} (hx : x ∈ Set.Ioc 1 2) : (q.totient : ℝ)⁻¹ ≤ (C + C') * (x - 1) :=
    (div_le_iff₀ <| sub_pos.mpr hx.1).mp <|
      sub_le_iff_le_add.mp <| (hC' hx).trans (H₁ hx.1)

Goal state after:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
⊢ False
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
hO : (fun n ↦ ∑ k ∈ Icc 1 n, f k) =O[atTop] fun n ↦ ↑n ^ r
h₁ : (-s - 1).re + r < -1
h₂ : s ≠ 0
h₃ : ∀ t ∈ Set.Ici 1, DifferentiableAt ℝ (fun x ↦ ↑x ^ (-s)) t
n : ℕ
⊢ ∑ k ∈ Icc 0 n, f k = ∑ k ∈ Icc 1 n, f k

Tactic:
by
    rw [← insert_Icc_add_one_left_eq_Icc n.zero_le, sum_insert (by aesop), hf, zero_add, zero_add]

Goal state after:
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 : ℝ
⊢ s ∈ Set.Ioi 1 → ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖ ≤ (s - 1) * s * C + s * ε

Tactic:
hs

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 : s ∈ Set.Ioi 1
⊢ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖ ≤ (s - 1) * s * C + s * ε
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
ha4 : a % 4 = 0
hb2 : b % 2 = 1
⊢ J(a / 4 | b) = J(a | b)

Tactic:
obtain ⟨a, rfl⟩ := Int.dvd_of_emod_eq_zero ha4

Goal state after:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ J(4 * a / 4 | b) = J(4 * a | b)
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 * ∫ (t : ℝ) in Set.Ioi 1, S t * ↑t ^ (-↑s - 1) - l * ↑t ^ (-↑s)‖ =
    ‖(↑s - 1) * ↑s * ∫ (t : ℝ) in Set.Ioi 1, (S t - l * ↑t) * ↑t ^ (-↑s - 1)‖

Tactic:
by
      congr 2
      refine setIntegral_congr_fun measurableSet_Ioi fun t ht ↦ ?_
      replace ht : (t : ℂ) ≠ 0 := ne_zero_of_one_lt_re ht
      rw [sub_mul, cpow_sub _ _ ht, cpow_one, mul_assoc, mul_div_cancel₀ _ ht]

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
hp : p ≠ 0
⊢ 1 ≤ (map (castRingHom ℂ) p).mahlerMeasure

Tactic:
apply le_trans _ (p.map (castRingHom ℂ)).leadingCoeff_le_mahlerMeasure

Goal state after:
p : ℤ[X]
hp : p ≠ 0
⊢ 1 ≤ ‖(map (castRingHom ℂ) p).leadingCoeff‖
Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : T2Space G
H : Subgroup G
inst✝ : H.FiniteIndex
hH : DiscreteTopology ↥H
this : IsOpen[inst✝³] ↑H
⊢ DiscreteTopology G

Tactic:
by
    rw [discreteTopology_iff_isOpen_singleton_one, isOpen_singleton_iff_nhds_eq_pure,
        ← H.coe_one, ← this.isOpenEmbedding_subtypeVal.map_nhds_eq, nhds_discrete, map_pure]

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : TopologicalSpace G
inst✝¹ : OrderTopology G
inst✝ : MulArchimedean G
H : Subgroup G
⊢ IsCyclic ↥H ↔ DiscreteTopology ↥H

Tactic:
by
  nontriviality G using isCyclic_of_subsingleton, Subsingleton.discreteTopology
  rw [Subgroup.isCyclic_iff_exists_zpowers_eq_top]
  constructor
  · rintro ⟨g, rfl⟩
    infer_instance
  · have := H.dense_or_cyclic
    simp only [← Subgroup.zpowers_eq_closure, Eq.comm (a := H)] at this
    refine fun hA ↦ this.elim (fun h ↦ ?_) id
    -- remains to show a contradiction assuming `H` is both dense and discrete
    obtain rfl : H = ⊤ := by
      rw [← coe_eq_univ, ← (dense_iff_closure_eq.mp h), H.isClosed_of_discrete.closure_eq]
    have : DiscreteTopology G := by rwa [← (Homeomorph.Set.univ G).discreteTopology_iff]
    exact isCyclic_iff_exists_zpowers_eq_top.mp inferInstance

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : SMul α ℝ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ ↑(c • 1) • ⇑f ∣[k] γ = ↑(c • 1) • ⇑f

Tactic:
slash_action_eqn _ _ hγ

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : SMul α ℝ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ ↑(c • 1) • ⇑f = ↑(c • 1) • ⇑f
Module: Mathlib.NumberTheory.ModularForms.Identities

Goal state before:
pp: N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
⊢ f (↑N * ↑n +ᵥ z) = f z

Tactic:
apply vAdd_apply_of_mem_strictPeriods

Goal state after:
N : ℕ
k n : ℤ
f : SlashInvariantForm (Subgroup.map (mapGL ℝ) Γ(N)) k
z : ℍ
⊢ ↑N * ↑n ∈ (Subgroup.map (mapGL ℝ) Γ(N)).strictPeriods
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨ 𝒢.strictPeriods.relIndex 𝒢.periods = 2

Tactic:
by
  by_cases h : 𝒢.strictPeriods = 𝒢.periods
  · simp [h]
  · replace h := 𝒢.strictPeriods_le_periods.lt_of_ne h
    obtain ⟨u, hu_mem, hu_notMem⟩ := (SetLike.lt_iff_le_and_exists.mp h).2
    rw [AddSubgroup.relIndex_eq_two_iff_exists_notMem_and]
    refine .inr ⟨u, hu_mem, hu_notMem, fun b hb ↦ ?_⟩
    simp only [Subgroup.periods, mem_strictPeriods_iff, mem_adjoinNegOne_iff,
      AddChar.map_add_eq_mul] at hu_mem hu_notMem hb ⊢
    rcases hb with h | h
    · exact Or.inr h
    · simpa only [neg_mul_neg] using Or.inl (mul_mem h <| hu_mem.resolve_left hu_notMem)

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

Goal state before:
pp: case succ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
ih : ⟨n • k, GradedMonoid.GMonoid.gnpow n f⟩ = ⟨↑n * k, f.pow n⟩
⊢ ⟨n • ⟨k, f⟩.fst, GradedMonoid.GMonoid.gnpow n ⟨k, f⟩.snd⟩ * ⟨k, f⟩ = ⟨↑(n + 1) * k, f.pow (n + 1)⟩

Tactic:
refine (congrArg (fun x : GradedMonoid (ModularForm Γ) ↦ x * ⟨k, f⟩) ih).trans ?_

Goal state after:
case succ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
k : ℤ
f : ModularForm Γ k
n : ℕ
ih : ⟨n • k, GradedMonoid.GMonoid.gnpow n f⟩ = ⟨↑n * k, f.pow n⟩
⊢ ⟨↑n * k, f.pow n⟩ * ⟨k, f⟩ = ⟨↑(n + 1) * k, f.pow (n + 1)⟩
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: ⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 0) = 1

Tactic:
by
  refine rank_eq_one (const 1) (by simp [DFunLike.ne_iff]) fun g ↦ ?_
  obtain ⟨c', hc'⟩ := levelOne_weight_zero_const g
  aesop

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

Goal state before:
pp: case pos
r : ℕ
v : Fin 2 → ℤ
hv✝ : v ∈ gammaSet 1 0 0
hr : True
hv : v 0 = 0 ∧ v 1 = 0
i : Fin 2
⊢ v i = 0 i

Tactic:
fin_cases i <;> simp [hv]

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

Goal state before:
pp: case h
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)
⊢ ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-k)‖

Tactic:
filter_upwards [eventually_le_nhds zero_lt_one] with _ hτ τ rfl

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
⊢ ‖f τ‖ ≤ C * ‖τ.im ^ (-k)‖
Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

Goal state before:
pp: k : ℤ
f g : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hg : (PowerSeries.coeff 0) (qExpansion 1 ⇑g) = 1
⊢ (PowerSeries.coeff 0) (qExpansion 1 ⇑f) -
      (PowerSeries.coeff 0) ((PowerSeries.coeff 0) (qExpansion 1 ⇑f) • qExpansion 1 ⇑g) =
    0

Tactic:
PowerSeries.coeff_smul

Goal state after:
k : ℤ
f g : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hg : (PowerSeries.coeff 0) (qExpansion 1 ⇑g) = 1
⊢ (PowerSeries.coeff 0) (qExpansion 1 ⇑f) -
      (PowerSeries.coeff 0) (qExpansion 1 ⇑f) • (PowerSeries.coeff 0) (qExpansion 1 ⇑g) =
    0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: z : ℍ
⊢ D2 ModularGroup.S z = 2 * ↑π * I / ↑z

Tactic:
simp [D2, ModularGroup.S, ModularGroup.denom_apply]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • ρ ∈ 𝒟
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 = ρ
hSTρ : (S * T) • ρ = ρ
this : ↑g 0 0 = 0 ∨ ↑g 0 0 = 1
⊢ T ^ ↑g 0 0 * S * T = S * T ∨ T ^ ↑g 0 0 * S * T = T * S * T

Tactic:
rcases this with h | h <;> simp [h]

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
rcases this with h | h <;> simp [h]

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

Goal state before:
pp: k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
x : ℂ
⊢ (σ g) x = x

Tactic:
grind [σ, ContinuousAlgEquiv.refl_apply]

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

Goal state before:
pp: ⊢ I ^ 12 = 1

Tactic:
show 12 = 4 * 3 by lia,

Goal state after:
⊢ I ^ (4 * 3) = 1
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: this :
  (Summable fun n ↦ (1 / 2) ^ (n + 1)) →
    (∀ (k : ℕ), Tendsto (fun x ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 0)) →
      (∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)) →
        Tendsto (fun n ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 1)
q : ℂ
⊢ q ∈ Metric.ball 0 (1 / 2) → ∀ (k : ℕ), ‖q‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)

Tactic:
hq

Goal state after:
this :
  (Summable fun n ↦ (1 / 2) ^ (n + 1)) →
    (∀ (k : ℕ), Tendsto (fun x ↦ -x ^ (k + 1)) (𝓝 0) (𝓝 0)) →
      (∀ᶠ (n : ℂ) in 𝓝 0, ∀ (k : ℕ), ‖n‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)) →
        Tendsto (fun n ↦ ∏' (k : ℕ), (1 + -n ^ (k + 1))) (𝓝 0) (𝓝 1)
q : ℂ
hq : q ∈ Metric.ball 0 (1 / 2)
⊢ ∀ (k : ℕ), ‖q‖ ^ (k + 1) ≤ (1 / 2) ^ (k + 1)
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: q : ℂ
⊢ q ∈ Metric.ball 0 1 → cuspFunction 1 Δ q = (fun q ↦ q * ∏' (i : ℕ), (1 - q ^ (i + 1)) ^ 24) q

Tactic:
hq

Goal state after:
q : ℂ
hq : q ∈ Metric.ball 0 1
⊢ cuspFunction 1 Δ q = (fun q ↦ q * ∏' (i : ℕ), (1 - q ^ (i + 1)) ^ 24) q
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case neg
q : ℂ
hq : q ∈ Metric.ball 0 1
hq0 : ¬q = 0
⊢ cuspFunction 1 Δ q = (fun q ↦ q * ∏' (i : ℕ), (1 - q ^ (i + 1)) ^ 24) q

Tactic:
· have him := Periodic.im_invQParam_pos_of_norm_lt_one one_pos
      (by simpa [dist_zero_right] using hq) hq0
    simp [cuspFunction, Periodic.cuspFunction_eq_of_nonzero 1 _ hq0,
      ofComplex_apply_of_im_pos him, discriminant_eq_q_prod ⟨_, him⟩,
      Periodic.qParam_right_inv one_ne_zero hq0, eta_q]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
γ : SL(2, ℤ)
hγ :
  Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ) ∈
    (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ ⇑f ∣[k] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ) /
      ⇑discriminant ∣[12] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ) =
    ⇑f / ⇑discriminant

Tactic:
slash_action_eqn _ _ hγ

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

Goal state before:
pp: case h
k : ℕ
z : ℍ
⊢ ∀ (k_1 : ℕ),
    1 ≤ k_1 →
      k_1 ≤ k → SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) ℍₒ

pp: case hf2
k : ℕ
z : ℍ
⊢ ∀ (n k_1 : ℕ) (r : ℂ),
    k_1 ≤ k → r ∈ ℍₒ → DifferentiableAt ℂ (iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) r

Tactic:
· exact fun n _ _ ↦ summableLocallyUniformlyOn_iteratedDerivWithin_cexp n

Goal state after:
case hf2
k : ℕ
z : ℍ
⊢ ∀ (n k_1 : ℕ) (r : ℂ),
    k_1 ≤ k → r ∈ ℍₒ → DifferentiableAt ℂ (iteratedDerivWithin k_1 (fun z ↦ cexp (2 * ↑π * I * z) ^ n) ℍₒ) r
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: x : ℍ
hxnorm : ‖↑x‖ = 1
hxre : |x.re| ≤ 1 / 2
⊢ x ∈ closure 𝒟ᵒ

Tactic:
rw [← closure_closure]
  -- Consider a vertical line going upwards from `x` (parametrized by `ℝ≥0`)
  apply mem_closure_of_frequently_of_tendsto (b := 𝓝[>] 0)
    (f := fun t : ℝ≥0 ↦ ⟨x + t * Complex.I, by
      simpa using! add_pos_of_pos_of_nonneg x.coe_im_pos t.property⟩)
  · apply Filter.Eventually.frequently
    filter_upwards [self_mem_nhdsWithin] with a (ha : 0 < a)
    refine mem_closure_of_one_lt_norm ?_ (by simpa using! hxre)
    suffices 1 < ‖(x : ℂ)‖ ^ 2 + a ^ 2 + 2 * a * x.im by
      rw [← one_lt_normSq_iff]
      convert! this
      simp [← normSq_eq_norm_sq, normSq_apply]
      ring
    rw [hxnorm, one_pow, add_assoc, lt_add_iff_pos_right]
    positivity
  · refine .mono_left ?_ nhdsWithin_le_nhds
    simpa [show 𝓝 (x : ℂ) = 𝓝 (x + (((0 : ℝ≥0) : ℝ) : ℂ) * Complex.I) by simp,
      isOpenEmbedding_coe.tendsto_nhds_iff] using! Continuous.tendsto (by fun_prop) _

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

Goal state before:
pp: ⊢ ∃ c a, ∀ (b : ℝ), a ≤ b → ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖

Tactic:
refine ⟨2 / (1 - rexp (-(π * 1))), 1, fun y hy τ hτ =>
    (norm_jacobiTheta_sub_one_le (hτ.symm ▸ zero_lt_one.trans_le hy : 0 < im τ)).trans ?_⟩

Goal state after:
y : ℝ
hy : 1 ≤ y
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) ≤ 2 / (1 - rexp (-(π * 1))) * ‖rexp (-π * τ.im)‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
τ : ℍ
h : τ.im ≤ 1 / 2
⊢ ∃ γ, 1 / 2 ≤ (γ • τ).im ∧ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1

Tactic:
refine (exists_one_half_le_im_smul τ).imp (fun γ hγ ↦ ⟨hγ, ?_⟩)

Goal state after:
case inr
τ : ℍ
h : τ.im ≤ 1 / 2
γ : SL(2, ℤ)
hγ : 1 / 2 ≤ (γ • τ).im
⊢ ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑τ‖ ≤ 1
Module: Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous

Goal state before:
pp: ⊢ ProperlyDiscontinuousSMul ↥(SpecialLinearGroup.mapGL ℝ).range ℍ

Tactic:
by
  let 𝒮ℒ' : Subgroup SL(2, ℝ) := (SpecialLinearGroup.map (Int.castRingHom ℝ)).range
  have : ProperlyDiscontinuousSMul 𝒮ℒ' ℍ := inferInstance
  simp only [Subgroup.properlyDiscontinuousSMul_iff] at this ⊢
  refine fun K L hK hL ↦ ((this hK hL).map SpecialLinearGroup.toGL).subset fun g ↦ ?_
  rintro ⟨⟨γ, rfl⟩, hγ⟩
  exact ⟨γ, ⟨by simp [𝒮ℒ'], hγ⟩, rfl⟩

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ x✝ ∈ (polarSpaceCoord K).target ↔
    x✝ ∈ (Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x ↦ Set.Ioo (-π) π

Tactic:
polarSpaceCoord_target,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : polarSpace K
⊢ (x✝ ∈ ⇑(homeoRealMixedSpacePolarSpace K).symm ⁻¹' Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target) ↔
    x✝ ∈ (Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0) ×ˢ Set.univ.pi fun x ↦ Set.Ioo (-π) π
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in ⇑(homeoRealMixedSpacePolarSpace K) ⁻¹' (polarSpaceCoord K).target,
      (∏ w, ((homeoRealMixedSpacePolarSpace K) x).1 ↑w) •
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) x)) ∂volume =
    ∫ (x : realMixedSpace K) in (mixedEmbedding.polarCoord K).target,
      (∏ w, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x)

Tactic:
polarSpaceCoord_target,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in
      ⇑(homeoRealMixedSpacePolarSpace K) ⁻¹'
        ⇑(homeoRealMixedSpacePolarSpace K).symm ⁻¹' Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ((homeoRealMixedSpacePolarSpace K) x).1 ↑w) •
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) x)) ∂volume =
    ∫ (x : realMixedSpace K) in (mixedEmbedding.polarCoord K).target,
      (∏ w, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (a : realMixedSpace K) in ⇑(homeoRealMixedSpacePolarSpace K) ⁻¹' (polarSpaceCoord K).target,
      (∏ w, ENNReal.ofReal (((homeoRealMixedSpacePolarSpace K) a).1 ↑w)) *
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) a)) ∂volume =
    ∫⁻ (x : realMixedSpace K) in (mixedEmbedding.polarCoord K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(mixedEmbedding.polarCoord K).symm x)

Tactic:
polarSpaceCoord_target,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (a : realMixedSpace K) in
      ⇑(homeoRealMixedSpacePolarSpace K) ⁻¹'
        ⇑(homeoRealMixedSpacePolarSpace K).symm ⁻¹' Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (((homeoRealMixedSpacePolarSpace K) a).1 ↑w)) *
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) a)) ∂volume =
    ∫⁻ (x : realMixedSpace K) in (mixedEmbedding.polarCoord K).target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(mixedEmbedding.polarCoord K).symm x)
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
x✝ : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = ↑x
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K) y = ↑x
⊢ ↑x ∈ K⁺

Tactic:
← hy,

Goal state after:
case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
x✝ : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = ↑x
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K) y = ↑x
⊢ (algebraMap (𝓞 ↥K⁺) K) y ∈ K⁺
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
n : ℕ
x✝ : ↑(integerSet K)
⊢ ((Algebra.norm ℤ) ↑(preimageOfMemIntegerSet x✝)).natAbs = n ↔ absNorm ↑↑((integerSetEquiv K) x✝).1 = n

Tactic:
integerSetEquiv_apply_fst,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
n : ℕ
x✝ : ↑(integerSet K)
⊢ ((Algebra.norm ℤ) ↑(preimageOfMemIntegerSet x✝)).natAbs = n ↔ absNorm (Ideal.span {↑(preimageOfMemIntegerSet x✝)}) = n
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ Nat.card ↑{I | IsPrincipal ↑I ∧ absNorm ↑I = n} * torsionOrder K = Nat.card ↑{a | mixedEmbedding.norm ↑a = ↑n}

Tactic:
rw [torsionOrder, ← Nat.card_prod]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ Nat.card (↑{I | IsPrincipal ↑I ∧ absNorm ↑I = n} × ↥(Units.torsion K)) = Nat.card ↑{a | mixedEmbedding.norm ↑a = ↑n}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ absNorm ↑I ≤ ⌊s⌋₊ } * torsionOrder K =
    Nat.card { a // intNorm ↑((idealSetEquiv K J) a) ≤ ⌊s⌋₊ }

Tactic:
rw [torsionOrder, ← Nat.card_prod]

Goal state after:
case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card ({ I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ absNorm ↑I ≤ ⌊s⌋₊ } × ↥(Units.torsion K)) =
    Nat.card { a // intNorm ↑((idealSetEquiv K J) a) ≤ ⌊s⌋₊ }