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

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ (1 / (1 - 0)) • ∫ (x : ℝ) in 0..1, (fourier (-0)) ↑x • ↑(bernoulliFun k x) = 0

Tactic:
neg_zero,

Goal state after:
k : ℕ
hk : k ≠ 0
⊢ (1 / (1 - 0)) • ∫ (x : ℝ) in 0..1, (fourier 0) ↑x • ↑(bernoulliFun k x) = 0
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: case inl
⊢ riemannZeta (-0) = -↑(bernoulli' (0 + 1)) / (0 + 1)

Tactic:
neg_zero,

Goal state after:
case inl
⊢ riemannZeta 0 = -↑(bernoulli' (0 + 1)) / (0 + 1)
Module: Mathlib.NumberTheory.LSeries.HurwitzZetaValues

Goal state before:
pp: k : ℕ
hk : k ≠ 0
⊢ k + 1 ≠ 1

Tactic:
by simp [hk]

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

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Odd Φ
s : ℂ
hs : 1 < s.re
⊢ (∑ x, Φ x * expZeta (toAddCircle x) s) / (2 * I) - (∑ x, Φ x * expZeta (toAddCircle (-x)) s) / (2 * I) =
    (∑ x, Φ (-x) * expZeta (toAddCircle (-x)) s) / ?m.227 - ?m.229

Tactic:
by
    congrm ?_ / _ - _
    exact (Fintype.sum_equiv (.neg _) _ _ fun x ↦ by rfl).symm

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

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
⊢ ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m

Tactic:
intro x hx

Goal state after:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
x : ℝ
hx : x ≥ y
⊢ (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
Module: Mathlib.NumberTheory.LSeries.Nonvanishing

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
B : BadChar N
s : ℂ
hs : 1 < s.re
⊢ Function.update (fun s ↦ riemannZeta s * LFunction B.χ s) 1 (deriv (LFunction B.χ) 1) s =
    LSeries (⇑↑zeta) s * LSeries (⇑(toArithmeticFunction fun x ↦ B.χ ↑x)) s

Tactic:
have hs' : s ≠ 1 := fun h ↦ by simp only [h, one_re, lt_self_iff_false] at hs
    simp only [ne_eq, hs', not_false_eq_true, Function.update_of_ne, B.χ.LFunction_eq_LSeries hs]
    congr 1
    · simp_rw [← LSeries_zeta_eq_riemannZeta hs, ← natCoe_apply]
    · exact LSeries_congr B.χ.apply_eq_toArithmeticFunction_apply s

Goal state after:
Module: Mathlib.NumberTheory.ZetaValues

Goal state before:
pp: case e'_3.e_a
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))
ofReal_two : ↑2 = 2
n : ℕ
⊢ ((fourier ↑n) ↑x + (fourier (-↑n)) ↑x) / 2 = ↑(Real.cos (2 * π * ↑n * x))

Tactic:
rw [ofReal_cos, ofReal_mul, fourier_coe_apply, fourier_coe_apply, cos, ofReal_one, div_one,
        div_one, ofReal_mul, ofReal_mul, ofReal_two, Int.cast_neg, Int.cast_natCast,
        ofReal_natCast]
      congr 3
      · ring
      · ring

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

Goal state before:
pp: hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
this : Summable fun pk ↦ (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)
pk : Nat.Primes × ℕ
⊢ 0 ≤ F'' pk

Tactic:
simp only [F'', Function.comp_apply, F', F₀, Prod.map_fst, id_eq, Prod.map_snd, Nat.cast_pow]

Goal state after:
hp₀ : ∀ (p : Nat.Primes), 0 < (↑↑p)⁻¹
hp₁ : ∀ (p : Nat.Primes), (↑↑p)⁻¹ < 1
this : Summable fun pk ↦ (↑↑pk.1)⁻¹ ^ (↑pk.2 + 3 / 2)
pk : Nat.Primes × ℕ
⊢ 0 ≤ (if Nat.Prime (↑pk.1 ^ (pk.2 + 1 + 1)) then 0 else Λ (↑pk.1 ^ (pk.2 + 1 + 1))) / ↑↑pk.1 ^ (pk.2 + 1 + 1)
Module: Mathlib.NumberTheory.LSeries.PrimesInAP

Goal state before:
pp: case refine_1
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
hFF' : F₀ ∘ Subtype.val = F' ∘ ⇑prodNatEquiv.symm
⊢ Summable (F' ∘ ⇑prodNatEquiv.symm)

Tactic:
refine (Nat.Primes.prodNatEquiv.symm.summable_iff (f := F')).mpr ?_

Goal state after:
case refine_1
q : ℕ
a : ZMod q
h₀ : ∀ (n : ℕ), 0 ≤ (if Nat.Prime n then 0 else residueClass a n) / ↑n
hleF₀ : ∀ (n : ℕ), (if Nat.Prime n then 0 else residueClass a n) / ↑n ≤ F₀ n
hF₀ : ∀ (p : Nat.Primes), F₀ ↑p = 0
hFF' : F₀ ∘ Subtype.val = F' ∘ ⇑prodNatEquiv.symm
⊢ Summable F'
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
⊢ Tendsto (fun x ↦ ∑' (m : ℕ), F x m) atTop (nhds 0)

Tactic:
show (0 : ℂ) = tsum (fun _ : ℕ ↦ 0) from tsum_zero.symm

Goal state after:
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x ↦ {m | n + 1 < m}.indicator fun m ↦ f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m ↦ (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
hys : Summable (F y)
hc : ∀ (k : ℕ), Tendsto (fun x ↦ F x k) atTop (nhds 0)
⊢ Tendsto (fun x ↦ ∑' (m : ℕ), F x m) atTop (nhds (∑' (x : ℕ), 0))
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha' : abscissaOfAbsConv F < ⊤
⊢ Tendsto (fun x ↦ LSeries f ↑x) atTop (nhds (f 1))

Tactic:
← LSeries_congr hF

Goal state after:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha' : abscissaOfAbsConv F < ⊤
⊢ Tendsto (fun x ↦ LSeries F ↑x) atTop (nhds (f 1))
Module: Mathlib.NumberTheory.LSeries.Injectivity

Goal state before:
pp: f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha' : abscissaOfAbsConv F < ⊤
⊢ Tendsto (fun x ↦ LSeries f ↑x) atTop (nhds (f 1))

Tactic:
simp_rw [← LSeries_congr hF]

Goal state after:
f : ℕ → ℂ
ha : abscissaOfAbsConv f < ⊤
F : ℕ → ℂ := fun n ↦ if n = 0 then 0 else f n
hF₀ : F 0 = 0
hF : ∀ {n : ℕ}, n ≠ 0 → F n = f n
ha' : abscissaOfAbsConv F < ⊤
⊢ Tendsto (fun x ↦ LSeries F ↑x) atTop (nhds (f 1))
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
n : ℕ
⊢ residueClass a n / ↑n =
    (if Nat.Prime n then 0 else residueClass a n) / ↑n + (if Nat.Prime n then residueClass a n else 0) / ↑n

Tactic:
simp only [← add_div, ite_add_ite, zero_add, add_zero, ite_self]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
⊢ ∀ x ∈ Ico 1 (p / 2).succ, (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ

Tactic:
intro x hx

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
a : ZMod p
hap : a ≠ 0
he : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x ≠ 0 ∧ x ≤ p / 2
hep : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → x < p
hpe : ∀ {x : ℕ}, x ∈ Ico 1 (p / 2).succ → ¬p ∣ x
x : ℕ
hx : x ∈ Ico 1 (p / 2).succ
⊢ (a * ↑x).valMinAbs.natAbs ∈ Ico 1 (p / 2).succ
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
h' : ϖ = 0
⊢ span {ϖ} = ⊥

Tactic:
h',

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
h' : ϖ = 0
⊢ span {0} = ⊥
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ ε * ((s - 1) * ∫ (t : ℝ) in Set.Ioi 1, t ^ (-s)) = ε

Tactic:
by
      rw [integral_Ioi_rpow_of_lt (by rwa [neg_lt_neg_iff]) zero_lt_one, Real.one_rpow]
      field [show -s + 1 ≠ 0 by linarith]

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

Goal state before:
pp: case inr.inr.inr
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc : IsCompact ↑𝒪[K]
this✝ : ∀ (z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ), (Set.Icc z 1).Finite
x y : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
hxy : x < y
this : (Set.Icc y⁻¹ x⁻¹).Finite
h : 1 < x
a✝ : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
⊢ a✝ ∈ Set.Icc x y → a✝ ∈ Set.Icc x⁻¹⁻¹ y⁻¹⁻¹

Tactic:
simp +contextual

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

Goal state before:
pp: case ind.isFalse.isTrue
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
⊢ (if (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) = true then -J(↑a / 2 | b) else J(↑a / 2 | b)) =
    if flip = true then -if b % 8 = 3 ∨ b % 8 = 5 then -J(↑a / 2 | b) else J(↑a / 2 | b)
    else if b % 8 = 3 ∨ b % 8 = 5 then -J(↑a / 2 | b) else J(↑a / 2 | b)

Tactic:
by_cases h : b % 8 = 3 ∨ b % 8 = 5 <;> simp [h]

Goal state after:
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)
Module: Mathlib.NumberTheory.LocalField.Basic

Goal state before:
pp: case inr
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r : ValueGroupWithZero K
hr✝ : r ≠ 0
hrs : {x | (valuation K) x < r} ⊆ s
r' : K
hr' : ¬r' = 0
hr : (valuation K) r' < 1
hr1 : 1 ≤ r
⊢ {x | (valuation K) x ≤ (valuation K) r'} ⊆ {x | (valuation K) x < r}

Tactic:
intro x hx

Goal state after:
case inr
K : Type u_1
inst✝³ : Field K
inst✝² : ValuativeRel K
inst✝¹ : TopologicalSpace K
inst✝ : IsNonarchimedeanLocalField K
γ : K
hγ : ¬γ = 0
this✝ : UniformSpace K := IsTopologicalAddGroup.rightUniformSpace K
this : IsUniformAddGroup K := isUniformAddGroup_of_addCommGroup
s : Set K
hs : s ∈ nhds 0
hs' : IsCompact s
r : ValueGroupWithZero K
hr✝ : r ≠ 0
hrs : {x | (valuation K) x < r} ⊆ s
r' : K
hr' : ¬r' = 0
hr : (valuation K) r' < 1
hr1 : 1 ≤ r
x : K
hx : x ∈ {x | (valuation K) x ≤ (valuation K) r'}
⊢ x ∈ {x | (valuation K) x < r}
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
w : 1 < p
⊢ sZMod p (p - 2) = 0 ↔ sMod p (p - 2) = 0

Tactic:
rw [sZMod_eq_sMod p]

Goal state after:
p : ℕ
w : 1 < p
⊢ ↑(sMod p (p - 2)) = 0 ↔ sMod p (p - 2) = 0
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ (2 * ω) ^ ((q + 1) / 2) = -2

Tactic:
rw [← one_add_α_sq, ← pow_mul]

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ (1 + α) ^ (2 * ((q + 1) / 2)) = -2
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
⊢ 2 ^ ((q + 1) / 2) = 2

Tactic:
obtain ⟨_, _⟩ := odd

Goal state after:
q : ℕ
inst✝ : Fact (Nat.Prime q)
leg3 : legendreSym q 3 = -1
leg2 : legendreSym q 2 = 1
w✝ : ℕ
h✝ : q = 2 * w✝ + 1
⊢ 2 ^ ((q + 1) / 2) = 2
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
⊢ Γ.HasDetPlusMinusOne

Tactic:
hasDetPlusMinusOne_iff_abs_det

Goal state after:
n : Type u_1
inst✝¹ : Fintype n
inst✝ : DecidableEq n
Γ : Subgroup (GL (Fin 2) ℝ)
h : Γ.IsArithmetic
⊢ ∀ {g : GL (Fin 2) ℝ}, g ∈ Γ → |↑(GeneralLinearGroup.det g)| = 1
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
h : ↑g 1 0 * c + ↑g 1 1 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ∞ = ↑c

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
h : ¬↑g 1 0 * c + ↑g 1 1 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑((↑g 0 0 * c + ↑g 0 1) / (↑g 1 0 * c + ↑g 1 1)) = ↑c

Tactic:
· refine ⟨fun hg ↦ (g.det_ne_zero ?_).elim, fun hg ↦ (infty_ne_coe _ hg).elim⟩
    rw [det_fin_two]
    grind

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
h : ¬↑g 1 0 * c + ↑g 1 1 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑((↑g 0 0 * c + ↑g 0 1) / (↑g 1 0 * c + ↑g 1 1)) = ↑c
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
inst✝ : NeZero 2
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
c : K
hc : ↑g 1 0 = 0
hd : ↑g 1 1 = ↑g 0 0
this : ↑g 0 1 ≠ 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑c = g.parabolicFixedPoint

Tactic:
simpa [parabolicFixedPoint, hc, hd]

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

Goal state before:
pp: β : Type u_1
G : Type u_2
α : Type u_3
inst✝² : Group G
inst✝¹ : AddGroup α
inst✝ : SlashAction β G α
k : β
g : G
a : α
⊢ a = 0 → a ∣[k] g = 0

Tactic:
simp +contextual

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

Goal state before:
pp: 𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
x✝ : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : n ≠ 0
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
⊢ c = g.parabolicFixedPoint

Tactic:
← hgp.smul_eq_self_iff

Goal state after:
𝒢 𝒢' : Subgroup (GL (Fin 2) ℝ)
h𝒢 : 𝒢' ≤ 𝒢
h𝒢' : 𝒢'.relIndex 𝒢 ≠ 0
c : OnePoint ℝ
x✝ : IsCusp c 𝒢
g : GL (Fin 2) ℝ
hg : g ∈ 𝒢
hgp : g.IsParabolic
hgc : g • c = c
n : ℕ
hn : n ≠ 0
hgn : g ^ n ∈ 𝒢' ⊓ 𝒢
⊢ g • c = c
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:
rw [← Rat.coe_castHom, OnePoint.map_smul, OnePoint.map_infty,
        ← (Rat.castHom ℝ).algebraMap_toAlgebra, map_mapGL]

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

Goal state before:
pp: ⊢ (mapGL ℝ).range.strictPeriods = AddSubgroup.zmultiples 1

Tactic:
simpa [MonoidHom.range_eq_map] using strictPeriods_eq_zmultiples_one_of_T_mem (mem_top _)

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

Tactic:
refine BoundedAtFilter.smul _ (BoundedAtFilter.prod (s := s) ?_)

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 ∈ s, atImInfty.BoundedAtFilter (⇑(F i) ∣[k i] γ)
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 : ι
hi : i ∈ s
⊢ atImInfty.BoundedAtFilter (⇑(F i) ∣[k i] γ)

Tactic:
simpa using! (F i).bdd_at_cusps' hc γ hγ

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
n : ℤ
⊢ (T ^ n • z).re = z.re + ↑n

Tactic:
rw [← coe_re, coe_T_zpow_smul_eq, add_re, intCast_re, coe_re]

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

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

Tactic:
intro x hx

Goal state after:
case refine_1
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 r 0
⊢ divIntMap (↑r) x ∈ gammaSet 1 1 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

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

Tactic:
intro x hx

Goal state after:
case refine_3
r : ℕ
inst✝ : NeZero r
x : Fin 2 → ℤ
hx : x ∈ gammaSet 1 1 0
⊢ x ∈ divIntMap ↑r '' gammaSet 1 r 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
hvr : v = r • (v / ↑r)
⊢ finGcdMap (v ᵥ* ↑A) = r

Tactic:
hvr,

Goal state after:
r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
hvr : v = r • (v / ↑r)
⊢ finGcdMap ((r • (v / ↑r)) ᵥ* ↑A) = r
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)
K : Set ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
⊢ 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

Tactic:
refine (tendstoUniformlyOn_tsum (hu := p_sum.mul_left <| r ⟨⟨A, B⟩, hB⟩ ^ (-k : ℝ))
    (fun p z hz ↦ ?_)).mono HABK

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 ℍ
hK : IsCompact K
A B : ℝ
hB : 0 < B
HABK : K ⊆ verticalStrip A B
p : ↑(gammaSet N 1 a)
z : ℍ
hz : z ∈ verticalStrip A B
⊢ ‖eisSummand k (↑p) z‖ ≤ r { coe := { re := A, im := B }, coe_im_pos := hB } ^ (-↑k) * ‖↑p‖ ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Defs

Goal state before:
pp: A B : SL(2, ℤ)
⊢ D2 (A * B) = D2 A ∣[2] B + D2 B

Tactic:
by
  ext z
  simp only [D2, mul_assoc, coe_mul, map_mul, ← mul_div, SL_slash_def,
    ModularGroup.sl_moeb, Int.reduceNeg, zpow_neg, Pi.add_apply, ← mul_add, mul_eq_mul_left_iff,
    I_ne_zero, or_false, ofReal_eq_zero, pi_ne_zero, OfNat.ofNat_ne_zero]
  have hd : (A.1 * B.1) 1 0 * denom (φ B) z - B 1 0 * denom (φ A * φ B) z = A 1 0 := by
    simpa [sub_eq_iff_eq_add] using denom_aux A B z
  have : denom A (num B z / denom B z) = denom A ↑(B • z) := by
    simp [specialLinearGroup_apply, denom, num]
  rw [(by intros; field_simp : ∀ {a b c d f e : ℂ} (he : e ≠ 0), a / b =
    c / d * (e ^ (2 : ℤ))⁻¹ + f / e ↔ a * e ^ 2 / b = c / d + e * f) (denom_ne_zero B z)]
  simp only [pow_two, ← mul_assoc, denom_cocycle A B z.im_ne_zero, this,
    ModularGroup.sl_moeb, ← hd]
  field_simp [denom_ne_zero A (toGL (φ B) • z)]
  ring

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 = ρ
⊢ S⁻¹ • T • ρ = ρ

Tactic:
inv_smul_eq_iff,

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 = ρ
⊢ T • ρ = S • ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
H : Summable fun m ↦ G2Term z m - δ m
⊢ ∀ (x : Fin 2 → ℤ), δ x = 0 x → (fun m ↦ G2Term z m - δ m) x = G2Term z x

Tactic:
simp +contextual

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (S * T⁻¹) • (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 • ρ
⊢ S⁻¹ • T⁻¹ • (1 +ᵥ ρ) = 1 +ᵥ ρ

Tactic:
inv_smul_eq_iff,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • (S * T⁻¹) • (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 • ρ
⊢ T⁻¹ • (1 +ᵥ ρ) = S • (1 +ᵥ ρ)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
⊢ EqOn (iteratedDeriv k fun s ↦ cexp (2 * ↑π * I * ↑m * s / ↑p))
    (fun s ↦ (2 * ↑π * I * ↑m / ↑p) ^ k * cexp (2 * ↑π * I * ↑m * s / ↑p)) S

Tactic:
intro x hx

Goal state after:
k m : ℕ
p : ℝ
S : Set ℂ
hs : IsOpen S
x : ℂ
hx : x ∈ S
⊢ iteratedDeriv k (fun s ↦ cexp (2 * ↑π * I * ↑m * s / ↑p)) x =
    (fun s ↦ (2 * ↑π * I * ↑m / ↑p) ^ k * cexp (2 * ↑π * I * ↑m * s / ↑p)) x
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : f =O[atTop] fun n ↦ ↑n ^ l
h0 : (fun n ↦ (2 * ↑π * I * ↑n / ↑p) ^ k) =O[atTop] fun n ↦ ↑n ^ k
⊢ (fun n ↦ f n * (2 * ↑π * I * ↑n / ↑p) ^ k) =O[atTop] fun n ↦ ↑n ^ (l + k)

Tactic:
convert! hf.mul h0

Goal state after:
case e'_8
k l : ℕ
p : ℝ
f : ℕ → ℂ
hf : f =O[atTop] fun n ↦ ↑n ^ l
h0 : (fun n ↦ (2 * ↑π * I * ↑n / ↑p) ^ k) =O[atTop] fun n ↦ ↑n ^ k
x✝ : ℕ
⊢ ↑x✝ ^ (l + k) = ↑x✝ ^ l * ↑x✝ ^ k
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: n a : ℕ
s : Set ℂ
hs : IsOpen s
r : ℂ
hr : r ∈ s
this : DifferentiableOn ℂ (iteratedDeriv a fun z ↦ cexp (2 * ↑π * I * z) ^ n) s
⊢ DifferentiableOn ℂ (iteratedDerivWithin a (fun z ↦ cexp (2 * ↑π * I * z) ^ n) s) s

Tactic:
by
    apply this.congr (iteratedDerivWithin_of_isOpen hs)

Goal state after: