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

Goal state before:
pp: a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a x y : ℕ
⊢ qrSign x a * qrSign y a * J(↑x * ↑y | a) = qrSign x a * J(↑x | a) * (qrSign y a * J(↑y | a))

Tactic:
mul_left,

Goal state after:
a✝ b : ℕ
ha : Odd a✝
hb : Odd b
a x y : ℕ
⊢ qrSign x a * qrSign y a * (J(↑x | a) * J(↑y | a)) = qrSign x a * J(↑x | a) * (qrSign y a * J(↑y | a))
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

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

Tactic:
mul_left,

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

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

Tactic:
mul_left,

Goal state after:
case inr
a b : ℕ
hb : Odd b
ha₀ : a ≠ 0
hb' : Odd (b % (4 * a))
e a' : ℕ
ha₁' : ¬2 ∣ a'
ha₂ : a = 2 ^ e * a'
ha₁ : Odd a'
⊢ J(↑(2 ^ e) | b) * J(↑a' | b) = J(↑(2 ^ e) | b % (4 * a)) * J(↑a' | b % (4 * a))
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:
v.isNontrivial_iff_exists_lt_one,

Goal state after:
K : Type u_3
Γ : Type u_4
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K Γ
⊢ (∃ x, x ≠ 0 ∧ v x < 1) ↔ ¬IsLocalRing.maximalIdeal ↥v.integer ≤ ⊥
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
⊢ Odd (mersenne (p + 1)) ↔ p + 1 ≠ 0

Tactic:
by
    simpa using! Nat.Even.sub_odd (one_le_pow₀ one_le_two)
      (even_two.pow_of_ne_zero p.succ_ne_zero) odd_one

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
apply Nat.eq_prime_pow_of_dvd_least_prime_pow
  -- the order of ω divides 2^p
  · exact Nat.prime_two
  · intro o
    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
    have h : (1 : ZMod (q (p' + 2))) = -1 :=
      congr_arg Prod.fst (ω_pow.symm.trans (ω_pow_eq_neg_one p' h))
    have : Fact (2 < (q (p' + 2) : ℕ)) := ⟨two_lt_q _⟩
    apply ZMod.neg_one_ne_one h.symm
  · apply orderOf_dvd_iff_pow_eq_one.2
    apply Units.ext
    push_cast
    exact ω_pow_eq_one p' h

Goal state after:
Module: Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete

Goal state before:
pp: case inr.mp
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
n : ℤ
⊢ g ^ (-1) < g ^ n → g ^ n < g ^ 1 → ⟨g ^ n, ⋯⟩ = 1

Tactic:
intro hn

Goal state after:
case inr.mp
G✝ : Type u_1
inst✝⁶ : CommGroup G✝
inst✝⁵ : TopologicalSpace G✝
G : Type u_1
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder G
inst✝² : IsOrderedMonoid G
inst✝¹ : TopologicalSpace G
inst✝ : OrderTopology G
g : G
ha✝ : 1 ≤ g
ha : 1 < g
n : ℤ
hn : g ^ (-1) < g ^ n
⊢ g ^ n < g ^ 1 → ⟨g ^ n, ⋯⟩ = 1
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
g : SL(2, ℤ)
⊢ OnePoint.map Rat.cast ((mapGL ℚ) g⁻¹ • ∞) = (mapGL ℝ) g⁻¹ • ∞

Tactic:
by rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
          ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
z : ℍ
⊢ (f ∣[k] ModularGroup.S) z = f { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * ↑z ^ (-k)

Tactic:
SL_slash_apply,

Goal state after:
f : ℍ → ℂ
k : ℤ
z : ℍ
⊢ f (ModularGroup.S • z) * denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)) ↑z ^ (-k) =
    f { coe := (-↑z)⁻¹, coe_im_pos := ⋯ } * ↑z ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
x : ℝ
⊢ x ∈ (map (mapGL ℝ) Γ).strictPeriods ↔ x ∈ AddSubgroup.zmultiples 1

Tactic:
simp only [mem_strictPeriods_iff, Subgroup.mem_map, Units.ext_iff, mapGL_coe_matrix,
    map_apply_coe]

Goal state after:
Γ : Subgroup SL(2, ℤ)
hΓ : ModularGroup.T ∈ Γ
x : ℝ
⊢ (∃ x_1 ∈ Γ, (algebraMap ℤ ℝ).mapMatrix ↑x_1 = ↑(upperRightHom x)) ↔ x ∈ AddSubgroup.zmultiples 1
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).toFun ∣[k] γ)

Tactic:
rw [SlashInvariantForm.toFun_eq_coe, SlashInvariantForm.coe_translate,
      ← SlashAction.slash_mul, ← isBoundedAt_infty_iff, ← OnePoint.IsBoundedAt.smul_iff]
    apply ModularFormClass.bdd_at_cusps f
    simpa [mul_smul, hγ] using hc.smul g

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
c : ℕ → ℂ
hf : ∀ (τ : ℍ), HasSum (fun m ↦ c m • 𝕢 h ↑τ ^ m) (f τ)
q : ℂ
hq : ‖q‖ < 1
hq1 : q ≠ 0
⊢ HasSum (fun m ↦ c m • q ^ m) (cuspFunction h f q)

Tactic:
by
  have h1 := Periodic.im_invQParam_pos_of_norm_lt_one hh hq hq1
  let τ : ℍ := ⟨Periodic.invQParam h q, h1⟩
  have h2 := (Periodic.cuspFunction_eq_of_nonzero h (f ∘ ofComplex) hq1)
  have : cuspFunction h f q = f τ := by simpa [UpperHalfPlane.ofComplex_apply_of_im_pos h1]
    using! h2
  grind [hf τ, Periodic.qParam_right_inv]

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

Goal state before:
pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ toGL ((map (Int.castRingHom ℝ)) g) • ∞ = (mapGL ℝ) g • ∞

Tactic:
by simp [mapGL]

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

Goal state before:
pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : CuspFormClass F Γ k
⊢ toGL ((map (Int.castRingHom ℝ)) g) • ∞ = (mapGL ℝ) g • ∞

Tactic:
by simp [mapGL]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
p : Fin 2 → ℤ
hp : IsCoprime (p 0) (p 1)
⊢ Tendsto (fun g ↦ |(↑g • z).re|) cofinite atTop

Tactic:
by
  suffices
    Tendsto (fun g : (fun g : SL(2, ℤ) => g 1) ⁻¹' {p} => ((g : SL(2, ℤ)) • z).re) cofinite
      (cocompact ℝ)
    by exact tendsto_norm_cocompact_atTop.comp this
  have : ((p 0 : ℝ) ^ 2 + (p 1 : ℝ) ^ 2)⁻¹ ≠ 0 := by
    apply inv_ne_zero
    exact mod_cast hp.sq_add_sq_ne_zero
  let f := Homeomorph.mulRight₀ _ this
  let ff := Homeomorph.addRight
    (((p 1 : ℂ) * z - p 0) / (((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) * (p 0 * z + p 1))).re
  convert! (f.trans ff).isClosedEmbedding.tendsto_cocompact.comp (tendsto_lcRow0 hp) with _ _ g
  change
    ((g : SL(2, ℤ)) • z).re =
      lcRow0 p ↑(↑g : SL(2, ℝ)) / ((p 0 : ℝ) ^ 2 + (p 1 : ℝ) ^ 2) +
        Complex.re (((p 1 : ℂ) * z - p 0) / (((p 0 : ℂ) ^ 2 + (p 1 : ℂ) ^ 2) * (p 0 * z + p 1)))
  exact mod_cast congr_arg Complex.re (smul_eq_lcRow0_add z hp g.2)

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
z : ℍ
⊢ f z = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f) 0) z

Tactic:
have hQ : 𝕢 1 z ∈ (Metric.ball 0 1) := by
    simpa using (norm_qParam_lt_iff zero_lt_one 0 z.1).mpr z.2

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 : ℍ
hQ : 𝕢 1 ↑z ∈ Metric.ball 0 1
⊢ f z = Function.const ℍ (UpperHalfPlane.cuspFunction 1 (⇑f) 0) z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: r : ℕ
inst✝ : NeZero r
⊢ BijOn (divIntMap ↑r) (gammaSet 1 r 0) (gammaSet 1 1 0)

Tactic:
refine ⟨?_, ?_, ?_⟩
  · intro x hx
    simp only [divIntMap, mem_gammaSet_one] at *
    exact finGcdMap_div _ hx.2
  · intro x hx v hv hv2
    ext i
    exact (Int.ediv_left_inj (gammaSet_div_gcd hx i) (gammaSet_div_gcd hv i)).mp
      (congr_fun hv2 i)
  · intro x hx
    use r • x
    simp only [nsmul_eq_mul, divIntMap, Int.cast_natCast]
    constructor
    · rw [mem_gammaSet_one, Int.isCoprime_iff_gcd_eq_one] at hx
      exact ⟨Subsingleton.eq_zero _, by simp [Int.gcd_mul_left, hx]⟩
    · ext i
      simp_all [NeZero.ne r]

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 : ∀ (g : SL(2, ℤ)), (fun τ ↦ f (g • τ)) =O[atImInfty] fun z ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst✝ : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
τ : ℍ
g h : SL(2, ℤ)
hgh : g ≈ h
⊢ ∃ j ∈ Γ, h = g * j

Tactic:
rw [← Quotient.eq_iff_equiv, Quotient.eq, QuotientGroup.leftRel_apply] at hgh
      exact ⟨g⁻¹ * h, hgh, (mul_inv_cancel_left g h).symm⟩

Goal state after:
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:
SL_slash_apply,

Goal state after:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
z : ℍ
⊢ eisensteinSeries a k (γ • z) *
      denom (SpecialLinearGroup.toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) γ)) ↑z ^ (-k) =
    eisensteinSeries (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)) k z
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
k : ℤ
A : GL (Fin 2) ℝ
hA : A ∈ Subgroup.map (SpecialLinearGroup.mapGL ℝ) Γ(N)
⊢ eisensteinSeries a k ∣[k] A = eisensteinSeries a k

Tactic:
obtain ⟨A, (hA : A ∈ Γ(N)), rfl⟩ := hA

Goal state after:
N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
k : ℤ
A : SL(2, ℤ)
hA : A ∈ Γ(N)
⊢ eisensteinSeries a k ∣[k] (SpecialLinearGroup.mapGL ℝ) A = eisensteinSeries a k
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 (UpperHalfPlane.coe '' Set.univ)

Tactic:
apply TendstoLocallyUniformlyOn.comp (s := ⊤) _ _ _ (OpenPartialHomeomorph.continuousOn_symm _)

Goal state after:
k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ TendstoLocallyUniformlyOn (fun n z ↦ ∑ x ∈ n, eisSummand k (↑x) z) (⇑(eisensteinSeriesSIF a k)) Filter.atTop ⊤

k : ℤ
N : ℕ
hk : 3 ≤ k
a : Fin 2 → ZMod N
⊢ MapsTo (↑(IsOpenEmbedding.toOpenPartialHomeomorph UpperHalfPlane.coe isOpenEmbedding_coe).symm)
    (IsOpenEmbedding.toOpenPartialHomeomorph UpperHalfPlane.coe isOpenEmbedding_coe).target ⊤
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
m : ℕ
q : ℂ
⊢ cuspFunction h 1 q = 1 q

Tactic:
rcases eq_or_ne q 0 with rfl | hq

Goal state after:
case inl
h : ℝ
m : ℕ
⊢ cuspFunction h 1 0 = 1 0

case inr
h : ℝ
m : ℕ
q : ℂ
hq : q ≠ 0
⊢ cuspFunction h 1 q = 1 q
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: z : ℂ
hz : z ∈ ℍₒ
⊢ ∏' (n : ℕ), (1 - eta_q n z) ≠ 0

Tactic:
refine tprod_one_add_ne_zero_of_summable (f := fun n ↦ -eta_q n z) ?_ ?_

Goal state after:
case refine_1
z : ℂ
hz : z ∈ ℍₒ
⊢ ∀ (i : ℕ), 1 + -eta_q i z ≠ 0

case refine_2
z : ℂ
hz : z ∈ ℍₒ
⊢ Summable fun x ↦ ‖-eta_q x z‖
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
⊢ (Δ ∣[12] ModularGroup.T) z = Δ z

Tactic:
SL_slash_apply,

Goal state after:
z : ℍ
⊢ Δ (ModularGroup.T • z) *
      denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.T)) ↑z ^
        (-12) =
    Δ z
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: z : ℍ
this : η (-(↑z)⁻¹) ^ 24 * (↑z ^ 12)⁻¹ = η ↑z ^ 24
⊢ (Δ ∣[12] ModularGroup.S) z = Δ z

Tactic:
SL_slash_apply,

Goal state after:
z : ℍ
this : η (-(↑z)⁻¹) ^ 24 * (↑z ^ 12)⁻¹ = η ↑z ^ 24
⊢ Δ (ModularGroup.S • z) *
      denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S)) ↑z ^
        (-12) =
    Δ z
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: case h
k : ℕ
ihn :
  ∀ m < k,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even k
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    ↑(if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1)

Tactic:
| h k ihn =>

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mp
g : SL(2, ℤ)
⊢ g • ρ = ρ → g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)}

pp: case mpr
g : SL(2, ℤ)
⊢ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} → g • ρ = ρ

Tactic:
· intro hg
    have neS : g ≠ S ∧ g ≠ -S := by
      have : S • ρ ≠ ρ := by
        rw [ne_eq, UpperHalfPlane.ext_iff, modular_S_smul, coe_mk, Complex.ext_iff]
        norm_num [ρ, ← pow_two, div_pow]
      grind [SL_neg_smul]
    have neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹ := by
      have : T • ρ ≠ ρ := by
        rw [ne_eq, UpperHalfPlane.ext_iff, modular_T_smul, coe_vadd]
        norm_num
      have : T⁻¹ • ρ ≠ ρ := by rwa [ne_eq, inv_smul_eq_iff, eq_comm]
      grind [SL_neg_smul]
    have neTST : g ≠ T * S * T ∧ g ≠ -(T * S * T) := by
      have : (T * S * T) • ρ ≠ ρ := by
        simp only [mul_smul, modular_T_smul, modular_S_smul,
          ne_eq, UpperHalfPlane.ext_iff, Complex.ext_iff]
        norm_num [ρ, ← pow_two, div_pow, normSq]
      grind [SL_neg_smul]
    have := cases_of_mem_fd_smul_mem_fd ρ_mem_fd (hg ▸ ρ_mem_fd)
    norm_num [UpperHalfPlane.ext_iff, Complex.ext_iff, norm_ρ, ρ, neS, neT, neTST] at this
    grind

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)} → g • ρ = ρ
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: τ : ℍ
hτ : τ ∈ 𝒟
⊢ ↑τ ∈ {z | 0 < z.im ∧ 1 ≤ ‖z‖ ∧ |z.re| ≤ 1 / 2}

Tactic:
exact ⟨τ.im_pos, one_le_normSq_iff.mp hτ.1, hτ.2⟩

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
ξ : ℍ
hξ : ξ ∈ 𝒟
⊢ ξ ∈ (fun τ ↦ ‖↑τ‖) ⁻¹' Set.Ici 1

Tactic:
simpa [Set.mem_preimage, Set.mem_Ici, one_le_normSq_iff] using hξ.1

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

Goal state before:
pp: 𝒮ℒ' : Subgroup SL(2, ℝ) := (SpecialLinearGroup.map (Int.castRingHom ℝ)).range
this : ∀ {K L : Set ℍ}, IsCompact K → IsCompact L → {g | g ∈ 𝒮ℒ' ∧ (g • K ∩ L).Nonempty}.Finite
⊢ ∀ {K L : Set ℍ},
    IsCompact K → IsCompact L → {g | g ∈ (SpecialLinearGroup.mapGL ℝ).range ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
refine fun K L hK hL ↦ ((this hK hL).map SpecialLinearGroup.toGL).subset fun g ↦ ?_

Goal state after:
𝒮ℒ' : Subgroup SL(2, ℝ) := (SpecialLinearGroup.map (Int.castRingHom ℝ)).range
this : ∀ {K L : Set ℍ}, IsCompact K → IsCompact L → {g | g ∈ 𝒮ℒ' ∧ (g • K ∩ L).Nonempty}.Finite
K L : Set ℍ
hK : IsCompact K
hL : IsCompact L
g : GL (Fin 2) ℝ
⊢ g ∈ {g | g ∈ (SpecialLinearGroup.mapGL ℝ).range ∧ (g • K ∩ L).Nonempty} →
    g ∈ ⇑SpecialLinearGroup.toGL <$> {g | g ∈ 𝒮ℒ' ∧ (g • K ∩ L).Nonempty}
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
⊢ (toConjAct (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))⁻¹ •
      Γ).IsArithmetic

Tactic:
convert Subgroup.IsArithmetic.conj Γ ↑(ModularGroup.S⁻¹)

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝¹ : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝ : FunLike F ℍ ℂ
f : F
s : ℂ
⊢ (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) ModularGroup.S))⁻¹ =
    (Matrix.GeneralLinearGroup.map (Rat.castHom ℝ))
      (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℚ)) ModularGroup.S⁻¹))
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ p ^ 2 ∣ (x + p) ^ (n + 1) - x ^ (n + 1 - 1) * p * ↑(n + 1) - x ^ (n + 1)

Tactic:
simp only [add_pow, sum_range_succ, add_tsub_cancel_left, pow_one, Nat.choose_succ_self_right,
      Nat.cast_succ, tsub_self, pow_zero, mul_one, Nat.choose_self, Nat.cast_zero, zero_add,
      Nat.succ_sub_succ_eq_sub, Nat.sub_zero]

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ p ^ 2 ∣
    ∑ m ∈ range n, x ^ m * p ^ (n + 1 - m) * ↑((n + 1).choose m) + x ^ n * p * (↑n + 1) + x ^ (n + 1) -
        x ^ n * p * (↑n + 1) -
      x ^ (n + 1)
Module: Mathlib.NumberTheory.ModularForms.LFunction

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

Tactic:
mul_div_assoc,

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : ↑k + 1 < s.re
⊢ HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)

Tactic:
refine hasSum_Λ_of_qExpansion_isBigO hk f (r := k)
    (by linarith [show (0 : ℝ) < k from mod_cast hk]) (by exact_mod_cast hs) ?_ ?_
  · rw [Λ, ← ((weakFEPair hk f).hasMellin <| by grind [weakFEPair]).2]
  · simpa using ModularFormClass.qExpansion_isBigO hk.le f

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
S₁ : ι₁ → Type u_7
S₂ : ι₂ → Type u_8
inst✝⁵ : (i : ι₁) → SetLike (S₁ i) (R₁ i)
inst✝⁴ : (j : ι₂) → SetLike (S₂ j) (R₂ j)
B₁ : (i : ι₁) → S₁ i
B₂ : (j : ι₂) → S₂ j
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
inst✝³ : (i : ι₁) → Monoid (R₁ i)
inst✝² : (i : ι₂) → Monoid (R₂ i)
inst✝¹ : ∀ (i : ι₁), SubmonoidClass (S₁ i) (R₁ i)
inst✝ : ∀ (i : ι₂), SubmonoidClass (S₂ i) (R₂ i)
φ : (j : ι₂) → R₁ (f j) →* R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo ⇑(φ j) ↑(B₁ (f j)) ↑(B₂ j)
x y : Πʳ (i : ι₁), [R₁ i, ↑(B₁ i)]_[𝓕₁]
⊢ mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ (x * y) =
    mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ x * mapAlong R₁ R₂ f hf (fun j r ↦ (φ j) r) hφ y

Tactic:
by
    ext i
    exact map_mul (φ i) _ _

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝⁴ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
j : ι
⊢ (single A i (x i * r)) j = (x * single A i r) j

Tactic:
rcases eq_or_ne i j with rfl | hne

Goal state after:
case inl
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝⁴ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
⊢ (single A i (x i * r)) i = (x * single A i r) i

case inr
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝⁴ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
j : ι
hne : i ≠ j
⊢ (single A i (x i * r)) j = (x * single A i r) j
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝⁴ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
j : ι
⊢ (single A i (r * x i)) j = (single A i r * x) j

Tactic:
rcases eq_or_ne i j with rfl | hne

Goal state after:
case inl
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝⁴ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
⊢ (single A i (r * x i)) i = (single A i r * x) i

case inr
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝⁴ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
j : ι
hne : i ≠ j
⊢ (single A i (r * x i)) j = (single A i r * x) j
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x : ℤ
hx : ∃ k, x = 2 * k + 1
⊢ x ^ 2 % 4 = 1

Tactic:
rcases hx with ⟨_, rfl⟩

Goal state after:
w✝ : ℤ
⊢ (2 * w✝ + 1) ^ 2 % 4 = 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case inl
x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
hyx : y ≤ x
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

Tactic:
iterate 3 rw [← Int.natCast_emultiplicity]
    simp only [Int.ofNat_sub hyx, Int.ofNat_sub (pow_le_pow_left' hyx _), Int.natCast_add,
      Int.natCast_pow]
    rw [← Int.natCast_dvd_natCast] at hx
    rw [← Int.natCast_dvd_natCast, Int.ofNat_sub hyx] at hxy
    convert! Int.two_pow_sub_pow hxy hx hn using 2
    rw [← Int.natCast_emultiplicity]
    rfl

Goal state after: