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

Goal state before:
pp: case neg
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r : K
hr : r ≠ 0
hr1 : (valuation K) r < 1
H : {x | (valuation K).restrict x ≤ (valuation K).restrict r} ⊆ s
⊢ IsCompact {x | (valuation K).restrict x ≤ (valuation K).restrict γ}

Tactic:
convert!
    (hs'.of_isClosed_subset (Valued.isClosed_closedBall K _) H).image
      (Homeomorph.mulLeft₀ (γ / r) (by simp [hr, div_eq_zero_iff, hγ])).continuous using 1

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r : K
hr : r ≠ 0
hr1 : (valuation K) r < 1
H : {x | (valuation K).restrict x ≤ (valuation K).restrict r} ⊆ s
⊢ {x | (valuation K).restrict x ≤ (valuation K).restrict γ} =
    ⇑(Homeomorph.mulLeft₀ (γ / r) ⋯) '' {x | Valued.v.restrict x ≤ (valuation K).restrict r}
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:
mod_left,

Goal state after:
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 | b) = 0
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
x : A
hx1✝ : x ∈ Subring.center A
hx1 : ∀ (g : A), g * x = x * g
hx2 : x ≠ 0
⊢ ∀ {x_1 : A}, (x_1 ∈ Set.range fun x_2 ↦ x * x_2) → -x_1 ∈ Set.range fun x_2 ↦ x * x_2

Tactic:
by rintro _ ⟨x, rfl⟩; exact ⟨-x, by simp⟩

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.MaricaSchoenheim

Goal state before:
pp: case calc_3
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ ∀ ⦃x : ℕ⦄,
    x < n →
      ∀ ⦃x_1 : ℕ⦄,
        x_1 < n →
          ∀ ⦃x_2 : ℕ⦄,
            x_2 < n →
              ∀ ⦃x_3 : ℕ⦄,
                x_3 < n →
                  ∏ p ∈ (f x).primeFactors \ (f x_1).primeFactors, p =
                      ∏ p ∈ (f x_2).primeFactors \ (f x_3).primeFactors, p →
                    (f x).primeFactors \ (f x_1).primeFactors = (f x_2).primeFactors \ (f x_3).primeFactors

Tactic:
rintro a ha b hb c hc d hd

Goal state after:
case calc_3
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ i < n, ∀ j < n, f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun n ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
a : ℕ
ha : a < n
b : ℕ
hb : b < n
c : ℕ
hc : c < n
d : ℕ
hd : d < n
⊢ ∏ p ∈ (f a).primeFactors \ (f b).primeFactors, p = ∏ p ∈ (f c).primeFactors \ (f d).primeFactors, p →
    (f a).primeFactors \ (f b).primeFactors = (f c).primeFactors \ (f d).primeFactors
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero.h₁
q : ℕ
⊢ (↑4).1 = ((2, 1) ^ 1 + (2, -1) ^ 1).1

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero.h₂
q : ℕ
⊢ (↑4).2 = ((2, 1) ^ 1 + (2, -1) ^ 1).2

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h₁
q : ℕ
⊢ 1 + 3 = 2 * 2

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h₂
q : ℕ
⊢ 1 + 1 = 2

Tactic:
norm_num

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
⊢ 1 ^ 2 - 3 = -2

Tactic:
norm_num

Goal state after:
Module: Mathlib.Topology.Algebra.IsUniformGroup.DiscreteSubgroup

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

Tactic:
exact H.isOpen_of_isClosed_of_finiteIndex Subgroup.isClosed_of_discrete

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)
⊢ False

Tactic:
have ω_pow :=
      congr_arg (Units.coeHom (X (q (p' + 2))) : Units (X (q (p' + 2))) → X (q (p' + 2))) <|
        orderOf_dvd_iff_pow_eq_one.1 o

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
⊢ False
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.ω ^ (2 ^ p' * 2 ^ 2 / 4) + X.ωb ^ (2 ^ p' * 2 ^ 2 / 4) = 0
⊢ 2 ^ 2 = 4

Tactic:
norm_num

Goal state after:
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.ω ^ (2 ^ p' * 4 / 4) + X.ωb ^ (2 ^ p' * 4 / 4) = 0
⊢ 4 ≠ 0

Tactic:
norm_num

Goal state after:
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✝¹ : LinearOrder R
inst✝ : IsOrderedRing R
h : ∀ {g : GL n R}, g ∈ Γ → |↑(GeneralLinearGroup.det g)| = 1
⊢ ∀ {g : GL n R}, g ∈ Γ → GeneralLinearGroup.det g = 1 ∨ GeneralLinearGroup.det g = -1

Tactic:
simpa [-GeneralLinearGroup.val_det_apply, abs_eq zero_le_one] using @h

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

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
⊢ Γ.HasDetPlusMinusOne

Tactic:
rw [hasDetPlusMinusOne_iff_abs_det]
  intro g hg
  obtain ⟨n, hn, _, hgn⟩ := Subgroup.exists_pow_mem_of_relIndex_ne_zero
    Subgroup.IsArithmetic.is_commensurable.2 hg
  suffices |(g.det ^ n).val| = 1 by simpa [← abs_pow, abs_pow_eq_one _ (Nat.ne_zero_of_lt hn)]
  obtain ⟨t, ht⟩ := hgn.1
  have := congr_arg Matrix.GeneralLinearGroup.det ht.symm
  rw [Matrix.SpecialLinearGroup.det_mapGL, map_pow] at this
  simp [this]

Goal state after:
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⁻¹
⊢ A₁ * A₂ = 1

Tactic:
simp only [← Matrix.GeneralLinearGroup.coe_mul,
    mul_inv_cancel, Matrix.GeneralLinearGroup.coe_one, A₁, A₂]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
p : ℙ K (Fin 2 → K)
w : Fin 2 → K
hw : w ≠ 0
t : K
hv : t • ↑⟨w, hw⟩ ≠ 0
ht : t ≠ 0
⊢ (if ↑⟨t • ↑⟨w, hw⟩, hv⟩ 1 = 0 then ∞ else ↑((↑⟨t • ↑⟨w, hw⟩, hv⟩ 1)⁻¹ * ↑⟨t • ↑⟨w, hw⟩, hv⟩ 0)) =
    if ↑⟨w, hw⟩ 1 = 0 then ∞ else ↑((↑⟨w, hw⟩ 1)⁻¹ * ↑⟨w, hw⟩ 0)

Tactic:
by_cases h₀ : w 1 = 0 <;> simp [h₀, ht, mul_assoc]

Goal state after:
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)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
i j : Fin 2
⊢ (Int.castRingHom (ZMod M)).mapMatrix z i j = ↑1 i j

Tactic:
z,

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)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
i j : Fin 2
⊢ (Int.castRingHom (ZMod M)).mapMatrix (1 + M • (A₁.num * k * A₂.num)) i j = ↑1 i j
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)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
i j : Fin 2
⊢ 1 i j + (M • (A₁.num * k * A₂.num)).map (fun x ↦ ↑x) i j = ↑1 i j

Tactic:
map_apply,

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)
hz_coe : z.map Int.cast = A₁ * y.map Int.cast * A₂
hz_det : z.det = 1
i j : Fin 2
⊢ 1 i j + ↑((M • (A₁.num * k * A₂.num)) i j) = ↑1 i j
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mpr.refine_1
a : SL(2, ℤ)
⊢ (1 + 1) ^ 2 - 4 = 0

Tactic:
norm_num

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

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : FunLike F ℍ ℂ
f g : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ (⇑f + ⇑g) ∣[k] γ = ⇑f + ⇑g

Tactic:
rw [SlashAction.add_slash, slash_action_eqn f γ hγ, slash_action_eqn g γ hγ]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
⊢ f = 0

Tactic:
ext z

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
⊢ f z = 0 z
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : f z = -1 * f z
h2 : 2 * f z = 0
⊢ ¬2 = 0

Tactic:
norm_num

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

Goal state before:
pp: ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
i : ι
⊢ i ∈ s → MDiff ⇑(F i).toSlashInvariantForm

Tactic:
hi

Goal state after:
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
i : ι
hi : i ∈ s
⊢ MDiff ⇑(F i).toSlashInvariantForm
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
γ : GL (Fin 2) ℝ
hγ : γ • OnePoint.infty = c✝
i : ι
⊢ i ∈ s → atImInfty.BoundedAtFilter (⇑(F i) ∣[k i] γ)

Tactic:
hi

Goal state after:
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
F : (i : ι) → ModularForm Γ (k i)
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
γ : GL (Fin 2) ℝ
hγ : γ • OnePoint.infty = c✝
i : ι
hi : i ∈ s
⊢ atImInfty.BoundedAtFilter (⇑(F i) ∣[k i] γ)
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
⊢ ↑(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:
have : ((↑) : ℤ → ℝ) ∘ p ≠ 0 := fun h => hp.ne_zero (by ext i; simpa using congr_fun h 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
this : Int.cast ∘ p ≠ 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)))
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case r_le
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
⊢ 1 ≤ (FormalMultilinearSeries.ofScalars ℂ c).radius

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun r hr ↦ ?_
    rcases eq_or_ne r 0 with rfl | hr'
    · simp
    · lift r to NNReal using hr.ne_top
      let : FiniteDimensional ℝ ℂ := basisOneI.finiteDimensional_of_finite
      apply FormalMultilinearSeries.le_radius_of_summable
      simpa [smul_eq_mul, norm_mul, mul_comm, mul_left_comm, mul_assoc] using
        (hasSum_cuspFunction_of_hasSum_punctured hh hf (q := r) (by simpa using hr)
          (mod_cast hr')).summable.norm

Goal state after:
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:
← ENNReal.coe_one,

Goal state after:
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))
Module: Mathlib.NumberTheory.ModularForms.LevelOne.Basic

Goal state before:
pp: case refine_3.inr
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
q : ℂ
hq : q ∈ Metric.ball 0 1
hq' : q ≠ 0
ξ : ℍ
hξ : 1 / 2 ≤ ξ.im
hξ₂ : ‖f { coe := invQParam 1 q, coe_im_pos := ⋯ }‖ ≤ ‖f ξ‖
⊢ ∃ w, ‖w‖ ≤ rexp (-π) ∧ ‖UpperHalfPlane.cuspFunction 1 (⇑f) q‖ ≤ ‖UpperHalfPlane.cuspFunction 1 (⇑f) w‖

Tactic:
exact ⟨_, norm_qParam_le_of_one_half_le_im hξ,
        by simpa [← SlashInvariantFormClass.eq_cuspFunction f _ one_mem_strictPeriods_SL
            one_ne_zero, qParam_right_inv one_ne_zero hq'] using hξ₂⟩

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

Goal state before:
pp: F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
⊢ ⇑f = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f) 0)

Tactic:
ext z

Goal state after:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
inst✝ : ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hk : k ≤ 0
f : F
z : ℍ
⊢ f z = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f) 0) z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case left
⊢ 1 ≤ normSq ↑I

Tactic:
norm_num

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
⊢ |I.re| ≤ 1 / 2

Tactic:
norm_num

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

Goal state before:
pp: case e_f
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
u : ℝ
τ : ℍ := { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h ↑τ
⊢ (2 * ↑π * Complex.I)⁻¹ * ↑(2 * π / h) * (𝕢 h ↑τ * Complex.I) • (cuspFunction h f (𝕢 h ↑τ) / 𝕢 h ↑τ ^ (n + 1)) =
    1 / ↑h * (1 / 𝕢 h ↑τ ^ n * f τ)

Tactic:
eq_cuspFunction _ hh.ne' hfper,

Goal state after:
case e_f
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
u : ℝ
τ : ℍ := { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ }
this : circleMap 0 R (u * (2 * π / h)) = 𝕢 h ↑τ
⊢ (2 * ↑π * Complex.I)⁻¹ * ↑(2 * π / h) * (𝕢 h ↑τ * Complex.I) • (f τ / 𝕢 h ↑τ ^ (n + 1)) =
    1 / ↑h * (1 / 𝕢 h ↑τ ^ n * f τ)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ (eisensteinSeries a k ∣[k] γ) z = eisensteinSeries (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)) k z

Tactic:
simp_rw [SL_slash_apply, zpow_neg,
    mul_inv_eq_iff_eq_mul₀ (zpow_ne_zero _ <| denom_ne_zero _ z),
    eisensteinSeries, eisSummand_SL2_apply, tsum_mul_left, mul_comm (_ ^ k)]

Goal state after:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ (∑' (x : ↑(gammaSet N 1 a)), eisSummand k (↑x ᵥ* ↑γ) z) *
      denom (SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ k =
    (∑' (x : ↑(gammaSet N 1 (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)))), eisSummand k (↑x) z) *
      denom (SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ k
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f g : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ cuspFunction h (f * g) = cuspFunction h f * cuspFunction h g

Tactic:
ext z

Goal state after:
h : ℝ
f g : ℍ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
z : ℂ
⊢ cuspFunction h (f * g) z = (cuspFunction h f * cuspFunction h g) z
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: case mp
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
H : qExpansion h f = 0
⊢ f = 0

Tactic:
ext z

Goal state after:
case mp
h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
H : qExpansion h f = 0
z : ℍ
⊢ f z = 0 z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic

Goal state before:
pp: ⊢ 3 ≤ 4

Tactic:
norm_num

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

Goal state before:
pp: ⊢ 3 ≤ 6

Tactic:
norm_num

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h : 0 < ‖↑τ.im ^ ↑k‖
⊢ ‖f τ‖ ^ 2 ≤ √C ^ 2 * max 1 (1 / τ.im ^ ↑k) ^ 2

Tactic:
sq_sqrt hC'

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h : 0 < ‖↑τ.im ^ ↑k‖
⊢ ‖f τ‖ ^ 2 ≤ C * max 1 (1 / τ.im ^ ↑k) ^ 2
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| ≤ ⌊1 + 1 / 2⌋
⊢ ↑1 ≤ 1 + 1 / 2 ∧ 1 + 1 / 2 < ↑1 + 1

Tactic:
norm_num

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

Goal state before:
pp: ⊢ D2 1 = 0

Tactic:
ext z

Goal state after:
z : ℍ
⊢ D2 1 z = 0 z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: A B : SL(2, ℤ)
⊢ D2 (A * B) = D2 A ∣[2] B + D2 B

Tactic:
ext z

Goal state after:
A B : SL(2, ℤ)
z : ℍ
⊢ D2 (A * B) z = (D2 A ∣[2] B + D2 B) z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

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

Tactic:
ext z

Goal state after:
z : ℍ
⊢ D2 ModularGroup.T z = 0 z
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
hSre : (S • z).re = -z.re
hzre : |z.re| = 1 / 2
h : ↑g 0 0 = -1
this : |↑(-1) + -z.re| ≤ 1 / 2
⊢ 0 ≤ 1 / 2

Tactic:
norm_num

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

Goal state before:
pp: r : ℂ
⊢ (logDeriv fun z ↦ 1 - r * cexp z) = fun z ↦ -r * cexp z / (1 - r * cexp z)

Tactic:
ext z

Goal state after:
r z : ℂ
⊢ logDeriv (fun z ↦ 1 - r * cexp z) z = -r * cexp z / (1 - r * cexp z)
Module: Mathlib.NumberTheory.Modular

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

Tactic:
norm_num

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
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g = ↑(T ^ ↑g 0 0 * S * T⁻¹)

Tactic:
rw [coe_mul, coe_mul, coe_T_zpow, coe_S, ← zpow_neg_one, coe_T_zpow, mul_fin_two, mul_fin_two]

Goal state after:
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
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g =
    !![(1 * 0 + ↑g 0 0 * 1) * 1 + (1 * -1 + ↑g 0 0 * 0) * 0, (1 * 0 + ↑g 0 0 * 1) * -1 + (1 * -1 + ↑g 0 0 * 0) * 1;
      (0 * 0 + 1 * 1) * 1 + (0 * -1 + 1 * 0) * 0, (0 * 0 + 1 * 1) * -1 + (0 * -1 + 1 * 0) * 1]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
x : ℕ
i : ℤ
hi : i ∈ Finset.Ico (-↑x) ↑x
⊢ 2 ≤ 2

Tactic:
norm_num

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

Goal state before:
pp: ⊢ G2 ∣[2] T = G2

Tactic:
ext z

Goal state after:
z : ℍ
⊢ (G2 ∣[2] T) z = G2 z
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

Tactic:
ext z

Goal state after:
case mem.inl
γ g : SL(2, ℤ)
h1 : g = S
z : ℍ
⊢ (G2 ∣[2] g) z = (G2 - D2 g) z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: γ : SL(2, ℤ)
⊢ E2 ∣[2] γ = E2 - (1 / (2 * riemannZeta 2)) • D2 γ

Tactic:
ext z

Goal state after:
γ : SL(2, ℤ)
z : ℍ
⊢ (E2 ∣[2] γ) z = (E2 - (1 / (2 * riemannZeta 2)) • D2 γ) z
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ D (F + G) = D F + D G

Tactic:
ext z

Goal state after:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ D (F + G) z = (D F + D G) z
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
⊢ D (F - G) = D F - D G

Tactic:
ext z

Goal state after:
F G : ℍ → ℂ
hF : MDiff F
hG : MDiff G
z : ℍ
⊢ D (F - G) z = (D F - D G) z
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: c : ℂ
⊢ (D fun x ↦ c) = 0

Tactic:
ext z

Goal state after:
c : ℂ
z : ℍ
⊢ D (fun x ↦ c) z = 0 z