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

Goal state before:
pp: case inr
a : ℝ
ha₀ : 0 ≤ a
ha₁ : a < 1
z : ℂ
hz : ‖z‖ = 1
hac₀ : ‖↑a‖ < 1
hac₁ : ‖↑a * z‖ < 1
hac₂ : ‖↑a * z ^ 2‖ < 1
n : ℕ
hn : n > 0
⊢ 0 ≤ 3 * (a ^ n / ↑n) + 4 * (a ^ n * (z ^ n).re / ↑n) + a ^ n * ((z ^ 2) ^ n).re / ↑n

Tactic:
· simp only [← mul_div_assoc, ← add_div]
    refine div_nonneg ?_ n.cast_nonneg
    rw [← pow_mul, pow_mul', sq, mul_re, ← sq, ← sq, ← sq_norm_sub_sq_re, norm_pow, hz]
    convert! (show 0 ≤ 2 * a ^ n * ((z ^ n).re + 1) ^ 2 by positivity) using 1
    ring

Goal state after:
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
⊢ 1 * ‖↑↑n ^ (-(I * ↑y))‖ = 1

Tactic:
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.LSeries.PrimesInAP

Goal state before:
pp: case inl
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
H : Summable fun n ↦ (if Nat.Prime n then residueClass a n else 0) / ↑n
key : Summable fun n ↦ residueClass a n / ↑n
C : ℝ := ∑' (n : ℕ), residueClass a n / ↑n
H₁✝ : ∀ {x : ℝ}, 1 < x → ∑' (n : ℕ), residueClass a n / ↑n ^ x ≤ C
C' : ℝ
hC' : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ / (x - 1) - C' ≤ ∑' (n : ℕ), residueClass a n / ↑n ^ x
H₁ : ∀ {x : ℝ}, x ∈ Set.Ioc 1 2 → (↑q.totient)⁻¹ ≤ (C + C') * (x - 1)
hq : 0 < (↑q.totient)⁻¹
h₀ : C + C' ≤ 0
this : 0 < C + C'
⊢ False

Tactic:
exact (this.trans_le h₀).false

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

Goal state before:
pp: n q a : ℕ
hq : q ≠ 0
h : a.Coprime q
⊢ ∃ p > n, Prime p ∧ p ≡ a [MOD q]

Tactic:
by
  simpa using forall_exists_prime_gt_and_zmodEq n (q := q) (a := a) hq (by simpa)

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) *
      ↑(∏ i ∈ Ico 1 (p / 2).succ, (↑a * ↑i).valMinAbs.natAbs) =
    (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ↑(p / 2)!

Tactic:
Finset.prod_eq_multiset_prod,

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
hap : ↑a ≠ 0
⊢ (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) *
      ↑(Multiset.map (fun i ↦ (↑a * ↑i).valMinAbs.natAbs) (Ico 1 (p / 2).succ).val).prod =
    (-1) ^ #({x ∈ Ico 1 (p / 2).succ | ¬(↑a * ↑x).val ≤ p / 2}) * ↑(p / 2)!
Module: Mathlib.RingTheory.Valuation.DiscreteValuativeRel

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : Semiring R
inst✝ : ValuativeRel R
⊢ IsDiscrete R ∧ IsNontrivial R ∧ MulArchimedean (ValueGroupWithZero R) →
    Nonempty (ValueGroupWithZero R ≃*o WithZero (Multiplicative ℤ))

Tactic:
· rintro ⟨hD, hN, hM⟩
    rw [isNontrivial_iff_nontrivial_units] at hN
    rw [LinearOrderedCommGroupWithZero.discrete_iff_not_denselyOrdered]
    intro H
    obtain ⟨x, hx, hx'⟩ := hD.has_maximal_element
    obtain ⟨y, hy, hy'⟩ := exists_between hx
    exact hy.not_ge (hx' y hy')

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 γ

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
⊢ IsCompact {x | (valuation K) x ≤ (valuation K) γ}
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case pos
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
h : b % 8 = 3 ∨ b % 8 = 5
⊢ (if flip = false then -J(↑a / 2 | b) else J(↑a / 2 | b)) = if flip = true then J(↑a / 2 | b) else -J(↑a / 2 | b)

Tactic:
cases flip

Goal state after:
case pos.false
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 : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
h : b % 8 = 3 ∨ b % 8 = 5
⊢ (if false = false then -J(↑a / 2 | b) else J(↑a / 2 | b)) = if false = true then J(↑a / 2 | b) else -J(↑a / 2 | b)

case pos.true
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 : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : a % 2 = 0
h : b % 8 = 3 ∨ b % 8 = 5
⊢ (if true = false then -J(↑a / 2 | b) else J(↑a / 2 | b)) = if true = true then J(↑a / 2 | b) else -J(↑a / 2 | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case pos
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
ha1 : ¬a = 1
hba : ¬b % a = 0
h : a % 4 = 3 ∧ b % 4 = 3
⊢ (if flip = false then -J(↑b | a) else J(↑b | a)) = if flip = true then J(↑b | a) else -J(↑b | a)

Tactic:
cases flip

Goal state after:
case pos.false
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 : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
h : a % 4 = 3 ∧ b % 4 = 3
⊢ (if false = false then -J(↑b | a) else J(↑b | a)) = if false = true then J(↑b | a) else -J(↑b | a)

case pos.true
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 : ℕ
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
ha4 : ¬a % 4 = 0
ha2 : ¬a % 2 = 0
ha1 : ¬a = 1
hba : ¬b % a = 0
h : a % 4 = 3 ∧ b % 4 = 3
⊢ (if true = false then -J(↑b | a) else J(↑b | a)) = if true = true then J(↑b | a) else -J(↑b | a)
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr.refine_1
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
⊢ (i : K) → i ∈ ↑t → (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ

Tactic:
refine fun i hi ↦ if hi' : v i ≤ z then z else Units.mk0 ⟨(v i), by simp⟩ ?_

Goal state after:
case inr.refine_1
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : K
hi : i ∈ ↑t
hi' : ¬v i ≤ ↑↑z
⊢ ⟨v i, ⋯⟩ ≠ 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
I : TwoSidedIdeal A := mk' (Set.range fun x_1 ↦ x * x_1) ⋯ ⋯ ⋯ ⋯ ⋯
y : A
hy : x * y = 1
a : A
⊢ a * y = x * y * a * y

Tactic:
rw [hy, one_mul]

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
this : p.leadingCoeff = 1 ∨ p.leadingCoeff = -1
⊢ (C (1 / p.leadingCoeff) * p).Monic

Tactic:
aesop (add safe (by simp [Monic.def]))

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
⊢ (g ^ n).parabolicFixedPoint = g.parabolicFixedPoint

Tactic:
eq_comm,

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
hg : g.IsParabolic
inst✝ : CharZero K
n : ℕ
hn : n ≠ 0
⊢ g.parabolicFixedPoint = (g ^ n).parabolicFixedPoint
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
⊢ (σ (A * B)) (f ((A * B) • τ)) * ↑|↑(Matrix.GeneralLinearGroup.det (A * B))| ^ (k - 1) * denom (A * B) ↑τ ^ (-k) =
    (σ B) ((σ A) (f (A • B • τ))) *
        (↑|↑(Matrix.GeneralLinearGroup.det A)| ^ (k - 1) * ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1)) *
      ((σ B) (denom A ↑(B • τ) ^ (-k)) * denom B ↑τ ^ (-k))

Tactic:
σ_mul_comm,

Goal state after:
k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
⊢ (σ (A * B)) (f ((A * B) • τ)) * ↑|↑(Matrix.GeneralLinearGroup.det (A * B))| ^ (k - 1) * denom (A * B) ↑τ ^ (-k) =
    (σ A) ((σ B) (f (A • B • τ))) *
        (↑|↑(Matrix.GeneralLinearGroup.det A)| ^ (k - 1) * ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1)) *
      ((σ B) (denom A ↑(B • τ) ^ (-k)) * denom B ↑τ ^ (-k))
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: g : GL (Fin 2) ℝ
f : ℍ → ℂ
k : ℤ
hg : ↑g 1 0 = 0
hf : IsZeroAtImInfty f
⊢ IsZeroAtImInfty (f ∣[k] g)

Tactic:
by
  rw [IsZeroAtImInfty, ZeroAtFilter, tendsto_zero_iff_norm_tendsto_zero] at hf ⊢
  simpa [ModularForm.slash_def, denom, hg, mul_assoc]
    using (hf.comp <| tendsto_smul_atImInfty hg).mul_const _

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

Goal state before:
pp: case neg
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
u : R
hu_mem : u ∈ 𝒢.periods
hu_notMem : u ∉ 𝒢.strictPeriods
⊢ 𝒢.strictPeriods.relIndex 𝒢.periods = 1 ∨
    ∃ a ∈ 𝒢.periods, a ∉ 𝒢.strictPeriods ∧ ∀ b ∈ 𝒢.periods, b + a ∈ 𝒢.strictPeriods ∨ b ∈ 𝒢.strictPeriods

Tactic:
refine .inr ⟨u, hu_mem, hu_notMem, fun b hb ↦ ?_⟩

Goal state after:
case neg
R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
h : 𝒢.strictPeriods < 𝒢.periods
u : R
hu_mem : u ∈ 𝒢.periods
hu_notMem : u ∉ 𝒢.strictPeriods
b : R
hb : b ∈ 𝒢.periods
⊢ b + u ∈ 𝒢.strictPeriods ∨ b ∈ 𝒢.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
h : ℝ
hh : 0 < h
h𝒢 : h ∈ 𝒢.strictPeriods
⊢ IsCusp ∞ 𝒢

Tactic:
by
  refine ⟨upperRightHom h, 𝒢.mem_strictPeriods_iff.mp h𝒢, ?_, smul_infty_eq_self_iff.mpr rfl⟩
  exact (GeneralLinearGroup.isParabolic_iff_of_upperTriangular rfl).mpr ⟨rfl, hh.ne'⟩

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

Goal state before:
pp: f : ℍ → ℂ
hf : MDiff f
k : ℤ
g : GL (Fin 2) ℝ
hg : 0 < ↑(Matrix.GeneralLinearGroup.det g)
⊢ MDiff fun x ↦ (σ g) (f (g • x))

Tactic:
simpa only [σ, hg, ↓reduceIte] using! hf.comp (mdifferentiable_smul hg)

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
⊢ ∞.IsBoundedAt (⇑f ∣[k] g) ?m.26

pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ ℤ

Tactic:
SL_slash,

Goal state after:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ ∞.IsBoundedAt (⇑f ∣[k] toGL ((map (Int.castRingHom ℝ)) g)) ?m.26

k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : ModularFormClass F Γ k
⊢ ℤ
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
⊢ ∞.IsZeroAt (⇑f ∣[k] g) ?m.27

pp: k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : CuspFormClass F Γ k
⊢ ℤ

Tactic:
SL_slash,

Goal state after:
k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : CuspFormClass F Γ k
⊢ ∞.IsZeroAt (⇑f ∣[k] toGL ((map (Int.castRingHom ℝ)) g)) ?m.27

k : ℤ
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : FunLike F ℍ ℂ
f : F
inst✝¹ : Γ.IsArithmetic
g : SL(2, ℤ)
inst✝ : CuspFormClass F Γ k
⊢ ℤ
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) *
      deriv (circleMap 0 R) (u * (2 * π / h)) •
        (cuspFunction h f (circleMap 0 R (u * (2 * π / h))) / circleMap 0 R (u * (2 * π / h)) ^ (n + 1)) =
    1 / ↑h * (1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ })

Tactic:
deriv_circleMap,

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) *
      (circleMap 0 R (u * (2 * π / h)) * Complex.I) •
        (cuspFunction h f (circleMap 0 R (u * (2 * π / h))) / circleMap 0 R (u * (2 * π / h)) ^ (n + 1)) =
    1 / ↑h * (1 / 𝕢 h (↑u + ↑t * ↑I) ^ n * f { coe := ↑u + ↑t * ↑I, coe_im_pos := ⋯ })
Module: Mathlib.NumberTheory.ModularForms.Bounds

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ ‖f τ‖ ^ 2 ≤ C / (τ.im ^ (↑k / 2)) ^ 2

Tactic:
grw [← hC]

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
C : ℝ
τ : ℍ
hC : ‖petersson k (⇑f) (⇑f) τ‖ ≤ C
⊢ ‖f τ‖ ^ 2 ≤ ‖petersson k (⇑f) (⇑f) τ‖ / (τ.im ^ (↑k / 2)) ^ 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ b
hre : (g • z).re = ↑b + z.re
this : |b| ≤ 1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
Int.abs_le_one_iff

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ b
hre : (g • z).re = ↑b + z.re
this : b = 0 ∨ b = 1 ∨ b = -1
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
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⌋

Tactic:
eq_comm,

Goal state after:
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 / 2⌋ = 1
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
⊢ (fun n ↦ (PowerSeries.coeff n) (qExpansion Γ.strictWidthInfty ⇑f)) =O[atTop] fun n ↦ ↑n ^ k

Tactic:
by
  simp only [← Real.rpow_intCast]
  apply qExpansion_coeff_isBigO_of_norm_isBigO
  obtain ⟨C, hC⟩ := exists_bound hk f
  simp_rw [IsBigO, ← Int.cast_neg, Real.rpow_intCast, IsBigOWith, eventually_comap]
  use C
  filter_upwards [eventually_le_nhds zero_lt_one] with _ hτ τ rfl
  refine (hC τ).trans (le_of_eq ?_)
  rw [max_eq_right, zpow_neg, Real.norm_of_nonneg (by positivity), one_div]
  exact one_le_one_div (by positivity) (zpow_le_one₀ τ.im_pos hτ hk)

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

Goal state before:
pp: z : ℍ
n b : ℤ
⊢ eisSummand 2 ![-n, -b] z = eisSummand 2 ![n, b] z

Tactic:
simp only [eisSummand, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
    Matrix.cons_val_fin_one, Int.reduceNeg, zpow_neg, Int.cast_neg, neg_mul, inv_inj]

Goal state after:
z : ℍ
n b : ℤ
⊢ (-(↑n * ↑z) + -↑b) ^ 2 = (↑n * ↑z + ↑b) ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: A B : SL(2, ℤ)
z : ℍ
⊢ ↑(↑(A * B) 1 0) * denom (toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) B)) ↑z =
    ↑(↑A 1 0) * ↑(↑B).det +
      ↑(↑B 1 0) *
        denom
          (toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) A) *
            toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) B))
          ↑z

Tactic:
have h0 := Matrix.two_mul_expl A.1 B.1

Goal state after:
A B : SL(2, ℤ)
z : ℍ
h0 :
  (↑A * ↑B) 0 0 = ↑A 0 0 * ↑B 0 0 + ↑A 0 1 * ↑B 1 0 ∧
    (↑A * ↑B) 0 1 = ↑A 0 0 * ↑B 0 1 + ↑A 0 1 * ↑B 1 1 ∧
      (↑A * ↑B) 1 0 = ↑A 1 0 * ↑B 0 0 + ↑A 1 1 * ↑B 1 0 ∧ (↑A * ↑B) 1 1 = ↑A 1 0 * ↑B 0 1 + ↑A 1 1 * ↑B 1 1
⊢ ↑(↑(A * B) 1 0) * denom (toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) B)) ↑z =
    ↑(↑A 1 0) * ↑(↑B).det +
      ↑(↑B 1 0) *
        denom
          (toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) A) *
            toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) B))
          ↑z
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr
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
this✝ : |↑(↑g 0 0) + -z.re| ≤ 1 / 2
this : |↑g 0 0| ≤ 1
hzre : |z.re| = 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
Int.abs_le_one_iff

Goal state after:
case inr
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
this✝ : |↑(↑g 0 0) + -z.re| ≤ 1 / 2
this : ↑g 0 0 = 0 ∨ ↑g 0 0 = 1 ∨ ↑g 0 0 = -1
hzre : |z.re| = 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.ModularForms.DedekindEta

Goal state before:
pp: n : ℕ
z : ℂ
hz : z ∈ ℍₒ
⊢ 1 - eta_q n z ≠ 0

Tactic:
by
  rw [eta_q_eq_cexp, sub_ne_zero]
  intro h
  simpa [← mul_assoc, ← h] using norm_exp_two_pi_I_lt_one ⟨(n + 1) • z, by
    simpa [(show 0 < (n + 1 : ℝ) by positivity)] using hz⟩

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
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
⊢ T • ρ = S • ρ

Tactic:
eq_comm,

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
hgeq : g = T ^ ↑g 0 0 * S * T
hnorm : normSq ↑z = 1
hre : z.re = -1 / 2
hρ : z = ρ
⊢ S • ρ = T • ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 : G2 = G2 ∣[2] g⁻¹ + (-D2 g) ∣[2] g⁻¹
⊢ G2 ∣[2] g⁻¹ = G2 - D2 g⁻¹

Tactic:
SL_slash,

Goal state after:
case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 :
  G2 =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) +
      (-D2 g) ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹)
⊢ G2 ∣[2] g⁻¹ = G2 - D2 g⁻¹
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 :
  G2 =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) +
      -D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹)
this : D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) = -D2 g⁻¹
⊢ G2 ∣[2] g⁻¹ =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) - -D2 g⁻¹ - D2 g⁻¹

Tactic:
SL_slash,

Goal state after:
case inv
γ g : SL(2, ℤ)
hx✝ : g ∈ Subgroup.closure {S, T}
ig : G2 ∣[2] g = G2 - D2 g
H1 :
  G2 =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) +
      -D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹)
this : D2 g ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) = -D2 g⁻¹
⊢ G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) =
    G2 ∣[2] Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g⁻¹) - -D2 g⁻¹ - D2 g⁻¹
Module: Mathlib.NumberTheory.Modular

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

Tactic:
eq_comm,

Goal state after:
case inr
g✝¹ : SL(2, ℤ)
z✝¹ : ℍ
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hden : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc✝ : 0 ≤ ↑g 1 0
hc : ↑g 1 0 = 1
⊢ z.im * normSq (denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z) = z.im
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: ⊢ Tendsto (fun z ↦ 𝕢 1 ↑z * ∏' (n : ℕ), (1 - eta_q n ↑z) ^ 24) atImInfty (𝓝 0)

Tactic:
show (0 : ℂ) = 0 * 1 by ring

Goal state after:
⊢ Tendsto (fun z ↦ 𝕢 1 ↑z * ∏' (n : ℕ), (1 - eta_q n ↑z) ^ 24) atImInfty (𝓝 (0 * 1))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: case e_a.e_f
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), 1 / (↑{ coe := (↑a + 1) * ↑z, coe_im_pos := ⋯ } + ↑n) ^ (1 + 1) =
    (-2 * ↑π * I) ^ (1 + 1) / ↑1! *
      ∑' (n : ℕ+), ↑↑n ^ 1 * cexp (2 * ↑π * I * ↑{ coe := (↑a + 1) * ↑z, coe_im_pos := ⋯ }) ^ ↑n
⊢ 2 * ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    -(8 * (↑π ^ 2 * ∑' (n : ℕ+), cexp (↑z * (I * ↑π) * 2) ^ ↑n * (cexp (↑z * (I * ↑π) * 2) ^ (a * ↑n) * ↑↑n)))

Tactic:
simp only [add_comm, Nat.reduceAdd, one_div, mul_comm, mul_neg, even_two,
    Even.neg_pow, Nat.factorial_one, Nat.cast_one, div_one, pow_one] at H2

Goal state after:
case e_a.e_f
z : ℍ
N a : ℕ
H2 :
  ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    (I * (↑π * 2)) ^ 2 * ∑' (n : ℕ+), cexp (↑z * (↑a + 1) * (I * (↑π * 2))) ^ ↑n * ↑↑n
⊢ 2 * ∑' (n : ℤ), ((↑n + ↑z * (↑a + 1)) ^ 2)⁻¹ =
    -(8 * (↑π ^ 2 * ∑' (n : ℕ+), cexp (↑z * (I * ↑π) * 2) ^ ↑n * (cexp (↑z * (I * ↑π) * 2) ^ (a * ↑n) * ↑↑n)))