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

Goal state before:
pp: k : ℕ
x y : ℝ
⊢ bernoulliFun (k + 1) y = bernoulliFun (k + 1) x + ∫ (t : ℝ) in x..y, ↑(k + 1) * bernoulliFun k t

Tactic:
rw [intervalIntegral.integral_eq_sub_of_hasDerivAt, add_sub_cancel]

Goal state after:
case hderiv
k : ℕ
x y : ℝ
⊢ ∀ x_1 ∈ [[x, y]], HasDerivAt (bernoulliFun (k + 1)) (↑(k + 1) * bernoulliFun k x_1) x_1

case hint
k : ℕ
x y : ℝ
⊢ IntervalIntegrable (fun t ↦ ↑(k + 1) * bernoulliFun k t) volume x y
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case refine_1
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ ↑(Real.sin (2 * π * x * ↑n)) / ↑n ^ (2 * ↑k + 1) = ↑(1 / ↑n ^ (2 * k + 1) * Real.sin (2 * π * ↑n * x))

Tactic:
norm_cast

Goal state after:
case refine_1
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
n : ℕ
⊢ Real.sin (2 * π * x * ↑n) / ↑(n ^ (2 * k + 1)) = 1 / ↑(n ^ (2 * k + 1)) * Real.sin (2 * π * ↑n * x)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 < (2 * ↑k + 1).re

Tactic:
norm_cast

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 1 < 2 * k + 1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 2 * ↑k = ↑(2 * k - 1) + 1

Tactic:
norm_cast

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
⊢ 2 * k = 2 * k - 1 + 1
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case e_a
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
this : ↑(2 * k)! = 2 * ↑k * Complex.Gamma (2 * ↑k)
⊢ (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / (2 * 2 * ↑k * Complex.Gamma (2 * ↑k)) =
    (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * ↑k) / (2 * 2 * ↑k * Complex.Gamma (2 * ↑k))

Tactic:
norm_cast

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

Goal state before:
pp: k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
⊢ 2 * ↑k ≠ 1

Tactic:
norm_cast

Goal state after:
k : ℕ
x : ℝ
hk : k ≠ 0
hx : x ∈ Icc 0 1
h1 : ∀ (n : ℕ), 2 * ↑k ≠ -↑n
⊢ ¬2 * k = 1
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
n : ℤ
hn : n ≠ 0
⊢ bernoulliFourierCoeff k n = 1 / (-2 * ↑π * I * ↑n) * ((if k = 1 then 1 else 0) - ↑k * bernoulliFourierCoeff (k - 1) n)

Tactic:
unfold bernoulliFourierCoeff
  rw [fourierCoeffOn_of_hasDerivAt zero_lt_one hn
      (fun x _ => (hasDerivAt_bernoulliFun k x).ofReal_comp)
      ((continuous_ofReal.comp <|
            continuous_const.mul <| Polynomial.continuous _).intervalIntegrable
        _ _)]
  simp_rw [ofReal_one, ofReal_zero, sub_zero, one_mul]
  rw [QuotientAddGroup.mk_zero, fourier_eval_zero, one_mul, ← ofReal_sub, bernoulliFun_eval_one,
    add_sub_cancel_left]
  congr 2
  · split_ifs <;> simp only [ofReal_one, ofReal_zero]
  · simp_rw [ofReal_mul, ofReal_natCast, fourierCoeffOn.const_mul]

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

Goal state before:
pp: case e'_3
k : ℕ
hk : k ≠ 0
⊢ (-1) ^ (k + 1) * 2 ^ (2 * k - 1) * ↑π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! =
    ↑((-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!)

Tactic:
norm_cast

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

Goal state before:
pp: case e'_3
⊢ ↑π ^ 2 / 6 = ↑(π ^ 2 / 6)

Tactic:
norm_cast

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : 2 ≤ k
⊢ Summable fun n ↦ -↑k ! / (2 * ↑π * I * ↑n) ^ k

Tactic:
have :
      ∀ n : ℤ, -(k ! : ℂ) / (2 * π * I * n) ^ k = -k ! / (2 * π * I) ^ k * (1 / (n : ℂ) ^ k) := by
    intro n; rw [mul_one_div, div_div, ← mul_pow]
  simp_rw [this]
  refine Summable.mul_left _ <| .of_norm ?_
  have : (fun x : ℤ => ‖1 / (x : ℂ) ^ k‖) = fun x : ℤ => |1 / (x : ℝ) ^ k| := by
    ext1 x
    simp only [one_div, norm_inv, norm_pow, norm_intCast, pow_abs, abs_inv]
  simp_rw [this]
  rwa [summable_abs_iff, Real.summable_one_div_int_pow]

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

Goal state before:
pp: case e'_3
⊢ ↑π ^ 4 / 90 = ↑(π ^ 4 / 90)

Tactic:
norm_cast

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

Goal state before:
pp: m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑n + 1 = ↑(↑n + 1)

Tactic:
norm_cast

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

Goal state before:
pp: m n : ℕ
z : ℂ
x : ℝ
Hn : 0 ≤ (↑n + 1)⁻¹
⊢ ↑m = ↑↑m

Tactic:
norm_cast

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

Goal state before:
pp: N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
⊢ LSeriesSummable (⇑χ.zetaMul) s

Tactic:
refine ArithmeticFunction.LSeriesSummable_mul (LSeriesSummable_zeta_iff.mpr hs) <|
    LSeriesSummable_of_bounded_of_one_lt_re (m := 1) (fun n hn ↦ ?_) hs

Goal state after:
N : ℕ
χ : DirichletCharacter ℂ N
s : ℂ
hs : 1 < s.re
n : ℕ
hn : n ≠ 0
⊢ ‖(toArithmeticFunction fun x ↦ χ ↑x) n‖ ≤ 1
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ False

Tactic:
refine B.F_neg_two.not_gt ?_

Goal state after:
N : ℕ
inst✝ : NeZero N
χ : DirichletCharacter ℂ N
hχ : χ ^ 2 = 1
χ_ne : χ ≠ 1
hL : LFunction χ 1 = 0
B : BadChar N := { χ := χ, χ_ne := χ_ne, χ_sq := hχ, hχ := hL }
⊢ 0 < B.F ↑(-2)
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k) * ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k) / ↑(2 * k)! * ↑(bernoulliFun (2 * k) x))
⊢ ↑2 = 2

Tactic:
norm_cast

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
x : ℝ
hx : x ∈ Icc 0 1
this :
  HasSum (fun n ↦ 1 / ↑n ^ (2 * k + 1) * ((fourier ↑n) ↑x - (fourier (-↑n)) ↑x))
    ((-1) ^ (k + 1) * I * (2 * ↑π) ^ (2 * k + 1) / ↑(2 * k + 1)! * ↑(bernoulliFun (2 * k + 1) x))
⊢ ↑2 = 2

Tactic:
norm_cast

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

Goal state before:
pp: case inl
q : ℕ
a : ZMod q
inst✝ : NeZero q
hs : 1 ∈ {s | 1 ≤ s.re}
⊢ 1 ∈ {s | s = 1 ∨ ∀ (χ : DirichletCharacter ℂ q), LFunction χ s ≠ 0}

Tactic:
simp only [ne_eq, Set.mem_ofPred_eq, true_or]

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

Goal state before:
pp: q : ℕ
a : ZMod q
inst✝ : NeZero q
ha : IsUnit a
x : ℝ
hx : 1 < x
⊢ 1 < ↑(↑x).re

Tactic:
norm_cast

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

Goal state before:
pp: 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
x : ℝ
hx : 1 < x
n : ℕ
hn : n > 0
⊢ 1 ≤ ↑n

Tactic:
norm_cast

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case a
k : ℕ
hk : k ≠ 0
| 2

Tactic:
rw [← pow_one (2 : ℝ)]

Goal state after:
case a
k : ℕ
hk : k ≠ 0
| 2 ^ 1
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_6
⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 * 1 - 1) * π ^ (2 * 1) * ↑(bernoulli (2 * 1)) / ↑(2 * 1)!

Tactic:
rw [mul_one]

Goal state after:
case e'_6
⊢ π ^ 2 / 6 = (-1) ^ (1 + 1) * 2 ^ (2 - 1) * π ^ 2 * ↑(bernoulli 2) / ↑2!
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
⊢ ↑↑a ≠ 0

Tactic:
norm_cast

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ ↑↑a = ↑a

Tactic:
norm_cast

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

Goal state before:
pp: case inl
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

pp: case inr
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b ≠ 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

Tactic:
· rw [hb, zero_right] at h; cases h

Goal state after:
case inr
a : ℤ
b : ℕ
h : J(a | b) = 0
hb : b ≠ 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr.refine_2
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
⊢ Set.Icc z 1 ⊆ {y | ∃ x, ∃ (_ : x ∈ ↑t), (if hi' : v x ≤ ↑↑z then z else Units.mk0 ⟨v x, ⋯⟩ ⋯) = y}

Tactic:
intro i

Goal state after:
case inr.refine_2
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 : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
⊢ i ∈ Set.Icc z 1 → i ∈ {y | ∃ x, ∃ (_ : x ∈ ↑t), (if hi' : v x ≤ ↑↑z then z else Units.mk0 ⟨v x, ⋯⟩ ⋯) = y}
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case inr.refine_2
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 : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
⊢ i ∈ Set.Icc z 1 → i ∈ {y | ∃ x, ∃ (_ : x ∈ ↑t), (if hi' : v x ≤ ↑↑z then z else Units.mk0 ⟨v x, ⋯⟩ ⋯) = y}

Tactic:
simp only [Set.mem_Icc, Finset.mem_coe, exists_prop, Set.mem_ofPred_eq, and_imp]

Goal state after:
case inr.refine_2
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 : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
⊢ z ≤ i → i ≤ 1 → ∃ x ∈ t, (if hi' : v x ≤ ↑↑z then z else Units.mk0 ⟨v x, ⋯⟩ ⋯) = i
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
h : Prime (mersenne p)
⊢ Prime p

Tactic:
by
  apply Nat.prime_of_pow_sub_one_prime _ h |>.2
  rintro rfl
  apply Nat.not_prime_one h

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

Goal state before:
pp: case refine_2
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
x✝ : CompleteSpace ↥𝒪[K] ∧ IsDiscreteValuationRing ↥𝒪[K] ∧ Finite 𝓀[K]
left✝¹ : CompleteSpace ↥𝒪[K]
left✝ : IsDiscreteValuationRing ↥𝒪[K]
h : TotallyBounded Set.univ
⊢ IsCompact Set.univ

Tactic:
rw [isCompact_iff_totallyBounded_isComplete]

Goal state after:
case refine_2
K : Type u_1
Γ₀ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : Valued K Γ₀
inst✝ : v.RankOne
x✝ : CompleteSpace ↥𝒪[K] ∧ IsDiscreteValuationRing ↥𝒪[K] ∧ Finite 𝓀[K]
left✝¹ : CompleteSpace ↥𝒪[K]
left✝ : IsDiscreteValuationRing ↥𝒪[K]
h : TotallyBounded Set.univ
⊢ TotallyBounded Set.univ ∧ IsComplete Set.univ
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
p : ℕ
hp : p ≠ 0
n✝ : ℕ
⊢ 2 ^ p - 1 ≠ 0

Tactic:
exact mersenne_int_ne_zero p hp

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: p : ℤ[X]
hp : p ≠ 0
⊢ 1 ≤ ‖↑p.leadingCoeff‖

Tactic:
norm_cast

Goal state after:
p : ℤ[X]
hp : p ≠ 0
⊢ 1 ≤ |p.leadingCoeff|
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case mpr
p : ℕ
w : 1 < p
⊢ sMod p (p - 2) = 0 → ↑(sMod p (p - 2)) = 0

Tactic:
· intro h
    rw [h]
    simp

Goal state after:
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ (↑(Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋)).ncard = ∏ i, (⌊B₂ i⌋ - ⌈B₁ i⌉ + 1).toNat

Tactic:
norm_cast

Goal state after:
n : ℕ
B₁ B₂ : Fin (n + 1) → ℝ
⊢ (Finset.Icc (fun x ↦ ⌈B₁ x⌉) fun x ↦ ⌊B₂ x⌋).card = ∏ x, (⌊B₂ x⌋ - ⌈B₁ x⌉ + 1).toNat
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
i : Fin (n + 1)
x✝ : i ∈ Finset.univ
⊢ 2 * ↑⌊↑(n.choose ↑i) * ↑B⌋₊ + 1 = 2 * ↑⌊↑(n.choose ↑i) * B⌋₊ + 1

Tactic:
norm_cast

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
⊢ ωb * ω = 1

Tactic:
by
  rw [mul_comm, ω_mul_ωb]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
w✝ : ℕ
h✝ : q = 2 * w✝ + 1
leg : ↑(legendreSym q 2) = ↑2 ^ (q / 2)
⊢ 2 = ↑2

Tactic:
norm_cast

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
pow2 : 2 ^ ((q + 1) / 2) = 2
this : 2 * ω ^ ((q + 1) / 2) = 2 * -1
coe : 2 = (ZMod.castHom ⋯ (X q)) 2
⊢ 2 * ↑((q + 1) / 2) = 1

Tactic:
norm_cast

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
pow2 : 2 ^ ((q + 1) / 2) = 2
this : 2 * ω ^ ((q + 1) / 2) = 2 * -1
coe : 2 = (ZMod.castHom ⋯ (X q)) 2
⊢ ↑(2 * ((q + 1) / 2)) = 1
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: x✝ : SL(2, ℤ)
⊢ x✝ ∈ Γ(1) ↔ x✝ ∈ ⊤

Tactic:
simp [eq_iff_true_of_subsingleton]

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

Goal state before:
pp: H K : Subgroup SL(2, ℤ)
h : H ≤ K
h2 : IsCongruenceSubgroup H
⊢ IsCongruenceSubgroup K

Tactic:
obtain ⟨N, hN⟩ := h2

Goal state after:
H K : Subgroup SL(2, ℤ)
h : H ≤ K
N : ℕ
hN : N ≠ 0 ∧ Γ(N) ≤ H
⊢ IsCongruenceSubgroup K
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
⊢ ∃ a, a • w = ![1, 0]

Tactic:
have : w 0 ≠ 0 := fun h ↦ hw <| funext <| by simp_all

Goal state after:
case pos
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : DecidableEq K
w : Fin 2 → K
hw : w ≠ 0
h₀ : w 1 = 0
this : w 0 ≠ 0
⊢ ∃ a, a • w = ![1, 0]
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: ι : Type u_1
inst✝¹ : Fintype ι
inst✝ : Nonempty ι
k : ℤ
g : GL (Fin 2) ℝ
f : ι → ℍ → ℂ
this : 0 < Fintype.card ι
⊢ (∏ i, f i) ∣[k * ↑(Fintype.card ι)] g = |↑(Matrix.GeneralLinearGroup.det g)| ^ (Fintype.card ι - 1) • ∏ i, f i ∣[k] g

Tactic:
simpa [← zpow_natCast, this] using ModularForm.prod_slash (s := (.univ : Finset ι))

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
x✝ : Fin 2 → ℝ
⊢ ↑(Function.eval 0 x✝) * ↑z + ↑(Function.eval 1 x✝) * 1 = ↑(x✝ 0) * ↑z + ↑(x✝ 1)

Tactic:
rw [mul_one]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ↑(cd 0) ^ 2 + (-↑(cd 1)) ^ 2 ≠ 0

Tactic:
norm_cast

Goal state after:
g : SL(2, ℤ)
z : ℍ
cd : Fin 2 → ℤ
hcd : IsCoprime (cd 0) (cd 1)
⊢ ¬cd 0 ^ 2 + (-cd 1) ^ 2 = 0
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
a b : GradedMonoid (ModularForm Γ)
h : a.fst = b.fst
h2 : mcast h a.snd ⋯ = b.snd
⊢ a = b

Tactic:
obtain ⟨i, a⟩ := a

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
b : GradedMonoid (ModularForm Γ)
i : ℤ
a : ModularForm Γ i
h : ⟨i, a⟩.fst = b.fst
h2 : mcast h ⟨i, a⟩.snd ⋯ = b.snd
⊢ ⟨i, a⟩ = b
Module: Mathlib.NumberTheory.ModularForms.Basic

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

Tactic:
intro i

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

Goal state before:
pp: z : ℍ
⊢ (T • z).im = z.im

Tactic:
simpa using im_T_zpow_smul z 1

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

Goal state before:
pp: k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ 2 < ↑k

Tactic:
norm_cast

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
A : SL(2, ℤ)
z : ℍ
hz : 2 ≤ z.im
n : ℤ
hn : ModularGroup.T ^ (↑N * n) • z ∈ verticalStrip (↑N) z.im
⊢ 2 < ↑k

Tactic:
norm_cast

Goal state after:
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 ^ 2 / (τ.im ^ (↑k / 2)) ^ 2

Tactic:
Real.sq_sqrt ((norm_nonneg _).trans 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 ≤ C / (τ.im ^ (↑k / 2)) ^ 2
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence

Goal state before:
pp: k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
⊢ 2 < ↑k

Tactic:
norm_cast

Goal state after:
Module: Mathlib.NumberTheory.TsumDivisorsAntidiagonal

Goal state before:
pp: case hbc
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : NormSMulClass ℤ 𝕜
k : ℕ
r : 𝕜
hr : ‖r‖ < 1
b : ℕ+
⊢ ↑(↑b).divisors.card ≤ ‖↑↑b‖

Tactic:
simpa using! Nat.card_divisors_le_self b

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

Goal state before:
pp: z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
hn0 : ↑n ≠ 0
⊢ ↑n + 1 ≠ 0

Tactic:
norm_cast

Goal state after:
z : ℍ
b n : ℤ
h : b = 0 → ¬n = 0
hb : b = 0
hn : ¬n = -1
hn0 : ↑n ≠ 0
⊢ ¬n + 1 = 0
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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 = 0 ∨ ↑g 1 0 = 1
⊢ (g • z).im = z.im

Tactic:
rcases hc with hc | hc

Goal state after:
case inl
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 = 0
⊢ (g • z).im = z.im

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
⊢ (g • z).im = z.im
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k b : ℕ
hb : 1 ≤ b
⊢ 1 ≤ 1 * ↑b ^ 1

Tactic:
norm_cast

Goal state after:
k b : ℕ
hb : 1 ≤ b
⊢ 1 ≤ 1 * b ^ 1
Module: Mathlib.NumberTheory.ModularForms.Discriminant

Goal state before:
pp: k : ℤ
f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
⊢ (fun τ ↦ rexp (-2 * π * τ.im / 1)) =O[atImInfty] Δ

Tactic:
simpa using exp_isBigO_discriminant

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

Goal state before:
pp: ⊢ 1 + 0 = 1

Tactic:
norm_cast

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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 = 0 ∨ ↑g 1 0 = 1
⊢ (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:
rcases hc with hc | hc

Goal state after:
case 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 = 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 = ρ

case inr
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
⊢ (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 = ρ
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℍ
this : ModularGroup.T ^ 2 = ModularGroup.T ^ 2
⊢ ↑↑2 + ↑τ = 2 + ↑τ

Tactic:
norm_cast

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

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

Tactic:
norm_cast

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

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

Tactic:
have := cases_of_mem_fd_smul_mem_fd ρ_mem_fd (hg ▸ ρ_mem_fd)

Goal state after:
case mp
g : SL(2, ℤ)
hg : g • ρ = ρ
neS : g ≠ S ∧ g ≠ -S
neT : g ≠ T ∧ g ≠ -T ∧ g ≠ T⁻¹ ∧ g ≠ -T⁻¹
neTST : g ≠ T * S * T ∧ g ≠ -(T * S * T)
this :
  (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ ρ.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ ρ.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖↑ρ‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ ρ = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ ρ = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ ρ = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ ρ = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ ρ = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ ρ = ρ
⊢ g ∈ {1, -1, S * T, -(S * T), T⁻¹ * S, -(T⁻¹ * S)}