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

Goal state before:
pp: case ind.isFalse.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
ha2 : a % 2 = 0
⊢ fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯ = if flip = true then -J(↑a | b) else J(↑a | b)

pp: case ind.isFalse.isFalse
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
ha2 : ¬a % 2 = 0
⊢ (if ha1 : a = 1 then if flip = true then -1 else 1
    else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
· rw [IH (a / 2) (a.div_lt_self ha0 (by decide)) hb2 hb1]
    simp only [Int.natCast_ediv, Nat.cast_ofNat, ← even_odd (a := a) (mod_cast ha2) hb2]
    by_cases h : b % 8 = 3 ∨ b % 8 = 5 <;> simp [h]; cases flip <;> simp

Goal state after:
case ind.isFalse.isFalse
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
ha2 : ¬a % 2 = 0
⊢ (if ha1 : a = 1 then if flip = true then -1 else 1
    else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: 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 : K
⊢ (valuation K) x ≤ (valuation K) γ ↔
    Valued.v.restrict r / Valued.v.restrict γ * Valued.v.restrict x ≤ (valuation K).restrict r

Tactic:
rw [div_mul_eq_mul_div, div_le_iff₀ (by simp [hγ])]

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 : K
⊢ (valuation K) x ≤ (valuation K) γ ↔
    Valued.v.restrict r * Valued.v.restrict x ≤ (valuation K).restrict r * Valued.v.restrict γ
Module: Mathlib.NumberTheory.MaricaSchoenheim

Goal state before:
pp: n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
⊢ ∃ i < n, ∃ j < n, (f i).gcd (f j) * n ≤ f i

Tactic:
by_contra!

Goal state after:
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
⊢ False
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case refine_2
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
p : ↑↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)
i : Fin (n + 1)
prop : (fun x ↦ ⌈B₁ x⌉) ≤ ↑p ∧ ↑p ≤ fun x ↦ ⌊B₂ x⌋
⊢ B₁ i ≤ ↑(↑p ⟨↑i, ⋯⟩) ∧ ↑(↑p ⟨↑i, ⋯⟩) ≤ B₂ i

Tactic:
exact ⟨ceil_le.mp (prop.1 i), le_floor.mp (prop.2 i)⟩

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case refine_4
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ Function.RightInverse (fun p ↦ ⟨(ofFn (n + 1)) ↑p, ⋯⟩) fun p ↦ ⟨(toFn (n + 1)) ↑p, ⋯⟩

Tactic:
· grind [toFn_comp_ofFn_eq_id]

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
⊢ Tendsto (fun s ↦ (↑s - 1) * LSeries f ↑s) (𝓝[>] 1) (𝓝 l)

Tactic:
have h₁ {C ε : ℝ} : Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε) := by
    rw [show 𝓝 ε = 𝓝 ((1 - 1) * 1 * C + 1 * ε) by congr; ring]
    exact tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))
  have h₂ : IsBoundedUnder
      (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s : ℝ ↦ ‖(s - 1) * LSeries f s - s * l‖ := by
    obtain ⟨C, _, hC₂⟩ :=
      LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS zero_lt_one
    exact h₁.isBoundedUnder_le.mono_le hC₂
  suffices Tendsto (fun s : ℝ ↦ (s - 1) * LSeries f s - s * l) (𝓝[>] 1) (𝓝 0) by
    rw [show 𝓝 l = 𝓝 (0 + 1 * l) by congr; ring]
    have h₃ : Tendsto (fun s : ℝ ↦ s * l) (𝓝[>] 1) (𝓝 (1 * l)) :=
      tendsto_nhdsWithin_of_tendsto_nhds (ContinuousAt.tendsto (by fun_prop))
    exact (this.add h₃).congr fun _ ↦ by ring
  refine tendsto_zero_iff_norm_tendsto_zero.mpr <| tendsto_of_le_liminf_of_limsup_le ?_ ?_ h₂ ?_
  · exact le_liminf_of_le h₂.isCoboundedUnder_ge (univ_mem' (fun _ ↦ norm_nonneg _))
  · refine le_of_forall_pos_le_add fun ε hε ↦ ?_
    rw [zero_add]
    obtain ⟨C, hC₁, hC₂⟩ := LSeries_tendsto_sub_mul_nhds_one_of_tendsto_sum_div_aux₃ hlim hfS hε
    refine le_of_le_of_eq (limsup_le_limsup hC₂ ?_ h₁.isBoundedUnder_le) h₁.limsup_eq
    exact isCoboundedUnder_le_of_eventually_le _ (univ_mem' fun _ ↦ norm_nonneg _)
  · exact isBoundedUnder_of_eventually_ge (univ_mem' fun _ ↦ norm_nonneg _)

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case e'_4
q : ℕ
inst✝ : NeZero q
w : 1 < q
this : Fact (1 < q)
⊢ q ^ 2 = Fintype.card (X q)

Tactic:
card_eq

Goal state after:
case e'_4
q : ℕ
inst✝ : NeZero q
w : 1 < q
this : Fact (1 < q)
⊢ q ^ 2 = q ^ 2
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h
p' : ℕ
k : ℤ
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1

Tactic:
have : 1 ≤ 2 ^ (p' + 2) := Nat.one_le_pow _ _ (by decide)

Goal state after:
case h
p' : ℕ
k : ℤ
t : 2 ^ p' + 2 ^ p' = 2 ^ (p' + 1)
h : ω ^ 2 ^ (p' + 1) = ↑k * ↑(2 ^ (p' + 2) - 1) * ω ^ 2 ^ p' - 1
this : 1 ≤ 2 ^ (p' + 2)
⊢ ω ^ 2 ^ (p' + 1) = ↑k * ↑(mersenne (p' + 2)) * ω ^ 2 ^ p' - 1
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: case right
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ (mapGL ℝ).range.relIndex (Γ ⊓ Γ') ≠ 0

Tactic:
apply relIndex_ne_zero_trans (K := Γ) IsArithmetic.is_commensurable.2

Goal state after:
case right
n : Type u_1
inst✝³ : Fintype n
inst✝² : DecidableEq n
Γ Γ' : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
inst✝ : Γ'.IsArithmetic
⊢ Γ.relIndex (Γ ⊓ Γ') ≠ 0
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ DiscreteTopology ↥(map (Int.castRingHom ℝ)).range

Tactic:
by
  refine (Topology.IsEmbedding.toHomeomorph ?_).discreteTopology
  exact Real.isClosedEmbedding_intCast.specialLinearGroup_map.1

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) ℝ)
inst✝ : 𝒢.IsArithmetic
⊢ DiscreteTopology ↥𝒢

Tactic:
by
  rw [is_commensurable.discreteTopology_iff]
  infer_instance

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

Goal state before:
pp: c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
x : GL (Fin 2) ℝ
⊢ x ∈ 𝒢 ↔ ConjAct.toConjAct g⁻¹ • x ∈ 𝒢

Tactic:
ConjAct.toConjAct_smul,

Goal state after:
c : OnePoint ℝ
𝒢 : Subgroup (GL (Fin 2) ℝ)
hc : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
x : GL (Fin 2) ℝ
⊢ x ∈ 𝒢 ↔ g⁻¹ * x * g⁻¹⁻¹ ∈ 𝒢
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
inst✝² : Γ.HasDetOne
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ (c • ⇑f) ∣[k] γ = c • ⇑f

Tactic:
← smul_one_smul ℂ

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
inst✝² : Γ.HasDetOne
α : Type u_2
inst✝¹ : SMul α ℂ
inst✝ : IsScalarTower α ℂ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ ((c • 1) • ⇑f) ∣[k] γ = (c • 1) • ⇑f
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : SMul α ℝ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ (σ γ) ↑(c • 1) • ⇑f ∣[k] γ = ↑(c • 1) • ⇑f

Tactic:
σ_ofReal,

Goal state after:
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝³ : FunLike F ℍ ℂ
α : Type u_2
inst✝² : SMul α ℂ
inst✝¹ : SMul α ℝ
inst✝ : IsScalarTower α ℝ ℂ
c : α
f : SlashInvariantForm Γ k
γ : GL (Fin 2) ℝ
hγ : γ ∈ Γ
⊢ ↑(c • 1) • ⇑f ∣[k] γ = ↑(c • 1) • ⇑f
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: F : Type u_1
Γ✝ : Subgroup (GL (Fin 2) ℝ)
k✝ : ℤ
inst✝¹ : FunLike F ℍ ℂ
ι : Type
s : Finset ι
k : ι → ℤ
m : ℤ
hm : m = ∑ i ∈ s, k i
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝ : Γ.HasDetPlusMinusOne
f : (i : ι) → SlashInvariantForm Γ (k i)
A : GL (Fin 2) ℝ
hA : A ∈ Γ
⊢ (∏ i ∈ s, ⇑(f i)) ∣[m] A = ∏ i ∈ s, ⇑(f i)

Tactic:
by
    simp [hm, prod_slash_sum_weights, -Matrix.GeneralLinearGroup.val_det_apply,
       Subgroup.HasDetPlusMinusOne.abs_det hA, SlashInvariantForm.slash_action_eqn (f _) A hA]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R := of ![![a, -b₀], cd]
⊢ A 0 0 * A 1 1 - A 0 1 * A 1 0 = b₀ * cd 0 + a * cd 1

Tactic:
simp [A, (by ring : a * cd 1 + b₀ * cd 0 = b₀ * cd 0 + a * cd 1)]

Goal state after:
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 ↑τ
⊢ petersson k (f ∣[k] g) (f' ∣[k] g) τ =
    ↑D ^ (k - 2 + k) * (starRingEnd ℂ) ((σ g) (f (g • τ))) * (σ g) (f' (g • τ)) *
      (↑τ.im ^ k * ↑(Complex.normSq j) ^ (-k))

Tactic:
simp [Complex.normSq_eq_conj_mul_self, (by abel : k - 2 + k = (k - 1) + (k - 1)), petersson,
      zpow_add₀ hD, mul_zpow, ModularForm.slash_def, -Matrix.GeneralLinearGroup.val_det_apply]
    ring

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

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

Tactic:
SlashInvariantForm.coe_translate,

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : ModularFormClass F Γ k
g : GL (Fin 2) ℝ
c : OnePoint ℝ
hc : IsCusp c (toConjAct g⁻¹ • Γ)
γ : GL (Fin 2) ℝ
hγ : γ • ∞ = c
⊢ IsBoundedAtImInfty ((⇑f ∣[k] g) ∣[k] γ)
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
⊢ ↑(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 nonZ1 : (p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2 ≠ 0 := mod_cast hp.sq_add_sq_ne_zero
  have : ((↑) : ℤ → ℝ) ∘ p ≠ 0 := fun h => hp.ne_zero (by ext i; simpa using congr_fun h i)
  have nonZ2 : (p 0 : ℂ) * z + p 1 ≠ 0 := by simpa using linear_ne_zero z this
  subst hg
  rw [coe_specialLinearGroup_apply]
  replace nonZ2 : z * (g 1 0 : ℂ) + g 1 1 ≠ 0 := by convert! nonZ2 using 1; ring
  have H := congr(Int.cast (R := ℂ) $(det_fin_two g))
  simp at H
  simp [field]
  linear_combination -((z : ℂ) * (g 1 1 : ℂ) - g 1 0) * H

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ∃ g, ↑g 1 = cd ∧ ∀ (g' : SL(2, ℤ)), ↑g 1 = ↑g' 1 → |(g • z).re| ≤ |(g' • z).re|

Tactic:
have : Nonempty { g : SL(2, ℤ) // g 1 = cd } :=
    let ⟨x, hx⟩ := bottom_row_surj hcd
    ⟨⟨x, hx.2⟩⟩
  obtain ⟨g, hg⟩ := Filter.Tendsto.exists_forall_le (tendsto_abs_re_smul z hcd)
  refine ⟨g, g.2, ?_⟩
  intro g1 hg1
  have : g1 ∈ (fun g : SL(2, ℤ) => g 1) ⁻¹' {cd} := by
    rw [Set.mem_preimage, Set.mem_singleton_iff]
    exact Eq.trans hg1.symm (Set.mem_singleton_iff.mp (Set.mem_preimage.mp g.2))
  exact hg ⟨g1, this⟩

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

Goal state before:
pp: E : Type u_1
inst✝ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : f =O[atImInfty] fun z ↦ z.im ^ t
hf_inv : ∀ (g : SL(2, ℤ)) (τ : ℍ), f (g • τ) = f τ
F : ℝ
τ : ℍ
g : SL(2, ℤ)
hF𝒟 : ‖f τ‖ ≤ F * (g • τ).im ^ t
hg✝ : g • τ ∈ 𝒟
hg : ¬↑g 1 0 = 0
⊢ Complex.normSq (↑(↑g 1 0) * ↑τ + ↑(↑g 1 1)) = (↑(↑g 1 0) * τ.re + ↑(↑g 1 1)) ^ 2 + ↑(↑g 1 0) ^ 2 * τ.im ^ 2

Tactic:
simp [Complex.normSq_apply]; ring

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

Goal state before:
pp: h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n✝ i : ℕ
hi : i ∈ Finset.range (n✝ + 1)
⊢ (↑n✝.factorial)⁻¹ *
      (↑(n✝.choose i) * iteratedDeriv i (cuspFunction h f) 0 * iteratedDeriv (n✝ - i) (cuspFunction h g) 0) =
    (↑i.factorial)⁻¹ * iteratedDeriv i (cuspFunction h f) 0 *
      ((↑(n✝ - i).factorial)⁻¹ * iteratedDeriv (n✝ - i) (cuspFunction h g) 0)

Tactic:
rw [Nat.cast_choose _ (by grind)]

Goal state after:
h : ℝ
f g : ℍ → ℂ
hf : AnalyticAt ℂ (cuspFunction h f) 0
hg : AnalyticAt ℂ (cuspFunction h g) 0
n✝ i : ℕ
hi : i ∈ Finset.range (n✝ + 1)
⊢ (↑n✝.factorial)⁻¹ *
      (↑n✝.factorial / (↑i.factorial * ↑(n✝ - i).factorial) * iteratedDeriv i (cuspFunction h f) 0 *
        iteratedDeriv (n✝ - i) (cuspFunction h g) 0) =
    (↑i.factorial)⁻¹ * iteratedDeriv i (cuspFunction h f) 0 *
      ((↑(n✝ - i).factorial)⁻¹ * iteratedDeriv (n✝ - i) (cuspFunction h g) 0)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence

Goal state before:
pp: k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformlyOn (fun s ↦ (fun z ↦ ∑ x ∈ s, eisSummand k (↑x) z) ∘ ↑ofComplex)
    (⇑(eisensteinSeriesSIF a k) ∘ ↑ofComplex) Filter.atTop {z | 0 < z.im}

Tactic:
by
  rw [← upperHalfPlaneSet, ← range_coe, ← image_univ]
  apply TendstoLocallyUniformlyOn.comp (s := ⊤) _ _ _ (OpenPartialHomeomorph.continuousOn_symm _)
  · simp only [Set.top_eq_univ, tendstoLocallyUniformlyOn_univ]
    apply eisensteinSeries_tendstoLocallyUniformly hk
  · simp only [IsOpenEmbedding.toOpenPartialHomeomorph_target, Set.top_eq_univ, mapsTo_range_iff,
    Set.mem_univ, forall_const]

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

Goal state before:
pp: k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
a✝ : ℝ
⊢ a✝ ≤ 1 → ∀ (a : ℍ), a.im = a✝ → ‖f a‖ ≤ C * ‖a.im ^ (-k)‖

Tactic:
hτ

Goal state after:
k : ℤ
hk : 0 ≤ k
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : ModularFormClass F Γ k
f : F
C : ℝ
hC : ∀ (τ : ℍ), ‖f τ‖ ≤ C * max 1 (1 / τ.im ^ k)
a✝ : ℝ
hτ : a✝ ≤ 1
⊢ ∀ (a : ℍ), a.im = a✝ → ‖f a‖ ≤ C * ‖a.im ^ (-k)‖
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
i j : Fin 2
⊢ ↑g i j = !![↑g 0 0, -1 + ↑g 0 0; 1, 1] i j

Tactic:
fin_cases i <;> fin_cases j <;> [tauto; simp; tauto; tauto]

Goal state after:
case «0».«1»
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 0 1 = -1 + ↑g 0 0
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:
by
  ext z
  simp [logDeriv]

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

Goal state before:
pp: x : Fin 2 → ℤ
hx : x ≠ ![0, 0]
hx' : x ≠ ![0, -1]
⊢ δ x = 0 x

Tactic:
simp_all [δ]

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

Goal state before:
pp: hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) 1 < 1 / 2
τ : ℍ
⊢ dist (∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24) 1 < 1 / 2 → ‖rexp (-2 * π * τ.im)‖ ≤ 2 * ‖Δ τ‖

Tactic:
hτ

Goal state after:
hprod : ∀ᶠ (x : ℍ) in atImInfty, dist (∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) 1 < 1 / 2
τ : ℍ
hτ : dist (∏' (n : ℕ), (1 - eta_q n ↑τ) ^ 24) 1 < 1 / 2
⊢ ‖rexp (-2 * π * τ.im)‖ ≤ 2 * ‖Δ τ‖
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
hcusp : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
⊢ qExpansion 1 ⇑f = qExpansion 1 Δ * qExpansion 1 ⇑(CuspForm.discriminantEquiv (f.toCuspForm hcusp))

Tactic:
rw [show (f : ℍ → ℂ) = discriminant * (toCuspForm f hcusp).discriminantEquiv from
      (discriminant_mul_discriminantEquiv (toCuspForm f hcusp)).symm, ← CuspForm.coe_discriminant]
  exact ModularForm.qExpansion_mul_coe one_pos one_mem_strictPeriods_SL _ _

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
this :
  Module.rank ℂ
      (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k ⧸
        cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    1
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    1 + Module.rank ℂ (CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k)

Tactic:
rw [(CuspForm.equivCuspFormSubmodule 𝒮ℒ k).rank_eq,
      ← Submodule.rank_quotient_add_rank (cuspFormSubmodule 𝒮ℒ k), this]

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

Goal state before:
pp: case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ (PowerSeries.coeff 0) (qExpansion 1 ⇑f) - (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0

pp: case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

pp: case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

pp: case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

pp: case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

Tactic:
sub_self

Goal state after:
case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 = 0

case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods

case h.hh
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 0 < 1

case h.hΓ
k : ℕ
hk : 3 ≤ k
hk2 : Even k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k
⊢ 1 ∈ (Matrix.SpecialLinearGroup.mapGL ℝ).range.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

Tactic:
rcases lt_or_ge k 0 with hk_neg | hk_nonneg

Goal state after:
case inl
k : ℤ
hk_neg : k < 0
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0

case inr
k : ℤ
hk_nonneg : 0 ≤ k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) < Cardinal.aleph0
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta₂ 0 (-↑τ)⁻¹ = (-I * ↑τ) ^ (1 / 2) * (1 / (-I * ↑τ) ^ (1 / 2) * cexp 0 * jacobiTheta₂ 0 (-1 / ↑τ))

Tactic:
Complex.exp_zero,

Goal state after:
τ : ℍ
h0 : ↑τ ≠ 0
h1 : (-I * ↑τ) ^ (1 / 2) ≠ 0
⊢ jacobiTheta₂ 0 (-↑τ)⁻¹ = (-I * ↑τ) ^ (1 / 2) * (1 / (-I * ↑τ) ^ (1 / 2) * 1 * jacobiTheta₂ 0 (-1 / ↑τ))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ+
h2 :
  ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ n -
      1 / ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ } =
    ∑' (n : ℕ+),
      (1 / (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ } - ↑↑n) + 1 / (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ } + ↑↑n))
⊢ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑N / ↑z - ↑↑m) + 1 / (-↑↑N / ↑z + ↑↑m)) -
      (-2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑N / ↑z)) ^ ↑m) =
    2 / ↑↑N

Tactic:
one_div,

Goal state after:
z : ℍ
N : ℕ+
h2 :
  ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ }) ^ n -
      (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ })⁻¹ =
    ∑' (n : ℕ+),
      (1 / (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ } - ↑↑n) + 1 / (↑{ coe := -↑↑N / ↑z, coe_im_pos := ⋯ } + ↑↑n))
⊢ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑N / ↑z - ↑↑m) + 1 / (-↑↑N / ↑z + ↑↑m)) -
      (-2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑N / ↑z)) ^ ↑m) =
    2 / ↑↑N
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
⊢ (riemannZeta ↑k)⁻¹ * (-2 * ↑π * I) ^ k / ↑(k - 1)! = -(2 * ↑k / ↑(bernoulli k))

Tactic:
have h2 : k = 2 * (k / 2 - 1 + 1) := by grind

Goal state after:
k : ℕ
hk2 : Even k
hkn0 : k ≠ 0
h2 : k = 2 * (k / 2 - 1 + 1)
⊢ (riemannZeta ↑k)⁻¹ * (-2 * ↑π * I) ^ k / ↑(k - 1)! = -(2 * ↑k / ↑(bernoulli k))
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 τ + cexp 0 - cexp 0 * 2)
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)

Tactic:
Complex.exp_zero,

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 - 1 * 2)
⊢ HasSum (fun n ↦ cexp (↑π * I * (↑n + 1) ^ 2 * τ)) ((jacobiTheta τ - 1) / 2)
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: y : ℝ
hy : 1 ≤ y
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) ≤ 2 / (1 - rexp (-(π * 1))) * ‖rexp (-π * τ.im)‖

Tactic:
Real.norm_eq_abs,

Goal state after:
y : ℝ
hy : 1 ≤ y
τ : ℂ
hτ : τ.im = y
⊢ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) ≤ 2 / (1 - rexp (-(π * 1))) * |rexp (-π * τ.im)|