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

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

Tactic:
rw [norm_mul, ← hn'.unit_spec, DirichletCharacter.unit_norm_eq_one χ hn'.unit,
        ← ofReal_natCast, norm_cpow_eq_rpow_re_of_pos (mod_cast by lia)]

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
n : ℕ
hn✝ : 2 ≤ n
x : ℝ
hx : 1 < x
y : ℝ
hn' : IsUnit ↑n
hn : ↑n ^ (-x) < 1
⊢ 1 * ↑n ^ (-(I * ↑y)).re = 1
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
| 2 ^ (2 * k - 1) * 2

Tactic:
congr
      · skip
      · rw [← pow_one (2 : ℝ)]

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp2✝ : Fact (p % 2 = 1)
a : ℕ
hap : ↑a ≠ 0
hp2 : ↑p = ↑1
⊢ ↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) + ↑(∑ x ∈ Ico 1 (p / 2).succ, (↑a * ↑x).valMinAbs.natAbs) =
    ↑(#({x ∈ Ico 1 (p / 2).succ | p / 2 < (↑a * ↑x).val})) + ↑(∑ x ∈ Ico 1 (p / 2).succ, x)

Tactic:
by
            rw [Finset.sum_eq_multiset_sum, Ico_map_valMinAbs_natAbs_eq_Ico_map_id p a hap, ←
              Finset.sum_eq_multiset_sum]

Goal state after:
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
γ : ValueGroupWithZero K
⊢ IsCompact {x | (valuation K) x ≤ γ}

Tactic:
obtain ⟨γ, rfl⟩ := ValuativeRel.valuation_surjective γ
  by_cases hγ : γ = 0
  · simp [hγ]
  let := IsTopologicalAddGroup.rightUniformSpace K
  let := isUniformAddGroup_of_addCommGroup (G := K)
  obtain ⟨s, hs, -, hs'⟩ := LocallyCompactSpace.local_compact_nhds (0 : K) .univ Filter.univ_mem
  obtain ⟨r, hr, hr1, H⟩ :
      ∃ r', r' ≠ 0 ∧ valuation K r' < 1 ∧ { x | valuation K x ≤ valuation K r' } ⊆ s := by
    obtain ⟨r, hr, hrs⟩ := (IsValuativeTopology.hasBasis_nhds_zero' K).mem_iff.mp hs
    obtain ⟨r', hr', hr⟩ := Valuation.IsNontrivial.exists_lt_one (v := valuation K)
    simp only [ne_eq] at hr'
    obtain hr1 | hr1 := lt_or_ge r 1
    · obtain ⟨r, rfl⟩ := ValuativeRel.valuation_surjective r
      simp only [ne_eq, map_eq_zero] at hr
      refine ⟨r ^ 2, by simpa using hr, by simpa [pow_two], fun x hx ↦ hrs ?_⟩
      simp only [map_pow, Set.mem_ofPred_eq] at hx ⊢
      exact hx.trans_lt (by simpa [pow_two, hr])
    · refine ⟨r', hr', hr, .trans ?_ hrs⟩
      intro x hx
      dsimp at hx ⊢
      exact hx.trans_lt (hr.trans_le hr1)
  simp_rw [← (valuation K).restrict_le_iff] at H ⊢
  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
  refine .trans ?_ (Equiv.image_eq_preimage_symm _ _).symm
  ext x
  simp only [Set.mem_ofPred_eq, Homeomorph.coe_symm_toEquiv, Homeomorph.mulLeft₀_symm_apply,
    inv_div, Set.preimage_ofPred_eq, map_mul, map_div₀, Valuation.restrict_le_iff]
  rw [div_mul_eq_mul_div, div_le_iff₀ (by simp [hγ])]
  simp only [IsValuativeTopology.v_eq_valuation, ← map_mul, Valuation.restrict_le_iff]
  simp [hr]

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

Goal state before:
pp: K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ v.IsNontrivial ↔ IsLocalRing.maximalIdeal ↥v.integer ≠ ⊥

Tactic:
simp_rw [ne_eq, eq_bot_iff, v.isNontrivial_iff_exists_lt_one, SetLike.le_def, Ideal.mem_bot,
    not_forall, exists_prop, IsLocalRing.notMem_maximalIdeal.not_right,
    Valuation.Integer.not_isUnit_iff_valuation_lt_one]
  exact ⟨fun ⟨x, hx0, hx1⟩ ↦ ⟨⟨x, hx1.le⟩, by simp [Subtype.ext_iff, *]⟩,
  fun ⟨x, hx1, hx0⟩ ↦ ⟨x, by simp [*]⟩⟩

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
n n✝ : ℕ
hmn✝ : 2 ≤ n✝
a✝ : mersenne n✝ % 4 = 3
⊢ mersenne (n✝ + 1) % 4 = 3

Tactic:
mersenne_succ

Goal state after:
case succ
n n✝ : ℕ
hmn✝ : 2 ≤ n✝
a✝ : mersenne n✝ % 4 = 3
⊢ (2 * mersenne n✝ + 1) % 4 = 3
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
k j : ℕ
hmn✝ : 1 ≤ j
a✝ : mersenne (2 * j + 1) % 3 = 1
⊢ (2 * mersenne (2 * j + 1 + 1) + 1) % 3 = 1

Tactic:
mersenne_succ

Goal state after:
case succ
k j : ℕ
hmn✝ : 1 ≤ j
a✝ : mersenne (2 * j + 1) % 3 = 1
⊢ (2 * (2 * mersenne (2 * j + 1) + 1) + 1) % 3 = 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
n n✝ : ℕ
hmn✝ : 3 ≤ n✝
a✝ : mersenne n✝ % 8 = 7
⊢ mersenne (n✝ + 1) % 8 = 7

Tactic:
mersenne_succ

Goal state after:
case succ
n n✝ : ℕ
hmn✝ : 3 ≤ n✝
a✝ : mersenne n✝ % 8 = 7
⊢ (2 * mersenne n✝ + 1) % 8 = 7
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case refine_1
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
h₁ : ∀ {C ε : ℝ}, Tendsto (fun s ↦ (s - 1) * s * C + s * ε) (𝓝[>] 1) (𝓝 ε)
h₂ : IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) (𝓝[>] 1) fun s ↦ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖
⊢ 0 ≤ liminf (fun x ↦ ‖(↑x - 1) * LSeries f ↑x - ↑x * l‖) (𝓝[>] 1)

Tactic:
exact le_liminf_of_le h₂.isCoboundedUnder_ge (univ_mem' (fun _ ↦ norm_nonneg _))

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz✝ : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ (aeval z) p = 0
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K :=
  { to_charZero := IntermediateField.charZero ℚ⟮z⟯,
    to_finiteDimensional := adjoin.finiteDimensional (IsIntegral.tower_top (isIntegral_of_mahlerMeasure_eq_one h hz✝)) }
y : ↥K := ⟨z, ⋯⟩
φ : ↥K →+* ℂ
ψ : ↥K →+* ℂ
⊢ (algebraMap ℤ ℂ).comp (RingHom.id ℤ) = ψ.comp (algebraMap ℤ ↥K)

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1 + 1)

Tactic:
apply orderOf_dvd_iff_pow_eq_one.2

Goal state after:
case h₂
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ωUnit (p' + 2) ^ 2 ^ (p' + 1 + 1) = 1
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
g : Matrix (Fin 2) (Fin 2) R
v : R × R
⊢ g • v = (g 0 0 * v.1 + g 0 1 * v.2, g 1 0 * v.1 + g 1 1 * v.2)

Tactic:
by
  simp [Equiv.smul_def, smul_eq_mulVec, Matrix.mulVec_eq_sum]

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

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : DecidableEq K
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsPrincipalIdealRing A
c : OnePoint K
⊢ ∃ g, (mapGL K) g • ∞ = c

Tactic:
cases c with
  | infty => exact ⟨1, by simp⟩
  | coe q =>
    obtain ⟨g, hg0, hg1⟩ := (IsFractionRing.num_den_reduced A q).isCoprime.exists_SL2_col 0
    exact ⟨g, by simp [hg0, hg1, smul_infty_eq_ite]⟩

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

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

Tactic:
· apply Subgroup.closure_induction (p := fun γ _ ↦ f ∣[k] γ = f) h (by simp)
    · simp +contextual [SlashAction.slash_mul]
    · intro x hx hf
      rw [← hf, ← SlashAction.slash_mul]
      simp [hf]
    · simpa [← hΓ]

Goal state after:
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) = LinearMap.id c

Tactic:
LinearMap.id_apply

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
⊢ (↑z).im⁻¹ • g (f c) = c
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: case mp
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
⊢ (∃ x_1, (↑(↑x_1 0 0) = 1 ∧ ↑(↑x_1 0 1) = 0 ∧ ↑(↑x_1 1 0) = 0 ∧ ↑(↑x_1 1 1) = 1) ∧ (mapGL ℝ) x_1 = upperRightHom x) →
    x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)

Tactic:
rintro ⟨g, ⟨-, hg, -, -⟩, hx⟩

Goal state after:
case mp
N : ℕ
x : ℝ
this : AddSubgroup.zmultiples ↑N = AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
g : SL(2, ℤ)
hx : (mapGL ℝ) g = upperRightHom x
hg : ↑(↑g 0 1) = 0
⊢ x ∈ AddSubgroup.map (Int.castAddHom ℝ) (AddSubgroup.zmultiples ↑N)
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⁻¹ * (↑(c 0) * ↑(normSq ↑z) + ↑z * ↑(c 1)).im = c 1

Tactic:
← ofReal_mul,

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⁻¹ * (↑(c 0 * normSq ↑z) + ↑z * ↑(c 1)).im = c 1
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✝
⊢ IsBoundedAtImInfty ((SlashInvariantForm.prod m hm fun i ↦ { toFun := ⇑(F i), slash_action_eq' := ⋯ }).toFun ∣[m] γ)

Tactic:
simp only [SlashInvariantForm.toFun_eq_coe, coe_prod, SlashInvariantForm.coe_mk, hm,
      prod_slash_sum_weights, IsBoundedAtImInfty]

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✝
⊢ atImInfty.BoundedAtFilter (|↑(Matrix.GeneralLinearGroup.det γ)| ^ (↑s.card - 1) • ∏ i ∈ s, ⇑(F i) ∣[k i] γ)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ Tendsto (fun g ↦ (lcRow0 cd) ↑((SpecialLinearGroup.map (Int.castRingHom ℝ)) ↑g)) cofinite (cocompact ℝ)

Tactic:
let mB : ℝ → Matrix (Fin 2) (Fin 2) ℝ := fun t => of ![![t, (-(1 : ℤ) : ℝ)], (↑) ∘ cd]
  have hmB : Continuous mB := by
    refine continuous_matrix ?_
    simp only [mB, Fin.forall_fin_two, continuous_const, continuous_id', of_apply, cons_val_zero,
      cons_val_one, and_self_iff]
  refine Filter.Tendsto.of_tendsto_comp ?_ (comap_cocompact_le hmB)
  let f₁ : SL(2, ℤ) → Matrix (Fin 2) (Fin 2) ℝ := fun g =>
    Matrix.map (↑g : Matrix _ _ ℤ) ((↑) : ℤ → ℝ)
  have cocompact_ℝ_to_cofinite_ℤ_matrix :
    Tendsto (fun m : Matrix (Fin 2) (Fin 2) ℤ => Matrix.map m ((↑) : ℤ → ℝ)) cofinite
      (cocompact _) := by
    simpa only [coprodᵢ_cofinite, coprodᵢ_cocompact] using!
      Tendsto.pi_map_coprodᵢ fun _ : Fin 2 =>
        Tendsto.pi_map_coprodᵢ fun _ : Fin 2 => Int.tendsto_coe_cofinite
  have hf₁ : Tendsto f₁ cofinite (cocompact _) :=
    cocompact_ℝ_to_cofinite_ℤ_matrix.comp Subtype.coe_injective.tendsto_cofinite
  have hf₂ : IsClosedEmbedding (lcRow0Extend hcd) :=
    (lcRow0Extend hcd).toContinuousLinearEquiv.toHomeomorph.isClosedEmbedding
  convert! hf₂.tendsto_cocompact.comp (hf₁.comp Subtype.coe_injective.tendsto_cofinite) using 1
  ext ⟨g, rfl⟩ i j : 3
  fin_cases i <;> [fin_cases j; skip]
  -- the following are proved by `simp`, but it is replaced by `simp only` to avoid timeouts.
  · simp only [Fin.isValue, Int.cast_one, map_apply_coe, RingHom.mapMatrix_apply,
      Int.coe_castRingHom, lcRow0_apply, map_apply, Fin.zero_eta, Function.comp_apply,
      of_apply, cons_val', cons_val_zero, empty_val', cons_val_fin_one, lcRow0Extend_apply,
      LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLin,
      val_planeConformalMatrix, neg_neg, mulVecLin_apply, mulVec, dotProduct, Fin.sum_univ_two,
      cons_val_one, mB, f₁]
  · convert! congr_arg (fun n : ℤ => (-n : ℝ)) g.det_coe.symm using 1
    simp only [Fin.zero_eta, Function.comp_apply, lcRow0Extend_apply, cons_val_zero,
      LinearMap.GeneralLinearGroup.coeFn_generalLinearEquiv, GeneralLinearGroup.coe_toLin,
      mulVecLin_apply, mulVec, dotProduct, det_fin_two, f₁]
    simp only [Fin.isValue, Fin.mk_one, val_planeConformalMatrix, neg_neg, of_apply, cons_val',
      empty_val', cons_val_fin_one, cons_val_one, map_apply, Fin.sum_univ_two,
      cons_val_zero, neg_mul, Int.cast_sub, Int.cast_mul, neg_sub]
    ring
  · rfl

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 ∈ ball 0 1
⊢ HasSum (fun n ↦ (FormalMultilinearSeries.ofScalars ℂ c n) fun x ↦ y) (update (cuspFunction h f) 0 (c 0) (0 + y))

Tactic:
mem_ball_zero_iff

Goal state after:
case hasSum
h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
y : ℂ
hy : ‖y‖ < 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: N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
v : Fin 2 → ℤ
hv : v ∈ gammaSet N r a
γ : SL(2, ℤ)
⊢ v ᵥ* ↑γ ∈ gammaSet N r (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ))

Tactic:
refine ⟨?_, vecMulSL_gcd hv.2 γ⟩

Goal state after:
N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
v : Fin 2 → ℤ
hv : v ∈ gammaSet N r a
γ : SL(2, ℤ)
⊢ Int.cast ∘ (v ᵥ* ↑γ) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : 3 * c' ^ 2 ≤ 4
⊢ |↑g 1 0| ≤ 1

Tactic:
replace this : c' ^ 2 ≤ 1 ^ 2 := by lia

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
this : c' ^ 2 ≤ 1 ^ 2
⊢ |↑g 1 0| ≤ 1
Module: Mathlib.NumberTheory.ModularForms.QExpansion

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

Tactic:
constructor
  · intro H
    ext z
    simp [← (hasSum_qExpansion hh hfper hfhol hfbdd z).tsum_eq, H]
  · intro H
    simpa [H] using qExpansion_zero h

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

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

Tactic:
sum_divisorsAntidiagonal ((fun x y ↦ ‖(y : 𝕜)‖ ^ k * _ ^ (x * y)))

Goal state after:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
⊢ ∑ i ∈ (↑b).divisors, ‖↑(↑b / i)‖ ^ k * ‖r‖ ^ (i * (↑b / i)) ≤ ∑ x ∈ (↑b).divisors, ‖↑↑b‖ ^ k * ‖r ^ ↑b‖
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: α : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
f : ℤ → α
a : α
⊢ HasProd f a (symmetricIoc ℤ) ↔ Tendsto (fun N ↦ ∏ n ∈ Ioc (-↑N) ↑N, f n) atTop (𝓝 a)

Tactic:
by
  simp [HasProd, symmetricIoc, ← Nat.map_cast_int_atTop, comp_def]

Goal state after:
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 : ℍ
hz : denom g ↑z ≠ 0
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
h_denom : HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z
hcomp :
  F ∣[k] g ∘ ↑ofComplex =ᶠ[𝓝 ↑z] fun w ↦ ↑(↑g).det ^ (k - 1) * ((F ∘ ↑ofComplex) ↑(g • ↑ofComplex w) * denom g w ^ (-k))
⊢ (2 * ↑π * I)⁻¹ *
      (↑(↑g).det ^ (k - 1) *
        (deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det / denom g ↑z ^ 2) * denom g ↑z ^ (-k) +
          F (g • z) * (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)))) =
    (↑(↑g).det)⁻¹ *
        ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z) * ↑(↑g).det ^ (k - 1 + 2) * denom g ↑z ^ (-k + -2)) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F (g • z) * ↑(↑g).det ^ (k - 1) * denom g ↑z ^ (-k))

Tactic:
zpow_add₀ hdetℂ,

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
h_smul : HasDerivAt (fun w ↦ ↑(g • ↑ofComplex w)) (↑(↑g).det / denom g ↑z ^ 2) ↑z
h_F : HasDerivAt (F ∘ ↑ofComplex) (deriv (F ∘ ↑ofComplex) ↑(g • ↑ofComplex ↑z)) ↑(g • ↑ofComplex ↑z)
h_denom : HasDerivAt (fun w ↦ denom g w ^ (-k)) (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)) ↑z
hcomp :
  F ∣[k] g ∘ ↑ofComplex =ᶠ[𝓝 ↑z] fun w ↦ ↑(↑g).det ^ (k - 1) * ((F ∘ ↑ofComplex) ↑(g • ↑ofComplex w) * denom g w ^ (-k))
⊢ (2 * ↑π * I)⁻¹ *
      (↑(↑g).det ^ (k - 1) *
        (deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det / denom g ↑z ^ 2) * denom g ↑z ^ (-k) +
          F (g • z) * (-↑k * ↑(↑g 1 0) * denom g ↑z ^ (-k - 1)))) =
    (↑(↑g).det)⁻¹ *
        ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑(g • z) * (↑(↑g).det ^ (k - 1) * ↑(↑g).det ^ 2) *
          denom g ↑z ^ (-k + -2)) -
      ↑k * (2 * ↑π * I)⁻¹ * (↑(↑g 1 0) / denom g ↑z) * (F (g • z) * ↑(↑g).det ^ (k - 1) * denom g ↑z ^ (-k))
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: case hf.hg
⊢ DifferentiableOn ℂ η upperHalfPlaneSet

pp: case hf.hf
⊢ DifferentiableOn ℂ (fun z ↦ -1 / z) upperHalfPlaneSet

pp: case hf.st
⊢ Set.MapsTo (fun z ↦ -1 / z) upperHalfPlaneSet upperHalfPlaneSet

Tactic:
· exact fun x hx ↦ (differentiableAt_eta_of_mem_upperHalfPlaneSet hx).differentiableWithinAt

Goal state after:
case hf.hf
⊢ DifferentiableOn ℂ (fun z ↦ -1 / z) upperHalfPlaneSet

case hf.st
⊢ Set.MapsTo (fun z ↦ -1 / z) upperHalfPlaneSet upperHalfPlaneSet
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: k : ℤ
hk : Odd k
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
⊢ (Matrix.SpecialLinearGroup.mapGL ℝ) (-1) = -1

Tactic:
by ext; simp

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

Goal state before:
pp: z : ℍ
⊢ G2 z = ∑'[symmetricIco ℤ] (m : ℤ), e2Summand m z

Tactic:
by
  rw [G2, tsum_symmetricIcc_eq_tsum_symmetricIco (summable_e2Summand_symmetricIcc z)]
  simpa using! (tendsto_e2Summand_atTop_nhds_zero z).neg.comp tendsto_natCast_atTop_atTop

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inl
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
him : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ = 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ

Tactic:
grind [cases_c_one_d_zero hz hg him.le hc hd]

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

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

Tactic:
simp_rw [IsBigO, IsBigOWith, Filter.eventually_comap, Filter.eventually_atTop]

Goal state after:
⊢ ∃ c a, ∀ (b : ℝ), a ≤ b → ∀ (a : ℂ), a.im = b → ‖jacobiTheta a - 1‖ ≤ c * ‖rexp (-π * a.im)‖
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mp
y : ℝ
z : ℂ
⊢ z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y → z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

Tactic:
rintro ⟨⟨z, hz⟩, h, rfl⟩

Goal state after:
case mp
y : ℝ
z : ℂ
hz : 0 < z.im
h : { coe := z, coe_im_pos := hz } ∈ truncatedFundamentalDomain y
⊢ ↑{ coe := z, coe_im_pos := hz } ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing

Goal state before:
pp: z : ℍ
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
hg : CuspForm.toModularFormₗ g = E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : ⇑g = ⇑E₄CubeSubE₆SqForm
⊢ c = 1728

Tactic:
have hcΔ : (c • CuspForm.discriminant : ℍ → ℂ) = g := congrArg DFunLike.coe hc

Goal state after:
z : ℍ
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
hg : CuspForm.toModularFormₗ g = E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : ⇑g = ⇑E₄CubeSubE₆SqForm
hcΔ : c • ⇑CuspForm.discriminant = ⇑g
⊢ c = 1728
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : ModularFormClass F Γ k
r : ℝ
⊢ (fun t ↦ f (↑ofComplex (I * ↑t)) - valueAtInfty ⇑f) =O[atTop] fun t ↦ t ^ r

Tactic:
obtain ⟨C, hCpos, hCO⟩ := ModularFormClass.exp_decay_sub_atImInfty' f
  refine (hCO.comp_tendsto tendsto_ofComplex_I_mul_atTop_atImInfty).trans ?_
  refine (EventuallyEq.isBigO ?_).trans (isLittleO_exp_neg_mul_rpow_atTop hCpos r).isBigO
  filter_upwards [eventually_gt_atTop 0] with t ht
  simp [ht, ofComplex_apply_of_im_pos, ← coe_im]

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

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hf : ModularForm.norm ℋ f = 0
⊢ ⇑f = 0

Tactic:
← DFunLike.coe_injective.eq_iff,

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝³ : FunLike F ℍ ℂ
k : ℤ
inst✝² : 𝒢.IsFiniteRelIndex ℋ
inst✝¹ : ℋ.HasDetPlusMinusOne
inst✝ : ModularFormClass F 𝒢 k
hf : ⇑(ModularForm.norm ℋ f) = ⇑0
⊢ ⇑f = 0
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝³ : Group Γ
inst✝² : TopologicalSpace α
inst✝¹ : SMul Γ α
inst✝ : ProperlyDiscontinuousSMul Γ α
G : Subgroup Γ
⊢ ProperlyDiscontinuousSMul (↥G) α

Tactic:
refine Subgroup.properlyDiscontinuousSMul_of_le ?_ le_top
  simp only [Subgroup.properlyDiscontinuousSMul_iff, Subgroup.mem_top, true_and]
  exact finite_disjoint_inter_image

Goal state after: