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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ -legendreSym 3 (↑(mersenne p) % ↑3) = -1

Tactic:
rw_mod_cast [mersenne_mod_three odd hp]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
odd : Odd p
⊢ -legendreSym 3 ↑1 = Int.negSucc 0
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ (Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋).card = ∏ x, (⌊B₂ x⌋ - ⌈B₁ x⌉ + 1).toNat

Tactic:
grind [Pi.card_Icc, card_Icc]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h₁
p' : ℕ
h✝ : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : (Units.coeHom (X ↑(q (p' + 2)))) (ωUnit (p' + 2) ^ 2 ^ (p' + 1)) = (Units.coeHom (X ↑(q (p' + 2)))) 1
h : 1 = -1
⊢ False

Tactic:
have : Fact (2 < (q (p' + 2) : ℕ)) := ⟨two_lt_q _⟩

Goal state after:
case h₁
p' : ℕ
h✝ : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
ω_pow : (Units.coeHom (X ↑(q (p' + 2)))) (ωUnit (p' + 2) ^ 2 ^ (p' + 1)) = (Units.coeHom (X ↑(q (p' + 2)))) 1
h : 1 = -1
this : Fact (2 < ↑(q (p' + 2)))
⊢ False
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: β : Type u_1
G : Type u_2
α : Type u_3
inst✝² : Monoid G
inst✝¹ : AddGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : α
⊢ (-a) ∣[k] g + a ∣[k] g = 0

Tactic:
rw [← add_slash, neg_add_cancel, zero_slash]

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

Goal state before:
pp: case mpr
c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ (∃ γ, (mapGL ℝ) γ • ∞ = c ∧ IsZeroAtImInfty (f ∣[k] γ)) → c.IsZeroAt f k

Tactic:
rintro ⟨γ, rfl, b⟩
    simpa [IsZeroAt.smul_iff, isZeroAt_infty_iff] using! b

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

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
hc : IsCusp c (mapGL ℝ).range
⊢ c.IsBoundedAt f k ↔ ∀ (γ : SL(2, ℤ)), (mapGL ℝ) γ • ∞ = c → IsBoundedAtImInfty (f ∣[k] γ)

Tactic:
refine ⟨fun hc _ hγ ↦ by simpa using! hc _ hγ, fun h ↦ ?_⟩
  obtain ⟨γ, rfl⟩ := isCusp_SL2Z_iff'.mp hc
  simpa [IsBoundedAt.smul_iff, isBoundedAt_infty_iff] using! h γ rfl

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ Function.Surjective (cosetToCuspOrbit 𝒢)

Tactic:
rintro ⟨c, (hc : IsCusp c _)⟩

Goal state after:
case mk
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
b✝ : CuspOrbits 𝒢
c : OnePoint ℝ
hc : IsCusp c 𝒢
⊢ ∃ a, cosetToCuspOrbit 𝒢 a = Quot.mk ⇑(MulAction.orbitRel ↥𝒢 ↥(cuspsSubMulAction 𝒢)) ⟨c, hc⟩
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : ModularForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ IsBoundedAtImInfty ((c • f.toSlashInvariantForm).toFun ∣[k] g)

Tactic:
simp_rw [IsBoundedAtImInfty, Filter.BoundedAtFilter, SlashInvariantForm.toFun_eq_coe,
        FunLike.coe_smul, toSlashInvariantForm_coe, ← smul_one_smul ℂ c ⇑f, smul_slash]

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
α : Type u_1
inst✝² : SMul α ℂ
inst✝¹ : IsScalarTower α ℂ ℂ
inst✝ : Γ.HasDetOne
c : α
f : ModularForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
g : GL (Fin 2) ℝ
hg : g • OnePoint.infty = c✝
⊢ ((σ g) (c • 1) • ⇑f ∣[k] g) =O[atImInfty] 1
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : CuspFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ IsZeroAtImInfty ((ModularForm.translate f g).toFun ∣[k] γ)

Tactic:
by
    rw [SlashInvariantForm.toFun_eq_coe, ModularForm.toSlashInvariantForm_coe,
      ModularForm.coe_translate, ← SlashAction.slash_mul, ← isZeroAt_infty_iff,
      ← OnePoint.IsZeroAt.smul_iff]
    apply CuspFormClass.zero_at_cusps f
    simpa [mul_smul, hγ] using hc.smul g

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

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
| fun τ ↦ Real.exp (-a * τ.im)

Tactic:
enter [

Goal state after:
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
| fun τ ↦ Real.exp (-a * τ.im)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
g' : SL(2, ℤ)
⊢ z.im / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g')) ↑z) ≤
    z.im / normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z)

Tactic:
div_le_div_iff_of_pos_left

Goal state after:
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
g' : SL(2, ℤ)
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) ≤
    normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g')) ↑z)

case ha
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
g' : SL(2, ℤ)
⊢ 0 < z.im

case hb
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
g' : SL(2, ℤ)
⊢ 0 < normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g')) ↑z)

case hc
z : ℍ
s : Set (Fin 2 → ℤ) := {cd | IsCoprime (cd 0) (cd 1)}
hs : s.Nonempty
p : Fin 2 → ℤ
hp_coprime : p ∈ s
hp : ∀ a ∈ s, normSq (↑(p 0) * ↑z + ↑(p 1)) ≤ normSq (↑(a 0) * ↑z + ↑(a 1))
g : SL(2, ℤ)
hg : (fun g ↦ ↑g 1) g = p
g' : SL(2, ℤ)
⊢ 0 < normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z)
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
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
| (2 * ↑π * Complex.I)⁻¹ *
      ∫ (θ : ℝ) in 0..h * (2 * π / h),
        deriv (circleMap 0 R) θ • (cuspFunction h f (circleMap 0 R θ) / circleMap 0 R θ ^ (n + 1)) =
    1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }

Tactic:
enter [

Goal state after:
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
t : ℝ
ht : 0 < t
R : ℝ := rexp (-2 * π * t / h)
hR0 : 0 < R
hR1 : R < 1
| (2 * ↑π * Complex.I)⁻¹ *
      ∫ (θ : ℝ) in 0..h * (2 * π / h),
        deriv (circleMap 0 R) θ • (cuspFunction h f (circleMap 0 R θ) / circleMap 0 R θ ^ (n + 1)) =
    1 / ↑h * ∫ (u : ℝ) in 0..h, 1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
| ∃ C, ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C * max τ.im (1 / τ.im) ^ k

Tactic:
enter [

Goal state after:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
| ∃ C, ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C * max τ.im (1 / τ.im) ^ k
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
| ∃ C, ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C

Tactic:
enter [

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
| ∃ C, ∀ (τ : ℍ), ‖petersson k (⇑f) (⇑f') τ‖ ≤ C
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: k : ℤ
F : Type u_1
inst✝⁴ : FunLike F ℍ ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
f : F
inst✝³ : ModularFormClass F Γ k
inst✝² : Γ.HasDetPlusMinusOne
inst✝¹ : DiscreteTopology ↥Γ
inst✝ : Fact (IsCusp OnePoint.infty Γ)
⊢ ∃ c > 0, (fun τ ↦ f τ - valueAtInfty ⇑f) =O[atImInfty] fun τ ↦ rexp (-c * τ.im)

Tactic:
have hh : 0 < Γ.strictWidthInfty := Γ.strictWidthInfty_pos_iff.mpr Fact.out
  have hΓ : Γ.strictWidthInfty ∈ Γ.strictPeriods := Γ.strictWidthInfty_mem_strictPeriods
  refine ⟨2 * π / Γ.strictWidthInfty, div_pos Real.two_pi_pos hh, ?_⟩
  convert! exp_decay_sub_atImInfty hh (periodic_comp_ofComplex f hΓ) (holo f) (bdd_at_infty f) using
    3 with τ
  ring_nf

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

Goal state before:
pp: h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (Periodic.cuspFunction h f) 0
hgcts : ContinuousAt (Periodic.cuspFunction h g) 0
⊢ update ((f * g) ∘ Periodic.invQParam h) 0 ((𝓝[≠] 0).limUnder ((f * g) ∘ Periodic.invQParam h)) 0 =
    Periodic.cuspFunction h f 0 * Periodic.cuspFunction h g 0

Tactic:
update_self

Goal state after:
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (Periodic.cuspFunction h f) 0
hgcts : ContinuousAt (Periodic.cuspFunction h g) 0
⊢ (𝓝[≠] 0).limUnder ((f * g) ∘ Periodic.invQParam h) = Periodic.cuspFunction h f 0 * Periodic.cuspFunction h g 0
Module: Mathlib.Order.Filter.AtTopBot.Interval

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NoBotOrder α
⊢ Tendsto (fun p ↦ Ioc p.1 p.2) (atBot ×ˢ atTop) atTop

Tactic:
by
  simpa [tendsto_atTop, ← coe_subset, Set.subset_def, -eventually_and]
    using fun b i _ ↦ (eventually_lt_atBot i).prod_mk (eventually_ge_atTop i)

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

Goal state before:
pp: ⊢ (symmetricIcc ℤ).filter = Filter.map (fun N ↦ Icc (-↑N) ↑N) atTop

Tactic:
by
  simp [← Nat.map_cast_int_atTop, Function.comp_def]

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

Goal state before:
pp: z : ℍ
HG : logDeriv (fun x ↦ ∏' (i : ℕ), (1 - eta_q i x)) ↑z = ∑' (i : ℕ), logDeriv (fun x ↦ 1 - eta_q i x) ↑z
⊢ 2 * ↑π * I / ↑24 + 2 * ↑π * I * ∑' (n : ℕ), (↑n + 1) * -eta_q n ↑z / (1 - eta_q n ↑z) =
    ↑π * I / 12 *
      ((↑π ^ 2 / 6)⁻¹ * 2⁻¹ * (2 * (↑π ^ 2 / 6)) +
        -((↑π ^ 2 / 6)⁻¹ * 2⁻¹ *
            (8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n ^ 1 * cexp (2 * ↑π * I * ↑z) ^ ↑n / (1 - cexp (2 * ↑π * I * ↑z) ^ ↑n))))

Tactic:
mul_add

Goal state after:
z : ℍ
HG : logDeriv (fun x ↦ ∏' (i : ℕ), (1 - eta_q i x)) ↑z = ∑' (i : ℕ), logDeriv (fun x ↦ 1 - eta_q i x) ↑z
⊢ 2 * ↑π * I / ↑24 + 2 * ↑π * I * ∑' (n : ℕ), (↑n + 1) * -eta_q n ↑z / (1 - eta_q n ↑z) =
    ↑π * I / 12 * ((↑π ^ 2 / 6)⁻¹ * 2⁻¹ * (2 * (↑π ^ 2 / 6))) +
      ↑π * I / 12 *
        -((↑π ^ 2 / 6)⁻¹ * 2⁻¹ *
            (8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n ^ 1 * cexp (2 * ↑π * I * ↑z) ^ ↑n / (1 - cexp (2 * ↑π * I * ↑z) ^ ↑n)))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.MDifferentiable

Goal state before:
pp: ⊢ MDiff E2

Tactic:
by
  rw [UpperHalfPlane.mdifferentiable_iff]
  have hη : DifferentiableOn ℂ η _ := fun z hz ↦
    (differentiableAt_eta_of_mem_upperHalfPlaneSet hz).differentiableWithinAt
  have hlog : DifferentiableOn ℂ (logDeriv η) _ :=
    (hη.deriv isOpen_upperHalfPlaneSet).div hη (fun _ hz ↦ eta_ne_zero hz)
  refine (hlog.const_mul (π * I / 12)⁻¹).congr (fun z hz ↦ ?_)
  simp [ofComplex_apply_of_im_pos hz, logDeriv_eta_eq_E2 ⟨z, hz⟩]
  field_simp

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

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * (deriv (F ∘ ↑ofComplex) ↑z + deriv (G ∘ ↑ofComplex) ↑z) =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z + (2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z

Tactic:
mul_add

Goal state after:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
hGz : DifferentiableAt ℂ (G ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z + (2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z =
    (2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z + (2 * ↑π * I)⁻¹ * deriv (G ∘ ↑ofComplex) ↑z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: htprod : Tendsto (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
⊢ Tendsto (fun x ↦ ∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) atImInfty (𝓝 1)

Tactic:
have := (htprod.comp (UpperHalfPlane.qParam_tendsto_atImInfty zero_lt_one)).pow 24

Goal state after:
htprod : Tendsto (fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) (𝓝 0) (𝓝 1)
this : Tendsto (fun x ↦ ((fun q ↦ ∏' (n : ℕ), (1 - q ^ (n + 1))) ∘ fun τ ↦ 𝕢 1 ↑τ) x ^ 24) atImInfty (𝓝 (1 ^ 24))
⊢ Tendsto (fun x ↦ ∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) atImInfty (𝓝 1)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ Tendsto (fun N ↦ ∑ m ∈ range N, -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)) atTop
    (𝓝 (-8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n))

Tactic:
have : -8 * π ^ 2 * ∑' n : ℕ+, σ 1 n * 𝕢 z ^ (n : ℕ) =
      ∑' m : ℕ, (-8 * π ^ 2 * ∑' n : ℕ+, n * 𝕢 z ^ ((m + 1) * n)) := by
    have := tsum_prod_pow_eq_tsum_sigma 1 (norm_exp_two_pi_I_lt_one z)
    rw [tsum_pnat_eq_tsum_succ (f := fun d ↦ ∑' c : ℕ+, c ^ 1 * 𝕢 z ^ (d * c : ℕ))] at this
    simp [← tsum_mul_left, ← this]
  rw [this]
  refine (Summable.mul_left _ ?_).hasSum.comp tendsto_finset_range
  rw [← summable_pnat_iff_summable_succ (f := fun b ↦ ∑' c : ℕ+, c * 𝕢 z ^ (b * c : ℕ))]
  apply (summable_prod_mul_pow 1 (norm_exp_two_pi_I_lt_one z)).prod.congr
  simp [← exp_nsmul]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} → g • ρ = ρ

Tactic:
suffices (S * T) • ρ = ρ ∧ (T⁻¹ * S) • ρ = ρ by simp +contextual [-sl_moeb, or_imp, this]
    rw [mul_smul T⁻¹, inv_smul_eq_iff, ← eq_inv_smul_iff (g := S), S_inv, SL_neg_smul,
      mul_smul, eq_comm, and_self, modular_T_smul, modular_S_smul, UpperHalfPlane.ext_iff]
    norm_num [ρ, Complex.ext_iff, normSq, ← pow_two, div_pow]

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
by
  -- We show that `x` is a limit of points known to be in the closure.
  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.Multiplicity

Goal state before:
pp: k : ℤ
hk : Odd k
⊢ 8 ∣ k ^ 2 - 1

Tactic:
by
  rcases hk with ⟨m, rfl⟩
  have eq : (2 * m + 1) ^ 2 - 1 = 4 * (m * (m + 1)) := by ring
  simpa [eq] using (mul_dvd_mul_iff_left four_ne_zero).mpr (two_dvd_mul_add_one m)

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S), Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map id (inclusion R A hS))
y : Y
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i | x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hxS : ∀ i ∈ S, x i ∈ A i
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ Tendsto (f ∘ fun p ↦ (id p.1, inclusion R A hS p.2)) (𝓝 (y, x')) (𝓝 (f (y, inclusion R A hS x')))

Tactic:
exact H S hS |>.tendsto ⟨y, x'⟩

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : realSpace K
⊢ ↑expMap (c • x) = ↑expMap x ^ c

Tactic:
ext
  simp [mul_comm c _, ← mul_assoc, Real.exp_mul]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ι : Type u_2
s : Finset ι
f : ι → realSpace K
x✝ : InfinitePlace K
⊢ ↑expMap (∑ i ∈ s, f i) x✝ = (∏ i ∈ s, ↑expMap (f i)) x✝

Tactic:
simp [← Real.exp_sum, ← mul_sum]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
⊢ span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} =
    Ideal.map (↑(mapEquiv (Int.quotientSpanNatEquivZMod p)))
      (span {Polynomial.map (Ideal.Quotient.mk (span {↑p})) (minpoly ℤ θ)})

Tactic:
simp [Ideal.map_span, Polynomial.map_map]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
| Real.exp (x w₀) • fun w ↦
    ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ if ↑i = w₀ then 0 else x ↑i

Tactic:
enter [

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
| Real.exp (x w₀) • fun w ↦
    ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ if ↑i = w₀ then 0 else x ↑i
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ Real.exp (x w₀) ^ finrank ℚ K *
      ∏ x_1, (∏ i, x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K

Tactic:
← prod_pow

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ Real.exp (x w₀) ^ finrank ℚ K *
      ∏ x_1, ∏ x_2, (x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm x_2))) ^ x ↑x_2) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
| ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun w ↦
        (∑ i, (if ↑i = w₀ then 0 else x ↑i) • (completeBasis K) ↑i) ↑w)
      (equivFinRank.symm ⟨w, hw⟩) ∈
    Set.Ico 0 1

Tactic:
enter [

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
| ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun w ↦
        (∑ i, (if ↑i = w₀ then 0 else x ↑i) • (completeBasis K) ↑i) ↑w)
      (equivFinRank.symm ⟨w, hw⟩) ∈
    Set.Ico 0 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasurableSet (paramSet K)

Tactic:
refine MeasurableSet.univ_pi fun _ ↦ ?_

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
⊢ MeasurableSet (if x✝ = w₀ then Set.Iic 0 else Set.Ico 0 1)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
⊢ (galEquivZMod m F) (σ.restrictNormal F) = (ZMod.unitsMap h) ((galEquivZMod n K) σ)

Tactic:
have hζ := IsCyclotomicExtension.zeta_spec m ℚ F

Goal state after:
n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
⊢ (galEquivZMod m F) (σ.restrictNormal F) = (ZMod.unitsMap h) ((galEquivZMod n K) σ)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this✝ : IsGalois ℚ K
this : IsGalois (FractionRing ℤ) (FractionRing (𝓞 K))
| ∏ i, span {i (hζ.toInteger - 1)}

Tactic:
enter [

Goal state after:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this✝ : IsGalois ℚ K
this : IsGalois (FractionRing ℤ) (FractionRing (𝓞 K))
| ∏ i, span {i (hζ.toInteger - 1)}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K,
        ∏ w, ENNReal.ofReal (x ↑w) =
    2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)

Tactic:
normAtAllPlaces_image_preimage_expMapBasis,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in ↑expMapBasis '' paramSet K, ∏ w, ENNReal.ofReal (x ↑w) =
    2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)