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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
y : Ideal S
hy : normalizedFactors (Ideal.map (algebraMap R S) I) = {y}
h : y = Ideal.map (algebraMap R S) I
⊢ Irreducible (Ideal.map (algebraMap R S) I)

Tactic:
← h

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : Module.IsTorsionFree R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
hf : Irreducible (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
mem_norm_factors :
  normalize (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x)) ∈
    normalizedFactors (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))
y : Ideal S
hy : normalizedFactors (Ideal.map (algebraMap R S) I) = {y}
h : y = Ideal.map (algebraMap R S) I
⊢ Irreducible y
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
this : ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s = 0
⊢ completedLFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s

Tactic:
completedLFunction,

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
s : ℂ
this : ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s = 0
⊢ ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s +
      ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s =
    ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : hurwitzZetaEven (↑x) (-(2 * ↑k)) = 0
⊢ hurwitzZetaOdd (↑x) (-(2 * ↑k)) =
    -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))

Tactic:
hurwitzZetaOdd_neg_two_mul_nat hk hx

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : hurwitzZetaEven (↑x) (-(2 * ↑k)) = 0
⊢ -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1))) =
    -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
Module: Mathlib.NumberTheory.LSeries.ZMod

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
this : ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0
⊢ completedLFunction Φ s = ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s

Tactic:
completedLFunction,

Goal state after:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
this : ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s = 0
⊢ ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaEven (toAddCircle j) s +
      ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s =
    ↑N ^ (-s) * ∑ j, Φ j * completedHurwitzZetaOdd (toAddCircle j) s
Module: Mathlib.NumberTheory.LSeries.Linearity

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

Tactic:
by
  simp [term_add]

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

Goal state before:
pp: case e'_6
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
hz : ‖χ ↑n * ↑n ^ (-(I * ↑y))‖ = 1
⊢ χ ↑n ^ 2 * ↑n ^ (-(↑x + 2 * I * ↑y)) = ↑(↑n ^ (-x)) * (χ ↑n * ↑n ^ (-(I * ↑y))) ^ 2

Tactic:
· rw [neg_add, cpow_add _ _ <| mod_cast by lia, ← ofReal_neg, ofReal_cpow n.cast_nonneg (-x),
        ofReal_natCast, show -(2 * I * y) = (2 : ℕ) * -(I * y) by ring, cpow_nat_mul, mul_pow,
        mul_left_comm]

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

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

Tactic:
convert! (ofReal_re _).symm
    rw [ofReal_mul]; rw [← mul_div]; congr
    · rw [ofReal_div, ofReal_one, ofReal_pow]; rfl
    · rw [ofReal_cos, ofReal_mul, fourier_coe_apply, fourier_coe_apply, cos, ofReal_one, div_one,
        div_one, ofReal_mul, ofReal_mul, ofReal_two, Int.cast_neg, Int.cast_natCast,
        ofReal_natCast]
      congr 3
      · ring
      · ring

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

Goal state before:
pp: q : ℕ
a : ZMod q
⊢ Summable fun n ↦ (if Nat.Prime n then 0 else residueClass a n) / ↑n

Tactic:
have h₀ (n : ℕ) : 0 ≤ (if n.Prime then 0 else residueClass a n) / n := by
    positivity [residueClass_nonneg a n]
  have hleF₀ (n : ℕ) : (if n.Prime then 0 else residueClass a n) / n ≤ F₀ n := by
    refine div_le_div_of_nonneg_right ?_ n.cast_nonneg
    split_ifs; exacts [le_rfl, residueClass_le a n]
  refine Summable.of_nonneg_of_le h₀ hleF₀ ?_
  have hF₀ (p : Nat.Primes) : F₀ p.val = 0 := by
    simp only [p.prop, ↓reduceIte, zero_div, F₀]
  refine (summable_subtype_iff_indicator (s := {n | IsPrimePow n}).mp ?_).congr
      fun n ↦ Set.indicator_apply_eq_self.mpr fun (hn : ¬ IsPrimePow n) ↦ ?_
  swap
  · simp +contextual only [div_eq_zero_iff, ite_eq_left_iff, vonMangoldt_eq_zero_iff, hn,
      not_false_eq_true, implies_true, Nat.cast_eq_zero, true_or, F₀]
  have hFF' :
      F₀ ∘ Subtype.val (p := fun n ↦ n ∈ {n | IsPrimePow n}) = F' ∘ ⇑prodNatEquiv.symm := by
    refine (Equiv.eq_comp_symm prodNatEquiv (F₀ ∘ Subtype.val) F').mpr ?_
    ext1 n
    simp only [Function.comp_apply, F']
    congr
  rw [hFF']
  refine (Nat.Primes.prodNatEquiv.symm.summable_iff (f := F')).mpr ?_
  have hF'₀ (p : Nat.Primes) : F' (p, 0) = 0 := by simp only [zero_add, pow_one, hF₀, F']
  have hF'₁ : F'' = F' ∘ (Prod.map _root_.id (· + 1)) := by
    ext1
    simp only [Function.comp_apply, Prod.map_fst, id_eq, Prod.map_snd, F'', F']
  refine (Function.Injective.summable_iff ?_ fun u hu ↦ ?_).mp <| hF'₁ ▸ summable_F''
  · exact Function.Injective.prodMap (fun ⦃a₁ a₂⦄ a ↦ a) <| add_left_injective 1
  · simp only [Set.range_prodMap, Set.range_id, Set.mem_prod, Set.mem_univ, Set.mem_range,
      Nat.exists_add_one_eq, true_and, not_lt, nonpos_iff_eq_zero] at hu
    rw [← hF'₀ u.1, ← hu]

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

Goal state before:
pp: case inl
this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
⊢ riemannZetaZerosᶜ ∈ nhdsWithin 1 {1}ᶜ

pp: case inr
this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
x : ℂ
hx : x ≠ 1
⊢ riemannZetaZerosᶜ ∈ nhdsWithin x {x}ᶜ

Tactic:
· exact riemannZeta_eventually_ne_zero_nhds_one.filter_mono nhdsWithin_le_nhds

Goal state after:
case inr
this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
x : ℂ
hx : x ≠ 1
⊢ riemannZetaZerosᶜ ∈ nhdsWithin x {x}ᶜ
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : DenselyOrdered (ValueGroupWithZero R)
⊢ (Set.range ⇑(ValueGroupWithZero.orderMonoidIso v).toMonoidWithZeroHom).Subsingleton

Tactic:
← WithZero.denselyOrdered_set_iff_subsingleton

Goal state after:
case pos
R : Type u_1
inst✝² : Ring R
inst✝¹ : ValuativeRel R
v : Valuation R (WithZero (Multiplicative ℤ))
inst✝ : v.Compatible
this : IsRankLeOne R
h : IsNontrivial R
H : DenselyOrdered (ValueGroupWithZero R)
⊢ DenselyOrdered ↑(Set.range ⇑(ValueGroupWithZero.orderMonoidIso v).toMonoidWithZeroHom)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

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

Tactic:
by
  induction l with
  | nil => simp only [List.prod_nil, List.map_nil, one_left]
  | cons n l' ih => rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]

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 : ℝ
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
⊢ 1 < (↑s).re

Tactic:
by rwa [ofReal_re]

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

Goal state before:
pp: K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
⊢ ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite

Tactic:
intro z

Goal state after:
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
⊢ (Set.Icc z 1).Finite
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
Γ✝ Γ : Subgroup (GL n R)
inst✝ : Γ.HasDetOne
g : ConjAct (GL n R)
h : GL n R
hh : h ∈ g • Γ
⊢ GeneralLinearGroup.det h = 1

Tactic:
rw [mem_pointwise_smul_iff_inv_smul_mem] at hh

Goal state after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
Γ✝ Γ : Subgroup (GL n R)
inst✝ : Γ.HasDetOne
g : ConjAct (GL n R)
h : GL n R
hh : g⁻¹ • h ∈ Γ
⊢ GeneralLinearGroup.det h = 1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
Γ✝ Γ : Subgroup (GL n R)
inst✝ : Γ.HasDetPlusMinusOne
g : ConjAct (GL n R)
h : GL n R
hh : h ∈ g • Γ
⊢ GeneralLinearGroup.det h = 1 ∨ GeneralLinearGroup.det h = -1

Tactic:
rw [mem_pointwise_smul_iff_inv_smul_mem] at hh

Goal state after:
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
R : Type u_2
inst✝¹ : CommRing R
Γ✝ Γ : Subgroup (GL n R)
inst✝ : Γ.HasDetPlusMinusOne
g : ConjAct (GL n R)
h : GL n R
hh : g⁻¹ • h ∈ Γ
⊢ GeneralLinearGroup.det h = 1 ∨ GeneralLinearGroup.det h = -1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case pos
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 ∈ 𝒢
hn : Even (Fintype.card n)
⊢ GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

Tactic:
convert! HasDetPlusMinusOne.det_eq hg using 1

Goal state after:
case e'_1
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 ∈ 𝒢
hn : Even (Fintype.card n)
⊢ GeneralLinearGroup.det g = 1 ↔ GeneralLinearGroup.det (-g) = 1

case e'_2
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 ∈ 𝒢
hn : Even (Fintype.card n)
⊢ 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
  fin_cases i <;>
  simp [mulVec_eq_sum]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
k : ℤ
A : SL(2, ℤ)
f : ℍ → ℂ
c : α
⊢ (c • f) ∣[k] A = c • f ∣[k] A

Tactic:
ext τ : 1
  simp [SL_slash_apply, Pi.smul_apply, smul_mul_assoc]

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 _)⟩
  rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, isCusp_SL2Z_iff'] at hc
  obtain ⟨g, rfl⟩ := hc
  use ⟦g⁻¹⟧
  aesop

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

Goal state before:
pp: case pos
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : DiscreteTopology ↥𝒢.strictPeriods
⊢ 𝒢.strictWidthInfty ∈ 𝒢.strictPeriods

Tactic:
simp [strictPeriods_eq_zmultiples_strictWidthInfty]

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

Goal state before:
pp: E : Type u_3
inst✝ : NormedAddCommGroup E
f : ℍ → E
a : ℝ
ha : a > 0
ha' : f =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)
⊢ Tendsto (HMul.hMul (-a)) atTop atBot

Tactic:
exact tendsto_id.const_mul_atTop_of_neg (neg_lt_zero.mpr ha)

Goal state after:
Module: Mathlib.NumberTheory.Modular

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

Tactic:
intro z

Goal state after:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = 1
hd : ↑g 1 1 = 1
this : g = T ^ ↑g 0 1
z : ℍ
⊢ g • z = T ^ ↑g 0 1 • z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

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

Tactic:
simp only [divIntMap, mem_gammaSet_one] at *

Goal state after:
case refine_1
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 r 0
⊢ IsCoprime ((x / ↑↑r) 0) ((x / ↑↑r) 1)
Module: Mathlib.NumberTheory.Modular

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

Tactic:
intro z

Goal state after:
g : SL(2, ℤ)
hc : ↑g 1 0 = 0
had : ↑g 0 0 * ↑g 1 1 = 1
ha : ↑g 0 0 = -1
hd : ↑g 1 1 = -1
this : g = -T ^ (-↑g 0 1)
z : ℍ
⊢ g • z = T ^ (-↑g 0 1) • z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: case h
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ r • x ∈ gammaSet 1 r 0 ∧ divIntMap (↑r) (r • x) = x

Tactic:
simp only [nsmul_eq_mul, divIntMap, Int.cast_natCast]

Goal state after:
case h
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ ↑r * x ∈ gammaSet 1 r 0 ∧ ↑r * x / ↑r = x
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
⊢ ∀ (z : ℍ),
    2 ≤ z.im →
      ‖(⇑{ toFun := eisensteinSeries a k, slash_action_eq' := ⋯ } ∣[k] A) z‖ ≤
        ∑' (x : Fin 2 → ℤ), r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖x‖ ^ (-k)

Tactic:
intro z

Goal state after:
N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
⊢ 2 ≤ z.im →
    ‖(⇑{ toFun := eisensteinSeries a k, slash_action_eq' := ⋯ } ∣[k] A) z‖ ≤
      ∑' (x : Fin 2 → ℤ), r { coe := { re := ↑N, im := 2 }, coe_im_pos := ⋯ } ^ (-k) * ‖x‖ ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable

Goal state before:
pp: k : ℤ
a : Fin 2 → ℤ
⊢ ∀ x ∈ {z | 0 < z.im}, (eisSummand k a ∘ ↑ofComplex) x = (↑(a 0) * x + ↑(a 1)) ^ (-k)

Tactic:
intro z

Goal state after:
k : ℤ
a : Fin 2 → ℤ
z : ℂ
⊢ z ∈ {z | 0 < z.im} → (eisSummand k a ∘ ↑ofComplex) z = (↑(a 0) * z + ↑(a 1)) ^ (-k)
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
h00 : ∑' (b : ℕ+) (c : ℕ+), ↑↑b ^ k * r ^ (↑c * ↑b) = ∑' (e : ℕ+), ↑((σ k) ↑e) * r ^ ↑e
⊢ ∑' (n : ℕ+) (n_1 : ℕ+), ↑↑n ^ k * (r ^ ↑n) ^ ↑n_1 = ∑' (n : ℕ+), ↑((σ k) ↑n) * r ^ ↑n

Tactic:
rw [← h00]

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
r : 𝕜
hr : ‖r‖ < 1
k : ℕ
this : ∀ (m : ℕ) [NeZero m], ∑' (n : ℕ), (r ^ m) ^ n = (1 - r ^ m)⁻¹
h00 : ∑' (b : ℕ+) (c : ℕ+), ↑↑b ^ k * r ^ (↑c * ↑b) = ∑' (e : ℕ+), ↑((σ k) ↑e) * r ^ ↑e
⊢ ∑' (n : ℕ+) (n_1 : ℕ+), ↑↑n ^ k * (r ^ ↑n) ^ ↑n_1 = ∑' (b : ℕ+) (c : ℕ+), ↑↑b ^ k * r ^ (↑c * ↑b)
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ 2⁻¹ * ‖∑ x ∈ Icc (-(x - 1)) (x - 1), f x + (f (-x) + ∑ x ∈ {x}, f x) - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖ = ‖f x‖

pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ -x ∉ {x}

pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ Disjoint (Icc (-(x - 1)) (x - 1)) {-x, x}

Tactic:
Finset.sum_singleton,

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ 2⁻¹ * ‖∑ x ∈ Icc (-(x - 1)) (x - 1), f x + (f (-x) + f x) - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖ = ‖f x‖

F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ -x ∉ {x}

F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ Disjoint (Icc (-(x - 1)) (x - 1)) {-x, x}
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ 2⁻¹ * ‖f x + f x‖ = ‖f x‖

pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ -x ∉ {x}

pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ Disjoint (Icc (-(x - 1)) (x - 1)) {-x, x}

Tactic:
← two_zsmul,

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ 2⁻¹ * ‖2 • f x‖ = ‖f x‖

F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ -x ∉ {x}

F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this✝ : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
this : Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x}
⊢ Disjoint (Icc (-(x - 1)) (x - 1)) {-x, x}
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case mem.inl
γ g : SL(2, ℤ)
h1 : g = S
⊢ G2 ∣[2] g = G2 - D2 g

pp: case mem.inr
γ g : SL(2, ℤ)
h2 : g = T
⊢ G2 ∣[2] g = G2 - D2 g

Tactic:
· ext z
        simp only [Pi.sub_apply, h1, D2_S z, SlashInvariantForm.slash_S_apply G2 2 z, mul_comm,
          G2_S_transform z, modular_S_smul]
        ring_nf
        aesop

Goal state after:
case mem.inr
γ g : SL(2, ℤ)
h2 : g = T
⊢ G2 ∣[2] g = G2 - D2 g
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case mem
γ g : SL(2, ℤ)
hg : g ∈ {S, T}
⊢ G2 ∣[2] g = G2 - D2 g

Tactic:
| mem g hg =>

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

Goal state before:
pp: F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ ↑ofComplex) {z | 0 < z.im}
c : ℂ := (2 * ↑π * I)⁻¹
hDeriv : DifferentiableOn ℂ (fun z ↦ c * deriv (F ∘ ↑ofComplex) z) upperHalfPlaneSet
⊢ ∀ x ∈ upperHalfPlaneSet, (D F ∘ ↑ofComplex) x = c * deriv (F ∘ ↑ofComplex) x

Tactic:
intro z

Goal state after:
F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ ↑ofComplex) {z | 0 < z.im}
c : ℂ := (2 * ↑π * I)⁻¹
hDeriv : DifferentiableOn ℂ (fun z ↦ c * deriv (F ∘ ↑ofComplex) z) upperHalfPlaneSet
z : ℂ
⊢ z ∈ upperHalfPlaneSet → (D F ∘ ↑ofComplex) z = c * deriv (F ∘ ↑ofComplex) z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inr
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
⊢ normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) = 1

Tactic:
rcases case_c_one_d_neg_one hz hg hden hc hd with ⟨(rfl | rfl), rfl⟩
      · rw [show S * T⁻¹ = ⟨!![0, -1; 1, -1], by simp⟩ by decide]
        norm_num [ρ, denom, normSq, ← pow_two, div_pow]
      · rw [show T⁻¹ * S * T⁻¹ = ⟨!![-1, 0; 1, -1], by simp⟩ by decide]
        norm_num [ρ, denom, normSq, ← pow_two, div_pow]

Goal state after: