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

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

Tactic:
convert! (ofReal_re _).symm
    rw [ofReal_mul, ofReal_div, ofReal_div, ofReal_mul, ofReal_pow, ofReal_pow, ofReal_neg,
      ofReal_natCast, ofReal_mul, ofReal_two, ofReal_one, ← div_div, div_I,
      div_mul_eq_mul_div₀]
    have : ∀ α β γ δ : ℂ, α * I * β / γ * δ * I = I ^ 2 * α * β / γ * δ := by intros; ring
    rw [this, I_sq]
    rw [bernoulliFun]
    ring

Goal state after:
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: n q : ℕ
a : ℤ
hq : q ≠ 0
h : IsCoprime a ↑q
this : NeZero q
⊢ IsUnit ↑a

Tactic:
rwa [ZMod.coe_int_isUnit_iff_isCoprime, isCoprime_comm]

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

Goal state before:
pp: a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, ∃ (_ : Nat.Prime a_1 ∧ a_1 ∣ b), ↑a_1 ∣ a) ↔ ∃ p, Nat.Prime p ∧ p ∣ a.natAbs ∧ p ∣ (↑b).natAbs

Tactic:
← Int.natCast_dvd,

Goal state after:
a : ℤ
b : ℕ
inst✝ : NeZero b
⊢ (∃ a_1, ∃ (_ : Nat.Prime a_1 ∧ a_1 ∣ b), ↑a_1 ∣ a) ↔ ∃ p, Nat.Prime p ∧ ↑p ∣ a ∧ ↑p ∣ ↑b
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑(2 ^ e) | b) * J(↑a' | b) = J(↑(2 ^ e) | b % (4 * a)) * J(↑a' | b % (4 * a))

Tactic:
quadratic_reciprocity' ha₁ hb,

Goal state after:
case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑(2 ^ e) | b) * (qrSign b a' * J(↑b | a')) = J(↑(2 ^ e) | b % (4 * a)) * J(↑a' | b % (4 * a))
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case ind.isTrue
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : a % 4 = 0
⊢ (if flip = true then -J(↑(a / 4) | b) else J(↑(a / 4) | b)) = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
simp only [Int.natCast_ediv, Nat.cast_ofNat, div_four_left (a := a) (mod_cast ha4) hb2]

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

Goal state before:
pp: case pos
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) = 0

Tactic:
rw [mod_left, hab, zero_left (lt_of_le_of_ne (Nat.pos_of_ne_zero hb0) (Ne.symm hb1))]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case mpr
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) = 0 → ↑(sMod p (p - 2)) = 0

Tactic:
intro h
    rw [h]
    simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
pow2 : 2 ^ ((q + 1) / 2) = 2
this : (2 * ω) ^ ((q + 1) / 2) = -2
⊢ ω ^ ((q + 1) / 2) = -1

Tactic:
rw [mul_pow] at this

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
pow2 : 2 ^ ((q + 1) / 2) = 2
this : 2 ^ ((q + 1) / 2) * ω ^ ((q + 1) / 2) = -2
⊢ ω ^ ((q + 1) / 2) = -1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : NeZero q
w : 1 < q
⊢ Fintype.card (X q)ˣ < q ^ 2

Tactic:
have : Fact (1 < (q : ℕ)) := ⟨w⟩

Goal state after:
q : ℕ
inst✝ : NeZero q
w : 1 < q
this : Fact (1 < q)
⊢ Fintype.card (X q)ˣ < q ^ 2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this✝ : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
this : X.ω ^ ((mersenne (p' + 2) + 1) / 4) + X.ωb ^ ((mersenne (p' + 2) + 1) / 4) = 0
⊢ (X.ω ^ 2 ^ p' + X.ωb ^ 2 ^ p').1 = 0

Tactic:
rw [succ_mersenne, pow_add, show 2 ^ 2 = 4 by norm_num, mul_div_cancel_right₀ _ (by norm_num)]
    at this

Goal state after:
p' : ℕ
w : 3 ≤ p' + 2
hp : Nat.Prime (mersenne (p' + 2))
this✝ : Fact (Nat.Prime (mersenne (p' + 2)))
hp' : p' = p' + 2 - 2
this : X.ω ^ 2 ^ p' + X.ωb ^ 2 ^ p' = 0
⊢ (X.ω ^ 2 ^ p' + X.ωb ^ 2 ^ p').1 = 0
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case inl
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

pp: case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

Tactic:
· exact HasDetPlusMinusOne.det_eq hg

Goal state after:
case inr
n : Type u_1
inst✝² : Fintype n
inst✝¹ : DecidableEq n
R : Type u_3
inst✝ : CommRing R
𝒢 : Subgroup (GL n R)
x✝ : 𝒢.HasDetPlusMinusOne
g : GL n R
hg : -g ∈ 𝒢
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
⊢ m *ᵥ v = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1]

Tactic:
ext i

Goal state after:
R : Type u_1
inst✝ : Semiring R
m : Matrix (Fin 2) (Fin 2) R
v : Fin 2 → R
i : Fin 2
⊢ (m *ᵥ v) i = ![m 0 0 * v 0 + m 0 1 * v 1, m 1 0 * v 0 + m 1 1 * v 1] i
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case h
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
this : w 0 ≠ 0
⊢ (w 0)⁻¹ • w = ![1, 0]

Tactic:
ext i

Goal state after:
case h
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
this : w 0 ≠ 0
i : Fin 2
⊢ ((w 0)⁻¹ • w) i = ![1, 0] i
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
⊢ M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast) =
    ↑M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast)

Tactic:
Nat.cast_smul_eq_nsmul

Goal state after:
g : GL (Fin 2) ℚ
M : ℕ
inst✝ : NeZero M
A₁ : Matrix (Fin 2) (Fin 2) ℚ := ↑g
A₂ : Matrix (Fin 2) (Fin 2) ℚ := ↑g⁻¹
hA₁₂ : A₁ * A₂ = 1
a₁ : ℕ := A₁.den
a₂ : ℕ := A₂.den
x✝ : SL(2, ℤ)
y : Matrix (Fin 2) (Fin 2) ℤ
hy : y.det = 1
hy' : ⟨y, hy⟩ ∈ Γ(a₁ * a₂ * M)
k : Matrix (Fin 2) (Fin 2) ℤ
hk : y = 1 + (a₁ * a₂ * M) • k
z : Matrix (Fin 2) (Fin 2) ℤ := 1 + M • (A₁.num * k * A₂.num)
⊢ M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast) =
    M • (A₁.num.map Int.cast * k.map Int.cast * A₂.num.map Int.cast)
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
hΓ : IsCongruenceSubgroup Γ
g : GL (Fin 2) ℚ
⊢ IsCongruenceSubgroup (CongruenceSubgroup.conjGL Γ ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))

Tactic:
obtain ⟨M, hN, hΓM⟩ := hΓ
  have _ : NeZero M := ⟨hN⟩
  obtain ⟨N, hN, hN'⟩ := exists_Gamma_le_conj' g M
  rw [Subgroup.pointwise_smul_subset_iff] at hN'
  refine ⟨N, ‹_›, fun x hx ↦ ?_⟩
  obtain ⟨y, hy, hy'⟩ := Subgroup.mem_inv_pointwise_smul_iff.mp <| hN' ⟨x, hx, rfl⟩
  exact mem_conjGL.mpr ⟨y, hΓM hy, hy'⟩

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.Identities

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

Tactic:
rw [← congr_fun (slash_action_eqn f _ <| Γ.mem_strictPeriods_iff.mp hH) τ]
  suffices GeneralLinearGroup.upperRightHom h • τ = h +ᵥ τ by
    simp_rw [slash_def, this]
    simp [σ, denom, GeneralLinearGroup.val_det_apply, denom]
  ext
  simp [σ, num, denom, coe_vadd, UpperHalfPlane.coe_smul, num, add_comm]

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

Goal state before:
pp: case mpr.inv
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ ∀ x ∈ Subgroup.closure s, f ∣[k] x = f → f ∣[k] x⁻¹ = f

Tactic:
intro x hx hf

Goal state after:
case mpr.inv
f : ℍ → ℂ
Γ : Subgroup (GL (Fin 2) ℝ)
s : Set (GL (Fin 2) ℝ)
hΓ : Γ = Subgroup.closure s
k : ℤ
h : ∀ γ ∈ s, f ∣[k] γ = f
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
x : GL (Fin 2) ℝ
hx : x ∈ Subgroup.closure s
hf : f ∣[k] x = f
⊢ f ∣[k] x⁻¹ = f
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)]
c : Fin 2 → ℝ
hz : (↑z).im ≠ 0
⊢ (↑z).im⁻¹ • g (f c) = c

Tactic:
ext i

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

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

Tactic:
mul_left_comm,

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

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

Tactic:
mul_left_comm,

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

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
g : GL (Fin 2) ℝ
τ : ℍ
D : ℝ := |↑(Matrix.GeneralLinearGroup.det g)|
hD : ↑D ≠ 0
j : ℂ := denom g ↑τ
⊢ ↑D ^ (k - 2) * ((starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) * ↑(g • τ).im ^ k) =
    ↑D ^ (k - 2) * (σ g) (petersson k f f' (g • τ))

Tactic:
simp [petersson, σ_conj]

Goal state after:
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
h : Int.cast ∘ p = 0
⊢ p = 0

Tactic:
ext i

Goal state after:
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
h : Int.cast ∘ p = 0
i : Fin 2
⊢ p i = 0 i
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case hasSum
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
y : ℂ
hy : y ∈ eball 0 ↑1
⊢ HasSum (fun n ↦ (FormalMultilinearSeries.ofScalars ℂ c n) fun x ↦ y) (update (cuspFunction h f) 0 (c 0) (0 + y))

Tactic:
Metric.eball_coe,

Goal state after:
case hasSum
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
y : ℂ
hy : y ∈ ball 0 ↑1
⊢ HasSum (fun n ↦ (FormalMultilinearSeries.ofScalars ℂ c n) fun x ↦ y) (update (cuspFunction h f) 0 (c 0) (0 + y))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: case refine_2
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 r 0
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hv2 : divIntMap (↑r) x = divIntMap (↑r) v
⊢ x = v

Tactic:
ext i

Goal state after:
case refine_2
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 r 0
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hv2 : divIntMap (↑r) x = divIntMap (↑r) v
i : Fin 2
⊢ x i = v i
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: case h.right
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ ↑r * x / ↑r = x

Tactic:
ext i

Goal state after:
case h.right
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
i : Fin 2
⊢ (↑r * x / ↑r) i = x i
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
⊢ v = 0

Tactic:
ext i

Goal state after:
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
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: case neg
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : ¬r = 0
⊢ v = r • divIntMap (↑r) v

Tactic:
ext i

Goal state after:
case neg
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : ¬r = 0
i : Fin 2
⊢ v i = (r • divIntMap (↑r) v) i
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
⊢ v = r • (v / ↑r)

Tactic:
ext i

Goal state after:
r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
i : Fin 2
⊢ v i = (r • (v / ↑r)) i
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝¹ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this✝ : |↑(↑g 1 1) + z.re| ≤ 1
this : |↑(↑g 1 1)| - |z.re| ≤ 1
⊢ |↑g 1 1| ≤ 1

Tactic:
grw [sub_le_iff_le_add, hz.2, ← Int.cast_abs, ← Int.le_floor] at this

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝¹ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this✝ : |↑(↑g 1 1) + z.re| ≤ 1
this : |↑g 1 1| ≤ ⌊1 + 1 / 2⌋
⊢ |↑g 1 1| ≤ 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: ⊢ D2 ModularGroup.T = 0

Tactic:
by
  ext z
  simp [D2, ModularGroup.T]

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

Goal state before:
pp: case h
⊢ ∀ K ⊆ Metric.ball 0 1,
    IsCompact K → HasProdUniformlyOn (fun n q ↦ 1 + -q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K

Tactic:
intro K hK hcK

Goal state after:
case h
K : Set ℂ
hK : K ⊆ Metric.ball 0 1
hcK : IsCompact K
⊢ HasProdUniformlyOn (fun n q ↦ 1 + -q ^ (n + 1)) (fun q ↦ ∏' (n : ℕ), (1 + -q ^ (n + 1))) K
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
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
⊢ (2 * ↑π * I)⁻¹ * deriv (F ∣[k] g ∘ ↑ofComplex) ↑z =
    (↑(↑g).det)⁻¹ *
        ((σ g) ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z)) *
            ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k + 2 - 1) *
          denom g ↑z ^ (-(k + 2))) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) *
        ((σ g) (F (g • z)) * ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 1) * denom g ↑z ^ (-k))

Tactic:
have hz := denom_ne_zero g z

Goal state after:
k : ℤ
F : ℍ → ℂ
hF : MDiff F
g : GL (Fin 2) ℝ
hg : 0 < (↑g).det
hdet : ↑(Matrix.GeneralLinearGroup.det g) = (↑g).det
hdetℂ : ↑(↑g).det ≠ 0
hσ : ∀ (x : ℂ), (σ g) x = x
z : ℍ
hz : denom g ↑z ≠ 0
⊢ (2 * ↑π * I)⁻¹ * deriv (F ∣[k] g ∘ ↑ofComplex) ↑z =
    (↑(↑g).det)⁻¹ *
        ((σ g) ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z)) *
            ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k + 2 - 1) *
          denom g ↑z ^ (-(k + 2))) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) *
        ((σ g) (F (g • z)) * ↑|↑(Matrix.GeneralLinearGroup.det g)| ^ (k - 1) * denom g ↑z ^ (-k))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : f =O[atTop] fun n ↦ ↑n ^ l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace ↑K
c : C(↑K, ℂ) := { toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
n : ℕ
z : ℂ
hz : z ∈ K
h0 : ‖cexp (2 * ↑π * I * z / ↑p)‖ ^ n ≤ ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ ^ n
hr : ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ < 1
⊢ ‖f n‖ * ((2 * |π| * ↑n / |p|) ^ k * ‖cexp (2 * ↑π * I * ↑n * z / ↑p)‖) ≤
    ‖f n‖ * (2 * |π| * ↑n / |p|) ^ k * ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ ^ n

Tactic:
rw [← mul_assoc]

Goal state after:
k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : f =O[atTop] fun n ↦ ↑n ^ l
K : Set ℂ
hK : K ⊆ ℍₒ
hKc : IsCompact K
this : CompactSpace ↑K
c : C(↑K, ℂ) := { toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }
r : ℝ := ‖mkOfCompact c‖
n : ℕ
z : ℂ
hz : z ∈ K
h0 : ‖cexp (2 * ↑π * I * z / ↑p)‖ ^ n ≤ ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ ^ n
hr : ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ < 1
⊢ ‖f n‖ * (2 * |π| * ↑n / |p|) ^ k * ‖cexp (2 * ↑π * I * ↑n * z / ↑p)‖ ≤
    ‖f n‖ * (2 * |π| * ↑n / |p|) ^ k * ‖{ toFun := fun r ↦ cexp (2 * ↑π * I * ↑r / ↑p), continuous_toFun := ⋯ }‖ ^ n
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ ↑ρ = ↑{ coe := (-↑(1 +ᵥ ρ))⁻¹, coe_im_pos := ⋯ }

Tactic:
norm_num [ρ, Complex.ext_iff, normSq, ← pow_two, div_pow]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
x : ℍ
hx✝ : 1 ≤ ‖↑x‖
hx' : |x.re| ≤ 1 / 2
hx : 1 = ‖↑x‖
⊢ x ∈ closure 𝒟ᵒ

Tactic:
· exact mem_closure_of_arc hx.symm hx'

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

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
⊢ DifferentiableAt ℂ jacobiTheta τ

Tactic:
simp_rw [funext jacobiTheta_eq_jacobiTheta₂]

Goal state after:
τ : ℂ
hτ : 0 < τ.im
⊢ DifferentiableAt ℂ (jacobiTheta₂ 0) τ
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this : ModularFormClass
  (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range
    (0 *
      ↑(Nat.card
          (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range))))
  (Matrix.SpecialLinearGroup.mapGL ℝ).range 0 :=
  Eq.mpr
    (id
      (congrArg
        (fun _a ↦
          ModularFormClass (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range _a)
            (Matrix.SpecialLinearGroup.mapGL ℝ).range 0)
        (zero_mul
          ↑(Nat.card
              (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range)))))
    inferInstance
⊢ ∃ c, ⇑f = Function.const ℍ c

Tactic:
obtain ⟨c, hc⟩ := ModularFormClass.levelOne_weight_zero_const
    (ModularForm.norm 𝒮ℒ (f - .const (f I)))

Goal state after:
𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : 𝒢.IsArithmetic
inst✝ : 𝒢.HasDetOne
f : ModularForm 𝒢 0
this : ModularFormClass
  (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range
    (0 *
      ↑(Nat.card
          (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range))))
  (Matrix.SpecialLinearGroup.mapGL ℝ).range 0 :=
  Eq.mpr
    (id
      (congrArg
        (fun _a ↦
          ModularFormClass (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range _a)
            (Matrix.SpecialLinearGroup.mapGL ℝ).range 0)
        (zero_mul
          ↑(Nat.card
              (↥(Matrix.SpecialLinearGroup.mapGL ℝ).range ⧸ 𝒢.subgroupOf (Matrix.SpecialLinearGroup.mapGL ℝ).range)))))
    inferInstance
c : ℂ
hc : ⇑(ModularForm.norm (Matrix.SpecialLinearGroup.mapGL ℝ).range (f - const (f I))) = Function.const ℍ c
⊢ ∃ c, ⇑f = Function.const ℍ c
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case refine_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
t : ℝ
⊢ t ∈ Set.Ioi 0 →
    HasSum
      (fun i ↦
        if 2 * ↑i / h Γ = 0 then 0 else (PowerSeries.coeff i) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑i / h Γ) * t)))
      ((weakFEPair hk f).f t - (weakFEPair hk f).f₀)

Tactic:
(ht : 0 < t)

Goal state after:
case refine_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
t : ℝ
ht : 0 < t
⊢ HasSum
    (fun i ↦
      if 2 * ↑i / h Γ = 0 then 0 else (PowerSeries.coeff i) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑i / h Γ) * t)))
    ((weakFEPair hk f).f t - (weakFEPair hk f).f₀)
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
x : WithAbs ↑v
⊢ ‖(v.embedding.comp (WithAbs.equiv ↑v).toRingHom) x‖ = ‖x‖

Tactic:
simpa using! v.norm_embedding_eq (WithAbs.equiv v.1 x)

Goal state after: