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

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
hg : ↑g 1 = p
nonZ1 : ↑(p 0) ^ 2 + ↑(p 1) ^ 2 ≠ 0
this : Int.cast ∘ p ≠ 0
nonZ2 : ↑(p 0) * ↑z + ↑(p 1) ≠ 0
⊢ ↑(g • z) =
    ↑((lcRow0 p) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(p 0) ^ 2 + ↑(p 1) ^ 2) +
      (↑(p 1) * ↑z - ↑(p 0)) / ((↑(p 0) ^ 2 + ↑(p 1) ^ 2) * (↑(p 0) * ↑z + ↑(p 1)))

Tactic:
subst hg

Goal state after:
g : SL(2, ℤ)
z : ℍ
hp : IsCoprime (↑g 1 0) (↑g 1 1)
nonZ1 : ↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2 ≠ 0
this : Int.cast ∘ ↑g 1 ≠ 0
nonZ2 : ↑(↑g 1 0) * ↑z + ↑(↑g 1 1) ≠ 0
⊢ ↑(g • z) =
    ↑((lcRow0 (↑g 1)) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) / (↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) +
      (↑(↑g 1 1) * ↑z - ↑(↑g 1 0)) / ((↑(↑g 1 0) ^ 2 + ↑(↑g 1 1) ^ 2) * (↑(↑g 1 0) * ↑z + ↑(↑g 1 1)))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
v : Fin 2 → ℤ
hv : v ∈ gammaSet N r a
γ : SL(2, ℤ)
⊢ v ᵥ* ↑γ ∈ gammaSet N r (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ))

Tactic:
by
  refine ⟨?_, vecMulSL_gcd hv.2 γ⟩
  have := RingHom.map_vecMul (m := Fin 2) (n := Fin 2) (Int.castRingHom (ZMod N)) γ v
  simp only [eq_intCast, Int.coe_castRingHom] at this
  simp_rw [Function.comp_def, this, hv.1]
  simp

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

Goal state before:
pp: k : ℤ
N : ℕ
inst✝ : NeZero N
hk : 3 ≤ k
a : Fin 2 → ZMod N
c : OnePoint ℝ
hc : IsCusp c (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ(N))
⊢ c.IsBoundedAt (⇑(eisensteinSeriesSIF a k)) k

Tactic:
rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z] at hc
    rw [OnePoint.isBoundedAt_iff_forall_SL2Z hc]
    exact fun γ hγ ↦ isBoundedAtImInfty_eisensteinSeriesSIF a hk γ

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
⊢ ∑ i ∈ (↑b).divisorsAntidiagonal.attach, ‖↑(↑i).2‖ ^ k * ‖r‖ ^ ((↑i).1 * (↑i).2) ≤ ‖↑↑b ^ (k + 1) * r ^ ↑b‖

Tactic:
transitivity ∑ _ ∈ (b : ℕ).divisors, ‖(b : 𝕜)‖ ^ k * ‖r ^ (b : ℕ)‖

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
⊢ ∑ i ∈ (↑b).divisorsAntidiagonal.attach, ‖↑(↑i).2‖ ^ k * ‖r‖ ^ ((↑i).1 * (↑i).2) ≤
    ∑ x ∈ (↑b).divisors, ‖↑↑b‖ ^ k * ‖r ^ ↑b‖

𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
⊢ ∑ x ∈ (↑b).divisors, ‖↑↑b‖ ^ k * ‖r ^ ↑b‖ ≤ ‖↑↑b ^ (k + 1) * r ^ ↑b‖
Module: Mathlib.NumberTheory.Modular

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

Tactic:
inv_re,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
⊢ (-↑z).re / normSq (-↑z) = -z.re
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ ∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z =
    t + ∑' (m : ℤ), ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))

Tactic:
← Summable.tsum_add

Goal state after:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ ∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z =
    ∑' (b : ℤ),
      (∑' (n : ℤ), G2Term z ![b, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1)))

case hf
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun m ↦ ∑' (n : ℤ), G2Term z ![m, n]

case hg
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun m ↦ ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑m * ↑z + ↑n) - 1 / (↑m * ↑z + ↑n + 1))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case h₂
z : ℍ
H : Summable (G2Term z ∘ ⇑((finTwoArrowEquiv ℤ).trans (Equiv.prodComm ℤ ℤ)).symm)
⊢ ∀ (c : ℤ), Summable fun b ↦ G2Term z ![b, c]

Tactic:
exact H.prod_factor

Goal state after:
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
⊢ (g = S * T⁻¹ ∨ g = T⁻¹ * S * T⁻¹) ∧ z = 1 +ᵥ ρ

Tactic:
by
  have : g 0 1 = -g 0 0 - 1 := by
    have := g.property
    simp_rw [det_fin_two] at this
    grind
  have hgeq : g = T ^ g 0 0 * S * T⁻¹ := by
    refine Subtype.ext ?_
    rw [coe_mul, coe_mul, coe_T_zpow, coe_S, ← zpow_neg_one, coe_T_zpow, mul_fin_two, mul_fin_two]
    ring_nf
    ext i j
    fin_cases i <;> fin_cases j <;> [tauto; skip; tauto; tauto]
    simp [this]
    ring_nf
  have hnorm : ‖(z : ℂ) - 1‖ ≤ 1 := by
    convert! hg' using 2
    simp [denom, hc, hd, sub_eq_add_neg]
  rw [norm_def, Real.sqrt_le_one] at hnorm
  have : normSq (z - 1) = normSq z + (-2 * z.re + 1) := by
    simp [normSq]
    ring
  rw [this] at hnorm
  obtain ⟨h, h'⟩ : normSq z = 1 ∧ z.re = 1 / 2 := by
    have : 1 ≤ normSq z := hz.1
    have : 0 ≤ -2 * z.re + 1 := by linarith [(le_abs_self _).trans hz.2]
    constructor <;> linarith
  have hρ : z = (1 : ℝ) +ᵥ ρ := by
    apply eq_of_re_of_norm
    · norm_num [h', ρ]
    · rw [norm_def, h, coe_vadd, ofReal_one,
        show 1 + (ρ : ℂ) = -ρ ^ 2 by grind [ρ_sq], norm_neg, norm_pow, norm_ρ, Real.sqrt_one,
        one_pow]
  refine ⟨?_, hρ⟩
  rw [hgeq, hρ, mul_assoc, mul_smul] at hg
  have : S • ρ = T • ρ := by
    rw [UpperHalfPlane.ext_iff, modular_S_smul, modular_T_smul, UpperHalfPlane.coe_mk,
      coe_vadd, ← mul_one (_ : ℂ)⁻¹, inv_mul_eq_iff_eq_mul₀ (neg_ne_zero.mpr ρ.ne_zero)]
    grind [ρ_sq, ofReal_one]
  have : (S * T⁻¹) • ((1 : ℝ) +ᵥ ρ) = (1 : ℝ) +ᵥ ρ := by
    rw [mul_smul, ← SL_neg_smul S, ← S_inv, inv_smul_eq_iff, ← zpow_neg_one,
    modular_T_zpow_smul, Int.cast_neg, Int.cast_one, neg_vadd_vadd,
    ← inv_smul_eq_iff, S_inv, SL_neg_smul, this, modular_T_smul]
  rw [this] at hg
  rw [hgeq]
  suffices g 0 0 = 0 ∨ g 0 0 = -1 by rcases this with h | h <;> simp [h]
  have : (-1 : ℝ) ≤ g 0 0 ∧ g 0 0 ≤ 0 := by
    simpa only [ρ, neg_div, one_div, ← coe_re, coe_T_zpow_smul_eq, coe_vadd, add_re, ofReal_re,
      show 1 + (-2⁻¹ : ℝ) = 2⁻¹ by norm_num, intCast_re, abs_le, ← sub_le_iff_le_add',
      show (-2⁻¹ : ℝ) - (2⁻¹ : ℝ) = -1 by norm_num, add_le_iff_nonpos_right, Int.cast_nonpos] using
      hg.2
  rw [← Int.cast_one, ← Int.cast_neg, Int.cast_le] at this
  grind

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
this : ∀ {g : SL(2, ℤ)} {z : ℍ}, z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → (g • z).im = z.im
hden : ¬z.im ≤ (g • z).im
⊢ (g • z).im = z.im

pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
⊢ (g • z).im = z.im

Tactic:
· rw [← this (g := g⁻¹) hg (by simpa using hz) (by simpa using le_of_not_ge hden)]
    simp

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : z.im ≤ (g • z).im
⊢ (g • z).im = z.im
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ Set.EqOn (η ∘ fun x ↦ -1 / x) (I.sqrt⁻¹ • (sqrt * η)) upperHalfPlaneSet

Tactic:
obtain ⟨z, hz, h⟩ := eta_comp_eqOn_const_mul_csqrt_eta
  have h3 : η I = z * sqrt I * η I := by simpa [← mul_assoc] using h (show I ∈ _ by simp)
  grind [sqrt, eta_ne_zero (show 0 < I.im by simp)]

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ∑' (n : ℤ), 1 / (↑z + ↑n) ^ (k + 1) = (-2 * ↑π * I) ^ (k + 1) / ↑k ! * ∑' (n : ℕ), ↑n ^ k * cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
have : (-1) ^ k * k ! * ∑' n : ℤ, 1 / ((z : ℂ) + n) ^ (k + 1) =
    -(2 * π * I) ^ (k + 1) * ∑' n : ℕ, n ^ k * cexp (2 * π * I * z) ^ n := by
    rw [← iteratedDerivWithin_tsum_exp_aux_eq hk z,
      ← iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow hk (by simpa using z.2)]
    exact iteratedDerivWithin_congr (fun x hx ↦ by (simpa using pi_mul_cot_pi_q_exp ⟨x, hx⟩))
      (by simpa using z.2)
  simp_rw [(eq_inv_mul_iff_mul_eq₀ (by simp [Nat.factorial_ne_zero])).mpr this, ← tsum_mul_left]
  congr
  ext n
  rw [show (-2 * π * I) ^ (k + 1) = (-1) ^ (k + 1) * (2 * π * I) ^ (k + 1) by rw [← neg_pow]; ring]
  field_simp
  ring_nf
  simp [Nat.mul_two]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
d : ℕ+
⊢ ∑' (n : ℕ+), ((-↑↑d + ↑↑n * ↑z)⁻¹ - (↑↑d + ↑↑n * ↑z)⁻¹) + ∑' (n : ℕ+), ((-↑↑d - ↑z * ↑↑n)⁻¹ - (↑↑d - ↑z * ↑↑n)⁻¹) =
    ∑' (m : ℕ+), ((-↑↑d + ↑z * ↑↑m)⁻¹ + (-↑↑d - ↑z * ↑↑m)⁻¹ - (↑↑d + ↑z * ↑↑m)⁻¹ - (↑↑d - ↑z * ↑↑m)⁻¹)

Tactic:
← Summable.tsum_add

Goal state after:
z : ℍ
d : ℕ+
⊢ ∑' (b : ℕ+), ((-↑↑d + ↑↑b * ↑z)⁻¹ - (↑↑d + ↑↑b * ↑z)⁻¹ + ((-↑↑d - ↑z * ↑↑b)⁻¹ - (↑↑d - ↑z * ↑↑b)⁻¹)) =
    ∑' (m : ℕ+), ((-↑↑d + ↑z * ↑↑m)⁻¹ + (-↑↑d - ↑z * ↑↑m)⁻¹ - (↑↑d + ↑z * ↑↑m)⁻¹ - (↑↑d - ↑z * ↑↑m)⁻¹)

case hf
z : ℍ
d : ℕ+
⊢ Summable fun n ↦ (-↑↑d + ↑↑n * ↑z)⁻¹ - (↑↑d + ↑↑n * ↑z)⁻¹

case hg
z : ℍ
d : ℕ+
⊢ Summable fun n ↦ (-↑↑d - ↑z * ↑↑n)⁻¹ - (↑↑d - ↑z * ↑↑n)⁻¹
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this : HasSum (fun n ↦ cexp (↑π * I * ↑(n + 1) ^ 2 * τ) * 2) (jacobiTheta τ + (1 - 1 * 2))
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
(by norm_num : (1 : ℂ) - 1 * 2 = -1),

Goal state after:
τ : ℂ
hτ : 0 < τ.im
this✝ : HasSum (fun n ↦ cexp (↑π * I * ↑n ^ 2 * τ)) (jacobiTheta τ)
this : HasSum (fun n ↦ cexp (↑π * I * ↑(n + 1) ^ 2 * τ) * 2) (jacobiTheta τ + -1)
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: ⊢ (fun τ ↦ jacobiTheta τ - 1) =O[comap im atTop] fun τ ↦ rexp (-π * τ.im)

Tactic:
simp_rw [IsBigO, IsBigOWith, Filter.eventually_comap, Filter.eventually_atTop]
  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 ?_⟩
  rw [Real.norm_eq_abs, Real.abs_exp, hτ, neg_mul]
  gcongr
  simp [pi_pos]

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

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ IsBoundedAtImInfty ((SlashInvariantForm.norm ℋ f).toFun ∣[k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ))] γ)

Tactic:
simp_rw [SlashInvariantForm.norm, IsBoundedAtImInfty, Filter.BoundedAtFilter]

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ ((∏ q, quotientFunc f q) ∣[k * ↑(Nat.card (↥ℋ ⧸ 𝒢.subgroupOf ℋ))] γ) =O[atImInfty] 1
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
G H : Subgroup Γ
hG : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
hGH : H ≤ G
⊢ ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
intro K L hK hL

Goal state after:
Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
G H : Subgroup Γ
hG : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
hGH : H ≤ G
K L : Set α
hK : IsCompact K
hL : IsCompact L
⊢ {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝⁴ : Group Γ
inst✝³ : TopologicalSpace α
inst✝² : MulAction Γ α
inst✝¹ : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
inst✝ : H.IsFiniteRelIndex G
⊢ ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
intro K L hK hL

Goal state after:
Γ : Type u_1
α : Type u_2
inst✝⁴ : Group Γ
inst✝³ : TopologicalSpace α
inst✝² : MulAction Γ α
inst✝¹ : ContinuousConstSMul Γ α
G H : Subgroup Γ
hH : ∀ {K L : Set α}, IsCompact K → IsCompact L → {g | g ∈ H ∧ (g • K ∩ L).Nonempty}.Finite
inst✝ : H.IsFiniteRelIndex G
K L : Set α
hK : IsCompact K
hL : IsCompact L
⊢ {g | g ∈ G ∧ (g • K ∩ L).Nonempty}.Finite
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
this : p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)
⊢ ∑ m ∈ range n, x ^ m * p ^ (n + 1 - m) * ↑((n + 1).choose m) + x ^ n * p * (↑n + 1) + x ^ (n + 1) -
        x ^ n * p * (↑n + 1) -
      x ^ (n + 1) =
    ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)

Tactic:
abel

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

Goal state before:
pp: case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
this : (2 * ↑n / ↑(h Γ)) ^ s = 2 ^ s * ↑n ^ s / ↑(h Γ) ^ s
⊢ p / ↑n ^ s = ↑π ^ (-s) * Gamma s * p / (2 * ↑n / ↑(h Γ)) ^ s * (2 ^ s * ↑π ^ s / Gamma s * ↑(h Γ) ^ (-s))

Tactic:
rw [this, cpow_neg, cpow_neg]

Goal state after:
case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
this : (2 * ↑n / ↑(h Γ)) ^ s = 2 ^ s * ↑n ^ s / ↑(h Γ) ^ s
⊢ p / ↑n ^ s = (↑π ^ s)⁻¹ * Gamma s * p / (2 ^ s * ↑n ^ s / ↑(h Γ) ^ s) * (2 ^ s * ↑π ^ s / Gamma s * (↑(h Γ) ^ s)⁻¹)
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)
⊢ IsOpen[topologicalSpace R A cofinite] (range (structureMap R A cofinite))

Tactic:
rw [range_structureMap]

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
⊢ IsOpen[topologicalSpace R A cofinite] {f | ∀ (i : ι), ↑f i ∈ A i}
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)
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i | IsCompact (A i) ∧ x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, x i ∈ A i
hSA : ∀ i ∈ S, IsCompact (A i)
this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
⊢ ∃ s, IsCompact s ∧ s ∈ Filter.map (inclusion R A hS) (𝓝 x')

Tactic:
rcases exists_compact_mem_nhds x' with ⟨K, K_compact, hK⟩

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝¹ i] (A i)
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
S : Set ι := {i | IsCompact (A i) ∧ x i ∈ A i}
hS : cofinite ≤ 𝓟 S
hSx : ∀ i ∈ S, x i ∈ A i
hSA : ∀ i ∈ S, IsCompact (A i)
this : WeaklyLocallyCompactSpace Πʳ (i : ι), [R i, A i]_[𝓟 S]
x' : Πʳ (i : ι), [R i, A i]_[𝓟 S]
hxx' : inclusion R A hS x' = x
K : Set Πʳ (i : ι), [R i, A i]_[𝓟 S]
K_compact : IsCompact K
hK : K ∈ 𝓝 x'
⊢ ∃ s, IsCompact s ∧ s ∈ Filter.map (inclusion R A hS) (𝓝 x')
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hx : Odd x
hn : Even n
hxy : Even (-(x - y))
⊢ y = -(x - y) + x

Tactic:
abel

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 : Πʳ (i : ι), [R i, A i] × Y → X
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map (inclusion R A hS) id)

Tactic:
refine ⟨fun H S hS ↦ H.comp ((continuous_inclusion hS).prodMap continuous_id),
    fun H ↦ ?_⟩
  simp_rw [continuous_iff_continuousAt, ContinuousAt]
  rintro ⟨x, y⟩
  set S : Set ι := {i | x i ∈ A i}
  have hS : cofinite ≤ 𝓟 S := le_principal_iff.mpr x.2
  have hxS : ∀ i ∈ S, x i ∈ A i := fun i hi ↦ hi
  rcases exists_inclusion_eq_of_eventually R A hS hxS with ⟨x', hxx'⟩
  rw [← hxx', nhds_prod_eq, nhds_eq_map_inclusion hAopen hS x',
    ← Filter.map_id (f := 𝓝 y), prod_map_map_eq, ← nhds_prod_eq, tendsto_map'_iff]
  exact H S hS |>.tendsto ⟨x', y⟩

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)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
inst✝² : (i : ι) → Inv (R i)
inst✝¹ : ∀ (i : ι), InvMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousInv (R i)
⊢ ∀ (S_1 : Set ι) (hS : 𝓕 ≤ 𝓟 S_1),
    Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 S_1), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
      ((fun a ↦ a⁻¹) ∘ inclusion R (fun i ↦ ↑(B i)) hS)

Tactic:
intro T hT

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T✝ : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
inst✝² : (i : ι) → Inv (R i)
inst✝¹ : ∀ (i : ι), InvMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousInv (R i)
T : Set ι
hT : 𝓕 ≤ 𝓟 T
⊢ Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 T), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
    ((fun a ↦ a⁻¹) ∘ inclusion R (fun i ↦ ↑(B i)) hT)
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousConstSMul G (R i)
g : G
⊢ ∀ (S_1 : Set ι) (hS : 𝓕 ≤ 𝓟 S_1),
    Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 S_1), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
      ((fun x ↦ g • x) ∘ inclusion R (fun i ↦ ↑(B i)) hS)

Tactic:
intro T hT

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T✝ : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousConstSMul G (R i)
g : G
T : Set ι
hT : 𝓕 ≤ 𝓟 T
⊢ Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 T), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
    ((fun x ↦ g • x) ∘ inclusion R (fun i ↦ ↑(B i)) hT)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : realMixedSpace K → ℝ≥0∞
x : realMixedSpace K
hx : x ∈ (polarCoordReal K).target
⊢ (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(polarCoordReal K).symm x) =
    ENNReal.ofReal |(FDerivPolarCoordRealSymm K x).det| * f (↑(polarCoordReal K).symm x)

Tactic:
simp_rw [det_fderivPolarCoordRealSymm, Finset.abs_prod,
    ENNReal.ofReal_prod_of_nonneg (fun _ _ ↦ abs_nonneg _), abs_of_mem_polarCoordReal_target K hx]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ (ENNReal.ofReal (2 * π) ^ Fintype.card { w // w.IsComplex } *
      ∫⁻ (a : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
        (⇑mixedSpaceOfRealSpace ⁻¹' normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A).indicator
          (fun x ↦ ∏ x, ENNReal.ofReal (a ↑x)) a ∂Measure.pi fun x ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w) ∂Measure.pi fun x ↦ volume

Tactic:
setLIntegral_indicator (by convert! hm.preimage mixedSpaceOfRealSpace.measurable)

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ (ENNReal.ofReal (2 * π) ^ Fintype.card { w // w.IsComplex } *
      ∫⁻ (a : InfinitePlace K → ℝ) in
        ⇑mixedSpaceOfRealSpace ⁻¹' normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A ∩
          Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
        (fun x ↦ ∏ x, ENNReal.ofReal (a ↑x)) a ∂Measure.pi fun x ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w) ∂Measure.pi fun x ↦ volume