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

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ ‖↑((s - 1) * s)‖ * ‖∫ (t : ℝ) in Set.Ioi 1, (S t - l * ↑t) * ↑t ^ (-↑s - 1)‖ ≤
    (s - 1) * s * ∫ (t : ℝ) in Set.Ioi 1, ‖(S t - l * ↑t) * ↑t ^ (-↑s - 1)‖

Tactic:
norm_real,

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ ‖(s - 1) * s‖ * ‖∫ (t : ℝ) in Set.Ioi 1, (S t - l * ↑t) * ↑t ^ (-↑s - 1)‖ ≤
    (s - 1) * s * ∫ (t : ℝ) in Set.Ioi 1, ‖(S t - l * ↑t) * ↑t ^ (-↑s - 1)‖
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case neg
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
⊢ J(a % 2 | 2) * J(a | b) = J(a | b)

Tactic:
Int.emod_two_ne_zero.mp ha2,

Goal state after:
case neg
a : ℤ
ha2 : ¬a % 2 = 0
b : ℕ
IH : ∀ m < 2 * b, J(a | m) = fastJacobiSym a m
hb0 : ¬2 * b = 0
hb2 : 2 * b % 2 = 0
⊢ J(1 | 2) * J(a | b) = J(a | b)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: case e_a
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
t : ℝ
ht : 0 ≤ t
⊢ ‖S t - l * ↑t‖ * ‖↑(t ^ (-s - 1))‖ = ‖S t - l * ↑t‖ * t ^ (-s - 1)

Tactic:
norm_real,

Goal state after:
case e_a
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
t : ℝ
ht : 0 ≤ t
⊢ ‖S t - l * ↑t‖ * ‖t ^ (-s - 1)‖ = ‖S t - l * ↑t‖ * t ^ (-s - 1)
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 Γ
⊢ (∃ x, x ≠ 0 ∧ v x < 1) ↔ ∃ x, ¬IsUnit x ∧ ¬x = 0

Tactic:
Valuation.Integer.not_isUnit_iff_valuation_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) ↔ ∃ x, v ↑x < 1 ∧ ¬x = 0
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ (s - 1) * s * (Cs + ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1)) ≤
    (s - 1) * s * C + s * ((s - 1) * ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1))

Tactic:
rw [mul_add, ← mul_assoc, mul_comm s]

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
h₃ : (↑s - 1) * ∫ (t : ℝ) in Set.Ioi 1, ↑t ^ (-↑s) = 1
Cs : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
h₄ : Cs ≤ C
⊢ (s - 1) * s * Cs + (s - 1) * s * ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤
    (s - 1) * s * C + (s - 1) * s * ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1)
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: case inl
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n = 0
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

pp: case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n ≠ 0
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1

Tactic:
· simp [hn]

Goal state after:
case inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Algebra R ℂ
n : ℕ
hn : n ≠ 0
⊢ (map (algebraMap R ℂ) (cyclotomic n R)).mahlerMeasure = 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ω ^ (2 ^ i * 2) + ωb ^ (2 ^ i * 2) = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1)

Tactic:
_root_.pow_succ

Goal state after:
q i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ω ^ (2 ^ i * 2) + ωb ^ (2 ^ i * 2) = ω ^ (2 ^ i * 2) + ωb ^ (2 ^ i * 2)
Module: Mathlib.NumberTheory.LucasLehmer

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

Tactic:
by
  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.NumberTheory.ModularForms.Cusps

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.strictPeriods ≤ 𝒢.periods

Tactic:
intro k
  simp only [Subgroup.periods, strictPeriods]
  apply 𝒢.le_adjoinNegOne

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

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

Tactic:
simp [hf]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case «0»
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
⊢ c 0 * ((↑z).im⁻¹ * (↑z).im) = c 0

Tactic:
inv_mul_cancel₀ hz,

Goal state after:
case «0»
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
⊢ c 0 * 1 = c 0
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : f (-1 • z) = denom (-1) ↑z ^ k * f z
⊢ f z = 0 z

Tactic:
rw [neg_smul, one_smul, denom_neg, denom_one, hk.neg_one_zpow] at hf

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
inst✝ : Γ.HasDetOne
h_neg_one : -1 ∈ Γ
hk : Odd k
f : ModularForm Γ k
z : ℍ
hf : f z = -1 * f z
⊢ f z = 0 z
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
τ : ℍ
⊢ (cuspFunction h f ∘ fun τ ↦ 𝕢 h ↑τ) τ = f τ

Tactic:
simpa using eq_cuspFunction τ hh.ne' hfper

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

Goal state before:
pp: case h.right
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
i : Fin 2
⊢ (↑r * x / ↑r) i = x i

Tactic:
simp_all [NeZero.ne r]

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

Goal state before:
pp: k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x ↦ ‖↑x‖ ^ (-k)
⊢ TendstoLocallyUniformly (fun s x ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1) x) (fun x ↦ eisensteinSeries a k x) Filter.atTop

Tactic:
simp only [tendstoLocallyUniformly_iff_forall_isCompact, eisensteinSeries]

Goal state after:
k : ℤ
hk : 3 ≤ k
N : ℕ
a : Fin 2 → ZMod N
hk' : 2 < ↑k
p_sum : Summable fun x ↦ ‖↑x‖ ^ (-k)
⊢ ∀ (K : Set ℍ),
    IsCompact K →
      TendstoUniformlyOn (fun s x ↦ ∑ x_1 ∈ s, eisSummand k (↑x_1) x)
        (fun x ↦ ∑' (x_1 : ↑(gammaSet N 1 a)), eisSummand k (↑x_1) x) Filter.atTop K
Module: Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
⊢ (fun x ↦ 2⁻¹ * ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) =ᶠ[atTop] fun x ↦ ‖f x‖

Tactic:
filter_upwards [eventually_ge_atTop 1] with x hx

Goal state after:
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hs : Function.Even f
L : F
hL : Tendsto (fun x ↦ ∑ b ∈ Icc (-x) x, f b) atTop (𝓝 L)
this : Tendsto (fun x ↦ ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖) atTop (𝓝 0)
x : ℤ
hx : 1 ≤ x
⊢ 2⁻¹ * ‖∑ b ∈ Icc (-x) x, f b - ∑ b ∈ Icc (-(x - 1)) (x - 1), f b‖ = ‖f x‖
Module: Mathlib.NumberTheory.Modular

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

Tactic:
rcases (abs_eq one_half_pos.le).mp hzre with hzre | hzre

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

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

Goal state before:
pp: ⊢ DifferentiableOn ℂ (E2 ∘ ↑ofComplex) {z | 0 < z.im}

Tactic:
have hη : DifferentiableOn ℂ η _ := fun z hz ↦
    (differentiableAt_eta_of_mem_upperHalfPlaneSet hz).differentiableWithinAt

Goal state after:
hη : DifferentiableOn ℂ η upperHalfPlaneSet
⊢ DifferentiableOn ℂ (E2 ∘ ↑ofComplex) {z | 0 < z.im}
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (1 +ᵥ ρ) ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this✝² : ↑g 0 1 = -↑g 0 0 - 1
hgeq : g = T ^ ↑g 0 0 * S * T⁻¹
hnorm : normSq ↑z + (-2 * z.re + 1) ≤ 1
this✝¹ : normSq (↑z - 1) = normSq ↑z + (-2 * z.re + 1)
h : normSq ↑z = 1
h' : z.re = 1 / 2
hρ : z = 1 +ᵥ ρ
this✝ : S • ρ = T • ρ
this : (S * T⁻¹) • (1 +ᵥ ρ) = 1 +ᵥ ρ
⊢ -1 ≤ ↑(↑g 0 0) ∧ ↑g 0 0 ≤ 0

Tactic:
simpa only [ρ, neg_div, one_div, ← coe_re, coe_T_zpow_smul_eq, coe_vadd, add_re, ofReal_re,
      show 1 + (-2⁻¹ : ℝ) = 2⁻¹ by norm_num, intCast_re, abs_le, ← sub_le_iff_le_add',
      show (-2⁻¹ : ℝ) - (2⁻¹ : ℝ) = -1 by norm_num, add_le_iff_nonpos_right, Int.cast_nonpos] using
      hg.2

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

Goal state before:
pp: case e'_5
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
x✝ : ℕ
⊢ (if x✝ + 1 = 0 then 1 else -24 * ↑((σ 1) (x✝ + 1))) • cexp (2 * ↑π * I * ↑z) ^ (x✝ + 1) =
    -24 * (↑((σ 1) (x✝ + 1)) * cexp (2 * ↑π * I * ↑z) ^ (x✝ + 1))

Tactic:
simp [mul_assoc]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: 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 = ρ

pp: 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 = ρ

Tactic:
· grind [cases_c_zero hz hg hc]

Goal state after:
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.Modular

Goal state before:
pp: case mpr
g : SL(2, ℤ)
⊢ (S * T) • ρ = ρ ∧ S • ρ = T • ρ

Tactic:
← eq_inv_smul_iff (g := S),

Goal state after:
case mpr
g : SL(2, ℤ)
⊢ (S * T) • ρ = ρ ∧ ρ = S⁻¹ • T • ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
H0 :
  (fun n ↦ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑n / ↑z - ↑↑m) + 1 / (-↑↑n / ↑z + ↑↑m))) = fun n ↦
    -2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑n / ↑z)) ^ ↑m + 2 / ↑↑n
⊢ Tendsto (fun x ↦ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑x / ↑z - ↑↑m) + 1 / (-↑↑x / ↑z + ↑↑m))) atTop (𝓝 (-2 * ↑π * I / ↑z))

Tactic:
H0

Goal state after:
z : ℍ
H0 :
  (fun n ↦ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑n / ↑z - ↑↑m) + 1 / (-↑↑n / ↑z + ↑↑m))) = fun n ↦
    -2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑n / ↑z)) ^ ↑m + 2 / ↑↑n
⊢ Tendsto
    (fun n ↦ -2 * ↑π * I / ↑z - 2 / ↑z * (2 * ↑π * I) * ∑' (m : ℕ+), cexp (2 * ↑π * I * (-↑↑n / ↑z)) ^ ↑m + 2 / ↑↑n)
    atTop (𝓝 (-2 * ↑π * I / ↑z))
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⟩
    exact ⟨hz.le, h.2, h.1.2, by simpa [Complex.normSq_eq_norm_sq] using h.1.1⟩

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

Goal state before:
pp: ⊢ (PowerSeries.coeff 1) (qExpansion 1 ⇑E₄CubeSubE₆SqForm) = 1728

Tactic:
rw [E₄CubeSubE₆SqForm_qExpansion_eq]

Goal state after:
⊢ (PowerSeries.coeff 1) (qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ - qExpansion 1 ⇑E₆ * qExpansion 1 ⇑E₆) =
    1728
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)‖ / (2 * ↑i / h Γ) ^ s.re

Tactic:
simp_rw [mul_comm (2 : ℝ), mul_div_assoc,
      Real.mul_rpow (Nat.cast_nonneg _) (show 0 ≤ 2 / h Γ by positivity), ← div_div]
    apply Summable.div_const
    apply summable_of_isBigO_nat (Real.summable_nat_rpow.mpr <| show r - s.re < -1 by linarith)
    simp only [Real.rpow_sub' (Nat.cast_nonneg _) (show r - s.re ≠ 0 by linarith)]
    apply IsBigO.mul _ (isBigO_refl _ _)
    simpa using hcoeff.norm_left

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 (x i)
Q : Set ((i : ι) → R i) := univ.pi fun i ↦ if i ∈ S then A i else K i
Q_def : Q = univ.pi fun i ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi K
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
have U_nhds : U ∈ 𝓝 (x : Π i, R i) := set_pi_mem_nhds hS fun i _ ↦ hK i

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 (x i)
Q : Set ((i : ι) → R i) := univ.pi fun i ↦ if i ∈ S then A i else K i
Q_def : Q = univ.pi fun i ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi K
U_nhds : U ∈ 𝓝 ⇑x
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: case refine_1
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 (x i)
Q : Set ((i : ι) → R i) := univ.pi fun i ↦ if i ∈ S then A i else K i
Q_def : Q = univ.pi fun i ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi K
U_nhds : U ∈ 𝓝 ⇑x
QU : DFunLike.coe ⁻¹' U ⊆ DFunLike.coe ⁻¹' Q
⊢ (univ.pi fun i ↦ if i ∈ S then A i else K i) ⊆ S.pi A

Tactic:
pi_if,

Goal state after:
case refine_1
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 (x i)
Q : Set ((i : ι) → R i) := univ.pi fun i ↦ if i ∈ S then A i else K i
Q_def : Q = univ.pi fun i ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi K
U_nhds : U ∈ 𝓝 ⇑x
QU : DFunLike.coe ⁻¹' U ⊆ DFunLike.coe ⁻¹' Q
⊢ {i | i ∈ univ ∧ i ∈ S}.pi A ∩ {i | i ∈ univ ∧ i ∉ S}.pi K ⊆ S.pi A
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ padicValNat p (x ^ n - y ^ n) = padicValNat p (x - y) + padicValNat p n

Tactic:
← Nat.cast_inj (R := ℕ∞),

Goal state after:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ ↑(padicValNat p (x ^ n - y ^ n)) = ↑(padicValNat p (x - y) + padicValNat p n)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ padicValNat p (x ^ n + (y + 1) ^ n) = padicValNat p (x + (y + 1)) + padicValNat p n

Tactic:
← Nat.cast_inj (R := ℕ∞),

Goal state after:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ ↑(padicValNat p (x ^ n + (y + 1) ^ n)) = ↑(padicValNat p (x + (y + 1)) + padicValNat p n)